EQ 2: Textual Replacement

prev: Table of Precedences


E [x := R] or \(E _{R} ^{x} \) denotes an expression that is the same as E, but with all the occurrences of x replaced by "(R)". Unnecessary parentheses maybe removed after substitution.

e.g: (z + y) [z := 5] becomes ((5) + y) becomes (by removing unnecessary parentheses) (5 + y)

If x is a list of *distinct* \( x_1, x_2,...x_n\) of variables and R a list \(R_1\ , R_2 , ... R_n\) of expressions then \(E _{R} ^{x} \) denotes the *simultaneous* replacement in E of the variables of x by corresponding expressions of R, each expression being enclosed by parentheses.

(z + y) [z,y := 5,6] becomes ((5) + (6)) becomes (by removing unnecessary parentheses) (5 + 6)

next: Inference Rules