:: deftheorem defines -Execution AOFA_A00:def 27 :
for B being non empty non void ManySortedSign
for Y being V2() ManySortedSet of the carrier of B
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself vf-free VarMSAlgebra over B
for C being image of T
for X being GeneratorSystem over B,Y,T
for A being preIfWhileAlgebra of the generators of X
for a being SortSymbol of B
for x being Element of the generators of X . a
for z being Element of C,a
for b₁₀ being Subset of (Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X))) holds
( b₁₀ = C -Execution (A,x,z) iff for f being Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) holds
( f in b₁₀ iff ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) ) ) );