# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660634997 -32400
# Node ID 95db436cce670975da11eb752a9703f80aa25c88
# Parent  1627cc8f193eaedc44b248834cd51b884d61522d
...

diff -r 1627cc8f193e -r 95db436cce67 src/zorn.agda
--- a/src/zorn.agda	Tue Aug 16 16:01:42 2022 +0900
+++ b/src/zorn.agda	Tue Aug 16 16:29:57 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 (osuc 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) 
 
@@ -511,7 +511,7 @@
               b<A : b o< & A
               b<A = z09 ab
               m05 : b ≡ ZChain.supf zc b
-              m05 = sym ( ZChain.sup=u zc ab (z09 ab) 
+              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 )  }  )
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
               m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
@@ -519,7 +519,7 @@
                            → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
               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 b<A 
+              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 ) } }  
         ... | 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 →
@@ -539,10 +539,10 @@
                        → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
               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  m09
+              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
               m06 : ChainP A f mf ay (ZChain.supf zc) b 
-              m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = ZChain.sup=u zc ab m09
+              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 )} } 
 
      ---
@@ -806,16 +806,16 @@
                  sup : {z : Ordinal} → z o< x → SUP A (UnionCF A f mf ay supf1 z)
                  sup {z} z<x with trio< z px
                  ... | tri< a ¬b ¬c = SUP⊆ (UnionCFR⊆ o≤-refl ? (o<→≤ a)) ( ZChain.sup zc  a )
-                 ... | tri> ¬a ¬b px<z = ?
                  ... | tri≈ ¬a b ¬c = record { sup = SUP.sup sup1 ; as = SUP.as sup1 ; x<sup = zc61 } where
                      zc61 : {w : HOD} → UnionCF A f mf ay supf1 z ∋ w → (w ≡ SUP.sup sup1) ∨ (w < SUP.sup sup1)
                      zc61 {w} 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
-                 sup=u {b} ab b<x is-sup with trio< b px
-                 ... | tri< a ¬b ¬c = ZChain.sup=u zc ab a record { x<sup = {!!} }
+                    b o≤ x → IsSup A (UnionCF A f mf ay supf1 (osuc 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 = ?
-                 ... | tri> ¬a ¬b px<b = {!!} 
+                 ... | tri> ¬a ¬b px<b = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) ? ⟫ )
                  csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
                  csupf {b} b≤x with trio< b px | inspect supf1 b
                  ... | tri< a ¬b ¬c | _ = UnionCF⊆ o≤-refl (o<→≤ a) b≤x ( ZChain.csupf zc (o<→≤ a) )
@@ -968,7 +968,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 (osuc 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 = {!!}