FunExperiments 138 % timbuk --fun 30 foldLeftSquare.txt

term height= 1

term height= 2

term height= 3

term height= 4

term height= 5
Rejected: 6555
term height= 6
Rejected: 6558

Generated equations:
-------------------
cons(X,Y) = Y
s(s(X)) = X
app(X,Y) = app(X,Y)
forall = forall
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: 1.449855 seconds
Equation generation time: 223.643728 seconds

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