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

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