set IJ = I ';' J;

now

let n be Element of NAT ; :: thesis: for i being Instruction of SCMPDS st inspos n in dom (I ';' J) & i = (I ';' J) . (inspos n) holds
( InsCode b₃ <> 1 & InsCode b₃ <> 3 & b₃ valid_at b₂ )
let i be Instruction of SCMPDS ; :: thesis: ( inspos n in dom (I ';' J) & i = (I ';' J) . (inspos n) implies ( InsCode b₂ <> 1 & InsCode b₂ <> 3 & b₂ valid_at b₁ ) )
assume that
A1: inspos n in dom (I ';' J) and
A2: i = (I ';' J) . (inspos n) ; :: thesis: ( InsCode b₂ <> 1 & InsCode b₂ <> 3 & b₂ valid_at b₁ )
set D = { (l + (card I)) where l is Element of NAT : l in dom J } ;
dom (Shift J,(card I)) = { (l + (card I)) where l is Element of NAT : l in dom J } by VALUED_1:def 12;
then A3: dom (I ';' J) = (dom I) \/ { (l + (card I)) where l is Element of NAT : l in dom J } by FUNCT_4:def 1;

per cases ( inspos n in dom I or inspos n in { (l + (card I)) where l is Element of NAT : l in dom J } ) by A1, A3, XBOOLE_0:def 3;

suppose A4: inspos n in dom I ; :: thesis: ( InsCode b₂ <> 1 & InsCode b₂ <> 3 & b₂ valid_at b₁ )

then I . (inspos n) = i by A2, Th37;
hence ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) by A4, Def12; :: thesis: verum

end;

suppose inspos n in { (l + (card I)) where l is Element of NAT : l in dom J } ; :: thesis: ( InsCode b₂ <> 1 & InsCode b₂ <> 3 & b₂ valid_at b₁ )

then consider l being Element of NAT such that
A5: n = l + (card I) and
A6: l in dom J ;
A7: J . (inspos l) = i by A2, A5, A6, Th38;
hence ( InsCode i <> 1 & InsCode i <> 3 ) by A6, Def12; :: thesis: i valid_at n
i valid_at l by A6, A7, Def12;
hence i valid_at n by A5, Th77, NAT_1:11; :: thesis: verum

end;

end;

end;

hence I ';' J is shiftable by Def12; :: thesis: verum