let b be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA holds UsedI*Loc (while=0 (b,I)) = UsedI*Loc I
let I be MacroInstruction of SCM+FSA ; :: thesis: UsedI*Loc (while=0 (b,I)) = UsedI*Loc I
set J = Stop SCM+FSA;
set a = b;
set IG = I ';' (goto 0);
A1: UsedI*Loc (I ';' (goto 0)) = UsedI*Loc I by SF_MASTR:67;
thus UsedI*Loc (while=0 (b,I)) = UsedI*Loc (if=0 (b,(I ';' (goto 0)))) by Lm4
.= (UsedI*Loc (((b =0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" (I ';' (goto 0)))) \/ {} by Th4, SF_MASTR:43
.= (UsedI*Loc ((b =0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1)))) \/ (UsedI*Loc I) by A1, SF_MASTR:43
.= ((UsedInt*Loc (b =0_goto 3)) \/ (UsedI*Loc (Goto ((card (I ';' (goto 0))) + 1)))) \/ (UsedI*Loc I) by SF_MASTR:45
.= ((UsedInt*Loc (b =0_goto 3)) \/ {}) \/ (UsedI*Loc I) by Th6
.= {} \/ (UsedI*Loc I) by SF_MASTR:32
.= UsedI*Loc I ; :: thesis: verum