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