On Tuesday 24 March 2009 05:07:09 Artur Oliveira Gomes wrote:
>I'm having hard times to achieve some proofs of preciondition
>and initialization using ProofPower.
>The file attached contains 3 examples that I still can not prove.
>If anyone could help me out with those proofs, I will be thankful.
Roger,
In the case of an existential with a schema as the
> signature the witness will usually be a binding
> display. So for each of your proofs you must
> come up with the binding display of a witness
> for your conjecture, i.e. a binding which satisfies
> the body of the existential, and then
Artur,
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
Roger,
When I execute:
a (REPEAT z_strip_tac
THEN POP_ASM_T ante_tac
THEN asm_rewrite_tac[]);
ProofPower returns the following message:
:# :# Exception- Fail * the assumption list is empty [POP_ASM_T.9302] *
raised
Exception+ Fail * the assumption list is empty [POP_ASM_T.9302]
