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:72;
hence (Exec ((b := (f,a)),s)) . b = (s . f) /. (abs (s . a)) ; :: thesis: verum