let I be shiftable Program of ; :: 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 :: thesis: for n being Nat
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 i <> 1 & InsCode i <> 3 & i valid_at n )
set D = { (l + (card I)) where l is Nat : l in dom (Load ((a,k1) >=0_goto k2)) } ;
let n be 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 b3 <> 1 & InsCode b3 <> 3 & b3 valid_at b2 )
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 b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 ) )
assume that
A2: n in dom (I ';' ((a,k1) >=0_goto k2)) and
A3: i = (I ';' ((a,k1) >=0_goto k2)) . n ; :: thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
dom (Shift ((Load ((a,k1) >=0_goto k2)),(card I))) = { (l + (card I)) where l is 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 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 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 b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
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 ((a,k1) >=0_goto k2)) } ; :: thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
then consider l being 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:13;
then A8: l = 0 by A7, TARSKI:def 1;
then A9: (a,k1) >=0_goto k2 = (Load ((a,k1) >=0_goto k2)) . 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 ';' ((a,k1) >=0_goto k2) is shiftable ; :: thesis: verum