Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura