Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0 1

-------------------------- Ax
X@p(X),X@X@p(X) --> X@p(X)
-------------------------- L@
   X@X@p(X) --> X@p(X)

# Proved in 0 msec.

Trying to prove with threshold = 0 1

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura