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),~p(Y),X#(~p(X))
------------------------- R#
    --> p(Y),X#(~p(X))
   --------------------- 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@
  X@p(X) --> p(Y)
  ----------------- L~
  X@p(X),~p(Y) --> 
  --------------------- 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