Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1026:8b3d7c461a84
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 26 Nov 2022 07:51:09 +0900 |
| parents | e4919cc0cfe8 |
| children | 91988ae176ab |
| files | src/zorn.agda |
| diffstat | 1 files changed, 19 insertions(+), 16 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Nov 25 23:39:04 2022 +0900 +++ b/src/zorn.agda Sat Nov 26 07:51:09 2022 +0900 @@ -1070,17 +1070,20 @@ ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) z51 cp (subst (λ k → FClosure A f k w) z52 fc) ⟫ where sa≤px : supf0 a o≤ px sa≤px = subst₂ (λ j k → j o< k) px=sa (sym (Oprev.oprev=x op)) px<x + spx=sa : supf0 px ≡ supf0 a + spx=sa = begin + supf0 px ≡⟨ cong supf0 px=sa ⟩ + supf0 (supf0 a) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩ + supf0 a ∎ where open ≡-Reasoning z51 : supf0 px o< b - z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ cong supf0 px=sa ⟩ - supf0 (supf0 a ) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩ + z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ spx=sa ⟩ supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩ supf1 a ∎ )) sa<b where open ≡-Reasoning z52 : supf1 a ≡ supf1 (supf0 px) z52 = begin supf1 a ≡⟨ sf1=sf0 a≤px ⟩ supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩ supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px) ⟩ - supf1 (supf0 a) ≡⟨ cong supf1 (sym (ZChain.supf-idem zc mf< a≤px sa≤px )) ⟩ - supf1 (supf0 (supf0 a)) ≡⟨ cong (λ k → supf1 (supf0 k)) (sym px=sa) ⟩ + supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa) ⟩ supf1 (supf0 px) ∎ where open ≡-Reasoning m : MinSUP A (UnionCF A f mf ay supf0 px) m = ZChain.minsup zc o≤-refl @@ -1088,15 +1091,13 @@ m=spx = begin MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc o≤-refl) ⟩ supf0 px ≡⟨ cong supf0 px=sa ⟩ - supf0 (supf0 a) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩ - supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩ - supf1 a ≡⟨ z52 ⟩ + supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px) ⟩ + supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa) ⟩ supf1 (supf0 px) ∎ where open ≡-Reasoning z53 : supf1 (supf0 px) ≡ supf0 px z53 = begin - supf1 (supf0 px) ≡⟨ sym z52 ⟩ - supf1 a ≡⟨ sf1=sf0 a≤px ⟩ - supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩ + supf1 (supf0 px) ≡⟨ cong supf1 spx=sa ⟩ + supf1 (supf0 a) ≡⟨ sf1=sf0 sa≤px ⟩ supf0 (supf0 a) ≡⟨ sym ( cong supf0 px=sa ) ⟩ supf0 px ∎ where open ≡-Reasoning cp : ChainP A f mf ay supf1 (supf0 px) @@ -1106,15 +1107,17 @@ uz : {s z1 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<px o≤-refl ss<px (subst (λ k → FClosure A f k z1) (sf1=sf0 (o<→≤ s<px)) fc ) where + s<spx : s o< supf0 px + s<spx = supf-inject0 supf1-mono ss<sp s<px : s o< px - s<px = ZChain.supf-inject zc (osucprev ( begin - osuc (supf0 s) ≡⟨ sym (cong osuc (sf1=sf0 ?) ) ⟩ - osuc (supf1 s) ≤⟨ osucc ss<sp ⟩ - supf1 (supf0 px) ≡⟨ z53 ⟩ - supf0 px ∎ )) where open o≤-Reasoning O + s<px = osucprev ( begin + osuc s ≤⟨ osucc s<spx ⟩ + supf0 px ≡⟨ spx=sa ⟩ + supf0 a ≡⟨ sym px=sa ⟩ + px ∎ ) where open o≤-Reasoning O ss<px : supf0 s o< px ss<px = osucprev ( begin - osuc (supf0 s) ≡⟨ sym (cong osuc (sf1=sf0 ?) ) ⟩ + osuc (supf0 s) ≡⟨ cong osuc (sym (sf1=sf0 (o<→≤ s<px))) ⟩ osuc (supf1 s) ≤⟨ osucc ss<sp ⟩ supf1 (supf0 px) ≡⟨ sym z52 ⟩ supf1 a ≡⟨ sf1=sf0 a≤px ⟩