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
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
C calculates X,A