Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 910:f28f119bfa6f
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 12 Oct 2022 10:23:27 +0900 |
| parents | fec6064b44be |
| children | 3105feb3c4e1 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 18 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Oct 12 01:46:29 2022 +0900 +++ b/src/zorn.agda Wed Oct 12 10:23:27 2022 +0900 @@ -1079,32 +1079,35 @@ psz1≤px = subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x cs01 : supf0 px o< px → odef (UnionCF A f mf ay supf0 px) (supf0 px) cs01 spx<px = ZChain.csupf zc spx<px - cs00 : supf1 (supf1 px) ≡ supf1 px - cs00 = ? csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) csupf2 with trio< z1 px | inspect supf1 z1 csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px - ... | case1 eq = ⟪ ZChain.asupf zc , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x) - record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where - -- supf0 z1 ≡ supf1 z1 ≡ px, z1 o< px - supu=u : supf1 (supf1 z1) ≡ supf1 z1 - supu=u = ? -- ZChain.sup=u zc ? ? ? ... | case2 lt = zc12 (case1 cs03) where cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) + ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) ) + ... | case1 sfz=sfpx = zc12 (case2 (init (ZChain.asupf zc) cs04 )) where + supu=u : supf1 (supf1 z1) ≡ supf1 z1 + supu=u = trans (cong supf1 sfz=px) (sym sfz=sfpx) + cs04 : supf0 px ≡ supf0 z1 + cs04 = begin + supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩ + supf1 px ≡⟨ sym sfz=sfpx ⟩ + supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a) ⟩ + supf0 z1 ∎ where open ≡-Reasoning + ... | case2 sfz<sfpx = ? --- supf0 z1 o< supf0 px csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) - csupf2 | tri> ¬a ¬b c | record { eq = eq1 } = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x) + csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } with trio< sp1 px + ... | tri< sp1<px ¬b ¬c = ? -- sp1 o< px, supf0 sp1 ≡ supf0 px, sp1 o< z1 + ... | tri≈ ¬a sp1=px ¬c = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x) record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where - -- supf1 z1 ≡ sp1, px o< z1, sp1 o< x + -- supf1 z1 ≡ sp1, px o< z1, sp1 o< x -- sp1 o< z1 + -- supf1 sp1 o≤ supf1 z1 ≡ sp1 o< z1 asm : odef A (supf1 z1) - asm = subst (λ k → odef A k ) (sym (sf1=sp1 c)) ( MinSUP.asm sup1) - sp1=px : sp1 ≡ px - sp1=px with trio< sp1 px - ... | tri< a ¬b ¬c = ? -- sp1 o< px, supf0 sp1 ≡ supf0 px - ... | tri≈ ¬a b ¬c = b - ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x ⟫ ) + asm = subst (λ k → odef A k ) (sym (sf1=sp1 px<z1)) ( MinSUP.asm sup1) supu=u : supf1 (supf1 z1) ≡ supf1 z1 supu=u = ? + ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x ⟫ ) zc4 : ZChain A f mf ay x --- x o≤ supf px zc4 with trio< x (supf0 px)