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