# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657371099 -32400
# Node ID 663b34227faf586d55da590cf86c6182b8b3c2ea
# Parent  c5c8e37d9a6c3cdb47e6e2951bc9ad3855667758
...

diff -r c5c8e37d9a6c -r 663b34227faf src/zorn.agda
--- a/src/zorn.agda	Sat Jul 09 18:36:23 2022 +0900
+++ b/src/zorn.agda	Sat Jul 09 21:51:39 2022 +0900
@@ -465,33 +465,23 @@
      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 = zc4 where
-          zc : {z1 : Ordinal} → z1 o< x → ZChain A f mf ay zc0 z1
-          zc z1 with Oprev-p x
-          ... | yes op = ? where
-              --
-              -- we have previous ordinal to use induction
-              --
-              px = Oprev.oprev op
-              supf : Ordinal → HOD
-              supf x =  ? -- ChainF A f mf ay x zc0 
-              -- 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
-          ... | no ¬ox = ? where
-             supf : Ordinal → HOD
-             supf x = ? -- Z?Chain1.chain zc0 
-             uzc : {z : Ordinal} → (u : UChain 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 = record { od = record { def = λ z → odef A z ∧ ( UChain z {!!} x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!}  }
-
+     ind f mf {y} ay x zc0 prev with Oprev-p x
+     ... | yes op = ? where
+          --
+          -- we have previous ordinal to use induction
+          --
+          px = Oprev.oprev op
+          supf : Ordinal → HOD
+          supf x =  ? -- ChainF A f mf ay x zc0 
+          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
           -- if previous chain satisfies maximality, we caan reuse it
           --
-          no-extenion : ( {a b z : Ordinal} → (z<x : z o< x)  → odef (ZChain.chain (zc z<x )) a → b o< osuc x → (ab : odef A b) →
-                    HasPrev A (ZChain.chain (zc z<x) ) ab f ∨  IsSup A (ZChain.chain (zc z<x) ) ab →
-                            * a < * b → odef (ZChain.chain (zc ?) ) b ) → ZChain A f mf ay zc0 x
+          no-extenion : ( {a b z : Ordinal} → (z<x : z o< x)  → odef (ZChain.chain ?) a → b o< osuc x → (ab : odef A b) →
+                    HasPrev A (ZChain.chain zc ) ab f ∨  IsSup A (ZChain.chain ? ) ab →
+                            * a < * b → odef (ZChain.chain zc ) b ) → ZChain A f mf ay zc0 x
           no-extenion is-max = ? 
 
           zc4 : ZChain A f mf ay zc0 x 
@@ -499,29 +489,29 @@
           ... | yes x=0 = ?
           ... | no 0<x with ODC.∋-p O A (* x)
           ... | no noax = no-extenion zc1  where -- ¬ A ∋ p, just skip
-                zc1 : {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain (zc z<x) ) a → b o< osuc x → (ab : odef A b) →
-                    HasPrev A (ZChain.chain (zc ?) ) ab f ∨  IsSup A (ZChain.chain (zc z<x) ) ab →
-                            * a < * b → odef (ZChain.chain (zc z<x) ) b
+                zc1 : {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc ) a → b o< osuc x → (ab : odef A b) →
+                    HasPrev A (ZChain.chain zc ) ab f ∨  IsSup A (ZChain.chain zc ) ab →
+                            * a < * b → odef (ZChain.chain zc ) b
                 zc1 {a} {b} z<x za b<ox ab P a<b with osuc-≡< b<ox
                 ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
-                ... | case2 lt = ZChain.is-max (zc z<x) za ?  ab P a<b
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain (zc ? ) ) ax f )   
+                ... | case2 lt = ZChain.is-max zc za ?  ab P a<b
+          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f )   
                -- we have to check adding x preserve is-max ZChain A y f mf zc0 x
           ... | case1 pr = no-extenion zc7  where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
