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