let I be Program of SCM+FSA; :: thesis: for a, b being Int-Location st not I destroys b holds
not while>0 (a,I) destroys b
let a, b be Int-Location ; :: thesis: ( not I destroys b implies not while>0 (a,I) destroys b )
set J = ((card I) + 4) .--> (goto 0);
set Gi = Goto 0;
set SS = Stop SCM+FSA;
set F = if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA));
A1: not Goto 0 destroys b by SCMFSA8C:57;
A2: not Stop SCM+FSA destroys b by SCMFSA8C:56;
assume not I destroys b ; :: thesis: not while>0 (a,I) destroys b
then not I ';' (Goto 0) destroys b by A1, SCMFSA8C:52;
then A3: not if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA)) destroys b by A2, SCMFSA8C:88;
A4: while>0 (a,I) = (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0)) by SCMFSA_9:def 2;
not ((card I) + 4) .--> (goto 0) destroys b by SCMFSA_9:30;
hence not while>0 (a,I) destroys b by A3, A4, SCMFSA8A:11; :: thesis: verum