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

now

let n be Element of NAT ; :: thesis: for i being Instruction of SCMPDS st inspos n in dom (Load (halt SCMPDS )) & i = (Load (halt SCMPDS )) . (inspos n) holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
let i be Instruction of SCMPDS ; :: thesis: ( inspos n in dom (Load (halt SCMPDS )) & i = (Load (halt SCMPDS )) . (inspos n) implies ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) )
assume A3: ( inspos n in dom (Load (halt SCMPDS )) & i = (Load (halt SCMPDS )) . (inspos n) ) ; :: thesis: ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
then A4: inspos n = inspos 0 by A2, TARSKI:def 1;
then A5: InsCode i = 0 by A1, A3, SCMPDS_2:21, SCMPDS_2:93;
thus InsCode i <> 1 by A1, A3, A4, SCMPDS_2:21, SCMPDS_2:93; :: thesis: ( InsCode i <> 3 & i valid_at n )
thus InsCode i <> 3 by A1, A3, A4, SCMPDS_2:21, SCMPDS_2:93; :: thesis: i valid_at n
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 A3, A4, FUNCOP_1:87, SCMPDS_2:93; :: thesis: n + 0 >= 0
thus n + 0 >= 0 ; :: thesis: verum

end;

hence i valid_at n by A5, Def11; :: thesis: verum

end;

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