let k be Element of NAT ; :: thesis: for loc being Instruction-Location of SCM+FSA
for a being Int-Location holds IncAddr (a =0_goto loc),k = a =0_goto (loc + k)
let loc be Instruction-Location of SCM+FSA ; :: thesis: for a being Int-Location holds IncAddr (a =0_goto loc),k = a =0_goto (loc + k)
let a be Int-Location ; :: thesis: IncAddr (a =0_goto loc),k = a =0_goto (loc + k)
InsCode (a =0_goto loc) = 7 by SCMFSA_2:48;
then InsCode (a =0_goto loc) in {6,7,8} by ENUMSET1:def 1;
then consider I being Instruction of SCM such that
A1: I = a =0_goto loc and
A2: IncAddr (a =0_goto loc),k = IncAddr I,k by Def3;
consider A being Data-Location , L being Instruction-Location of SCM such that
A3: ( a = A & loc = L ) and
A4: a =0_goto loc = A =0_goto L by SCMFSA_2:def 17;
reconsider i = A =0_goto (L + k) as Instruction of SCM+FSA by SCMFSA_2:38;
thus IncAddr (a =0_goto loc),k = i by A1, A2, A4, RELOC:11
.= a =0_goto (loc + k) by A3, SCMFSA_2:def 17 ; :: thesis: verum