let A be Data-Location ; :: thesis: for a being Int-Location
for S being State of SCM
for s1, s being State of SCM+FSA st s1 = (s +* S) +* (s | NAT) & A = a holds
S . A = s1 . a
let a be Int-Location ; :: thesis: for S being State of SCM
for s1, s being State of SCM+FSA st s1 = (s +* S) +* (s | NAT) & A = a holds
S . A = s1 . a
let S be State of SCM; :: thesis: for s1, s being State of SCM+FSA st s1 = (s +* S) +* (s | NAT) & A = a holds
S . A = s1 . a
let s1, s be State of SCM+FSA; :: thesis: ( s1 = (s +* S) +* (s | NAT) & A = a implies S . A = s1 . a )
assume that
A1: s1 = (s +* S) +* (s | NAT) and
A2: A = a ; :: thesis: S . A = s1 . a
A3: dom S = the carrier of SCM by PARTFUN1:def 4
.= SCM-Memory ;
A4: a in SCM+FSA-Data-Loc by Def4;

A5: now

assume a in NAT ; :: thesis: contradiction
then SCM+FSA-OK . a = SCM+FSA-Instr by SCMFSA_1:11;
hence contradiction by A4, SCMFSA_1:10, SCMFSA_1:13; :: thesis: verum

end;

dom (s | NAT) = (dom s) /\ NAT by RELAT_1:90;
then not a in dom (s | NAT) by A5, XBOOLE_0:def 4;
hence s1 . a = (s +* S) . a by A1, FUNCT_4:12
.= S . A by A2, A3, FUNCT_4:14 ;
:: thesis: verum