FunExperiments 184 % timbuk --fung 30 foldRightMult.txt 

term height= 1

term height= 2

term height= 3

term height= 4
Rejected: 0

Generated equations:
-------------------
cons(s(o),nil) = nil
cons(o,nil) = nil
s(s(o)) = s(o)
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 q40 q42 
Final States q42 
Transitions
s(q40) -> q42
s(q42) -> q42
o -> q40

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

Step: 9


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.012172 seconds
Equation generation time: 0.002725 seconds

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