FunExperiments 293 % timbuk --fun 30 mapTree2NoGen.txt
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)
Node(X,Y,Z) = Node(X,Y,Z)
Leaf = Leaf
map = map
app(X,Y) = app(X,Y)
zero = zero
s(X) = s(X)
member = member
true = true
false = false
ite = ite
or = or
plus = plus
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(member,X),Leaf) = false
app(app(member,X),Node(Y,Z,U)) = app(app(app(ite,app(app(eq,X),Y)),true),app(app(or,app(app(member,X),Z)),app(app(member,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))
#U(U,V) = #U(U,V)
#bot = #bot
#q0(U) = #q0(U)
#q1(U) = #q1(U)
#q2(U) = #q2(U)
#q3(U) = #q3(U)
#q4(U) = #q4(U)
#q5(U) = #q5(U)
#q6(U) = #q6(U)
#q7(U) = #q7(U)
#q8(U) = #q8(U)
#q9(U) = #q9(U)
#q10(U) = #q10(U)
#q11(U) = #q11(U)
#U(#q3(#X1),#bot) = #U(#q2(s(#X1)),#U(#q3(#X1),#bot))
#U(#q2(#X1),#bot) = #U(#q2(s(#X1)),#U(#q2(#X1),#bot))
#U(#q7(#X1),#q4(#X2)) = #U(#q6(app(#X1,#X2)),#U(#q7(#X1),#q4(#X2)))
#bot = #U(#bot,#q8(map))
#U(#q1(#X1),#bot) = #U(#q3(s(#X1)),#U(#q1(#X1),#bot))
#U(#q10(#X1),#q1(#X2)) = #U(#q7(app(#X1,#X2)),#U(#q10(#X1),#q1(#X2)))
#U(#q8(#X1),#q9(#X2)) = #U(#q5(app(#X1,#X2)),#U(#q8(#X1),#q9(#X2)))
#U(#q5(#X1),#q0(#X2)) = #U(#q4(app(#X1,#X2)),#U(#q5(#X1),#q0(#X2)))
#U(#q11(#X1),#q3(#X2)) = #U(#q9(app(#X1,#X2)),#U(#q11(#X1),#q3(#X2)))
#bot = #U(#bot,#q11(plus))
#bot = #U(#bot,#q0(Leaf))
#U(#q3(#X1),#U(#q0(#X2),#q0(#X3))) = #U(#q0(Node(#X1,#X2,#X3)),#U(#q3(#X1),#U(#q0(#X2),#q0(#X3))))
#U(#q2(#X1),#U(#q0(#X2),#q0(#X3))) = #U(#q0(Node(#X1,#X2,#X3)),#U(#q2(#X1),#U(#q0(#X2),#q0(#X3))))
#U(#q1(#X1),#U(#q0(#X2),#q0(#X3))) = #U(#q0(Node(#X1,#X2,#X3)),#U(#q1(#X1),#U(#q0(#X2),#q0(#X3))))
#bot = #U(#bot,#q1(zero))
#bot = #U(#bot,#q10(member))
#U(#X1,#X2) = #U(#X2,#X1)
#U(#X1,#U(#X2,#X3)) = #U(#U(#X1,#X2),#X3)
#U(#U(#X1,#X2),#X3) = #U(#X1,#U(#X2,#X3))
#U(#X1,#X2) = #X1
#U(#X1,#X2) = #X2

Completion step: 1
---------------------------------------------------------
New transitions: 15
New epsilon: 5



Completion step: 2
---------------------------------------------------------
New transitions: 9
New epsilon: 3



Completion step: 3
---------------------------------------------------------
New transitions: 27
New epsilon: 9



Completion step: 4
---------------------------------------------------------
New transitions: 3
New epsilon: 1



Completion step: 5
---------------------------------------------------------
New transitions: 6
New epsilon: 2



Completion step: 6
---------------------------------------------------------
New transitions: 16
New epsilon: 11



Completion step: 7
---------------------------------------------------------
New transitions: 39
New epsilon: 17



Completion step: 8
---------------------------------------------------------
New transitions: 0
New epsilon: 3



Completion step: 9
---------------------------------------------------------
New transitions: 0
New epsilon: 0



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

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

Step: 9


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.080221 seconds

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