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)
consider A being Data-Location , L being Instruction-Location of SCM such that
A1: ( a = A & loc = L ) and
A2: a >0_goto loc = A >0_goto L by SCMFSA_2:def 18;
reconsider i = A >0_goto (L + k) as Instruction of by SCMFSA_2:38;
InsCode (a >0_goto loc) = 8 by SCMFSA_2:49;
then InsCode (a >0_goto loc) in {6,7,8} by ENUMSET1:def 1;
then ex I being Instruction of st
( I = a >0_goto loc & IncAddr (a >0_goto loc),k = IncAddr I,k ) by Def3;
hence IncAddr (a >0_goto loc),k = i by A2, RELOC:12
.= a >0_goto (loc + k) by A1, SCMFSA_2:def 18 ;
:: thesis: verum