Verify-guard-implication
Guard implication for memoize keyword :invoke
Examples:
(verify-guard-implication f g)
(verify-guard-implication f g
:hints (("Goal" :in-theory (enable nth))))
General Form:
(verify-guard-implication fn1 fn2 &key hints otf-flg)
where none of the arguments is evaluated. This macro creates a defthm event with :rule-classes nil, using :hints and
:otf-flg if provided. The formula of that event is generally an
implication formed from the guards of the two functions, but might be T,
as we now describe.
Let guard-fn1 be the guard for fn1, and let guard-fn2
be the result of substituting the formals of fn1 for the formals of
fn2 in the guard for fn2. If guard-fn1 tautologically implies
guard-fn2 (for example, the two are equal or guard-fn2 is 'T),
then the formula of the generated event is T. Otherwise, the formula is
(IMPLIES guard-fn1 guard-fn2).
Note that the formula might be unpleasant for a human to read, since
guard-fn1 and guard-fn2 are translated terms (see term).
