Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1130:4a4ac5141b95
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 11 Jan 2023 08:38:05 +0900 |
parents | 5053fd12134a |
children | d3dbc18d2437 |
files | src/filter.agda |
diffstat | 1 files changed, 38 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/src/filter.agda Tue Jan 10 18:12:05 2023 +0900 +++ b/src/filter.agda Wed Jan 11 08:38:05 2023 +0900 @@ -183,6 +183,17 @@ mfy : odef (filter (MaximumFilter.mf mx)) y y-p⊂x : ( * y \ * p ) ⊂ * x +mu10 : {a b : HOD} → (a \ b) ⊆ a +mu10 {a} {b} {x} ⟪ ax , ¬bx ⟫ = ax + +mu11 : {a b : HOD} → o∅ o< & b → (a \ b) ⊂ a +mu11 {a} {b} 0<b = ⟪ mu12 , mu10 {a} {b} ⟫ where + mu12 : & (a \ b) o< & a + mu12 = ? + +mu13 : {a b c : HOD} → o∅ o< & b → a ⊆ c → (a \ b) ⊂ c +mu13 = ? + max→ultra : {L P : HOD} (LP : L ⊆ Power P) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p \ q)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) @@ -198,10 +209,35 @@ F = record { od = record { def = λ x → odef L x ∧ Fp {L} {P} LP mx (& p) x } ; odmax = & L ; <odmax = λ lt → odef< (proj1 lt) } mu01 : {r : HOD} {q : HOD} → L ∋ q → F ∋ r → r ⊆ q → F ∋ q - mu01 {r} {q} Lq ⟪ Lr , record { y = y ; mfy = mfy ; y-p⊂x = y-p⊂x } ⟫ r⊆q = ⟪ Lq , record { y = y ; mfy = mfy ; y-p⊂x = ? } ⟫ + mu01 {r} {q} Lq ⟪ Lr , record { y = y ; mfy = mfy ; y-p⊂x = y-p⊂x } ⟫ r⊆q = ⟪ Lq , record { y = y ; mfy = mfy ; y-p⊂x = mu03 } ⟫ where + mu05 : (* y \ p) ⊆ r + mu05 = subst₂ (λ j k → (* y \ j ) ⊆ k ) *iso *iso (proj2 y-p⊂x) + mu04 : (* y \ * (& p)) ⊆ * (& q) + mu04 {x} ⟪ yx , npx ⟫ = subst (λ k → odef k x ) (sym *iso) (r⊆q (mu05 ⟪ yx , (λ px1 → npx (subst (λ k → odef k x) (sym *iso) px1 )) ⟫ ) ) + mu03 : (* y \ * (& p)) ⊂ * (& q) + mu03 = ⟪ ordtrans<-≤ (proj1 y-p⊂x) (subst₂ (λ j k → j o≤ k) (sym &iso) (sym &iso) (⊆→o≤ r⊆q)) , mu04 ⟫ mu02 : {r : HOD} {q : HOD} → F ∋ r → F ∋ q → L ∋ (r ∩ q) → F ∋ (r ∩ q) mu02 {r} {q} ⟪ Lr , record { y = ry ; mfy = mfry ; y-p⊂x = ry-p⊂x } ⟫ - ⟪ Lq , record { y = qy ; mfy = mfqy ; y-p⊂x = qy-p⊂x } ⟫ Lrq = ⟪ Lrq , record { y = & (* qy ∩ * ry) ; mfy = ? ; y-p⊂x = ? } ⟫ + ⟪ Lq , record { y = qy ; mfy = mfqy ; y-p⊂x = qy-p⊂x } ⟫ Lrq = ⟪ Lrq , record { y = & (* qy ∩ * ry) ; mfy = mu20 ; y-p⊂x = mu22 } ⟫ where + mu21 : L ∋ (* qy ∩ * ry) + mu21 = CAP (subst (λ k → odef L k ) (sym &iso) (f⊆L mf mfqy)) (subst (λ k → odef L k ) (sym &iso) (f⊆L mf mfry)) + mu20 : odef (filter mf) (& (* qy ∩ * ry)) + mu20 = filter2 mf (subst (λ k → odef (filter mf) k) (sym &iso) mfqy) (subst (λ k → odef (filter mf) k) (sym &iso) mfry) mu21 + mu05 : & (* qy \ p) o< & q + mu05 = subst₂ (λ j k → & (* qy \ j ) o< k ) *iso &iso (proj1 qy-p⊂x) + mu06 : (* ry \ p) ⊆ r + mu06 = subst₂ (λ j k → (* ry \ j ) ⊆ k ) *iso *iso (proj2 ry-p⊂x) + mu24 : ((* qy ∩ * ry) \ * (& p)) ⊆ (r ∩ q) + mu24 {x} ⟪ qry , npx ⟫ = ⟪ subst (λ k → odef k x) *iso ( proj2 ry-p⊂x ⟪ proj2 qry , npx ⟫ ) + , subst (λ k → odef k x) *iso ( proj2 qy-p⊂x ⟪ proj1 qry , npx ⟫ ) ⟫ + mu25 : & ((* qy ∩ * ry) \ * (& p)) o≤ & (r ∩ q) + mu25 = ⊆→o≤ mu24 + mu23 : ((* qy ∩ * ry) \ * (& p) ) ⊂ (r ∩ q) + mu23 with osuc-≡< mu25 + ... | case1 eq = ? + ... | case2 lt = ⟪ lt , mu24 ⟫ + mu22 : (* (& (* qy ∩ * ry)) \ * (& p)) ⊂ * (& (r ∩ q)) + mu22 = subst₂ (λ j k → (j \ * (& p)) ⊂ k ) (sym *iso) (sym *iso) mu23 FisFilter : Filter {L} {P} LP FisFilter = record { filter = F ; f⊆L = ? ; filter1 = mu01 ; filter2 = mu02 } FisGreater : {x : Ordinal } → odef (filter (MaximumFilter.mf mx)) x → odef (filter FisFilter ) x