let S1, S2 be non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr ; ( Terminals S1 = SCM-Data-Loc & NonTerminals S1 = [:1,5:] & ( for x, y, z being Symbol of S1 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) & Terminals S2 = SCM-Data-Loc & NonTerminals S2 = [:1,5:] & ( for x, y, z being Symbol of S2 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) implies S1 = S2 )
assume that
A24:
( Terminals S1 = SCM-Data-Loc & NonTerminals S1 = [:1,5:] )
and
A25:
for x, y, z being Symbol of S1 holds
( x ==> <*y,z*> iff x in [:1,5:] )
; ( not Terminals S2 = SCM-Data-Loc or not NonTerminals S2 = [:1,5:] or ex x, y, z being Symbol of S2 st
( ( x ==> <*y,z*> implies x in [:1,5:] ) implies ( x in [:1,5:] & not x ==> <*y,z*> ) ) or S1 = S2 )
assume that
A26:
( Terminals S2 = SCM-Data-Loc & NonTerminals S2 = [:1,5:] )
and
A27:
for x, y, z being Symbol of S2 holds
( x ==> <*y,z*> iff x in [:1,5:] )
; S1 = S2
A28: the carrier of S1 =
(Terminals S1) \/ (NonTerminals S1)
by LANG1:1
.=
the carrier of S2
by A24, A26, LANG1:1
;
the Rules of S1 = the Rules of S2
proof
set p1 = the
Rules of
S1;
set p2 = the
Rules of
S2;
let a,
b be
object ;
RELAT_1:def 2 ( ( not [a,b] in the Rules of S1 or [a,b] in the Rules of S2 ) & ( not [a,b] in the Rules of S2 or [a,b] in the Rules of S1 ) )
hereby ( not [a,b] in the Rules of S2 or [a,b] in the Rules of S1 )
assume A29:
[a,b] in the
Rules of
S1
;
[a,b] in the Rules of S2then reconsider l =
a as
Symbol of
S1 by ZFMISC_1:87;
reconsider r =
b as
Element of the
carrier of
S1 * by A29, ZFMISC_1:87;
A30:
l ==> r
by A29, LANG1:def 1;
then consider x1,
x2 being
Symbol of
S1 such that A31:
r = <*x1,x2*>
by BINTREE1:def 4;
reconsider l =
l,
x1 =
x1,
x2 =
x2 as
Symbol of
S2 by A28;
l in [:1,5:]
by A25, A30, A31;
then
l ==> <*x1,x2*>
by A27;
hence
[a,b] in the
Rules of
S2
by A31, LANG1:def 1;
verum
end;
assume A32:
[a,b] in the
Rules of
S2
;
[a,b] in the Rules of S1
then reconsider l =
a as
Symbol of
S2 by ZFMISC_1:87;
reconsider r =
b as
Element of the
carrier of
S2 * by A32, ZFMISC_1:87;
A33:
l ==> r
by A32, LANG1:def 1;
then consider x1,
x2 being
Symbol of
S2 such that A34:
r = <*x1,x2*>
by BINTREE1:def 4;
reconsider l =
l,
x1 =
x1,
x2 =
x2 as
Symbol of
S1 by A28;
l in [:1,5:]
by A27, A33, A34;
then
l ==> <*x1,x2*>
by A25;
hence
[a,b] in the
Rules of
S1
by A34, LANG1:def 1;
verum
end;
hence
S1 = S2
by A28; verum