Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura