# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1685613120 -32400
# Node ID 255b9708a308e236b1dde4023c08ef6d642e7c16
# Parent  8bf6db0b82df7593a33f5de4edb4e1f7481fbaca
it is a bad idea to use & ( * x , * x ) = osuc x
go back to original ho< restriction

diff -r 8bf6db0b82df -r 255b9708a308 src/OD.agda
--- a/src/OD.agda	Mon May 29 15:50:25 2023 +0900
+++ b/src/OD.agda	Thu Jun 01 18:52:00 2023 +0900
@@ -454,7 +454,11 @@
 
 -- ｛_｝ : ZFSet → ZFSet
 -- ｛ x ｝ = ( x ,  x )     -- better to use (x , x) directly
-
+--    (x , y ) ∋ z     x ≡  z ∨ y ≡ z
+--    (x , x )         x ≡  z ∨ x ≡ z    --- {x}  a set which contains x only 
+--             od∅ {od∅}        {od∅,{od∅}} .....
+--  Ordinal    o∅   osuc o∅      osuc (osuc o∅) ....  o< ω = next o∅
+--      (* x , * y ) ≡ omax x y
 
 data infinite-d  : ( x : Ordinal  ) → Set n where
     iφ :  infinite-d o∅
@@ -472,14 +476,8 @@
 infinite-od : OD
 infinite-od = record { def = λ x → infinite-d x } 
 
-ux=osucx : {x : Ordinal} → infinite-d x → Union (* x , (* x , * x )) ≡ (* x , * x) -- looks like wrong
-ux=osucx {.(Ordinals.o∅ O)} iφ = ?
-ux=osucx {.(& (Union (* x , (* x , * x))))} (isuc {x} ix) = ==→o≡ record { eq→ = ? ; eq← = ? } where
-       lemma10 : Union (* x , (* x , * x )) ≡ (* x , * x)
-       lemma10 = ux=osucx ix
-
-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← = lemma11 } where
+nat⊆Ord : {x : Ordinal} → infinite-d x → (Union (* x , (* x , * x ))) ⊆ Ord (osuc x)
+nat⊆Ord {.(Ordinals.o∅ O)} iφ = lemma10 where
        lemma10 : {x : Ordinal} → Own (* o∅ , (* o∅ , * o∅)) x → x o< osuc o∅
        lemma10 {x} record { owner = owner ; ao = (case1 eq) ; ox = ox } = ⊥-elim (o<¬≡ (sym &iso) (∈∅< lemma4)) where
              lemma4 : odef (* o∅) x
@@ -491,7 +489,7 @@
        lemma11 {x} lt with osuc-≡< lt
        ... | case1 eq = record { owner = _ ; ao = case2 refl ; ox = subst (λ k → odef k x) (sym *iso) (case1 (trans eq (sym &iso))) } 
        ... | case2 x<0 = ⊥-elim (¬x<0 x<0)
-nat=Ord {.(& (Union (* x , (* x , * x))))} (isuc {x} it) = ==→o≡ record { eq→ = lemma12 ; eq← = lemma14 } where
+nat⊆Ord {.(& (Union (* x , (* x , * x))))} (isuc {x} it) = lemma12 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))))
@@ -503,41 +501,41 @@
        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 (trans eq1 &iso )
        ... | case2 eq1 = o≤-refl0 (trans eq1 &iso )
