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<m . ~(t[n].key = k) )
==>	0<= m< #t /\ ~(t[m].key = k) /\ (!n<m . ~(t[n].key = k) )
==>	0<= m< #t /\ (!n<m+1 . ~(t[n].key = k) )
==>	0<= m+1<= #t /\ (!n<m+1 . ~(t[n].key = k) )

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