Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]

Trying to prove with threshold = 0 1

--------------------------- Ax     --------------------------- Ax
p(a) --> p(a),q,X#(p(X)->q)        p(b) --> p(b),q,X#(p(X)->q)
----------------------------- R->  ----------------------------- R->  ------------------------ Ax
--> p(a),p(a)->q,X#(p(X)->q)       --> p(b),p(b)->q,X#(p(X)->q)      p(Y),q --> q,X#(p(X)->q)
----------------------------- R#   ----------------------------- R#   ------------------------- R->
--> p(a),X#(p(X)->q)               --> p(b),X#(p(X)->q)          q --> p(Y)->q,X#(p(X)->q)
-------------------------------------------------------- R/\      ------------------------- R#
--> p(a)/\p(b),X#(p(X)->q)                             q --> X#(p(X)->q)
------------------------------------------------------------------------- L->
p(a)/\p(b)->q --> X#(p(X)->q)
--------------------------------- R->
--> (p(a)/\p(b)->q)->X#(p(X)->q)

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura