I am trying to prove one algorithm refines another algorithm. Let's call them Implementation and Specification.
For example, the Specification has one subaction that :
subaction1(a) == /\ F1(a)
/\ F2(a')
While in the Implementation, it will batch several of this step in one subaction, which is like:
subaction2(A) ==
\A a \in A :
/\ F1(a) /\ F2(a')
(A is a set consisting of element a, and each element doesn't interfere with other elements in A)
Then how can I represent it with the format of refinement mapping, for example using auxiliary variables? Or is it not a refinement mapping cause they don't have same behaviors?