# Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]

```Trying to prove with threshold = 0

----------- Ax                  ----------- Ax
q,r --> p,q                     q,r --> p,r
--------- Ax  ------------ L/\  --------- Ax  ------------ L/\
p --> p,q     q/\r --> p,q      p --> p,r     q/\r --> p,r
-------------------------- L\/  -------------------------- L\/
p\/q/\r --> p,q                 p\/q/\r --> p,r
---------------- R\/            ---------------- R\/
p\/q/\r --> p\/q                p\/q/\r --> p\/r
------------------------------------------------ R/\
p\/q/\r --> (p\/q)/\p\/r

# Proved in 0 msec.

Trying to prove with threshold = 0

----------- Ax  ----------- Ax   ----------- Ax  ----------- Ax   ----------- Ax  ----------- Ax   ----------- Ax  ----------- Ax
p,p --> p,q     p,r --> p,q      q,p --> p,q     q,r --> p,q      p,p --> p,r     p,r --> p,r      q,p --> p,r     q,r --> p,r
--------------------------- L\/  --------------------------- L\/  --------------------------- L\/  --------------------------- L\/
p,p\/r --> p,q                   q,p\/r --> p,q                   p,p\/r --> p,r                   q,p\/r --> p,r
----------------------------------------------- L\/               ----------------------------------------------- L\/
p\/q,p\/r --> p,q                                                 p\/q,p\/r --> p,r
----------------------------------------------------------------------------------- R/\
p\/q,p\/r --> p,q/\r
--------------------- R\/
p\/q,p\/r --> p\/q/\r
------------------------ L/\
(p\/q)/\p\/r --> p\/q/\r

# Proved in 0 msec.
```

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura