FunExperiments 181 % timbuk --fung 30 mapSquare.txt 

term height= 1

term height= 2

term height= 3

term height= 4

term height= 5

term height= 6
Rejected: 11

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

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

Step: 11


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.318737 seconds
Equation generation time: 4.251963 seconds

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