# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1666595178 -32400
# Node ID ed711d7be1913c97cbd441b2efba57b926432217
# Parent  ebcad8e5ae557ec56ad3171563243d44a506cd90
mem exhaust fix on fixpoint

diff -r ebcad8e5ae55 -r ed711d7be191 src/zorn.agda
--- a/src/zorn.agda	Mon Oct 24 09:36:07 2022 +0900
+++ b/src/zorn.agda	Mon Oct 24 16:06:18 2022 +0900
@@ -1349,43 +1349,46 @@
      sp0 f mf ay zc = M→S (ZChain.supf zc) (msp0 f mf ay zc )
 
      fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
-            → ZChain.supf zc (& (SUP.sup (sp0 f mf as0 zc))) o< ZChain.supf zc (& A)
-            → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc  ))
-     fixpoint f mf zc ss<sa = z14 where
+            → (sp1 : SUP A (ZChain.chain zc))   -- & (SUP.sup (sp0 f mf as0 zc  ))
+            → (ssp<as :  ZChain.supf zc (& (SUP.sup sp1)) o< ZChain.supf zc (& A))
+            → f (& (SUP.sup sp1))  ≡ & (SUP.sup sp1) 
+     fixpoint f mf zc sp1 ssp<as = z14 where
            chain = ZChain.chain zc
            supf = ZChain.supf zc
-           sp1 : SUP A chain
-           sp1 = sp0 f mf as0 zc 
+           sp : Ordinal
+           sp = & (SUP.sup sp1)
+           asp : odef A sp
+           asp = SUP.as sp1
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& 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) )
-           z22 : & (SUP.sup sp1) o< & A
-           z22 = c<→o< ( SUP.as sp1 )
-           z21 : supf (& (SUP.sup sp1)) o< supf (& A)
-           z21 = ss<sa
-           -- 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))
+           z22 : sp o< & A
+           z22 = z09 asp
+           x<sup : {x : HOD} → chain ∋ x → (x ≡ SUP.sup sp1 ) ∨ (x < SUP.sup sp1 )
+           x<sup bz with SUP.x<sup sp1 bz 
+           ... | case1 eq = case1 ?
+           ... | case2 lt = case2 ?
+           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 as0 zc (& A)) {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1)
+           ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {sp} ( ZChain.chain∋init zc ) ssp<as asp
                 (case2 z19 ) z13 where
-               z13 :  * (& s) < * (& (SUP.sup sp1))
-               z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc )
+               z13 :  * (& s) < * sp
+               z13 with x<sup ( ZChain.chain∋init zc )
                ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
                ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
                z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1)
                z19 = record {   x<sup = z20 }  where
                    z20 :  {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1))
-                   z20 {y} zy with SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) zy)
+                   z20 {y} zy with x<sup (subst (λ k → odef chain k ) (sym &iso) zy)
                    ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
                    ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
            ztotal : IsTotalOrderSet (ZChain.chain zc)
            ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf as0 supf ( (proj2 ca)) ( (proj2 cb)) 
-           z14 :  f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc ))
+           z14 :  f sp ≡ sp
            z14 with ztotal (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
                z16 : ⊥
@@ -1394,12 +1397,12 @@
                ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
            ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
            ... | tri> ¬a ¬b c = ⊥-elim z17 where
-               z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) <  SUP.sup sp1)
-               z15  = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
+               z15 : (* (f sp) ≡ SUP.sup sp1) ∨ (* (f sp) <  * sp )
+               z15  = ? -- x<sup (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
                z17 : ⊥
                z17 with z15
                ... | case1 eq = ¬b eq
-               ... | case2 lt = ¬a lt
+               ... | case2 lt = ¬a ?
 
 
      -- ZChain contradicts ¬ Maximal
@@ -1411,7 +1414,8 @@
      z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥
      z04 nmx zc = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as  sp1 ))))
                                                (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) )
-           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ss<sa ))) -- x ≡ f x ̄
+           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc 
+               (sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc  )  ss<sa ))) -- x ≡ f x ̄
            (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where          -- x < f x
           supf = ZChain.supf zc
           msp1 : MinSUP A (ZChain.chain zc)