let s be State of SCM+FSA ; :: thesis: for f being FinSeq-Location
for a, b being Int-Location holds (Exec (b := f,a),s) . b = (s . f) /. (abs (s . a))
let f be FinSeq-Location ; :: thesis: for a, b being Int-Location holds (Exec (b := f,a),s) . b = (s . f) /. (abs (s . a))
let a, b be Int-Location ; :: thesis: (Exec (b := f,a),s) . b = (s . f) /. (abs (s . a))
ex k being Element of NAT st
( k = abs (s . a) & (Exec (b := f,a),s) . b = (s . f) /. k ) by SCMFSA_2:98;
hence (Exec (b := f,a),s) . b = (s . f) /. (abs (s . a)) ; :: thesis: verum