Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0 1

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura