Sequent Prover (seqprover)

Sequent:
Output style:

[Top page] 

Trying to prove with threshold = 0

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

# Proved in 0 msec.
Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura