:: deftheorem defines specifies CIRCTRM1:def 16 :
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
( X,A specifies C iff C,X -Circuit A are_similar );