# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564476735 -32400
# Node ID ed88384b51026ad8ddc7274658e1eda115ff906e
# Parent  a1a7caa8b30522eb8b332738b4422833b2b40f3b
ε-induction like loop again

diff -r a1a7caa8b305 -r ed88384b5102 OD.agda
--- a/OD.agda	Tue Jul 30 01:12:24 2019 +0900
+++ b/OD.agda	Tue Jul 30 17:52:15 2019 +0900
@@ -509,8 +509,6 @@
          ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (lv (osuc (od→ord x))) (ord (osuc (od→ord x)))  <-osuc) where
             ε-induction-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly }
                 → (ly < lx) ∨ (oy d< ox  ) → ψ (ord→od (record { lv = ly ; ord = oy } ) )
-            ε-induction-ord Zero (Φ 0)  (case1 ())
-            ε-induction-ord Zero (Φ 0)  (case2 ())
             ε-induction-ord lx  (OSuc lx ox) {ly} {oy} y<x = 
                 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where
                     lemma :  (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → od→ord z o< record { lv = lx ; ord = ox }
@@ -563,23 +561,12 @@
                 a-choice : OD {suc n}
                 is-in : X ∋ a-choice
          choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) )  → ¬ ( X == od∅ ) → choiced X
-         choice-func' X ∋-p not = lemma-ord (od→ord X) (subst (λ k → <-not {X} k ) (sym diso) lemma-init )
-            where
-            <-not : {X : OD {suc n}} → ( ox : Ordinal {suc n}) → Set (suc n)
-            <-not {X} ox =  ( y : Ordinal {suc n}) → ox o< osuc y → ¬ (X ∋ (ord→od y)) 
-            ind : {x : OD} → ({y : OD} → x ∋ y → <-not {X} (od→ord y) → choiced X) → <-not {X} (od→ord x) → choiced X
-            ind {x} ψ nox = lemma (od→ord x) nox where
-                 lemma : (ox : Ordinal {suc n}) → <-not {X} ox → choiced X
-                 lemma ox nox with ∋-p X (ord→od ox)
-                 ... | yes p = record { a-choice = ord→od ox ; is-in = p }
-                 lemma record { lv = Zero ; ord = (Φ 0) } nox | no ¬p = {!!}
-                 lemma record { lv = lx ; ord = (OSuc lx ox) } nox | no ¬p = lemma record { lv = lx ; ord = ox } {!!}
-                 lemma record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } nox | no ¬p = lemma  record { lv = lx ; ord = Φ lx } lemma2 where
-                      lemma2 : ( y : Ordinal {suc n}) → record { lv = lx ; ord = Φ lx } o< osuc y → ¬ (X ∋ (ord→od y))
-                      lemma2 y lt = {!!}
-            lemma-ord : ( x : Ordinal {suc n} ) → (<-not {X} (od→ord (ord→od x))) → choiced X
-            lemma-ord x = ε-induction {n} {suc (suc n)} { λ x → (<-not {X} (od→ord x)) → choiced X} ind (ord→od x)
-            lemma-init : (y : Ordinal) → od→ord X o< osuc y → ¬ (X ∋ ord→od y)
-            lemma-init y lt lt2 with osuc-≡< lt
-            lemma-init y lt lt2 | case1 refl = o<¬≡ refl ( o<-subst (c<→o< {suc n} {_} {X} lt2) diso refl )
-            lemma-init y lt lt2 | case2 lt1 = o<> lt1 ( o<-subst (c<→o< lt2) diso refl )
+         choice-func' X ∋-p not = {!!} where
+            lemma-ord : ( lx : Nat ) (ox : OrdinalD lx ) → {ly : Nat} → {oy : OrdinalD ly }
+                → ordinal ly oy o< ordinal lx ox  → choiced X ∨ ( ¬ ( def X (ordinal ly oy) ))
+            lemma-ord lx (OSuc lx ox) y<x with ∋-p X (ord→od (ordinal lx (OSuc lx ox)))
+            lemma-ord lx (OSuc lx ox) y<x | yes p = case1 ( record { a-choice = (ord→od (ordinal lx (OSuc lx ox))) ; is-in = p } )
+            lemma-ord lx (OSuc lx ox) y<x | no ¬p with osuc-≡< y<x
+            lemma-ord lx (OSuc lx ox) y<x | no ¬p | case1 refl = {!!}
+            lemma-ord lx (OSuc lx ox) y<x | no ¬p | case2 t = lemma-ord lx ox t
+            lemma-ord (Suc lx) (Φ (Suc lx)) (case1 x) = {!!}
diff -r a1a7caa8b305 -r ed88384b5102 ordinal.agda
--- a/ordinal.agda	Tue Jul 30 01:12:24 2019 +0900
+++ b/ordinal.agda	Tue Jul 30 17:52:15 2019 +0900
@@ -13,6 +13,7 @@
    OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
 
 record Ordinal {n : Level} : Set n where
+   constructor ordinal  
    field
      lv : Nat
      ord : OrdinalD {n} lv