FunExperiments 296 % timbuk --fun 30 reverse.txt

term height= 1

term height= 2

term height= 3
Rejected: 6
term height= 4
Rejected: 570
term height= 5
Rejected: 660

Generated equations:
-------------------
cons(A,cons(Y,cons(A,X))) = cons(Y,cons(A,X))
cons(X,cons(B,cons(A,Y))) = cons(B,cons(A,Y))
cons(B,cons(Y,cons(B,X))) = cons(Y,cons(B,X))
cons(X,cons(A,cons(B,Y))) = cons(A,cons(B,Y))
cons(A,cons(A,X)) = cons(A,X)
cons(B,cons(B,X)) = cons(B,X)
sorted = sorted
B = B
app(X,Y) = app(X,Y)
nil = nil
A = A
true = true
geq = geq
rev = rev
cons(X,Y) = cons(X,Y)
false = false
append = append
leq = leq
ite = ite
app(app(append,nil),X) = X
app(app(append,cons(X,Y)),Z) = cons(X,app(app(append,Y),Z))
app(rev,nil) = nil
app(rev,cons(X,Y)) = app(app(append,app(rev,Y)),cons(X,nil))
app(app(leq,A),A) = true
app(app(leq,A),B) = true
app(app(leq,B),A) = false
app(app(leq,B),B) = true
app(app(geq,A),A) = true
app(app(geq,A),B) = false
app(app(geq,B),A) = true
app(app(geq,B),B) = true
app(app(sorted,P),nil) = true
app(app(sorted,P),cons(X,nil)) = true
app(app(sorted,P),cons(X,cons(Y,Z))) = app(app(app(ite,app(app(P,X),Y)),app(app(sorted,P),cons(Y,Z))),false)
app(app(app(ite,true),X),Y) = X
app(app(app(ite,false),X),Y) = Y

Automaton projected on constructor terms:
-----------------------------------------
States q91 
Final States q91 
Transitions
true -> q91

Regular expression:
-------------------
true

Step: 8


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.065906 seconds
Equation generation time: 20.106824 seconds

FunExperiments 297 % checker -fp comp.res
Post fixpoint : 
- R1*(Ainit) included in Acomp :	 OK