let i be Instruction of SCMPDS ; :: thesis: ( 0 in dom (Initialize (stop (Load i))) & 1 in dom (Initialize (stop (Load i))) & (Initialize (stop (Load i))) . 0 = i & (Initialize (stop (Load i))) . 1 = halt SCMPDS )
set si = stop (Load i);
set Ii = Initialize (stop (Load i));
A1: 0 in dom (stop (Load i)) by Th9;
A2: 1 in dom (stop (Load i)) by Th9;
stop (Load i) c= Initialize (stop (Load i)) by SCMPDS_4:9;
then dom (stop (Load i)) c= dom (Initialize (stop (Load i))) by RELAT_1:25;
hence ( 0 in dom (Initialize (stop (Load i))) & 1 in dom (Initialize (stop (Load i))) ) by A1, A2; :: thesis: ( (Initialize (stop (Load i))) . 0 = i & (Initialize (stop (Load i))) . 1 = halt SCMPDS )
thus (Initialize (stop (Load i))) . 0 = (stop (Load i)) . 0 by A1, SCMPDS_4:33
.= i by Th10 ; :: thesis: (Initialize (stop (Load i))) . 1 = halt SCMPDS
thus (Initialize (stop (Load i))) . 1 = (stop (Load i)) . 1 by A2, SCMPDS_4:33
.= halt SCMPDS by Th10 ; :: thesis: verum