:: deftheorem Def3 defines IGTree CIRCUIT2:def 3 :
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for v being Vertex of IIG
for iv being InputValues of SCS
for b₅ being Element of the Sorts of (FreeEnv SCS) . v holds
( b₅ = IGTree (v,iv) iff ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & b₅ = ((Fix_inp_ext iv) . v) . e ) );