### changeset 283:2d77b6d12a22

...
author Shinji KONO Sun, 10 May 2020 00:18:59 +0900 6630dab08784 a8f9c8a27e8d LEMC.agda 1 files changed, 9 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
```--- 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)

```