# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1673393885 -32400
# Node ID 4a4ac5141b95a4f4848779de9572468df146b527
# Parent  5053fd12134ab70681b98f38cdeaf3652f513828
...

diff -r 5053fd12134a -r 4a4ac5141b95 src/filter.agda
--- 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