:: deftheorem Def28 defines INT-Exec AOFA_I00:def 28 :
for X being non empty set
for T being Subset of (Funcs (X,INT))
for c being Enumeration of X st rng c c= NAT holds
for b₄ being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (X,INT),T holds
( b₄ is INT-Exec of c,T iff for s being Element of Funcs (X,INT)
for v being Element of Funcs ((Funcs (X,INT)),X)
for e being Element of Funcs ((Funcs (X,INT)),INT) holds b₄ . (s,(root-tree [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s)) );