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