2018-03-18 00:15:05 UTC
exists an m such that n equals 2*m. Or rather, a proof and a non-proof.
The equation I need to prove is
suc (suc (m + (m + 0))) â¡ suc (m + suc (m + 0)) (*)
If I use
sym (+-suc m (m + 0)) : suc (m + (m + 0)) â¡ m + suc (m + 0)
to rewrite then it works perfectly, rewriting the lhs of (*). But if I
remove the sym then it fails to work, even though it should rewrite the rhs
of (*). What am I doing wrong?
Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK