let k be Element of NAT ; :: thesis: for a being Int-Location
for f being FinSeq-Location holds IncAddr (f :=<0,...,0> a),k = f :=<0,...,0> a
let a be Int-Location ; :: thesis: for f being FinSeq-Location holds IncAddr (f :=<0,...,0> a),k = f :=<0,...,0> a
let f be FinSeq-Location ; :: thesis: IncAddr (f :=<0,...,0> a),k = f :=<0,...,0> a
A1: InsCode (f :=<0,...,0> a) = 12 by SCMFSA_2:53;
not 12 in {6,7,8} by ENUMSET1:def 1;
hence IncAddr (f :=<0,...,0> a),k = f :=<0,...,0> a by A1, Def3; :: thesis: verum