let N be with_zero set ; 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 ; 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); ( InsCode i = 1 implies NIC (i,l) = {(NextLoc (l,(STC N)))} )
assume A1:
InsCode i = 1
; 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; verum