# Lab 04: QE, Lattices and Fixed points

## Exercise 1

Recall the algorithm for quantifier elimination for Presburger arithmetic.

Use this algorithm to eliminate quantifiers in the following formula in Presburger arithmetic.

## Exercise 2

Prove the following:

## Exercise 3

Let be a partial order such that every set has the greatest lower bound.
Prove that then every set has the least upper bound.

## Exercise 4

Let be the set of continuous functions from to the reals. Define on by if and only if for all . Show that is a partial order and that with this order forms a lattice.

## Exercise 5

Let be the interval of real numbers. Recall that, by definition of real numbers and complete lattice, is a complete lattice with least lattice element and greatest lattice element . Here is the least upper bound operator on sets of real numbers, also called supremum and denoted sup in real analysis.

Let function be given by

#### Part a)

Prove that is monotonic and injective (so it is strictly monotonic).

#### Part b)

Compute the set of fixpoints of .

#### Part c)

Define . (This is in fact equal to when is a monotonic bounded function.)

Compute (prove that the computed value is correct by definition of , that is, that the value is indeed of the set of values). Is a fixpoint of ? Is a fixpoint of ? Is an -continuous function?