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

changeset 978:94357ced682d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... csupf is bad
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 09 Nov 2022 03:14:40 +0900
parents 2a67cae517d8
children 6229017a6176 0d8dafbecb0d
files src/zorn.agda
diffstat 1 files changed, 16 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Nov 07 17:56:03 2022 +0900
+++ b/src/zorn.agda	Wed Nov 09 03:14:40 2022 +0900
@@ -490,9 +490,9 @@
         → ( { x : Ordinal } → z o≤ x → supf z o≤ supf1 x)
         → UnionCF A f mf ay supf z ⊆' UnionCF A f mf ay supf1 z
 UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-UChain⊆ A f mf {z} {y} ay {supf} {supf1} spuf-mono eq<x lex ⟪ az , ch-is-sup u {x} u<x is-sup fc ⟫ = ⟪ az , ch-is-sup u u<x1 cp1 fc1 ⟫  where
+UChain⊆ A f mf {z} {y} ay {supf} {supf1} supf-mono eq<x lex ⟪ az , ch-is-sup u {x} u<x is-sup fc ⟫ = ⟪ az , ch-is-sup u u<x1 cp1 fc1 ⟫  where
           u<x0 : u o< z
-          u<x0 = supf-inject0 spuf-mono u<x
+          u<x0 = supf-inject0 supf-mono u<x
           u<x1 : supf1 u o< supf1 z
           u<x1 = subst (λ k → k o< supf1 z ) (eq<x u<x0) (ordtrans<-≤ u<x (lex o≤-refl ) )
           fc1 : FClosure A f (supf1 u) x
@@ -958,7 +958,7 @@
                  ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) px<x ))
                  ... | tri> ¬a ¬b c = subst₂ (λ j k → j o≤ k ) (trans (sf1=sf0 o≤-refl ) (sym (ZChain.supfmax zc px<x))) (sf1=sp1 c) 
                      (supf1-mono (o<→≤ c ))
-                      --  px o<z → spuf0 x ≡ supf0 px ≡ supf1 px o≤ supf1 z
+                      --  px o<z → supf x ≡ supf0 px ≡ supf1 px o≤ supf1 z
 
                  fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z
                  fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sf1=sf0 u≤px) fc
@@ -1127,7 +1127,7 @@
                               zc17 :  {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px →
                                     FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px)
                               zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx
-                                     (MinSUP.x≤sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where
+                                     (MinSUP.x≤sup mins (zc25 (fcup fc (o<→≤ s<px) )) ) where
                                   mins : MinSUP A (UnionCF A f mf ay supf0 px)
                                   mins = ZChain.minsup zc o≤-refl
                                   mins-is-spx : MinSUP.sup mins ≡ supf1 px
@@ -1136,9 +1136,9 @@
                                   s<px = supf-inject0 supf1-mono ss<spx
                                   sf<px : supf0 s o< px
                                   sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sfpx=px)) ss<spx
-                                  csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
-                                  csupf17 (init as refl ) = ZChain.csupf zc sf<px
-                                  csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc)
+                                  zc25 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
+                                  zc25 (init as refl ) = ZChain.csupf zc sf<px
+                                  zc25 (fsuc x fc) = ZChain.f-next zc (zc25 fc)
 
 
                  record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where
@@ -1173,6 +1173,13 @@
                         odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2
                     ms01 {sup2} us P = MinSUP.minsup m ? ?
 
+                 csupf0 : {z1 : Ordinal } → supf1 z1 o< px → z1 o≤ px  → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
+                 csupf0 {z1} s0z<px z≤px = subst (λ k → odef (UnionCF A f mf ay supf1 x) k ) (sym (sf1=sf0 z≤px)) (
+                       UChain⊆ A f mf {x} {y} ay {supf0} {supf1} (ZChain.supf-mono zc) sf=eq sf≤ 
+                         (chain-mono f mf ay supf0 (ZChain.supf-mono zc) (o<→≤ px<x) 
+                         (ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 z≤px) s0z<px))))
+                 -- px o< z1 , px o≤ supf1 z1  -->   px o≤ sp1 o< x -- sp1 ≡ px--> odef (UnionCF A f mf ay supf1 x) sp1
+
                  csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
                  csupf1 {z1} sz1<x = csupf2 where
                      --  z1 o< px → supf1 z1 ≡ supf0 z1
@@ -1208,7 +1215,7 @@
                            cs08 = subst (λ k → k o< sp1 ) (proj1 p) (proj2 p )
                            cs09 : sp1 o< osuc px
                            cs09  = subst ( λ k → sp1 o< k ) (sym (Oprev.oprev=x op)) sz1<x 
-                     csupf2 | case2 (case1 p) with trio< (supf0 px) sp1 --  ¬ (supf0 px o< sp1  --  sp1 o≤ spuf0 px)
+                     csupf2 | case2 (case1 p) with trio< (supf0 px) sp1 --  ¬ (supf0 px o< sp1  --  sp1 o≤ supf px)
                      ... | tri< a ¬b ¬c = ⊥-elim (p a)
                      ... | tri≈ ¬a b ¬c = ?
                      ... | tri> ¬a ¬b c = ⊥-elim ( o≤> sfpx≤sp1 c )
@@ -1757,7 +1764,7 @@
                     z61 : u ≡ supf mc → (a ≡ d ) ∨ ( * a < * d )
                     z61 u=sc = case2 (fsc<<d {mc} asc spd (subst (λ k → FClosure A (cf nmx) k a) (trans (ChainP.supu=u is-sup1) u=sc) fc ) )
                     -- u<x    : ZChain.supf zc u o< ZChain.supf zc d
-                    --     supf u o< spuf c → order
+                    --     supf u o< supf c → order
 
           sd=d : supf d ≡ d
           sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