Thanks.
On 28/03/18 05:00, michael.norr...@data61.csiro.au wrote:
> I'm afraid there is no solution to this problem whereby automatic tools will
> make lots of progress. First order reasoners such as PROVE_TAC and METIS_TAC
> try to do a little in this area (converting lambda-expressions to
I'm afraid there is no solution to this problem whereby automatic tools will
make lots of progress. First order reasoners such as PROVE_TAC and METIS_TAC
try to do a little in this area (converting lambda-expressions to terms
involving combinators for example), but this only goes so far, and
Hello.
Metis can prove «(λx m. x ≤ m) = (λx m. x < SUC m)» using
arithmeticTheory.LESS_EQ_IFF_LESS_SUC, but if the left hand side and
right hand instead appear as the operands of a combination then it no
longer works. The same behavior applies to “PROVE_TAC”.
> TAC_PROOF (([], “(λx m. x ≤ m) =
