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