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

comparison filter.agda @ 366:1a8ca713bc32

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, 18 Jul 2020 18:11:13 +0900
parents 7f919d6b045b
children f74681db63c7
comparison
equal deleted inserted replaced
365:7f919d6b045b 366:1a8ca713bc32
157 157
158 postulate 158 postulate
159 ho< : {x : HOD} → hod-ord< {x} -- : ({x : HOD} → od→ord x o< next (odmax x)) 159 ho< : {x : HOD} → hod-ord< {x} -- : ({x : HOD} → od→ord x o< next (odmax x))
160 160
161 161
162 data Hω2 : ( x : Ordinal ) → Set n where 162 data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where
163 hφ : Hω2 o∅ 163 hφ : Hω2 0 o∅
164 h0 : {x : Ordinal } → Hω2 x → 164 h0 : {i : Nat} {x : Ordinal } → Hω2 i x →
165 Hω2 (od→ord < nat→ω 0 , ord→od x >) 165 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) , ord→od x )))
166 h1 : {x : Ordinal } → Hω2 x → 166 h1 : {i : Nat} {x : Ordinal } → Hω2 i x →
167 Hω2 (od→ord < nat→ω 1 , ord→od x >) 167 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) , ord→od x )))
168 h2 : {x : Ordinal } → Hω2 x → 168 he : {i : Nat} {x : Ordinal } → Hω2 i x →
169 Hω2 (od→ord < nat→ω 2 , ord→od x >) 169 Hω2 (Suc i) x
170
171 record Hω2r (x : Ordinal) : Set n where
172 field
173 count : Nat
174 hω2 : Hω2 count x
175
176 open Hω2r
170 177
171 HODω2 : HOD 178 HODω2 : HOD
172 HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = next o∅ ; <odmax = odmax0 } where 179 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where
173 ω<next : {y : Ordinal} → infinite-d y → y o< next o∅ 180 ω<next : {y : Ordinal} → infinite-d y → y o< next o∅
174 ω<next = ω<next-o∅ ho< 181 ω<next = ω<next-o∅ ho<
175 lemma0 : {n y : Ordinal} → Hω2 y → odef infinite n → od→ord < ord→od n , ord→od y > o< next y 182 lemma : {i j : Nat} {x : Ordinal } → od→ord (Union (< nat→ω i , nat→ω j > , ord→od x)) o< next x
176 lemma0 {n} {y} hw2 inf = nexto=n {!!} 183 lemma = {!!}
177 odmax0 : {y : Ordinal} → Hω2 y → y o< next o∅ 184 odmax0 : {y : Ordinal} → Hω2r y → y o< next o∅
178 odmax0 {o∅} hφ = x<nx 185 odmax0 {y} r with hω2 r
179 odmax0 (h0 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {0} ))) 186 ... | hφ = x<nx
180 odmax0 (h1 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {1} ))) 187 ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x})
181 odmax0 (h2 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {2} ))) 188 ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x})
189 ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx
182 190
183 HODω2-Filter : Filter HODω2 191 HODω2-Filter : Filter HODω2
184 HODω2-Filter = record { 192 HODω2-Filter = record {
185 filter = {!!} 193 filter = {!!}
186 ; f⊆PL = {!!} 194 ; f⊆PL = {!!}