Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 713:55e82405ec0d
px?
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 15 Jul 2022 10:33:55 +0900 |
| parents | 92275389e623 |
| children | e1ef5e6961ce |
| files | src/zorn.agda |
| diffstat | 1 files changed, 30 insertions(+), 24 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Jul 15 07:44:50 2022 +0900 +++ b/src/zorn.agda Fri Jul 15 10:33:55 2022 +0900 @@ -569,32 +569,34 @@ chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono } zc4 : ZChain A f mf ay x - zc4 with ODC.∋-p O A (* x) - ... | no noax = no-extenion zc1 where -- ¬ A ∋ p, just skip + zc4 with ODC.∋-p O A (* px) + ... | no nopax = no-extenion zc1 where -- ¬ A ∋ p, just skip zc1 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → HasPrev A pchain ab f ∨ IsSup A pchain ab → * a < * b → odef pchain b - zc1 {a} {b} za b<ox ab P a<b with osuc-≡< ? - ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) ) - ... | case2 lt = zcp za (chain-≡ zc10) ? ab P a<b where - zc10 : pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op) - zc10 {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = - ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ - zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ = - ⟪ az , record { u = u ; u<x = case1 ? ; uchain = ch-init z fc } ⟫ - zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = - ⟪ az , record { u = u ; u<x = case1 ? ; uchain = ch-is-sup is-sup fc } ⟫ - ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f ) + zc1 {a} {b} za b<x ab P a<b with trio< b px + ... | tri< lt ¬b ¬c = zcp za (chain-≡ zc10) lt ab P a<b where + zc10 : pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op) + zc10 {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = + ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ + zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ = + ⟪ az , record { u = u ; u<x = case1 ? ; uchain = ch-init z fc } ⟫ + zc10 {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } ⟫ = + ⟪ az , record { u = u ; u<x = case1 ? ; uchain = ch-is-sup is-sup fc } ⟫ + -- ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) ) + ... | tri≈ ¬a b=px ¬c = ? + ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) + ... | yes apx with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) apx f ) -- we have to check adding x preserve is-max ZChain A y f mf x ... | case1 pr = no-extenion ? where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next zc7 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → HasPrev A pchain ab f ∨ IsSup A pchain ab → * a < * b → odef pchain b - zc7 {a} {b} za b<ox ab P a<b with osuc-≡< ? + zc7 {a} {b} za b<x ab P a<b with osuc-≡< ? ... | case2 lt = zcp za ? ? 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 ) + ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) apx ) ... | case1 is-sup = -- x is a sup of zc record { chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal ; initial = pinit ; chain∋init = pcy ; is-max = p-ismax } where @@ -602,8 +604,8 @@ b o< 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<x ab (case1 hasp) a<b = ? + p-ismax {a} {b} ua b<x ab (case2 sup) a<b = ? ... | case2 ¬x=sup = no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention z18 : {a b : Ordinal} → odef pchain a → b o< x → (ab : odef A b) → @@ -668,24 +670,28 @@ uzc : {a : Ordinal } → (za : odef pchain a) → ZChain A f mf ay (UChain.u (proj2 za)) uzc {a} za with UChain.u<x (proj2 za) ... | case1 u<x = pzc _ u<x - ... | case2 u=0 = ? + ... | 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 ≡ ? + → 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 = ? where - zc12 : odef ? b - zc12 = ZChain.is-max (pzc _ ?) ? ? ab - (subst (λ k → HasPrev A k ab f ∨ IsSup A k ab ) ? P) a<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} za = ⟪ proj1 za , record { u = UChain.u (proj2 za) ; u<x = UChain.u<x (proj2 za) ; uchain = zc11 } ⟫ where zc11 : Chain A f mf ay psupf (UChain.u (proj2 za)) a zc11 with UChain.uchain (proj2 za) ... | ch-init .a x = ch-init a x - ... | ch-is-sup is-sup fc = ch-is-sup ? ? + ... | ch-is-sup is-sup fc = ch-is-sup ? (subst (λ k → FClosure A f k a ) ? fc ) chain-≡ : UnionCF A f mf ay psupf x ⊆' pchain → UnionCF A f mf ay psupf x ≡ pchain