for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V st ( for t being Term of S,V
for o being OperSymbol of S holds
( not t in Subtrees X or not t . {} = [o, the carrier of S] or not the_arity_of o = {} ) ) holds
for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for t being Term of S,V st t in Subtrees X holds
( Following (s,(height (dom t))) is_stable_at t & (Following (s,(height (dom t)))) . t = t @ (f,A) )