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

changeset 972:520aff512969

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, 07 Nov 2022 16:08:29 +0900
parents 4fdf889ca95a
children 2a67cae517d8
files src/zorn.agda
diffstat 1 files changed, 23 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon Nov 07 10:23:53 2022 +0900
+++ b/src/zorn.agda	Mon Nov 07 16:08:29 2022 +0900
@@ -861,8 +861,13 @@
           sup1 = minsupP pchainpx pcha ptotal
           sp1 = MinSUP.sup sup1
 
-          sfpx<sp1 : supf0 px <= sp1
-          sfpx<sp1 = MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl ))
+          sfpx<=sp1 : supf0 px <= sp1
+          sfpx<=sp1 = MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl ))
+
+          sfpx≤sp1 : supf0 px o≤ sp1
+          sfpx≤sp1 = subst ( λ k → k o≤ sp1) (sym (ZChain.supf-is-minsup zc o≤-refl ))  
+            ( MinSUP.minsup (ZChain.minsup zc o≤-refl) (MinSUP.asm sup1)  
+              (λ {x} ux → MinSUP.x≤sup sup1 (case1 ux)) )
 
           --
           --     supf0 px o≤ sp1
@@ -882,14 +887,14 @@
           --  supf px ≡ px → UnionCF A f mf ay supf px ⊂ UnionCF A f mf ay supf x ≡ pchainx
           --  x < supf px  → UnionCF A f mf ay supf px ≡ UnionCF A f mf ay supf x
 
-          zc43 :  ( x o< sp1 ) ∨ ( sp1 o≤ x )
-          zc43 with trio< x sp1
+          zc43 : (x : Ordinal ) → ( x o< sp1 ) ∨ ( sp1 o≤ x )
+          zc43 x with trio< x sp1
           ... | tri< a ¬b ¬c = case1 a
           ... | tri≈ ¬a b ¬c = case2 (o≤-refl0 (sym b))
           ... | tri> ¬a ¬b c = case2 (o<→≤ c)
           
           zc41 : ZChain A f mf ay x
-          zc41 with zc43
+          zc41 with zc43 x
           zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ?
               ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1    }  where
                  --  supf0 px is included in the chain of sp1
@@ -1203,9 +1208,19 @@
                            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) = ?
-                     csupf2 | case1 p = ?
+                     csupf2 | case2 (case1 p) with trio< (supf0 px) sp1 --  ¬ (supf0 px o< sp1  --  sp1 o≤ spuf0 px)
+                     ... | tri< a ¬b ¬c = ⊥-elim (p a)
+                     ... | tri≈ ¬a b ¬c = ?
+                     ... | tri> ¬a ¬b c = ⊥-elim ( o≤> sfpx≤sp1 c )
+                     csupf2 | case1 p with trio< (supf0 px) px           --  ¬ (supf0 px ≡ px )
+                     ... | tri< sf0px<px ¬b ¬c = ? where
+                           cs10 : odef (UnionCF A f mf ay supf0 px) (supf0 px)
+                           cs10 = ZChain.csupf zc sf0px<px
+                     ... | tri≈ ¬a b ¬c = ⊥-elim (p b)
+                     ... | tri> ¬a ¬b px<sf0px = ? where
+                           cs11 : px o< z1 →  odef (UnionCF A f mf ay supf1 x) (supf1 z1)
+                           cs11 px<z1 = ⊥-elim ( ¬p<x<op ⟪ px<sf0px , subst₂ (λ j k → j o< k ) refl (sym (Oprev.oprev=x op)) 
+                              (ordtrans≤-< (subst (λ k → supf0 px o< k) (cong osuc (sym (sf1=sp1 px<z1 )))  sfpx≤sp1 ) sz1<x) ⟫ )
 
 
           zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?