Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 282:6630dab08784

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 May 2020 22:25:12 +0900
parents 81d639ee9bfd
children 2d77b6d12a22
files LEMC.agda
diffstat 1 files changed, 7 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/LEMC.agda	Sat May 09 22:03:17 2020 +0900
+++ b/LEMC.agda	Sat May 09 22:25:12 2020 +0900
@@ -121,8 +121,8 @@
                   } 
                 ... | no n =  record {
                       min = min min3
-                   ;  x∋min = ?
-                   ;  min-empty = {!!}
+                   ;  x∋min = {!!}
+                   ;  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∅ 
                        lemma eq = begin 
@@ -136,6 +136,11 @@
                        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-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)
+                           -- p : (min min3 ∋ y) ∧ (x ∋ y)
 
                    
          Min1 : (x : OD) → (ne : ¬ (x == od∅ )) → Minimal x ne