let s be State of SCM+FSA ; :: thesis: for f being FinSeq-Location
for m, n being Element of 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 Element of 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 Element of 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 AMI_3:52;
hence (Exec ((intloc m) := f,a),(Initialized s)) . (intloc (n + 1)) = (Initialized s) . (intloc (n + 1)) by SCMFSA_2:98
.= s . (intloc (n + 1)) by SCMFSA6C:3 ;
:: thesis: verum