Reading Timbuk's output

Here is the plus.txt specification.

Ops plus:0 s:1 o:0 app:2
Const s o
Vars X Y 

TRS R
  app(app(plus,o),X) -> X
  app(app(plus,s(X)),Y) -> s(app(app(plus,X),Y))

Automaton A1
States qf qp qp2 qi qnz
Final States qf
Transitions
   app(qp,qi) -> qf
   app(qp2,qnz) -> qp
   plus -> qp2
   o -> qi
   s(qi) -> qi
   s(qi) -> qnz

Automaton TC
States qi
Final States qi
Transitions
   o -> qi
   s(qi) -> qi

Patterns
   o

If we run

timbuk --fung 10 plus.txt

we obtain the following output:

FunExperiments % timbuk --fung 30 plus.txt


term height= 1

term height= 2

term height= 3

term height= 4
Rejected: 0

Generated equations:
-------------------
s(s(o)) = s(o)
app(X,Y) = app(X,Y)
o = o
s(X) = s(X)
plus = plus
app(app(plus,o),X) = X
app(app(plus,s(X)),Y) = s(app(app(plus,X),Y))

Automaton projected on constructor terms:
-----------------------------------------
States q23 q28 
Final States q23 
Transitions
o -> q28
s(q23) -> q23
s(q28) -> q23

Regular expression:
-------------------
[s(*|s(o))]

Step: 7


Automaton complete!
------------------

Proof done!
-----------


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.007186 seconds
Equation generation time: 0.002898 seconds

where we can see the set of generated equations, the automaton projected on constructor terms (i.e. the aproximation of the result language of the function call), the same language expressed as a simplified regular expression (when it is possible to produce such an expression). Then, Step: 7 means that 7 steps of completion were necessary to complete the automaton. Finally Proof done! means that the terms declared in the Patterns section are not reachable, thus that our property is true. Finally Timbuk output several result files, in particular the comp.res file which contains every detail about the proof. This file is used by the checker to certify the result.