Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0

----------- Ax  ----------- Ax                   ----------- Ax  ----------- Ax
p --> p,p,s     p --> q,p,s                      p,q --> p,s     p,q --> q,s
--------------------------- R/\  ----------- Ax  --------------------------- R/\  ----------- Ax
      p --> p/\q,p,s             p,s --> p,s           p,q --> p/\q,s             p,q,s --> s
      -------------------------------------- L->       -------------------------------------- L->
                p,p/\q->s --> p,s                                p,q,p/\q->s --> s
                ------------------------------------------------------------------ L->
                                       p,p->q,p/\q->s --> s
                                       ------------------------- L/\
                                       p,(p->q)/\(p/\q->s) --> s
                                       -------------------------- L/\
                                       p/\(p->q)/\(p/\q->s) --> s
                                       ---------------------------- R->
                                        --> p/\(p->q)/\(p/\q->s)->s

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura