# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1666952194 -32400
# Node ID 18759411644956fee6e3c069377ea4c8fc309f13
# Parent  93a49ffa9183fb5701f62d540ab59d175e648281
...

diff -r 93a49ffa9183 -r 187594116449 src/zorn.agda
--- a/src/zorn.agda	Fri Oct 28 18:37:05 2022 +0900
+++ b/src/zorn.agda	Fri Oct 28 19:16:34 2022 +0900
@@ -1474,33 +1474,22 @@
                 z24 = MinSUP.x<sup spd (init asc refl)
                 z28 : supf mc o< & A
                 z28 = z09 (ZChain.asupf zc)
+                --
+                --   f ( f .. ( supf mc ) <= d1
+                --   f d1 <= d1
+                --
                 z25 : supf mc << d1
                 z25 with z24
                 ... | case2 lt = lt
                 ... | case1 eq = ⊥-elim ( <-irr z29 (proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) ) )  where
                     --  supf mc ≡ d1
-                    z27 :  odef (ZChain.chain zc) (cf nmx d1)
-                    z27 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k ) eq (ZChain.csupf zc z28))
-                    z31 : {z w : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z 
-                        → (* w ≡ * z) ∨ (* w < * z)
-                        → (* w ≡ * d1) ∨ (* w < * d1)
-                    z31 {z} uz (case1 w=z) with MinSUP.x<sup spd uz
-                    ... | case1 eq = case1 (trans w=z (cong (*) eq) )
-                    ... | case2 lt = case2 (subst (λ k → k < * d1 ) (sym w=z) lt )
-                    z31 {z} {w} uz (case2 w<z) with MinSUP.x<sup spd uz
-                    ... | case1 eq = case2 (subst (λ k → * w < k ) (cong (*) eq) w<z )
-                    ... | case2 lt = case2 (  IsStrictPartialOrder.trans PO w<z lt)
+                    z32 : ((cf nmx (supf mc)) ≡ d1) ∨ ( (cf nmx (supf mc)) << d1 )
+                    z32 = MinSUP.x<sup spd (fsuc _ (init asc refl))
                     z29 :  (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
-                    z29 with z27
-                    ... | ⟪ aa , ch-init fc ⟫ = ? where
-                          z30 : FClosure A (cf nmx) (& s) (cf nmx d1)
-                          z30 = fc
-                    ... | ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ with trio< u (supf mc) -- u<x : supf u o< supf (& A)
-                    ... | tri< a ¬b ¬c = ?  -- u o< supf mc 
-                    ... | tri> ¬a ¬b c = ?  -- supf mc o< u
-                    ... | tri≈ ¬a b ¬c with MinSUP.x<sup spd ( subst₂ (λ j k → FClosure A (cf nmx) j k ) (trans (ChainP.supu=u is-sup) b) refl fc )
-                    ... | case1 eq = case1 (cong (*) eq)
-                    ... | case2 lt = case2 lt 
+                    z29  with z32
+                    ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1)  ) 
+                    ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt) 
+
           sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d
           sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) )
           ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd )