Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura