let I be Program of ; :: thesis: for k being Nat holds stop (I ';' (Goto k)) = I ';' (Macro (goto k))
let k be Nat; :: thesis: stop (I ';' (Goto k)) = I ';' (Macro (goto k))
A1: IncAddr ((Macro (goto k)),((card I) -' 1)) = (IncAddr ((Goto k),((card I) -' 1))) ^ (Stop SCM+FSA) by COMPOS_1:76;
thus stop (I ';' (Goto k)) = ((CutLastLoc I) ^ (IncAddr ((Goto k),((card I) -' 1)))) ^ (Stop SCM+FSA) by COMPOS_1:75
.= (CutLastLoc I) ^ (IncAddr ((Macro (goto k)),((card I) -' 1))) by A1, AFINSQ_1:27
.= I ';' (Macro (goto k)) by COMPOS_1:75 ; :: thesis: verum