--- a/src/OD.agda	Sat May 27 18:41:04 2023 +0900
+++ b/src/OD.agda	Sun May 28 21:15:53 2023 +0900
@@ -472,31 +472,34 @@
 infinite-od : OD
 infinite-od = record { def = λ x → infinite-d x } 
 
+nat-Ord : {x : Ordinal} → infinite-d x → (Union (* x , (* x , * x ))) ≡ Ord (osuc x)
+nat-Ord {.(Ordinals.o∅ O)} iφ = ==→o≡ record { eq→ = lemma10 ; eq← = ? } where
+       lemma10 : {x : Ordinal} → Own (* o∅ , (* o∅ , * o∅)) x → x o< osuc o∅
+       lemma10 {x} record { owner = owner ; ao = (case1 eq) ; ox = ox } = ?
+       lemma10 {x} record { owner = owner ; ao = (case2 eq) ; ox = ox } with (subst (λ k → odef k x) (trans (cong (*) eq) *iso )  ox)
+       ... | case1 eq1 = ?
+       ... | case2 eq1 = ?
+       lemma11 : {x : Ordinal} → x o< osuc o∅ → Own (* o∅ , (* o∅ , * o∅)) x 
+       lemma11 {x} lt = record { owner = _ ; ao = case2 refl ; ox = ? } 
+nat-Ord {.(& (Union (* x , (* x , * x))))} (isuc {x} it) = ==→o≡ record { eq→ = ? ; eq← = ? } where
+       lemma12 : {z : Ordinal} →
+            Own (* (& (Union (* x , (* x , * x)))) , (* (& (Union (* x , (* x , * x)))) , * (& (Union (* x , (* x , * x)))))) z →
+            z o< osuc (& (Union (* x , (* x , * x))))
+       lemma12 {z} record { owner = owner ; ao = (case1 eq) ; ox = ox } = ? where
+           lemma13 : ?
+           lemma13 = ?
+       lemma12 {z} record { owner = owner ; ao = (case2 eq) ; ox = ox } with (subst (λ k → odef k z) (trans (cong (*) eq) *iso )  ox)
+       ... | case1 eq1 = o≤-refl0 ?
+       ... | case2 eq1 = ?
+
 infinite : HOD
 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = osuc (& (Ord (next o∅))) ; <odmax = lemma }  
    where
-      u : (y : Ordinal ) → HOD
-      u y = Union (* y , (* y , * y))
-      --- main recursion
+      lemma-i : {y x : Ordinal} → infinite-d y → odef (* y) x → odef (Ord (next o∅)) x
+      lemma-i = ?
       lemma : {y : Ordinal} → infinite-d y → y o< osuc (& (Ord (next o∅)))
-      lemma {o∅} iφ = b<x→0<x <-osuc 
-      lemma (isuc {y} iy) = ⊆→o≤ lemma2 where
-          lemma0 : y o< osuc (& (Ord (next o∅)))
-          lemma0 = lemma iy
-          lemma2 :  {z : Ordinal} → Own (* y , (* y , * y)) z → z o< next o∅
-          lemma2 {z} record { owner = yo ; ao = (case1 eq) ; ox = oyz } = ?
-          lemma2 {z} record { owner = yo ; ao = (case2 eq) ; ox = oyz } = ?
-      lemma-i : {y : Ordinal} → infinite-d y → * y ⊆ Ord (next o∅)
-      lemma-i {.(Ordinals.o∅ O)} iφ {x} x<0 = ⊥-elim ( empty (* x) (subst₂ (λ j k → odef j k ) o∅≡od∅ (sym &iso) x<0) )
-      lemma-i {.(& (Union (* z , (* z , * z))))} (isuc {z} iz) {x} ux = lemma3 where
-          lemma4 : * z ⊆ Ord (next o∅)
-          lemma4 = lemma-i iz
-          lemma3 : x o< next o∅
-          lemma3 with subst (λ k → odef k x) *iso ux
-          ... | record { owner = oz ; ao = case1 eq ; ox = ozx } = lemma-i iz (subst (λ k → odef k x) (trans (cong (*) eq) *iso )  ozx)
-          ... | record { owner = oz ; ao = case2 eq ; ox = ozx } with subst (λ k → odef k x) (trans (cong (*) eq) *iso ) ozx
-          ... | case1 eq1 = lemma-i iz ?
-          ... | case2 eq1 = ?
+      lemma iy = subst₂ (λ j k → j o< k ) &iso refl ( ⊆→o≤ (lemma-i iy) )
+
 
 pair→ : ( x y t : HOD  ) →  (x , y)  ∋ t  → ( t =h= x ) ∨ ( t =h= y )
 pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) *iso *iso (o≡→== t≡x ))