Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0 1 2

--------------------------- Ax
p(Y),X@p(X) --> p(Y),X#p(X)
--------------------------- R#
  p(Y),X@p(X) --> X#p(X)
  ---------------------- L@
    X@p(X) --> X#p(X)

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura