YES Time: 0.047529 TRS: { test(x_0, y) -> True(), test(x_0, y) -> False(), match_0(l1_2, l2_1, Nil()) -> l2_1, match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)), append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2), match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()), match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')), part(a_4, l_3) -> match_1(a_4, l_3, l_3), match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)), match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)), match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2), match_4(l_5, Nil()) -> Nil(), match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')), quick l_5 -> match_4(l_5, l_5), match_5(a, l', l_5, Pair(l1, l2)) -> append(quick l1, Cons(a, quick l2))} DP: DP: { match_0#(l1_2, l2_1, Cons(x, l)) -> append#(l, l2_1), append#(l1_2, l2_1) -> match_0#(l1_2, l2_1, l1_2), match_1#(a_4, l_3, Cons(x, l')) -> part#(a_4, l'), match_1#(a_4, l_3, Cons(x, l')) -> match_2#(x, l', a_4, l_3, part(a_4, l')), part#(a_4, l_3) -> match_1#(a_4, l_3, l_3), match_2#(x, l', a_4, l_3, Pair(l1, l2)) -> test#(a_4, x), match_2#(x, l', a_4, l_3, Pair(l1, l2)) -> match_3#(l1, l2, x, l', a_4, l_3, test(a_4, x)), match_4#(l_5, Cons(a, l')) -> part#(a, l'), match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l')), quick# l_5 -> match_4#(l_5, l_5), match_5#(a, l', l_5, Pair(l1, l2)) -> append#(quick l1, Cons(a, quick l2)), match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l1, match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l2} TRS: { test(x_0, y) -> True(), test(x_0, y) -> False(), match_0(l1_2, l2_1, Nil()) -> l2_1, match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)), append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2), match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()), match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')), part(a_4, l_3) -> match_1(a_4, l_3, l_3), match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)), match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)), match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2), match_4(l_5, Nil()) -> Nil(), match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')), quick l_5 -> match_4(l_5, l_5), match_5(a, l', l_5, Pair(l1, l2)) -> append(quick l1, Cons(a, quick l2))} UR: { test(x_0, y) -> True(), test(x_0, y) -> False(), match_0(l1_2, l2_1, Nil()) -> l2_1, match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)), append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2), match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()), match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')), part(a_4, l_3) -> match_1(a_4, l_3, l_3), match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)), match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)), match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2), match_4(l_5, Nil()) -> Nil(), match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')), quick l_5 -> match_4(l_5, l_5), match_5(a, l', l_5, Pair(l1, l2)) -> append(quick l1, Cons(a, quick l2)), a(z, w) -> z, a(z, w) -> w} EDG: {(match_5#(a, l', l_5, Pair(l1, l2)) -> append#(quick l1, Cons(a, quick l2)), append#(l1_2, l2_1) -> match_0#(l1_2, l2_1, l1_2)) (match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l2, quick# l_5 -> match_4#(l_5, l_5)) (match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l')), match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l2) (match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l')), match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l1) (match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l')), match_5#(a, l', l_5, Pair(l1, l2)) -> append#(quick l1, Cons(a, quick l2))) (match_4#(l_5, Cons(a, l')) -> part#(a, l'), part#(a_4, l_3) -> match_1#(a_4, l_3, l_3)) (part#(a_4, l_3) -> match_1#(a_4, l_3, l_3), match_1#(a_4, l_3, Cons(x, l')) -> part#(a_4, l')) (part#(a_4, l_3) -> match_1#(a_4, l_3, l_3), match_1#(a_4, l_3, Cons(x, l')) -> match_2#(x, l', a_4, l_3, part(a_4, l'))) (match_1#(a_4, l_3, Cons(x, l')) -> part#(a_4, l'), part#(a_4, l_3) -> match_1#(a_4, l_3, l_3)) (match_1#(a_4, l_3, Cons(x, l')) -> match_2#(x, l', a_4, l_3, part(a_4, l')), match_2#(x, l', a_4, l_3, Pair(l1, l2)) -> test#(a_4, x)) (match_1#(a_4, l_3, Cons(x, l')) -> match_2#(x, l', a_4, l_3, part(a_4, l')), match_2#(x, l', a_4, l_3, Pair(l1, l2)) -> match_3#(l1, l2, x, l', a_4, l_3, test(a_4, x))) (append#(l1_2, l2_1) -> match_0#(l1_2, l2_1, l1_2), match_0#(l1_2, l2_1, Cons(x, l)) -> append#(l, l2_1)) (match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l1, quick# l_5 -> match_4#(l_5, l_5)) (match_0#(l1_2, l2_1, Cons(x, l)) -> append#(l, l2_1), append#(l1_2, l2_1) -> match_0#(l1_2, l2_1, l1_2)) (quick# l_5 -> match_4#(l_5, l_5), match_4#(l_5, Cons(a, l')) -> part#(a, l')) (quick# l_5 -> match_4#(l_5, l_5), match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l')))} STATUS: arrows: 0.905325 SCCS (3): Scc: { match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l')), quick# l_5 -> match_4#(l_5, l_5), match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l1, match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l2} Scc: {match_0#(l1_2, l2_1, Cons(x, l)) -> append#(l, l2_1), append#(l1_2, l2_1) -> match_0#(l1_2, l2_1, l1_2)} Scc: {match_1#(a_4, l_3, Cons(x, l')) -> part#(a_4, l'), part#(a_4, l_3) -> match_1#(a_4, l_3, l_3)} SCC (4): Strict: { match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l')), quick# l_5 -> match_4#(l_5, l_5), match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l1, match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l2} Weak: { test(x_0, y) -> True(), test(x_0, y) -> False(), match_0(l1_2, l2_1, Nil()) -> l2_1, match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)), append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2), match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()), match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')), part(a_4, l_3) -> match_1(a_4, l_3, l_3), match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)), match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)), match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2), match_4(l_5, Nil()) -> Nil(), match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')), quick l_5 -> match_4(l_5, l_5), match_5(a, l', l_5, Pair(l1, l2)) -> append(quick l1, Cons(a, quick l2))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [match_3](x0, x1, x2, x3, x4, x5, x6) = x0 + x1 + 1, [match_2](x0, x1, x2, x3, x4) = x0 + 1, [match_5](x0, x1, x2, x3) = 0, [match_0](x0, x1, x2) = 0, [match_1](x0, x1, x2) = x0, [test](x0, x1) = 0, [append](x0, x1) = x0, [Cons](x0, x1) = x0 + 1, [part](x0, x1) = x0, [Pair](x0, x1) = x0 + x1, [match_4](x0, x1) = 0, [quick](x0) = 1, [True] = 0, [False] = 0, [Nil] = 0, [match_5#](x0, x1, x2, x3) = x0, [match_4#](x0, x1) = x0, [quick#](x0) = x0 Strict: match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l2 0 + 0l' + 1l1 + 1l2 + 0l_5 + 0a >= 0 + 1l2 match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l1 0 + 0l' + 1l1 + 1l2 + 0l_5 + 0a >= 0 + 1l1 quick# l_5 -> match_4#(l_5, l_5) 0 + 1l_5 >= 0 + 1l_5 match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l')) 1 + 1l' + 0l_5 + 0a >= 0 + 1l' + 0l_5 + 0a Weak: match_5(a, l', l_5, Pair(l1, l2)) -> append(quick l1, Cons(a, quick l2)) 0 + 0l' + 0l1 + 0l2 + 0l_5 + 0a >= 1 + 0l1 + 0l2 + 0a quick l_5 -> match_4(l_5, l_5) 1 + 0l_5 >= 0 + 0l_5 match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')) 0 + 0l' + 0l_5 + 0a >= 0 + 0l' + 0l_5 + 0a match_4(l_5, Nil()) -> Nil() 0 + 0l_5 >= 0 match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2) 1 + 0x + 0a_4 + 0l_3 + 0l' + 1l1 + 1l2 >= 1 + 0x + 1l1 + 1l2 match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)) 1 + 0x + 0a_4 + 0l_3 + 0l' + 1l1 + 1l2 >= 1 + 0x + 1l1 + 1l2 match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) 1 + 0x + 0a_4 + 0l_3 + 0l' + 1l1 + 1l2 >= 1 + 0x + 0a_4 + 0l_3 + 0l' + 1l1 + 1l2 part(a_4, l_3) -> match_1(a_4, l_3, l_3) 0 + 0a_4 + 1l_3 >= 0 + 0a_4 + 1l_3 match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')) 1 + 0x + 0a_4 + 0l_3 + 1l' >= 1 + 0x + 0a_4 + 0l_3 + 1l' match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()) 0 + 0a_4 + 0l_3 >= 0 append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2) 0 + 1l1_2 + 0l2_1 >= 0 + 0l1_2 + 0l2_1 match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)) 0 + 0l1_2 + 0l2_1 + 0x + 0l >= 1 + 0l2_1 + 0x + 1l match_0(l1_2, l2_1, Nil()) -> l2_1 0 + 0l1_2 + 0l2_1 >= 1l2_1 test(x_0, y) -> False() 0 + 0x_0 + 0y >= 0 test(x_0, y) -> True() 0 + 0x_0 + 0y >= 0 SCCS (0): SCC (2): Strict: {match_0#(l1_2, l2_1, Cons(x, l)) -> append#(l, l2_1), append#(l1_2, l2_1) -> match_0#(l1_2, l2_1, l1_2)} Weak: { test(x_0, y) -> True(), test(x_0, y) -> False(), match_0(l1_2, l2_1, Nil()) -> l2_1, match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)), append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2), match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()), match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')), part(a_4, l_3) -> match_1(a_4, l_3, l_3), match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)), match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)), match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2), match_4(l_5, Nil()) -> Nil(), match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')), quick l_5 -> match_4(l_5, l_5), match_5(a, l', l_5, Pair(l1, l2)) -> append(quick l1, Cons(a, quick l2))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [match_3](x0, x1, x2, x3, x4, x5, x6) = 0, [match_2](x0, x1, x2, x3, x4) = x0 + x1 + x2 + 1, [match_5](x0, x1, x2, x3) = 0, [match_0](x0, x1, x2) = x0 + x1 + 1, [match_1](x0, x1, x2) = x0 + x1 + 1, [test](x0, x1) = 0, [append](x0, x1) = 1, [Cons](x0, x1) = x0 + 1, [part](x0, x1) = x0 + x1 + 1, [Pair](x0, x1) = 0, [match_4](x0, x1) = x0 + x1 + 1, [quick](x0) = 0, [True] = 0, [False] = 0, [Nil] = 1, [match_0#](x0, x1, x2) = x0, [append#](x0, x1) = x0 Strict: append#(l1_2, l2_1) -> match_0#(l1_2, l2_1, l1_2) 0 + 1l1_2 + 0l2_1 >= 0 + 1l1_2 + 0l2_1 match_0#(l1_2, l2_1, Cons(x, l)) -> append#(l, l2_1) 1 + 0l1_2 + 0l2_1 + 0x + 1l >= 0 + 0l2_1 + 1l Weak: match_5(a, l', l_5, Pair(l1, l2)) -> append(quick l1, Cons(a, quick l2)) 0 + 0l' + 0l1 + 0l2 + 0l_5 + 0a >= 1 + 0l1 + 0l2 + 0a quick l_5 -> match_4(l_5, l_5) 0 + 0l_5 >= 1 + 2l_5 match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')) 2 + 1l' + 1l_5 + 0a >= 0 + 0l' + 0l_5 + 0a match_4(l_5, Nil()) -> Nil() 2 + 1l_5 >= 1 match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2) 0 + 0x + 0a_4 + 0l_3 + 0l' + 0l1 + 0l2 >= 0 + 0x + 0l1 + 0l2 match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)) 0 + 0x + 0a_4 + 0l_3 + 0l' + 0l1 + 0l2 >= 0 + 0x + 0l1 + 0l2 match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) 1 + 0x + 1a_4 + 0l_3 + 1l' + 0l1 + 0l2 >= 0 + 0x + 0a_4 + 0l_3 + 0l' + 0l1 + 0l2 part(a_4, l_3) -> match_1(a_4, l_3, l_3) 1 + 1a_4 + 1l_3 >= 1 + 0a_4 + 2l_3 match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')) 2 + 0x + 0a_4 + 1l_3 + 1l' >= 2 + 0x + 2a_4 + 0l_3 + 2l' match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()) 2 + 0a_4 + 1l_3 >= 0 append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2) 1 + 0l1_2 + 0l2_1 >= 1 + 2l1_2 + 0l2_1 match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)) 2 + 1l1_2 + 0l2_1 + 0x + 1l >= 2 + 0l2_1 + 0x + 0l match_0(l1_2, l2_1, Nil()) -> l2_1 2 + 1l1_2 + 0l2_1 >= 1l2_1 test(x_0, y) -> False() 0 + 0x_0 + 0y >= 0 test(x_0, y) -> True() 0 + 0x_0 + 0y >= 0 SCCS (0): SCC (2): Strict: {match_1#(a_4, l_3, Cons(x, l')) -> part#(a_4, l'), part#(a_4, l_3) -> match_1#(a_4, l_3, l_3)} Weak: { test(x_0, y) -> True(), test(x_0, y) -> False(), match_0(l1_2, l2_1, Nil()) -> l2_1, match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)), append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2), match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()), match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')), part(a_4, l_3) -> match_1(a_4, l_3, l_3), match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)), match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)), match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2), match_4(l_5, Nil()) -> Nil(), match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')), quick l_5 -> match_4(l_5, l_5), match_5(a, l', l_5, Pair(l1, l2)) -> append(quick l1, Cons(a, quick l2))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [match_3](x0, x1, x2, x3, x4, x5, x6) = 0, [match_2](x0, x1, x2, x3, x4) = x0 + x1 + x2 + 1, [match_5](x0, x1, x2, x3) = 0, [match_0](x0, x1, x2) = x0 + x1 + 1, [match_1](x0, x1, x2) = x0 + x1 + 1, [test](x0, x1) = 0, [append](x0, x1) = 1, [Cons](x0, x1) = x0 + 1, [part](x0, x1) = x0 + x1 + 1, [Pair](x0, x1) = 0, [match_4](x0, x1) = x0 + x1 + 1, [quick](x0) = 0, [True] = 0, [False] = 0, [Nil] = 1, [match_1#](x0, x1, x2) = x0, [part#](x0, x1) = x0 Strict: part#(a_4, l_3) -> match_1#(a_4, l_3, l_3) 0 + 0a_4 + 1l_3 >= 0 + 0a_4 + 1l_3 match_1#(a_4, l_3, Cons(x, l')) -> part#(a_4, l') 1 + 0x + 0a_4 + 0l_3 + 1l' >= 0 + 0a_4 + 1l' Weak: match_5(a, l', l_5, Pair(l1, l2)) -> append(quick l1, Cons(a, quick l2)) 0 + 0l' + 0l1 + 0l2 + 0l_5 + 0a >= 1 + 0l1 + 0l2 + 0a quick l_5 -> match_4(l_5, l_5) 0 + 0l_5 >= 1 + 2l_5 match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')) 2 + 1l' + 1l_5 + 0a >= 0 + 0l' + 0l_5 + 0a match_4(l_5, Nil()) -> Nil() 2 + 1l_5 >= 1 match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2) 0 + 0x + 0a_4 + 0l_3 + 0l' + 0l1 + 0l2 >= 0 + 0x + 0l1 + 0l2 match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)) 0 + 0x + 0a_4 + 0l_3 + 0l' + 0l1 + 0l2 >= 0 + 0x + 0l1 + 0l2 match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)) 1 + 0x + 1a_4 + 0l_3 + 1l' + 0l1 + 0l2 >= 0 + 0x + 0a_4 + 0l_3 + 0l' + 0l1 + 0l2 part(a_4, l_3) -> match_1(a_4, l_3, l_3) 1 + 1a_4 + 1l_3 >= 1 + 0a_4 + 2l_3 match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')) 2 + 0x + 0a_4 + 1l_3 + 1l' >= 2 + 0x + 2a_4 + 0l_3 + 2l' match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()) 2 + 0a_4 + 1l_3 >= 0 append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2) 1 + 0l1_2 + 0l2_1 >= 1 + 2l1_2 + 0l2_1 match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)) 2 + 1l1_2 + 0l2_1 + 0x + 1l >= 2 + 0l2_1 + 0x + 0l match_0(l1_2, l2_1, Nil()) -> l2_1 2 + 1l1_2 + 0l2_1 >= 1l2_1 test(x_0, y) -> False() 0 + 0x_0 + 0y >= 0 test(x_0, y) -> True() 0 + 0x_0 + 0y >= 0 SCCS (0):