let A be Data-Location; :: thesis: for a being Int-Location
for S being State of SCM
for s being State of SCM+FSA st S = s | SCM-Memory & A = a holds
S . A = s . a
let a be Int-Location; :: thesis: for S being State of SCM
for s being State of SCM+FSA st S = s | SCM-Memory & A = a holds
S . A = s . a
let S be State of SCM; :: thesis: for s being State of SCM+FSA st S = s | SCM-Memory & A = a holds
S . A = s . a
let s be State of SCM+FSA; :: thesis: ( S = s | SCM-Memory & A = a implies S . A = s . a )
assume S = s | SCM-Memory ; :: thesis: ( not A = a or S . A = s . a )
then s = s +* S by Th45;
hence ( not A = a or S . A = s . a ) by Th47; :: thesis: verum