:: deftheorem defines swap AOFA_I00:def 46 :
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 v1, v2 being INT-Variable of A,f
for x being Variable of f holds swap (v1,x,v2) = ((x := v1) \; (v1 := v2)) \; (v2 := (. x));