Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0 1

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura