Program Verification - Translation rule

[craigs]

Hi

I am doing a course on Program verification and am having trouble with the properties of summation, more specifically the rule of translation:

"Suppose function f maps values of type J to values of type K, and suppose g is a function that maps values of type K to values of type J. suppose further that f and g are inverses. That is, suppose that, for all j$\in$J and k$\in$K, (f.j=k) $\equiv$ (j=g.k)

$\left\langle$ $\Sigma$k$\in$K:R:T$\right\rangle$ = $\left\langle$ $\Sigma$j$\in$J:R[k:=f.j]:T[k:=f.j]$\right\rangle$

My question: I actually do not understand how the LHS of the equation equals the RHS.
Perhaps more specifically I am not sure how R[k:=f.j] and T[k:=f.j] appears on the right side, where does it come from?

 

[Mark44]

Hi

I am doing a course on Program verification and am having trouble with the properties of summation, more specifically the rule of translation:

"Suppose function f maps values of type J to values of type K, and suppose g is a function that maps values of type K to values of type J. suppose further that f and g are inverses. That is, suppose that, for all j$\in$J and k$\in$K, (f.j=k) $\equiv$ (j=g.k)

$\left\langle$ $\Sigma$k$\in$K:R:T$\right\rangle$ = $\left\langle$ $\Sigma$j$\in$J:R[k:=f.j]:T[k:=f.j]$\right\rangle$

My question: I actually do not understand how the LHS of the equation equals the RHS.
Perhaps more specifically I am not sure how R[k:=f.j] and T[k:=f.j] appears on the right side, where does it come from?

Please fix your LaTeX so that it is readable. I can't tell what you're trying to say, so I can't fix it.

 

[craigs]

Sorry. Here is my next attempt:

"Suppose function f maps values of type J to values of type K, and suppose g is a function that maps values of type K to values of type J. suppose further that f and g are inverses. That is, suppose that, for all j$\in$J and k$\in$K, (f.j=k) $\equiv$ (j=g.k)

$\langle$ $\Sigma$k$\in$K:R:T$\rangle$ = $\langle$ $\Sigma$j$\in$J:R[k:=f.j]:T[k:=f.j]$\rangle$

My question: I actually do not understand how the LHS of the equation equals the RHS.
Perhaps more specifically I am not sure how R[k:=f.j] and T[k:=f.j] appears on the right side, where does it come from?