**Set Membership:**
` x in S `

True iff x is an element of the set S.

**Set Comprehension:**
` { x | p } `

The set of elements `x` satisfying predicate `p`.

**Relation:** A relation is a set of pairs, e.g.,
`R = { (x,y) | p } `, and `x` is related to `y` by
`R` if
`(x,y) in R`.

**Domain:**
` (dom R) = { x | ?y. (x,y) in R }`

**Range:**
` (ran R) = { y | ?x. (x,y) in R }`

**
Partial Function:** A partial function is a relation in which each domain
element `x` has at most one corresponding range element `y`.

**
Application:** If `f` is a partial function, and `x in dom f`,
then we write `f(x)` for that unique `y` corresponding to
`x` in
`f`.

**Array Declaration:**
` s : ARRAY OF T `

Declares `s` to be an array of elements of type `T`.

**Array Size:**
` #s `

**Array Indexing:**
` s[i] `

The first element of `s` is `s[0]`, while the last element
is `s[#s-1]`.

**Less than or equal to:**
`E <= F`

**Greater than or equal to:**
`E >= F`