# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657608589 -32400
# Node ID 3de5a1fb8011a0dad148d5f530b13c73897acd82
# Parent  4df0b36db3055310a1bf0aa7a527ca4e9e638d45
...

diff -r 4df0b36db305 -r 3de5a1fb8011 src/zorn.agda
--- a/src/zorn.agda	Tue Jul 12 15:42:33 2022 +0900
+++ b/src/zorn.agda	Tue Jul 12 15:49:49 2022 +0900
@@ -536,78 +536,40 @@
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
          → (zc0 : (x : Ordinal) →  ZChain1 A f mf ay x) 
          → ((z : Ordinal) → z o< x → ZChain A f mf ay zc0 z) → ZChain A f mf ay zc0 x
-     ind f mf {y} ay x zc0 prev with trio< o∅ x
-     ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c )
-     ... | tri≈ ¬a refl ¬c = record { initial = initial1 } where
-          initial1 :  {z : Ordinal} → odef (UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) (& A)) z → * y ≤ * z 
-          initial1 {z} uz = ? where
-             zc01 : odef A z ∧ UChain A f mf ay (ZChain1.supf (zc0 (& A))) (& A) z
-             zc01 = uz
-     ... | tri< 0<x ¬b ¬c with Oprev-p x
-     ... | yes op = zc4 where
-          --
-          -- we have previous ordinal to use induction
-          --
-          px = Oprev.oprev op
-          zc : ZChain A f mf ay zc0 (Oprev.oprev op)
-          zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
-          px<x : px o< x
-          px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
-          zc0-b<x : (b : Ordinal ) → b o< x → b o< osuc px
-          zc0-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
-
-
-          zc4 : ZChain A f mf ay zc0 x 
-          zc4 = record {  chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
+     ind f mf {y} ay x zc0 prev = record {  chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
                      ; initial = pinit ; chain∋init  = pcy ; is-max = p-ismax } where
-                pchain : HOD
-                pchain = UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) (& A)
-                psupf = ZChain1.supf (zc0 (& A))
-                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 = fua } ⟫ 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 _ is-sup ) (fsuc _ fc)
-                ptotal : {a b : HOD } → odef pchain (& a) → odef pchain (& b)
-                   →   Tri ( a <  b) ( a ≡  b) ( b <  a )
-                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 _ (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) 
-                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) (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 ) →
-                        * a < * b → odef pchain b
-                p-ismax {a} {b} ua b<ox ab (case1 hasp) a<b = ⟪ ab , ? ⟫
-                p-ismax {a} {b} ua b<ox ab (case2 sup)  a<b = ⟪ ab , ? ⟫
-
-     ... | no op = zc5 where
-          uzc : {z : Ordinal} → (u : UChain A f mf ay (ZChain1.supf (zc0 (& A))) x z ) → ZChain A f mf ay zc0 (UChain.u u)
-          uzc {z} u =  prev (UChain.u u) (UChain.u<x u) 
-          UZ : HOD
-          UZ = UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) x
-          zc5 : ZChain A f mf ay zc0 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 )   
-               -- we have to check adding x preserve is-max ZChain A y f mf zc0 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 )
-          ... | 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
-
+        pchain : HOD
+        pchain = UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) (& A)
+        psupf = ZChain1.supf (zc0 (& A))
+        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 = fua } ⟫ 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 _ is-sup ) (fsuc _ fc)
+        ptotal : {a b : HOD } → odef pchain (& a) → odef pchain (& b)
+           →   Tri ( a <  b) ( a ≡  b) ( b <  a )
+        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 _ (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) 
+        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) (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 ) →
+                * a < * b → odef pchain b
+        p-ismax {a} {b} ua b<ox ab (case1 hasp) a<b = ⟪ ab , ? ⟫
+        p-ismax {a} {b} ua b<ox ab (case2 sup)  a<b = ⟪ ab , ? ⟫
          
      SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain1 A f mf ay x
      SZ0 f mf ay x = TransFinite {λ z → ZChain1 A f mf ay z} (sind f mf ay ) x