Members/kono/Proof/ZF-in-agda: filter.agda comparison

comparison filter.agda @ 385:edbf7459a85f

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Wed, 22 Jul 2020 08:08:04 +0900
parents	171a3d587d6e
children	24a66a246316

comparison

equal deleted inserted replaced

-:171a3d587d6e
+:edbf7459a85f
 lemma Zero Zero i z≤n | i1 = refl
 lemma Zero (Suc y) i z≤n | i1 = 3⊆-[]  {3↑22 f (Suc y) i}
 lemma (Suc x) (Suc y) i (s≤s x<y) with f i
 lemma (Suc x) (Suc y) i (s≤s x<y) | i0 = lemma x y (Suc i) x<y
 lemma (Suc x) (Suc y) i (s≤s x<y) | i1 = lemma x y (Suc i) x<y
-lemma12 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j0 ∷ t))
-lemma12 s t eq = eq
-lemma13 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j1 ∷ t))
-lemma13 s t eq = eq
-lemma14 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j2 ∷ t))
-lemma14 s t eq = eq
-record Finite3 (p : List Three ) : Set  where
-field
-3-max :  Nat
-3-func :  Nat → Two
-3-p⊆f :  p 3⊆ (3-func 3↑ 3-max)
-3-f⊆p :  (3-func 3↑ 3-max) 3⊆ p
 Finite3b : (p : List Three ) → Bool
 Finite3b [] = true
 Finite3b (j0 ∷ f) = Finite3b f
 Finite3b (j1 ∷ f) = Finite3b f
 ... | hφ = x<nx
 ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x})
 ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x})
 ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx
+3→Hω2 : List Three → HOD
+3→Hω2 t = list→hod t 0 where
+list→hod : List Three → Nat → HOD
+list→hod [] _ = od∅
+list→hod (j0 ∷ t) i = Union (< nat→ω i , nat→ω 0 > , ( list→hod t (Suc i) ))
+list→hod (j1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) ))
+list→hod (j2 ∷ t) i = list→hod t (Suc i )
+Hω2→3 : (x :  HOD) → HODω2 ∋ x → List Three
+Hω2→3 x = lemma where
+lemma : { y : Ordinal } →  Hω2r y → List Three
+lemma record { count = 0 ; hω2 = hφ } = []
+lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = j0 ∷ lemma record { count = i ; hω2 =  hω3 }
+lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = j1 ∷ lemma record { count = i ; hω2 =  hω3 }
+lemma record { count = (Suc i) ; hω2 = (he hω3) } = j2 ∷ lemma record { count = i ; hω2 =  hω3 }
 ω→2 : HOD
 ω→2 = Replace (Power infinite) (λ p  → Replace infinite (λ x → < x , repl p x > )) where
 repl : HOD → HOD → HOD
 repl p x with ODC.∋-p O p x
 ... | yes _  = nat→ω 1
 ... | no _  = nat→ω 0
-record _↑n (f : HOD) (ω→2∋f : ω→2 ∋ f ) : Set n where
+ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two
--- field
+ω→2f x = {!!}
--- n : HOD
--- ? : Select f (λ x f∋x → ω→nat (π1 f∋x) < ω→nat n
+↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD
+↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) ))
--- Gf : {f : HOD} → ω→2 ∋ f  → HOD
--- Gf {f} lt = Select HODω2 (λ x H∋x → {!!}   )
+record Gfo (x : Ordinal) : Set n where
+field
+gfunc : Ordinal
+gmax : Ordinal
+gcond : (odef ω→2  gfunc) ∧ (odef infinite gmax)
+gfdef : {!!} -- ( ↑n (ord→od gfunc) (ord→od gmax) (subst₂ ? ? ? gcond) )  ⊆ ord→od x
+pcond : odef HODω2 x
+open Gfo
+HODGf : HOD
+HODGf = record { od = record { def = λ x → Gfo x } ; odmax = next o∅ ; <odmax = {!!} }
 G : (Nat → Two) → Filter HODω2
 G f = record {
-filter = {!!}
+filter = HODGf
 ; f⊆PL = {!!}
 ; filter1 = {!!}
 ; filter2 = {!!}
 } where
 filter0 : HOD

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

comparison filter.agda @ 385:edbf7459a85f