let k, loc be Element of NAT ; :: thesis: IncAddr (goto loc),k = goto (loc + k)
consider L being Element of NAT such that
A1: loc = L and
A2: goto loc = SCM-goto L by SCMFSA_2:def 16;
reconsider i = SCM-goto (L + k) as Instruction of SCM+FSA by SCMFSA_2:38;
InsCode (goto loc) = 6 by SCMFSA_2:47;
then InsCode (goto loc) in {6,7,8} by ENUMSET1:def 1;
then ex I being Instruction of SCM st
( I = goto loc & IncAddr (goto loc),k = IncAddr I,k ) by Def3;
hence IncAddr (goto loc),k = i by A2, RELOC:10
.= goto (loc + k) by A1, SCMFSA_2:def 16 ;
:: thesis: verum