--- a/src/generic-filter.agda	Tue Mar 21 20:28:56 2023 +0900
+++ b/src/generic-filter.agda	Wed Mar 22 12:48:06 2023 +0900
@@ -275,12 +275,12 @@
       p⊆r : p ⊆ r
       ¬compat : (s : HOD) → L ∋ s → ¬ ( (q ⊆ s) ∧ (r ⊆ s) )
 
-lemma232 : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
+Incompatible→¬M∋G : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
       → (C : CountableModel )
       → ctl-M C ∋ L
       → ( {p : HOD} → (Lp : L ∋ p ) → Incompatible L p Lp )
       →  ¬ ( ctl-M C ∋  ⊆-Ideal.ideal (genf ( P-GenericFilter P L p0 LPP Lp0 C )))
-lemma232 P L p0 LPP Lp0 C ML NC MF = ¬G∩D=0 D∩G=0 where
+Incompatible→¬M∋G P L p0 LPP Lp0 C ML NC MF = ¬G∩D=0 D∩G=0 where
     PG = P-GenericFilter P L p0 LPP Lp0 C
     GF =  genf PG
     G =  ⊆-Ideal.ideal (genf PG)
@@ -339,10 +339,6 @@
 -- in D, we have V ≠ L
 --
 
---
---   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
---
-
 val< : {x y p : Ordinal} → odef (* x) ( & < * y , * p >  ) → y o< x
 val< {x} {y} {p} xyp = osucprev ( begin
     osuc y ≤⟨ osucc (odef< (subst (λ k → odef (* y , * y)  k) &iso (v00 _  _ ) )) ⟩
@@ -364,6 +360,9 @@
      z=valy : z ≡ & (val y (val< is-val))
      z<x : z o< x
 
+--
+--   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
+--
 val : (x : HOD) →  (G : HOD) →  HOD
 val x G = TransFinite {λ x → HOD } ind (& x) where
   ind : (x : Ordinal) → (valy : (y : Ordinal) → y o< x → HOD) → HOD
@@ -374,28 +373,24 @@
 TCS : (G : HOD) → Set (Level.suc n)
 TCS G = {x y : HOD} → G ∋ x → x ∋ y → G ∋ y
 
-lemma233 : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
-      → (C : CountableModel )
-      → ctl-M C ∋ L → {x : HOD } → ( ⊆-Ideal.ideal (genf ( P-GenericFilter P L p0 LPP Lp0 C ))) ∋ x
-      → ctl-M C ∋  val x ( ⊆-Ideal.ideal (genf ( P-GenericFilter P L p0 LPP Lp0 C )))
-lemma233 P L p0 LPP Lp0 C ML {x} Gx = subst (λ k → odef M (& (val k _))) *iso (lm00 (& x) ? ) where
-    M = ctl-M C
-    pind : (x : Ordinal) → ((y : Ordinal) → y o< x → ? → M ∋ val (* y) (PDHOD L p0 C)) → ? → M ∋ val (* x) (PDHOD L p0 C)
-    pind x prev = ?
-    lm00 : (x : Ordinal) → PDHOD L p0 C ∋ * x → M ∋ val (* x) (PDHOD L p0 C)
-    lm00  x gx = TransFinite0 {λ x →  PDHOD L p0 C ∋ * x →  M ∋ val (* x) (PDHOD L p0 C)} pind x gx
+GH : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
+      → (C : CountableModel ) → HOD
+GH P L p0 LPP Lp0 C = ⊆-Ideal.ideal (genf ( P-GenericFilter P L p0 LPP Lp0 C ))
+
+-- M ∋ x ∧ val x G ∋ val y G → M ∋ y
 
-val∋→∋p :  {G : HOD} → (TCS G) → {x y : HOD} → {p : HOD} → G ∋ p  → ( val x G ∋ val y G ) → x ∋ < y , p >
-val∋→∋p = ?
+lemma233 : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
+      → (C : CountableModel ) 
+      → {x y : HOD } → ctl-M C ∋ x
+      → val x (GH P L p0 LPP Lp0 C) ∋ val y (GH P L p0 LPP Lp0 C)
+      → ctl-M C ∋  y
+lemma233 P L p0 LPP Lp0 C {x} {y} Mx vx∋vy  = ? where
+    M = ctl-M C
+    G = ⊆-Ideal.ideal (genf ( P-GenericFilter P L p0 LPP Lp0 C ))
+    pind :  (x : Ordinal) → ((z : Ordinal) →
+             z o< x → odef M z → odef (val (* z) G) (& (val y G)) → M ∋ y) →
+            odef M x → odef (val (* x) G) (& (val y G)) → M ∋ y
+    pind  x prev Mx vxvy = ?
+    lm00 : (x : Ordinal) → odef M x → odef (val (* x) G) (& (val y G)) → M ∋ y
+    lm00 x Mx vgvy = TransFinite0 {λ x → odef M x → odef (val (* x) G) (& (val y G)) → M ∋ y} pind x Mx vgvy
 
-p∋→val∋ :  {G : HOD} → (TCS G) → {x y : HOD} → {p : HOD} → G ∋ p  → x ∋ < y , p >  → ( val x G ∋ val y G ) 
-p∋→val∋ {G} TG {x} {y} {p} Gp = subst (λ k → k ∋ < y , p >  → ( val k G ∋ val y G ) ) *iso (
-        TransFinite0 {λ x → ( * x ) ∋ < y , p >  → ( val (* x) G ∋ val y G )} ? (& x) ) where
-    pind : (x : Ordinal) → ((z : Ordinal) → z o< x → ( * z ) ∋ < y , p > → val (* z) G ∋ val y G) →
-            (* x ) ∋ < y , p > → val (* x) G ∋ val y G
-    pind x prev xyp = ?
-    -- subst (λ k → odef ( TransFinite (generic-filter.ind (* x) G) (& (* x))) (& (val y G))) ? ( 
-    --    record { y = ? ; p = ? ; G∋p = ? ; is-val = ? ; z=valy = ? ; z<x = ? } )
-
-
-