# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658361808 -32400
# Node ID d92ad9e365b60b65303f528e3a2a300390684441
# Parent  71556e611842a148f9ed1c4d0ad0d3e141559c47
...

diff -r 71556e611842 -r d92ad9e365b6 src/OrdUtil.agda
--- a/src/OrdUtil.agda	Thu Jul 21 07:58:34 2022 +0900
+++ b/src/OrdUtil.agda	Thu Jul 21 09:03:28 2022 +0900
@@ -40,6 +40,7 @@
 osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y
 osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x
 
+                                                      
 open _∧_
 
 ¬p<x<op : { p b : Ordinal } → ¬ ( (p o< b ) ∧ (b o< osuc p ) )
@@ -53,6 +54,12 @@
 ... | tri≈ ¬a 0=b ¬c = ⊥-elim ( ¬x<0 ( subst (λ k → p o< k) (sym 0=b) p<b ) )
 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
 
+ob<x : {b x : Ordinal} (lim : ¬ (Oprev Ordinal osuc x ) ) (b<x : b o< x ) → osuc b o< x                                        
+ob<x {b} {x} lim b<x with trio< (osuc b) x                                                                                     
+... | tri< a ¬b ¬c = a                                                                                                         
+... | tri≈ ¬a ob=x ¬c = ⊥-elim ( lim record { op = b ; oprev=x = ob=x }  )                                                     
+... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ b<x , c ⟫ )                           
+
 osucc :  {ox oy : Ordinal } → oy o< ox  → osuc oy o< osuc ox  
 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
diff -r 71556e611842 -r d92ad9e365b6 src/zorn.agda
--- a/src/zorn.agda	Thu Jul 21 07:58:34 2022 +0900
+++ b/src/zorn.agda	Thu Jul 21 09:03:28 2022 +0900
@@ -496,9 +496,16 @@
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
                          (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤  (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ))  o≤-refl lt)  } ) a<b
                  ... | tri≈ ¬a b=px ¬c = ? -- b = px case
-        ... | no lim = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = ? }  where
+        ... | no lim = record { is-max = is-max ; chain-mono2 = chain-mono2 x ; fcy<sup = fcy<sup ; sup=u = sup=u ; order = order  }  where
            fcy<sup : {u w : Ordinal} → u o< x → FClosure A f y w → w << ZChain.supf zc u
-           fcy<sup {u} {w} u<x fc = ?
+           fcy<sup {u} {w} u<x fc = ZChain1.fcy<sup (prev (osuc u) (ob<x lim u<x)) <-osuc fc
+           sup=u :  {b : Ordinal} {ab : odef A b} → b o< x →
+                IsSup A (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) ab →
+                ZChain.supf zc b ≡ b
+           sup=u {b} {ab} b<x is-sup = ZChain1.sup=u (prev (osuc b) (ob<x lim b<x)) <-osuc is-sup
+           order : {b sup1 z1 : Ordinal} → b o< x → sup1 o< b →
+                FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
+           order {b} b<x s<b fc = ZChain1.order (prev (osuc b) (ob<x lim b<x)) <-osuc s<b fc
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
               HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
@@ -507,23 +514,19 @@
            is-max {a} {b} ua b<x ab (case2 is-sup) a<b with IsSup.x<sup is-sup (init-uchain A f mf ay )
            ... | case1 b=y = ⊥-elim ( <-irr ( ZChain.initial zc (chain<ZA (chain-mono2 (osuc x) (o<→≤ <-osuc ) o≤-refl ua )) )
                        (subst (λ k → * a < * k ) (sym b=y) a<b ) )
-           ... | case2 y<b = chain-mono2 x (o<→≤ ob<x) o≤-refl m04 where
+           ... | case2 y<b = chain-mono2 x (o<→≤ (ob<x lim b<x) ) o≤-refl m04 where
                  y<s : y << ZChain.supf zc b
                  y<s = y<s 
-                 ob<x : osuc b o< x
-                 ob<x with trio< (osuc b) x
-                 ... | tri< a ¬b ¬c = a
-                 ... | tri≈ ¬a ob=x ¬c = ⊥-elim ( lim record { op = b ; oprev=x = ob=x }  )
-                 ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ b<x , c ⟫ )
                  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
+                 m07 {z} fc = ZChain1.fcy<sup (prev (osuc b) (ob<x lim b<x)) <-osuc fc
                  m08 : {sup1 z1 : Ordinal} → sup1 o< b → FClosure A f (ZChain.supf zc sup1) z1 → z1 << ZChain.supf zc b
-                 m08 {sup1} {z1} s<b fc = ZChain1.order (prev (osuc b) ob<x) <-osuc s<b fc
+                 m08 {sup1} {z1} s<b fc = ZChain1.order (prev (osuc b) (ob<x lim b<x) ) <-osuc s<b fc
                  m05 : b ≡ ZChain.supf zc b
-                 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
+                 m05 = sym (ZChain1.sup=u (prev (osuc b) (ob<x lim b<x)) {_} {ab} <-osuc 
+                        record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ (ob<x lim b<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 ; y<s = y<s }
+                 m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 ; y<s = y<s 
+                       ; supfu=u = sym m05 }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
                  m04 = ⟪ ab , record { u = b ; u<x = case1 <-osuc ; uchain = ch-is-sup m06 (subst (λ k → FClosure A f k b) m05 (init ab)) } ⟫