let N be non empty with_non-empty_elements set ; :: thesis: for l being Element of NAT
for i being Element of the Instructions 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 Instructions of (STC N) st InsCode i = 1 holds
NIC (i,l) = {(NextLoc (l,(STC N)))}
let i be Element of the Instructions 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 natural number such that
A2: l = il. ((STC N),k) by Th26;
k = locnum (l,(STC N)) by A2, Def13;
then NextLoc (l,(STC N)) = k + 1 by Th37;
hence NIC (i,l) = {(NextLoc (l,(STC N)))} by A1, A2, Lm3, Th37; :: thesis: verum