Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0

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

Trying to prove with threshold = 0

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura