:: MSATERM semantic presentation

Lm1: for n being set
for p being FinSequence st n in dom p holds
ex k being Nat st
( n = k + 1 & k < len p )

proof end;

Lm2: now

let n be Nat; :: thesis:
let x be set ; :: thesis:
let p be FinSequence of x; :: thesis:
assume A1: n < len p ; :: thesis:
n >= 0 by NAT_1:18;
then ( n + 1 >= 0 + 1 & n + 1 <= len p ) by A1, NAT_1:38, XREAL_1:9;
then n + 1 in dom p by FINSEQ_3:27;
then A2: p . (n + 1) in rng p by FUNCT_1:def 5;
rng p c= x by FINSEQ_1:def 4;
hence p . (n + 1) in x by A2; :: thesis:

end;

registration

let I be non empty set ;
let X be V3 ManySortedSet of I;
let i be Element of I;
cluster X . i -> non empty ;
coherence ;

end;

definition

let S be non empty non void ManySortedSign ;
let V be ManySortedSet of the carrier of S;
func S -Terms V -> Subset of (FinTrees the carrier of (DTConMSA V)) equals :Def1: :: MSATERM:def 1
TS (DTConMSA V);
correctness ;

end;

:: deftheorem Def1 defines -Terms MSATERM:def 1 :

registration

let S be non empty non void ManySortedSign ;
let V be V3 ManySortedSet of the carrier of S;
cluster S -Terms V -> non empty ;
correctness ;

end;

definition

let S be non empty non void ManySortedSign ;
let V be V3 ManySortedSet of the carrier of S;
mode Term of S,V is Element of S -Terms V;

end;

definition

let S be non empty non void ManySortedSign ;
let V be V3 ManySortedSet of the carrier of S;
let o be OperSymbol of S;
:: original: Sym
redefine func Sym o,V -> NonTerminal of (DTConMSA V);
coherence

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let V be V3 ManySortedSet of the carrier of S;
let sy be NonTerminal of (DTConMSA V);
mode ArgumentSeq of sy -> FinSequence of S -Terms V means :Def2: :: MSATERM:def 2
it is SubtreeSeq of sy;
existence

proof end;

end;

:: deftheorem Def2 defines ArgumentSeq MSATERM:def 2 :

