theorem :: SCMFSA_X:10

for a being Int-Location
for I being MacroInstruction of SCM+FSA holds
( (while=0 (a,I)) . 0 = a =0_goto 3 & (while=0 (a,I)) . 1 = goto 2 & (while>0 (a,I)) . 0 = a >0_goto 3 & (while>0 (a,I)) . 1 = goto 2 )