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