# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1663180326 -32400
# Node ID f9fc8da87b5aeb58e8e1d90dd2d533f41a297b78
# Parent  1ca338c3f09c2b69c3cefd2126ca7e07db9dde93
..

diff -r 1ca338c3f09c -r f9fc8da87b5a src/zorn.agda
--- a/src/zorn.agda	Tue Sep 13 15:26:19 2022 +0900
+++ b/src/zorn.agda	Thu Sep 15 03:32:06 2022 +0900
@@ -447,7 +447,7 @@
            → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b 
       supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
-      csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) 
+      csupf : {b : Ordinal } → supf b o≤ z → odef (UnionCF A f mf ay supf z) (supf b) 
 
 
    chain∋init : odef chain y
@@ -490,7 +490,6 @@
         {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    supf = ZChain.supf zc
    field
-      order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
       is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) →  b o< z  → (ab : odef A b) 
           → HasPrev A (UnionCF A f mf ay supf z) b f ∨  IsSup A (UnionCF A f mf ay supf z) ab  
           → * a < * b  → odef ((UnionCF A f mf ay supf z)) b
@@ -633,18 +632,20 @@
                 s<b = ZChain.supf-inject zc ss<sb
                 s≤<z : s o≤ & A
                 s≤<z = ordtrans s<b b≤z
-                zc04 : odef (UnionCF A f mf ay supf (supf s))  (supf s)
-                zc04 = ? ZChain.csupf zc ? 
-                zc03 : odef (UnionCF A f mf ay supf (& A))  (supf s)
-                zc03 = ZChain.csupf zc ? 
+                zc04 : odef (UnionCF A f mf ay supf (& A))  (supf s)
+                zc04 = ZChain.csupf zc (o<→≤ (z09 (ZChain.asupf zc)))
                 zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
                 zc05 with zc04
                 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫ 
-                ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (zc09 u<x ) is-sup fc ⟫ where
+                ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u ? is-sup fc ⟫ where
+                    zc07 : FClosure A f (supf u) (supf s)   -- supf u ≤ supf s  → supf u o≤ supf s
+                    zc07 = fc
                     zc06 : supf u ≡ u
                     zc06 = ChainP.supu=u is-sup
-                    zc09 : u o< supf s  →  u o< b 
-                    zc09 u<s = ordtrans (ZChain.supf-inject zc (subst (λ k → k o< supf s) (sym zc06) u<s)) s<b
+                    zc09 : u o≤ supf s  →  u o< b 
+                    zc09 u≤s with osuc-≡< u≤s
+                    ... | case1 u=ss = ZChain.supf-inject zc (subst (λ k → k o< supf b) (sym (trans zc06 u=ss)) ss<sb )
+                    ... | case2 u<ss = ordtrans (ZChain.supf-inject zc (subst (λ k → k o< supf s) (sym zc06) u<ss)) s<b
         csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04  where
                 zc04 : odef (UnionCF A f mf ay supf b) (f x)
                 zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc  )
@@ -654,6 +655,7 @@
         order {b} {s} {z1} b<z ss<sb fc = zc04 where
           zc00 : ( * z1  ≡  SUP.sup (ZChain.sup zc (o<→≤ b<z) )) ∨ ( * z1  < SUP.sup ( ZChain.sup zc (o<→≤ b<z) ) )
           zc00 = SUP.x<sup (ZChain.sup zc (o<→≤  b<z) ) (csupf-fc (o<→≤ b<z) ss<sb fc )
+          -- supf (supf b) ≡ supf b
           zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
           zc04 with zc00
           ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (ZChain.supf-is-sup zc (o<→≤ b<z))  ) (cong (&) eq) )
@@ -858,7 +860,7 @@
 
           no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A pchain x f) → ZChain A f mf ay x
           no-extension P = record { supf = supf0 ;  asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 
-              ; order = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) }  where
+              ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) }  where
                  zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
                  zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
                  zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) u1-is-sup  fc  ⟫
@@ -1085,7 +1087,7 @@
           zc70 pr xsup = ?
 
           no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) → ZChain A f mf ay x
-          no-extension ¬sp=x  = record { supf = supf1  ; sup=u = sup=u  ; order = ? 
+          no-extension ¬sp=x  = record { supf = supf1  ; sup=u = sup=u  
                ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; asupf = ? } where
                  supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
                  supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z