let I be Program of ; :: 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 = (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 );
A1: Goto (insloc 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 (insloc 0 )) does_not_destroy b by A1, SCMFSA8C:81;
then A3: if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ) does_not_destroy b by A2, SCMFSA8C:121;
A4: 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;
(insloc ((card I) + 4)) .--> (goto (insloc 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