Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff OD.agda @ 204:d4802eb159ff
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 |
line wrap: on
line diff
--- a/OD.agda Wed Jul 31 12:40:02 2019 +0900 +++ b/OD.agda Wed Jul 31 15:29:51 2019 +0900 @@ -104,15 +104,15 @@ otrans : {n : Level} {a x y : Ordinal {n} } → def (Ord a) x → def (Ord x) y → def (Ord a) y otrans x<a y<x = ordtrans y<x x<a -∅3 : {n : Level} → { x : Ordinal {n}} → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n} +∅3 : {n : Level} → { x : Ordinal {suc n}} → ( ∀(y : Ordinal {suc n}) → ¬ (y o< x ) ) → x ≡ o∅ {suc n} ∅3 {n} {x} = TransFinite {n} c2 c3 x where - c0 : Nat → Ordinal {n} → Set n - c0 lx x = (∀(y : Ordinal {n}) → ¬ (y o< x)) → x ≡ o∅ {n} - c2 : (lx : Nat) → c0 lx (record { lv = lx ; ord = Φ lx } ) - c2 Zero not = refl - c2 (Suc lx) not with not ( record { lv = lx ; ord = Φ lx } ) + c0 : Nat → Ordinal {suc n} → Set (suc n) + c0 lx x = (∀(y : Ordinal {suc n}) → ¬ (y o< x)) → x ≡ o∅ {suc n} + 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 } ) + c2 Zero _ not = refl + c2 (Suc lx) _ not with not ( record { lv = lx ; ord = Φ lx } ) ... | t with t (case1 ≤-refl ) - c2 (Suc lx) not | t | () + c2 (Suc lx) _ not | t | () c3 : (lx : Nat) (x₁ : OrdinalD lx) → c0 lx (record { lv = lx ; ord = x₁ }) → c0 lx (record { lv = lx ; ord = OSuc lx x₁ }) c3 lx (Φ .lx) d not with not ( record { lv = lx ; ord = Φ lx } ) ... | t with t (case2 Φ< )