# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1678980823 -32400
# Node ID 04fc80af6f77a693320f0953e0d669cdbc82a52d
# Parent  004d8794697f568f3601ac29c4f99c2f4ed6a187
....

diff -r 004d8794697f -r 04fc80af6f77 src/generic-filter.agda
--- a/src/generic-filter.agda	Fri Mar 17 00:30:43 2023 +0900
+++ b/src/generic-filter.agda	Fri Mar 17 00:33:43 2023 +0900
@@ -130,23 +130,6 @@
 gf05 {a} {b} {x} (case1 ax) nax nbx = nax ax
 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
-       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
 
@@ -187,7 +170,7 @@
 P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0
       → (C : CountableModel ) → GenericFilter {L} {P} LP ( ctl-M C )
 P-GenericFilter P L p0 L⊆PP Lp0 C = record {
-      genf = record { ideal = PDHOD L p0 C ; i⊆L = x∈PP ; ideal1 = ideal1 ; ideal2 =  ? }
+      genf = record { ideal = PDHOD L p0 C ; i⊆L = x∈PP ; ideal1 = ideal1 ; ideal2 =  ideal2 }
     ; generic = fdense
    } where
        ideal1 : {p q : HOD} → L ∋ q → PDHOD L p0 C ∋ p → q ⊆ p → PDHOD L p0 C ∋ q