set p = Load i;

now

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

end;

hence Load i is shiftable by Def12; :: thesis: verum