--- a/OD.agda	Sun Jul 12 12:32:42 2020 +0900
+++ b/OD.agda	Sun Jul 12 19:55:37 2020 +0900
@@ -103,12 +103,13 @@
   sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal 
   sup-o< :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<  sup-o A ψ 
 
---  another form of infinite
---  pair-ord< :  {x : Ordinal } → od→ord ( ord→od x , ord→od x ) o< next (od→ord x)
-
 postulate  odAxiom : ODAxiom
 open ODAxiom odAxiom
 
+-- possible restriction
+hod-ord< :  {x : HOD } → Set n
+hod-ord< {x} =  od→ord x o< next (odmax x)
+
 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD
 ¬OD-order : ( od→ord : OD  → Ordinal ) → ( ord→od : Ordinal  → OD ) → ( { x y : OD  }  → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥
 ¬OD-order od→ord ord→od c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj )
@@ -221,6 +222,9 @@
     lemma {t} (case1 refl) = omax-x  _ _
     lemma {t} (case2 refl) = omax-y  _ _
 
+--  another form of infinite
+pair-ord< :  {x : Ordinal } → Set n
+pair-ord< {x} =  od→ord ( ord→od x , ord→od x ) o< next x
 
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
@@ -370,15 +374,23 @@
     infinite : HOD 
     infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } 
 
-    -- infinite' : HOD 
-    -- infinite' = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
-    --     u : (y : Ordinal ) → HOD
-    --     u y = Union (ord→od y , (ord→od y , ord→od y))
-    --     lemma : {y : Ordinal} → infinite-d y → y o< next o∅
-    --     lemma {o∅} iφ = {!!}
-    --     lemma (isuc {y} x) = {!!} where
-    --         lemma1 : od→ord (Union (ord→od y , (ord→od y , ord→od y))) o< od→ord (Union (u y , (u y , u y )))
-    --         lemma1 = {!!}
+    infinite' : ({x : HOD} → od→ord x o< next (odmax x)) → HOD 
+    infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
+        u : (y : Ordinal ) → HOD
+        u y = Union (ord→od y , (ord→od y , ord→od y))
+        lemma : {y : Ordinal} → infinite-d y → y o< next o∅
+        lemma {o∅} iφ = proj1  next-limit
+        lemma (isuc {y} x) = lemma2 where
+            lemma0 : y o< next o∅
+            lemma0 = lemma x
+            lemma3 : odef (u y ) y 
+            lemma3 = FExists _ (λ {z} t not → not (od→ord (ord→od y , ord→od y)) record { proj1 = case2 refl ; proj2 = lemma4 }) (λ not → not y (infinite-d y)) where
+                lemma4 : def (od (ord→od (od→ord (ord→od y , ord→od y)))) y 
+                lemma4 = subst₂ ( λ j k → def (od j) k ) (sym oiso) diso (case1 refl)
+            lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))
+            lemma1 = ho<
+            lemma2 : od→ord (u y) o< next o∅
+            lemma2 = {!!}
         
 
     _=h=_ : (x y : HOD) → Set n