:: deftheorem Def25 defines INT-Exec AOFA_I00:def 25 :
for b₁ being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (NAT,INT),(Funcs (NAT,INT)) \ (0,0) holds
( b₁ is INT-Exec iff for s being Element of Funcs (NAT,INT)
for v being Element of Funcs ((Funcs (NAT,INT)),NAT)
for e being Element of Funcs ((Funcs (NAT,INT)),INT) holds b₁ . (s,(root-tree [v,e])) = s +* ((v . s),(e . s)) );