Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0 1 2

                       ----------------------------------------------------- Ax  -------------------------------------------------------- Ax
                       n(0),n(s(0)),X@(n(X)->n(s(X))) --> n(s(0)),n(s(s(0)))     n(0),n(s(0)),n(s(s(0))),X@(n(X)->n(s(X))) --> n(s(s(0)))
                       ------------------------------------------------------------------------------------------------------------------ L->
                                               n(0),n(s(0)),n(s(0))->n(s(s(0))),X@(n(X)->n(s(X))) --> n(s(s(0)))
------------------------------------------ Ax  ----------------------------------------------------------------- L@
n(0),X@(n(X)->n(s(X))) --> n(0),n(s(s(0)))               n(0),n(s(0)),X@(n(X)->n(s(X))) --> n(s(s(0)))
------------------------------------------------------------------------------------------------------ L->
                         n(0),n(0)->n(s(0)),X@(n(X)->n(s(X))) --> n(s(s(0)))
                         --------------------------------------------------- L@
                                n(0),X@(n(X)->n(s(X))) --> n(s(s(0)))

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura