# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1678767451 -32400
# Node ID dd3debafba2d24bfa61dac962788008c6d33626b
# Parent  11049e3168adeeb0c74ddb08befa6b5d1894c24f
...

diff -r 11049e3168ad -r dd3debafba2d src/generic-filter.agda
--- a/src/generic-filter.agda	Tue Mar 14 11:58:15 2023 +0900
+++ b/src/generic-filter.agda	Tue Mar 14 13:17:31 2023 +0900
@@ -350,26 +350,37 @@
       p⊆r : p ⊆ r  
       ¬compat : (s : HOD) → ¬ ( (q ⊆ s) ∧ (r ⊆ s) )
 
-lemma232 : (P L p0 : HOD ) → (LP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
+lemma232 : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
       → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q ))  -- L is a Boolean Algebra
       → (UNI : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q ))
       → (NEG : ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)))
       → (C : CountableModel ) 
       → ( MP : ctl-M C ∋ P )
       → ( {p : HOD} → (Lp : L ∋ p ) → NotCompatible L p Lp )
-      →  ¬ ( ctl-M C ∋  rgen ( P-GenericFilter P L p0 LP Lp0 CAP UNI NEG  C ))
-lemma232 P L p0 LP Lp0 CAP UNI NEG C MP NC M∋gf = ¬gf∩D=0 record { eq→ = λ {x} gf∩D → ⊥-elim( proj2 (proj2 gf∩D) (proj1 gf∩D)) 
+      →  ¬ ( ctl-M C ∋  rgen ( P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG  C ))
+lemma232 P L p0 LPP Lp0 CAP UNI NEG C MP NC M∋gf = ¬gf∩D=0 record { eq→ = λ {x} gf∩D → ⊥-elim( proj2 (proj2 gf∩D) (proj1 gf∩D)) 
         ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where
-    gf =  rgen ( P-GenericFilter P L p0 LP Lp0 CAP UNI NEG  C )
+    gf =  rgen ( P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG  C )
     M = ctl-M C
     D : HOD  
     D = L ＼ gf
     M∋D : M ∋ D
     M∋D = ?
+    D⊆PP : D ⊆ Power P
+    D⊆PP {x} ⟪ Lx , ngx ⟫  = LPP Lx 
+    DD : Dense {L} {P} LPP
+    Dense.dense DD = D
+    Dense.d⊆P DD ⟪ Lx , _ ⟫ = Lx
+    Dense.dense-f DD Lp = ? where
+        ll00 : HOD
+        ll00 with NotCompatible.¬compat (NC Lp)
+        ... | nc = ? where
+           ll01 : {q r : HOD } → (s : HOD) → ¬ ( (q ⊆ s) ∧ (r ⊆ s)) → (¬ (gf ∋ q)) ∨ (¬ (gf ∋ q))
+           ll01 = ?
+    Dense.dense-d DD = ?
+    Dense.dense-p DD = ?
     ¬gf∩D=0 : ¬ ( (gf ∩ D) =h= od∅ )
     ¬gf∩D=0 = ?
-    gf∩D∋x :  (gf ∩ D) ∋ ?
-    gf∩D∋x = ?
 
 --
 -- P-Generic Filter defines a countable model D ⊂ C from P