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

changeset 986:557f8145d3c1

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 Sat, 12 Nov 2022 18:11:14 +0900
parents 0d8dafbecb0d
children c8c60a05b39b
files src/zorn.agda
diffstat 1 files changed, 24 insertions(+), 30 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Nov 12 01:49:25 2022 +0900
+++ b/src/zorn.agda	Sat Nov 12 18:11:14 2022 +0900
@@ -666,7 +666,7 @@
                 s<z : s o< & A
                 s<z = ordtrans s<b b<z
                 zc04 : odef (UnionCF A f mf ay supf (& A))  (supf s)
-                zc04 = ZChain.csupf zc ? -- (z09 (ZChain.asupf zc))
+                zc04 = ZChain.csupf zc (ordtrans<-≤ ss<sb (ZChain.supf-mono zc (o<→≤ b<z)))
                 zc05 : odef (UnionCF A f mf ay supf b)  (supf s)
                 zc05 with zc04
                 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc  ⟫
@@ -1027,7 +1027,7 @@
                         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 : Ordinal } → supf1 z1 o< supf1 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) 
@@ -1035,7 +1035,13 @@
                  -- 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< supf1 x → odef (UnionCF A f mf ay supf1 x) (supf1 z1)
-                 csupf1 {z1} sz<sx = ⟪ ? , ch-is-sup (supf1 z1) ? ? (init ? ? ) ⟫
+                 csupf1 {z1} sz<sx = ⟪ asupf1 , ch-is-sup (supf1 z1) (subst (λ k → k o< supf1 x) (sym cs00) sz<sx) cp (init asupf1 cs00 ) ⟫ where
+                     z<x : z1 o< x
+                     z<x = supf-inject0 supf1-mono sz<sx
+                     cs00 :  supf1 (supf1 z1) ≡ supf1 z1
+                     cs00 = ?
+                     cp : ChainP A f mf ay supf1 (supf1 z1) 
+                     cp = ?
 
 
           zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?
@@ -1417,35 +1423,23 @@
 
           sc<<d : {mc : Ordinal } → (asc : odef A (supf mc)) → (spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc ))
              → supf mc << MinSUP.sup spd
-          sc<<d {mc} asc spd = z25 where
-                d1 :  Ordinal
-                d1 = MinSUP.sup spd -- supf d1 ≡ d
-                z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 )
-                z24 = MinSUP.x≤sup spd (init asc refl)
-                --
-                --   f ( f .. ( supf mc ) <= d1
-                --   f d1 <= d1
-                --
-                z25 : supf mc << 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 (supf mc)) ≡ d1) ∨ ( (cf nmx (supf mc)) << d1 )
-                    z32 = MinSUP.x≤sup spd (fsuc _ (init asc refl))
-                    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)
-
-          z11 : odef (ZChain.chain zc) d
-          z11 = ZChain1.is-max (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) {& s} ? ? ? ? ? where
-
-          z10 : supf d o≤ supf (& A)
-          z10 = ?
+          sc<<d {mc} asc spd with MinSUP.x≤sup spd (init asc refl)
+          ... | case1 eq = ?
+          ... | case2 lt = ?
 
           ss<sa : supf c o< supf (& A)
-          ss<sa = ?
+          ss<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ c<A))
+          ... | case2 sc<sa = sc<sa
+          ... | case1 sc=sa = ⊥-elim (  nmx record { maximal = * d ; as = subst (λ k → odef A k) (sym &iso) (MinSUP.asm spd) 
+                ; ¬maximal<x = λ {x} ax → subst₂ (λ j k → ¬ ( j < k)) refl *iso (zc10 sc=sa ax) } ) where 
+             zc10 : supf c ≡ supf (& A) → {x : Ordinal } → odef A x  → ¬ ( d << x )
+             zc10 = ? --    supf x o≤ supf c → supf x ≡ supf c ∨ supf x o< supf c
+                    --      c << x → x is sup of chain or x = f ( .. ( f c ))
+                    --      c << x → x is not in chain
+                    --      supf c o≤ x (minimulity)
+                    --  odef chain z → supf z o< supf (& A) ≡ supf c → minimulity  c o≤ supf c 
+                    --   supf c o≤ supf (supf c) o≤ supf x o≤ supf (& A)
+                    --   supf c ≡ supf (supf c) ≡ supf x  ≡ supf (& A)  means supf of FClosure of (supf c) is Maximal
 
      zorn00 : Maximal A
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM