let a be Int_position ; :: thesis: for i being Integer
for I being Program of SCMPDS holds
( (while<>0 a,i,I) . 0 = a,i <>0_goto 2 & (while<>0 a,i,I) . 1 = goto ((card I) + 2) & (while<>0 a,i,I) . ((card I) + 2) = goto (- ((card I) + 2)) )
let i be Integer; :: thesis: for I being Program of SCMPDS holds
( (while<>0 a,i,I) . 0 = a,i <>0_goto 2 & (while<>0 a,i,I) . 1 = goto ((card I) + 2) & (while<>0 a,i,I) . ((card I) + 2) = goto (- ((card I) + 2)) )
let I be Program of SCMPDS ; :: thesis: ( (while<>0 a,i,I) . 0 = a,i <>0_goto 2 & (while<>0 a,i,I) . 1 = goto ((card I) + 2) & (while<>0 a,i,I) . ((card I) + 2) = goto (- ((card I) + 2)) )
set i1 = a,i <>0_goto 2;
set i2 = goto ((card I) + 2);
set i3 = goto (- ((card I) + 2));
set I4 = ((a,i <>0_goto 2) ';' (goto ((card I) + 2))) ';' I;
set WHL = while<>0 a,i,I;
A1: while<>0 a,i,I = ((a,i <>0_goto 2) ';' (goto ((card I) + 2))) ';' (I ';' (goto (- ((card I) + 2)))) by SCMPDS_4:47;
hence (while<>0 a,i,I) . 0 = a,i <>0_goto 2 by Th5; :: thesis: ( (while<>0 a,i,I) . 1 = goto ((card I) + 2) & (while<>0 a,i,I) . ((card I) + 2) = goto (- ((card I) + 2)) )
thus (while<>0 a,i,I) . 1 = goto ((card I) + 2) by A1, Th5; :: thesis: (while<>0 a,i,I) . ((card I) + 2) = goto (- ((card I) + 2))
card (((a,i <>0_goto 2) ';' (goto ((card I) + 2))) ';' I) = (card ((a,i <>0_goto 2) ';' (goto ((card I) + 2)))) + (card I) by SCMPDS_4:45
.= (card I) + 2 by SCMP_GCD:9 ;
hence (while<>0 a,i,I) . ((card I) + 2) = goto (- ((card I) + 2)) by SCMP_GCD:10; :: thesis: verum