MAYBE Time: 0.136063 TRS: { 0() -> n__0(), p X -> n__p X, p 0() -> 0(), p s X -> X, s X -> n__s X, leq(0(), Y) -> true(), leq(s X, 0()) -> false(), leq(s X, s Y) -> leq(X, Y), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__diff(X1, X2) -> diff(activate X1, activate X2), activate n__p X -> p activate X, if(true(), X, Y) -> activate X, if(false(), X, Y) -> activate Y, diff(X, Y) -> if(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)), diff(X1, X2) -> n__diff(X1, X2)} DP: DP: { leq#(s X, s Y) -> leq#(X, Y), activate# n__0() -> 0#(), activate# n__s X -> s# activate X, activate# n__s X -> activate# X, activate# n__diff(X1, X2) -> activate# X1, activate# n__diff(X1, X2) -> activate# X2, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2), activate# n__p X -> p# activate X, activate# n__p X -> activate# X, if#(true(), X, Y) -> activate# X, if#(false(), X, Y) -> activate# Y, diff#(X, Y) -> leq#(X, Y), diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y))} TRS: { 0() -> n__0(), p X -> n__p X, p 0() -> 0(), p s X -> X, s X -> n__s X, leq(0(), Y) -> true(), leq(s X, 0()) -> false(), leq(s X, s Y) -> leq(X, Y), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__diff(X1, X2) -> diff(activate X1, activate X2), activate n__p X -> p activate X, if(true(), X, Y) -> activate X, if(false(), X, Y) -> activate Y, diff(X, Y) -> if(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)), diff(X1, X2) -> n__diff(X1, X2)} UR: { 0() -> n__0(), p X -> n__p X, p 0() -> 0(), p s X -> X, s X -> n__s X, leq(0(), Y) -> true(), leq(s X, 0()) -> false(), leq(s X, s Y) -> leq(X, Y), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__diff(X1, X2) -> diff(activate X1, activate X2), activate n__p X -> p activate X, if(true(), X, Y) -> activate X, if(false(), X, Y) -> activate Y, diff(X, Y) -> if(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)), diff(X1, X2) -> n__diff(X1, X2), a(x, y) -> x, a(x, y) -> y} EDG: {(diff#(X, Y) -> leq#(X, Y), leq#(s X, s Y) -> leq#(X, Y)) (activate# n__p X -> activate# X, activate# n__p X -> activate# X) (activate# n__p X -> activate# X, activate# n__p X -> p# activate X) (activate# n__p X -> activate# X, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2)) (activate# n__p X -> activate# X, activate# n__diff(X1, X2) -> activate# X2) (activate# n__p X -> activate# X, activate# n__diff(X1, X2) -> activate# X1) (activate# n__p X -> activate# X, activate# n__s X -> activate# X) (activate# n__p X -> activate# X, activate# n__s X -> s# activate X) (activate# n__p X -> activate# X, activate# n__0() -> 0#()) (diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)), if#(false(), X, Y) -> activate# Y) (diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)), if#(true(), X, Y) -> activate# X) (activate# n__diff(X1, X2) -> activate# X1, activate# n__p X -> activate# X) (activate# n__diff(X1, X2) -> activate# X1, activate# n__p X -> p# activate X) (activate# n__diff(X1, X2) -> activate# X1, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2)) (activate# n__diff(X1, X2) -> activate# X1, activate# n__diff(X1, X2) -> activate# X2) (activate# n__diff(X1, X2) -> activate# X1, activate# n__diff(X1, X2) -> activate# X1) (activate# n__diff(X1, X2) -> activate# X1, activate# n__s X -> activate# X) (activate# n__diff(X1, X2) -> activate# X1, activate# n__s X -> s# activate X) (activate# n__diff(X1, X2) -> activate# X1, activate# n__0() -> 0#()) (activate# n__diff(X1, X2) -> activate# X2, activate# n__p X -> activate# X) (activate# n__diff(X1, X2) -> activate# X2, activate# n__p X -> p# activate X) (activate# n__diff(X1, X2) -> activate# X2, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2)) (activate# n__diff(X1, X2) -> activate# X2, activate# n__diff(X1, X2) -> activate# X2) (activate# n__diff(X1, X2) -> activate# X2, activate# n__diff(X1, X2) -> activate# X1) (activate# n__diff(X1, X2) -> activate# X2, activate# n__s X -> activate# X) (activate# n__diff(X1, X2) -> activate# X2, activate# n__s X -> s# activate X) (activate# n__diff(X1, X2) -> activate# X2, activate# n__0() -> 0#()) (activate# n__diff(X1, X2) -> diff#(activate X1, activate X2), diff#(X, Y) -> leq#(X, Y)) (activate# n__diff(X1, X2) -> diff#(activate X1, activate X2), diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y))) (if#(false(), X, Y) -> activate# Y, activate# n__0() -> 0#()) (if#(false(), X, Y) -> activate# Y, activate# n__s X -> s# activate X) (if#(false(), X, Y) -> activate# Y, activate# n__s X -> activate# X) (if#(false(), X, Y) -> activate# Y, activate# n__diff(X1, X2) -> activate# X1) (if#(false(), X, Y) -> activate# Y, activate# n__diff(X1, X2) -> activate# X2) (if#(false(), X, Y) -> activate# Y, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2)) (if#(false(), X, Y) -> activate# Y, activate# n__p X -> p# activate X) (if#(false(), X, Y) -> activate# Y, activate# n__p X -> activate# X) (if#(true(), X, Y) -> activate# X, activate# n__0() -> 0#()) (if#(true(), X, Y) -> activate# X, activate# n__s X -> s# activate X) (if#(true(), X, Y) -> activate# X, activate# n__s X -> activate# X) (if#(true(), X, Y) -> activate# X, activate# n__diff(X1, X2) -> activate# X1) (if#(true(), X, Y) -> activate# X, activate# n__diff(X1, X2) -> activate# X2) (if#(true(), X, Y) -> activate# X, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2)) (if#(true(), X, Y) -> activate# X, activate# n__p X -> p# activate X) (if#(true(), X, Y) -> activate# X, activate# n__p X -> activate# X) (activate# n__s X -> activate# X, activate# n__0() -> 0#()) (activate# n__s X -> activate# X, activate# n__s X -> s# activate X) (activate# n__s X -> activate# X, activate# n__s X -> activate# X) (activate# n__s X -> activate# X, activate# n__diff(X1, X2) -> activate# X1) (activate# n__s X -> activate# X, activate# n__diff(X1, X2) -> activate# X2) (activate# n__s X -> activate# X, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2)) (activate# n__s X -> activate# X, activate# n__p X -> p# activate X) (activate# n__s X -> activate# X, activate# n__p X -> activate# X) (leq#(s X, s Y) -> leq#(X, Y), leq#(s X, s Y) -> leq#(X, Y))} STATUS: arrows: 0.680473 SCCS (2): Scc: { activate# n__s X -> activate# X, activate# n__diff(X1, X2) -> activate# X1, activate# n__diff(X1, X2) -> activate# X2, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2), activate# n__p X -> activate# X, if#(true(), X, Y) -> activate# X, if#(false(), X, Y) -> activate# Y, diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y))} Scc: {leq#(s X, s Y) -> leq#(X, Y)} SCC (8): Strict: { activate# n__s X -> activate# X, activate# n__diff(X1, X2) -> activate# X1, activate# n__diff(X1, X2) -> activate# X2, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2), activate# n__p X -> activate# X, if#(true(), X, Y) -> activate# X, if#(false(), X, Y) -> activate# Y, diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y))} Weak: { 0() -> n__0(), p X -> n__p X, p 0() -> 0(), p s X -> X, s X -> n__s X, leq(0(), Y) -> true(), leq(s X, 0()) -> false(), leq(s X, s Y) -> leq(X, Y), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__diff(X1, X2) -> diff(activate X1, activate X2), activate n__p X -> p activate X, if(true(), X, Y) -> activate X, if(false(), X, Y) -> activate Y, diff(X, Y) -> if(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)), diff(X1, X2) -> n__diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + x1, [leq](x0, x1) = 0, [n__diff](x0, x1) = x0 + x1 + 1, [diff](x0, x1) = x0 + x1 + 1, [p](x0) = x0, [s](x0) = x0, [activate](x0) = x0, [n__s](x0) = x0, [n__p](x0) = x0, [0] = 0, [true] = 0, [false] = 0, [n__0] = 0, [if#](x0, x1, x2) = x0 + x1, [diff#](x0, x1) = x0 + x1 + 1, [activate#](x0) = x0 Strict: diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)) 1 + 1X + 1Y >= 1 + 1X + 1Y if#(false(), X, Y) -> activate# Y 0 + 1X + 1Y >= 0 + 1Y if#(true(), X, Y) -> activate# X 0 + 1X + 1Y >= 0 + 1X activate# n__p X -> activate# X 0 + 1X >= 0 + 1X activate# n__diff(X1, X2) -> diff#(activate X1, activate X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 activate# n__diff(X1, X2) -> activate# X2 1 + 1X1 + 1X2 >= 0 + 1X2 activate# n__diff(X1, X2) -> activate# X1 1 + 1X1 + 1X2 >= 0 + 1X1 activate# n__s X -> activate# X 0 + 1X >= 0 + 1X Weak: diff(X1, X2) -> n__diff(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 diff(X, Y) -> if(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)) 1 + 1X + 1Y >= 1 + 1X + 1Y if(false(), X, Y) -> activate Y 0 + 1X + 1Y >= 0 + 1Y if(true(), X, Y) -> activate X 0 + 1X + 1Y >= 0 + 1X activate n__p X -> p activate X 0 + 1X >= 0 + 1X activate n__diff(X1, X2) -> diff(activate X1, activate X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 activate n__s X -> s activate X 0 + 1X >= 0 + 1X activate n__0() -> 0() 0 >= 0 activate X -> X 0 + 1X >= 1X leq(s X, s Y) -> leq(X, Y) 0 + 0X + 0Y >= 0 + 0X + 0Y leq(s X, 0()) -> false() 0 + 0X >= 0 leq(0(), Y) -> true() 0 + 0Y >= 0 s X -> n__s X 0 + 1X >= 0 + 1X p s X -> X 0 + 1X >= 1X p 0() -> 0() 0 >= 0 p X -> n__p X 0 + 1X >= 0 + 1X 0() -> n__0() 0 >= 0 SCCS (1): Scc: { activate# n__s X -> activate# X, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2), activate# n__p X -> activate# X, if#(true(), X, Y) -> activate# X, if#(false(), X, Y) -> activate# Y, diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y))} SCC (6): Strict: { activate# n__s X -> activate# X, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2), activate# n__p X -> activate# X, if#(true(), X, Y) -> activate# X, if#(false(), X, Y) -> activate# Y, diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y))} Weak: { 0() -> n__0(), p X -> n__p X, p 0() -> 0(), p s X -> X, s X -> n__s X, leq(0(), Y) -> true(), leq(s X, 0()) -> false(), leq(s X, s Y) -> leq(X, Y), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__diff(X1, X2) -> diff(activate X1, activate X2), activate n__p X -> p activate X, if(true(), X, Y) -> activate X, if(false(), X, Y) -> activate Y, diff(X, Y) -> if(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)), diff(X1, X2) -> n__diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 0, [leq](x0, x1) = 0, [n__diff](x0, x1) = 0, [diff](x0, x1) = 0, [p](x0) = 0, [s](x0) = 0, [activate](x0) = 0, [n__s](x0) = x0, [n__p](x0) = x0 + 1, [0] = 0, [true] = 0, [false] = 0, [n__0] = 0, [if#](x0, x1, x2) = x0 + x1, [diff#](x0, x1) = 0, [activate#](x0) = x0 Strict: diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)) 0 + 0X + 0Y >= 0 + 0X + 0Y if#(false(), X, Y) -> activate# Y 0 + 1X + 1Y >= 0 + 1Y if#(true(), X, Y) -> activate# X 0 + 1X + 1Y >= 0 + 1X activate# n__p X -> activate# X 1 + 1X >= 0 + 1X activate# n__diff(X1, X2) -> diff#(activate X1, activate X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate# n__s X -> activate# X 0 + 1X >= 0 + 1X Weak: diff(X1, X2) -> n__diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X, Y) -> if(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)) 0 + 0X + 0Y >= 0 + 0X + 0Y if(false(), X, Y) -> activate Y 0 + 0X + 0Y >= 0 + 0Y if(true(), X, Y) -> activate X 0 + 0X + 0Y >= 0 + 0X activate n__p X -> p activate X 0 + 0X >= 0 + 0X activate n__diff(X1, X2) -> diff(activate X1, activate X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__s X -> s activate X 0 + 0X >= 0 + 0X activate n__0() -> 0() 0 >= 0 activate X -> X 0 + 0X >= 1X leq(s X, s Y) -> leq(X, Y) 0 + 0X + 0Y >= 0 + 0X + 0Y leq(s X, 0()) -> false() 0 + 0X >= 0 leq(0(), Y) -> true() 0 + 0Y >= 0 s X -> n__s X 0 + 0X >= 0 + 1X p s X -> X 0 + 0X >= 1X p 0() -> 0() 0 >= 0 p X -> n__p X 0 + 0X >= 1 + 1X 0() -> n__0() 0 >= 0 SCCS (1): Scc: { activate# n__s X -> activate# X, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2), if#(true(), X, Y) -> activate# X, if#(false(), X, Y) -> activate# Y, diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y))} SCC (5): Strict: { activate# n__s X -> activate# X, activate# n__diff(X1, X2) -> diff#(activate X1, activate X2), if#(true(), X, Y) -> activate# X, if#(false(), X, Y) -> activate# Y, diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s n__diff(n__p X, Y))} Weak: { 0() -> n__0(), p X -> n__p X, p 0() -> 0(), p s X -> X, s X -> n__s X, leq(0(), Y) -> true(), leq(s X, 0()) -> false(), leq(s X, s Y) -> leq(X, Y), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__diff(X1, X2) -> diff(activate X1, activate X2), activate n__p X -> p activate X, if(true(), X, Y) -> activate X, if(false(), X, Y) -> activate Y, diff(X, Y) -> if(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)), diff(X1, X2) -> n__diff(X1, X2)} Fail SCC (1): Strict: {leq#(s X, s Y) -> leq#(X, Y)} Weak: { 0() -> n__0(), p X -> n__p X, p 0() -> 0(), p s X -> X, s X -> n__s X, leq(0(), Y) -> true(), leq(s X, 0()) -> false(), leq(s X, s Y) -> leq(X, Y), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__diff(X1, X2) -> diff(activate X1, activate X2), activate n__p X -> p activate X, if(true(), X, Y) -> activate X, if(false(), X, Y) -> activate Y, diff(X, Y) -> if(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)), diff(X1, X2) -> n__diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 0, [leq](x0, x1) = x0 + 1, [n__diff](x0, x1) = x0 + 1, [diff](x0, x1) = 0, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [activate](x0) = x0 + 1, [n__s](x0) = 1, [n__p](x0) = 1, [0] = 1, [true] = 0, [false] = 0, [n__0] = 1, [leq#](x0, x1) = x0 Strict: leq#(s X, s Y) -> leq#(X, Y) 1 + 0X + 1Y >= 0 + 0X + 1Y Weak: diff(X1, X2) -> n__diff(X1, X2) 0 + 0X1 + 0X2 >= 1 + 1X1 + 0X2 diff(X, Y) -> if(leq(X, Y), n__0(), n__s n__diff(n__p X, Y)) 0 + 0X + 0Y >= 0 + 0X + 0Y if(false(), X, Y) -> activate Y 0 + 0X + 0Y >= 1 + 1Y if(true(), X, Y) -> activate X 0 + 0X + 0Y >= 1 + 1X activate n__p X -> p activate X 2 + 0X >= 2 + 1X activate n__diff(X1, X2) -> diff(activate X1, activate X2) 2 + 1X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__s X -> s activate X 2 + 0X >= 2 + 1X activate n__0() -> 0() 2 >= 1 activate X -> X 1 + 1X >= 1X leq(s X, s Y) -> leq(X, Y) 2 + 1X + 0Y >= 1 + 1X + 0Y leq(s X, 0()) -> false() 2 + 1X >= 0 leq(0(), Y) -> true() 2 + 0Y >= 0 s X -> n__s X 1 + 1X >= 1 + 0X p s X -> X 2 + 1X >= 1X p 0() -> 0() 2 >= 1 p X -> n__p X 1 + 1X >= 1 + 0X 0() -> n__0() 1 >= 1 Qed