:: deftheorem defines INT-Expression AOFA_I00:def 17 :
for A being preIfWhileAlgebra
for X being non empty set
for T being Subset of (Funcs (X,INT))
for f being ExecutionFunction of A, Funcs (X,INT),T st ex I being Element of A st I is_assignment_wrt A,X,f holds
for b₅ being INT-Expression of X holds
( b₅ is INT-Expression of A,f iff ex v being INT-Variable of X st v,b₅ form_assignment_wrt f );