[isabelle] yet another simplifier question
I'm interested in what exactly happens in the following proof -
lemma "sin((x::real) + y + x) = sin(2*x + y)"
the proof succeeds, and because of the sin() I guess it can't be due to
so I guess there is a true rewriting process here, but I failed to
from the output what exactly happens and how the following expression
in the process -
(Numeral1 / Numeral1 + Numeral1 / Numeral1) * (x / 1) + y = 2 /
Numeral1 * (x / 1) + (y + 0)
where did all the numerals come from? I expect a rewriting process to
like Numerla1, not add them.
This archive was generated by a fusion of
Pipermail (Mailman edition) and