# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564367253 -32400
# Node ID 2a5844398f1cf1350bc7353fb01c51c741ac9d30
# Parent  0b9645a655426c21925e5e74815410f5f45e02b1
emulate ε-induction proof

diff -r 0b9645a65542 -r 2a5844398f1c OD.agda
--- a/OD.agda	Mon Jul 29 08:41:16 2019 +0900
+++ b/OD.agda	Mon Jul 29 11:27:33 2019 +0900
@@ -559,18 +559,18 @@
                           lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl)
 
          choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) )  → ¬ ( X == od∅ ) → OD {suc n}
-         choice-func' X ∋-p not = c
+         choice-func' X ∋-p not = lemma-ord (lv (osuc (od→ord X))) (ord (osuc (od→ord X)))  <-osuc
            where
-             ψ :  (y : OD {suc n} ) →  Set (suc (suc n))
-             ψ y =  OD {suc n} 
-             lemma : ( x : OD {suc n} )  →  ({ y : OD {suc n} } →  x ∋ y → ψ y)   → ψ x
-             lemma x prev = lemma1 (od→ord X) <-osuc  where
-                 lemma1 : (ox : Ordinal {suc n}) → ox o< osuc (od→ord X)  → OD {suc n}
-                 lemma1 ox lt with ∋-p X (ord→od ox)
-                 lemma1 ox lt | yes p = ord→od ox
-                 lemma1 record { lv = Zero ; ord = (Φ .0) } lt | no ¬p = {!!}
-                 lemma1 record { lv = Zero ; ord = (OSuc .0 ord₁) } lt | no ¬p = lemma1 record { lv = Zero ; ord = ord₁ } {!!} 
-                 lemma1 record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } lt | no ¬p = {!!}
-                 lemma1 record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } lt | no ¬p = lemma1 record { lv = Suc lv₁ ; ord = ord₁ } {!!} 
-             c : OD {suc n}
-             c = ε-induction (λ {x} → lemma x) X
+            lemma-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly }
+                → (ly < lx) ∨ (oy d< ox  ) → OD {suc n}
+            lemma-ord Zero (Φ 0) (case1 ())
+            lemma-ord Zero (Φ 0) (case2 ())
+            lemma-ord Zero (OSuc 0 ox) lt with ∋-p X (ord→od record { lv = Zero ; ord = OSuc 0 ox })
+            lemma-ord Zero (OSuc Zero ox) lt | yes p = ord→od record { lv = Zero ; ord = OSuc 0 ox }
+            lemma-ord Zero (OSuc Zero ox) {ly} {oy} lt | no ¬p = lemma-ord Zero ox {!!}
+            lemma-ord (Suc lx) (OSuc (Suc lx) ox) lt with ∋-p X (ord→od record { lv = (Suc lx)  ; ord = ox } )
+            lemma-ord (Suc lx) (OSuc (Suc lx) ox) lt | yes p = ord→od record { lv = (Suc lx)  ; ord = ox } 
+            lemma-ord (Suc lx) (OSuc (Suc lx) ox) {ly} {oy} lt | no ¬p = lemma-ord (Suc lx) ox {!!}
+            lemma-ord (Suc lx) (Φ (Suc lx)) lt with ∋-p X (ord→od record { lv = Suc lx ; ord = Φ (Suc lx)})
+            lemma-ord (Suc lx) (Φ (Suc lx)) lt | yes p = ord→od record { lv = Suc lx ; ord = Φ (Suc lx)}
+            lemma-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} lt | no ¬p = {!!}