FunExperiments 164 % timbuk --fung 30 filterNz.txt 

term height= 1

term height= 2

term height= 3

term height= 4
Rejected: 5
term height= 5
Rejected: 7

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)) = s(o)
app(X,Y) = app(X,Y)
o = o
filter = filter
nil = nil
s(X) = s(X)
true = true
nz = nz
cons(X,Y) = cons(X,Y)
false = false
forAll = forAll
ite = ite
app(app(app(ite,true),X),Y) = X
app(app(app(ite,false),X),Y) = Y
app(nz,o) = false
app(nz,s(X)) = true
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(forAll,X),nil) = true
app(app(forAll,X),cons(Y,Z)) = app(app(app(ite,app(X,Y)),app(app(forAll,X),Z)),false)

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

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

Step: 6


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.01949 seconds
Equation generation time: 0.116683 seconds

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