# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658344692 -32400
# Node ID de9d9c70a0d713e26cb0233e08da8d1f22f2ce64
# Parent  adbe43c07ce7139a1f7dba4a2b85911de9f07952
...

diff -r adbe43c07ce7 -r de9d9c70a0d7 src/zorn.agda
--- a/src/zorn.agda	Thu Jul 21 03:56:54 2022 +0900
+++ b/src/zorn.agda	Thu Jul 21 04:18:12 2022 +0900
@@ -298,8 +298,8 @@
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
-      sup=u : {b : Ordinal} → {ab : odef A b}  → b o< z → IsSup A chain ab → supf b ≡ b 
-      order : {sup1 b z1 : Ordinal} → b o< z → sup1 o< b → FClosure A f (supf sup1) z1 → z1 << supf b
+      sup=u : {b : Ordinal} → {ab : odef A b} → b o< z → IsSup A chain ab → supf b ≡ b 
+      order : {b sup1 z1 : Ordinal} → b o< z → sup1 o< b → FClosure A f (supf sup1) z1 → z1 << supf b
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
         {init : Ordinal} (ay : odef A init)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
@@ -310,6 +310,8 @@
           → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) z) ab f ∨  IsSup A (UnionCF A f mf ay (ZChain.supf zc) z) ab  
           → * a < * b  → odef ((UnionCF A f mf ay (ZChain.supf zc) z)) b
       fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f init w → w << (ZChain.supf zc) u
+      sup=u : {b : Ordinal} → {ab : odef A b} → b o< z  → IsSup A (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) ab → (ZChain.supf zc) b ≡ b 
+      order : {b sup1 z1 : Ordinal} → b o< z → sup1 o< b → FClosure A f ((ZChain.supf zc) sup1) z1 → z1 << (ZChain.supf zc) b
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
@@ -495,10 +497,10 @@
                  m07 : {z : Ordinal} → FClosure A f y z → z << ZChain.supf zc b
                  m07 {z} fc = ZChain1.fcy<sup (prev (osuc b) ob<x) <-osuc fc
                  m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
-                 m08 = ?
+                 m08 {sup1} {z1} s<b fc = ZChain1.order (prev (osuc b) ob<x) <-osuc s<b fc
                  m05 : b ≡ ZChain.supf zc b
-                 m05 = sym (ZChain.sup=u zc {_} {ab} ?
-                        record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ ob<x) o≤-refl ? )} )   -- ZChain on x
+                 m05 = sym (ZChain1.sup=u (prev (osuc b) ob<x) {_} {ab} <-osuc 
+                        record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ ob<x) o≤-refl lt )} )   -- ZChain on x
                  m06 : ChainP A f mf ay (ZChain.supf zc) b b
                  m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b