Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0 1

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

# Proved in 0 msec.

Trying to prove with threshold = 0 1

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura