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

comparison Ordinals.agda @ 338:bca043423554

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 Sun, 12 Jul 2020 12:32:42 +0900
parents 0faa7120e4b5
children feb0fcc430a9
comparison
equal deleted inserted replaced
337:de2c472bcbcd 338:bca043423554
104 osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc 104 osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc
105 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c with osuc-≡< c 105 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c with osuc-≡< c
106 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox) 106 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox)
107 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox) 107 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox)
108 108
109 osucprev : {ox oy : Ordinal } → osuc oy o< osuc ox → oy o< ox
110 osucprev {ox} {oy} oy<ox with trio< oy ox
111 osucprev {ox} {oy} oy<ox | tri< a ¬b ¬c = a
112 osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox )
113 osucprev {ox} {oy} oy<ox | tri> ¬a ¬b c = ⊥-elim (o<> (osucc c) oy<ox )
114
109 open _∧_ 115 open _∧_
110 116
111 osuc2 : ( x y : Ordinal ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y) 117 osuc2 : ( x y : Ordinal ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
112 proj2 (osuc2 x y) lt = osucc lt 118 proj2 (osuc2 x y) lt = osucc lt
113 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy 119 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy