:: deftheorem Def32 defines gt AOFA_I00:def 32 :
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₇ = gt (t1,t2) iff for s being Element of Funcs (X,INT) holds b₇ . s = IFGT ((t1 . s),(t2 . s),1,0) );