let N be with_zero set ; :: thesis: for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
IC (Exec (i,s)) = NextLoc ((IC s),(STC N))
let i be Instruction of (STC N); :: thesis: for s being State of (STC N) st InsCode i = 1 holds
IC (Exec (i,s)) = NextLoc ((IC s),(STC N))
let s be State of (STC N); :: thesis: ( InsCode i = 1 implies IC (Exec (i,s)) = NextLoc ((IC s),(STC N)) )
set M = STC N;
set k = locnum ((IC s),(STC N));
reconsider K = IC s as Element of NAT ;
assume InsCode i = 1 ; :: thesis: IC (Exec (i,s)) = NextLoc ((IC s),(STC N))
then A1: IC (Exec (i,s)) = (IC s) + 1 by Lm2
.= K + 1 ;
( il. ((STC N),(locnum ((IC s),(STC N)))) = locnum ((IC s),(STC N)) & il. ((STC N),((locnum ((IC s),(STC N))) + 1)) = (locnum ((IC s),(STC N))) + 1 ) by Th17;
hence IC (Exec (i,s)) = NextLoc ((IC s),(STC N)) by A1, Def5; :: thesis: verum