-                chain0 = ZChain.chain (zc ? ) 
-                zc7 :  {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain (zc z<x) ) a → b o< osuc x → (ab : odef A b) →
-                            HasPrev A (ZChain.chain (zc z<x) ) ab f ∨ IsSup A (ZChain.chain (zc z<x) ) ab →
-                            * a < * b → odef (ZChain.chain (zc z<x) ) b
+                chain0 = ZChain.chain zc 
+                zc7 :  {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc ) a → b o< osuc x → (ab : odef A b) →
+                            HasPrev A (ZChain.chain zc ) ab f ∨ IsSup A (ZChain.chain zc ) ab →
+                            * a < * b → odef (ZChain.chain zc ) b
                 zc7 {a} {b} z<x za b<ox ab P a<b with osuc-≡< b<ox
-                ... | case2 lt = ZChain.is-max (zc z<x) za ? ab P a<b
-                ... | case1 b=x = ? -- subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next (zc z<x) (HasPrev.ay pr))
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain (zc ?) ) ax )
-          ... | case1 is-sup = -- x is a sup of (zc ?) 
+                ... | case2 lt = ZChain.is-max zc za ? ab P a<b
+                ... | case1 b=x = ? -- subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
+          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
+          ... | case1 is-sup = -- x is a sup of zc 
                 record {  chain⊆A = {!!} ; f-next = {!!}  ; f-total = {!!}
                      ; initial = {!!} ; chain∋init  = {!!} ; is-max = {!!}   } where
-                sup0 : SUP A (ZChain.chain (zc ?) ) 
+                sup0 : SUP A (ZChain.chain zc ) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
-                        x21 :  {y : HOD} → ZChain.chain (zc ?) ∋ y → (y ≡ * x) ∨ (y < * x)
+                        x21 :  {y : HOD} → ZChain.chain zc ∋ y → (y ≡ * x) ∨ (y < * x)
                         x21 {y} zy with IsSup.x<sup is-sup zy 
                         ... | case1 y=x = case1 ( subst₂ (λ j k → j ≡ * k  ) *iso &iso ( cong (*) y=x)  )
                         ... | case2 y<x = case2 (subst₂ (λ j k → j < * k ) *iso &iso y<x  )
@@ -529,9 +519,9 @@
                 sp = SUP.sup sup0 
                 x=sup : x ≡ & sp 
                 x=sup = sym &iso 
-                chain0 = ZChain.chain (zc ?) 
+                chain0 = ZChain.chain zc 
                 sc<A : {y : Ordinal} → odef chain0 y ∨ FClosure A f (& sp) y → y o< & A
-                sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< (ZChain.chain⊆A (zc ?) (subst (λ k → odef chain0 k) (sym &iso) zx )))
+                sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< (ZChain.chain⊆A zc (subst (λ k → odef chain0 k) (sym &iso) zx )))
                 sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) )
                 schain : HOD
                 schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
@@ -541,10 +531,10 @@
                 ... | tri≈ ¬a b ¬c = schain 
                 ... | tri> ¬a ¬b c = schain
                 A∋schain : {x : HOD } → schain ∋ x → A ∋ x
-                A∋schain (case1 zx ) = ZChain.chain⊆A (zc ?) zx 
+                A∋schain (case1 zx ) = ZChain.chain⊆A zc zx 
                 A∋schain {y} (case2 fx ) = A∋fc (& sp) f mf fx 
                 s⊆A : schain ⊆' A
-                s⊆A {x} (case1 zx) = ZChain.chain⊆A (zc ?) zx
+                s⊆A {x} (case1 zx) = ZChain.chain⊆A zc zx
                 s⊆A {x} (case2 fx) = A∋fc (& sp) f mf fx 
                 cmp  : {a b : HOD} (za : odef chain0 (& a)) (fb : FClosure A f (& sp) (& b)) → Tri (a < b) (a ≡ b) (b < a )
                 cmp {a} {b} za fb  with SUP.x<sup sup0 za | s≤fc (& sp) f mf fb  
