set p = Load i;

now

let n be Element of NAT ; :: thesis: for j being Instruction of SCMPDS st n in dom (Load i) & j = (Load i) . n holds
( InsCode j <> 1 & InsCode j <> 3 & j valid_at n )
let j be Instruction of SCMPDS ; :: thesis: ( n in dom (Load i) & j = (Load i) . n implies ( InsCode j <> 1 & InsCode j <> 3 & j valid_at n ) )
assume that
A1: n in dom (Load i) and
A2: j = (Load i) . n ; :: thesis: ( InsCode j <> 1 & InsCode j <> 3 & j valid_at n )
dom (Load i) = {0 } by FUNCOP_1:19;
then n = 0 by A1, TARSKI:def 1;
then A3: j = i by A2, FUNCOP_1:87;
hence InsCode j <> 1 by Def13; :: thesis: ( InsCode j <> 3 & j valid_at n )
thus InsCode j <> 3 by A3, Def13; :: thesis: j valid_at n
A4: ( InsCode j <> 4 & InsCode j <> 5 ) by A3, Def13;
( InsCode j = 2 or InsCode j > 6 ) by A3, Def13;
hence j valid_at n by A4, Def11; :: thesis: verum

end;

hence for b₁ being Program of SCMPDS st b₁ = Load i holds
b₁ is shiftable by Def12; :: thesis: verum