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

comparison OD.agda @ 204:d4802eb159ff

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Transfinite induction fixed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 31 Jul 2019 15:29:51 +0900
parents ed88384b5102
children 61ff37d51230
comparison
equal deleted inserted replaced
203:8edd2a13a7f3 204:d4802eb159ff
102 lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso) ) 102 lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso) )
103 103
104 otrans : {n : Level} {a x y : Ordinal {n} } → def (Ord a) x → def (Ord x) y → def (Ord a) y 104 otrans : {n : Level} {a x y : Ordinal {n} } → def (Ord a) x → def (Ord x) y → def (Ord a) y
105 otrans x<a y<x = ordtrans y<x x<a 105 otrans x<a y<x = ordtrans y<x x<a
106 106
107 ∅3 : {n : Level} → { x : Ordinal {n}} → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n} 107 ∅3 : {n : Level} → { x : Ordinal {suc n}} → ( ∀(y : Ordinal {suc n}) → ¬ (y o< x ) ) → x ≡ o∅ {suc n}
108 ∅3 {n} {x} = TransFinite {n} c2 c3 x where 108 ∅3 {n} {x} = TransFinite {n} c2 c3 x where
109 c0 : Nat → Ordinal {n} → Set n 109 c0 : Nat → Ordinal {suc n} → Set (suc n)
110 c0 lx x = (∀(y : Ordinal {n}) → ¬ (y o< x)) → x ≡ o∅ {n} 110 c0 lx x = (∀(y : Ordinal {suc n}) → ¬ (y o< x)) → x ≡ o∅ {suc n}
111 c2 : (lx : Nat) → c0 lx (record { lv = lx ; ord = Φ lx } ) 111 c2 : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → c0 (lv x₁) (record { lv = lv x₁ ; ord = ord x₁ }))→ c0 lx (record { lv = lx ; ord = Φ lx } )
112 c2 Zero not = refl 112 c2 Zero _ not = refl
113 c2 (Suc lx) not with not ( record { lv = lx ; ord = Φ lx } ) 113 c2 (Suc lx) _ not with not ( record { lv = lx ; ord = Φ lx } )
114 ... | t with t (case1 ≤-refl ) 114 ... | t with t (case1 ≤-refl )
115 c2 (Suc lx) not | t | () 115 c2 (Suc lx) _ not | t | ()
116 c3 : (lx : Nat) (x₁ : OrdinalD lx) → c0 lx (record { lv = lx ; ord = x₁ }) → c0 lx (record { lv = lx ; ord = OSuc lx x₁ }) 116 c3 : (lx : Nat) (x₁ : OrdinalD lx) → c0 lx (record { lv = lx ; ord = x₁ }) → c0 lx (record { lv = lx ; ord = OSuc lx x₁ })
117 c3 lx (Φ .lx) d not with not ( record { lv = lx ; ord = Φ lx } ) 117 c3 lx (Φ .lx) d not with not ( record { lv = lx ; ord = Φ lx } )
118 ... | t with t (case2 Φ< ) 118 ... | t with t (case2 Φ< )
119 c3 lx (Φ .lx) d not | t | () 119 c3 lx (Φ .lx) d not | t | ()
120 c3 lx (OSuc .lx x₁) d not with not ( record { lv = lx ; ord = OSuc lx x₁ } ) 120 c3 lx (OSuc .lx x₁) d not with not ( record { lv = lx ; ord = OSuc lx x₁ } )