@@ -561,7 +551,7 @@
                         a<b : a < b
                         a<b = ptrans  (subst (λ k → a < k ) (sym *iso) a<sp ) ( subst₂ (λ j k → j < k ) refl *iso sp<b )
                 scmp : {a b : HOD} → odef schain (& a) → odef schain (& b) → Tri (a < b) (a ≡ b) (b < a )
-                scmp {a} {b} (case1 za) (case1 zb) = {!!} -- ZChain.f-total (zc ?) {px} {px} o≤-refl za zb
+                scmp {a} {b} (case1 za) (case1 zb) = {!!} -- ZChain.f-total zc {px} {px} o≤-refl za zb
                 scmp {a} {b} (case1 za) (case2 fb) = cmp za fb 
                 scmp  (case2 fa) (case1 zb) with  cmp zb fa
                 ... | tri< a ¬b ¬c = tri> ¬c (λ eq → ¬b (sym eq))  a
@@ -569,17 +559,17 @@
                 ... | tri> ¬a ¬b c = tri< c (λ eq → ¬b (sym eq))  ¬a
                 scmp (case2 fa) (case2 fb) = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp (& sp) f mf fa fb)
                 scnext : {a : Ordinal} → odef schain a → odef schain (f a)
-                scnext {x} (case1 zx) = case1 (ZChain.f-next (zc ?) zx)
+                scnext {x} (case1 zx) = case1 (ZChain.f-next zc zx)
                 scnext {x} (case2 sx) = case2 ( fsuc x sx )
                 scinit :  {x : Ordinal} → odef schain x → * y ≤ * x
-                scinit {x} (case1 zx) = ZChain.initial (zc ?) zx
-                scinit {x} (case2 sx) with  (s≤fc (& sp) f mf sx ) |  SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) ( ZChain.chain∋init (zc ?) ) )
+                scinit {x} (case1 zx) = ZChain.initial zc zx
+                scinit {x} (case2 sx) with  (s≤fc (& sp) f mf sx ) |  SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) ( ZChain.chain∋init zc ) )
                 ... | case1 sp=x | case1 y=sp = case1 (trans y=sp (subst (λ k → k ≡ * x ) *iso sp=x ) )
                 ... | case1 sp=x | case2 y<sp = case2 (subst (λ k → * y < k ) (trans (sym *iso) sp=x) y<sp )
                 ... | case2 sp<x | case1 y=sp = case2 (subst (λ k → k < * x ) (trans *iso (sym y=sp )) sp<x )
                 ... | case2 sp<x | case2 y<sp = case2 (ptrans y<sp (subst (λ k → k < * x ) *iso sp<x) )
                 A∋za : {a : Ordinal } → odef chain0 a → odef A a
-                A∋za za = ZChain.chain⊆A (zc ?) za 
+                A∋za za = ZChain.chain⊆A zc za 
                 za<sup :  {a : Ordinal } → odef chain0 a → ( * a ≡ sp ) ∨  ( * a < sp )
                 za<sup za =  SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) za )
                 s-ismax : {a b : Ordinal} → odef schain a → b o< osuc x → (ab : odef A b)
@@ -590,21 +580,21 @@
                 s-ismax {a} {b} (case1 za) b<ox ab (case1 p) a<b | case2 b<x = z21 p where   -- has previous
                      z21 : HasPrev A schain ab f → odef schain b
                      z21 record { y = y ; ay = (case1 zy) ; x=fy = x=fy } = 
