# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564398078 -32400
# Node ID 8589660ee38808e7225316378f4b5abfe7d215b8
# Parent  b114cf5b9130fd649ab3a1f9e8b4f39dd4dfea9f
another approach

diff -r b114cf5b9130 -r 8589660ee388 OD.agda
--- a/OD.agda	Mon Jul 29 18:27:22 2019 +0900
+++ b/OD.agda	Mon Jul 29 20:01:18 2019 +0900
@@ -563,7 +563,7 @@
                 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) lemma-init 
+         choice-func' X ∋-p not = proj2 ( lemma-ord (od→ord X) )
            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)) 
@@ -571,14 +571,19 @@
             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 → {!!} )
-                
+            lemma-ord : ( ox : Ordinal {suc n} ) → <-not {X} ox ∧ choiced X
+            lemma-ord  ox = lemma1 (lv ox) (ord ox) where
+                lemma1 : (lx : Nat) ( ox : OrdinalD lx ) → <-not {X} record {lv = lx ; ord = ox} ∧ choiced X
+                lemma1 lx ox with ∋-p X (ord→od record { lv = lx ; ord = ox})
+                ... | yes p = record { proj2 = record { a-choice = ord→od record { lv = lx ; ord = ox} ; is-in = p }; proj1 = {!!} }
+                lemma1 Zero (Φ 0) | no ¬p = {!!}
+                lemma1 lx (OSuc lx ox) | no ¬p = record { proj2 = proj2 (lemma1 lx ox)  ; proj1 = {!!} }
+                lemma1 (Suc lx) (Φ (Suc lx)) | no ¬p = record { proj2 = proj2 ( lemma1 lx (Φ lx) ) ; proj1 = {!!} } where
+                    -- not : ( y : Ordinal {suc n}) →  (record { lv = Suc lx ; ord = Φ (Suc lx) }) o< osuc y → ¬ (X ∋ (ord→od y))
+                    -- we also have lemma1 lx any
+                    lemmaΦ : ( y : Ordinal {suc n}) → (record { lv = lx ; ord = Φ lx }) o< osuc y → ¬ (X ∋ (ord→od y))
+                    lemmaΦ y lt with trio<  (record { lv = Suc lx ; ord = Φ (Suc lx) }) (osuc y )
+                    lemmaΦ y lt | tri< a ¬b ¬c = {!!} -- not y a
+                    --  record { lv = lx ; ord = Φ lx }  o< osuc y o< record { lv = Suc lx ; ord = Φ (Suc lx) }
+                    lemmaΦ y lt | tri> ¬a ¬b c = {!!}
+