FunExperiments 187 % timbuk --fung 30 foldRightMult2.txt

term height= 1

term height= 2

term height= 3

term height= 4

term height= 5
Rejected: 7
term height= 6
Rejected: 10

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

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

Step: 11


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.05685 seconds
Equation generation time: 0.298305 seconds

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