Sequent Prover (seqprover)

[Top page]

Trying to prove with threshold = 0 1

--------------------------- Ax  --------------------------- Ax
p(Y) --> p(Y),X#p(X),X#q(X)     q(Y) --> X#p(X),q(Y),X#q(X)
--------------------------- R#  --------------------------- R#
  p(Y) --> X#p(X),X#q(X)          q(Y) --> X#p(X),X#q(X)
  ------------------------------------------------------ L\/
               p(Y)\/q(Y) --> X#p(X),X#q(X)
               -------------------------------- L#
               X#(p(X)\/q(X)) --> X#p(X),X#q(X)
               --------------------------------- R\/
               X#(p(X)\/q(X)) --> X#p(X)\/X#q(X)

# Proved in 0 msec.

Trying to prove with threshold = 0 1

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

# Proved in 0 msec.