# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564562888 -32400
# Node ID 684d70f1f26b3d0cb1900192394d3e3918491498
# Parent  61ff37d51230ec87208794d22d59c3f960bea1e5
...

diff -r 61ff37d51230 -r 684d70f1f26b OD.agda
--- a/OD.agda	Wed Jul 31 17:17:24 2019 +0900
+++ b/OD.agda	Wed Jul 31 17:48:08 2019 +0900
@@ -564,7 +564,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 = lemma0 
+         choice-func' X ∋-p not = have_to_find 
            where
             <-not : {X : OD {suc n}} → ( ox : Ordinal {suc n}) → Set (suc n)
             <-not {X} ox =  ( y : Ordinal {suc n}) → y o< ox → ¬ (X ∋ (ord→od y)) 
@@ -574,7 +574,14 @@
                     <-not {X} (record { lv = lx ; ord = Φ lx }) ∨ choiced X
                caseΦ lx prev with ∋-p X ( ord→od (ordinal lx (Φ lx) ))
                caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
-               caseΦ lx prev | no ¬p = {!!}
+               caseΦ lx prev | no ¬p = lemma (ordinal lx (Φ lx)) <-osuc  where
+                    lemma : (x : Ordinal {suc n}) → x o<  osuc (ordinal lx (Φ lx))
+                        → ((y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< Φ lx) → def X (od→ord (ord→od y)) → ⊥) ∨ choiced X
+                    lemma x lt with osuc-≡< lt
+                    lemma x lt | case1 refl = case1 ?
+                    lemma x lt | case2 lt1 with prev x lt1
+                    lemma x lt | case2 lt1 | case1 lt2 = case1 {!!}
+                    lemma x lt | case2 lt1 | case2 found = case2 found
                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 } )
@@ -588,10 +595,10 @@
                     lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl )
                     lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 )
                caseOSuc lx x (case2 found) | no ¬p = case2 found
-            lemma0 : choiced X
-            lemma0 with lemma-ord (od→ord X )
-            lemma0 | case1 not_found = ⊥-elim ( not ( record {
+            have_to_find : choiced X
+            have_to_find with lemma-ord (od→ord X )
+            have_to_find | case1 not_found = ⊥-elim ( not ( record {
                 eq→ = λ {x} lt → ⊥-elim (not_found x (def→o< lt)  (def-subst {suc n} {_} {_} {X} {_} lt refl (sym diso ))) ;
                 eq← = λ lt → ⊥-elim (¬x<0 lt) } ) )
-            lemma0 | case2 found = found
+            have_to_find | case2 found = found