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