FunExperiments 33 % timbuk --fung 30 orderedTreeTraversal.txt 

term height= 1

term height= 2

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

Generated equations:
-------------------
cons(A,cons(A,cons(B,nil))) = cons(A,cons(B,nil))
cons(B,cons(A,cons(B,nil))) = cons(A,cons(B,nil))
cons(A,cons(A,nil)) = cons(A,nil)
cons(B,cons(A,nil)) = cons(A,nil)
cons(B,cons(B,nil)) = cons(B,nil)
Node(A,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(A,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(A,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(A,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(A,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(A,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(A,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Leaf) = Leaf
Node(A,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(A,Node(B,Node(A,Leaf,Leaf),Leaf),Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(A,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(A,Node(A,Leaf,Leaf),Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(A,Node(B,Leaf,Leaf),Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(A,Leaf,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(B,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(B,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(B,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(B,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(B,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(B,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(B,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Leaf) = Leaf
Node(B,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(B,Node(B,Node(A,Leaf,Leaf),Leaf),Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(B,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(B,Node(A,Leaf,Leaf),Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(B,Node(B,Leaf,Leaf),Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(B,Leaf,Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(A,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(A,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(A,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(A,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(A,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(A,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Leaf) = Leaf
Node(A,Node(B,Node(A,Leaf,Leaf),Leaf),Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(A,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(A,Node(A,Leaf,Leaf),Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(A,Node(B,Leaf,Leaf),Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(A,Leaf,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(B,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(B,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(B,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(B,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(B,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(B,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)),Leaf) = Leaf
Node(B,Node(B,Node(A,Leaf,Leaf),Leaf),Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(B,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(B,Node(A,Leaf,Leaf),Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(B,Node(B,Leaf,Leaf),Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(B,Leaf,Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))) = Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf))
Node(A,Node(B,Node(A,Leaf,Leaf),Leaf),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(A,Node(B,Node(A,Leaf,Leaf),Leaf),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(A,Node(B,Node(A,Leaf,Leaf),Leaf),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(A,Node(B,Node(A,Leaf,Leaf),Leaf),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(A,Node(B,Node(A,Leaf,Leaf),Leaf),Leaf) = Leaf
Node(A,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(A,Node(A,Leaf,Leaf),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(A,Node(B,Leaf,Leaf),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(A,Leaf,Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(B,Node(B,Node(A,Leaf,Leaf),Leaf),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(B,Node(B,Node(A,Leaf,Leaf),Leaf),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(B,Node(B,Node(A,Leaf,Leaf),Leaf),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(B,Node(B,Node(A,Leaf,Leaf),Leaf),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(B,Node(B,Node(A,Leaf,Leaf),Leaf),Leaf) = Leaf
Node(B,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(B,Node(A,Leaf,Leaf),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(B,Node(B,Leaf,Leaf),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(B,Leaf,Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(A,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(A,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(A,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(A,Node(A,Leaf,Node(B,Leaf,Leaf)),Leaf) = Leaf
Node(A,Node(A,Leaf,Leaf),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(A,Node(B,Leaf,Leaf),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(A,Leaf,Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(B,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(B,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(B,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(B,Node(A,Leaf,Node(B,Leaf,Leaf)),Leaf) = Leaf
Node(B,Node(A,Leaf,Leaf),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(B,Node(B,Leaf,Leaf),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(B,Leaf,Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(A,Node(A,Leaf,Leaf),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(A,Node(A,Leaf,Leaf),Leaf) = Node(A,Leaf,Leaf)
Node(A,Node(B,Leaf,Leaf),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(A,Leaf,Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(B,Node(A,Leaf,Leaf),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(B,Node(B,Leaf,Leaf),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(B,Leaf,Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(A,Node(B,Leaf,Leaf),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(A,Node(B,Leaf,Leaf),Leaf) = Leaf
Node(B,Node(B,Leaf,Leaf),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(B,Node(B,Leaf,Leaf),Leaf) = Node(B,Leaf,Leaf)
Node(B,Leaf,Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
sorted(U) = sorted(U)
B = B
nil = nil
A = A
true = true
Leaf = Leaf
cons(U,V) = cons(U,V)
false = false
Node(U,V,X) = Node(U,V,X)
traversalIn(U) = traversalIn(U)
leq(U,V) = leq(U,V)
append(U,V) = append(U,V)
ite(U,V,X) = ite(U,V,X)
traversalIn(Leaf) = nil
traversalIn(Node(Y,Z,U)) = append(traversalIn(Z),cons(Y,traversalIn(U)))
append(nil,X) = X
append(cons(X,Y),Z) = cons(X,append(Y,Z))
sorted(nil) = true
sorted(cons(X,nil)) = true
sorted(cons(X,cons(Y,Z))) = ite(leq(X,Y),sorted(cons(Y,Z)),false)
leq(A,B) = true
leq(A,A) = true
leq(B,A) = false
leq(B,B) = true
ite(true,X,Y) = X
ite(false,X,Y) = Y

Automaton projected on constructor terms:
-----------------------------------------
States q165 
Final States q165 
Transitions
true -> q165

Regular expression:
-------------------
true

Step: 7


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.133736 seconds
Equation generation time: 1.715227 seconds

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