--- a/VL.agda	Thu Jul 30 16:06:36 2020 +0900
+++ b/VL.agda	Thu Jul 30 17:22:34 2020 +0900
@@ -25,19 +25,48 @@
 open HOD
 
 -- The cumulative hierarchy 
---    V 0 := ∅ .
---    V β + 1 := P ( V β ) .
---    V λ := ⋃ β < λ V β .
+--    V 0 := ∅ 
+--    V α + 1 := P ( V α ) 
+--    V α := ⋃ { V β | β < α }
 
-{-# TERMINATING #-}
 V : ( β : Ordinal ) → HOD
 V β = TransFinite1  Vβ₁ β where
    Vβ₁ : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
    Vβ₁ x Vβ₀ with trio< x o∅
    Vβ₁ x Vβ₀ | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
-   Vβ₁ x Vβ₀ | tri≈ ¬a refl ¬c = od∅ 
+   Vβ₁ x Vβ₀ | tri≈ ¬a refl ¬c = Ord o∅
    Vβ₁ x Vβ₀ | tri> ¬a ¬b c with Oprev-p  x
    Vβ₁ x Vβ₀ | tri> ¬a ¬b c | yes p = Power ( Vβ₀ (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
-   Vβ₁ x Vβ₀ | tri> ¬a ¬b c | no ¬p = Vβ<α x where
-      Vβ<α : (α : Ordinal ) → HOD 
-      Vβ<α α = record { od = record { def = λ x → (x o< α ) ∧ odef (V x) x  } ; odmax = α; <odmax = λ {x} lt → proj1 lt }
+   Vβ₁ x Vβ₀ | tri> ¬a ¬b c | no ¬p = 
+        record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) →  odef (Vβ₀ y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
+
+--
+-- Definition for Power Set
+--
+record Definitions  : Set (suc n) where
+   field
+      Definition : HOD → HOD   
+
+open Definitions
+
+Df : Definitions → (x : HOD) → HOD
+Df D x = Power x ∩ Definition D x 
+
+-- The constructible Sets
+--    L 0 := ∅ 
+--    L α + 1 := Df (L α)   -- Definable Power Set
+--    V α := ⋃ { L β | β < α }
+
+L : ( β : Ordinal ) → Definitions → HOD
+L β D = TransFinite1  Lβ₁ β where
+   Lβ₁ : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
+   Lβ₁ x Lβ₀ with trio< x o∅
+   Lβ₁ x Lβ₀ | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
+   Lβ₁ x Lβ₀ | tri≈ ¬a refl ¬c = Ord o∅
+   Lβ₁ x Lβ₀ | tri> ¬a ¬b c with Oprev-p  x
+   Lβ₁ x Lβ₀ | tri> ¬a ¬b c | yes p = Df D ( Lβ₀ (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
+   Lβ₁ x Lβ₀ | tri> ¬a ¬b c | no ¬p = 
+        record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) →  odef (Lβ₀ y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
+
+V=L0 : Set (suc n)
+V=L0 = (x : Ordinal) → V x ≡  L x record { Definition = λ y → y }