# Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]

```Trying to prove with threshold = 0

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

# Proved in 0 msec.

Trying to prove with threshold = 0

----------- Ax                  ----------- Ax
p,q,r --> q                     p,q,r --> r
--------- Ax  ------------ L/\  --------- Ax  ------------ L/\
p --> p,q     p,q/\r --> q      p --> p,r     p,q/\r --> r
-------------------------- L->  -------------------------- L->
p,p->q/\r --> q                 p,p->q/\r --> 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.
```

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura