let I, J be Program of ; :: thesis: I c= stop (I ';' J)
stop (I ';' J) = I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:27;
hence I c= stop (I ';' J) by AFINSQ_1:74; :: thesis: verum