:: deftheorem Def30 defines mod AOFA_I00:def 30 :
for A being Euclidean preIfWhileAlgebra
for X being non empty countable set
for T being Subset of (Funcs (X,INT))
for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T
for t1, t2, b₇ being INT-Expression of A,f holds
( b₇ = t1 mod t2 iff for s being Element of Funcs (X,INT) holds b₇ . s = (t1 . s) mod (t2 . s) );