let I be shiftable Program of ; 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; for a being Int_position st (card I) + k2 >= 0 holds
I ';' ((a,k1) <>0_goto k2) is shiftable
let a be Int_position; ( (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
; I ';' ((a,k1) <>0_goto k2) is shiftable
now 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;
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;
( 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
;
( 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
n in { (l + (card I)) where l is Nat : l in dom (Load ((a,k1) <>0_goto k2)) }
;
( 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 )
;
i valid_at nthus
i valid_at n
by A1, A6, A8, A9;
verum end; end; end;
hence
I ';' ((a,k1) <>0_goto k2) is shiftable
; verum