set IJ = I ';' J;

now :: thesis: for n being Nat
for i being Instruction of SCMPDS st n in dom (I ';' J) & i = (I ';' J) . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )

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

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

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

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

end;

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

then consider l being Nat such that
A5: n = l + (card I) and
A6: l in dom J ;
A7: J . l = i by A2, A5, A6, AFINSQ_1:def 3;
hence ( InsCode i <> 1 & InsCode i <> 3 ) by A6, Def9; :: thesis: i valid_at n
i valid_at l by A6, A7, Def9;
hence i valid_at n by A5, Th20, NAT_1:11; :: thesis: verum

end;

end;

end;

hence for b₁ being Program of st b₁ = I ';' J holds
b₁ is shiftable ; :: thesis: verum