let i be Instruction of SCMPDS ; :: thesis: ( (stop (Load i)) . (inspos 0 ) = i & (stop (Load i)) . (inspos 1) = halt SCMPDS )
set II = Load i;
inspos 0 in dom (Load i) by Th5;
hence (stop (Load i)) . (inspos 0 ) = (Load i) . (inspos 0 ) by SCMPDS_4:37
.= i by FUNCOP_1:87 ;
:: thesis: (stop (Load i)) . (inspos 1) = halt SCMPDS
inspos 1 = (inspos 0 ) + (card (Load i)) by Th6;
hence (stop (Load i)) . (inspos 1) = halt SCMPDS by SCMPDS_4:38, SCMPDS_4:73; :: thesis: verum