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

changeset 944:e1d727251e25

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bad with trio< o
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 30 Oct 2022 22:53:22 +0900
parents df68bb333cd0
children da156642b8d0
files src/zorn.agda
diffstat 1 files changed, 23 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Oct 30 18:19:33 2022 +0900
+++ b/src/zorn.agda	Sun Oct 30 22:53:22 2022 +0900
@@ -1480,9 +1480,7 @@
                    z30 : * mc < * (cf nmx mc)
                    z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1))
                    z26 : (* (cf nmx mc) ≡ * mc) ∨ (* (cf nmx mc) < * mc)
-                   z26 with  MinSUP.x<sup msp1 ?
-                   ... | case1 eq = case1 (cong (*) eq)
-                   ... | case2 lt = case2 lt
+                   z26 = ?
 
           is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd)
           is-sup = record { x<sup = z22 } where
@@ -1496,33 +1494,38 @@
                     --     supf u o< spuf c → order
 
           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 hp )  where
+          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 ))))
+               --   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 hp = <-irr z26 z30 where
+               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
                    y : Ordinal
-                   y = HasPrev.y hp
+                   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
-                   z31 :  odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) (cf nmx (MinSUP.sup spd))
-                   z31 = ?
                    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) ) ))
-                   z26 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
-                   z26 with  MinSUP.x<sup spd z31
-                   ... | case1 eq = case1 (cong (*) eq)
-                   ... | case2 lt = case2 lt
-               --   case1 : FClosure of y
-               --   case2 : u o< supf mc
-               --   case3 : u ≡ supf mc      z31
-               --   case4 : supf mc o< u     ⊥ ( why ? )
-               z25 : odef (ZChain.chain zc) (cf nmx d)
-               z25 = 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 ))))
+                   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
 
           sd=d : supf d ≡ d
           sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