Sequent Prover (seqprover)

[Top page]

Trying to prove with threshold = 0 1

--------------------------------- Ax  --------------------------------- Ax
q(Y),p(Y) --> p(Y),X#(p(X)/\q(X))     q(Y),p(Y) --> q(Y),X#(p(X)/\q(X))
----------------------------------------------------------------------- R/\
                q(Y),p(Y) --> p(Y)/\q(Y),X#(p(X)/\q(X))
                --------------------------------------- R#
                     q(Y),p(Y) --> X#(p(X)/\q(X))
                     ----------------------------- R~
                     p(Y) --> X#(p(X)/\q(X)),~q(Y)
                     -------------------------------- R->
                      --> X#(p(X)/\q(X)),p(Y)-> ~q(Y)
                     ------------------------------------ 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
                                        p(Y),q(Y),X@(p(X)-> ~q(X)) --> q(Y)
----------------------------------- Ax  ------------------------------------- L~
p(Y),q(Y),X@(p(X)-> ~q(X)) --> p(Y)     p(Y),q(Y),~q(Y),X@(p(X)-> ~q(X)) --> 
----------------------------------------------------------------------------- L->
                p(Y),q(Y),p(Y)-> ~q(Y),X@(p(X)-> ~q(X)) --> 
                -------------------------------------------- L@
                      p(Y),q(Y),X@(p(X)-> ~q(X)) --> 
                      -------------------------------- L/\
                      p(Y)/\q(Y),X@(p(X)-> ~q(X)) --> 
                      ------------------------------------ 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.