FunExperiments 275 % timbuk --fun 30 insertionSort.txt 

term height= 1

term height= 2

term height= 3

term height= 4
Rejected: 24
term height= 5
Rejected: 66

Generated equations:
-------------------
cons(A,cons(X,cons(A,F))) = cons(X,cons(A,F))
cons(B,cons(B,cons(X,F))) = cons(B,cons(X,F))
cons(F,cons(B,cons(A,X))) = cons(B,cons(A,X))
cons(A,cons(A,F)) = cons(A,F)
cons(B,nil) = nil
sorted = sorted
app(F,X) = app(F,X)
B = B
insert = insert
nil = nil
A = A
true = true
geq = geq
sort = sort
cons(F,X) = cons(F,X)
false = false
leq = leq
ite = ite
app(app(app(ite,true),X),Y) = X
app(app(app(ite,false),X),Y) = Y
app(app(leq,A),A) = true
app(app(leq,A),B) = true
app(app(leq,B),A) = false
app(app(leq,B),B) = true
app(app(geq,A),A) = true
app(app(geq,A),B) = false
app(app(geq,B),A) = true
app(app(geq,B),B) = true
app(app(app(insert,P),X),nil) = cons(X,nil)
app(app(app(insert,P),X),cons(Y,Z)) = app(app(app(ite,app(app(P,X),Y)),cons(X,cons(Y,Z))),cons(Y,app(app(app(insert,P),X),Z)))
app(app(sort,P),nil) = nil
app(app(sort,P),cons(X,Y)) = app(app(app(insert,P),X),app(app(sort,P),Y))
app(app(sorted,P),nil) = true
app(app(sorted,P),cons(X,nil)) = true
app(app(sorted,P),cons(X,cons(Y,Z))) = app(app(app(ite,app(app(P,X),Y)),app(app(sorted,P),cons(Y,Z))),false)

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

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

Step: 8


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.54207 seconds
Equation generation time: 1.116922 seconds

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