Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 918:4c33f8383d7d
supf px o< px is in csupf
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 15 Oct 2022 20:05:34 +0900 |
| parents | 3105feb3c4e1 |
| children | 213f12f27003 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 12 insertions(+), 20 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Oct 12 11:11:42 2022 +0900 +++ b/src/zorn.agda Sat Oct 15 20:05:34 2022 +0900 @@ -796,6 +796,9 @@ zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) px<x : px o< x px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc + opx=x : osuc px ≡ x + opx=x = Oprev.oprev=x op + zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt @@ -1076,9 +1079,7 @@ -- z1 ≡ px , supf0 px o< px .. px o< z1, x o≤ z1 ... supf1 z1 ≡ sp1 -- z1 ≡ px , supf0 px ≡ px psz1≤px : supf1 z1 o≤ px - 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 + psz1≤px = subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x 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 @@ -1095,24 +1096,15 @@ supf1 px ≡⟨ sym sfz=sfpx ⟩ supf1 z1 ≡⟨ sf1=sf0 (o<→≤ a) ⟩ supf0 z1 ∎ where open ≡-Reasoning - ... | case2 sfz<sfpx = ? --- supf0 z1 o< supf0 px + ... | case2 sfz<sfpx = ⊥-elim ( ¬p<x<op ⟪ cs05 , cs06 ⟫ ) where + --- supf1 z1 ≡ px , z1 o< px , px ≡ supf0 z1 o< supf0 px o< x + cs05 : px o< supf0 px + cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx + cs06 : supf0 px o< osuc px + cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) sfpx<x csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) - 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 -- 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 px<z1)) ( MinSUP.asm sup1) - cs05 : odef (UnionCF A f mf ay supf1 x) (supf1 sp1) - cs05 = zc12 (case2 (init (ZChain.asupf zc) ( begin - supf0 px ≡⟨ sym (sf1=sf0 o≤-refl ) ⟩ - supf1 px ≡⟨ cong supf1 (sym sp1=px) ⟩ - supf1 sp1 ∎ ))) where open ≡-Reasoning - 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 ⟫ ) + csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ? -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ ) + zc4 : ZChain A f mf ay x --- x o≤ supf px zc4 with trio< x (supf0 px)