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

changeset 941:6f342473f298

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoided
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 29 Oct 2022 14:17:04 +0900
parents aee83a7f9f57
children d396af76c559
files src/zorn.agda
diffstat 1 files changed, 18 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Oct 29 13:55:18 2022 +0900
+++ b/src/zorn.agda	Sat Oct 29 14:17:04 2022 +0900
@@ -1475,21 +1475,26 @@
                     --     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 ( <-irr ? z30 )  where
-               y : Ordinal
-               y = HasPrev.y hp
+          not-hasprev hp = ⊥-elim (z29 spd ? hp)  where
                -- z31 : odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) (cf nmx d)
                -- z31 = ?
-               -- z29 : {mc : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )) 
-               --    →  odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) (cf nmx (MinSUP.sup spd))
-               --    →  (* (cf nmx (MinSUP.sup spd)) ≡ * (MinSUP.sup spd)) ∨ (* (cf nmx (MinSUP.sup spd)) < * (MinSUP.sup spd))
-               -- z29 {mc} {asc} spd afd with  MinSUP.x<sup spd afd
-               -- ... | case1 eq = ?
-               -- ... | case2 lt = ?
-               z30 : * d < * (cf nmx d)
-               z30 = ?
-               z24 : y << d
-               z24 = subst (λ k → y <<  k) (sym (HasPrev.x=fy hp)) ( proj1 (cf-is-<-monotonic nmx y (proj1 (HasPrev.ay hp) ) ))
+               z29 : {mc : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )) 
+                  →  odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) (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 ufd hp = <-irr ? z30 where
+                   y : Ordinal
+                   y = HasPrev.y hp
+                   d1 :  Ordinal
+                   d1 = MinSUP.sup spd -- supf d1 ≡ d
+                   z30 : * d1 < * (cf nmx d1)
+                   z30 = ?
+                   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 (MinSUP.sup spd)) ≡ * (MinSUP.sup spd)) ∨ (* (cf nmx (MinSUP.sup spd)) < * (MinSUP.sup spd))
+                   -- z26 with  MinSUP.x<sup spd ?
+                   -- ... | case1 eq = ?
+                   -- ... | case2 lt = ?
                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