# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564392442 -32400
# Node ID b114cf5b9130fd649ab3a1f9e8b4f39dd4dfea9f
# Parent  a3211dcb4d83fa347823c452332ee2c7d57277a4
transfinite

diff -r a3211dcb4d83 -r b114cf5b9130 OD.agda
--- a/OD.agda	Mon Jul 29 11:58:10 2019 +0900
+++ b/OD.agda	Mon Jul 29 18:27:22 2019 +0900
@@ -513,10 +513,10 @@
             ε-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 :  (y : OD) → ord→od record { lv = ly ; ord = oy } ∋ y → od→ord y o< record { lv = lx ; ord = ox }
-                    lemma y lt with osuc-≡< y<x
-                    lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso
-                    lemma y lt | case2 lt1 = ordtrans  (o<-subst (c<→o< lt) refl diso) lt1  
+                    lemma :  (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → od→ord z o< record { lv = lx ; ord = ox }
+                    lemma z lt with osuc-≡< y<x
+                    lemma z lt | case1 refl = o<-subst (c<→o< lt) refl diso
+                    lemma z lt | case2 lt1 = ordtrans  (o<-subst (c<→o< lt) refl diso) lt1  
             ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) =                    
                 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt )  where  
                     --
@@ -563,15 +563,22 @@
                 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 (lv (osuc (od→ord X))) (ord (osuc (od→ord X)))  <-osuc
+         choice-func' X ∋-p not = lemma-ord (od→ord X) lemma-init 
            where
-            lemma-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly }
-                → (ly < lx) ∨ (oy d< ox  ) → choiced X
-            lemma-ord Zero (Φ 0) (case1 ())
-            lemma-ord Zero (Φ 0) (case2 ())
-            lemma-ord lx (OSuc lx ox) lt with ∋-p X (ord→od record { lv = lx ; ord = OSuc lx ox })
-            lemma-ord lx (OSuc lx ox) lt | yes p = record { a-choice = ord→od record { lv = lx ; ord = OSuc lx ox } ; is-in = p } 
-            lemma-ord lx (OSuc lx ox) {ly} {oy} lt | no ¬p = lemma-ord lx ox {ly} {oy} {!!}
-            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 =  record { a-choice =  ord→od record { lv = Suc lx ; ord = Φ (Suc lx)}  ; is-in = p }
-            lemma-ord (Suc lx) (Φ .(Suc lx)) {ly} {oy} (case1 lt ) | no ¬p = {!!}
+            <-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)) 
+            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 )
+            lemma-ord : ( ox : Ordinal {suc n} ) → <-not {X} ox → choiced X
+            lemma-ord  ox = TransFinite {suc n} {suc (suc n)} {λ ox → <-not {X} ox →  choiced X  } caseΦ caseOSuc ox where
+               caseΦ : (lx : Nat) → <-not {X} (record { lv = lx ; ord = Φ lx }) → choiced X
+               caseΦ Zero n = ⊥-elim ( not {!!} )
+               caseΦ (Suc lx) n = caseΦ lx ( λ y lt → {!!} )
+               caseOSuc : (lx : Nat) (x : OrdinalD lx) → (<-not {X} (record { lv = lx ; ord = x }) → choiced X) →
+                    <-not {X} (record { lv = lx ; ord = OSuc lx x }) → choiced X
+               caseOSuc lx x prev with ∋-p X (ord→od record { lv = lx ; ord = x } )
+               caseOSuc lx x prev | yes p = λ _ → record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p }
+               caseOSuc lx x prev | no ¬p = λ px → prev ( λ y lt → {!!} )
+