Spent several hours working on this problem:
Apply the indicated change of variable, if possible.
$\langle\sum{i}:|i|<5: i\mathbf{div} 2\rangle$ with $i \mapsto 2*i$ (that is, f.i = 2*i)
In A Logical Approach to Discrete Math by David Gries, Change of dummy theorem is defined:
My interpretation of the theorem is as follows. Function f, in this case, $f(i) = 2*i$, has an inverse in the range of specification (I need to compose R with f, to get $R(f) = |2*i*| < 5$). This is the set **{-2,-1,0,1,2}**.
When I map f with this set as a domain, I get {-4,-2,0,2,4}. Hence, f is a bijective function. And I think it is possible to change that dummy variable with proposed function.
Is this reasoning correct? Is the theorem saying that f needs to be a bijective function with $R(f)$ as its domain?
Any help would be appreciated.
P.D: By the way, what does it mean x = f.y, before theorem definition?