--- a/src/generic-filter.agda	Wed Mar 15 12:59:55 2023 +0900
+++ b/src/generic-filter.agda	Wed Mar 15 19:44:38 2023 +0900
@@ -131,12 +131,22 @@
 gf05 {a} {b} {x} (case2 bx) nax nbx = nbx bx
 
 gf02 : {P a b : HOD } → (P ＼ a) ∩ (P ＼ b) ≡ ( P ＼ (a ∪ b) )
-gf02 {P} {a} {b} = ==→o≡  record { eq→ = gf03 ; eq← = gf04 }where
+gf02 {P} {a} {b} = ==→o≡  record { eq→ = gf03 ; eq← = gf04 } where
        gf03 : {x : Ordinal} → odef ((P ＼ a) ∩ (P ＼ b)) x → odef (P ＼ (a ∪ b)) x
        gf03 {x} ⟪ ⟪ Px , ¬ax ⟫ , ⟪ _ , ¬bx ⟫ ⟫ = ⟪ Px , (λ pab → gf05 {a} {b} {x} pab ¬ax ¬bx )   ⟫
        gf04 : {x : Ordinal} → odef (P ＼ (a ∪ b)) x → odef ((P ＼ a) ∩ (P ＼ b)) x
        gf04 {x} ⟪ Px , abx ⟫  = ⟪ ⟪ Px , (λ ax → abx (case1 ax) ) ⟫ , ⟪ Px  , (λ bx → abx (case2 bx) ) ⟫ ⟫
 
+gf45 : {P a b : HOD } → (P ＼ a) ∪ (P ＼ b) ≡ ( P ＼ (a ∩ b) )
+gf45 {P} {a} {b} = ==→o≡  record { eq→ = gf03 ; eq← = gf04 } where
+       gf03 : {x : Ordinal} → odef ((P ＼ a) ∪ (P ＼ b)) x → odef (P ＼ (a ∩ b)) x
+       gf03 {x} (case1 pa) = ⟪ proj1 pa , (λ ab → proj2 pa (proj1 ab) ) ⟫ 
+       gf03 {x} (case2 pb) = ⟪ proj1 pb , (λ ab → proj2 pb (proj2 ab) ) ⟫ 
+       gf04 : {x : Ordinal} → odef (P ＼ (a ∩ b)) x → odef ((P ＼ a) ∪ (P ＼ b)) x
+       gf04 {x} ⟪ Px , nab ⟫ with ODC.p∨¬p O (odef b x)
+       ... | case1 bx = case1 ⟪ Px , ( λ ax → nab ⟪ ax , bx ⟫ ) ⟫
+       ... | case2 nbx = case2 ⟪ Px , ( λ bx → nbx bx ) ⟫
+
 open import Data.Nat.Properties
 open import nat
 
@@ -344,17 +354,36 @@
        fd03 = record { gr = suc an ; pn<gr = λ y lt → lt ; x∈PP = fd09 (suc an)} 
        fd01 : (dense D ∩ PDHOD L p0 C) ∋ (* pn+1)
        fd01 = ⟪ subst (λ k → odef (dense D)  k ) (sym &iso) fd07 , subst (λ k → odef  (PDHOD L p0 C) k) (sym &iso) fd03 ⟫  
+    gpx→⊆P : {p : Ordinal } → odef GP p → (* p) ⊆ P
+    gpx→⊆P {p} record { z = z ; az = az ; x=ψz = x=ψz } {x} px with subst (λ k → odef k x ) 
+       (trans (cong (*) x=ψz) *iso) px
+    ... | ⟪ Px , npz ⟫ = Px
+    L∋gpr : {p : HOD } → GPR ∋ p → L ∋ (P ＼ p)
+    L∋gpr {p} record { z = z ; az = az ; x=ψz = x=ψz }  = ?
+    gpr→gp : {p : HOD} → GPR ∋ p → GP ∋ (P ＼ p ) 
+    gpr→gp {p} record { z = zp ; az = azp ; x=ψz = x=ψzp } = gfp where
+        open ≡-Reasoning
+        gfp : GP ∋ (P ＼ p ) 
+        gfp = subst (λ k → odef GP k) (begin
+           zp ≡⟨ sym &iso ⟩
+           & (* zp) ≡⟨ cong (&) (sym (L＼Lx=x (gpx→⊆P azp) )) ⟩
+           & (P ＼ (P ＼ (* zp) )) ≡⟨ cong (λ k → & ( P ＼ k)) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (sym x=ψzp)))  ⟩
+           & (P ＼ p) ∎ ) azp
     gfilter1 : {p q : HOD} → GPR ∋ p → q ⊆ p → GPR ∋ q
-    gfilter1 {p} {q} record { z = z ; az = az ; x=ψz = x=ψz } q⊆p = record { z = _ ; az = gf30 ; x=ψz = ? }  where
+    gfilter1 {p} {q} record { z = np ; az = record { z = z ; az = pdz ; x=ψz = x=ψznp } ; x=ψz = x=ψz } q⊆p = record { z = _ ; az = gf30 ; x=ψz = ? } where
+        gp =  record { z = np ; az = record { z = z ; az = pdz ; x=ψz = x=ψznp } ; x=ψz = x=ψz } 
+        q⊆P : q ⊆ P
+        q⊆P = ?
+        gf32 : (P ＼ p) ⊆ (P ＼ q)
+        gf32 = proj1 (＼-⊆ {P} {q} {p} q⊆P ) q⊆p 
         gf30 : GP ∋ (P ＼ q )
-        gf30 = f1 ? ? ?
+        gf30 = f1 ? (gpr→gp gp) gf32
     gfilter2 : {p q : HOD} → (GPR ∋ p) ∧ (GPR ∋ q) → Replace GP (_＼_ P) ∋ (p ∪ q)
-    gfilter2 {p} {q} ⟪ record { z = zp ; az = azp ; x=ψz = x=ψzp } , record { z = zq ; az = azq ; x=ψz = x=ψzq } ⟫ 
-       = record { z = _ ; az = gf31 ; x=ψz = ? } where
-        gfp : GP ∋ (P ＼ p ) 
-        gfp = ?
+    gfilter2 {p} {q} ⟪ gp , gq ⟫ 
+       = record { z = _ ; az = gf31 ; x=ψz = cong (&) ?  } where
+        open ≡-Reasoning
         gf31 : GP ∋ ( (P ＼ p ) ∩ (P ＼ q ) )
-        gf31 = f2 gfp ? ? 
+        gf31 = f2 (gpr→gp gp) (gpr→gp gq) (CAP (L∋gpr gp) (L∋gpr gq)  ) 
 
 open GenericFilter
 open Filter