set m = Load (halt SCMPDS);
A1: dom (Load (halt SCMPDS)) = {0} by FUNCOP_1:13;
let n be Element of 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 = halt SCMPDS by A3, A4, AFINSQ_1:34;
then i = [0,{},{}] by SCMPDS_2:80;
then A5: InsCode i = 0 by RECDEF_2:def 1;
hence ( InsCode i <> 1 & InsCode i <> 3 ) ; :: thesis: i valid_at n
( InsCode i <> 4 & InsCode i <> 5 & InsCode i <> 6 & InsCode i <> 14 ) by A5;
hence i valid_at n by Def8; :: thesis: verum