theorem Th1: :: MSATERM:1

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence holds
( ( [o,the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym o,V )

proof end;

Lm3: now

let S be non empty non void ManySortedSign ; :: thesis:
let V be V3 ManySortedSet of the carrier of S; :: thesis:
let x be set ; :: thesis:
set X = V;
set G = DTConMSA V;
A1: Terminals (DTConMSA V) = Union (coprod V) by MSAFREE:6;
A2: dom (coprod V) = the carrier of S by PBOOLE:def 3;

hereby :: thesis:

assume x in Terminals (DTConMSA V) ; :: thesis:
then consider s being set such that
A3: ( s in dom (coprod V) & x in (coprod V) . s ) by A1, CARD_5:10;
reconsider s = s as SortSymbol of S by A3, PBOOLE:def 3;
(coprod V) . s = coprod s,V by MSAFREE:def 3;
then consider a being set such that
A4: ( a in V . s & x = [a,s] ) by A3, MSAFREE:def 2;
thus ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] by A4; :: thesis:

end;

let s be SortSymbol of S; :: thesis:
let a be Element of V . s; :: thesis:
assume x = [a,s] ; :: thesis:
then x in coprod s,V by MSAFREE:def 2;
then x in (coprod V) . s by MSAFREE:def 3;
hence x in Terminals (DTConMSA V) by A1, A2, CARD_5:10; :: thesis:

end;

Lm4: now

let S be non empty non void ManySortedSign ; :: thesis:
let A be MSAlgebra of S; :: thesis:
let V be V3 ManySortedSet of the carrier of S; :: thesis:
let x be set ; :: thesis:
set X = the Sorts of A \/ V;
set G = DTConMSA (the Sorts of A \/ V);
A1: Terminals (DTConMSA (the Sorts of A \/ V)) = Union (coprod (the Sorts of A \/ V)) by MSAFREE:6;
A2: dom (coprod (the Sorts of A \/ V)) = the carrier of S by PBOOLE:def 3;

hereby :: thesis:

assume x in Terminals (DTConMSA (the Sorts of A \/ V)) ; :: thesis:
then consider s being set such that
A3: ( s in dom (coprod (the Sorts of A \/ V)) & x in (coprod (the Sorts of A \/ V)) . s ) by A1, CARD_5:10;
reconsider s = s as SortSymbol of S by A3, PBOOLE:def 3;
(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
A4: ( a in (the Sorts of A \/ V) . s & x = [a,s] ) by A3, 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 A4, XBOOLE_0:def 2;
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 A4; :: thesis:

end;

let s be SortSymbol of S; :: thesis:
A5: (the Sorts of A \/ V) . s = (the Sorts of A . s) \/ (V . s) by PBOOLE:def 7;

hereby :: thesis:

let a be set ; :: thesis:
assume A6: a in the Sorts of A . s ; :: thesis:
assume A7: x = [a,s] ; :: thesis:
a in (the Sorts of A \/ V) . s by A5, A6, XBOOLE_0:def 2;
then x in coprod s,(the Sorts of A \/ V) by A7, 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 A1, A2, CARD_5:10; :: thesis:

end;

let a be Element of V . s; :: thesis:
assume A8: x = [a,s] ; :: thesis:
a in (the Sorts of A \/ V) . s by A5, XBOOLE_0:def 2;
then x in coprod s,(the Sorts of A \/ V) by A8, 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 A1, A2, CARD_5:10; :: thesis:

end;

Lm5: now

let S be non empty non void ManySortedSign ; :: thesis:
let V be V3 ManySortedSet of the carrier of S; :: thesis:
set G = DTConMSA V;
let x be set ; :: thesis:
NonTerminals (DTConMSA V) = [:the OperSymbols of S,{the carrier of S}:] by MSAFREE:6;
hence ( x is NonTerminal of (DTConMSA V) iff x in [:the OperSymbols of S,{the carrier of S}:] ) ; :: thesis:

end;

scheme :: MSATERM:sch 1
TermInd{ F₁() -> non empty non void ManySortedSign , F₂() -> V3 ManySortedSet of the carrier of F₁(), P₁[ set ] } :

for t being Term of F₁(),F₂() holds P₁[t]

provided

A1: for s being SortSymbol of F₁()
for v being Element of F₂() . s holds P₁[ root-tree [v,s]] and
A2: for o being OperSymbol of F₁()
for p being ArgumentSeq of Sym o,F₂() st ( for t being Term of F₁(),F₂() st t in rng p holds
P₁[t] ) holds
P₁[[o,the carrier of F₁()] -tree p]

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra of S;
let V be V3 ManySortedSet of the carrier of S;
mode c-Term of A,V is Term of S,(the Sorts of A \/ V);

end;

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra of S;
let V be V3 ManySortedSet of the carrier of S;
let o be OperSymbol of S;
mode ArgumentSeq of o,A,V is ArgumentSeq of Sym o,(the Sorts of A \/ V);

end;

scheme :: MSATERM:sch 2
CTermInd{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra of F₁(), F₃() -> V3 ManySortedSet of the carrier of F₁(), P₁[ set ] } :

for t being c-Term of F₂(),F₃() holds P₁[t]

provided

A1: for s being SortSymbol of F₁()
for x being Element of the Sorts of F₂() . s holds P₁[ root-tree [x,s]] and
A2: for s being SortSymbol of F₁()
for v being Element of F₃() . s holds P₁[ root-tree [v,s]] and
A3: for o being OperSymbol of F₁()
for p being ArgumentSeq of o,F₂(),F₃() st ( for t being c-Term of F₂(),F₃() st t in rng p holds
P₁[t] ) holds
P₁[(Sym o,(the Sorts of F₂() \/ F₃())) -tree p]

proof end;

definition

let S be non empty non void ManySortedSign ;
let V be V3 ManySortedSet of the carrier of S;
let t be Term of S,V;
let p be Node of t;
:: original: .
redefine func t . p -> Symbol of (DTConMSA V);
coherence

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let V be V3 ManySortedSet of the carrier of S;
cluster -> finite Element of S -Terms V;
coherence ;

end;

Lm6: now

let G be non empty with_terminals with_nonterminals DTConstrStr ; :: thesis:
let s be Symbol of G; :: thesis:
the carrier of G = (Terminals G) \/ (NonTerminals G) by LANG1:1;
hence ( s is Terminal of G or s is NonTerminal of G ) by XBOOLE_0:def 2; :: thesis:
Terminals G misses NonTerminals G by DTCONSTR:8;
hence ( not s is Terminal of G or not s is NonTerminal of G ) by XBOOLE_0:3; :: thesis:

end;

theorem Th2: :: MSATERM:2

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for t being Term of S,V holds
( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [:the OperSymbols of S,{the carrier of S}:] )

proof end;

theorem :: MSATERM:3

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being MSAlgebra of S
for t being c-Term of A,V holds
( ex s being SortSymbol of S ex x being set st
( x in the Sorts of A . s & t . {} = [x,s] ) or ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [:the OperSymbols of S,{the carrier of S}:] )

proof end;

theorem Th4: :: MSATERM:4

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is Term of S,V

proof end;

theorem Th5: :: MSATERM:5

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for t being Term of S,V
for s being SortSymbol of S
for v being Element of V . s st t . {} = [v,s] holds
t = root-tree [v,s]

proof end;

theorem Th6: :: MSATERM:6

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being MSAlgebra of S
for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
root-tree [x,s] is c-Term of A,V

proof end;

theorem :: MSATERM:7

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being MSAlgebra of S
for t being c-Term of A,V
for s being SortSymbol of S
for x being set st x in the Sorts of A . s & t . {} = [x,s] holds
t = root-tree [x,s]

proof end;

theorem Th8: :: MSATERM:8

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being MSAlgebra of S
for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is c-Term of A,V

proof end;

theorem :: MSATERM:9

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being MSAlgebra of S
for t being c-Term of A,V
for s being SortSymbol of S
for v being Element of V . s st t . {} = [v,s] holds
t = root-tree [v,s]

proof end;

theorem Th10: :: MSATERM:10

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for t being Term of S,V
for o being OperSymbol of S st t . {} = [o,the carrier of S] holds
ex a being ArgumentSeq of Sym o,V st t = [o,the carrier of S] -tree a

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
let V be V3 ManySortedSet of the carrier of S;
let s be SortSymbol of S;
let x be Element of the Sorts of A . s;
func x -term A,V -> c-Term of A,V equals :: MSATERM:def 3
root-tree [x,s];
correctness by Th6;

end;

:: deftheorem defines -term MSATERM:def 3 :

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra of S;
let V be V3 ManySortedSet of the carrier of S;
let s be SortSymbol of S;
let v be Element of V . s;
func v -term A -> c-Term of A,V equals :: MSATERM:def 4
root-tree [v,s];
correctness by Th8;

end;

:: deftheorem defines -term MSATERM:def 4 :

definition

let S be non empty non void ManySortedSign ;
let V be V3 ManySortedSet of the carrier of S;
let sy be NonTerminal of (DTConMSA V);
let p be ArgumentSeq of sy;
:: original: -tree
redefine func sy -tree p -> Term of S,V;
coherence

proof end;

end;

scheme :: MSATERM:sch 3
TermInd2{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra of F₁(), F₃() -> V3 ManySortedSet of the carrier of F₁(), P₁[ set ] } :

for t being c-Term of F₂(),F₃() holds P₁[t]

provided

A1: for s being SortSymbol of F₁()
for x being Element of the Sorts of F₂() . s holds P₁[x -term F₂(),F₃()] and
A2: for s being SortSymbol of F₁()
for v being Element of F₃() . s holds P₁[v -term F₂()] and
A3: for o being OperSymbol of F₁()
for p being ArgumentSeq of Sym o,(the Sorts of F₂() \/ F₃()) st ( for t being c-Term of F₂(),F₃() st t in rng p holds
P₁[t] ) holds
P₁[(Sym o,(the Sorts of F₂() \/ F₃())) -tree p]

proof end;

theorem Th11: :: MSATERM:11

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for t being Term of S,V ex s being SortSymbol of S st t in FreeSort V,s

proof end;

theorem :: MSATERM:12

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for s being SortSymbol of S holds FreeSort V,s c= S -Terms V ;

theorem :: MSATERM:13

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S holds S -Terms V = Union (FreeSort V)

proof end;

Lm7: for x being set holds not x in x
;

definition

let S be non empty non void ManySortedSign ;
let V be V3 ManySortedSet of the carrier of S;
let t be Term of S,V;
func the_sort_of t -> SortSymbol of S means :Def5: :: MSATERM:def 5
t in FreeSort V,it;
existence by Th11;
uniqueness

proof end;

end;

:: deftheorem Def5 defines the_sort_of MSATERM:def 5 :

theorem Th14: :: MSATERM:14

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for t being Term of S,V
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s

proof end;

theorem Th15: :: MSATERM:15

proof end;

theorem :: MSATERM:16

proof end;

theorem Th17: :: MSATERM:17

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for t being Term of S,V
for o being OperSymbol of S st t . {} = [o,the carrier of S] holds
the_sort_of t = the_result_sort_of o

proof end;

theorem Th18: :: MSATERM:18

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being non-empty MSAlgebra of S
for s being SortSymbol of S
for x being Element of the Sorts of A . s holds the_sort_of (x -term A,V) = s by Th15;

theorem Th19: :: MSATERM:19

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being MSAlgebra of S
for s being SortSymbol of S
for v being Element of V . s holds the_sort_of (v -term A) = s

proof end;

theorem Th20: :: MSATERM:20

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being ArgumentSeq of Sym o,V holds the_sort_of ((Sym o,V) -tree p) = the_result_sort_of o

proof end;

theorem Th21: :: MSATERM:21

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence of S -Terms V holds
( a is ArgumentSeq of Sym o,V iff Sym o,V ==> roots a )

proof end;

Lm8: for S being non empty non void ManySortedSign
for V being V3 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 ) ) )

