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

diff -r 1f3a93bb4229 -r f52c610cca06 src/zorn.agda
--- a/src/zorn.agda	Thu Oct 06 17:39:31 2022 +0900
+++ b/src/zorn.agda	Thu Oct 06 18:44:18 2022 +0900
@@ -458,7 +458,7 @@
         {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
-      is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) →  supf b o< z  → (ab : odef A 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
 
@@ -598,7 +598,7 @@
             → odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
         chain-mono1  {a} {b} {c} a≤b = chain-mono f mf ay (ZChain.supf zc) a≤b
         is-max-hp : (x : Ordinal) {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
-            ZChain.supf zc b o< x → (ab : odef A b) →
+            b o< x → (ab : odef A b) →
             HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) b f → 
             * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
         is-max-hp x {a} {b} ua b<x ab has-prev a<b with HasPrev.ay has-prev
@@ -648,7 +648,7 @@
            zc-b<x : {b : Ordinal } → b o< x → b o< osuc px
            zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
-              supf b o< x → (ab : odef A b) →
+              b o< x → (ab : odef A b) →
               HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab →
               * a < * b → odef (UnionCF A f mf ay supf x) b
            is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
@@ -657,8 +657,6 @@
              = ⟪ ab , ch-is-sup b sb<sx m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
               b<A : b o< & A
               b<A = z09 ab
-              sb<sx : supf b o< supf x
-              sb<sx = ?
               m04 : ¬ HasPrev A (UnionCF A f mf ay supf b) b f
               m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = 
                     chain-mono1 ?  (HasPrev.ay  nhp) 
@@ -673,9 +671,21 @@
               m09 {s} {z} s<b fcz = order b<A s<b fcz    
               m06 : ChainP A f mf ay supf b 
               m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
+              sb<sx : supf b o< supf x
+              sb<sx with osuc-≡< ( ZChain.supf-mono zc (o<→≤ b<x ) )
+              ... | case2 lt = lt
+              ... | case1 eq = ⊥-elim ( <-irr (case1 (sym m11)) m12 ) where 
+                    ---    supf b ≡ supf x     * ( supf x ) ≤ * a < * b , * (supf x) ≡ * (supf b) ≡ * b
+                    m10 : {a : Ordinal} → odef  (UnionCF A f mf ay supf x) a  → * ( supf x ) ≤ * a
+                    m10 {a} ⟪ ua , ch-init fc ⟫ = ?
+                    m10 {a} ⟪ ua , ch-is-sup u u<x is-sup fc ⟫ = ?
+                    m12 : * ( supf x ) < * b
+                    m12 = ?
+                    m11 : * ( supf x ) ≡ * b
+                    m11 = ?
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
-              supf b o< x → (ab : odef A b) →
+              b o< x → (ab : odef A b) →
               HasPrev A (UnionCF A f mf ay supf x) b f ∨ IsSup A (UnionCF A f mf ay supf x) ab →
               * a < * b → odef (UnionCF A f mf ay supf x) b
            is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P
@@ -710,12 +720,14 @@
            supf = ZChain.supf zc
            sp1 : SUP A chain
            sp1 = sp0 f mf as0 zc 
-           z10 :  {a b : Ordinal } → (ca : odef chain a ) → supf b o< & A → (ab : odef A b ) 
+           z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< & A → (ab : odef A b ) 
               →  HasPrev A chain b f ∨  IsSup A chain {b} ab 
               → * a < * b  → odef chain b
            z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
-           z21 : supf (& (SUP.sup sp1)) o< & A
-           z21 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (ZChain.asupf zc ) ))
+           z21 : & (SUP.sup sp1) o< & A
+           z21 = c<→o< (SUP.as sp1 )
+           -- z21 : supf (& (SUP.sup sp1)) o< & A
+           -- z21 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (ZChain.asupf zc ) ))
            z12 : odef chain (& (SUP.sup sp1))
            z12 with o≡? (& s) (& (SUP.sup sp1))
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )