set k2 = n;
set ii = (a,k1) >=0_goto n;
set J = Load ((a,k1) >=0_goto n);
now for n being Nat
for i being Instruction of SCMPDS st n in dom (Load ((a,k1) >=0_goto n)) & i = (Load ((a,k1) >=0_goto n)) . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )let n be
Nat;
for i being Instruction of SCMPDS st n in dom (Load ((a,k1) >=0_goto n)) & i = (Load ((a,k1) >=0_goto n)) . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )let i be
Instruction of
SCMPDS;
( n in dom (Load ((a,k1) >=0_goto n)) & i = (Load ((a,k1) >=0_goto n)) . n implies ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) )assume that A1:
n in dom (Load ((a,k1) >=0_goto n))
and A2:
i = (Load ((a,k1) >=0_goto n)) . n
;
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
dom (Load ((a,k1) >=0_goto n)) = {0}
by FUNCOP_1:13;
then
n = 0
by A1, TARSKI:def 1;
then A3:
(
a,
k1)
>=0_goto n = i
by A2;
hence
(
InsCode i <> 1 &
InsCode i <> 3 )
;
i valid_at nA4:
(
n + n >= 0 &
InsCode i <> 5 &
InsCode i <> 14 )
by A3;
thus
i valid_at n
by A3, A4;
verum end;
hence
for b1 being Program of st b1 = Load ((a,k1) >=0_goto n) holds
b1 is shiftable
; verum