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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura