Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 945:da156642b8d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
memory exhaust work around
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 31 Oct 2022 02:08:52 +0900
parents e1d727251e25
children 3377379a1479
files src/zorn.agda
diffstat 1 files changed, 19 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Oct 30 22:53:22 2022 +0900
+++ b/src/zorn.agda	Mon Oct 31 02:08:52 2022 +0900
@@ -1493,6 +1493,12 @@
                     -- u<x    : ZChain.supf zc u o< ZChain.supf zc d
                     --     supf u o< spuf c → order
 
+          z43 : (u w : Ordinal ) → ( u o< w ) ∨ ( u ≡  w ) ∨ ( w o< u )
+          z43 u w with trio< u w
+          ... | tri< a ¬b ¬c = case1 a
+          ... | 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)
@@ -1508,7 +1514,7 @@
                   →  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 u mc d1) z30 where
+               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
@@ -1519,13 +1525,18 @@
                    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) ) ))
-                   z26 : (u mc d1 : Ordinal ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
-                   z26 u mc d1 = ? -- with trio< u (supf mc)
-                   -- ... | tri< a ¬b ¬c = ?
-                   -- ... | tri> ¬a ¬b x<z = ?
-                   -- ... | tri≈ ¬a b ¬c = ? -- with  MinSUP.x<sup spd fc
-                   -- ... | case1 eq = ? -- case1 (cong (*) eq)
-                   -- ... | case2 lt = ? -- case2 lt
+                   z40 : ( u ≡ supf mc ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
+                   z40 = ?
+                   z41 : ( u o< supf mc ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
+                   z41 = ?
+                   z42 : ( supf mc o< u ) → (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
+                   z42 = ?
+                   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
 
           sd=d : supf d ≡ d
           sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