let N be with_zero set ; :: thesis: for l being Element of NAT
for i being Element of the InstructionsF of (STC N) st InsCode i = 1 holds
NIC (i,l) = {(NextLoc (l,(STC N)))}
let l be Element of NAT ; :: thesis: for i being Element of the InstructionsF of (STC N) st InsCode i = 1 holds
NIC (i,l) = {(NextLoc (l,(STC N)))}
let i be Element of the InstructionsF of (STC N); :: thesis: ( InsCode i = 1 implies NIC (i,l) = {(NextLoc (l,(STC N)))} )
assume A1: InsCode i = 1 ; :: thesis: NIC (i,l) = {(NextLoc (l,(STC N)))}
set M = STC N;
consider k being Nat such that
A2: l = il. ((STC N),k) by Th6;
k = locnum (l,(STC N)) by A2, Def5;
then NextLoc (l,(STC N)) = k + 1 by Th17;
hence NIC (i,l) = {(NextLoc (l,(STC N)))} by A1, A2, Lm3, Th17; :: thesis: verum