Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison LEMC.agda @ 280:a2991ce14ced
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 09 May 2020 17:35:56 +0900 |
parents | 197e0b3d39dc |
children | 81d639ee9bfd |
comparison
equal
deleted
inserted
replaced
279:197e0b3d39dc | 280:a2991ce14ced |
---|---|
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 | 87 record Minimal (x : OD) : Set (suc n) where |
88 minimal-choice X ne = choice-func {!!} ne | 88 field |
89 min : OD | |
90 x∋min : ¬ (x == od∅ ) → x ∋ min | |
91 min-empty : ¬ (x == od∅ ) → (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y) | |
92 open Minimal | |
93 induction : {x : OD} → ({y : OD} → x ∋ y → Minimal y) → Minimal x | |
94 induction {x} prev = record { | |
95 min = {!!} | |
96 ; x∋min = {!!} | |
97 ; min-empty = {!!} | |
98 } where | |
99 c1 : OD | |
100 c1 = a-choice (choice-func x {!!} ) | |
101 c2 : OD | |
102 c2 with p∨¬p ( (y : OD ) → def c1 (od→ord y) ∧ (def x (od→ord y))) | |
103 c2 | case1 _ = c1 | |
104 c2 | case2 No = {!!} -- minimal ( record { def = λ y → def c1 y ∧ def x y } ) {!!} | |
105 Min1 : (x : OD) → Minimal x | |
106 Min1 x = (ε-induction {λ y → Minimal y } induction x ) | |
89 minimal : (x : OD ) → ¬ (x == od∅ ) → OD | 107 minimal : (x : OD ) → ¬ (x == od∅ ) → OD |
90 minimal x not = a-choice (minimal-choice x not ) | 108 minimal x not = min (Min1 x) |
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 ) ) | 109 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 ) | 110 x∋minimal x ne = x∋min (Min1 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) ) | 111 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 = {!!} | 112 minimal-1 x ne y = min-empty (Min1 x) ne y |
97 | 113 |
98 | 114 |
99 | 115 |
100 | 116 |