FunExperiments 203 % timbuk --fung 30 reverseFirstOrder.txt

term height= 1

term height= 2
Rejected: 0
term height= 3
Rejected: 4
term height= 4
Rejected: 8

Generated equations:
-------------------
cons(A,cons(B,cons(A,nil))) = cons(B,cons(A,nil))
cons(B,cons(B,cons(A,nil))) = cons(B,cons(A,nil))
cons(A,cons(A,cons(B,nil))) = cons(A,cons(B,nil))
cons(B,cons(A,cons(B,nil))) = cons(A,cons(B,nil))
cons(A,cons(A,nil)) = cons(A,nil)
cons(B,cons(B,nil)) = cons(B,nil)
B = B
nil = nil
A = A
rev(X) = rev(X)
cons(X,Y) = cons(X,Y)
append(X,Y) = append(X,Y)
append(nil,X) = X
append(cons(X,Y),Z) = cons(X,append(Y,Z))
rev(nil) = nil
rev(cons(X,Y)) = append(rev(Y),cons(X,nil))

Automaton projected on constructor terms:
-----------------------------------------
States q1 q4 q7 q19 q28 q35 
Final States q1 q19 q28 q35 
Transitions
cons(q7,q1) -> q19
cons(q7,q19) -> q19
nil -> q1
cons(q4,q1) -> q28
cons(q4,q28) -> q28
A -> q4
B -> q7
cons(q7,q28) -> q35
cons(q7,q35) -> q35

Regular expression:
-------------------
((([cons(A, *|cons(A, nil))] | nil) | [cons(B, *|cons(B, nil))]) | [cons(B, *|cons(B, [cons(A, *|cons(A, nil))]))])

Step: 7


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.012621 seconds
Equation generation time: 0.032973 seconds

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