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:73;
hence (Exec (((f,a) := b),s)) . f = (s . f) +* ((abs (s . a)),(s . b)) ; :: thesis: verum