let s1, s2 be State of SCM+FSA ; :: thesis: ( IC s1 = IC s2 & ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & ( for i being Element of NAT holds s1 . i = s2 . i ) implies s1 = s2 )
assume that
A1: IC s1 = IC s2 and
A2: for a being Int-Location holds s1 . a = s2 . a and
A3: for f being FinSeq-Location holds s1 . f = s2 . f and
A4: for i being Element of NAT holds s1 . i = s2 . i ; :: thesis: s1 = s2
s1 in product SCM+FSA-OK by PBOOLE:155;
then consider g1 being Function such that
A5: s1 = g1 and
A6: dom g1 = dom SCM+FSA-OK and
for x being set st x in dom SCM+FSA-OK holds
g1 . x in SCM+FSA-OK . x by CARD_3:def 5;
s2 in product SCM+FSA-OK by PBOOLE:155;
then consider g2 being Function such that
A7: s2 = g2 and
A8: dom g2 = dom SCM+FSA-OK and
for x being set st x in dom SCM+FSA-OK holds
g2 . x in SCM+FSA-OK . x by CARD_3:def 5;
A9: now
let x be set ; :: thesis: ( x in SCM+FSA-Memory implies g1 . b1 = g2 . b1 )
assume x in SCM+FSA-Memory ; :: thesis: g1 . b1 = g2 . b1
then ( x in ({(IC SCM+FSA )} \/ SCM+FSA-Data-Loc ) \/ SCM+FSA-Data*-Loc or x in NAT ) by Th7, SCMFSA_1:8, XBOOLE_0:def 3;
then A10: ( x in {(IC SCM+FSA )} \/ SCM+FSA-Data-Loc or x in SCM+FSA-Data*-Loc or x in NAT ) by XBOOLE_0:def 3;
per cases ( x in {(IC SCM+FSA )} or x in SCM+FSA-Data-Loc or x in SCM+FSA-Data*-Loc or x in NAT ) by A10, XBOOLE_0:def 3;
suppose x in {(IC SCM+FSA )} ; :: thesis: g1 . b1 = g2 . b1
then x = IC SCM+FSA by TARSKI:def 1;
hence g1 . x = g2 . x by A1, A5, A7; :: thesis: verum
end;
suppose x in NAT ; :: thesis: g1 . b1 = g2 . b1
then reconsider l = x as Element of NAT ;
g1 . l = g2 . l by A4, A5, A7;
hence g1 . x = g2 . x ; :: thesis: verum
end;
end;
end;
SCM+FSA-Memory = dom g1 by A6, FUNCT_2:def 1;
hence s1 = s2 by A5, A6, A7, A8, A9, FUNCT_1:9; :: thesis: verum