:: deftheorem defines INT-Variable AOFA_I00:def 16 :
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-Variable of X holds
( b₅ is INT-Variable of A,f iff ex t being INT-Expression of X st b₅,t form_assignment_wrt f );