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