for A being preIfWhileAlgebra
for S being non empty set
for T being Subset of S
for f being ExecutionFunction of A,S,T
for C, I, J being Element of A st C is_terminating_wrt f & I is_terminating_wrt f & J is_terminating_wrt f holds
if-then-else (C,I,J) is_terminating_wrt f