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[itex]\in[/itex]J and k[itex]\in[/itex]K, (f.j=k) [itex]\equiv[/itex] (j=g.k)

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

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[itex]\in[/itex]J and k[itex]\in[/itex]K, (f.j=k) [itex]\equiv[/itex] (j=g.k)

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

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[itex]\in[/itex]J and k[itex]\in[/itex]K, (f.j=k) [itex]\equiv[/itex] (j=g.k)

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

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?