proof end;

theorem Th22: :: MSATERM:22

for S being non empty non void ManySortedSign
for V being V3 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
a . i is Term of S,V ) )

proof end;

theorem :: MSATERM:23

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being ArgumentSeq of Sym o,V
for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )

proof end;

theorem Th24: :: MSATERM:24

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence st ( len a = len (the_arity_of o) or 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 & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) holds
a is ArgumentSeq of Sym o,V

proof end;

theorem :: MSATERM:25

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence of S -Terms V st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ) holds
a is ArgumentSeq of Sym o,V

proof end;

theorem Th26: :: MSATERM:26

for S being non empty non void ManySortedSign
for V1, V2 being V3 ManySortedSet of the carrier of S st V1 c= V2 holds
for t being Term of S,V1 holds t is Term of S,V2

proof end;

theorem :: MSATERM:27

for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for V being V3 ManySortedSet of the carrier of S
for t being Term of S,V holds t is c-Term of A,V

proof end;

definition

let S be non empty non void ManySortedSign ;
let V be V3 ManySortedSet of the carrier of S;
mode CompoundTerm of S,V -> Term of S,V means :: MSATERM:def 6
it . {} in [:the OperSymbols of S,{the carrier of S}:];
existence

proof end;

end;

:: deftheorem defines CompoundTerm MSATERM:def 6 :

definition

let S be non empty non void ManySortedSign ;
let V be V3 ManySortedSet of the carrier of S;
mode SetWithCompoundTerm of S,V -> non empty Subset of (S -Terms V) means :: MSATERM:def 7
ex t being CompoundTerm of S,V st t in it;
existence

proof end;

end;

:: deftheorem defines SetWithCompoundTerm MSATERM:def 7 :

theorem :: MSATERM:28

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for t being Term of S,V st not t is root holds
t is CompoundTerm of S,V

proof end;

Lm9: for n being Nat
for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )

proof end;

theorem Th29: :: MSATERM:29

for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for t being Term of S,V
for p being Node of t holds t | p is Term of S,V

proof end;

definition

let S be non empty non void ManySortedSign ;
let V be V3 ManySortedSet of the carrier of S;
let t be Term of S,V;
let p be Node of t;
:: original: |
redefine func t | p -> Term of S,V;
coherence by Th29;

end;

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra of S;
mode Variables of A -> V3 ManySortedSet of the carrier of S means :Def8: :: MSATERM:def 8
it misses the Sorts of A;
existence

proof end;

end;

:: deftheorem Def8 defines Variables MSATERM:def 8 :

theorem Th30: :: MSATERM:30

for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for V being Variables of A
for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
for v being Element of V . s holds x <> v

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
let V be V3 ManySortedSet of the carrier of S;
let t be c-Term of A,V;
let f be ManySortedFunction of V,the Sorts of A;
let vt be finite DecoratedTree;
pred vt is_an_evaluation_of t,f means :Def9: :: MSATERM:def 9
( 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) ) ) ) );

