:: deftheorem defines gt AOFA_I00:def 65 :
for A being Euclidean preIfWhileAlgebra
for X being non empty countable set
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for v1, v2 being INT-Variable of A,g holds v1 gt v2 = (. v1) gt (. v2);