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