YES
TRS:
 {           0(#()) -> #(),
          +(x, #()) -> x,
          +(#(), x) -> x,
      +(0(x), 0(y)) -> 0(+(x, y)),
      +(0(x), 1(y)) -> 1(+(x, y)),
      +(+(x, y), z) -> +(x, +(y, z)),
      +(1(x), 0(y)) -> 1(+(x, y)),
      +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
          -(x, #()) -> x,
          -(#(), x) -> #(),
      -(0(x), 0(y)) -> 0(-(x, y)),
      -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
      -(1(x), 0(y)) -> 1(-(x, y)),
      -(1(x), 1(y)) -> 0(-(x, y)),
       not(false()) -> true(),
        not(true()) -> false(),
  if(false(), x, y) -> y,
   if(true(), x, y) -> x,
         ge(x, #()) -> true(),
      ge(#(), 0(x)) -> ge(#(), x),
      ge(#(), 1(x)) -> false(),
     ge(0(x), 0(y)) -> ge(x, y),
     ge(0(x), 1(y)) -> not(ge(y, x)),
     ge(1(x), 0(y)) -> ge(x, y),
     ge(1(x), 1(y)) -> ge(x, y),
          log'(#()) -> #(),
         log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
         log'(1(x)) -> +(log'(x), 1(#())),
             log(x) -> -(log'(x), 1(#()))}
 DP:
  Strict:
   { +#(0(x), 0(y)) -> 0#(+(x, y)),
     +#(0(x), 0(y)) -> +#(x, y),
     +#(0(x), 1(y)) -> +#(x, y),
     +#(+(x, y), z) -> +#(x, +(y, z)),
     +#(+(x, y), z) -> +#(y, z),
     +#(1(x), 0(y)) -> +#(x, y),
     +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))),
     +#(1(x), 1(y)) -> +#(x, y),
     +#(1(x), 1(y)) -> +#(+(x, y), 1(#())),
     -#(0(x), 0(y)) -> 0#(-(x, y)),
     -#(0(x), 0(y)) -> -#(x, y),
     -#(0(x), 1(y)) -> -#(x, y),
     -#(0(x), 1(y)) -> -#(-(x, y), 1(#())),
     -#(1(x), 0(y)) -> -#(x, y),
     -#(1(x), 1(y)) -> 0#(-(x, y)),
     -#(1(x), 1(y)) -> -#(x, y),
     ge#(#(), 0(x)) -> ge#(#(), x),
    ge#(0(x), 0(y)) -> ge#(x, y),
    ge#(0(x), 1(y)) -> not#(ge(y, x)),
    ge#(0(x), 1(y)) -> ge#(y, x),
    ge#(1(x), 0(y)) -> ge#(x, y),
    ge#(1(x), 1(y)) -> ge#(x, y),
        log'#(0(x)) -> +#(log'(x), 1(#())),
        log'#(0(x)) -> if#(ge(x, 1(#())), +(log'(x), 1(#())), #()),
        log'#(0(x)) -> ge#(x, 1(#())),
        log'#(0(x)) -> log'#(x),
        log'#(1(x)) -> +#(log'(x), 1(#())),
        log'#(1(x)) -> log'#(x),
            log#(x) -> -#(log'(x), 1(#())),
            log#(x) -> log'#(x)}
  Weak:
  {           0(#()) -> #(),
           +(x, #()) -> x,
           +(#(), x) -> x,
       +(0(x), 0(y)) -> 0(+(x, y)),
       +(0(x), 1(y)) -> 1(+(x, y)),
       +(+(x, y), z) -> +(x, +(y, z)),
       +(1(x), 0(y)) -> 1(+(x, y)),
       +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
           -(x, #()) -> x,
           -(#(), x) -> #(),
       -(0(x), 0(y)) -> 0(-(x, y)),
       -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
       -(1(x), 0(y)) -> 1(-(x, y)),
       -(1(x), 1(y)) -> 0(-(x, y)),
        not(false()) -> true(),
         not(true()) -> false(),
   if(false(), x, y) -> y,
    if(true(), x, y) -> x,
          ge(x, #()) -> true(),
       ge(#(), 0(x)) -> ge(#(), x),
       ge(#(), 1(x)) -> false(),
      ge(0(x), 0(y)) -> ge(x, y),
      ge(0(x), 1(y)) -> not(ge(y, x)),
      ge(1(x), 0(y)) -> ge(x, y),
      ge(1(x), 1(y)) -> ge(x, y),
           log'(#()) -> #(),
          log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
          log'(1(x)) -> +(log'(x), 1(#())),
              log(x) -> -(log'(x), 1(#()))}
  EDG:
   {(+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(+(x, y), z) -> +#(y, z))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(0(x), 1(y)) -> +#(x, y))
    (log'#(0(x)) -> +#(log'(x), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (log'#(0(x)) -> +#(log'(x), 1(#())), +#(1(x), 1(y)) -> +#(x, y))
    (log'#(0(x)) -> +#(log'(x), 1(#())), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (log'#(0(x)) -> +#(log'(x), 1(#())), +#(+(x, y), z) -> +#(y, z))
    (log'#(0(x)) -> +#(log'(x), 1(#())), +#(+(x, y), z) -> +#(x, +(y, z)))
    (log'#(0(x)) -> +#(log'(x), 1(#())), +#(0(x), 1(y)) -> +#(x, y))
    (log'#(1(x)) -> +#(log'(x), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (log'#(1(x)) -> +#(log'(x), 1(#())), +#(1(x), 1(y)) -> +#(x, y))
    (log'#(1(x)) -> +#(log'(x), 1(#())), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (log'#(1(x)) -> +#(log'(x), 1(#())), +#(+(x, y), z) -> +#(y, z))
    (log'#(1(x)) -> +#(log'(x), 1(#())), +#(+(x, y), z) -> +#(x, +(y, z)))
    (log'#(1(x)) -> +#(log'(x), 1(#())), +#(0(x), 1(y)) -> +#(x, y))
    (log'#(0(x)) -> log'#(x), log'#(1(x)) -> log'#(x))
    (log'#(0(x)) -> log'#(x), log'#(1(x)) -> +#(log'(x), 1(#())))
    (log'#(0(x)) -> log'#(x), log'#(0(x)) -> log'#(x))
    (log'#(0(x)) -> log'#(x), log'#(0(x)) -> ge#(x, 1(#())))
    (log'#(0(x)) -> log'#(x), log'#(0(x)) -> if#(ge(x, 1(#())), +(log'(x), 1(#())), #()))
    (log'#(0(x)) -> log'#(x), log'#(0(x)) -> +#(log'(x), 1(#())))
    (log#(x) -> log'#(x), log'#(1(x)) -> log'#(x))
    (log#(x) -> log'#(x), log'#(1(x)) -> +#(log'(x), 1(#())))
    (log#(x) -> log'#(x), log'#(0(x)) -> log'#(x))
    (log#(x) -> log'#(x), log'#(0(x)) -> ge#(x, 1(#())))
    (log#(x) -> log'#(x), log'#(0(x)) -> if#(ge(x, 1(#())), +(log'(x), 1(#())), #()))
    (log#(x) -> log'#(x), log'#(0(x)) -> +#(log'(x), 1(#())))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(1(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (-#(0(x), 0(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y))
    (-#(0(x), 0(y)) -> -#(x, y), -#(1(x), 1(y)) -> 0#(-(x, y)))
    (-#(0(x), 0(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y))
    (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
    (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y))
    (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y))
    (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> 0#(-(x, y)))
    (-#(1(x), 0(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y))
    (-#(1(x), 0(y)) -> -#(x, y), -#(1(x), 1(y)) -> 0#(-(x, y)))
    (-#(1(x), 0(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y))
    (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
    (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y))
    (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y))
    (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> 0#(-(x, y)))
    (ge#(0(x), 0(y)) -> ge#(x, y), ge#(1(x), 1(y)) -> ge#(x, y))
    (ge#(0(x), 0(y)) -> ge#(x, y), ge#(1(x), 0(y)) -> ge#(x, y))
    (ge#(0(x), 0(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> ge#(y, x))
    (ge#(0(x), 0(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> not#(ge(y, x)))
    (ge#(0(x), 0(y)) -> ge#(x, y), ge#(0(x), 0(y)) -> ge#(x, y))
    (ge#(0(x), 0(y)) -> ge#(x, y), ge#(#(), 0(x)) -> ge#(#(), x))
    (ge#(1(x), 1(y)) -> ge#(x, y), ge#(1(x), 1(y)) -> ge#(x, y))
    (ge#(1(x), 1(y)) -> ge#(x, y), ge#(1(x), 0(y)) -> ge#(x, y))
    (ge#(1(x), 1(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> ge#(y, x))
    (ge#(1(x), 1(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> not#(ge(y, x)))
    (ge#(1(x), 1(y)) -> ge#(x, y), ge#(0(x), 0(y)) -> ge#(x, y))
    (ge#(1(x), 1(y)) -> ge#(x, y), ge#(#(), 0(x)) -> ge#(#(), x))
    (ge#(0(x), 1(y)) -> ge#(y, x), ge#(#(), 0(x)) -> ge#(#(), x))
    (ge#(0(x), 1(y)) -> ge#(y, x), ge#(0(x), 0(y)) -> ge#(x, y))
    (ge#(0(x), 1(y)) -> ge#(y, x), ge#(0(x), 1(y)) -> not#(ge(y, x)))
    (ge#(0(x), 1(y)) -> ge#(y, x), ge#(0(x), 1(y)) -> ge#(y, x))
    (ge#(0(x), 1(y)) -> ge#(y, x), ge#(1(x), 0(y)) -> ge#(x, y))
    (ge#(0(x), 1(y)) -> ge#(y, x), ge#(1(x), 1(y)) -> ge#(x, y))
    (ge#(1(x), 0(y)) -> ge#(x, y), ge#(#(), 0(x)) -> ge#(#(), x))
    (ge#(1(x), 0(y)) -> ge#(x, y), ge#(0(x), 0(y)) -> ge#(x, y))
    (ge#(1(x), 0(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> not#(ge(y, x)))
    (ge#(1(x), 0(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> ge#(y, x))
    (ge#(1(x), 0(y)) -> ge#(x, y), ge#(1(x), 0(y)) -> ge#(x, y))
    (ge#(1(x), 0(y)) -> ge#(x, y), ge#(1(x), 1(y)) -> ge#(x, y))
    (-#(1(x), 1(y)) -> -#(x, y), -#(0(x), 0(y)) -> 0#(-(x, y)))
    (-#(1(x), 1(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y))
    (-#(1(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y))
    (-#(1(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
    (-#(1(x), 1(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y))
    (-#(1(x), 1(y)) -> -#(x, y), -#(1(x), 1(y)) -> 0#(-(x, y)))
    (-#(1(x), 1(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y))
    (-#(0(x), 1(y)) -> -#(x, y), -#(0(x), 0(y)) -> 0#(-(x, y)))
    (-#(0(x), 1(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y))
    (-#(0(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y))
    (-#(0(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
    (-#(0(x), 1(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y))
    (-#(0(x), 1(y)) -> -#(x, y), -#(1(x), 1(y)) -> 0#(-(x, y)))
    (-#(0(x), 1(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(1(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(0(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(+(x, y), z) -> +#(y, z), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(+(x, y), z) -> +#(y, z), +#(0(x), 0(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(0(x), 1(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
    (+#(+(x, y), z) -> +#(y, z), +#(1(x), 0(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (log'#(1(x)) -> log'#(x), log'#(0(x)) -> +#(log'(x), 1(#())))
    (log'#(1(x)) -> log'#(x), log'#(0(x)) -> if#(ge(x, 1(#())), +(log'(x), 1(#())), #()))
    (log'#(1(x)) -> log'#(x), log'#(0(x)) -> ge#(x, 1(#())))
    (log'#(1(x)) -> log'#(x), log'#(0(x)) -> log'#(x))
    (log'#(1(x)) -> log'#(x), log'#(1(x)) -> +#(log'(x), 1(#())))
    (log'#(1(x)) -> log'#(x), log'#(1(x)) -> log'#(x))
    (ge#(#(), 0(x)) -> ge#(#(), x), ge#(#(), 0(x)) -> ge#(#(), x))
    (log#(x) -> -#(log'(x), 1(#())), -#(0(x), 1(y)) -> -#(x, y))
    (log#(x) -> -#(log'(x), 1(#())), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
    (log#(x) -> -#(log'(x), 1(#())), -#(1(x), 1(y)) -> 0#(-(x, y)))
    (log#(x) -> -#(log'(x), 1(#())), -#(1(x), 1(y)) -> -#(x, y))
    (log'#(0(x)) -> ge#(x, 1(#())), ge#(0(x), 1(y)) -> not#(ge(y, x)))
    (log'#(0(x)) -> ge#(x, 1(#())), ge#(0(x), 1(y)) -> ge#(y, x))
    (log'#(0(x)) -> ge#(x, 1(#())), ge#(1(x), 1(y)) -> ge#(x, y))
    (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(0(x), 1(y)) -> -#(x, y))
    (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
    (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(1(x), 1(y)) -> 0#(-(x, y)))
    (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(1(x), 1(y)) -> -#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 0(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 1(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 0(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))}
   SCCS:
    Scc:
     {log'#(0(x)) -> log'#(x),
      log'#(1(x)) -> log'#(x)}
    Scc:
     {ge#(0(x), 0(y)) -> ge#(x, y),
      ge#(0(x), 1(y)) -> ge#(y, x),
      ge#(1(x), 0(y)) -> ge#(x, y),
      ge#(1(x), 1(y)) -> ge#(x, y)}
    Scc:
     {ge#(#(), 0(x)) -> ge#(#(), x)}
    Scc:
     {-#(0(x), 0(y)) -> -#(x, y),
      -#(0(x), 1(y)) -> -#(x, y),
      -#(0(x), 1(y)) -> -#(-(x, y), 1(#())),
      -#(1(x), 0(y)) -> -#(x, y),
      -#(1(x), 1(y)) -> -#(x, y)}
    Scc:
     {+#(0(x), 0(y)) -> +#(x, y),
      +#(0(x), 1(y)) -> +#(x, y),
      +#(+(x, y), z) -> +#(x, +(y, z)),
      +#(+(x, y), z) -> +#(y, z),
      +#(1(x), 0(y)) -> +#(x, y),
      +#(1(x), 1(y)) -> +#(x, y),
      +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
    SCC:
     Strict:
      {log'#(0(x)) -> log'#(x),
       log'#(1(x)) -> log'#(x)}
     Weak:
     {           0(#()) -> #(),
              +(x, #()) -> x,
              +(#(), x) -> x,
          +(0(x), 0(y)) -> 0(+(x, y)),
          +(0(x), 1(y)) -> 1(+(x, y)),
          +(+(x, y), z) -> +(x, +(y, z)),
          +(1(x), 0(y)) -> 1(+(x, y)),
          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
              -(x, #()) -> x,
              -(#(), x) -> #(),
          -(0(x), 0(y)) -> 0(-(x, y)),
          -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
          -(1(x), 0(y)) -> 1(-(x, y)),
          -(1(x), 1(y)) -> 0(-(x, y)),
           not(false()) -> true(),
            not(true()) -> false(),
      if(false(), x, y) -> y,
       if(true(), x, y) -> x,
             ge(x, #()) -> true(),
          ge(#(), 0(x)) -> ge(#(), x),
          ge(#(), 1(x)) -> false(),
         ge(0(x), 0(y)) -> ge(x, y),
         ge(0(x), 1(y)) -> not(ge(y, x)),
         ge(1(x), 0(y)) -> ge(x, y),
         ge(1(x), 1(y)) -> ge(x, y),
              log'(#()) -> #(),
             log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
             log'(1(x)) -> +(log'(x), 1(#())),
                 log(x) -> -(log'(x), 1(#()))}
     SPSC:
      Simple Projection:
       pi(log'#) = 0
      Strict:
       {log'#(1(x)) -> log'#(x)}
      EDG:
       {(log'#(1(x)) -> log'#(x), log'#(1(x)) -> log'#(x))}
       SCCS:
        Scc:
         {log'#(1(x)) -> log'#(x)}
        SCC:
         Strict:
          {log'#(1(x)) -> log'#(x)}
         Weak:
         {           0(#()) -> #(),
                  +(x, #()) -> x,
                  +(#(), x) -> x,
              +(0(x), 0(y)) -> 0(+(x, y)),
              +(0(x), 1(y)) -> 1(+(x, y)),
              +(+(x, y), z) -> +(x, +(y, z)),
              +(1(x), 0(y)) -> 1(+(x, y)),
              +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                  -(x, #()) -> x,
                  -(#(), x) -> #(),
              -(0(x), 0(y)) -> 0(-(x, y)),
              -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
              -(1(x), 0(y)) -> 1(-(x, y)),
              -(1(x), 1(y)) -> 0(-(x, y)),
               not(false()) -> true(),
                not(true()) -> false(),
          if(false(), x, y) -> y,
           if(true(), x, y) -> x,
                 ge(x, #()) -> true(),
              ge(#(), 0(x)) -> ge(#(), x),
              ge(#(), 1(x)) -> false(),
             ge(0(x), 0(y)) -> ge(x, y),
             ge(0(x), 1(y)) -> not(ge(y, x)),
             ge(1(x), 0(y)) -> ge(x, y),
             ge(1(x), 1(y)) -> ge(x, y),
                  log'(#()) -> #(),
                 log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
                 log'(1(x)) -> +(log'(x), 1(#())),
                     log(x) -> -(log'(x), 1(#()))}
         SPSC:
          Simple Projection:
           pi(log'#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {ge#(0(x), 0(y)) -> ge#(x, y),
       ge#(0(x), 1(y)) -> ge#(y, x),
       ge#(1(x), 0(y)) -> ge#(x, y),
       ge#(1(x), 1(y)) -> ge#(x, y)}
     Weak:
     {           0(#()) -> #(),
              +(x, #()) -> x,
              +(#(), x) -> x,
          +(0(x), 0(y)) -> 0(+(x, y)),
          +(0(x), 1(y)) -> 1(+(x, y)),
          +(+(x, y), z) -> +(x, +(y, z)),
          +(1(x), 0(y)) -> 1(+(x, y)),
          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
              -(x, #()) -> x,
              -(#(), x) -> #(),
          -(0(x), 0(y)) -> 0(-(x, y)),
          -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
          -(1(x), 0(y)) -> 1(-(x, y)),
          -(1(x), 1(y)) -> 0(-(x, y)),
           not(false()) -> true(),
            not(true()) -> false(),
      if(false(), x, y) -> y,
       if(true(), x, y) -> x,
             ge(x, #()) -> true(),
          ge(#(), 0(x)) -> ge(#(), x),
          ge(#(), 1(x)) -> false(),
         ge(0(x), 0(y)) -> ge(x, y),
         ge(0(x), 1(y)) -> not(ge(y, x)),
         ge(1(x), 0(y)) -> ge(x, y),
         ge(1(x), 1(y)) -> ge(x, y),
              log'(#()) -> #(),
             log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
             log'(1(x)) -> +(log'(x), 1(#())),
                 log(x) -> -(log'(x), 1(#()))}
     POLY:
      Argument Filtering:
       pi(log) = [], pi(log') = [], pi(ge#) = [0,1], pi(ge) = [], pi(if) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(-) = [], pi(1) = [0], pi(+) = [], pi(0) = [0], pi(#) = []
      Usable Rules:
       {}
      Interpretation:
       [ge#](x0, x1) = x0 + x1,
       [1](x0) = x0 + 1,
       [0](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {           0(#()) -> #(),
                +(x, #()) -> x,
                +(#(), x) -> x,
            +(0(x), 0(y)) -> 0(+(x, y)),
            +(0(x), 1(y)) -> 1(+(x, y)),
            +(+(x, y), z) -> +(x, +(y, z)),
            +(1(x), 0(y)) -> 1(+(x, y)),
            +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                -(x, #()) -> x,
                -(#(), x) -> #(),
            -(0(x), 0(y)) -> 0(-(x, y)),
            -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
            -(1(x), 0(y)) -> 1(-(x, y)),
            -(1(x), 1(y)) -> 0(-(x, y)),
             not(false()) -> true(),
              not(true()) -> false(),
        if(false(), x, y) -> y,
         if(true(), x, y) -> x,
               ge(x, #()) -> true(),
            ge(#(), 0(x)) -> ge(#(), x),
            ge(#(), 1(x)) -> false(),
           ge(0(x), 0(y)) -> ge(x, y),
           ge(0(x), 1(y)) -> not(ge(y, x)),
           ge(1(x), 0(y)) -> ge(x, y),
           ge(1(x), 1(y)) -> ge(x, y),
                log'(#()) -> #(),
               log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
               log'(1(x)) -> +(log'(x), 1(#())),
                   log(x) -> -(log'(x), 1(#()))}
      Qed
    SCC:
     Strict:
      {ge#(#(), 0(x)) -> ge#(#(), x)}
     Weak:
     {           0(#()) -> #(),
              +(x, #()) -> x,
              +(#(), x) -> x,
          +(0(x), 0(y)) -> 0(+(x, y)),
          +(0(x), 1(y)) -> 1(+(x, y)),
          +(+(x, y), z) -> +(x, +(y, z)),
          +(1(x), 0(y)) -> 1(+(x, y)),
          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
              -(x, #()) -> x,
              -(#(), x) -> #(),
          -(0(x), 0(y)) -> 0(-(x, y)),
          -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
          -(1(x), 0(y)) -> 1(-(x, y)),
          -(1(x), 1(y)) -> 0(-(x, y)),
           not(false()) -> true(),
            not(true()) -> false(),
      if(false(), x, y) -> y,
       if(true(), x, y) -> x,
             ge(x, #()) -> true(),
          ge(#(), 0(x)) -> ge(#(), x),
          ge(#(), 1(x)) -> false(),
         ge(0(x), 0(y)) -> ge(x, y),
         ge(0(x), 1(y)) -> not(ge(y, x)),
         ge(1(x), 0(y)) -> ge(x, y),
         ge(1(x), 1(y)) -> ge(x, y),
              log'(#()) -> #(),
             log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
             log'(1(x)) -> +(log'(x), 1(#())),
                 log(x) -> -(log'(x), 1(#()))}
     SPSC:
      Simple Projection:
       pi(ge#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {-#(0(x), 0(y)) -> -#(x, y),
       -#(0(x), 1(y)) -> -#(x, y),
       -#(0(x), 1(y)) -> -#(-(x, y), 1(#())),
       -#(1(x), 0(y)) -> -#(x, y),
       -#(1(x), 1(y)) -> -#(x, y)}
     Weak:
     {           0(#()) -> #(),
              +(x, #()) -> x,
              +(#(), x) -> x,
          +(0(x), 0(y)) -> 0(+(x, y)),
          +(0(x), 1(y)) -> 1(+(x, y)),
          +(+(x, y), z) -> +(x, +(y, z)),
          +(1(x), 0(y)) -> 1(+(x, y)),
          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
              -(x, #()) -> x,
              -(#(), x) -> #(),
          -(0(x), 0(y)) -> 0(-(x, y)),
          -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
          -(1(x), 0(y)) -> 1(-(x, y)),
          -(1(x), 1(y)) -> 0(-(x, y)),
           not(false()) -> true(),
            not(true()) -> false(),
      if(false(), x, y) -> y,
       if(true(), x, y) -> x,
             ge(x, #()) -> true(),
          ge(#(), 0(x)) -> ge(#(), x),
          ge(#(), 1(x)) -> false(),
         ge(0(x), 0(y)) -> ge(x, y),
         ge(0(x), 1(y)) -> not(ge(y, x)),
         ge(1(x), 0(y)) -> ge(x, y),
         ge(1(x), 1(y)) -> ge(x, y),
              log'(#()) -> #(),
             log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
             log'(1(x)) -> +(log'(x), 1(#())),
                 log(x) -> -(log'(x), 1(#()))}
     POLY:
      Argument Filtering:
       pi(log) = [], pi(log') = [], pi(ge) = [], pi(if) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(-#) = [1], pi(-) = [], pi(1) = [0], pi(+) = [], pi(0) = 0, pi(#) = []
      Usable Rules:
       {}
      Interpretation:
       [-#](x0) = x0 + 1,
       [1](x0) = x0 + 1,
       [#] = 0
      Strict:
       {-#(0(x), 0(y)) -> -#(x, y),
        -#(0(x), 1(y)) -> -#(-(x, y), 1(#())),
        -#(1(x), 0(y)) -> -#(x, y)}
      Weak:
       {           0(#()) -> #(),
                +(x, #()) -> x,
                +(#(), x) -> x,
            +(0(x), 0(y)) -> 0(+(x, y)),
            +(0(x), 1(y)) -> 1(+(x, y)),
            +(+(x, y), z) -> +(x, +(y, z)),
            +(1(x), 0(y)) -> 1(+(x, y)),
            +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                -(x, #()) -> x,
                -(#(), x) -> #(),
            -(0(x), 0(y)) -> 0(-(x, y)),
            -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
            -(1(x), 0(y)) -> 1(-(x, y)),
            -(1(x), 1(y)) -> 0(-(x, y)),
             not(false()) -> true(),
              not(true()) -> false(),
        if(false(), x, y) -> y,
         if(true(), x, y) -> x,
               ge(x, #()) -> true(),
            ge(#(), 0(x)) -> ge(#(), x),
            ge(#(), 1(x)) -> false(),
           ge(0(x), 0(y)) -> ge(x, y),
           ge(0(x), 1(y)) -> not(ge(y, x)),
           ge(1(x), 0(y)) -> ge(x, y),
           ge(1(x), 1(y)) -> ge(x, y),
                log'(#()) -> #(),
               log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
               log'(1(x)) -> +(log'(x), 1(#())),
                   log(x) -> -(log'(x), 1(#()))}
      EDG:
       {(-#(1(x), 0(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y))
        (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
        (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y))
        (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
        (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y))
        (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())))
        (-#(0(x), 0(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y))}
       SCCS:
        Scc:
         {-#(0(x), 1(y)) -> -#(-(x, y), 1(#()))}
        Scc:
         {-#(0(x), 0(y)) -> -#(x, y),
          -#(1(x), 0(y)) -> -#(x, y)}
        SCC:
         Strict:
          {-#(0(x), 1(y)) -> -#(-(x, y), 1(#()))}
         Weak:
         {           0(#()) -> #(),
                  +(x, #()) -> x,
                  +(#(), x) -> x,
              +(0(x), 0(y)) -> 0(+(x, y)),
              +(0(x), 1(y)) -> 1(+(x, y)),
              +(+(x, y), z) -> +(x, +(y, z)),
              +(1(x), 0(y)) -> 1(+(x, y)),
              +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                  -(x, #()) -> x,
                  -(#(), x) -> #(),
              -(0(x), 0(y)) -> 0(-(x, y)),
              -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
              -(1(x), 0(y)) -> 1(-(x, y)),
              -(1(x), 1(y)) -> 0(-(x, y)),
               not(false()) -> true(),
                not(true()) -> false(),
          if(false(), x, y) -> y,
           if(true(), x, y) -> x,
                 ge(x, #()) -> true(),
              ge(#(), 0(x)) -> ge(#(), x),
              ge(#(), 1(x)) -> false(),
             ge(0(x), 0(y)) -> ge(x, y),
             ge(0(x), 1(y)) -> not(ge(y, x)),
             ge(1(x), 0(y)) -> ge(x, y),
             ge(1(x), 1(y)) -> ge(x, y),
                  log'(#()) -> #(),
                 log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
                 log'(1(x)) -> +(log'(x), 1(#())),
                     log(x) -> -(log'(x), 1(#()))}
         POLY:
          Argument Filtering:
           pi(log) = [], pi(log') = [], pi(ge) = [], pi(if) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(-#) = 0, pi(-) = 0, pi(1) = [0], pi(+) = [], pi(0) = [0], pi(#) = []
          Usable Rules:
           {}
          Interpretation:
           [0](x0) = x0 + 1
          Strict:
           {}
          Weak:
           {           0(#()) -> #(),
                    +(x, #()) -> x,
                    +(#(), x) -> x,
                +(0(x), 0(y)) -> 0(+(x, y)),
                +(0(x), 1(y)) -> 1(+(x, y)),
                +(+(x, y), z) -> +(x, +(y, z)),
                +(1(x), 0(y)) -> 1(+(x, y)),
                +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                    -(x, #()) -> x,
                    -(#(), x) -> #(),
                -(0(x), 0(y)) -> 0(-(x, y)),
                -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
                -(1(x), 0(y)) -> 1(-(x, y)),
                -(1(x), 1(y)) -> 0(-(x, y)),
                 not(false()) -> true(),
                  not(true()) -> false(),
            if(false(), x, y) -> y,
             if(true(), x, y) -> x,
                   ge(x, #()) -> true(),
                ge(#(), 0(x)) -> ge(#(), x),
                ge(#(), 1(x)) -> false(),
               ge(0(x), 0(y)) -> ge(x, y),
               ge(0(x), 1(y)) -> not(ge(y, x)),
               ge(1(x), 0(y)) -> ge(x, y),
               ge(1(x), 1(y)) -> ge(x, y),
                    log'(#()) -> #(),
                   log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
                   log'(1(x)) -> +(log'(x), 1(#())),
                       log(x) -> -(log'(x), 1(#()))}
          Qed
        SCC:
         Strict:
          {-#(0(x), 0(y)) -> -#(x, y),
           -#(1(x), 0(y)) -> -#(x, y)}
         Weak:
         {           0(#()) -> #(),
                  +(x, #()) -> x,
                  +(#(), x) -> x,
              +(0(x), 0(y)) -> 0(+(x, y)),
              +(0(x), 1(y)) -> 1(+(x, y)),
              +(+(x, y), z) -> +(x, +(y, z)),
              +(1(x), 0(y)) -> 1(+(x, y)),
              +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                  -(x, #()) -> x,
                  -(#(), x) -> #(),
              -(0(x), 0(y)) -> 0(-(x, y)),
              -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
              -(1(x), 0(y)) -> 1(-(x, y)),
              -(1(x), 1(y)) -> 0(-(x, y)),
               not(false()) -> true(),
                not(true()) -> false(),
          if(false(), x, y) -> y,
           if(true(), x, y) -> x,
                 ge(x, #()) -> true(),
              ge(#(), 0(x)) -> ge(#(), x),
              ge(#(), 1(x)) -> false(),
             ge(0(x), 0(y)) -> ge(x, y),
             ge(0(x), 1(y)) -> not(ge(y, x)),
             ge(1(x), 0(y)) -> ge(x, y),
             ge(1(x), 1(y)) -> ge(x, y),
                  log'(#()) -> #(),
                 log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
                 log'(1(x)) -> +(log'(x), 1(#())),
                     log(x) -> -(log'(x), 1(#()))}
         SPSC:
          Simple Projection:
           pi(-#) = 0
          Strict:
           {-#(0(x), 0(y)) -> -#(x, y)}
          EDG:
           {(-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y))}
           SCCS:
            Scc:
             {-#(0(x), 0(y)) -> -#(x, y)}
            SCC:
             Strict:
              {-#(0(x), 0(y)) -> -#(x, y)}
             Weak:
             {           0(#()) -> #(),
                      +(x, #()) -> x,
                      +(#(), x) -> x,
                  +(0(x), 0(y)) -> 0(+(x, y)),
                  +(0(x), 1(y)) -> 1(+(x, y)),
                  +(+(x, y), z) -> +(x, +(y, z)),
                  +(1(x), 0(y)) -> 1(+(x, y)),
                  +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                      -(x, #()) -> x,
                      -(#(), x) -> #(),
                  -(0(x), 0(y)) -> 0(-(x, y)),
                  -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
                  -(1(x), 0(y)) -> 1(-(x, y)),
                  -(1(x), 1(y)) -> 0(-(x, y)),
                   not(false()) -> true(),
                    not(true()) -> false(),
              if(false(), x, y) -> y,
               if(true(), x, y) -> x,
                     ge(x, #()) -> true(),
                  ge(#(), 0(x)) -> ge(#(), x),
                  ge(#(), 1(x)) -> false(),
                 ge(0(x), 0(y)) -> ge(x, y),
                 ge(0(x), 1(y)) -> not(ge(y, x)),
                 ge(1(x), 0(y)) -> ge(x, y),
                 ge(1(x), 1(y)) -> ge(x, y),
                      log'(#()) -> #(),
                     log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
                     log'(1(x)) -> +(log'(x), 1(#())),
                         log(x) -> -(log'(x), 1(#()))}
             SPSC:
              Simple Projection:
               pi(-#) = 0
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {+#(0(x), 0(y)) -> +#(x, y),
       +#(0(x), 1(y)) -> +#(x, y),
       +#(+(x, y), z) -> +#(x, +(y, z)),
       +#(+(x, y), z) -> +#(y, z),
       +#(1(x), 0(y)) -> +#(x, y),
       +#(1(x), 1(y)) -> +#(x, y),
       +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
     Weak:
     {           0(#()) -> #(),
              +(x, #()) -> x,
              +(#(), x) -> x,
          +(0(x), 0(y)) -> 0(+(x, y)),
          +(0(x), 1(y)) -> 1(+(x, y)),
          +(+(x, y), z) -> +(x, +(y, z)),
          +(1(x), 0(y)) -> 1(+(x, y)),
          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
              -(x, #()) -> x,
              -(#(), x) -> #(),
          -(0(x), 0(y)) -> 0(-(x, y)),
          -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
          -(1(x), 0(y)) -> 1(-(x, y)),
          -(1(x), 1(y)) -> 0(-(x, y)),
           not(false()) -> true(),
            not(true()) -> false(),
      if(false(), x, y) -> y,
       if(true(), x, y) -> x,
             ge(x, #()) -> true(),
          ge(#(), 0(x)) -> ge(#(), x),
          ge(#(), 1(x)) -> false(),
         ge(0(x), 0(y)) -> ge(x, y),
         ge(0(x), 1(y)) -> not(ge(y, x)),
         ge(1(x), 0(y)) -> ge(x, y),
         ge(1(x), 1(y)) -> ge(x, y),
              log'(#()) -> #(),
             log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
             log'(1(x)) -> +(log'(x), 1(#())),
                 log(x) -> -(log'(x), 1(#()))}
     POLY:
      Argument Filtering:
       pi(log) = [], pi(log') = [], pi(ge) = [], pi(if) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(-) = [], pi(1) = [0], pi(+#) = [0,1], pi(+) = [0,1], pi(0) = 0, pi(#) = []
      Usable Rules:
       {}
      Interpretation:
       [+#](x0, x1) = x0 + x1 + 1,
       [+](x0, x1) = x0 + x1,
       [1](x0) = x0 + 1,
       [#] = 1
      Strict:
       {+#(0(x), 0(y)) -> +#(x, y),
        +#(+(x, y), z) -> +#(x, +(y, z)),
        +#(+(x, y), z) -> +#(y, z),
        +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
      Weak:
       {           0(#()) -> #(),
                +(x, #()) -> x,
                +(#(), x) -> x,
            +(0(x), 0(y)) -> 0(+(x, y)),
            +(0(x), 1(y)) -> 1(+(x, y)),
            +(+(x, y), z) -> +(x, +(y, z)),
            +(1(x), 0(y)) -> 1(+(x, y)),
            +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                -(x, #()) -> x,
                -(#(), x) -> #(),
            -(0(x), 0(y)) -> 0(-(x, y)),
            -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
            -(1(x), 0(y)) -> 1(-(x, y)),
            -(1(x), 1(y)) -> 0(-(x, y)),
             not(false()) -> true(),
              not(true()) -> false(),
        if(false(), x, y) -> y,
         if(true(), x, y) -> x,
               ge(x, #()) -> true(),
            ge(#(), 0(x)) -> ge(#(), x),
            ge(#(), 1(x)) -> false(),
           ge(0(x), 0(y)) -> ge(x, y),
           ge(0(x), 1(y)) -> not(ge(y, x)),
           ge(1(x), 0(y)) -> ge(x, y),
           ge(1(x), 1(y)) -> ge(x, y),
                log'(#()) -> #(),
               log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
               log'(1(x)) -> +(log'(x), 1(#())),
                   log(x) -> -(log'(x), 1(#()))}
      EDG:
       {(+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
        (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))
        (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
        (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 0(y)) -> +#(x, y))
        (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
        (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
        (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
        (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
        (+#(+(x, y), z) -> +#(y, z), +#(0(x), 0(y)) -> +#(x, y))
        (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
        (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
        (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
        (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(+(x, y), z) -> +#(x, +(y, z)))
        (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(+(x, y), z) -> +#(y, z))
        (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))}
       SCCS:
        Scc:
         {+#(0(x), 0(y)) -> +#(x, y),
          +#(+(x, y), z) -> +#(x, +(y, z)),
          +#(+(x, y), z) -> +#(y, z),
          +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
        SCC:
         Strict:
          {+#(0(x), 0(y)) -> +#(x, y),
           +#(+(x, y), z) -> +#(x, +(y, z)),
           +#(+(x, y), z) -> +#(y, z),
           +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
         Weak:
         {           0(#()) -> #(),
                  +(x, #()) -> x,
                  +(#(), x) -> x,
              +(0(x), 0(y)) -> 0(+(x, y)),
              +(0(x), 1(y)) -> 1(+(x, y)),
              +(+(x, y), z) -> +(x, +(y, z)),
              +(1(x), 0(y)) -> 1(+(x, y)),
              +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                  -(x, #()) -> x,
                  -(#(), x) -> #(),
              -(0(x), 0(y)) -> 0(-(x, y)),
              -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
              -(1(x), 0(y)) -> 1(-(x, y)),
              -(1(x), 1(y)) -> 0(-(x, y)),
               not(false()) -> true(),
                not(true()) -> false(),
          if(false(), x, y) -> y,
           if(true(), x, y) -> x,
                 ge(x, #()) -> true(),
              ge(#(), 0(x)) -> ge(#(), x),
              ge(#(), 1(x)) -> false(),
             ge(0(x), 0(y)) -> ge(x, y),
             ge(0(x), 1(y)) -> not(ge(y, x)),
             ge(1(x), 0(y)) -> ge(x, y),
             ge(1(x), 1(y)) -> ge(x, y),
                  log'(#()) -> #(),
                 log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
                 log'(1(x)) -> +(log'(x), 1(#())),
                     log(x) -> -(log'(x), 1(#()))}
         POLY:
          Argument Filtering:
           pi(log) = [], pi(log') = [], pi(ge) = [], pi(if) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(-) = [], pi(1) = [0], pi(+#) = [0,1], pi(+) = [0,1], pi(0) = 0, pi(#) = []
          Usable Rules:
           {}
          Interpretation:
           [+#](x0, x1) = x0 + x1,
           [+](x0, x1) = x0 + x1,
           [1](x0) = x0 + 1,
           [#] = 0
          Strict:
           {+#(0(x), 0(y)) -> +#(x, y),
            +#(+(x, y), z) -> +#(x, +(y, z)),
            +#(+(x, y), z) -> +#(y, z)}
          Weak:
           {           0(#()) -> #(),
                    +(x, #()) -> x,
                    +(#(), x) -> x,
                +(0(x), 0(y)) -> 0(+(x, y)),
                +(0(x), 1(y)) -> 1(+(x, y)),
                +(+(x, y), z) -> +(x, +(y, z)),
                +(1(x), 0(y)) -> 1(+(x, y)),
                +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                    -(x, #()) -> x,
                    -(#(), x) -> #(),
                -(0(x), 0(y)) -> 0(-(x, y)),
                -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
                -(1(x), 0(y)) -> 1(-(x, y)),
                -(1(x), 1(y)) -> 0(-(x, y)),
                 not(false()) -> true(),
                  not(true()) -> false(),
            if(false(), x, y) -> y,
             if(true(), x, y) -> x,
                   ge(x, #()) -> true(),
                ge(#(), 0(x)) -> ge(#(), x),
                ge(#(), 1(x)) -> false(),
               ge(0(x), 0(y)) -> ge(x, y),
               ge(0(x), 1(y)) -> not(ge(y, x)),
               ge(1(x), 0(y)) -> ge(x, y),
               ge(1(x), 1(y)) -> ge(x, y),
                    log'(#()) -> #(),
                   log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
                   log'(1(x)) -> +(log'(x), 1(#())),
                       log(x) -> -(log'(x), 1(#()))}
          EDG:
           {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
            (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
            (+#(+(x, y), z) -> +#(y, z), +#(0(x), 0(y)) -> +#(x, y))
            (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
            (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
            (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
            (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 0(y)) -> +#(x, y))
            (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
            (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))}
           SCCS:
            Scc:
             {+#(0(x), 0(y)) -> +#(x, y),
              +#(+(x, y), z) -> +#(x, +(y, z)),
              +#(+(x, y), z) -> +#(y, z)}
            SCC:
             Strict:
              {+#(0(x), 0(y)) -> +#(x, y),
               +#(+(x, y), z) -> +#(x, +(y, z)),
               +#(+(x, y), z) -> +#(y, z)}
             Weak:
             {           0(#()) -> #(),
                      +(x, #()) -> x,
                      +(#(), x) -> x,
                  +(0(x), 0(y)) -> 0(+(x, y)),
                  +(0(x), 1(y)) -> 1(+(x, y)),
                  +(+(x, y), z) -> +(x, +(y, z)),
                  +(1(x), 0(y)) -> 1(+(x, y)),
                  +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                      -(x, #()) -> x,
                      -(#(), x) -> #(),
                  -(0(x), 0(y)) -> 0(-(x, y)),
                  -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
                  -(1(x), 0(y)) -> 1(-(x, y)),
                  -(1(x), 1(y)) -> 0(-(x, y)),
                   not(false()) -> true(),
                    not(true()) -> false(),
              if(false(), x, y) -> y,
               if(true(), x, y) -> x,
                     ge(x, #()) -> true(),
                  ge(#(), 0(x)) -> ge(#(), x),
                  ge(#(), 1(x)) -> false(),
                 ge(0(x), 0(y)) -> ge(x, y),
                 ge(0(x), 1(y)) -> not(ge(y, x)),
                 ge(1(x), 0(y)) -> ge(x, y),
                 ge(1(x), 1(y)) -> ge(x, y),
                      log'(#()) -> #(),
                     log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
                     log'(1(x)) -> +(log'(x), 1(#())),
                         log(x) -> -(log'(x), 1(#()))}
             SPSC:
              Simple Projection:
               pi(+#) = 0
              Strict:
               {+#(0(x), 0(y)) -> +#(x, y),
                +#(+(x, y), z) -> +#(y, z)}
              EDG:
               {(+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
                (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
                (+#(+(x, y), z) -> +#(y, z), +#(0(x), 0(y)) -> +#(x, y))
                (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))}
               SCCS:
                Scc:
                 {+#(0(x), 0(y)) -> +#(x, y),
                  +#(+(x, y), z) -> +#(y, z)}
                SCC:
                 Strict:
                  {+#(0(x), 0(y)) -> +#(x, y),
                   +#(+(x, y), z) -> +#(y, z)}
                 Weak:
                 {           0(#()) -> #(),
                          +(x, #()) -> x,
                          +(#(), x) -> x,
                      +(0(x), 0(y)) -> 0(+(x, y)),
                      +(0(x), 1(y)) -> 1(+(x, y)),
                      +(+(x, y), z) -> +(x, +(y, z)),
                      +(1(x), 0(y)) -> 1(+(x, y)),
                      +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                          -(x, #()) -> x,
                          -(#(), x) -> #(),
                      -(0(x), 0(y)) -> 0(-(x, y)),
                      -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
                      -(1(x), 0(y)) -> 1(-(x, y)),
                      -(1(x), 1(y)) -> 0(-(x, y)),
                       not(false()) -> true(),
                        not(true()) -> false(),
                  if(false(), x, y) -> y,
                   if(true(), x, y) -> x,
                         ge(x, #()) -> true(),
                      ge(#(), 0(x)) -> ge(#(), x),
                      ge(#(), 1(x)) -> false(),
                     ge(0(x), 0(y)) -> ge(x, y),
                     ge(0(x), 1(y)) -> not(ge(y, x)),
                     ge(1(x), 0(y)) -> ge(x, y),
                     ge(1(x), 1(y)) -> ge(x, y),
                          log'(#()) -> #(),
                         log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
                         log'(1(x)) -> +(log'(x), 1(#())),
                             log(x) -> -(log'(x), 1(#()))}
                 SPSC:
                  Simple Projection:
                   pi(+#) = 0
                  Strict:
                   {+#(0(x), 0(y)) -> +#(x, y)}
                  EDG:
                   {(+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))}
                   SCCS:
                    Scc:
                     {+#(0(x), 0(y)) -> +#(x, y)}
                    SCC:
                     Strict:
                      {+#(0(x), 0(y)) -> +#(x, y)}
                     Weak:
                     {           0(#()) -> #(),
                              +(x, #()) -> x,
                              +(#(), x) -> x,
                          +(0(x), 0(y)) -> 0(+(x, y)),
                          +(0(x), 1(y)) -> 1(+(x, y)),
                          +(+(x, y), z) -> +(x, +(y, z)),
                          +(1(x), 0(y)) -> 1(+(x, y)),
                          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                              -(x, #()) -> x,
                              -(#(), x) -> #(),
                          -(0(x), 0(y)) -> 0(-(x, y)),
                          -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))),
                          -(1(x), 0(y)) -> 1(-(x, y)),
                          -(1(x), 1(y)) -> 0(-(x, y)),
                           not(false()) -> true(),
                            not(true()) -> false(),
                      if(false(), x, y) -> y,
                       if(true(), x, y) -> x,
                             ge(x, #()) -> true(),
                          ge(#(), 0(x)) -> ge(#(), x),
                          ge(#(), 1(x)) -> false(),
                         ge(0(x), 0(y)) -> ge(x, y),
                         ge(0(x), 1(y)) -> not(ge(y, x)),
                         ge(1(x), 0(y)) -> ge(x, y),
                         ge(1(x), 1(y)) -> ge(x, y),
                              log'(#()) -> #(),
                             log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()),
                             log'(1(x)) -> +(log'(x), 1(#())),
                                 log(x) -> -(log'(x), 1(#()))}
                     SPSC:
                      Simple Projection:
                       pi(+#) = 0
                      Strict:
                       {}
                      Qed