Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison Ordinals.agda @ 308:b172ab9f12bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 30 Jun 2020 00:05:16 +0900
parents 304c271b3d47
children d4802179a66f
comparison
equal deleted inserted replaced
307:d5c5d87b72df 308:b172ab9f12bc
118 maxα x y with trio< x y 118 maxα x y with trio< x y
119 maxα x y | tri< a ¬b ¬c = y 119 maxα x y | tri< a ¬b ¬c = y
120 maxα x y | tri> ¬a ¬b c = x 120 maxα x y | tri> ¬a ¬b c = x
121 maxα x y | tri≈ ¬a refl ¬c = x 121 maxα x y | tri≈ ¬a refl ¬c = x
122 122
123 minα : Ordinal → Ordinal → Ordinal 123 omin : Ordinal → Ordinal → Ordinal
124 minα x y with trio< x y 124 omin x y with trio< x y
125 minα x y | tri< a ¬b ¬c = x 125 omin x y | tri< a ¬b ¬c = x
126 minα x y | tri> ¬a ¬b c = y 126 omin x y | tri> ¬a ¬b c = y
127 minα x y | tri≈ ¬a refl ¬c = x 127 omin x y | tri≈ ¬a refl ¬c = x
128 128
129 min1 : {x y z : Ordinal } → z o< x → z o< y → z o< minα x y 129 min1 : {x y z : Ordinal } → z o< x → z o< y → z o< omin x y
130 min1 {x} {y} {z} z<x z<y with trio< x y 130 min1 {x} {y} {z} z<x z<y with trio< x y
131 min1 {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x 131 min1 {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
132 min1 {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x 132 min1 {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
133 min1 {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y 133 min1 {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y
134 134