# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1589037539 -32400
# Node ID 2d77b6d12a2298e185642023075c14fa62c89e43
# Parent  6630dab08784e456b6d25660e8a7d9d162581498
...

diff -r 6630dab08784 -r 2d77b6d12a22 LEMC.agda
--- a/LEMC.agda	Sat May 09 22:25:12 2020 +0900
+++ b/LEMC.agda	Sun May 10 00:18:59 2020 +0900
@@ -97,7 +97,7 @@
              ch : choiced x
              ch = choice-func x ne 
              c1 : OD
-             c1 = a-choice ch
+             c1 = a-choice ch   -- x ∋ c1
              c2 : Minimal x ne
              c2 with p∨¬p ( (y : OD ) → ¬ ( def c1 (od→ord y) ∧ (def x (od→ord  y)))  )
              c2 | case1 Yes = record {
@@ -110,7 +110,7 @@
                 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 : choiced y1 --  a-choice ch1 ∈ c1 , a-choice ch1 ∈ x
                 ch1 = choice-func y1 noty1
                 c3 : Minimal x ne
                 c3 with is-o∅ (od→ord (a-choice ch1))
@@ -121,7 +121,7 @@
                   } 
                 ... | no n =  record {
                       min = min min3
-                   ;  x∋min = {!!}
+                   ;  x∋min = x∋min3 (x∋min min3)
                    ;  min-empty = min3-empty -- λ y p → min3-empty min3 y p    -- p : (min min3 ∋ y) ∧ (x ∋ y)
                   }  where
                        lemma : (a-choice ch1 == od∅ ) → od→ord (a-choice ch1) ≡ o∅ 
@@ -132,14 +132,16 @@
                          ≡⟨ ord-od∅ ⟩
                            o∅
                          ∎ where open ≡-Reasoning 
+                       --  Minimal (a-choice ch1) ch1not
+                       --      min ∈ a-choice ch1 ,  min ∩ a-choice ch1  ≡ ∅
                        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)))
-                       x∋min3 : a-choice ch1 ∋ min min3
-                       x∋min3 = x∋min min3 
+                       min3 =  prev (proj2 (is-in ch1)) (λ ch1=0 → n (lemma ch1=0))
+                       x∋min3 : a-choice ch1 ∋ min min3 → x ∋ min min3
+                       x∋min3 lt = {!!}
                        min3-empty : (y : OD ) → ¬ ((min min3 ∋ y) ∧ (x ∋ y))
-                       min3-empty y p = min-empty min3 y record { proj1 = proj1 p ; proj2 = {!!} } --  (min min3 ∋ y) ∧ (a-choice ch1 ∋ y)
+                       min3-empty y p = min-empty min3 y record { proj1 = proj1 p ; proj2 = ? } --  (min min3 ∋ y) ∧ (a-choice ch1 ∋ y)
                            -- p : (min min3 ∋ y) ∧ (x ∋ y)