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, Lm5, Th37; :: thesis: verum