# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1589029397 -32400
# Node ID 81d639ee9bfd049bdbadf4674487c4ee01ee2d9f
# Parent  a2991ce14ced1bec71dff01e8053396a4e6e7423
...

diff -r a2991ce14ced -r 81d639ee9bfd LEMC.agda
--- a/LEMC.agda	Sat May 09 17:35:56 2020 +0900
+++ b/LEMC.agda	Sat May 09 22:03:17 2020 +0900
@@ -84,32 +84,68 @@
                             eq→ = λ {x} lt → ⊥-elim  (nn x (def→o< lt) lt) 
                           ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
                         }
-         record Minimal (x : OD)  : Set (suc n) where
+         record Minimal (x : OD) (ne : ¬ (x == od∅ ) )  : Set (suc n) where
            field
                min : OD
-               x∋min :  ¬ (x == od∅ ) → x ∋ min 
-               min-empty :  ¬ (x == od∅ ) → (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
+               x∋min :   x ∋ min 
+               min-empty :  (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
          open Minimal
-         induction : {x : OD} → ({y : OD} → x ∋ y → Minimal y) → Minimal x
-         induction {x} prev = record {
-                  min = {!!}
-               ;  x∋min = {!!}
-               ;  min-empty = {!!}
-            } where
+         open _∧_
+         induction : {x : OD} → ({y : OD} → x ∋ y → (ne : ¬ (y == od∅ )) → Minimal y ne ) →  (ne : ¬ (x == od∅ )) → Minimal x ne
+         induction {x} prev ne = c2
+            where
+             ch : choiced x
+             ch = choice-func x ne 
              c1 : OD
-             c1 = a-choice (choice-func x {!!} ) 
-             c2 : OD
-             c2 with p∨¬p ( (y : OD ) →  def c1 (od→ord y) ∧ (def x (od→ord  y)))  
-             c2 | case1 _ = c1
-             c2 | case2 No =  {!!} -- minimal ( record { def = λ y → def c1 y ∧ def x y  } ) {!!}
-         Min1 : (x : OD) → Minimal x 
-         Min1 x = (ε-induction {λ y → Minimal y  } induction x ) 
+             c1 = a-choice ch
+             c2 : Minimal x ne
+             c2 with p∨¬p ( (y : OD ) → ¬ ( def c1 (od→ord y) ∧ (def x (od→ord  y)))  )
+             c2 | case1 Yes = record {
+                  min = c1
+               ;  x∋min = is-in ch 
+               ;  min-empty = Yes
+               }
+             c2 | case2 No = c3 where
+                y1 : OD
+                y1 =  record { def = λ y → ( def c1 y ∧ def x y) } 
+                noty1 : ¬ (y1 == od∅ )
+                noty1 not = ⊥-elim ( No (λ z n → ∅< n not ) )
+                ch1 : choiced y1
+                ch1 = choice-func y1 noty1
+                c3 : Minimal x ne
+                c3 with is-o∅ (od→ord (a-choice ch1))
+                ... | yes eq =  record {
+                      min = od∅
+                   ;  x∋min = def-subst {x} {od→ord (a-choice ch1)} {x} (proj2 (is-in ch1)) refl (trans eq (sym ord-od∅) ) 
+                   ;  min-empty = λ z p → ⊥-elim ( ¬x<0 (proj1 p) )
+                  } 
+                ... | no n =  record {
+                      min = min min3
+                   ;  x∋min = ?
+                   ;  min-empty = {!!}
+                  }  where
+                       lemma : (a-choice ch1 == od∅ ) → od→ord (a-choice ch1) ≡ o∅ 
+                       lemma eq = begin 
+                           od→ord (a-choice ch1) 
+                         ≡⟨ cong (λ k → od→ord k ) (==→o≡ eq ) ⟩
+                           od→ord od∅  
+                         ≡⟨ ord-od∅ ⟩
+                           o∅
+                         ∎ where open ≡-Reasoning 
+                       ch1not : ¬ (a-choice ch1 == od∅)
+                       ch1not ch1=0 = n (lemma ch1=0)
+                       min3 : Minimal (a-choice ch1) ch1not
+                       min3 = ( prev (proj2 (is-in ch1)) (λ ch1=0 → n (lemma ch1=0)))
+
+                   
+         Min1 : (x : OD) → (ne : ¬ (x == od∅ )) → Minimal x ne
+         Min1 x ne = (ε-induction {λ y → (ne : ¬ (y == od∅ ) ) → Minimal y ne } induction x ne ) 
          minimal : (x : OD  ) → ¬ (x == od∅ ) → OD 
-         minimal x not = min (Min1 x) 
+         minimal x not = min (Min1 x not ) 
          x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
-         x∋minimal x ne = x∋min (Min1 x) ne
+         x∋minimal x ne = x∋min (Min1 x ne) 
          minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
-         minimal-1 x ne y = min-empty (Min1 x) ne y
+         minimal-1 x ne y = min-empty (Min1 x ne ) y