environ
vocabularies HIDDEN, FINSEQ_1, RELAT_1, SUBSET_1, NUMBERS, ARYTM_3, XXREAL_0, NAT_1, CARD_1, FUNCT_1, TARSKI, STRUCT_0, XBOOLE_0, MSUALG_1, PBOOLE, TREES_3, MSAFREE, DTCONSTR, LANG1, ZFMISC_1, TREES_4, TDGROUP, CARD_3, TREES_2, FINSET_1, MARGREL1, PARTFUN1, TREES_9, ORDINAL4, ORDINAL1, TREES_1, MCART_1, FUNCT_6, TREES_A, QC_LANG1, MSATERM, SETLIM_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, XTUPLE_0, MCART_1, RELAT_1, STRUCT_0, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, FUNCT_2, FINSET_1, TREES_1, TREES_2, CARD_3, FUNCT_6, LANG1, TREES_3, TREES_4, TREES_9, PBOOLE, MSUALG_1, DTCONSTR, MSUALG_3, MSAFREE, XXREAL_0;
definitions TARSKI, PBOOLE, XBOOLE_0;
theorems TARSKI, NAT_1, ZFMISC_1, CARD_3, FUNCT_1, FINSEQ_1, FUNCT_2, FINSEQ_3, FINSEQ_4, CARD_5, FUNCT_6, TREES_1, TREES_2, TREES_3, TREES_4, LANG1, DTCONSTR, TREES_9, PBOOLE, MSUALG_1, MSAFREE, DOMAIN_1, RELAT_1, XBOOLE_0, FINSET_1, XREAL_1, ORDINAL1, PARTFUN1, FINSEQ_2, XTUPLE_0;
schemes TREES_2, CLASSES1, DTCONSTR, PBOOLE;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, FINSEQ_1, PBOOLE, TREES_2, TREES_3, TREES_9, STRUCT_0, DTCONSTR, MSUALG_1, MSUALG_2, MSAFREE, FINSET_1, TREES_1, RELSET_1, XTUPLE_0;
constructors HIDDEN, NAT_1, NAT_D, TREES_9, MSUALG_3, MSAFREE, RELSET_1, XTUPLE_0;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities TARSKI;
expansions TARSKI, PBOOLE;
Lm1:
for n being set
for p being FinSequence st n in dom p holds
ex k being Element of NAT st
( n = k + 1 & k < len p )
Lm3:
now for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for x being set holds
( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V) ) )
let S be non
empty non
void ManySortedSign ;
for V being V2() ManySortedSet of the carrier of S
for x being set holds
( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V) ) )let V be
V2()
ManySortedSet of the
carrier of
S;
for x being set holds
( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V) ) )let x be
set ;
( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V) ) )set X =
V;
set G =
DTConMSA V;
A1:
Terminals (DTConMSA V) = Union (coprod V)
by MSAFREE:6;
let s be
SortSymbol of
S;
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V)let a be
Element of
V . s;
( x = [a,s] implies x in Terminals (DTConMSA V) )assume
x = [a,s]
;
x in Terminals (DTConMSA V)then
x in coprod (
s,
V)
by MSAFREE:def 2;
then A4:
x in (coprod V) . s
by MSAFREE:def 3;
dom (coprod V) = the
carrier of
S
by PARTFUN1:def 2;
hence
x in Terminals (DTConMSA V)
by A1, A4, CARD_5:2;
verum
end;
Lm4:
now for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for V being V2() ManySortedSet of the carrier of S
for x being set holds
( ( not x in Terminals (DTConMSA ( the Sorts of A (\/) V)) or ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) ) ) )
let S be non
empty non
void ManySortedSign ;
for A being MSAlgebra over S
for V being V2() ManySortedSet of the carrier of S
for x being set holds
( ( not x in Terminals (DTConMSA ( the Sorts of A (\/) V)) or ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) ) ) )let A be
MSAlgebra over
S;
for V being V2() ManySortedSet of the carrier of S
for x being set holds
( ( not x in Terminals (DTConMSA ( the Sorts of A (\/) V)) or ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) ) ) )let V be
V2()
ManySortedSet of the
carrier of
S;
for x being set holds
( ( not x in Terminals (DTConMSA ( the Sorts of A (\/) V)) or ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) ) ) )let x be
set ;
( ( not x in Terminals (DTConMSA ( the Sorts of A (\/) V)) or ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) ) ) )set X = the
Sorts of
A (\/) V;
set G =
DTConMSA ( the Sorts of A (\/) V);
A1:
dom (coprod ( the Sorts of A (\/) V)) = the
carrier of
S
by PARTFUN1:def 2;
A2:
Terminals (DTConMSA ( the Sorts of A (\/) V)) = Union (coprod ( the Sorts of A (\/) V))
by MSAFREE:6;
hereby for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) )
assume
x in Terminals (DTConMSA ( the Sorts of A (\/) V))
;
( ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] )then consider s being
object such that A3:
s in dom (coprod ( the Sorts of A (\/) V))
and A4:
x in (coprod ( the Sorts of A (\/) V)) . s
by A2, CARD_5:2;
reconsider s =
s as
SortSymbol of
S by A3, PARTFUN1:def 2;
(coprod ( the Sorts of A (\/) V)) . s = coprod (
s,
( the Sorts of A (\/) V))
by MSAFREE:def 3;
then consider a being
set such that A5:
a in ( the Sorts of A (\/) V) . s
and A6:
x = [a,s]
by A4, MSAFREE:def 2;
( the Sorts of A (\/) V) . s = ( the Sorts of A . s) \/ (V . s)
by PBOOLE:def 4;
then
(
a in the
Sorts of
A . s or
a in V . s )
by A5, XBOOLE_0:def 3;
hence
( ex
s being
SortSymbol of
S ex
a being
set st
(
a in the
Sorts of
A . s &
x = [a,s] ) or ex
s being
SortSymbol of
S ex
v being
Element of
V . s st
x = [v,s] )
by A6;
verum
end;
let s be
SortSymbol of
S;
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) )A7:
( the Sorts of A (\/) V) . s = ( the Sorts of A . s) \/ (V . s)
by PBOOLE:def 4;
let a be
Element of
V . s;
( x = [a,s] implies x in Terminals (DTConMSA ( the Sorts of A (\/) V)) )assume A9:
x = [a,s]
;
x in Terminals (DTConMSA ( the Sorts of A (\/) V))
a in ( the Sorts of A (\/) V) . s
by A7, XBOOLE_0:def 3;
then
x in coprod (
s,
( the Sorts of A (\/) V))
by A9, MSAFREE:def 2;
then
x in (coprod ( the Sorts of A (\/) V)) . s
by MSAFREE:def 3;
hence
x in Terminals (DTConMSA ( the Sorts of A (\/) V))
by A2, A1, CARD_5:2;
verum
end;
Lm7:
for x being set holds not x in x
;
Lm8:
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being ArgumentSeq of Sym (o,V) holds
( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) ) )
Lm9:
for n being Element of NAT
for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )