let R be good Ring; :: thesis: for s1, s2 being State of st IC s1 = IC s2 & ( for a being Data-Location of R holds s1 . a = s2 . a ) & ( for i being Instruction-Location of SCM R holds s1 . i = s2 . i ) holds
s1 = s2
let s1, s2 be State of ; :: thesis: ( IC s1 = IC s2 & ( for a being Data-Location of R holds s1 . a = s2 . a ) & ( for i being Instruction-Location of SCM R holds s1 . i = s2 . i ) implies s1 = s2 )
assume that
A1: IC s1 = IC s2 and
A2: for a being Data-Location of R holds s1 . a = s2 . a and
A3: for i being Instruction-Location of SCM R holds s1 . i = s2 . i ; :: thesis: s1 = s2
s1 is Element of product (SCM-OK R) by SCMRING2:def 1;
then consider g1 being Function such that
A4: s1 = g1 and
A5: dom g1 = dom (SCM-OK R) and
for x being set st x in dom (SCM-OK R) holds
g1 . x in (SCM-OK R) . x by CARD_3:def 5;
s2 is Element of product (SCM-OK R) by SCMRING2:def 1;
then consider g2 being Function such that
A6: s2 = g2 and
A7: dom g2 = dom (SCM-OK R) and
for x being set st x in dom (SCM-OK R) holds
g2 . x in (SCM-OK R) . x by CARD_3:def 5;
A8: now
A9: SCM-Memory = ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ NAT by SCMRING2:def 1;
let x be set ; :: thesis: ( x in SCM-Memory implies g1 . b1 = g2 . b1 )
assume x in SCM-Memory ; :: thesis: g1 . b1 = g2 . b1
then A10: ( x in {(IC (SCM R))} \/ SCM-Data-Loc or x in NAT ) by A9, XBOOLE_0:def 3;
per cases ( x in {(IC (SCM R))} or x in SCM-Data-Loc or x in NAT ) by A10, XBOOLE_0:def 3;
suppose x in {(IC (SCM R))} ; :: thesis: g1 . b1 = g2 . b1
then x = IC (SCM R) by TARSKI:def 1;
hence g1 . x = g2 . x by A1, A4, A6; :: thesis: verum
end;
suppose x in NAT ; :: thesis: g1 . b1 = g2 . b1
then reconsider l = x as Instruction-Location of SCM R by AMI_1:def 4;
l = x ;
hence g1 . x = g2 . x by A3, A4, A6; :: 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