Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff Ordinals.agda @ 308:b172ab9f12bc
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 30 Jun 2020 00:05:16 +0900 |
| parents | 304c271b3d47 |
| children | d4802179a66f |
line wrap: on
line diff
--- a/Ordinals.agda Mon Jun 29 23:09:14 2020 +0900 +++ b/Ordinals.agda Tue Jun 30 00:05:16 2020 +0900 @@ -120,13 +120,13 @@ maxα x y | tri> ¬a ¬b c = x maxα x y | tri≈ ¬a refl ¬c = x - minα : Ordinal → Ordinal → Ordinal - minα x y with trio< x y - minα x y | tri< a ¬b ¬c = x - minα x y | tri> ¬a ¬b c = y - minα x y | tri≈ ¬a refl ¬c = x + omin : Ordinal → Ordinal → Ordinal + omin x y with trio< x y + omin x y | tri< a ¬b ¬c = x + omin x y | tri> ¬a ¬b c = y + omin x y | tri≈ ¬a refl ¬c = x - min1 : {x y z : Ordinal } → z o< x → z o< y → z o< minα x y + min1 : {x y z : Ordinal } → z o< x → z o< y → z o< omin x y min1 {x} {y} {z} z<x z<y with trio< x y min1 {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x min1 {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x