FunExperiments 271 % timbuk --fun 30 filterEven.txt 

term height= 1

term height= 2

term height= 3

term height= 4
Rejected: 71
term height= 5
Rejected: 934
term height= 6
Rejected: 953

Generated equations:
-------------------
cons(F,cons(o,X)) = cons(o,X)
cons(s(o),F) = F
s(s(F)) = F
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.068807 seconds
Equation generation time: 27.895985 seconds

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