let S be non void Signature; for X being ManySortedSet of the carrier of S st X is with_missing_variables holds
( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) )
let X be ManySortedSet of the carrier of S; ( X is with_missing_variables implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) )
assume A1:
X is with_missing_variables
; ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) )
set D = DTConMSA X;
set A = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
A2:
Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:]
by MSAFREE:4;
A3:
Terminals (DTConMSA X) misses NonTerminals (DTConMSA X)
by DTCONSTR:8;
thus
NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:]
by MSAFREE:6; XBOOLE_0:def 10 ( [: the carrier' of S,{ the carrier of S}:] c= NonTerminals (DTConMSA X) & Terminals (DTConMSA X) = Union (coprod X) )
thus A4:
[: the carrier' of S,{ the carrier of S}:] c= NonTerminals (DTConMSA X)
Terminals (DTConMSA X) = Union (coprod X)proof
let o,
x2 be
object ;
RELAT_1:def 3 ( not x2 ast in [: the carrier' of S,{ the carrier of S}:] or x2 ast in NonTerminals (DTConMSA X) )
assume A5:
[o,x2] in [: the carrier' of S,{ the carrier of S}:]
;
x2 ast in NonTerminals (DTConMSA X)
then A6:
x2 in { the carrier of S}
by ZFMISC_1:87;
reconsider o =
o as
OperSymbol of
S by A5, ZFMISC_1:87;
A7:
the
carrier of
S = x2
by A6, TARSKI:def 1;
then reconsider xa =
[o, the carrier of S] as
Element of the
carrier of
(DTConMSA X) by A5, XBOOLE_0:def 3;
set O =
the_arity_of o;
defpred S1[
object ,
object ]
means ( $2
in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) & (
X . ((the_arity_of o) . $1) <> {} implies $2
in coprod (
((the_arity_of o) . $1),
X) ) & (
X . ((the_arity_of o) . $1) = {} implies ex
o being
OperSymbol of
S st
( $2
= [o, the carrier of S] &
the_result_sort_of o = (the_arity_of o) . $1 ) ) );
A8:
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 A9:
a in dom (the_arity_of o)
by FINSEQ_1:def 3;
then A10:
(the_arity_of o) . a in rng (the_arity_of o)
by FUNCT_1:def 3;
then reconsider s =
(the_arity_of o) . a as
SortSymbol of
S ;
per cases
( not X . ((the_arity_of o) . a) is empty or X . ((the_arity_of o) . a) = {} )
;
suppose
not
X . ((the_arity_of o) . a) is
empty
;
ex b being object st S1[a,b]then consider x being
object such that A11:
x in X . ((the_arity_of o) . a)
by XBOOLE_0:def 1;
take y =
[x,((the_arity_of o) . a)];
S1[a,y]A12:
y in coprod (
((the_arity_of o) . a),
X)
by A10, A11, MSAFREE:def 2;
A13:
(the_arity_of o) . a in rng (the_arity_of o)
by A9, FUNCT_1:def 3;
dom (coprod X) = the
carrier of
S
by PARTFUN1:def 2;
then
(coprod X) . ((the_arity_of o) . a) in rng (coprod X)
by A13, FUNCT_1:def 3;
then
coprod (
((the_arity_of o) . a),
X)
in rng (coprod X)
by A13, MSAFREE:def 3;
then
y in Union (coprod X)
by A12, TARSKI:def 4;
hence
S1[
a,
y]
by A10, A11, MSAFREE:def 2, XBOOLE_0:def 3;
verum end; end;
end;
consider b being
Function such that A16:
(
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(A8);
reconsider b =
b as
FinSequence by A16, 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;
A17:
len b = len (the_arity_of o)
by A16, FINSEQ_1:def 3;
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 b . c in coprod (((the_arity_of o) . c),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 b . c in coprod (((the_arity_of o) . c),X) ) ) )assume A18:
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 b . c in coprod (((the_arity_of o) . c),X) ) )then A19:
S1[
c,
b . c]
by A16;
dom (the_arity_of o) = Seg (len (the_arity_of o))
by FINSEQ_1:def 3;
then A20:
(the_arity_of o) . c in rng (the_arity_of o)
by A16, A18, FUNCT_1:def 3;
dom (coprod X) = the
carrier of
S
by PARTFUN1:def 2;
then
(coprod X) . ((the_arity_of o) . c) in rng (coprod X)
by A20, FUNCT_1:def 3;
then
coprod (
((the_arity_of o) . c),
X)
in rng (coprod X)
by A20, MSAFREE:def 3;
then
(
X . ((the_arity_of o) . c) <> {} implies
b . c in Union (coprod X) )
by A19, TARSKI: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 A2, A19, XBOOLE_0:3, XTUPLE_0:1;
( b . c in Union (coprod X) implies b . c in coprod (((the_arity_of o) . c),X) )assume A21:
b . c in Union (coprod X)
;
b . c in coprod (((the_arity_of o) . c),X)hence
b . c in coprod (
((the_arity_of o) . c),
X)
by A16, A18;
verum end;
then
[xa,b] in REL X
by A17, MSAFREE:5;
then
xa ==> b
;
hence
x2 ast in NonTerminals (DTConMSA X)
by A7;
verum
end;
thus
Terminals (DTConMSA X) c= Union (coprod X)
XBOOLE_0:def 10 Union (coprod X) c= Terminals (DTConMSA X)
thus
Union (coprod X) c= Terminals (DTConMSA X)
by MSAFREE:6; verum