Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0 1

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

# Proved in 0 msec.

Trying to prove with threshold = 0 1

-------------------------- Ax
X#p(X) --> X#p(X),X#X#p(X)
-------------------------- R#
   X#p(X) --> X#X#p(X)

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura