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