Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0 1

--------------------------------- Ax    --------------------------------- Ax
p(Y),q(Y),X@(p(X)/\q(X)) --> p(Y)       p(Z),q(Z),X@(p(X)/\q(X)) --> q(Z)
---------------------------------- L/\  ---------------------------------- L/\
p(Y)/\q(Y),X@(p(X)/\q(X)) --> p(Y)      p(Z)/\q(Z),X@(p(X)/\q(X)) --> q(Z)
---------------------------------- L@   ---------------------------------- L@
     X@(p(X)/\q(X)) --> p(Y)                 X@(p(X)/\q(X)) --> q(Z)
     ------------------------- R@            ------------------------- R@
     X@(p(X)/\q(X)) --> X@p(X)               X@(p(X)/\q(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),X@p(X),X@q(X) --> p(Y)     X@p(X),q(Y),X@q(X) --> q(Y)
--------------------------- L@  --------------------------- L@
  X@p(X),X@q(X) --> p(Y)          X@p(X),X@q(X) --> q(Y)
  ------------------------------------------------------ R/\
               X@p(X),X@q(X) --> p(Y)/\q(Y)
               -------------------------------- R@
               X@p(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.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura