let I be shiftable Program of ; :: thesis: for k1 being Integer st (card I) + k1 >= 0 holds
I ';' (goto k1) is shiftable
let k1 be Integer; :: thesis: ( (card I) + k1 >= 0 implies I ';' (goto k1) is shiftable )
set J = Load (goto k1);
set Ig = I ';' (goto k1);
assume A1: (card I) + k1 >= 0 ; :: thesis: I ';' (goto k1) is shiftable

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

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

per cases ( n in dom I or n in { (l + (card I)) where l is Nat : l in dom (Load (goto k1)) } ) by A2, A4, XBOOLE_0:def 3;

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

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

end;

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

then consider l being Nat such that
A6: n = l + (card I) and
A7: l in dom (Load (goto k1)) ;
dom (Load (goto k1)) = {0} by FUNCOP_1:13;
then A8: l = 0 by A7, TARSKI:def 1;
then A9: goto k1 = (Load (goto k1)) . l
.= i by A3, A6, A7, AFINSQ_1:def 3 ;
hence ( InsCode i <> 1 & InsCode i <> 3 ) ; :: thesis: i valid_at n
thus i valid_at n by A1, A6, A8, A9; :: thesis: verum

end;

end;

end;

hence I ';' (goto k1) is shiftable ; :: thesis: verum