Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0 1 2

------------------------------------------- Ax
p(Y1),p(X1) --> p(Z),p(X1),X#Y@(p(Y)->p(X))
-------------------------------------------- R->
p(X1) --> p(Z),p(Y1)->p(X1),X#Y@(p(Y)->p(X))
----------------------------------------------- R@
p(X1) --> p(Z),Y@(p(Y)->p(X1)),X#Y@(p(Y)->p(X))
----------------------------------------------- R#
        p(X1) --> p(Z),X#Y@(p(Y)->p(X))
        --------------------------------- R->
         --> p(X1)->p(Z),X#Y@(p(Y)->p(X))
        ------------------------------------ R@
         --> Y@(p(Y)->p(Z)),X#Y@(p(Y)->p(X))
        ------------------------------------ R#
                --> X#Y@(p(Y)->p(X))

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura