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

# Proved in 0 msec.

Trying to prove with threshold = 0

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura