# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1659936912 -32400
# Node ID 8373b130ba41af89738980023755d9acc9131eb7
# Parent  06eedb0d26a04202a50faab146d6776fb54477cf
...

diff -r 06eedb0d26a0 -r 8373b130ba41 src/zorn.agda
--- a/src/zorn.agda	Mon Aug 08 14:20:26 2022 +0900
+++ b/src/zorn.agda	Mon Aug 08 14:35:12 2022 +0900
@@ -288,7 +288,6 @@
       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) 
-      supf≤x :{x : Ordinal } → z o≤ x → supf z ≡  supf x
 
    fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
    fcy<sup  {u} {w} u≤z fc with SUP.x<sup (sup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
@@ -516,10 +515,9 @@
               m09 : {sup1 z1 : Ordinal} → sup1 o< b 
                            → 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
-              m10 :  {y₁ : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) y₁ → (y₁ ≡ b) ∨ (y₁ << b)
-              m10 = {!!}
               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 record { x<sup = m10} } 
+              m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = ZChain.sup=u zc ab 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 →
               b o< x → (ab : odef A b) →
@@ -540,10 +538,9 @@
               m05 : b ≡ ZChain.supf zc b
               m05 = sym (ZChain.sup=u zc ab m09
                       record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) lt )} )   -- ZChain on x
-              m10 :  {y₁ : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) y₁ → (y₁ ≡ b) ∨ (y₁ << b)
-              m10 = {!!}
               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 record { x<sup = m10 } }
+              m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = ZChain.sup=u zc ab m09 
+                      record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono1 (osucc b<x) lt )} } 
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function