FunExperiments 309 % timbuk --fun 30 foldRightMult2.txt 

term height= 1

term height= 2

term height= 3

term height= 4

term height= 5
Rejected: 6562
term height= 6
Rejected: 6567

Generated equations:
-------------------
cons(X,Y) = Y
s(s(s(X))) = X
app(X,Y) = app(X,Y)
forall = forall
o = o
nil = nil
mult = mult
s(X) = s(X)
true = true
cons(X,Y) = cons(X,Y)
foldR = foldR
false = false
map = map
leq = leq
ite = ite
plus = plus
app(app(app(foldR,F),nil),Acc) = Acc
app(app(app(foldR,F),cons(X,Y)),Acc) = app(app(F,X),app(app(app(foldR,F),Y),Acc))
app(app(plus,o),X) = X
app(app(plus,s(X)),Y) = s(app(app(plus,X),Y))
app(app(mult,o),X) = o
app(app(mult,s(X)),Y) = app(app(plus,Y),app(app(mult,X),Y))

Automaton projected on constructor terms:
-----------------------------------------
States q13 q22 q52 
Final States q52 
Transitions
s(q13) -> q22
o -> q52
s(q22) -> q52
s(q52) -> q13

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

Step: 11


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 1.360896 seconds
Equation generation time: 310.287906 seconds

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