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