let s be State of SCM+FSA; :: thesis: for f being FinSeq-Location
for m, n being Nat
for a being Int-Location st m <> n + 1 holds
(Exec (((intloc m) := (f,a)),(Initialized s))) . (intloc (n + 1)) = s . (intloc (n + 1))
let f be FinSeq-Location ; :: thesis: for m, n being Nat
for a being Int-Location st m <> n + 1 holds
(Exec (((intloc m) := (f,a)),(Initialized s))) . (intloc (n + 1)) = s . (intloc (n + 1))
let m, n be Nat; :: thesis: for a being Int-Location st m <> n + 1 holds
(Exec (((intloc m) := (f,a)),(Initialized s))) . (intloc (n + 1)) = s . (intloc (n + 1))
let a be Int-Location; :: thesis: ( m <> n + 1 implies (Exec (((intloc m) := (f,a)),(Initialized s))) . (intloc (n + 1)) = s . (intloc (n + 1)) )
assume m <> n + 1 ; :: thesis: (Exec (((intloc m) := (f,a)),(Initialized s))) . (intloc (n + 1)) = s . (intloc (n + 1))
then intloc m <> intloc (n + 1) by SCMFSA_2:101;
hence (Exec (((intloc m) := (f,a)),(Initialized s))) . (intloc (n + 1)) = (Initialized s) . (intloc (n + 1)) by SCMFSA_2:72
.= s . (intloc (n + 1)) by SCMFSA_M:37 ;
:: thesis: verum