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

comparison ordinal.agda @ 94:4659a815b70d

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 Sat, 08 Jun 2019 13:18:10 +0900
parents b4742cf4ef97
children f2b579106770
comparison
equal deleted inserted replaced
93:d382a7902f5e 94:4659a815b70d
106 nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥ 106 nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥
107 nat-≡< refl lt = nat-<≡ lt 107 nat-≡< refl lt = nat-<≡ lt
108 108
109 ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥ 109 ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
110 ¬a≤a (s≤s lt) = ¬a≤a lt 110 ¬a≤a (s≤s lt) = ¬a≤a lt
111
112 =→¬< : {x : Nat } → ¬ ( x < x )
113 =→¬< {Zero} ()
114 =→¬< {Suc x} (s≤s lt) = =→¬< lt
115
116 o<¬≡ : {n : Level } ( ox oy : Ordinal {n}) → ox ≡ oy → ox o< oy → ⊥
117 o<¬≡ ox ox refl (case1 lt) = =→¬< lt
118 o<¬≡ ox ox refl (case2 (s< lt)) = trio<≡ refl lt
119
120 ¬x<0 : {n : Level} → { x : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
121 ¬x<0 {n} {x} (case1 ())
122 ¬x<0 {n} {x} (case2 ())
111 123
112 o<> : {n : Level} → {x y : Ordinal {n} } → y o< x → x o< y → ⊥ 124 o<> : {n : Level} → {x y : Ordinal {n} } → y o< x → x o< y → ⊥
113 o<> {n} {x} {y} (case1 x₁) (case1 x₂) = nat-<> x₁ x₂ 125 o<> {n} {x} {y} (case1 x₁) (case1 x₂) = nat-<> x₁ x₂
114 o<> {n} {x} {y} (case1 x₁) (case2 x₂) = nat-≡< (sym (d<→lv x₂)) x₁ 126 o<> {n} {x} {y} (case1 x₁) (case2 x₂) = nat-≡< (sym (d<→lv x₂)) x₁
115 o<> {n} {x} {y} (case2 x₁) (case1 x₂) = nat-≡< (sym (d<→lv x₁)) x₂ 127 o<> {n} {x} {y} (case2 x₁) (case1 x₂) = nat-≡< (sym (d<→lv x₁)) x₂