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

changeset 722:0dd8cc755ec9

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, 16 Jul 2022 04:11:07 +0900
parents 562ddd33fe21
children e5cde0cd6a83
files src/zorn.agda
diffstat 1 files changed, 1 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Jul 16 04:05:18 2022 +0900
+++ b/src/zorn.agda	Sat Jul 16 04:11:07 2022 +0900
@@ -718,20 +718,6 @@
           ... | case1 u<x = pzc _ u<x
           ... | case2 u=0 =  subst (λ k → ZChain A f mf ay k ) (sym u=0) (inititalChain f mf {y} ay )
 
-          zcp : {a b : Ordinal} → (za : odef pchain a )
-              → pchain ≡ UnionCF A f mf ay psupf x
-              → b o< x → (ab : odef A b) 
-              → HasPrev A pchain ab f ∨  IsSup A pchain ab 
-              → * a < * b → odef pchain b
-          zcp {a} {b} za cheq b<x ab P a<b = subst (λ k → odef k b) (sym cheq) zc12  where
-              zc13 : odef (UnionCF A f mf ay (ZChain.supf (uzc za)) (UChain.u (proj2 za))) a
-              zc13 = ⟪ proj1 za , record { u = UChain.u (proj2 za) ; u<x = ? ; uchain = ? } ⟫
-              zc14 : b o< UChain.u (proj2 za)
-              zc14 = ?
-              zc12 : odef (UnionCF A f mf ay psupf x) b
-              zc12 = ⟪ ab , record { u = UChain.u (proj2 za) ;  u<x = ? ; uchain = ? } ⟫
-              -- ZChain.is-max (uzc za) ? ? ab (subst (λ k → HasPrev A k ab f ∨  IsSup A k ab ) cheq P)  a<b 
-
           chain-mono : pchain ⊆'  UnionCF A f mf ay psupf x  
           chain-mono {a} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫ = 
                    ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-init a x } ⟫ 
@@ -740,9 +726,6 @@
           chain-mono {.(f x)} ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup (fsuc x fc) } ⟫ = 
                    ⟪ az , record { u = u ; u<x = u<x ; uchain = ch-is-sup ? (fsuc x ?) } ⟫ 
           
-          chain-x : {z : Ordinal } → ¬ ( z << spu ) → odef (UnionCF A f mf ay psupf x) z → odef pchain z
-          chain-x = ?
-
           chain-≡ : UnionCF A f mf ay psupf x ⊆' pchain 
              → UnionCF A f mf ay psupf x ≡ pchain 
           chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono }
@@ -762,7 +745,7 @@
                             * a < * b → odef pchain b
                 z18 {a} {b} za b<x ab P a<b with P
                 ... | case1 pr = subst (λ k → odef pchain k ) (sym (HasPrev.x=fy pr)) ( pnext (HasPrev.ay pr) )
-                ... | case2 b=sup = ? where
+                ... | case2 b=sup = ⟪ proj1 z30 , ? ⟫ where
                     z30 = ZChain.is-max (uzc za) ? ? ab (case2 ?) a<b 
 
                 --⊥-elim ( ¬x=sup record {