• English only

# Lab for Automated Reasoning and Analysis LARA

## Problem 1

Let be the set of all first-order formulas (viewed as syntax trees) and let be the implication relation on formulas:

Check whether is reflexive, antisymmetric, and transitive relation.

## Problem 2

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

## Problem 3

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?