[isabelle] Summing/subtracting functions
Is the summation (and/or subtraction) of functions already defined in the
f :: "nat => nat" and
g :: "nat => nat" where
ax1 : "ALL x. f x = 2" and
ax2 : "ALL x. g x = 1"
lemma "f - g = g"
using ax1 ax2
Presuming it's not, why not? It seems that there's only one definition for
summation/subtraction of functions anyway, i.e. "f - g <--> ALL x. f x - g
x" -- is it not?
This archive was generated by a fusion of
Pipermail (Mailman edition) and