FunExperiments 207 % timbuk --fung 30 reverseFirstOrder2.txt

term height= 1

term height= 2

term height= 3
Rejected: 2
term height= 4
Rejected: 9
term height= 5
Rejected: 13

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
true = true
invsorted(X) = invsorted(X)
rev(X) = rev(X)
cons(X,Y) = cons(X,Y)
false = false
append(X,Y) = append(X,Y)
leq(X,Y) = leq(X,Y)
ite(X,Y,Z) = ite(X,Y,Z)
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))
leq(A,A) = true
leq(A,B) = true
leq(B,A) = false
leq(B,B) = true
invsorted(nil) = true
invsorted(cons(X,nil)) = true
invsorted(cons(X,cons(Y,Z))) = ite(leq(Y,X),invsorted(cons(Y,Z)),false)
ite(true,X,Y) = X
ite(false,X,Y) = Y

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

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

Step: 8


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.020086 seconds
Equation generation time: 0.132903 seconds

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