```
Proving Hoare's assignment axiom from Floyd's:

1. {P[E/V]} V := E {EXISTS v. V = E[v/V] /\ (P[E/V])[v/V]}   by Floyd's axiom
2. (EXISTS v. V = E[v/V] /\ (P[E/V])[v/V]) ==> P             by logic below
3. {P[E/V]} V := E {P}                                       by postcondition weakening 1. and 2.

Lemma:

(EXISTS v. V = E[v/V] /\ (P[E/V])[v/V])
= (EXISTS v. V = E[v/V] /\ (P[E[v/V]/V]))
= (EXISTS v. V = E[v/V] /\ (P[V/V]))
= (EXISTS v. V = E[v/V] /\ P)
= (EXISTS v. V = E[v/V]) /\ P
==> P

Proving Floyd's assignment axiom from Hoare's:

1. {(EXISTS v. V = E[v/V] /\ P[v/V])[E/V]} V := E
{(EXISTS v. V = E[v/V] /\ P[v/V])}                        by Hoare's axiom
2. P ==> (EXISTS v. V = E[v/V] /\ P[v/V])[E/V]               by logic below
3. {P} V := E {EXISTS v. V = E[v/V] /\ P[v/V]}               by precondition strengthening

Lemma:

(EXISTS v. V = E[v/V] /\ P[v/V])[E/V]
= (EXISTS v. E = E[v/V] /\ P[v/V])
<== (E = E[V/V]) /\ P[V/V]
= (E = E) /\ P
= P

Important terminology from metatheory:

expression
statement
sentence
(first-order) theory
soundness  |- p ==> |= p
consistency
completeness |= p ==> |- p
incompleteness

Example proof:

1. {(X+1)=3}X:=X+1{X=3}
2. {((X+1)+1)=3}X:=X+1{(X+1)=3}
3. {((X+1)+1)=3}X:=X+1;X:=X+1{X=3} from 1. and 2.
4. X=1 ==> ((X+1)+1)=3
5. {X=1}X:=X+1;X:=X+1{X=3} from 3. and 4.

```