# Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]

```Trying to prove with threshold = 0 1

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