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