Prove:

```    m=0  ==>  inv
```

as follows: assume m=0, then:

```        inv
==  0<= m <= #t  /\  (!n<m . ~(t[n].key = k) )

==  0<= 0 <= #t  /\  (!n<0 . ~(t[n].key = k) )

==  true  /\  true

==  true
```

Prove:

```    inv /\ ~G   ==>  setm
```

as follows:

inv /\ ~G

== inv /\ ~(m<#t /\ ~(t[m].key = k))

== inv /\ (m>=#t \/ t[m].key = k)

== inv /\ (m>=#t \/ (m<#t /\ t[m].key = k))

==> (inv /\ m>=#t) \/ (m<#t /\ t[m].key = k) (*)

Now

```        inv  /\  m>=#t

==  0<= m <= #t  /\  (!n<m . ~(t[n].key = k) )   /\  m>=#t

==  m = #t  /\  (!n<m . ~(t[n].key = k) )

==  m = #t  /\  (!n<#t . ~(t[n].key = k) )

==> m = #t  /\  ~(k in (dom (abs t)))
```

so

```        (*)
==>  (m = #t  /\  ~(k in (dom (abs t))))  \/  m<#t /\ t[m].key = k

==   setm
```

Prove:

```    m<#t  /\  ~(t[m].key = k)  /\  inv  ==>  inv[m\m+1]
```

as follows:

 m<#t /\ ~(t[m].key = k) /\ inv == m<#t /\ ~(t[m].key = k) /\ 0<= m <= #t /\ (!n 0<= m< #t /\ ~(t[m].key = k) /\ (!n 0<= m< #t /\ (!n 0<= m+1<= #t /\ (!n

Prove:

`    m<#t  ==>  0 <= #t-(m+1) < #t-m`

as follows:

 m<#t ==> 0 <= #t-(m+1) ==> 0 <= #t-(m+1) /\ (#t-m)-1 < #t-m ==> 0 <= #t-(m+1) /\ #t-(m+1) < #t-m

```

```