CONDITIONAL ::= conditional TERM FORMULA TERM
A conditional term is written:
T1 when F else T2
It is well-sorted for some sort when both T1 and T2 are well-sorted for that sort and F is a well-formed formula. The enclosing atomic formula `A[T1 when F else T2]' expands to:
(A[T1] if F) /\ (A[T2] if ¬ F)When several conditional terms occur in the same atomic formula, the expansions are made in a fixed but arbitrary order (all orders yield equivalent formulae).