Go backward to Recursively Defined Abstractions Go up to Top

Example

(alias A=loc₁, alias B=loc₂);
proc ADD = (rec ADD: comm.
if @A=0 then skip else
B:=@B+1; A:=@A-1; call ADD fi)
in A:=2; B:=3; call ADD

=> alias A=loc₁, alias B=loc₂,
proc ADD = (rec ADD: comm.
if @loc₁=0 then skip else
loc₂:=@loc₂+1; loc₁:=@loc₁-1; call ADD fi)
in A:=2; B:=3; call ADD

=> loc₁:=2; loc₂:=3;
(rec ADD: comm.
if @loc₁=0 then skip else
loc₂:=@loc₂+1; loc₁:=@loc₁-1; call ADD fi)

=> loc₁:=2; loc₂:=3;
if @loc₁=0 then skip else
loc₂:=@loc₂+1; loc₁:=@loc₁-1; (rec ADD: ...fi) fi)