FunExperiments 149 % timbuk --fung 30 filterEven.txt 

term height= 1

term height= 2

term height= 3

term height= 4
Rejected: 5
term height= 5
Rejected: 16
term height= 6
Rejected: 18

Generated equations:
-------------------
cons(s(o),cons(o,nil)) = cons(o,nil)
cons(o,cons(o,nil)) = cons(o,nil)
cons(s(o),nil) = nil
s(s(o)) = o
app(F,X) = app(F,X)
o = o
exists = exists
filter = filter
nil = nil
even = even
s(F) = s(F)
true = true
nz = nz
cons(F,X) = cons(F,X)
false = false
odd = odd
ite = ite
app(app(app(ite,true),X),Y) = X
app(app(app(ite,false),X),Y) = Y
app(even,o) = true
app(odd,o) = false
app(even,s(X)) = app(odd,X)
app(odd,s(X)) = app(even,X)
app(app(filter,X),nil) = nil
app(app(filter,X),cons(Y,Z)) = app(app(app(ite,app(X,Y)),cons(Y,app(app(filter,X),Z))),app(app(filter,X),Z))
app(app(exists,X),nil) = false
app(app(exists,X),cons(Y,Z)) = app(app(app(ite,app(X,Y)),true),app(app(exists,X),Z))

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

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

Step: 6


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.128868 seconds
Equation generation time: 1.161413 seconds

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