MAYBE 0.00/0.85 MAYBE 0.00/0.87 0.00/0.87 0.00/0.87
0.00/0.87 0.00/0.870 CpxTRS0.00/0.87
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.87
↳2 CdtProblem0.00/0.87
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.87
↳4 CdtProblem0.00/0.87
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication)0.00/0.87
↳6 CdtProblem0.00/0.87
equal0(Nil) → number42(Nil) 0.00/0.87
equal0(Cons(x, xs)) → equal0(Cons(x, xs)) 0.00/0.87
number42(x) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) 0.00/0.87
goal(x) → equal0(x)
Tuples:
equal0(Nil) → number42(Nil) 0.00/0.87
equal0(Cons(z0, z1)) → equal0(Cons(z0, z1)) 0.00/0.87
number42(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) 0.00/0.87
goal(z0) → equal0(z0)
S tuples:
EQUAL0(Nil) → c(NUMBER42(Nil)) 0.00/0.87
EQUAL0(Cons(z0, z1)) → c1(EQUAL0(Cons(z0, z1))) 0.00/0.87
GOAL(z0) → c3(EQUAL0(z0))
K tuples:none
EQUAL0(Nil) → c(NUMBER42(Nil)) 0.00/0.87
EQUAL0(Cons(z0, z1)) → c1(EQUAL0(Cons(z0, z1))) 0.00/0.87
GOAL(z0) → c3(EQUAL0(z0))
equal0, number42, goal
EQUAL0, GOAL
c, c1, c3
Tuples:
equal0(Nil) → number42(Nil) 0.00/0.87
equal0(Cons(z0, z1)) → equal0(Cons(z0, z1)) 0.00/0.87
number42(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) 0.00/0.87
goal(z0) → equal0(z0)
S tuples:
EQUAL0(Cons(z0, z1)) → c1(EQUAL0(Cons(z0, z1))) 0.00/0.87
GOAL(z0) → c3(EQUAL0(z0)) 0.00/0.87
EQUAL0(Nil) → c
K tuples:none
EQUAL0(Cons(z0, z1)) → c1(EQUAL0(Cons(z0, z1))) 0.00/0.87
GOAL(z0) → c3(EQUAL0(z0)) 0.00/0.87
EQUAL0(Nil) → c
equal0, number42, goal
EQUAL0, GOAL
c1, c3, c
Removed 1 trailing nodes:
GOAL(z0) → c3(EQUAL0(z0))
EQUAL0(Nil) → c
Tuples:
equal0(Nil) → number42(Nil) 0.00/0.87
equal0(Cons(z0, z1)) → equal0(Cons(z0, z1)) 0.00/0.87
number42(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) 0.00/0.87
goal(z0) → equal0(z0)
S tuples:
EQUAL0(Cons(z0, z1)) → c1(EQUAL0(Cons(z0, z1)))
K tuples:none
EQUAL0(Cons(z0, z1)) → c1(EQUAL0(Cons(z0, z1)))
equal0, number42, goal
EQUAL0
c1