Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff Ordinals.agda @ 338:bca043423554
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 12 Jul 2020 12:32:42 +0900 |
parents | 0faa7120e4b5 |
children | feb0fcc430a9 |
line wrap: on
line diff
--- a/Ordinals.agda Tue Jul 07 15:32:11 2020 +0900 +++ b/Ordinals.agda Sun Jul 12 12:32:42 2020 +0900 @@ -106,6 +106,12 @@ osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox) osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox) + osucprev : {ox oy : Ordinal } → osuc oy o< osuc ox → oy o< ox + osucprev {ox} {oy} oy<ox with trio< oy ox + osucprev {ox} {oy} oy<ox | tri< a ¬b ¬c = a + osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox ) + osucprev {ox} {oy} oy<ox | tri> ¬a ¬b c = ⊥-elim (o<> (osucc c) oy<ox ) + open _∧_ osuc2 : ( x y : Ordinal ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)