:: deftheorem Def9 defines shiftable SCMPDS_4:def 9 :
for IT being NAT -defined the InstructionsF of SCMPDS -valued finite Function holds
( IT is shiftable iff for n being Nat
for i being Instruction of SCMPDS st n in dom IT & i = IT . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) );