Mercurial > hg > Members > ryokka > HoareLogic

comparison utilities.agda @ 79:52d957db0222

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author ryokka
date Mon, 30 Dec 2019 20:53:00 +0900
parents a39a82820742
children 07b183a726f6
comparison
equal deleted inserted replaced
78:083a18424f75 79:52d957db0222
61 ≡⟨ cong ( λ z → suc z ) (+-sym {y} {x}) ⟩ 61 ≡⟨ cong ( λ z → suc z ) (+-sym {y} {x}) ⟩
62 suc (x + y) 62 suc (x + y)
63 ≡⟨ sym ( +-sym {y} {suc x}) ⟩ 63 ≡⟨ sym ( +-sym {y} {suc x}) ⟩
64 y + suc x 64 y + suc x
65 ∎ ) 65 ∎ )
66
66 67
67 minus-plus : { x y : ℕ } → (suc x - 1) + (y + 1) ≡ suc x + y 68 minus-plus : { x y : ℕ } → (suc x - 1) + (y + 1) ≡ suc x + y
68 minus-plus {zero} {y} = +-sym {y} {1} 69 minus-plus {zero} {y} = +-sym {y} {1}
69 minus-plus {suc x} {y} = cong ( λ z → suc z ) (minus-plus {x} {y}) 70 minus-plus {suc x} {y} = cong ( λ z → suc z ) (minus-plus {x} {y})
70 71