Conditional Expressions

The Idea

• Expressions of the form $ite(φ,s,t)
• Replaces the old $ite_t and $ite_f
• Conditional expressions removed from plain TFF

Examples

• max: ($int * $int) > $int
  ! [X: $int,Y: $int]: max(X,Y) = $ite($greatereq(X,Y),X,Y)
  ! [X: $int,Y: $int]:
    $ite(max(X,Y) = X,$greatereq(X,Y),$greatereq(Y,X))