set m = Load (halt SCMPDS);
A1: (Load (halt SCMPDS)) . 0 = halt SCMPDS by FUNCOP_1:87;
A2: dom (Load (halt SCMPDS)) = {0} by FUNCOP_1:19;

now

let n be Element of NAT ; :: 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
A3: n in dom (Load (halt SCMPDS)) and
A4: i = (Load (halt SCMPDS)) . n ; :: thesis: ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
A5: n = 0 by A2, A3, TARSKI:def 1;
hence InsCode i <> 1 by A1, A4, SCMPDS_2:21, SCMPDS_2:93; :: thesis: ( InsCode i <> 3 & i valid_at n )
A6: ex k1 being Integer st
( i = goto k1 & n + k1 >= 0 )

proof

take 0 ; :: thesis: ( i = goto 0 & n + 0 >= 0 )
thus i = goto 0 by A4, A5, FUNCOP_1:87, SCMPDS_2:93; :: thesis: n + 0 >= 0
thus n + 0 >= 0 ; :: thesis: verum

end;

thus InsCode i <> 3 by A1, A4, A5, SCMPDS_2:21, SCMPDS_2:93; :: thesis: i valid_at n
InsCode i = 0 by A1, A4, A5, SCMPDS_2:21, SCMPDS_2:93;
hence i valid_at n by A6, Def11; :: thesis: verum

end;

hence Load (halt SCMPDS) is shiftable by Def12; :: thesis: verum