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