:: deftheorem defines calculates CIRCTRM1:def 15 :
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 X being non empty Subset of (S -Terms V)
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G holds
( C calculates X,A iff ex f, g being Function st
( f,g form_embedding_of X -Circuit A,C & f preserves_inputs_of X -CircuitStr ,G ) );