:: deftheorem defines is_assignment_wrt AOFA_I00:def 14 :
for A being preIfWhileAlgebra
for I being Element of A
for X being non empty set
for T being Subset of (Funcs (X,INT))
for f being ExecutionFunction of A, Funcs (X,INT),T holds
( I is_assignment_wrt A,X,f iff ( I in ElementaryInstructions A & ex v being INT-Variable of X ex t being INT-Expression of X st
for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) );