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

comparison LEMC.agda @ 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
comparison
equal deleted inserted replaced
281:81d639ee9bfd 282:6630dab08784
119 ; x∋min = def-subst {x} {od→ord (a-choice ch1)} {x} (proj2 (is-in ch1)) refl (trans eq (sym ord-od∅) ) 119 ; x∋min = def-subst {x} {od→ord (a-choice ch1)} {x} (proj2 (is-in ch1)) refl (trans eq (sym ord-od∅) )
120 ; min-empty = λ z p → ⊥-elim ( ¬x<0 (proj1 p) ) 120 ; min-empty = λ z p → ⊥-elim ( ¬x<0 (proj1 p) )
121 } 121 }
122 ... | no n = record { 122 ... | no n = record {
123 min = min min3 123 min = min min3
124 ; x∋min = ? 124 ; x∋min = {!!}
125 ; min-empty = {!!} 125 ; min-empty = min3-empty -- λ y p → min3-empty min3 y p -- p : (min min3 ∋ y) ∧ (x ∋ y)
126 } where 126 } where
127 lemma : (a-choice ch1 == od∅ ) → od→ord (a-choice ch1) ≡ o∅ 127 lemma : (a-choice ch1 == od∅ ) → od→ord (a-choice ch1) ≡ o∅
128 lemma eq = begin 128 lemma eq = begin
129 od→ord (a-choice ch1) 129 od→ord (a-choice ch1)
130 ≡⟨ cong (λ k → od→ord k ) (==→o≡ eq ) ⟩ 130 ≡⟨ cong (λ k → od→ord k ) (==→o≡ eq ) ⟩
134 ∎ where open ≡-Reasoning 134 ∎ where open ≡-Reasoning
135 ch1not : ¬ (a-choice ch1 == od∅) 135 ch1not : ¬ (a-choice ch1 == od∅)
136 ch1not ch1=0 = n (lemma ch1=0) 136 ch1not ch1=0 = n (lemma ch1=0)
137 min3 : Minimal (a-choice ch1) ch1not 137 min3 : Minimal (a-choice ch1) ch1not
138 min3 = ( prev (proj2 (is-in ch1)) (λ ch1=0 → n (lemma ch1=0))) 138 min3 = ( prev (proj2 (is-in ch1)) (λ ch1=0 → n (lemma ch1=0)))
139 x∋min3 : a-choice ch1 ∋ min min3
140 x∋min3 = x∋min min3
141 min3-empty : (y : OD ) → ¬ ((min min3 ∋ y) ∧ (x ∋ y))
142 min3-empty y p = min-empty min3 y record { proj1 = proj1 p ; proj2 = {!!} } -- (min min3 ∋ y) ∧ (a-choice ch1 ∋ y)
143 -- p : (min min3 ∋ y) ∧ (x ∋ y)
139 144
140 145
141 Min1 : (x : OD) → (ne : ¬ (x == od∅ )) → Minimal x ne 146 Min1 : (x : OD) → (ne : ¬ (x == od∅ )) → Minimal x ne
142 Min1 x ne = (ε-induction {λ y → (ne : ¬ (y == od∅ ) ) → Minimal y ne } induction x ne ) 147 Min1 x ne = (ε-induction {λ y → (ne : ¬ (y == od∅ ) ) → Minimal y ne } induction x ne )
143 minimal : (x : OD ) → ¬ (x == od∅ ) → OD 148 minimal : (x : OD ) → ¬ (x == od∅ ) → OD