--- a/src/generic-filter.agda	Sun Mar 26 20:30:46 2023 +0900
+++ b/src/generic-filter.agda	Wed Mar 29 10:25:46 2023 +0900
@@ -339,13 +339,34 @@
 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
 --
 --  We can define the valuation, but to use this, we need V=L, which makes things complicated.
---
--- 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
---   ind x valy = record { od = record { def = λ z → valS G x z  valy  } ; odmax = x ; <odmax = v02 } where
---       v02 : {z : Ordinal} → valS G x z valy → z o< x
---       v02 {z} lt = valS.z<x lt
+
+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 _  _ ) )) ⟩
+    & (* y , * y) <⟨ c<→o< (v01 _ _)  ⟩
+    & < * y , * p > <⟨ odef< xyp ⟩
+    & (* x) ≡⟨ &iso ⟩
+    x ∎ ) where
+       v00 : (x y : HOD) → odef (x , y) (& x)
+       v00 _ _ = case1 refl
+       v01 : (x y : HOD) → < x , y > ∋ (x , x)
+       v01 _ _ = case1 refl
+       open o≤-Reasoning O
+
+record valS (G : HOD) (x z : Ordinal) (val : (y : Ordinal) → y o< x → HOD): Set n where
+   field
+     y p : Ordinal
+     G∋p : odef G p
+     is-val : odef (* x) ( & < * y , * p >  )
+     z=valy : z ≡ & (val y (val< is-val))
+     z<x : z o< x
+
+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
+  ind x valy = record { od = record { def = λ z → valS G x z  valy  } ; odmax = x ; <odmax = v02 } where
+       v02 : {z : Ordinal} → valS G x z valy → z o< x
+       v02 {z} lt = valS.z<x lt
 
 --
 -- What we nedd
@@ -353,8 +374,10 @@
 --     M ⊆ M[G]
 --     M[G] ∋ G
 --     M[G] ∋ ∪G
---     L of M ≡ L of M[G]
+--
+--     assume countable L as M
 --     L is a countable subset of Power ω i.e. Power ω ∩ M
+--     it defines countable Ordinal
 --
 --  Generic Filter is a countable sequence of element of M
 --    Mg is set of all elementns of M which contains an element of G
@@ -371,8 +394,8 @@
 MgH : {L P : HOD} (LP : L ⊆ Power P) (M : HOD) (G : GenericFilter {L} {P} LP M) → HOD
 MgH {L} {P} LP M G = record { od = record { def = λ x → odef M x ∧ Mg LP M G x } ; odmax = & M ; <odmax = odef∧<  }
 
-MG : {L P : HOD} (LP : L ⊆ Power P) (M : HOD) (G : GenericFilter {L} {P} LP M) → HOD
-MG {L} {P} LP M G = M ∪ Union (MgH LP M G)
+MG1 : {L P : HOD} (LP : L ⊆ Power P) (M : HOD) (G : GenericFilter {L} {P} LP M) → HOD
+MG1 {L} {P} LP M G = M ∪ Union (MgH LP M G)
 
 TCS : (G : HOD) → Set (Level.suc n)
 TCS G = {x y : HOD} → G ∋ x → x ∋ y → G ∋ y
@@ -381,3 +404,22 @@
       → (C : CountableModel ) → HOD
 GH P L p0 LPP Lp0 C = ⊆-Ideal.ideal (genf ( P-GenericFilter P L p0 LPP Lp0 C ))
 
+module _ {L P : HOD} (LP : L ⊆ Power P) (M : HOD) (GF : GenericFilter {L} {P} LP M) where
+
+    MG = MG1 {L} {P} LP M GF 
+    G = ⊆-Ideal.ideal (genf GF)
+
+    M⊆MG : M ⊆ MG 
+    M⊆MG = case1
+
+    MG∋G : MG ∋ G
+    MG∋G = case2 record { owner = ? ; ao = ? ; ox = ? } where
+       gf00 : ?
+       gf00 = ?
+
+    MG∋UG : MG ∋ Union G
+    MG∋UG = case2 record { owner = ? ; ao = ? ; ox = ? } where
+       gf00 : ?
+       gf00 = ?
+
+