let s1, s2 be State of ; :: thesis: ( IC s1 = IC s2 & ( for a being Data-Location holds s1 . a = s2 . a ) & ( for i being Instruction-Location of SCM holds s1 . i = s2 . i ) implies s1 = s2 )
assume that
A1: IC s1 = IC s2 and
A2: for a being Data-Location holds s1 . a = s2 . a and
A3: for i being Instruction-Location of SCM holds s1 . i = s2 . i ; :: thesis: s1 = s2
consider g1 being Function such that
A4: s1 = g1 and
A5: dom g1 = dom SCM-OK and
for x being set st x in dom SCM-OK holds
g1 . x in SCM-OK . x by CARD_3:def 5;
consider g2 being Function such that
A6: s2 = g2 and
A7: dom g2 = dom SCM-OK and
for x being set st x in dom SCM-OK holds
g2 . x in SCM-OK . x by CARD_3:def 5;

A8: now

let x be set ; :: thesis: ( x in SCM-Memory implies g1 . b₁ = g2 . b₁ )
assume x in SCM-Memory ; :: thesis: g1 . b₁ = g2 . b₁
then A9: ( x in {(IC SCM )} \/ SCM-Data-Loc or x in NAT ) by AMI_3:4, XBOOLE_0:def 3;

per cases ( x in {(IC SCM )} or x in SCM-Data-Loc or x in NAT ) by A9, XBOOLE_0:def 3;

suppose x in {(IC SCM )} ; :: thesis: g1 . b₁ = g2 . b₁

then x = IC SCM by TARSKI:def 1;
hence g1 . x = g2 . x by A1, A4, A6; :: thesis: verum

end;

suppose x in SCM-Data-Loc ; :: thesis: g1 . b₁ = g2 . b₁

then x is Data-Location by AMI_3:def 2;
hence g1 . x = g2 . x by A2, A4, A6; :: thesis: verum

end;

suppose x in NAT ; :: thesis: g1 . b₁ = g2 . b₁

then reconsider l = x as Instruction-Location of SCM by AMI_1:def 4;
g1 . l = g2 . l by A3, A4, A6;
hence g1 . x = g2 . x ; :: thesis: verum

end;

end;

end;

SCM-Memory = dom g1 by A5, FUNCT_2:def 1;
hence s1 = s2 by A4, A5, A6, A7, A8, FUNCT_1:9; :: thesis: verum