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

diff -r 0ef3ef93c5c3 -r d68114d45d2f src/zorn.agda
--- a/src/zorn.agda	Tue Jun 14 14:36:45 2022 +0900
+++ b/src/zorn.agda	Tue Jun 14 15:14:28 2022 +0900
@@ -233,20 +233,20 @@
    field
       x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 
-record FChain ( A : HOD ) ( f : Ordinal → Ordinal ) (p c : Ordinal)   ( x : Ordinal ) : Set n where
+record FChain ( A : HOD ) ( f : Ordinal → Ordinal ) (p c z : Ordinal)   ( x : Ordinal ) : Set n where
    field
       fc∨sup :  FClosure A f p x
       chain∋p : odef (* c) p 
 
-record FSup ( A : HOD ) ( f : Ordinal → Ordinal ) (p c : Ordinal)   ( x : Ordinal ) : Set n where
+record FSup ( A : HOD ) ( f : Ordinal → Ordinal ) (p c z : Ordinal)   ( x : Ordinal ) : Set n where
    field
       sup :  (z : Ordinal) → FClosure A f p z → * z < * x 
       chain∋p : odef (* c) p 
 
-data Fc∨sup (A : HOD) {y : Ordinal} (ay : odef A y)  ( f : Ordinal → Ordinal ) (c : Ordinal) : (x : Ordinal) → Set n where
-      Finit :  {z : Ordinal} → z ≡ y  → Fc∨sup A ay f c z
-      Fsup  :  {p x : Ordinal} → p o< x → Fc∨sup A ay f c p → FSup   A f p c x →  Fc∨sup A ay f c x
-      Fc    :  {p x : Ordinal} → p o< x → Fc∨sup A ay f c p → FChain A f p c x →  Fc∨sup A ay f c x
+data Fc∨sup (A : HOD) {y : Ordinal} (ay : odef A y)  ( f : Ordinal → Ordinal ) (c z : Ordinal) : (x : Ordinal) → Set n where
+      Finit :  {i : Ordinal} → i ≡ y  → Fc∨sup A ay f c z i
+      Fsup  :  {p x : Ordinal} → p o< x → Fc∨sup A ay f c z p → FSup   A f p c z x → x o< osuc z  →  Fc∨sup A ay f c z x
+      Fc    :  {p x : Ordinal} → p o< x → Fc∨sup A ay f c z p → FChain A f p c z x →  Fc∨sup A ay f c z x
 
 record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where
    field
@@ -260,8 +260,8 @@
       is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ab : odef A b) 
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
-      chain∋sup : (s : HOD) → s ⊆' chain → {b : Ordinal} (ab : odef A b) → b o< z  → IsSup A s ab → odef chain b
-      fc∨sup :  {c : Ordinal } → ( ca : odef chain c )  → Fc∨sup A (chain⊆A chain∋x) f (& chain) c 
+      chain∋sup : (s : HOD) → s ⊆' chain → {b : Ordinal} (ab : odef A b) → b o< osuc z  → IsSup A s ab → odef chain b
+      fc∨sup :  {c : Ordinal } → ( ca : odef chain c )  → Fc∨sup A (chain⊆A chain∋x) f (& chain) z c
 
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
@@ -426,12 +426,21 @@
                      ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = init ay ; is-max = {!!} ; fc∨sup = {!!} } where
                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₂  } 
+                 (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₂} 
+
           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 = ZChain.fc∨sup zc0 }  where -- no extention
+                     ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 ; fc∨sup = {!!}  }  where -- no extention
                 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
@@ -450,7 +459,7 @@
                 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 = {!!}
-                     ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 ; fc∨sup = ZChain.fc∨sup zc0 } 
+                     ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 ; fc∨sup = {!!} } 
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
           ... | case1 is-sup = -- x is a sup of zc0 
                 record { chain = schain ; chain⊆A = s⊆A  ; f-total = scmp ; f-next = scnext ; chain∋sup = {!!}
@@ -477,7 +486,7 @@
                 s⊆A : schain ⊆' A
                 s⊆A {x} (case1 zx) = ZChain.chain⊆A zc0 zx
                 s⊆A {x} (case2 fx) = A∋fc (& sp) f mf fx 
-                s-fc∨sup : {c : Ordinal} → odef schain c → Fc∨sup A (s⊆A (case1 (ZChain.chain∋x zc0))) f (& schain) c
+                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 )
@@ -558,7 +567,7 @@
                      ... | 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 = {!!}
-                     ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = z18 ; fc∨sup = ZChain.fc∨sup zc0 }  where
+                     ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = z18 ; fc∨sup = {!!} }  where
                       -- no extention
                 z18 :  {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 →
@@ -602,12 +611,12 @@
                  → ((j : Ordinal) → j o< i →  odef (chain za) j → odef (chain zb) j)
                  → odef (chain za) i → odef (chain zb) i
             uind i previ zai = um01 where
-                FC : Fc∨sup A (chain⊆A za (chain∋x za)) f (& (chain za)) i 
-                FC = fc∨sup za zai 
+                FC : Fc∨sup A (chain⊆A za (chain∋x za)) f (& (chain za)) a i
+                FC = fc∨sup za zai
                 um01 : odef (chain zb) i
                 um01 with FC
                 ... | Finit i=y = subst (λ k → odef (chain zb) k ) (sym i=y) ( chain∋x zb )
-                ... | Fsup {p} {i} p<i pFC sup = cb∋i where
+                ... | Fsup {p} {i} p<i pFC sup i≤b  = cb∋i where
                      i-asup : (z : Ordinal) → FClosure A f p z → * z < * i
                      i-asup = FSup.sup sup
                      um06 : odef (chain za) p