:: deftheorem Def1 defines Fix_inp CIRCUIT2:def 1 :
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty Circuit of IIG
for iv being InputValues of A
for b₄ being ManySortedFunction of FreeGen the Sorts of A, the Sorts of (FreeEnv A) holds
( b₄ = Fix_inp iv iff for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b₄ . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b₄ . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b₄ . v = id (FreeGen (v, the Sorts of A)) ) ) );