let S be OrderSortedSign; for X being V2() ManySortedSet of S holds
( NonTerminals (DTConOSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConOSA X) = Union (coprod X) )
let X be V2() ManySortedSet of S; ( NonTerminals (DTConOSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConOSA X) = Union (coprod X) )
set D = DTConOSA X;
set A = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
A1:
the carrier of (DTConOSA X) = (Terminals (DTConOSA X)) \/ (NonTerminals (DTConOSA X))
by LANG1:1;
thus A2:
NonTerminals (DTConOSA X) c= [: the carrier' of S,{ the carrier of S}:]
XBOOLE_0:def 10 ( [: the carrier' of S,{ the carrier of S}:] c= NonTerminals (DTConOSA X) & Terminals (DTConOSA X) = Union (coprod X) )proof
let x be
object ;
TARSKI:def 3 ( not x in NonTerminals (DTConOSA X) or x in [: the carrier' of S,{ the carrier of S}:] )
assume
x in NonTerminals (DTConOSA X)
;
x in [: the carrier' of S,{ the carrier of S}:]
then
x in { s where s is Symbol of (DTConOSA X) : ex n being FinSequence st s ==> n }
by LANG1:def 3;
then consider s being
Symbol of
(DTConOSA X) such that A3:
s = x
and A4:
ex
n being
FinSequence st
s ==> n
;
consider n being
FinSequence such that A5:
s ==> n
by A4;
[s,n] in the
Rules of
(DTConOSA X)
by A5, LANG1:def 1;
then reconsider n =
n as
Element of
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;
reconsider s =
s as
Element of
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) ;
[s,n] in OSREL X
by A5, LANG1:def 1;
hence
x in [: the carrier' of S,{ the carrier of S}:]
by A3, Def4;
verum
end;
A6:
Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:]
by MSAFREE:4;
thus A7:
[: the carrier' of S,{ the carrier of S}:] c= NonTerminals (DTConOSA X)
Terminals (DTConOSA X) = Union (coprod X)proof
let x be
object ;
TARSKI:def 3 ( not x in [: the carrier' of S,{ the carrier of S}:] or x in NonTerminals (DTConOSA X) )
assume A8:
x in [: the carrier' of S,{ the carrier of S}:]
;
x in NonTerminals (DTConOSA X)
then consider o being
Element of the
carrier' of
S,
x2 being
Element of
{ the carrier of S} such that A9:
x = [o,x2]
by DOMAIN_1:1;
set O =
the_arity_of o;
defpred S1[
object ,
object ]
means ex
i being
Element of
S st
(
i <= (the_arity_of o) /. $1 & $2
in coprod (
i,
X) );
A10:
for
a being
object st
a in Seg (len (the_arity_of o)) holds
ex
b being
object st
S1[
a,
b]
proof
let a be
object ;
( a in Seg (len (the_arity_of o)) implies ex b being object st S1[a,b] )
assume
a in Seg (len (the_arity_of o))
;
ex b being object st S1[a,b]
then A11:
a in dom (the_arity_of o)
by FINSEQ_1:def 3;
then A12:
(the_arity_of o) . a in rng (the_arity_of o)
by FUNCT_1:def 3;
A13:
rng (the_arity_of o) c= the
carrier of
S
by FINSEQ_1:def 4;
then consider x being
object such that A14:
x in X . ((the_arity_of o) . a)
by A12, XBOOLE_0:def 1;
take y =
[x,((the_arity_of o) . a)];
S1[a,y]
take
(the_arity_of o) /. a
;
( (the_arity_of o) /. a <= (the_arity_of o) /. a & y in coprod (((the_arity_of o) /. a),X) )
y in coprod (
((the_arity_of o) . a),
X)
by A12, A13, A14, MSAFREE:def 2;
hence
(
(the_arity_of o) /. a <= (the_arity_of o) /. a &
y in coprod (
((the_arity_of o) /. a),
X) )
by A11, PARTFUN1:def 6;
verum
end;
consider b being
Function such that A15:
(
dom b = Seg (len (the_arity_of o)) & ( for
a being
object st
a in Seg (len (the_arity_of o)) holds
S1[
a,
b . a] ) )
from CLASSES1:sch 1(A10);
reconsider b =
b as
FinSequence by A15, FINSEQ_1:def 2;
rng b c= [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
then reconsider b =
b as
FinSequence of
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by FINSEQ_1:def 4;
reconsider b =
b as
Element of
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by FINSEQ_1:def 11;
A19:
now for c being set st c in dom b holds
( ( b . c in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . c holds
the_result_sort_of o1 <= (the_arity_of o) /. c ) & ( b . c in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. c & b . c in coprod (i,X) ) ) )let c be
set ;
( c in dom b implies ( ( b . c in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . c holds
the_result_sort_of o1 <= (the_arity_of o) /. c ) & ( b . c in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. c & b . c in coprod (i,X) ) ) ) )assume
c in dom b
;
( ( b . c in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . c holds
the_result_sort_of o1 <= (the_arity_of o) /. c ) & ( b . c in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. c & b . c in coprod (i,X) ) ) )then consider i being
Element of
S such that A20:
i <= (the_arity_of o) /. c
and A21:
b . c in coprod (
i,
X)
by A15;
dom (coprod X) = the
carrier of
S
by PARTFUN1:def 2;
then
(coprod X) . i in rng (coprod X)
by FUNCT_1:def 3;
then
coprod (
i,
X)
in rng (coprod X)
by MSAFREE:def 3;
then
b . c in union (rng (coprod X))
by A21, TARSKI:def 4;
then
b . c in Union (coprod X)
by CARD_3:def 4;
hence
(
b . c in [: the carrier' of S,{ the carrier of S}:] implies for
o1 being
OperSymbol of
S st
[o1, the carrier of S] = b . c holds
the_result_sort_of o1 <= (the_arity_of o) /. c )
by A6, XBOOLE_0:3;
( b . c in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. c & b . c in coprod (i,X) ) )assume
b . c in Union (coprod X)
;
ex i being Element of S st
( i <= (the_arity_of o) /. c & b . c in coprod (i,X) )thus
ex
i being
Element of
S st
(
i <= (the_arity_of o) /. c &
b . c in coprod (
i,
X) )
by A20, A21;
verum end;
A22:
the
carrier of
S = x2
by TARSKI:def 1;
then reconsider xa =
[o, the carrier of S] as
Element of the
carrier of
(DTConOSA X) by A8, A9, XBOOLE_0:def 3;
len b = len (the_arity_of o)
by A15, FINSEQ_1:def 3;
then
[xa,b] in OSREL X
by A19, Th2;
then
xa ==> b
by LANG1:def 1;
then
xa in { t where t is Symbol of (DTConOSA X) : ex n being FinSequence st t ==> n }
;
hence
x in NonTerminals (DTConOSA X)
by A9, A22, LANG1:def 3;
verum
end;
A23:
Terminals (DTConOSA X) misses NonTerminals (DTConOSA X)
by DTCONSTR:8;
thus
Terminals (DTConOSA X) c= Union (coprod X)
XBOOLE_0:def 10 Union (coprod X) c= Terminals (DTConOSA X)
let x be object ; TARSKI:def 3 ( not x in Union (coprod X) or x in Terminals (DTConOSA X) )
assume A26:
x in Union (coprod X)
; x in Terminals (DTConOSA X)
then
x in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
by XBOOLE_0:def 3;
then
( x in Terminals (DTConOSA X) or x in NonTerminals (DTConOSA X) )
by A1, XBOOLE_0:def 3;
hence
x in Terminals (DTConOSA X)
by A6, A2, A26, XBOOLE_0:3; verum