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