FunExperiments 300 % timbuk --fun 30 mapSquare.txt 

term height= 1

term height= 2

term height= 3

term height= 4

term height= 5

term height= 6
Rejected: 139

Generated equations:
-------------------
cons(X,cons(s(s(o)),Y)) = cons(s(s(o)),Y)
cons(s(o),cons(Y,X)) = cons(Y,X)
cons(o,cons(Y,X)) = cons(Y,X)
s(s(s(X))) = X
app(X,Y) = app(X,Y)
o = o
filter = filter
nil = nil
mult = mult
s(X) = s(X)
true = true
cons(X,Y) = cons(X,Y)
false = false
map = map
square = square
ite = ite
plus = plus
eq = eq
app(app(eq,o),o) = true
app(app(eq,s(X)),o) = false
app(app(eq,o),s(X)) = false
app(app(eq,s(X)),s(Y)) = app(app(eq,X),Y)
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))
app(app(app(ite,true),X),Y) = X
app(app(app(ite,false),X),Y) = Y
app(app(map,F),nil) = nil
app(app(map,F),cons(X,Y)) = cons(app(F,X),app(app(map,F),Y))
app(app(filter,X),nil) = nil
app(app(filter,X),cons(Y,Z)) = app(app(app(ite,app(X,Y)),cons(Y,app(app(filter,X),Z))),app(app(filter,X),Z))
app(square,X) = app(app(mult,X),X)

Automaton projected on constructor terms:
-----------------------------------------
States q154 
Final States q154 
Transitions
nil -> q154

Regular expression:
-------------------
nil

Step: 11


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.335872 seconds
Equation generation time: 24.925285 seconds

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