• English only

# Lab for Automated Reasoning and Analysis LARA

This is a sketch of the solution of SAV07 Homework 4

### Part 1

Then we have

.

Then we have .

Note that we have .

Basically, and both act as a left zeros of for the relations of the form .

### Part 2

It is easiest to use the definition of Galois connection given by . The condition then reduces to

Both sides are equivalent to , that is, to the Hoare triple .

### Part 3

is not a partial order, it is merely a preorder.

### Part 4

Let denote . We then have and the statement reduces to proving the equivalence between

and

We prove both directions.

: Let . Take any such that . Then , so . Therefore .

: Let . Let . Then , so also . Thus .

### Part 5

Lemma: .

: Let . Then by construction of , so by definition of we have , i.e. .

: Let . Then . By monotonicity of wp, also , so .

: Let . Then , so by basic set theory .

assume(F) skip assert(F), assert(F); assume(F) assert(F), assume(F); assert(F) assume(F) - follow from rules for computing weakest preconditions.

### Part 6

Suppose . Then by Part 5 we have

Suppose . Then

Suppose . Then

Suppose . Then

### Part 7

By shunting rules in Part 6 we have . By monotonicity properties in Part 5, we then obtain by structural induction.