let N be with_non-empty_elements set ; :: thesis: for l being Instruction-Location of STC N
for i being Element of the Instructions of (STC N) st InsCode i = 1 holds
NIC i,l = {(NextLoc l)}
let l be Instruction-Location of STC N; :: thesis: for i being Element of the Instructions of (STC N) st InsCode i = 1 holds
NIC i,l = {(NextLoc l)}
let i be Element of the Instructions of (STC N); :: thesis: ( InsCode i = 1 implies NIC i,l = {(NextLoc l)} )
assume A1: InsCode i = 1 ; :: thesis: NIC i,l = {(NextLoc l)}
set M = STC N;
consider k being natural number such that
A2: l = il. (STC N),k by Th26;
k = locnum l by A2, Def13;
then NextLoc l = k + 1 by Th37;
hence NIC i,l = {(NextLoc l)} by A1, A2, Lm5, Th37; :: thesis: verum