Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1055:60211e5b1fe5
order (px case) done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 09 Dec 2022 23:27:05 +0900 |
| parents | 38148b08d85c |
| children | 0dff7ab7a55f |
| files | src/zorn.agda |
| diffstat | 1 files changed, 8 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Dec 09 22:59:10 2022 +0900 +++ b/src/zorn.agda Fri Dec 09 23:27:05 2022 +0900 @@ -1253,14 +1253,14 @@ (ordtrans<-≤ sa<sb (o≤-refl0 (sym (sf1=sf0 (o≤-refl0 b=px))) ))) where x≤sa : x o≤ supf1 a x≤sa = subst (λ k → k o≤ supf1 a ) (trans (cong osuc b=px) (Oprev.oprev=x op)) (osucc b<sa ) - ... | case1 b=sa = z28 where - a<x : a o< x - a<x = ? - z28 : odef (UnionCF A f ay supf0 b) w - z28 with cfcs a<x ? ? fc - ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ - ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u ? ? (fcup fc ?) ⟫ - -- px ≡ supf1 a + ... | case1 b=sa = ⊥-elim (o<¬≡ sa=sb sa<sb) where + sa=sb : supf1 a ≡ supf0 b + sa=sb = begin + supf1 a ≡⟨ sf1=sf0 a≤px ⟩ + supf0 a ≡⟨ sym (ZChain.supf-idem zc a≤px (o≤-refl0 (sym (trans (sym b=px) (trans b=sa (sf1=sf0 a≤px) ))))) ⟩ + supf0 (supf0 a) ≡⟨ cong supf0 (sym (sf1=sf0 a≤px )) ⟩ + supf0 (supf1 a) ≡⟨ cong supf0 (sym b=sa) ⟩ + supf0 b ∎ where open ≡-Reasoning ... | case1 sa<b with cfcs a<b b≤x sa<b fc ... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ ... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u u<x (trans (sym (sf1=sf0 u≤px)) su=u) (fcup fc u≤px) ⟫ where