Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0 1

                                        ----------------------------------- Ax
                                        q(Y),p(Y) --> q(Y),X#(p(X)/\ ~q(X))
----------------------------------- Ax  ------------------------------------ R~
p(Y) --> q(Y),p(Y),X#(p(X)/\ ~q(X))     p(Y) --> q(Y),~q(Y),X#(p(X)/\ ~q(X))
---------------------------------------------------------------------------- R/\
                p(Y) --> q(Y),p(Y)/\ ~q(Y),X#(p(X)/\ ~q(X))
                ------------------------------------------- R#
                      p(Y) --> q(Y),X#(p(X)/\ ~q(X))
                      -------------------------------- R->
                       --> p(Y)->q(Y),X#(p(X)/\ ~q(X))
                      ------------------------------------ R@
                       --> X@(p(X)->q(X)),X#(p(X)/\ ~q(X))
                      ------------------------------------ L~
                      ~X@(p(X)->q(X)) --> X#(p(X)/\ ~q(X))

# Proved in 0 msec.

Trying to prove with threshold = 0 1

--------------------------------- Ax  --------------------------------- Ax
X@(p(X)->q(X)),p(Y) --> p(Y),q(Y)     q(Y),X@(p(X)->q(X)),p(Y) --> q(Y)
----------------------------------------------------------------------- L->
                p(Y)->q(Y),X@(p(X)->q(X)),p(Y) --> q(Y)
                --------------------------------------- L@
                     X@(p(X)->q(X)),p(Y) --> q(Y)
                     ------------------------------ L~
                     X@(p(X)->q(X)),p(Y),~q(Y) --> 
                     -------------------------------- L/\
                     X@(p(X)->q(X)),p(Y)/\ ~q(Y) --> 
                     ------------------------------------ L#
                     X@(p(X)->q(X)),X#(p(X)/\ ~q(X)) --> 
                     ------------------------------------ R~
                     X#(p(X)/\ ~q(X)) --> ~X@(p(X)->q(X))

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura