let I be shiftable Program of SCMPDS ; :: thesis: for k1, k2 being Integer
for a being Int_position st (card I) + k2 >= 0 holds
I ';' (a,k1 <=0_goto k2) is shiftable
let k1, k2 be Integer; :: thesis: for a being Int_position st (card I) + k2 >= 0 holds
I ';' (a,k1 <=0_goto k2) is shiftable
let a be Int_position ; :: thesis: ( (card I) + k2 >= 0 implies I ';' (a,k1 <=0_goto k2) is shiftable )
set ii = a,k1 <=0_goto k2;
set J = Load (a,k1 <=0_goto k2);
set Ig = I ';' (a,k1 <=0_goto k2);
assume A1: (card I) + k2 >= 0 ; :: thesis: I ';' (a,k1 <=0_goto k2) is shiftable

now

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

per cases ( n in dom I or n in { (l + (card I)) where l is Element of NAT : l in dom (Load (a,k1 <=0_goto k2)) } ) 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, Th37;
hence ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) by A5, Def12; :: thesis: verum

end;

suppose n in { (l + (card I)) where l is Element of NAT : l in dom (Load (a,k1 <=0_goto k2)) } ; :: thesis: ( InsCode b₂ <> 1 & InsCode b₂ <> 3 & b₂ valid_at b₁ )

then consider l being Element of NAT such that
A6: n = l + (card I) and
A7: l in dom (Load (a,k1 <=0_goto k2)) ;
dom (Load (a,k1 <=0_goto k2)) = {0 } by FUNCOP_1:19;
then A8: l = 0 by A7, TARSKI:def 1;
then A9: a,k1 <=0_goto k2 = (Load (a,k1 <=0_goto k2)) . l by FUNCOP_1:87
.= i by A3, A6, A7, Th38 ;
hence ( InsCode i <> 1 & InsCode i <> 3 ) by SCMPDS_2:26; :: thesis: i valid_at n
A10: InsCode i <> 6 by A9, SCMPDS_2:26;
( InsCode i <> 0 & InsCode i <> 4 ) by A9, SCMPDS_2:26;
hence i valid_at n by A1, A6, A8, A9, A10, Def11; :: thesis: verum

end;

end;

end;

hence I ';' (a,k1 <=0_goto k2) is shiftable by Def12; :: thesis: verum