let I be Program of SCM+FSA ; :: thesis: for a, b being Int-Location st not I destroysdestroy b holds
not while>0 a,I destroysdestroy b
let a, b be Int-Location ; :: thesis: ( not I destroysdestroy b implies not while>0 a,I destroysdestroy 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 destroysdestroy b by SCMFSA8C:86;
A2: not Stop SCM+FSA destroysdestroy b by SCMFSA8C:85;
assume not I destroysdestroy b ; :: thesis: not while>0 a,I destroysdestroy b
then not I ';' (Goto 0 ) destroysdestroy b by A1, SCMFSA8C:81;
then A3: not if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA ) destroysdestroy b by A2, SCMFSA8C:121;
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 ) destroysdestroy b by SCMFSA_9:35;
hence not while>0 a,I destroysdestroy b by A3, A4, SCMFSA8A:25; :: thesis: verum