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) /. |.(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) /. |.(s . bb).|
let bb be Int-Location; :: thesis: for f being FinSeq-Location holds (Exec ((a := (f,bb)),s)) . a = (s . f) /. |.(s . bb).|
let f be FinSeq-Location ; :: thesis: (Exec ((a := (f,bb)),s)) . a = (s . f) /. |.(s . bb).|
ex k being Nat st
( k = |.(s . bb).| & (Exec ((a := (f,bb)),s)) . a = (s . f) /. k ) by SCMFSA_2:72;
hence (Exec ((a := (f,bb)),s)) . a = (s . f) /. |.(s . bb).| ; :: thesis: verum