-       lemma14 : {z : Ordinal} →
-            z o< osuc (& (Union (* x , (* x , * x)))) → 
-            Own (* (& (Union (* x , (* x , * x)))) , (* (& (Union (* x , (* x , * x)))) , * (& (Union (* x , (* x , * x)))))) z 
-       lemma14 {z} lt with osuc-≡< lt
-       ... | case1 eq   = record { owner = _ ; ao = case2 refl ; ox = subst (λ k → odef k z) (sym *iso) ( case2 (trans eq (sym &iso) )) } 
-       ... | case2 z<ux = record { owner = _ ; ao = case1 refl ; ox = lemma17 } where
-            lemma16 : (Union (* x , (* x , * x ))) ≡ Ord (osuc x)
-            lemma16 = nat=Ord it
-            lemma22 : {z : Ordinal} → z o< osuc x → odef (Union (* x , (* x , * x ))) z
-            lemma22 {z} z<ox = subst (λ k → odef k z) (sym lemma16) z<ox
-            lemma19 : odef (Union (* x , (* x , * x))) x
-            lemma19 = record { owner = _ ; ao = case2 refl ; ox = subst₂ (λ j k → odef j k ) (sym *iso) &iso (case1 refl) } 
-            lemma24 : x o< (& (Union (* x , (* x , * x))))
-            lemma24 = ?
-            lemma25 : osuc x ≡ (& (Union (* x , (* x , * x))))
-            lemma25 = ?
-            lemma23 : z o< osuc (& (Union (* x , (* x , * x)))) → z o< osuc x
-            lemma23 = ?
-            lemma18 : z o< osuc x
-            lemma18 = begin
-               z <⟨ z<ux ⟩
-               & (Union (* x , (* x , * x))) ≤⟨ ? ⟩
-               x ∎ where open o≤-Reasoning O
-            lemma21 : odef (Ord (osuc x)) z
-            lemma21 = lemma18
-            lemma17 : odef (* (& (* (& (Union (* x , (* x , * x))))))) z
-            lemma17 = subst (λ k → odef k z) (trans (sym lemma16) (sym (trans *iso *iso))) lemma18
+
+nat⊆Ord' : {x z : Ordinal} → infinite-d x → odef (Union (* x , (* x , * x ))) z → z o< osuc x
+nat⊆Ord' {x} {z} ix uxz = nat⊆Ord {x} ix {z} uxz 
 
 infinite : HOD
 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = osuc (& (Ord (next o∅))) ; <odmax = lemma }  
    where
+      lemma0 : {x : Ordinal} → infinite-d x → * x ⊆ Ord (next o∅)
+      lemma0 {.(Ordinals.o∅ O)} iφ = ?
+      lemma0 {.(& (Union (* _ , (* _ , * _))))} (isuc {x} ix) = subst (λ k → k ⊆ (Ord (next o∅))) (sym *iso) lemma6 where
+         lemma2 : * x ⊆ Ord (next o∅)
+         lemma2 = lemma0 ix
+         lemma5 : (Union (* x , (* x , * x))) ⊆ Ord (osuc x)
+         lemma5 = nat⊆Ord ix
+         lemma6 : (Union (* x , (* x , * x))) ⊆ Ord (next o∅)
+         lemma6 {z} lt = ordtrans (lemma5 lt ) ?
+
+
       lemma-i : {y x : Ordinal} → infinite-d y → odef (* y) x → odef (Ord (next o∅)) x
-      lemma-i = ?
+      lemma-i {.(Ordinals.o∅ O)} {x} iφ yz = ⊥-elim (¬x<0  (subst (λ k → odef k x) o∅≡od∅ yz ))
+      lemma-i {.(& (Union (* _ , (* _ , * _))))} {x} (isuc {z} iy) yz with (subst (λ k → odef k x) *iso yz)
+      ... | record { owner = owner ; ao = case1 eq ; ox = ox } = ordtrans <-osuc (osuc<nx (lemma-i {z} {x} iy ?) )
+      ... | record { owner = owner ; ao = case2 eq ; ox = ox } with (subst (λ k → odef k x) (trans (cong (*) eq) *iso )  ox)
+      ... | case1 eq1 = subst (λ k →  k o< next o∅) ? ( lemma-i {z} {x} iy ? )
+      ... | case2 eq1 = ordtrans ( nat⊆Ord iy ? ) ?
+      -- ordtrans  ? ( osuc<nx ? )
       lemma : {y : Ordinal} → infinite-d y → y o< osuc (& (Ord (next o∅)))
       lemma iy = subst₂ (λ j k → j o< k ) &iso refl ( ⊆→o≤ (lemma-i iy) )
+      lemma-j : {y : Ordinal} → infinite-d y → odef (Ord (next o∅)) y
+      lemma-j {.(Ordinals.o∅ O)} iφ = ?
+      lemma-j {.(& (Union (* _ , (* _ , * _))))} (isuc {z} iy) = ? where
+          lemma-k : odef (Ord (next o∅)) z
+          lemma-k = lemma-j iy
+          lemma-m : osuc (& (Ord (osuc z))) o< & (Ord (next o∅))
+          lemma-m = ?
 
 
 pair→ : ( x y t : HOD  ) →  (x , y)  ∋ t  → ( t =h= x ) ∨ ( t =h= y )