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\inJ and k\inK, (f.j=k) \equiv (j=g.k)

\left\langle \Sigmak\inK:R:T\right\rangle = \left\langle \Sigmaj\inJ: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\inJ and k\inK, (f.j=k) \equiv (j=g.k)

\left\langle \Sigmak\inK:R:T\right\rangle = \left\langle \Sigmaj\inJ: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\inJ and k\inK, (f.j=k) \equiv (j=g.k)

\langle \Sigmak\inK:R:T\rangle = \langle \Sigmaj\inJ: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?