# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1667198218 -32400
# Node ID a028409f5ca22d8af7f2d8e978fc92d4749526a6
# Parent  3377379a147964b7925a368057e4ba06596f1aef
avoid memory exhaust

diff -r 3377379a1479 -r a028409f5ca2 src/zorn.agda
--- a/src/zorn.agda	Mon Oct 31 11:28:47 2022 +0900
+++ b/src/zorn.agda	Mon Oct 31 15:36:58 2022 +0900
@@ -1522,59 +1522,30 @@
           ... | tri≈ ¬a b ¬c = case2 (case1 b)
           ... | tri> ¬a ¬b c = case2 (case2 c) 
 
-          not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) d (cf nmx)
-          not-hasprev hp = ⊥-elim (z29 {mc} {asc} spd z31 hp )  where
-               z31 : odef (ZChain.chain zc) (cf nmx d)
-               z31 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp))
-                   (ZChain.f-next zc 
-                   (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ d<A) ( HasPrev.ay hp ))))
-               z32 : odef (ZChain.chain zc) d
-               z32 =  subst (λ k → odef (ZChain.chain zc) k) (sym (HasPrev.x=fy hp))
-                   (ZChain.f-next zc 
-                   (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ d<A) ( HasPrev.ay hp )))
-               --   case1 : FClosure of s
-               --   case2 : u o< supf mc
-               --   case3 : u ≡ supf mc      z31
-               --   case4 : supf mc o< u     ⊥ ( why ? )
-               z29 : {mc : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )) 
-                  →  odef (ZChain.chain zc) (cf nmx (MinSUP.sup spd))
-                  →  HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) (MinSUP.sup spd) (cf nmx)
-                  →  ⊥
-               z29 {mc} {asc} spd  ⟪ aa , ch-init fc ⟫  hp = ?
-               z29 {mc} {asc} spd  ⟪ aa , ch-is-sup u u<x is-sup fc ⟫  hp = <-irr z26 z30 where
-                   y : Ordinal
-                   y = HasPrev.y hp -- cf nmx y ≡ d1
-                   zy : odef (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) (MinSUP.sup spd)) y
-                   zy = HasPrev.ay hp
-                   d1 :  Ordinal
-                   d1 = MinSUP.sup spd -- supf d1 ≡ d
-                   z45 : (* (cf nmx (cf nmx y)) ≡ * d1) ∨ (* (cf nmx (cf nmx y)) < * d1) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
-                   z45 p = subst (λ k → (* (cf nmx k) ≡ * d1) ∨ (* (cf nmx k) < * d1)) (sym (HasPrev.x=fy hp)) p
-                   z30 : * d1 < * (cf nmx d1)
-                   z30 = proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd))
-                   z24 : y << d1
-                   z24 = subst (λ k → y <<  k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) ))
-                   z40 : ( u ≡ supf mc ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
-                   z40 eq1 with  MinSUP.x<sup spd (subst (λ k → FClosure A (cf nmx) k (cf nmx d1) ) (trans (ChainP.supu=u is-sup) eq1 ) fc )
-                   ... | case1 eq = case1 (cong (*) eq)
-                   ... | case2 lt = case2 lt
-                   postulate 
-                      sc : Ordinal
-                      sc=sc : supf mc ≡ sc
-                   z41 : ( u o< supf mc ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
-                   z41 u<sc with  MinSUP.x<sup spd {sc} (init asc sc=sc )
-                   ... | case2 lt = ?   -- sc << d1, u o< mc, supf u ≤ sc, spuf u << d1
-                   ... | case1 eq = ?
-                   z42 : ( supf mc o< u ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
-                   z42 sc<u = ? where --   spuf mc o< spuf u, mc o< u, ,l
-                        z44 : ( cf nmx d1 ≡ supf u ) ∨ ( cf nmx d1 << supf u )
-                        z44 = ChainP.order is-sup (subst (λ k → supf mc o< k ) ? sc<u ) (init ? ? )
-                   postulate
-                      z26 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
-                   -- z26 with z43 u (supf mc)
-                   -- ... | case1 lt = z41 lt
-                   -- ... | case2 (case1 eq) = z40 eq
-                   -- ... | case2 (case2 lt) = z42 lt
+          not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d) d (cf nmx)
+          not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ?
+          not-hasprev record { ax = ax ; y = y ; ay =   ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ?
+--               z29 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )) 
+--                  →  d1 ≡ MinSUP.sup spd
+--                  →  HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf d1) d1 (cf nmx)
+--                  →  ⊥
+--               z29 {mc} {asc} spd d1=spd hp with HasPrev.ay hp
+--               ... | ⟪ ua1 , ch-init fc ⟫ = ?
+--               ... | ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫ = ? 
+--                   y : Ordinal
+--                   y = HasPrev.y hp 
+--                   d1 :  Ordinal
+--                   d1 = MinSUP.sup spd -- supf d1 ≡ d
+--                   z45 : (* (cf nmx (cf nmx y)) ≡ * d1) ∨ (* (cf nmx (cf nmx y)) < * d1) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
+--                   z45 p = subst (λ k → (* (cf nmx k) ≡ * d1) ∨ (* (cf nmx k) < * d1)) (sym (HasPrev.x=fy hp)) p
+--                   z30 : * d1 < * (cf nmx d1)
+--                   z30 = proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd))
+--                   z47 : * (cf nmx (cf nmx y)) < * d1
+--                   z47 = ?
+--                   z24 : y << d1
+--                   z24 = subst (λ k → y <<  k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) ))
+--                   z46 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
+--                   z46 = z45 (case2 z47 )
 
           sd=d : supf d ≡ d
           sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