Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 911:3105feb3c4e1
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 12 Oct 2022 11:11:42 +0900 |
| parents | f28f119bfa6f |
| children | 870a6b57dd39 8695050933a7 4c33f8383d7d |
| files | src/zorn.agda |
| diffstat | 1 files changed, 9 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Oct 12 10:23:27 2022 +0900 +++ b/src/zorn.agda Wed Oct 12 11:11:42 2022 +0900 @@ -1091,10 +1091,10 @@ 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 + 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 px<z1 | record { eq = eq1 } with trio< sp1 px @@ -1105,6 +1105,11 @@ -- 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 ⟫ )