FunExperiments 289 % timbuk --fun 30 mapTree.txt 

term height= 1

term height= 2

term height= 3

term height= 4

term height= 5
Rejected: 505

Generated equations:
-------------------
Node(U,Node(zero,Y,X),V) = Node(zero,Y,X)
Node(U,V,Node(zero,Y,X)) = Node(zero,Y,X)
Node(s(U),Leaf,V) = V
Node(s(U),V,Leaf) = V
s(s(U)) = s(U)
app(U,V) = app(U,V)
s(U) = s(U)
true = true
Leaf = Leaf
map = map
false = false
Node(U,V,X) = Node(U,V,X)
ite = ite
or = or
plus = plus
eq = eq
zero = zero
app(app(map,X),Leaf) = Leaf
app(app(map,X),Node(Y,Z,U)) = Node(app(X,Y),app(app(map,X),Z),app(app(map,X),U))
app(app(eq,zero),zero) = true
app(app(eq,zero),s(X)) = false
app(app(eq,s(X)),zero) = false
app(app(eq,s(X)),s(Y)) = app(app(eq,X),Y)
app(app(or,true),Y) = true
app(app(or,false),Y) = Y
app(app(app(ite,true),X),Y) = X
app(app(app(ite,false),X),Y) = Y
app(app(plus,zero),X) = X
app(app(plus,s(X)),Y) = s(app(app(plus,X),Y))

Automaton projected on constructor terms:
-----------------------------------------
States q52 q55 q69 
Final States q52 
Transitions
Node(q55,q52,q52) -> q52
Leaf -> q52
s(q55) -> q55
s(q69) -> q55
zero -> q69

Regular expression:
-------------------
[Node([s(*|s(zero))], *|Leaf, *|Leaf)]

Step: 9


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.046675 seconds
Equation generation time: 270.373692 seconds

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