Reading `comp.res` files

A typical comp.res file will be of the form:

% Completion time: 0.007028 seconds
% Equation generation time: :0.003262 seconds

Ops app:2 o:0 s:1 plus:0 

Const s o

Vars X Y 

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

Automaton Ainit
States q1 q4 q7 q12 q20 q23 
Final States q20 q23 
Transitions
plus -> q1
app(q12,q7) -> q23
app(q1,q7) -> q12
o -> q4
s(q4) -> q7
s(q7) -> q7
app(q12,q4) -> q20


Automaton Acomp
States q1 q12 q23 q27 q28 
Final States q19 q23 
Transitions
app(q1,q28) -> q27
app(q27,q28) -> q28
o -> q28
plus -> q1
app(q12,q23) -> q23
app(q12,q28) -> q23
app(q27,q23) -> q23
s(q23) -> q23
s(q28) -> q23
app(q1,q23) -> q12



Automaton AcompInterConst
States q23 q28 
Final States q23 
Transitions
o -> q28
s(q23) -> q23
s(q28) -> q23


Patterns
o

Equations Approx
Rules
s(s(X)) = s(X)
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))

where we find the same sections as in a specification file, except that: the automaton Ainit is a transformation of the initial automaton of the specification. The transformed automaton recognizes the same language as the initial tree automaton but is deterministic and satisfies the R/E coherence condition of completion. The automaton Acomp is the completed automaton and Approx is the set of generated equations. Those files can be certified by Coq automatically as follows.

Reading comp.res files

Reading `comp.res` files