# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564554591 -32400
# Node ID d4802eb159ff73c8b038337c2d72c89ffe6fe2d6
# Parent  8edd2a13a7f38c3e5f52c9bc53bc30667a23bea6
Transfinite induction fixed

diff -r 8edd2a13a7f3 -r d4802eb159ff OD.agda
--- 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 Φ< )
diff -r 8edd2a13a7f3 -r d4802eb159ff ordinal.agda
--- a/ordinal.agda	Wed Jul 31 12:40:02 2019 +0900
+++ b/ordinal.agda	Wed Jul 31 15:29:51 2019 +0900
@@ -331,23 +331,25 @@
   → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx)  → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
   → ( ∀ (lx : Nat ) → (x : OrdinalD lx )  → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
   →  ∀ (x : Ordinal)  → ψ x
-TransFinite {n} {m} {ψ} caseΦ caseOSuc x = TransFinite1 (lv x) (ord x) where
-  TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox)
-  TransFinite1 Zero (Φ 0) = caseΦ Zero lemma where
+TransFinite {n} {m} {ψ} caseΦ caseOSuc x = proj1 (TransFinite1 (lv x) (ord x) ) where
+  TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx)  → ψ x ) )
+  TransFinite1 Zero (Φ 0) = record { proj1 = caseΦ Zero lemma ; proj2 = lemma1 } where
       lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
       lemma x (case1 ())
       lemma x (case2 ())
-  TransFinite1 (Suc lx) (Φ (Suc lx)) = caseΦ (Suc lx) lemma where
-      lemma : (x : Ordinal) → x o< ordinal (Suc lx) (Φ (Suc lx)) → ψ x
-      lemma (ordinal lx1 ox1) (case1 lt) with <-∨ lt
-      lemma (ordinal lx (Φ lx)) (case1 lt) | case1 refl = TransFinite1 lx (Φ lx)
-      lemma (ordinal lx (OSuc lx ox1)) (case1 lt) | case1 refl = caseOSuc lx ox1 ( lemma (ordinal lx ox1) (case1 a<sa)) 
-      lemma (ordinal Zero (Φ 0)) (case1 lt) | case2 (s≤s lt1) = caseΦ Zero ( λ x lt → ⊥-elim (¬x<0 lt) )
-      lemma (ordinal (Suc lx1) (Φ (Suc lx1))) (case1 lt) | case2 (s≤s lt1) = caseΦ (Suc lx1) lemma2 where
-          lemma2 : (y : Ordinal) → (Suc (lv y) ≤ Suc lx1) ∨ (ord y d< Φ (Suc lx1)) → ψ y
-          lemma2 y (case1 lt2 ) = {!!}
-      lemma (ordinal lx1 (OSuc lx1 ox1)) (case1 lt) | case2 lt1 = caseOSuc lx1 ox1 ( lemma (ordinal lx1 ox1) (case1 (<-trans lt1 a<sa ))) 
-  TransFinite1 lx (OSuc lx ox)  = caseOSuc lx ox (TransFinite1 lx ox )
+      lemma1 : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
+      lemma1 x (case1 ())
+      lemma1 x (case2 ())
+  TransFinite1 (Suc lx) (Φ (Suc lx)) = record { proj1 = caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) ; proj2 = (λ x → lemma (lv x) (ord x)) } where
+      lemma0 : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal lx (Φ lx) → ψ (ordinal ly oy)
+      lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt
+      lemma : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy)
+      lemma lx1 ox1 (case1 lt) with <-∨ lt
+      lemma lx (Φ lx) (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) )
+      lemma lx (OSuc lx ox1) (case1 lt) | case1 refl = caseOSuc lx ox1 ( lemma lx ox1 (case1 a<sa)) 
+      lemma lx (Φ lx) (case1 lt) | case2 (s≤s lt1) = lemma0  lx (Φ lx) (case1 (s≤s lt1))
+      lemma lx1 (OSuc lx1 ox1) (case1 lt) | case2 lt1 = caseOSuc lx1 ox1 ( lemma lx1 ox1 (case1 (<-trans lt1 a<sa ))) 
+  TransFinite1 lx (OSuc lx ox)  = record { proj1 = caseOSuc lx ox (proj1 (TransFinite1 lx ox )) ; proj2 = proj2 (TransFinite1 lx ox )}
 
 -- we cannot prove this in intutionistic logic 
 --  (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )  → p