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
         ------------------ L/\
         p/\q,p->q->r --> r
         ------------------- R->
         p->q->r --> p/\q->r

# Proved in 0 msec.

Trying to prove with threshold = 0

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura