FunExperiments 168 % timbuk --fung 30 mapTree.txt 

term height= 1

term height= 2

term height= 3

term height= 4

term height= 5
Rejected: 3

Generated equations:
-------------------
Node(s(zero),Node(zero,Leaf,Leaf),Node(zero,Leaf,Leaf)) = Node(zero,Leaf,Leaf)
Node(s(zero),Node(zero,Leaf,Leaf),Leaf) = Node(zero,Leaf,Leaf)
Node(s(zero),Leaf,Node(zero,Leaf,Leaf)) = Node(zero,Leaf,Leaf)
Node(zero,Node(zero,Leaf,Leaf),Node(zero,Leaf,Leaf)) = Node(zero,Leaf,Leaf)
Node(zero,Node(zero,Leaf,Leaf),Leaf) = Node(zero,Leaf,Leaf)
Node(zero,Leaf,Node(zero,Leaf,Leaf)) = Node(zero,Leaf,Leaf)
Node(s(zero),Leaf,Leaf) = Leaf
s(s(zero)) = s(zero)
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 q10 q57 q71 
Final States q10 
Transitions
s(q57) -> q57
s(q71) -> q57
Node(q57,q10,q10) -> q10
Leaf -> q10
zero -> q71

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.031027 seconds
Equation generation time: 16.153995 seconds

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