:: deftheorem defines INT-Exec AOFA_I00:def 27 :
for X being non empty set
for x being Element of X
for b₃ being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,(INT-ElemIns X)), Funcs (X,INT),(Funcs (X,INT)) \ (x,0) holds
( b₃ is INT-Exec of x 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 [v,e])) = s +* ((v . s),(e . s)) );