# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657634731 -32400
# Node ID 01a88eeb9d00acac9db4e291a36b3c486927428b
# Parent  0278f0d151f28798a6692ce368803c687e1edbb3
...

diff -r 0278f0d151f2 -r 01a88eeb9d00 src/zorn.agda
--- a/src/zorn.agda	Tue Jul 12 22:50:40 2022 +0900
+++ b/src/zorn.agda	Tue Jul 12 23:05:31 2022 +0900
@@ -477,7 +477,7 @@
      ind f mf {y} ay x prev with trio< y x
      ... | tri> ¬a ¬b c = ?
      ... | tri≈ ¬a refl ¬c = ?
-     ... | tri< 0<x ¬b ¬c with Oprev-p x
+     ... | tri< y<x ¬b ¬c with Oprev-p x
      ... | yes op = zc4 where
           --
           -- we have previous ordinal to use induction
@@ -496,6 +496,29 @@
           ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay (ZChain.supf zc) (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) 
+          psupf : Ordinal → Ordinal
+          psupf z with trio< z x 
+          ... | tri< a ¬b ¬c = ZChain.supf zc z
+          ... | tri≈ ¬a b ¬c = x
+          ... | tri> ¬a ¬b c = x
+          pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
+          pchain⊆A {y} ny = proj1 ny
+          pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
+          pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; chain∋z = ? } ⟫ where
+               afa : odef A ( f a )
+               afa = proj2 ( mf a aa )
+               fua : Chain A f mf ay psupf (UChain.u ua) (f a)
+               fua with UChain.chain∋z ua
+               ... | ch-init a fc = ch-init (f a) ( fsuc _ fc )
+               ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ ? ) (fsuc _ ? )
+          pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
+          pinit {a} ⟪ aa , ua ⟫  with UChain.chain∋z ua
+          ... | ch-init a fc = s≤fc y f mf fc
+          ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) ? where -- (s≤fc _ f mf fc)  where
+               zc7 : y << psupf (UChain.u ua)
+               zc7 = ? -- ChainP.fcy<sup is-sup (init ay)
+          pcy : odef pchain y
+          pcy = ⟪ ay , record { u =  y ; u<x = y<x ; chain∋z = ch-init _ (init ay)  }  ⟫
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
@@ -527,29 +550,6 @@
           ... | case1 is-sup = -- x is a sup of zc 
                 record {  chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
                      ; initial = pinit ; chain∋init  = pcy ; is-max = p-ismax } where
-                psupf : Ordinal → Ordinal
-                psupf z with trio< z x 
-                ... | tri< a ¬b ¬c = ZChain.supf zc z
-                ... | tri≈ ¬a b ¬c = x
-                ... | tri> ¬a ¬b c = x
-                pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
-                pchain⊆A {y} ny = proj1 ny
-                pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
-                pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; chain∋z = ? } ⟫ where
-                    afa : odef A ( f a )
-                    afa = proj2 ( mf a aa )
-                    fua : Chain A f mf ay psupf (UChain.u ua) (f a)
-                    fua with UChain.chain∋z ua
-                    ... | ch-init a fc = ch-init (f a) ( fsuc _ fc )
-                    ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ ? ) (fsuc _ ? )
-                pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
-                pinit {a} ⟪ aa , ua ⟫  with UChain.chain∋z ua
-                ... | ch-init a fc = s≤fc y f mf fc
-                ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) ? where -- (s≤fc _ f mf fc)  where
-                     zc7 : y << psupf (UChain.u ua)
-                     zc7 = ? -- ChainP.fcy<sup is-sup (init ay)
-                pcy : odef pchain y
-                pcy = ? -- ⟪ ay , record { u =  y ; u<x = ∈∧P→o< ⟪  ay , lift true  ⟫ ; chain∋z = ch-init _ (init ay)  }  ⟫
                 p-ismax :  {a b : Ordinal} → odef pchain  a →
                     b o< osuc x → (ab : odef A b) →
                     ( HasPrev A pchain ab f ∨ IsSup A pchain ab ) →
@@ -573,29 +573,50 @@
           psupf0 : (z : Ordinal) → Ordinal
           psupf0 z with trio< z x
           ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
-          ... | tri≈ ¬a b ¬c = o∅
-          ... | tri> ¬a ¬b c = o∅
-          UZ : HOD
-          UZ = UnionCF A f mf ay psupf0 x
-          total-UZ : IsTotalOrderSet UZ
-          total-UZ {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
+          ... | tri≈ ¬a b ¬c = y
+          ... | tri> ¬a ¬b c = y
+          pchain : HOD
+          pchain = UnionCF A f mf ay psupf0 x
+          ptotal : IsTotalOrderSet pchain
+          ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay psupf0 (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) 
-          usup : SUP A UZ
-          usup = supP UZ (λ lt → proj1 lt) total-UZ 
+
+          pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
+          pchain⊆A {y} ny = proj1 ny
+          pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
+          pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; chain∋z = ? } ⟫ where
+               afa : odef A ( f a )
+               afa = proj2 ( mf a aa )
+               fua : Chain A f mf ay psupf0 (UChain.u ua) (f a)
+               fua with UChain.chain∋z ua
+               ... | ch-init a fc = ch-init (f a) ( fsuc _ fc )
+               ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ ? ) (fsuc _ ? )
+          pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
+          pinit {a} ⟪ aa , ua ⟫  with UChain.chain∋z ua
+          ... | ch-init a fc = s≤fc y f mf fc
+          ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) ? where -- (s≤fc _ f mf fc)  where
+               zc7 : y << psupf0 (UChain.u ua)
+               zc7 = ? -- ChainP.fcy<sup is-sup (init ay)
+          pcy : odef pchain y
+          pcy = ⟪ ay , record { u =  y ; u<x = y<x ; chain∋z = ch-init _ (init ay)  }  ⟫
+
+          usup : SUP A pchain
+          usup = supP pchain (λ lt → proj1 lt) ptotal
           spu = & (SUP.sup usup)
           psupf : Ordinal → Ordinal
           psupf z with trio< z x 
           ... | tri< a ¬b ¬c = ZChain.supf (pzc z a) z
           ... | tri≈ ¬a b ¬c = spu
           ... | tri> ¬a ¬b c = spu
+
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = {!!} where -- ¬ A ∋ p, just skip
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A UZ ax f )   
+          ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = {!!} where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A UZ ax )
+          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
           ... | case1 is-sup = {!!} -- x is a sup of (zc ?) 
           ... | case2 ¬x=sup =  {!!} -- no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention