FunExperiments 14 % timbuk --fung 30 delete.txt

term height= 1

term height= 2

term height= 3
Rejected: 0

Generated equations:
-------------------
cons(A,cons(A,nil)) = cons(A,nil)
cons(B,cons(A,nil)) = cons(A,nil)
cons(B,nil) = nil
B = B
nil = nil
delete(X,Y) = delete(X,Y)
A = A
true = true
cons(X,Y) = cons(X,Y)
member(X,Y) = member(X,Y)
false = false
ite(X,Y,Z) = ite(X,Y,Z)
eq(X,Y) = eq(X,Y)
eq(A,A) = true
eq(A,B) = false
eq(B,A) = false
eq(B,B) = true
delete(X,nil) = nil
delete(X,cons(Y,Z)) = ite(eq(X,Y),delete(X,Z),cons(Y,delete(X,Z)))
ite(true,X,Y) = X
ite(false,X,Y) = Y
member(X,nil) = false
member(X,cons(Y,Z)) = ite(eq(X,Y),true,member(X,Z))

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

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

Step: 6


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.009471 seconds
Equation generation time: 0.005241 seconds

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