Members/kono/Proof/ZF-in-agda: src/zorn.agda comparison

comparison src/zorn.agda @ 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

comparison

equal deleted inserted replaced

-:92275389e623
+:55e82405ec0d
 chain-≡ : pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op )
 → pchain ≡ UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op )
 chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono }
 zc4 : ZChain A f mf ay x
-zc4 with ODC.∋-p O A (* x)
+zc4 with ODC.∋-p O A (* px)
-... | no noax = no-extenion zc1 where -- ¬ A ∋ p, just skip
+... | 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-≡< ?
+zc1 {a} {b} za b<x ab P a<b with trio< b px
-... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
+... | tri< lt ¬b ¬c = zcp za (chain-≡ zc10) lt ab P a<b where
-... | 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 : 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 } ⟫ =
-zc10 {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ =
+⟪ 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 } ⟫ =
-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 } ⟫
-⟪ 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 } ⟫ =
-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 } ⟫
-⟪ 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 ) )
-... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f )
+... | 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
 p-ismax :  {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
-p-ismax {a} {b} ua b<ox ab (case1 hasp) a<b = ?
+p-ismax {a} {b} ua b<x 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 (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) →
 HasPrev A pchain ab f ∨ IsSup A pchain   ab →
 * a < * b → odef pchain b
 ... | tri> ¬a ¬b c = spu
 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
+zcp {a} {b} za cheq b<x ab P a<b = subst (λ k → odef k b) (sym cheq) zc12  where
-zc12 : odef ? b
+zc13 : odef (UnionCF A f mf ay (ZChain.supf (uzc za)) (UChain.u (proj2 za))) a
-zc12 = ZChain.is-max (pzc _ ?) ? ? ab
+zc13 = ⟪ proj1 za , record { u = UChain.u (proj2 za) ; u<x = ? ; uchain = ? } ⟫
-(subst (λ k → HasPrev A k ab f ∨  IsSup A k ab ) ? P)  a<b
+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
 chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono }

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

comparison src/zorn.agda @ 713:55e82405ec0d