Result of llprover

You are the 92363-rd user of this script.
System:
Sequent:
Output Style:
Threshold value:

------------- Ax  ------------------- Ax
n(0) --> n(0)     n(s(0)) --> n(s(0))
------------------------------------- L->
   n(0)->n(s(0)),n(0) --> n(s(0))
   ------------------------------------- Lall
   all(X,n(X)->n(s(X))),n(0) --> n(s(0))
   -------------------------------------- L!  ------------------------- Ax
   !all(X,n(X)->n(s(X))),n(0) --> n(s(0))     n(s(s(0))) --> n(s(s(0)))
   -------------------------------------------------------------------- L->
      n(s(0))->n(s(s(0))),!all(X,n(X)->n(s(X))),n(0) --> n(s(s(0)))
      -------------------------------------------------------------- Lall
      all(X,n(X)->n(s(X))),!all(X,n(X)->n(s(X))),n(0) --> n(s(s(0)))
      --------------------------------------------------------------- L!
      !all(X,n(X)->n(s(X))),!all(X,n(X)->n(s(X))),n(0) --> n(s(s(0)))
      --------------------------------------------------------------- C!
                 !all(X,n(X)->n(s(X))),n(0) --> n(s(s(0)))
                 ------------------------------------------ L!
                 !all(X,n(X)->n(s(X))),!n(0) --> n(s(s(0)))

CPU Time = 20 msec.


Naoyuki Tamura