FunExperiments 190 % timbuk --fung 30 foldLeftPlus.txt 

term height= 1

term height= 2

term height= 3

term height= 4

term height= 5
Rejected: 9
term height= 6
Rejected: 11

Generated equations:
-------------------
cons(s(o),nil) = nil
cons(o,nil) = nil
s(s(o)) = o
app(X,Y) = app(X,Y)
o = o
filter = filter
nil = nil
even = even
mult = mult
s(X) = s(X)
true = true
foldL = foldL
cons(X,Y) = cons(X,Y)
false = false
odd = odd
plus = plus
app(app(app(foldL,F),Acc),nil) = Acc
app(app(app(foldL,F),Acc),cons(X,Y)) = app(app(app(foldL,F),app(app(F,Acc),X)),Y)
app(even,o) = true
app(odd,o) = false
app(even,s(X)) = app(odd,X)
app(odd,s(X)) = app(even,X)
app(app(plus,o),X) = X
app(app(plus,s(X)),Y) = s(app(app(plus,X),Y))

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

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

Step: 8


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.017088 seconds
Equation generation time: 0.218796 seconds

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