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

comparison LEMC.agda @ 280:a2991ce14ced

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 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