# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1662596211 -32400
# Node ID f72b35ab0ef978d082308c3660442bffed1d14f0
# Parent  bba4ce6d276687c83710477774fdaa2f8a955225
...

diff -r bba4ce6d2766 -r f72b35ab0ef9 src/zorn.agda
--- a/src/zorn.agda	Wed Sep 07 23:17:29 2022 +0900
+++ b/src/zorn.agda	Thu Sep 08 09:16:51 2022 +0900
@@ -576,20 +576,19 @@
               * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b
            is-max {a} {b} ua b<x ab (case1 has-prev) a<b = is-max-hp x {a} {b} ua b<x ab has-prev a<b 
            is-max {a} {b} ua b<x ab (case2 is-sup) a<b 
-             = ⟪ ab , ch-is-sup b (o<→≤ b<x) m06 (subst (λ k → FClosure A f k b) m05 (init ab refl)) ⟫   where
+             = ⟪ ab , ch-is-sup b (o<→≤ b<x) m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl)) ⟫   where
               b<A : b o< & A
               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 (o<→≤ b<x) uz )  }  )
+              m05 : ZChain.supf zc b ≡ b
+              m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )
+                      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 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
                            → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
               m09 {s} {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 (o<→≤ b<x) uz ) } }  
+              m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
         ... | 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) →
@@ -599,7 +598,7 @@
            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 = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl ))  ⟫
            ... | case2 y<b = chain-mono1 (osucc b<x) 
-             ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc )  m06 (subst (λ k → FClosure A f k b) m05 (init ab refl))  ⟫ where
+             ⟪ ab , ch-is-sup b (ordtrans o≤-refl <-osuc )  m06 (subst (λ k → FClosure A f k b) (sym m05) (init ab refl))  ⟫ where
               m09 : b o< & A
               m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
               m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
@@ -607,12 +606,11 @@
               m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
                        → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
               m08 {s} {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 (o<→≤ b<x) lt )} )   -- ZChain on x
+              m05 : ZChain.supf zc b ≡ b
+              m05 = ZChain.sup=u zc ab (o<→≤  m09)
+                      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 (o<→≤ b<x) lt )} } 
+              m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -838,9 +836,6 @@
                           zc13 : odef pchain z
                           zc13 = subst (λ k → odef pchain k) (trans (sym (HasPrev.x=fy hp)) zc14) ( ZChain.f-next zc (HasPrev.ay hp) )
                         zc20 {.(f w)} (fsuc w fc) = ZChain.f-next zc (zc20 fc)
-
-                     -- zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup (init asu su=z ) ⟫ | case1 eq = zc13 where
-                     --zc11 (case2 hp) {.(f w)} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup (fsuc w fc) ⟫ | case1 eq = ?
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
                      field
                          tsup : SUP A (UnionCF A f mf ay supf0 z)
@@ -870,13 +865,14 @@
                      zc30 with osuc-≡< b≤x
                      ... | case1 eq = sym (eq)
                      ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
+                     zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
+                     zcsup with zc30
+                     ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → 
+                        IsSup.x<sup is-sup (subst (λ k → odef k w) pchain0=1 lt)  } }
                      zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A pchain x f) → supf0 b ≡ b
-                     zc31 (case1 ¬sp=x) = ⊥-elim (¬sp=x zcsup ) where
-                         zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
-                         zcsup with zc30
-                         ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → 
-                            IsSup.x<sup is-sup (subst (λ k → odef k w) pchain0=1 lt)  } }
+                     zc31 (case1 ¬sp=x) = ⊥-elim (¬sp=x zcsup ) 
                      zc31 (case2 hasPrev ) = ?
+                     --  f a ≡ x ,   a ≡ x ∨ ( a < x ) -- supf0 (f a) ≡ f a/j
 
                  zc04 : {b : Ordinal} → b o≤ x → (b o≤ px ) ∨ (b ≡ x )
                  zc04 {b} b≤x with trio< b px