# 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