let i be Instruction of SCMPDS ; :: thesis: ( 0 in dom (Initialized (stop (Load i))) & 1 in dom (Initialized (stop (Load i))) & (Initialized (stop (Load i))) . 0 = i & (Initialized (stop (Load i))) . 1 = halt SCMPDS )
set si = stop (Load i);
set Ii = Initialized (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= Initialized (stop (Load i)) by SCMPDS_4:9;
then dom (stop (Load i)) c= dom (Initialized (stop (Load i))) by RELAT_1:25;
hence ( 0 in dom (Initialized (stop (Load i))) & 1 in dom (Initialized (stop (Load i))) ) by A1, A2; :: thesis: ( (Initialized (stop (Load i))) . 0 = i & (Initialized (stop (Load i))) . 1 = halt SCMPDS )
thus (Initialized (stop (Load i))) . 0 = (stop (Load i)) . 0 by A1, SCMPDS_4:33
.= i by Th10 ; :: thesis: (Initialized (stop (Load i))) . 1 = halt SCMPDS
thus (Initialized (stop (Load i))) . 1 = (stop (Load i)) . 1 by A2, SCMPDS_4:33
.= halt SCMPDS by Th10 ; :: thesis: verum