# Sequent Prover (seqprover)

Sequent:
Output style:

[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.
```

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura