let p be Program of ; :: thesis: ( p = Load i implies p is shiftable )
assume A1: p = Load i ; :: thesis: p is shiftable
let n be Nat; :: according to SCMPDS_4:def 9 :: thesis: for i being Instruction of SCMPDS st n in dom p & i = p . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
let j be Instruction of SCMPDS; :: thesis: ( n in dom p & j = p . n implies ( InsCode j <> 1 & InsCode j <> 3 & j valid_at n ) )
assume that
A2: n in dom p and
A3: j = p . n ; :: thesis: ( InsCode j <> 1 & InsCode j <> 3 & j valid_at n )
dom p = {0} by A1, FUNCOP_1:13;
then n = 0 by A2, TARSKI:def 1;
then A4: j = i by A3, A1;
hence InsCode j <> 1 by Def10; :: thesis: ( InsCode j <> 3 & j valid_at n )
thus InsCode j <> 3 by A4, Def10; :: thesis: j valid_at n
( InsCode j <> 4 & InsCode j <> 5 & InsCode j <> 6 & InsCode j <> 14 ) by A4, Def10;
hence j valid_at n ; :: thesis: verum