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

changeset 948:51556591c879

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 31 Oct 2022 18:34:06 +0900
parents a028409f5ca2
children efc833407350
files src/zorn.agda
diffstat 1 files changed, 21 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Oct 31 15:36:58 2022 +0900
+++ b/src/zorn.agda	Mon Oct 31 18:34:06 2022 +0900
@@ -1524,28 +1524,27 @@
 
           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 )
+          not-hasprev record { ax = ax ; y = y ; ay =   ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z46 z30 ) where
+                z45 : (* (cf nmx (cf nmx y)) ≡ * d) ∨ (* (cf nmx (cf nmx y)) < * d) → (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d)
+                z45 p = subst (λ k → (* (cf nmx k) ≡ * d) ∨ (* (cf nmx k) < * d)) (sym x=fy) p
+                z48 : supf mc << d
+                z48 = sc<<d {mc} asc spd
+                z47 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )) 
+                    →  * (cf nmx (cf nmx y)) < * d1
+                z47 {mc} {d1} {asc} spd = ?
+                z30 : * d < * (cf nmx d)
+                z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd))
+                z46 : (* (cf nmx d) ≡ * d) ∨ (* (cf nmx d) < * d)
+                z46 = z45 (case2 (z47 {mc} {d} {asc} spd  ))
+
+-- ax      : odef A d
+-- y       : Ordinal
+-- ua1     : odef A y
+-- u       : Ordinal
+-- u<x     : supf u o< supf d
+-- is-sup1 : ChainP A (cf nmx) (cf-is-≤-monotonic nmx) as0 supf u
+-- fc      : FClosure A (cf nmx) (supf u) y
+-- x=fy    : d ≡ cf nmx y
 
           sd=d : supf d ≡ d
           sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