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

comparison generic-filter.agda @ 394:65491783aa57

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 Sun, 26 Jul 2020 21:39:27 +0900
parents 43b0a6ca7602
children 77c6123f49ee
comparison
equal deleted inserted replaced
393:43b0a6ca7602 394:65491783aa57
84 84
85 HODω2 : HOD 85 HODω2 : HOD
86 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where 86 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where
87 P : (i j : Nat) (x : Ordinal ) → HOD 87 P : (i j : Nat) (x : Ordinal ) → HOD
88 P i j x = ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , ord→od x 88 P i j x = ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , ord→od x
89 nat0 : (i : Nat) → od→ord (nat→ω i) o< next o∅ 89 nat1 : (i : Nat) (x : Ordinal) → od→ord (nat→ω i) o< next x
90 nat0 i = <odmax infinite (ω∋nat→ω {i}) 90 nat1 i x = next< nexto∅ ( <odmax infinite (ω∋nat→ω {i}))
91 lemma3 : (i j : Nat) → od→ord ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) o< next o∅
92 lemma3 i j = pair-<xy (pair-<xy (nat0 i) (nat0 i) ) (pair-<xy (nat0 i) (nat0 j) )
93 lemma1 : (i j : Nat) (x : Ordinal ) → osuc (od→ord (P i j x)) o< next x 91 lemma1 : (i j : Nat) (x : Ordinal ) → osuc (od→ord (P i j x)) o< next x
94 lemma1 i j x = osuc<nx ( next< lemma2 ho< ) where 92 lemma1 i j x = osuc<nx (pair-<xy (pair-<xy (pair-<xy (nat1 i x) (nat1 i x) ) (pair-<xy (nat1 i x) (nat1 j x) ) )
95 lemma2 : odmax (((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , ord→od x) o< next x 93 (subst (λ k → k o< next x) (sym diso) x<nx ))
96 lemma2 with trio< (od→ord ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j))) (od→ord (ord→od x))
97 | inspect (omax (od→ord ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)))) (od→ord (ord→od x))
98 lemma2 | tri< a ¬b ¬c | _ = osuc<nx (subst (λ k → k o< next x ) (sym diso) x<nx )
99 lemma2 | tri≈ ¬a b ¬c | record { eq = eq1 } = subst₂ (λ j k → j o< next k ) (trans (omax≡ _ _ b ) eq1 ) diso (osuc<nx x<nx)
100 lemma2 | tri> ¬a ¬b c | record { eq = eq1 } = osuc<nx ( next< nexto∅ (lemma3 i j))
101 lemma : (i j : Nat) (x : Ordinal ) → od→ord (Union (P i j x)) o< next x 94 lemma : (i j : Nat) (x : Ordinal ) → od→ord (Union (P i j x)) o< next x
102 lemma i j x = next< (lemma1 i j x ) ho< 95 lemma i j x = next< (lemma1 i j x ) ho<
103 odmax0 : {y : Ordinal} → Hω2r y → y o< next o∅ 96 odmax0 : {y : Ordinal} → Hω2r y → y o< next o∅
104 odmax0 {y} r with hω2 r 97 odmax0 {y} r with hω2 r
105 ... | hφ = x<nx 98 ... | hφ = x<nx
122 lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 = hω3 } 115 lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 = hω3 }
123 lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i1 ∷ lemma record { count = i ; hω2 = hω3 } 116 lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i1 ∷ lemma record { count = i ; hω2 = hω3 }
124 lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 = hω3 } 117 lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 = hω3 }
125 118
126 ω→2 : HOD 119 ω→2 : HOD
127 ω→2 = Replace (Power infinite) (λ p → Replace infinite (λ x → < x , repl p x > )) where 120 ω→2 = Power infinite
128 repl : HOD → HOD → HOD
129 repl p x with ODC.∋-p O p x
130 ... | yes _ = nat→ω 1
131 ... | no _ = nat→ω 0
132 121
133 ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two 122 ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two
134 ω→2f x = {!!} 123 ω→2f x lt n with ODC.∋-p O x (nat→ω n)
124 ω→2f x lt n | yes p = i1
125 ω→2f x lt n | no ¬p = i0
135 126
136 ↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD 127 ↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD
137 ↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) )) 128 ↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) ))
138
139 129
140 record CountableOrdinal : Set (suc (suc n)) where 130 record CountableOrdinal : Set (suc (suc n)) where
141 field 131 field
142 ctl→ : Nat → Ordinal 132 ctl→ : Nat → Ordinal
143 ctl← : Ordinal → Nat 133 ctl← : Ordinal → Nat