Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0 1 2

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura