set m = Load (halt SCMPDS);
A1: dom (Load (halt SCMPDS)) = {0} by FUNCOP_1:13;
let n be Nat; :: according to SCMPDS_4:def 9 :: thesis: for i being Instruction of SCMPDS st n in dom (Load (halt SCMPDS)) & i = (Load (halt SCMPDS)) . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
let i be Instruction of SCMPDS; :: thesis: ( n in dom (Load (halt SCMPDS)) & i = (Load (halt SCMPDS)) . n implies ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) )
assume that
A2: n in dom (Load (halt SCMPDS)) and
A3: i = (Load (halt SCMPDS)) . n ; :: thesis: ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
A4: n = 0 by A1, A2, TARSKI:def 1;
i = [0,{},{}] by A3, A4, SCMPDS_2:80;
then InsCode i = 0 ;
hence ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) ; :: thesis: verum