let i be Instruction of SCMPDS; :: thesis: for I being Program of
for P being Instruction-Sequence of SCMPDS holds Shift ((stop I),1) c= P +* (stop (i ';' I))
let I be Program of ; :: thesis: for P being Instruction-Sequence of SCMPDS holds Shift ((stop I),1) c= P +* (stop (i ';' I))
let P be Instruction-Sequence of SCMPDS; :: thesis: Shift ((stop I),1) c= P +* (stop (i ';' I))
set pI = stop I;
set iI = i ';' I;
set piI = stop (i ';' I);
set P3 = P +* (stop (i ';' I));
( card (Load i) = 1 & i ';' I = (Load i) ';' I ) by COMPOS_1:54;
then A1: Shift ((stop I),1) c= stop (i ';' I) by Th5;
stop (i ';' I) c= P +* (stop (i ';' I)) by FUNCT_4:25;
then Shift ((stop I),1) c= P +* (stop (i ';' I)) by A1, XBOOLE_1:1;
hence Shift ((stop I),1) c= P +* (stop (i ';' I)) ; :: thesis: verum