# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660657756 -32400
# Node ID 26450ab6dd4edca2e2102163167efb0cdb541778
# Parent  648131d2b83c2e1c81c0b741e9061e3a60ddb028
...

diff -r 648131d2b83c -r 26450ab6dd4e src/zorn.agda
--- a/src/zorn.agda	Tue Aug 16 22:36:14 2022 +0900
+++ b/src/zorn.agda	Tue Aug 16 22:49:16 2022 +0900
@@ -284,7 +284,7 @@
       f-total : IsTotalOrderSet chain
 
       sup : {x : Ordinal } → x o< z  → SUP A (UnionCF A f mf ay supf x)
-      sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b 
+      sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z  → IsSup A (UnionCF A f mf ay supf b) ab → supf b ≡ b 
       supf-is-sup : {x : Ordinal } → (x≤z : x o< z) → supf x ≡ & (SUP.sup (sup x≤z) )
       csupf : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
 
@@ -512,7 +512,7 @@
               b<A = z09 ab
               m05 : b ≡ ZChain.supf zc b
               m05 = sym ( ZChain.sup=u zc ab (o<→≤ (z09 ab) )
-                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) uz )  }  )
+                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) uz )  }  )
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
               m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
               m09 : {sup1 z1 : Ordinal} → sup1 o< b 
@@ -520,7 +520,7 @@
               m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz
               m06 : ChainP A f mf ay (ZChain.supf zc) b 
               m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = ZChain.sup=u zc ab (o<→≤ b<A )
-                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) uz ) } }  
+                      record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) uz ) } }  
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
@@ -540,10 +540,10 @@
               m08 {sup1} {z1} s<b fc = ZChain.order zc m09 s<b fc
               m05 : b ≡ ZChain.supf zc b
               m05 = sym (ZChain.sup=u zc ab (o<→≤  m09)
-                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) lt )} )   -- ZChain on x
+                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) lt )} )   -- ZChain on x
               m06 : ChainP A f mf ay (ZChain.supf zc) b 
               m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = ZChain.sup=u zc ab (o<→≤  m09)
-                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) lt )} } 
+                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (o<→≤ b<x) lt )} } 
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -811,10 +811,10 @@
                      zc61 {w} lt = SUP.x<sup sup1 (UnionCFR⊆ (o<→≤ z<x) (o<→≤ z<x)  lt )
                  ... | tri> ¬a ¬b px<z = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
                  sup=u : {b : Ordinal} (ab : odef A b) →
-                    b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
+                    b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 b ≡ b
                  sup=u {b} ab b≤x is-sup with trio< b px
-                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = {!!} }
-                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab {!!} record { x<sup = {!!} }
+                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = ? }
+                 ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = {!!} }
                  ... | tri> ¬a ¬b px<b = {!!} where
                      zc30 : x ≡ b
                      zc30 with osuc-≡< b≤x
@@ -972,7 +972,7 @@
                      zc8 = ZChain.supf-is-sup (pzc z a) {!!}
                  ... | tri≈ ¬a b ¬c = {!!}
                  ... | tri> ¬a ¬b c = {!!}
-                 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc b)) ab → supf1 b ≡ b
+                 sup=u : {b : Ordinal} (ab : odef A b) → b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 b ≡ b
                  sup=u {b} ab b<x is-sup with trio< b x
                  ... | tri< a ¬b ¬c = ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab {!!} record { x<sup = {!!} }
                  ... | tri≈ ¬a b ¬c = {!!} -- ZChain.sup=u (pzc (osuc ?)  ?)  ab {!!} record { x<sup = {!!} }