let N be with_zero set ; 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); 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); ( 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
; 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; verum