# Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]

```Trying to prove with threshold = 0 1

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

# Proved in 0 msec.

Trying to prove with threshold = 0 1

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

# Proved in 0 msec.
```

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura