:: deftheorem defines form_assignment_wrt AOFA_I00:def 15 :
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
for v being INT-Variable of X
for t being INT-Expression of X holds
( v,t form_assignment_wrt f iff ex I being Element of A st
( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) );