comparison LEMC.agda @ 331:12071f79f3cf

HOD done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jul 2020 16:56:21 +0900
parents 0faa7120e4b5
children 2a8a51375e49
comparison
equal deleted inserted replaced
330:0faa7120e4b5 331:12071f79f3cf
110 p : HOD 110 p : HOD
111 p = record { od = record { def = λ y1 → odef x y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where 111 p = record { od = record { def = λ y1 → odef x y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where
112 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u) 112 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u)
113 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt)) 113 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt))
114 np : ¬ (p =h= od∅) 114 np : ¬ (p =h= od∅)
115 np p∅ = NP (λ y p∋y → ∅< p∋y p∅ ) 115 np p∅ = NP (λ y p∋y → ∅< {p} {_} p∋y p∅ )
116 y1choice : choiced p 116 y1choice : choiced p
117 y1choice = choice-func p np 117 y1choice = choice-func p np
118 y1 : HOD 118 y1 : HOD
119 y1 = a-choice y1choice 119 y1 = a-choice y1choice
120 y1prop : (x ∋ y1) ∧ (u ∋ y1) 120 y1prop : (x ∋ y1) ∧ (u ∋ y1)
124 Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u 124 Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u
125 Min2 x u u∋x = (ε-induction1 {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x ) 125 Min2 x u u∋x = (ε-induction1 {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x )
126 cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced x 126 cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced x
127 cx {x} nx = choice-func x nx 127 cx {x} nx = choice-func x nx
128 minimal : (x : HOD ) → ¬ (x =h= od∅ ) → HOD 128 minimal : (x : HOD ) → ¬ (x =h= od∅ ) → HOD
129 minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not))) 129 minimal x ne = min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne)))
130 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) ) 130 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
131 x∋minimal x ne = x∋min (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) 131 x∋minimal x ne = x∋min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne)))
132 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) 132 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) )
133 minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y 133 minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y
134 134
135 135
136 136