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 )
:: deftheorem Def1 defines -Terms MSATERM:def 1 :
for S being non empty non void ManySortedSign
for V being ManySortedSet of the carrier of S holds S -Terms V = TS (DTConMSA V);
:: deftheorem Def2 defines ArgumentSeq MSATERM:def 2 :
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for sy being NonTerminal of (DTConMSA V)
for b4 being FinSequence of S -Terms V holds
( b4 is ArgumentSeq of sy iff b4 is SubtreeSeq of sy );
theorem Th1:
Lm3:
now
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 4;
hence
x in Terminals (DTConMSA V)
by A1, A4, CARD_5:10;
verum
end;
Lm4:
now
let S be non
empty non
void ManySortedSign ;
for A being MSAlgebra of 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 of
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 4;
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:10;
reconsider s =
s as
SortSymbol of
S by A3, PARTFUN1:def 4;
(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 7;
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 7;
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:10;
verum
end;
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem
theorem Th10:
:: deftheorem defines -term MSATERM:def 3 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for V being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S
for x being Element of the Sorts of A . s holds x -term (A,V) = root-tree [x,s];
:: deftheorem defines -term MSATERM:def 4 :
for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for V being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S
for v being Element of V . s holds v -term A = root-tree [v,s];
begin
theorem Th11:
theorem
theorem
Lm7:
for x being set holds not x in x
;
:: deftheorem Def5 defines the_sort_of MSATERM:def 5 :
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V
for b4 being SortSymbol of S holds
( b4 = the_sort_of t iff t in FreeSort (V,b4) );
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem
theorem Th19:
theorem Th20:
begin
theorem Th21:
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 ) ) )
theorem Th22:
theorem
theorem Th24:
theorem
theorem Th26:
theorem
begin
:: deftheorem defines CompoundTerm MSATERM:def 6 :
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for b3 being Term of S,V holds
( b3 is CompoundTerm of S,V iff b3 . {} in [: the carrier' of S,{ the carrier of S}:] );
:: deftheorem defines SetWithCompoundTerm MSATERM:def 7 :
for S being non empty non void ManySortedSign
for V being V16() ManySortedSet of the carrier of S
for b3 being non empty Subset of (S -Terms V) holds
( b3 is SetWithCompoundTerm of S,V iff ex t being CompoundTerm of S,V st t in b3 );
theorem
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 )
theorem Th29:
begin
:: deftheorem Def8 defines Variables MSATERM:def 8 :
for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for b3 being V16() ManySortedSet of the carrier of S holds
( b3 is Variables of A iff b3 misses the Sorts of A );
theorem Th30:
:: deftheorem Def9 defines is_an_evaluation_of MSATERM:def 9 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for V being V16() ManySortedSet of the carrier of S
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for vt being finite DecoratedTree holds
( vt is_an_evaluation_of t,f iff ( dom vt = dom t & ( for p being Node of vt holds
( ( for s being SortSymbol of S
for v being Element of V . s st t . p = [v,s] holds
vt . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st t . p = [x,s] holds
vt . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds
vt . p = (Den (o,A)) . (succ (vt,p)) ) ) ) ) );
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
:: deftheorem Def10 defines @ MSATERM:def 10 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for b6 being Element of the Sorts of A . (the_sort_of t) holds
( b6 = t @ f iff ex vt being finite DecoratedTree st
( vt is_an_evaluation_of t,f & b6 = vt . {} ) );
theorem Th39:
theorem
theorem
theorem
theorem