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 | NAT ) = (dom s) /\ NAT by RELAT_1:90;
A4: a in SCM+FSA-Data-Loc by Def4;

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;

then A5: not a in dom (s | NAT ) by A3, XBOOLE_0:def 4;
A6: dom S = dom SCM-OK by CARD_3:18
.= SCM-Memory by FUNCT_2:def 1 ;
thus s1 . a = (s +* S) . a by A1, A5, FUNCT_4:12
.= S . A by A2, A6, FUNCT_4:14 ; :: thesis: verum