set k1 = n;

set J = Load (goto n);

_{1} being Program of st b_{1} = Load (goto n) holds

b_{1} is shiftable
; :: thesis: verum

set J = Load (goto n);

now :: thesis: for n being Nat

for i being Instruction of SCMPDS st n in dom (Load (goto n)) & i = (Load (goto n)) . n holds

( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )

hence
for bfor i being Instruction of SCMPDS st n in dom (Load (goto n)) & i = (Load (goto n)) . n holds

( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )

let n be Nat; :: thesis: for i being Instruction of SCMPDS st n in dom (Load (goto n)) & i = (Load (goto n)) . n holds

( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )

let i be Instruction of SCMPDS; :: thesis: ( n in dom (Load (goto n)) & i = (Load (goto n)) . n implies ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) )

assume that

A1: n in dom (Load (goto n)) and

A2: i = (Load (goto n)) . n ; :: thesis: ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )

dom (Load (goto n)) = {0} by FUNCOP_1:13;

then n = 0 by A1, TARSKI:def 1;

then A3: goto n = i by A2;

hence ( InsCode i <> 1 & InsCode i <> 3 ) ; :: thesis: i valid_at n

A4: ( n + n >= 0 & InsCode i <> 6 ) by A3;

thus i valid_at n by A3, A4; :: thesis: verum

end;( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )

let i be Instruction of SCMPDS; :: thesis: ( n in dom (Load (goto n)) & i = (Load (goto n)) . n implies ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) )

assume that

A1: n in dom (Load (goto n)) and

A2: i = (Load (goto n)) . n ; :: thesis: ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )

dom (Load (goto n)) = {0} by FUNCOP_1:13;

then n = 0 by A1, TARSKI:def 1;

then A3: goto n = i by A2;

hence ( InsCode i <> 1 & InsCode i <> 3 ) ; :: thesis: i valid_at n

A4: ( n + n >= 0 & InsCode i <> 6 ) by A3;

thus i valid_at n by A3, A4; :: thesis: verum

b