let il be Instruction-Location of SCM ; :: thesis: Next = NextLoc il
Next = il. SCM ,((locnum il) + 1)

proof

Next = il. SCM ,((locnum il) + 1) by Th55;
hence Next = il. SCM ,((locnum il) + 1) by AMISTD_1:def 13; :: thesis: verum

end;

hence Next = NextLoc il ; :: thesis: verum