let N be non empty with_non-empty_elements set ; :: thesis: for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
(Exec i,s) . (IC (STC N)) = 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
(Exec i,s) . (IC (STC N)) = NextLoc (IC s),(STC N)
let s be State of (STC N); :: thesis: ( InsCode i = 1 implies (Exec i,s) . (IC (STC N)) = 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: (Exec i,s) . (IC (STC N)) = NextLoc (IC s),(STC N)
then A1: (Exec i,s) . (IC (STC N)) = succ (IC s) by Lm4
.= 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 Th37;
hence (Exec i,s) . (IC (STC N)) = NextLoc (IC s),(STC N) by A1, Def13; :: thesis: verum