:: deftheorem Def4 defines size CIRCUIT1:def 4 :
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty finite-yielding MSAlgebra over IIG
for v being SortSymbol of IIG
for b₄ being Nat holds
( b₄ = size (v,A) iff ex s being non empty finite Subset of NAT st
( s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b₄ = max s ) );