begin
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 V16() 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 V16() 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
V16()
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 V16() 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 V16() 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 V16() 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
V16()
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
set 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;
begin
Lm7:
for x being set holds not x in x
;
begin
Lm8:
for S being non empty non void ManySortedSign
for V being V16() 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 ) ) )
begin
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 )
begin