let I, J be Program of SCMPDS ; :: thesis: Shift (stop J),(card I) c= stop (I ';' J)
stop (I ';' J) = (I ';' J) ';' (Stop SCMPDS )
.= I ';' (J ';' (Stop SCMPDS )) by SCMPDS_4:46
.= I ';' (stop J) ;
then stop (I ';' J) = I +* (Shift (stop J),(card I)) ;
hence Shift (stop J),(card I) c= stop (I ';' J) by FUNCT_4:26; :: thesis: verum