FunExperiments 3 % timbuk --fung 100 experiments/split.txt

term height= 1

term height= 2

term height= 3
Rejected: 2
term height= 4
Rejected: 5
term height= 5
Rejected: 16
term height= 6
Rejected: 21
term height= 7
Rejected: 44
term height= 8
Rejected: 51
term height= 9
Rejected: 61Finite compRejected: 70Finite completion timeoRejectRejecteRejected: 87Finite completRejected: 105Finite completion timeoutFinite completion timeout
term height= 10
Finite completion timeoutFinite completion timeoutFinite completion timeoutFinite completion timeoutFinite completion timeoutFinite completion timeoutFinite completion timeoutFinite completion timeoutFinite completion timeoutFinite completion timeoutFinite comRejected: 106Finite completion timeoutFinite completion timeoutFinite completion timeoutFinite completion timeoutFinite completion timeoutFinite completion timeoutFinite completion timeoutFinite completion timeoutFinite completion timeoutFinite completion timRejected: 114Finite completion timeout
term height= 11
Rejected: 122

Generated equations:
-------------------
cons(A,cons(B,cons(A,cons(B,nil)))) = cons(A,cons(B,nil))
cons(B,cons(B,cons(A,cons(B,nil)))) = cons(B,cons(A,cons(B,nil)))
cons(A,cons(A,cons(B,nil))) = cons(A,cons(B,nil))
cons(A,cons(B,cons(B,nil))) = cons(B,cons(B,nil))
cons(B,cons(B,cons(B,nil))) = cons(B,cons(B,nil))
cons(A,cons(A,nil)) = cons(A,nil)
cons(B,cons(A,nil)) = cons(A,nil)
B = B
nil = nil
let2(X,Y,Z) = let2(X,Y,Z)
and(X,Y) = and(X,Y)
A = A
not(X) = not(X)
true = true
member(X,Y) = member(X,Y)
cons(X,Y) = cons(X,Y)
false = false
split(X) = split(X)
pair(X,Y) = pair(X,Y)
ite(X,Y,Z) = ite(X,Y,Z)
let3(X,Y) = let3(X,Y)
eq(X,Y) = eq(X,Y)
let1(X,Y,Z) = let1(X,Y,Z)
ite(true,X,Y) = X
ite(false,X,Y) = Y
member(X,nil) = false
member(X,cons(Y,Z)) = ite(eq(X,Y),true,member(X,Z))
eq(A,A) = true
eq(A,B) = false
eq(B,A) = false
eq(B,B) = true
split(nil) = pair(nil,nil)
split(cons(X,nil)) = pair(cons(X,nil),nil)
split(cons(X,cons(Y,Z))) = let1(X,Y,split(Z))
let1(X,Y,pair(Z,U)) = pair(cons(X,Z),cons(Y,U))
and(true,X) = X
and(false,X) = false
not(true) = false
not(false) = true
let2(X,Y,pair(Z,U)) = and(not(member(X,Z)),not(member(Y,U)))
let3(X,pair(Z,U)) = member(X,Z)

Completed automaton:
--------------------
States q1 q4 q7 q10 q13 q16 q23 q26 q42 q47 q52 q58 
Final States q52 
Transitions
cons(q4,q1) -> q42
cons(q4,q42) -> q42
cons(q7,q1) -> q10
nil -> q1
cons(q7,q16) -> q26
split(q16) -> q23
pair(q42,q10) -> q23
pair(q42,q47) -> q23
let1(q4,q7,q13) -> q23
let1(q4,q7,q23) -> q23
cons(q7,q10) -> q47
cons(q7,q47) -> q47
let2(q7,q4,q13) -> q52
let2(q7,q4,q23) -> q52
and(q52,q52) -> q52
not(q58) -> q52
true -> q52
member(q4,q1) -> q58
member(q4,q10) -> q58
member(q4,q47) -> q58
member(q7,q1) -> q58
member(q7,q42) -> q58
false -> q58
ite(q58,q52,q58) -> q58
eq(q4,q7) -> q58
eq(q7,q4) -> q58
A -> q4
split(q1) -> q13
pair(q1,q1) -> q13
B -> q7
cons(q4,q10) -> q16
cons(q4,q26) -> q16

Automaton too big to produce the regular expression


Step: 10


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

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


Exported comp.res file
Exported comp.res.epsi file
Completion time: 403.554169 seconds
Equation generation time: 185.64601 seconds
FunExperiments 4 % checker  -fp comp.res
Post fixpoint : 
- R1*(Ainit) included in Acomp :	 OK