for A being preIfWhileAlgebra
for C, I, J being Element of A
for S being non empty set
for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T st A is free & [s,(if-then-else (C,I,J))] in TerminatingPrograms (A,S,T,f) holds
( [s,C] in TerminatingPrograms (A,S,T,f) & ( f . (s,C) in T implies [(f . (s,C)),I] in TerminatingPrograms (A,S,T,f) ) & ( f . (s,C) nin T implies [(f . (s,C)),J] in TerminatingPrograms (A,S,T,f) ) )