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 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 ; :: 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 that
A3: inspos n in dom (Load (halt SCMPDS )) and
A4: i = (Load (halt SCMPDS )) . (inspos n) ; :: thesis: ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
A5: inspos n = inspos 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