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