let k be Element of NAT ; :: thesis: for a, b being Int-Location holds IncAddr (SubFrom a,b),k = SubFrom a,b
let a, b be Int-Location ; :: thesis: IncAddr (SubFrom a,b),k = SubFrom a,b
A1: InsCode (SubFrom a,b) = 3 by SCMFSA_2:44;
not 3 in {6,7,8} by ENUMSET1:def 1;
hence IncAddr (SubFrom a,b),k = SubFrom a,b by A1, Def3; :: thesis: verum