{n+1 =< nmax and (exist i (1= (if i=n+1 then x else table(i)) = x)))} Since n< nmax impleis n+1 =< nmax, and the predicate, (exist i (1= (if i=n+1 then x else table(i)) = x)))} is satisfied by i=n+1, therefore, the precondition guarantees the desired postcondition.
Since n< nmax impleis n+1 =< nmax, and the predicate,
(exist i (1= (if i=n+1 then x else table(i)) = x)))} is satisfied by i=n+1, therefore, the precondition guarantees the desired postcondition.
is satisfied by i=n+1, therefore, the precondition guarantees the desired postcondition.
