let N be 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)
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)
let s be State of (STC N); :: thesis: ( InsCode i = 1 implies (Exec i,s) . (IC (STC N)) = NextLoc (IC s) )
assume A1: InsCode i = 1 ; :: thesis: (Exec i,s) . (IC (STC N)) = NextLoc (IC s)
set M = STC N;
set k = locnum (IC s);
A2: ( il. (STC N),(locnum (IC s)) = locnum (IC s) & il. (STC N),((locnum (IC s)) + 1) = (locnum (IC s)) + 1 ) by Th37;
reconsider K = IC s as Element of NAT by AMI_1:def 4;
(Exec i,s) . (IC (STC N)) = succ (IC s) by A1, Lm4
.= K + 1 by NAT_1:39 ;
hence (Exec i,s) . (IC (STC N)) = NextLoc (IC s) by A2, Def13; :: thesis: verum