LARA This is an old revision of the document! FOL with Update Expressions Syntactic extension of FOL. If-Then-Else ite(p,x,y) = if p then x else y Function Update f(a:=b)(x) = ite(x=a,b,f(x)) Sets Syntax Summary Elimination of Extensions Substituting Function Symbols