Sequent Prover (seqprover)

[Top page]

Trying to prove with threshold = 0

              --------- Ax                  --------- Ax
              p --> q,p                     p,q --> q
--------- Ax  ---------- L~   --------- Ax  ----------- L~
p --> p,p     p,~q --> p      p,q --> p     p,q,~q --> 
------------------------ L->  ------------------------- L->
     p,p-> ~q --> p                p,q,p-> ~q --> 
     --------------------------------------------- L->
                  p,p->q,p-> ~q --> 
                  ------------------ R~
                  p->q,p-> ~q --> ~p
                  ---------------------- R->
                  p-> ~q --> (p->q)-> ~p
                  -------------------------- R->
                   --> (p-> ~q)->(p->q)-> ~p

# Proved in 0 msec.