Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison LEMC.agda @ 279:197e0b3d39dc
...
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 |