# Re: [isabelle] need help

`The correct way to formalise your system is by expressing the axiom in
``the form
`
[| B x False; S x |] ==> False

`in the first place. Then it looks like you would have nothing to do.
``As I mentioned earlier, we do not attempt to create complex formulas
``in the assumptions. In a formal sequent calculus this is simply
``impossible: the available rules only allow formulas to be broken down,
``not built up. (When used to construct a backward proof of course.)
`
Larry Paulson
On 1 Jul 2008, at 15:16, Erich Kummerfeld wrote:

`The trick I'm trying to accomplish with the first problem actually
``ties into
``the second problem I'm having. Basically I'm trying to solve [| B x
``False;
``S x |] ==> False by transforming it into [| B x False & S x |] ==>
``False and
``then using the axiom I mentioned earlier. Neither of these steps
``appears to
`work though and that's my confusion.

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*