:: deftheorem defines is_an_evaluation_of MSATERM:def 9 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being V2() 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)) ) ) ) ) );