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

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 )

hence
I ';' (goto k1) is shiftable
; :: thesis: verumfor 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_{3} <> 1 & InsCode b_{3} <> 3 & b_{3} valid_at b_{2} )

let i be Instruction of SCMPDS; :: thesis: ( n in dom (I ';' (goto k1)) & i = (I ';' (goto k1)) . n implies ( InsCode b_{2} <> 1 & InsCode b_{2} <> 3 & b_{2} valid_at b_{1} ) )

assume that

A2: n in dom (I ';' (goto k1)) and

A3: i = (I ';' (goto k1)) . n ; :: thesis: ( InsCode b_{2} <> 1 & InsCode b_{2} <> 3 & b_{2} valid_at b_{1} )

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;

end;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

let i be Instruction of SCMPDS; :: thesis: ( n in dom (I ';' (goto k1)) & i = (I ';' (goto k1)) . n implies ( InsCode b

assume that

A2: n in dom (I ';' (goto k1)) and

A3: i = (I ';' (goto k1)) . n ; :: thesis: ( InsCode 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;

end;

suppose A5:
n in dom I
; :: thesis: ( InsCode b_{2} <> 1 & InsCode b_{2} <> 3 & b_{2} valid_at b_{1} )

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;hence ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) by A5, Def9; :: thesis: verum

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

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;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