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