# Exercise 3

## 1.

read is a partial function because it has a precondition.

## 2.

### (a)

Correct and holds. Application of A4.

### (b)

Correct and holds.

```read(n,write(m,d2,write(n,d1,f))) = read(n, write(n,d1,write(m,d2,f))) [Axiom 5]
```
```d1 = d1
```

### c)

Correct, but does not hold. Left hand side:

```read (n,write (n,d2,write (n,d1,f))) = (A4)
d2
```

Right hand side:

```read (n,write (n,d1,write (n,d2,f)) = (A4)
d1
```

### d)

Not correct.

```read (n,write (m,d1,format_disk)) = (A5)
read (n, format_disk) <-- violates P1 because A1
```

## 3.

We prove sufficient completeness by structural Induction over the terms.

Let d: DATA; n,m: NAME with n != m; f: FILE_SYSTEM).

Base case: file_exists(n, format_disk) = false (A1)

read can not be executed for arbitrary n on format_disk because P1.

Step case: Induction hypothesis: Sufficient completness holds for $T_{sub}$ being a subterm of T.

file_exists(n,write(n,d,f)) = true (A2)

file_exists(m,write(n,d,f)) = file_exists(m,f) (A3)

Q.E.D.

## 4.

delete: NAME x FILE_SYSTEM -/-> FILE_SYSTEM

let n,m : NAME

delete(n,f) requires file_exists(n,f)

A6: file_exists(n, delete(m,f)) = false

Since we only would need to adapt the step case of the proof, and read(n, delete(n,f)) is not possible (P1), read(m, delete(n,f)) = read(m,f) because it does not affect m, and can be easily adapted similiar, the ADT is still sufficiently complete specified.