When I execute:
a (REPEAT z_strip_tac
THEN POP_ASM_T ante_tac
ProofPower returns the following message:
:# :# Exception- Fail * the assumption list is empty [POP_ASM_T.9302] *
Exception+ Fail * the assumption list is empty [POP_ASM_T.9302] * raised
Is everything fine?
2009/3/24 Roger Bishop Jones <r...@rbjones.com>
> On Tuesday 24 March 2009 10:35:51 Artur Oliveira Gomes wrote:
> >The problem is: only for those cases,
> >what I choose as witness does not satisfy the predicate.
> Well, any sequence of length 1 (or zero?) does for the
> first case. Proof attached.
> If you still can't crack the other two send me your
> best attempt.
> Proofpower mailing list
Artur Oliveira Gomes
Proofpower mailing list