let I be Program of SCMPDS ; :: thesis: ( card I in dom (stop I) & (stop I) . (card I) = halt SCMPDS )
set SS = Stop SCMPDS ;
set pI = stop I;
card (stop I) = (card I) + 1 by SCMPDS_5:7;
then card I < card (stop I) by XREAL_1:31;
hence card I in dom (stop I) by AFINSQ_1:70; :: thesis: (stop I) . (card I) = halt SCMPDS
(stop I) . (0 + (card I)) = halt SCMPDS by JJ, KK, SCMPDS_4:38;
hence (stop I) . (card I) = halt SCMPDS ; :: thesis: verum