FunExperiments 57 % timbuk --fung 30 mapPlus.txt

term height= 1

term height= 2

term height= 3

term height= 4

term height= 5
Rejected: 1

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
nil = nil
s(X) = s(X)
cons(X,Y) = cons(X,Y)
map = map
plus = plus
app(app(plus,o),X) = X
app(app(plus,s(X)),Y) = s(app(app(plus,X),Y))
app(app(map,F),nil) = nil
app(app(map,F),cons(X,Y)) = cons(app(F,X),app(app(map,F),Y))

Automaton projected on constructor terms:
-----------------------------------------
States q1 q46 q56 
Final States q1 
Transitions
o -> q56
cons(q46,q1) -> q1
nil -> q1
s(q46) -> q46
s(q56) -> q46

Regular expression:
-------------------
[cons([s(*|s(o))], *|nil)]

Step: 9


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.025032 seconds
Equation generation time: 0.081022 seconds

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