Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0

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

# Proved in 0 msec.

Trying to prove with threshold = 0

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura