# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655188321 -32400
# Node ID 021fcb324990d94737c4ea243aa18675e0d31f08
# Parent  d68114d45d2f1254c8de626ffd2824d144076615
...

diff -r d68114d45d2f -r 021fcb324990 src/zorn.agda
--- a/src/zorn.agda	Tue Jun 14 15:14:28 2022 +0900
+++ b/src/zorn.agda	Tue Jun 14 15:32:01 2022 +0900
@@ -412,11 +412,15 @@
           --
           -- we have previous ordinal to use induction
           --
+          open ZChain
+          
           px = Oprev.oprev op
           zc0 : ZChain A y f (Oprev.oprev op)
           zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay
           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 
+          px<x : px o< x
+          px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
 
           ys : HOD
           ys = record { od = record { def = λ x →  FClosure A f y x  } ; odmax = & A ; <odmax = {!!} }
@@ -427,20 +431,23 @@
                i-total : IsTotalOrderSet ys
                i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb)
 
-          fcs< :   {w : Ordinal}    (c z : Ordinal) (x : Ordinal) → z o< w → Fc∨sup  A ay f c z x → Fc∨sup  A ay f c w x 
-          fcs< c z x z<w (Finit x₁) = Finit x₁
-          fcs< {w} c z x z<w (Fsup {p} x₁ FC x₂ x₃) = Fsup x₁ (fcs< c z p z<w FC) record { sup = FSup.sup x₂  ; chain∋p =  FSup.chain∋p x₂  } 
+          fcs< :  (A : HOD) {w y : Ordinal} (ay : odef A y)   (c z : Ordinal) (x : Ordinal)
+                → z o< w → Fc∨sup  A ay f c z x → Fc∨sup  A ay f c w x 
+          fcs< A ay c z x z<w (Finit x₁) = Finit x₁
+          fcs< A {w} ay c z x z<w (Fsup {p} x₁ FC x₂ x₃) = Fsup x₁ (fcs< A ay c z p z<w FC) record { sup = FSup.sup x₂  ; chain∋p =  FSup.chain∋p x₂  } 
                  (x<ow x₃ z<w ) where
               x<ow : x o< osuc z → z o< w → x o< osuc w
               x<ow x<z z<w = ordtrans x<z (osucc z<w)
-          fcs< {w} c z x z<w (Fc {p} x₁ FC x₂) = Fc x₁ (fcs< c z p z<w FC) record { fc∨sup = FChain.fc∨sup x₂; chain∋p = FChain.chain∋p x₂} 
+          fcs< A {w} ay c z x z<w (Fc {p} x₁ FC x₂) = Fc x₁ (fcs< A ay c z p z<w FC) record { fc∨sup = FChain.fc∨sup x₂; chain∋p = FChain.chain∋p x₂} 
 
           zc4 : ZChain A y f x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax =  -- ¬ A ∋ p, just skip
                  record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 
                      ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0 ; chain∋sup = {!!}
-                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 ; fc∨sup = {!!}  }  where -- no extention
+                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 ; fc∨sup = {!!} }  where -- no extention
+                zc12 : {c : Ordinal} → odef (ZChain.chain zc0) c → Fc∨sup A (ZChain.chain⊆A zc0 (ZChain.chain∋x zc0)) f (& (ZChain.chain zc0)) x c
+                zc12 {c} cc = fcs< A (ZChain.chain⊆A zc0 (ZChain.chain∋x zc0)) (& (ZChain.chain zc0)) px c px<x (ZChain.fc∨sup zc0 cc)
                 zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
                     HasPrev A (ZChain.chain zc0) ab f ∨  IsSup A (ZChain.chain zc0) ab →
                             * a < * b → odef (ZChain.chain zc0) b
@@ -449,13 +456,13 @@
                 ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt)  ab P a<b
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) ax f )   -- we have to check adding x preserve is-max ZChain A y f mf supO x
           ... | case1 pr = zc9 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
-                chain = ZChain.chain zc0
+                chain0 = ZChain.chain zc0
                 zc17 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
                             HasPrev A (ZChain.chain zc0) ab f ∨ IsSup A (ZChain.chain zc0) ab →
                             * a < * b → odef (ZChain.chain zc0) b
                 zc17 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
                 ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab P a<b
-                ... | case1 b=x = subst (λ k → odef chain k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
+                ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
                 zc9 :  ZChain A y f x
                 zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0 -- no extention
                      ; chain∋sup = {!!}
@@ -474,12 +481,12 @@
                 sp = SUP.sup sup0 
                 x=sup : x ≡ & sp 
                 x=sup = sym &iso 
-                chain = ZChain.chain zc0
-                sc<A : {y : Ordinal} → odef chain 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 zc0 (subst (λ k → odef chain k) (sym &iso) zx )))
+                chain0 = ZChain.chain zc0
+                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 zc0 (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 chain x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
+                schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
                 A∋schain : {x : HOD } → schain ∋ x → A ∋ x
                 A∋schain (case1 zx ) = ZChain.chain⊆A zc0 zx 
                 A∋schain {y} (case2 fx ) = A∋fc (& sp) f mf fx 
@@ -489,7 +496,7 @@
                 s-fc∨sup : {c : Ordinal} → odef schain c → Fc∨sup A (s⊆A (case1 (ZChain.chain∋x zc0))) f (& schain) x c 
                 s-fc∨sup {c} (case1 cx) = {!!}
                 s-fc∨sup {c} (case2 fc) = {!!}
-                cmp  : {a b : HOD} (za : odef chain (& a)) (fb : FClosure A f (& sp) (& b)) → Tri (a < b) (a ≡ b) (b < a )
+                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  
                 ... | case1 sp=a | case1 sp=b = tri≈ (λ lt → <-irr (case1 (sym eq)) lt ) eq (λ lt → <-irr (case1 eq) lt ) where
                         eq : a ≡ b
@@ -516,15 +523,15 @@
                 scnext {x} (case2 sx) = case2 ( fsuc x sx )
                 scinit :  {x : Ordinal} → odef schain x → * y ≤ * x
                 scinit {x} (case1 zx) = ZChain.initial zc0 zx
-                scinit {x} (case2 sx) with  (s≤fc (& sp) f mf sx ) |  SUP.x<sup sup0 (subst (λ k → odef chain k ) (sym &iso) ( ZChain.chain∋x zc0 ) )
+                scinit {x} (case2 sx) with  (s≤fc (& sp) f mf sx ) |  SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) ( ZChain.chain∋x zc0 ) )
                 ... | 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 chain a → odef A a
+                A∋za : {a : Ordinal } → odef chain0 a → odef A a
                 A∋za za = ZChain.chain⊆A zc0 za 
-                za<sup :  {a : Ordinal } → odef chain a → ( * a ≡ sp ) ∨  ( * a < sp )
-                za<sup za =  SUP.x<sup sup0 (subst (λ k → odef chain k ) (sym &iso) 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 )
                 simm : {a b : Ordinal}  → odef schain a → odef schain b → ¬ (* a < * b) ∧ (* b < * (f a))
                 simm {a} {b} (case1 za) (case1 zb) = ZChain.f-immediate zc0 za zb
                 simm {a} {b} (case1 za) (case2 sb) p with  proj1 (mf a (A∋za za) )
@@ -556,14 +563,14 @@
                      z22 : IsSup A (ZChain.chain zc0)   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 chain k ) (sym (HasPrev.x=fy p)) (ZChain.f-next zc0 zy ))               -- in previous closure of f
+                ... | case1 zy = case1 (subst (λ k → odef chain0 k ) (sym (HasPrev.x=fy p)) (ZChain.f-next zc0 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 zc0
                      z24 : IsSup A schain ab → IsSup A (ZChain.chain zc0) ab 
                      z24 p = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) }
-                     z23 : odef chain b
+                     z23 : odef chain0 b
                      z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋x zc0 )
-                     ... | case1 y=b  = subst (λ k → odef chain k )  y=b ( ZChain.chain∋x zc0 )
+                     ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋x zc0 )
                      ... | case2 y<b  = ZChain.is-max zc0 (ZChain.chain∋x zc0 ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<b
           ... | case2 ¬x=sup =  -- x is not f y' nor sup of former ZChain from y
                    record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 ; chain∋sup = {!!}