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

changeset 946:3377379a1479

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 11:28:47 +0900
parents da156642b8d0
children a028409f5ca2
files src/zorn.agda
diffstat 1 files changed, 41 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Oct 31 02:08:52 2022 +0900
+++ b/src/zorn.agda	Mon Oct 31 11:28:47 2022 +0900
@@ -1465,6 +1465,29 @@
                     ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1)  ) 
                     ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt) 
 
+          fsc<<d : {mc z : Ordinal } → (asc : odef A (supf mc)) → (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc )) 
+             → (fc : FClosure A (cf nmx) (supf mc) z) → z << MinSUP.sup spd
+          fsc<<d {mc} {z} asc spd fc = z25 where
+                d1 :  Ordinal
+                d1 = MinSUP.sup spd -- supf d1 ≡ d
+                z24 : (z ≡ d1) ∨ ( z << d1 )
+                z24 = MinSUP.x<sup spd fc
+                --
+                --   f ( f .. ( supf mc ) <= d1
+                --   f d1 <= d1
+                --
+                z25 : z << d1
+                z25 with z24
+                ... | case2 lt = lt
+                ... | case1 eq = ⊥-elim ( <-irr z29 (proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) ) )  where
+                    --  supf mc ≡ d1
+                    z32 : ((cf nmx z) ≡ d1) ∨ ( (cf nmx z) << d1 )
+                    z32 = MinSUP.x<sup spd (fsuc _ fc)
+                    z29 :  (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1)
+                    z29  with z32
+                    ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1)  ) 
+                    ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt) 
+
           smc<<d : supf mc << d
           smc<<d = sc<<d asc spd
 
@@ -1505,6 +1528,10 @@
                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
@@ -1521,16 +1548,27 @@
                    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 = ?
+                   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 = ?
+                   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 = ?
+                   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)