let n be Nat; :: thesis: for i being Instruction of SCMPDS st n in dom (Load ((a,k1) <>0_goto n)) & i = (Load ((a,k1) <>0_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 ((a,k1) <>0_goto n)) & i = (Load ((a,k1) <>0_goto n)) . n implies ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) )
assume that
A1: n in dom (Load ((a,k1) <>0_goto n)) and
A2: i = (Load ((a,k1) <>0_goto n)) . n ; :: thesis: ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
dom (Load ((a,k1) <>0_goto n)) = {0} by FUNCOP_1:13;
then n = 0 by A1, TARSKI:def 1;
then A3: (a,k1) <>0_goto n = i by A2;
hence ( InsCode i <> 1 & InsCode i <> 3 ) ; :: thesis: i valid_at n
A4: ( n + n >= 0 & InsCode i <> 6 & InsCode i <> 14 ) by A3;
thus i valid_at n by A3, A4; :: thesis: verum