# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1565337270 -32400
# Node ID 59771eb07df0ddc668c9bbfa73c2a4accd2a5bf0
# Parent  1709c80b72754abadfbb34d8e26852ad40c9d9df
TransFinite induction fixed

diff -r 1709c80b7275 -r 59771eb07df0 Ordinals.agda
--- a/Ordinals.agda	Thu Aug 08 17:32:21 2019 +0900
+++ b/Ordinals.agda	Fri Aug 09 16:54:30 2019 +0900
@@ -13,17 +13,19 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 
-
-
-record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) : Set n where
+record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
    field
      Otrans :  {x y z : ord }  → x o< y → y o< z → x o< z
      OTri : Trichotomous {n} _≡_  _o<_ 
      ¬x<0 :   { x  : ord  } → ¬ ( x o< o∅  )
      <-osuc :  { x : ord  } → x o< osuc x
      osuc-≡< :  { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
+     TransFinite : { ψ : ord  → Set (suc n) }
+          → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : ord)  → ψ x
 
-record Ordinals {n : Level} : Set (suc n) where
+
+record Ordinals {n : Level} : Set (suc (suc n)) where
    field
      ord : Set n
      o∅ : ord
diff -r 1709c80b7275 -r 59771eb07df0 ordinal.agda
--- a/ordinal.agda	Thu Aug 08 17:32:21 2019 +0900
+++ b/ordinal.agda	Fri Aug 09 16:54:30 2019 +0900
@@ -303,10 +303,10 @@
 
 TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m }
   → ( ∀ (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 } ) )
+  → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x)  → ψ y )   → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
   →  ∀ (x : Ordinal)  → ψ x
 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 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx ox  → ψ x ) )
   TransFinite1 Zero (Φ 0) = record { proj1 = caseΦ Zero lemma ; proj2 = lemma1 } where
       lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
       lemma x (case1 ())
@@ -320,10 +320,24 @@
       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 (Φ lx)          (case1 lt) | case2 (s≤s lt1) = lemma0  lx (Φ lx) (case1 (s≤s lt1))
-      lemma lx (OSuc lx ox1)   (case1 lt) | case1 refl = caseOSuc lx ox1  ( lemma lx ox1 (case1 a<sa)) 
-      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 )}
+      lemma lx (Φ lx)          (case1 lt) | case2 lt1 = lemma0  lx (Φ lx) (case1 lt1)
+      lemma lx (OSuc lx ox1)   (case1 lt) | case1 refl = caseOSuc lx ox1 lemma2 where
+          lemma2 : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx ox1) → ψ y
+          lemma2 y lt1 with osuc-≡< lt1
+          lemma2 y lt1 | case1 refl = lemma lx ox1 (case1 a<sa)
+          lemma2 y lt1 | case2 t = proj2 (TransFinite1 lx ox1) y t 
+      lemma lx1 (OSuc lx1 ox1) (case1 lt) | case2 lt1 = caseOSuc lx1 ox1 lemma2 where
+          lemma2 : (y : Ordinal) → (Suc (lv y) ≤ lx1) ∨ (ord y d< OSuc lx1 ox1) → ψ y
+          lemma2 y lt2 with osuc-≡< lt2
+          lemma2 y lt2 | case1 refl = lemma lx1 ox1 (ordtrans lt2 (case1 lt))
+          lemma2 y lt2 | case2 (case1 lt3) = proj2 (TransFinite1 lx (Φ lx)) y (case1 (<-trans lt3 lt1 ))
+          lemma2 y lt2 | case2 (case2 lt3) with d<→lv lt3
+          ... | refl = proj2 (TransFinite1 lx (Φ lx)) y (case1 lt1)
+  TransFinite1 lx (OSuc lx ox)  = record { proj1 = caseOSuc lx ox lemma ; proj2 = lemma } where
+      lemma : (y : Ordinal) → y o< ordinal lx (OSuc lx ox) → ψ y
+      lemma y lt with osuc-≡< lt
+      lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) 
+      lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1
 
 -- we cannot prove this in intutionistic logic 
 --  (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )  → p
@@ -341,3 +355,32 @@
   → ¬ p
 TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
 
+open import Ordinals
+
+C-Ordinal : {n : Level } → Ordinals {suc n} 
+C-Ordinal {n} = record {
+     ord = Ordinal {suc n}
+   ; o∅ = o∅
+   ; osuc = osuc
+   ; _o<_ = _o<_
+   ; isOrdinal = record {
+       Otrans = ordtrans
+     ; OTri = trio<
+     ; ¬x<0 = ¬x<0 
+     ; <-osuc = <-osuc
+     ; osuc-≡< = osuc-≡<
+     ; TransFinite = TransFinite1
+   }
+  } where
+     ord1 : Set (suc n)
+     ord1 = Ordinal {suc n}
+     TransFinite1 : { ψ : ord1  → Set (suc (suc n)) }
+          → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : ord1)  → ψ x
+     TransFinite1 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
+        caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
+            ψ (record { lv = lx ; ord = Φ lx })
+        caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
+        caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
+            ψ (record { lv = lx ; ord = OSuc lx x₁ })
+        caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev