YES(O(1), O(1)) 0.00/0.55 YES(O(1), O(1)) 0.00/0.56 0.00/0.56 0.00/0.56
0.00/0.56 0.00/0.560 CpxRelTRS0.00/0.56
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))0.00/0.56
↳2 CdtProblem0.00/0.56
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)0.00/0.56
↳4 CdtProblem0.00/0.56
↳5 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.56
↳6 BOUNDS(O(1), O(1))0.00/0.56
loop(Cons(x, xs), Nil, pp, ss) → False 0.00/0.56
loop(Cons(x', xs'), Cons(x, xs), pp, ss) → loop[Ite][False][Ite][False][Ite](!EQ(x', x), Cons(x', xs'), Cons(x, xs), pp, ss) 0.00/0.56
loop(Nil, s, pp, ss) → True 0.00/0.56
match1(p, s) → loop(p, s, p, s)
!EQ(S(x), S(y)) → !EQ(x, y) 0.00/0.56
!EQ(0, S(y)) → False 0.00/0.56
!EQ(S(x), 0) → False 0.00/0.56
!EQ(0, 0) → True
Tuples:
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 0.00/0.56
!EQ(0, S(z0)) → False 0.00/0.56
!EQ(S(z0), 0) → False 0.00/0.56
!EQ(0, 0) → True 0.00/0.56
loop(Cons(z0, z1), Nil, z2, z3) → False 0.00/0.56
loop(Cons(z0, z1), Cons(z2, z3), z4, z5) → loop[Ite][False][Ite][False][Ite](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5) 0.00/0.56
loop(Nil, z0, z1, z2) → True 0.00/0.56
match1(z0, z1) → loop(z0, z1, z0, z1)
S tuples:
!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 0.00/0.56
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c5(!EQ'(z0, z2)) 0.00/0.56
MATCH1(z0, z1) → c7(LOOP(z0, z1, z0, z1))
K tuples:none
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c5(!EQ'(z0, z2)) 0.00/0.56
MATCH1(z0, z1) → c7(LOOP(z0, z1, z0, z1))
loop, match1, !EQ
!EQ', LOOP, MATCH1
c, c5, c7
MATCH1(z0, z1) → c7(LOOP(z0, z1, z0, z1)) 0.00/0.56
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c5(!EQ'(z0, z2))
Tuples:
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 0.00/0.56
!EQ(0, S(z0)) → False 0.00/0.56
!EQ(S(z0), 0) → False 0.00/0.56
!EQ(0, 0) → True 0.00/0.56
loop(Cons(z0, z1), Nil, z2, z3) → False 0.00/0.56
loop(Cons(z0, z1), Cons(z2, z3), z4, z5) → loop[Ite][False][Ite][False][Ite](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5) 0.00/0.56
loop(Nil, z0, z1, z2) → True 0.00/0.56
match1(z0, z1) → loop(z0, z1, z0, z1)
S tuples:none
!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1))
loop, match1, !EQ
!EQ'
c