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

changeset 699:4df0b36db305

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 Tue, 12 Jul 2022 15:42:33 +0900
parents 3837fa940cd9
children 3de5a1fb8011
files src/zorn.agda
diffstat 1 files changed, 3 insertions(+), 39 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jul 12 15:29:41 2022 +0900
+++ b/src/zorn.agda	Tue Jul 12 15:42:33 2022 +0900
@@ -556,35 +556,9 @@
           zc0-b<x : (b : Ordinal ) → b o< x → b o< osuc px
           zc0-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
 
-          -- if previous chain satisfies maximality, we caan reuse it
-          --
-          no-extenion : ( {a b z : Ordinal} → (z<x : z o< x)  → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
-                    HasPrev A (ZChain.chain zc ) ab f ∨  IsSup A (ZChain.chain zc ) ab →
-                            * a < * b → odef (ZChain.chain zc ) b ) → ZChain A f mf ay zc0 x
-          no-extenion is-max  = record { initial = ZChain.initial zc ; chain∋init = ZChain.chain∋init zc }
 
           zc4 : ZChain A f mf ay zc0 x 
-          zc4 with ODC.∋-p O A (* x)
-          ... | no noax = no-extenion zc1  where -- ¬ A ∋ p, just skip
-                zc1 : {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc ) a → b o< osuc x → (ab : odef A b) →
-                    HasPrev A (ZChain.chain zc ) ab f ∨  IsSup A (ZChain.chain zc ) ab →
-                            * a < * b → odef (ZChain.chain zc ) b
-                zc1 {a} {b} z<x za b<ox ab P a<b with osuc-≡< b<ox
-                ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
-                ... | case2 lt = ZChain.is-max zc za (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt ) ab P a<b
-          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f )   
-               -- we have to check adding x preserve is-max ZChain A y f mf zc0 x
-          ... | case1 pr = no-extenion zc7  where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
-                chain0 = ZChain.chain zc 
-                zc7 :  {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc ) a → b o< osuc x → (ab : odef A b) →
-                            HasPrev A (ZChain.chain zc ) ab f ∨ IsSup A (ZChain.chain zc ) ab →
-                            * a < * b → odef (ZChain.chain zc ) b
-                zc7 {a} {b} z<x za b<ox ab P a<b with osuc-≡< b<ox
-                ... | case2 lt = ZChain.is-max zc za (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt ) ab P a<b
-                ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
-          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
-          ... | case1 is-sup = -- x is a sup of zc 
-                record {  chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
+          zc4 = record {  chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal
                      ; initial = pinit ; chain∋init  = pcy ; is-max = p-ismax } where
                 pchain : HOD
                 pchain = UnionCF A f mf ay (ZChain1.supf (zc0 (& A))) (& A)
@@ -616,19 +590,9 @@
                     b o< osuc x → (ab : odef A b) →
                     ( HasPrev A pchain ab f ∨ IsSup A pchain ab ) →
                         * a < * b → odef pchain b
-                p-ismax {a} {b} ua b<ox ab (case1 hasp) a<b = ?
-                p-ismax {a} {b} ua b<ox ab (case2 sup)  a<b = ?
+                p-ismax {a} {b} ua b<ox ab (case1 hasp) a<b = ⟪ ab , ? ⟫
+                p-ismax {a} {b} ua b<ox ab (case2 sup)  a<b = ⟪ ab , ? ⟫
 
-          ... | case2 ¬x=sup =  no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
-                z18 :  {a b z : Ordinal} → (z<x : z o< x) → odef (ZChain.chain zc ) a → b o< osuc x → (ab : odef A b) →
-                            HasPrev A (ZChain.chain zc ) ab f ∨ IsSup A (ZChain.chain zc )   ab →
-                            * a < * b → odef (ZChain.chain zc ) b
-                z18 {a} {b} z<x za b<x ab p a<b with osuc-≡< b<x
-                ... | case2 lt = ZChain.is-max zc za (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt ) ab p a<b 
-                ... | case1 b=x with p
-                ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
-                ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
-                      x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy )  } ) 
      ... | no op = zc5 where
           uzc : {z : Ordinal} → (u : UChain A f mf ay (ZChain1.supf (zc0 (& A))) x z ) → ZChain A f mf ay zc0 (UChain.u u)
           uzc {z} u =  prev (UChain.u u) (UChain.u<x u)