end;

:: deftheorem Def9 defines is_an_evaluation_of MSATERM:def 9 :

theorem Th31: :: MSATERM:31

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 s being SortSymbol of S
for x being Element of the Sorts of A . s st t = root-tree [x,s] holds
root-tree x is_an_evaluation_of t,f

proof end;

theorem Th32: :: MSATERM:32

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 s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
root-tree ((f . s) . v) is_an_evaluation_of t,f

proof end;

theorem Th33: :: MSATERM:33

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for V being Variables of A
for f being ManySortedFunction of V,the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being DTree-yielding FinSequence st len q = len p & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den o,A) . (roots q)) -tree q & vt is_an_evaluation_of (Sym o,(the Sorts of A \/ V)) -tree p,f )

proof end;

theorem Th34: :: MSATERM:34

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for V being Variables of A
for f being ManySortedFunction of V,the Sorts of A
for t being c-Term of A,V
for e being finite DecoratedTree st e is_an_evaluation_of t,f holds
for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f

proof end;

theorem Th35: :: MSATERM:35

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for V being Variables of A
for f being ManySortedFunction of V,the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym o,(the Sorts of A \/ V)) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den o,A) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )

proof end;

theorem Th36: :: MSATERM:36

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 ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f

proof end;

theorem Th37: :: MSATERM:37

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 e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2

proof end;

theorem Th38: :: MSATERM:38

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 vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
vt . {} in the Sorts of A . (the_sort_of t)

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
let V be Variables of A;
let t be c-Term of A,V;
let f be ManySortedFunction of V,the Sorts of A;
func t @ f -> Element of the Sorts of A . (the_sort_of t) means :Def10: :: MSATERM:def 10
ex vt being finite DecoratedTree st
( vt is_an_evaluation_of t,f & it = vt . {} );
existence

proof end;

uniqueness by Th37;

end;

:: deftheorem Def10 defines @ MSATERM:def 10 :

theorem Th39: :: MSATERM:39

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for V being Variables of A
for f being ManySortedFunction of V,the Sorts of A
for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
t @ f = vt . {}

proof end;

theorem :: MSATERM:40

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for V being Variables of A
for f being ManySortedFunction of V,the Sorts of A
for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
for p being Node of t holds vt . p = (t | p) @ f

proof end;

theorem :: MSATERM:41

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for V being Variables of A
for f being ManySortedFunction of V,the Sorts of A
for s being SortSymbol of S
for x being Element of the Sorts of A . s holds (x -term A,V) @ f = x

proof end;

theorem :: MSATERM:42

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for V being Variables of A
for f being ManySortedFunction of V,the Sorts of A
for s being SortSymbol of S
for v being Element of V . s holds (v -term A) @ f = (f . s) . v

proof end;

theorem :: MSATERM:43

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for V being Variables of A
for f being ManySortedFunction of V,the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being FinSequence st len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) holds
((Sym o,(the Sorts of A \/ V)) -tree p) @ f = (Den o,A) . q

proof end;