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

comparison ordinal.agda @ 147:c848550c8b39

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 Mon, 08 Jul 2019 19:35:23 +0900
parents 3ba37037faf4
children b97b4ee06f01
comparison
equal deleted inserted replaced
146:2eafa89733ed 147:c848550c8b39
115 ¬a≤a (s≤s lt) = ¬a≤a lt 115 ¬a≤a (s≤s lt) = ¬a≤a lt
116 116
117 =→¬< : {x : Nat } → ¬ ( x < x ) 117 =→¬< : {x : Nat } → ¬ ( x < x )
118 =→¬< {Zero} () 118 =→¬< {Zero} ()
119 =→¬< {Suc x} (s≤s lt) = =→¬< lt 119 =→¬< {Suc x} (s≤s lt) = =→¬< lt
120
121 case12-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord x d< ord y → ⊥
122 case12-⊥ {x} {y} lt1 lt2 with d<→lv lt2
123 ... | refl = nat-≡< refl lt1
124
125 case21-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord y d< ord x → ⊥
126 case21-⊥ {x} {y} lt1 lt2 with d<→lv lt2
127 ... | refl = nat-≡< refl lt1
120 128
121 o<¬≡ : {n : Level } { ox oy : Ordinal {n}} → ox ≡ oy → ox o< oy → ⊥ 129 o<¬≡ : {n : Level } { ox oy : Ordinal {n}} → ox ≡ oy → ox o< oy → ⊥
122 o<¬≡ {_} {ox} {ox} refl (case1 lt) = =→¬< lt 130 o<¬≡ {_} {ox} {ox} refl (case1 lt) = =→¬< lt
123 o<¬≡ {_} {ox} {ox} refl (case2 (s< lt)) = trio<≡ refl lt 131 o<¬≡ {_} {ox} {ox} refl (case2 (s< lt)) = trio<≡ refl lt
124 132