Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0

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

# Proved in 0 msec.

Trying to prove with threshold = 0

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura