# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564398128 -32400
# Node ID 68eecbb011efb183b95b60de17fadd793024dfa3
# Parent  8589660ee38808e7225316378f4b5abfe7d215b8
curry form

diff -r 8589660ee388 -r 68eecbb011ef OD.agda
--- a/OD.agda	Mon Jul 29 20:01:18 2019 +0900
+++ b/OD.agda	Mon Jul 29 20:02:08 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 = proj2 ( lemma-ord (od→ord X) )
+         choice-func' X ∋-p not = lemma-ord (od→ord X) 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)) 
@@ -571,19 +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 = 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
+            lemma-ord : ( ox : Ordinal {suc n} ) → <-not {X} ox → choiced X
+            lemma-ord  ox not = lemma1 (lv ox) (ord ox) not where
+                lemma1 : (lx : Nat) ( ox : OrdinalD lx ) → <-not {X} record {lv = lx ; ord = ox} → choiced X
+                lemma1 lx ox not with ∋-p X (ord→od record { lv = lx ; ord = ox})
+                ... | yes p = record { a-choice = ord→od record { lv = lx ; ord = ox} ; is-in = p }
+                lemma1 Zero (Φ 0) not | no ¬p = {!!}
+                lemma1 lx (OSuc lx ox) not | no ¬p = lemma1 lx ox {!!}
+                lemma1 (Suc lx) (Φ (Suc lx)) not | no ¬p = lemma1 lx (Φ lx) lemmaΦ 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
+                    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 = {!!}