FunExperiments 172 % timbuk --fung 30 incTree.txt

term height= 1

term height= 2

term height= 3
Rejected: 2
term height= 4
Rejected: 9
term height= 5
Rejected: 11

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)
s(U) = s(U)
true = true
Leaf = Leaf
member(U,V) = member(U,V)
false = false
Node(U,V,X) = Node(U,V,X)
inc(U) = inc(U)
ite(U,V,X) = ite(U,V,X)
or(U,V) = or(U,V)
eq(U,V) = eq(U,V)
zero = zero
inc(Leaf) = Leaf
inc(Node(X,Y,Z)) = Node(s(X),inc(Y),inc(Z))
member(X,Leaf) = false
member(X,Node(Y,Z,U)) = ite(eq(X,Y),true,or(member(X,Z),member(X,U)))
eq(zero,zero) = true
eq(zero,s(X)) = false
eq(s(X),zero) = false
eq(s(X),s(Y)) = eq(X,Y)
or(true,Y) = true
or(false,Y) = Y
ite(true,X,Y) = X
ite(false,X,Y) = Y

Automaton projected on constructor terms:
-----------------------------------------
States q47 
Final States q47 
Transitions
false -> q47

Regular expression:
-------------------
false

Step: 5


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.089423 seconds
Equation generation time: 1.051789 seconds

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