let n be Element of NAT ; :: thesis: for i being Instruction of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS holds Shift (stop I),1 c= Comput (ProgramPart ((Initialize s) +* (stop (i ';' I)))),((Initialize s) +* (stop (i ';' I))),n
let i be Instruction of SCMPDS ; :: thesis: for s being State of SCMPDS
for I being Program of SCMPDS holds Shift (stop I),1 c= Comput (ProgramPart ((Initialize s) +* (stop (i ';' I)))),((Initialize s) +* (stop (i ';' I))),n
let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS holds Shift (stop I),1 c= Comput (ProgramPart ((Initialize s) +* (stop (i ';' I)))),((Initialize s) +* (stop (i ';' I))),n
let I be Program of SCMPDS ; :: thesis: Shift (stop I),1 c= Comput (ProgramPart ((Initialize s) +* (stop (i ';' I)))),((Initialize s) +* (stop (i ';' I))),n
set pI = stop I;
set iI = i ';' I;
set piI = stop (i ';' I);
set s3 = (Initialize s) +* (stop (i ';' I));
( card (Load i) = 1 & i ';' I = (Load i) ';' I ) by SCMPDS_5:6;
then A1: Shift (stop I),1 c= stop (i ';' I) by Th24;
stop (i ';' I) c= (Initialize s) +* (stop (i ';' I)) by FUNCT_4:26;
then Shift (stop I),1 c= (Initialize s) +* (stop (i ';' I)) by A1, XBOOLE_1:1;
hence Shift (stop I),1 c= Comput (ProgramPart ((Initialize s) +* (stop (i ';' I)))),((Initialize s) +* (stop (i ';' I))),n by AMI_1:81; :: thesis: verum