# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1668619986 -32400
# Node ID e11c244d7eacf7ca1caacc9c26383634df6d4e61
# Parent  4aaecae58da5bc42f69e3931f08e431feaa97fc8
SZ1 done

diff -r 4aaecae58da5 -r e11c244d7eac src/zorn.agda
--- a/src/zorn.agda	Thu Nov 17 02:22:39 2022 +0900
+++ b/src/zorn.agda	Thu Nov 17 02:33:06 2022 +0900
@@ -664,8 +664,8 @@
      --
 
      SZ1 : ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) (mf< : <-monotonic-f A f)
-        {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal)   → ZChain1 A f mf ay zc x
-     SZ1 f mf mf< {y} ay zc x = ? where
+        {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → x o≤ & A → ZChain1 A f mf ay zc x
+     SZ1 f mf mf< {y} ay zc x x≤A = zc1 x x≤A  where
         chain-mono1 :  {a b c : Ordinal} → a o≤ b
             → 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) (ZChain.supf-mono zc) a≤b
@@ -712,8 +712,8 @@
           ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z))  ) eq )
           ... | case2 lt = case2 (subst₂ (λ j k → j < * k ) refl (sym (ZChain.supf-is-minsup zc (o<→≤ b<z) )) lt )
 
-        zc1 :  (x : Ordinal ) → x o< & A →   ZChain1 A f mf ay zc x
-        zc1 x x<A with Oprev-p x  
+        zc1 :  (x : Ordinal ) → x o≤ & A →   ZChain1 A f mf ay zc x
+        zc1 x x≤A with Oprev-p x  
         ... | yes op = record { is-max = is-max ; order = order  } where
                px = Oprev.oprev op
                is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay supf x) a →
@@ -739,8 +739,6 @@
                   m06 : ChainP A f mf ay supf b
                   m06 = record {  fcy<sup = m08  ; order = m09 ; supu=u = m05 }
                ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
-                  x≤A : x o≤ & A
-                  x≤A = o<→≤ x<A
                   m17 : MinSUP A (UnionCF A f mf ay supf x) -- supf z o< supf ( supf x )
                   m17 = ZChain.minsup zc x≤A
                   m18 : supf x ≡ MinSUP.sup m17 
@@ -779,8 +777,6 @@
                   m06 : ChainP A f mf ay supf b
                   m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
                ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
-                  x≤A : x o≤ & A
-                  x≤A = o<→≤ x<A
                   m17 : MinSUP A (UnionCF A f mf ay supf x) -- supf z o< supf ( supf x )
                   m17 = ZChain.minsup zc x≤A
                   m18 : supf x ≡ MinSUP.sup m17 
@@ -1400,13 +1396,13 @@
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< (& A) → (ab : odef A b )
               →  HasPrev A chain f b  ∨  IsSUP A (UnionCF A f mf as0 (ZChain.supf zc) b) ab
               → * a < * b  → odef chain b
-           z10 = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) )
+           z10 = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl )
            z22 : sp o< & A
            z22 = z09 asp
            z12 : odef chain sp
            z12 with o≡? (& s) sp
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
-           ... | no ne = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) (z09 asp) asp (case2 z19 ) z13 where
+           ... | no ne = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl) {& s} {sp} ( ZChain.chain∋init zc ) (z09 asp) asp (case2 z19 ) z13 where
                z13 :  * (& s) < * sp
                z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc )
                ... | case1 eq = ⊥-elim ( ne eq )