:: deftheorem Def8 defines CompatibleValuation CIRCTRM1:def 8 :
for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S
for X being SetWithCompoundTerm of S,V
for A being non-empty finite-yielding MSAlgebra over S
for s being State of (X -Circuit A)
for b₆ being ManySortedFunction of V, the Sorts of A holds
( b₆ is CompatibleValuation of s iff for x being Vertex of S
for v being Element of V . x st root-tree [v,x] in Subtrees X holds
(b₆ . x) . v = s . (root-tree [v,x]) );