# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1685343025 -32400
# Node ID 8bf6db0b82df7593a33f5de4edb4e1f7481fbaca
# Parent  95b62a08c3d0ccc39d92c20dae608a9fc3f4944f
...

diff -r 95b62a08c3d0 -r 8bf6db0b82df src/OD.agda
--- a/src/OD.agda	Mon May 29 09:29:28 2023 +0900
+++ b/src/OD.agda	Mon May 29 15:50:25 2023 +0900
@@ -472,6 +472,12 @@
 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
        lemma10 : {x : Ordinal} → Own (* o∅ , (* o∅ , * o∅)) x → x o< osuc o∅
@@ -505,13 +511,23 @@
        ... | 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