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 )
assume A1: I does_not_destroy b ; :: thesis: while>0 a,I does_not_destroy b
set J = (insloc ((card I) + 4)) .--> (goto (insloc 0 ));
set Gi = Goto (insloc 0 );
set SS = Stop SCM+FSA ;
set F = if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA );
A2: (insloc ((card I) + 4)) .--> (goto (insloc 0 )) does_not_destroy b by SCMFSA_9:35;
Goto (insloc 0 ) does_not_destroy b by SCMFSA8C:86;
then A3: I ';' (Goto (insloc 0 )) does_not_destroy b by A1, SCMFSA8C:81;
Stop SCM+FSA does_not_destroy b by SCMFSA8C:85;
then A4: if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ) does_not_destroy b by A3, SCMFSA8C:121;
while>0 a,I = (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) by SCMFSA_9:def 2;
hence while>0 a,I does_not_destroy b by A2, A4, SCMFSA8A:25; :: thesis: verum