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

comparison LEMC.agda @ 279:197e0b3d39dc

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 16:41:40 +0900
parents d9d3654baee1
children a2991ce14ced
comparison
equal deleted inserted replaced
278:bfb5e807718b 279:197e0b3d39dc
82 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) 82 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
83 ¬¬X∋x nn = not record { 83 ¬¬X∋x nn = not record {
84 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) 84 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
85 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) 85 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
86 } 86 }
87 minimal-choice : (X : OD ) → ¬ (X == od∅) → choiced X
88 minimal-choice X ne = choice-func {!!} ne
89 minimal : (x : OD ) → ¬ (x == od∅ ) → OD
90 minimal x not = a-choice (minimal-choice x not )
91 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x )
92 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
93 x∋minimal x ne = is-in (minimal-choice x ne )
94 -- minimality (may proved by ε-induction )
95 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) )
96 minimal-1 x ne y = {!!}
97
98
99
87 100