-                           case1 (ZChain.is-max (zc ?) za ? ab (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b )
+                           case1 (ZChain.is-max zc za ? ab (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b )
                      z21 record { y = y ; ay = (case2 sy) ; x=fy = x=fy } = subst (λ k → odef schain k) (sym x=fy) (case2 (fsuc y sy) )
-                s-ismax {a} {b} (case1 za) b<ox ab (case2 p) a<b | case2 b<x = case1 (ZChain.is-max (zc ?) za ? ab (case2 z22) a<b ) where -- previous sup
-                     z22 : IsSup A (ZChain.chain (zc ?) )   ab 
+                s-ismax {a} {b} (case1 za) b<ox ab (case2 p) a<b | case2 b<x = case1 (ZChain.is-max zc za ? ab (case2 z22) a<b ) where -- previous sup
+                     z22 : IsSup A (ZChain.chain zc )   ab 
                      z22 = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) }
                 s-ismax {a} {b} (case2 sa) b<ox ab (case1 p)  a<b | case2 b<x with HasPrev.ay p
-                ... | case1 zy = case1 (subst (λ k → odef chain0 k ) (sym (HasPrev.x=fy p)) (ZChain.f-next (zc ?) zy ))               -- in previous closure of f
+                ... | case1 zy = case1 (subst (λ k → odef chain0 k ) (sym (HasPrev.x=fy p)) (ZChain.f-next zc zy ))               -- in previous closure of f
                 ... | case2 sy = case2 (subst (λ k → FClosure A f (& (* x)) k ) (sym (HasPrev.x=fy p)) (fsuc (HasPrev.y p) sy ))  -- in current  closure of f
                 s-ismax {a} {b} (case2 sa) b<ox ab (case2 p)  a<b | case2 b<x = case1 z23 where -- sup o< x is already in zc
-                     z24 : IsSup A schain ab → IsSup A (ZChain.chain (zc ?) ) ab 
+                     z24 : IsSup A schain ab → IsSup A (ZChain.chain zc ) ab 
                      z24 p = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) }
                      z23 : odef chain0 b
-                     z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋init (zc ?) )
-                     ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋init (zc ?) )
-                     ... | case2 y<b  = ZChain.is-max (zc ?) (ZChain.chain∋init (zc ?) ) ? ab (case2 (z24 p)) y<b
+                     z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋init zc )
+                     ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋init zc )
+                     ... | case2 y<b  = ZChain.is-max zc (ZChain.chain∋init zc ) ? ab (case2 (z24 p)) y<b
                 seq : schain ≡ supf0 x 
                 seq with trio< x x
                 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
@@ -617,15 +607,34 @@
                 ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
 
           ... | case2 ¬x=sup =  no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
-                z18 :  {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain (zc z<x) ) a → b o< osuc x → (ab : odef A b) →
-                            HasPrev A (ZChain.chain (zc ?) ) ab f ∨ IsSup A (ZChain.chain (zc z<x) )   ab →
-                            * a < * b → odef (ZChain.chain (zc z<x) ) b
+                z18 :  {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc ) a → b o< osuc x → (ab : odef A b) →
+                            HasPrev A (ZChain.chain zc ) ab f ∨ IsSup A (ZChain.chain zc )   ab →
+                            * a < * b → odef (ZChain.chain zc ) b
                 z18 {a} {b} z<x za b<x ab p a<b with osuc-≡< b<x
-                ... | case2 lt = ZChain.is-max (zc z<x) za ? ab p a<b 
+                ... | case2 lt = ZChain.is-max zc za ? ab p a<b 
                 ... | case1 b=x with p
                 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = ? ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup ? )  } ) 
+     ... | no op = zc5 where
+          supf : (z : Ordinal ) → z o< x  → HOD
+          supf x lt = ZChain1.chainf ( zc0  (& A) ) x 
+          uzc : {z : Ordinal} → (u : UChain x supf z) → ZChain A f mf ay zc0 (UChain.u u)
+          uzc {z} u =  prev (UChain.u u) (UChain.u<x u) 
+          Uz : HOD
+          Uz = record { od = record { def = λ z → odef A z ∧ ( UChain x supf z ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!}  }
+          zc5 : ZChain A f mf ay zc0 x 
+          zc5 with o≤? x o∅
+          ... | yes x=0 = ?
+          ... | no 0<x 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
+
          
      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