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