Input TRS: 1: active(minus(0(),Y)) -> mark(0()) 2: active(minus(s(X),s(Y))) -> mark(minus(X,Y)) 3: active(geq(X,0())) -> mark(true()) 4: active(geq(0(),s(Y))) -> mark(false()) 5: active(geq(s(X),s(Y))) -> mark(geq(X,Y)) 6: active(div(0(),s(Y))) -> mark(0()) 7: active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())) 8: active(if(true(),X,Y)) -> mark(X) 9: active(if(false(),X,Y)) -> mark(Y) 10: active(s(X)) -> s(active(X)) 11: active(div(X1,X2)) -> div(active(X1),X2) 12: active(if(X1,X2,X3)) -> if(active(X1),X2,X3) 13: s(mark(X)) -> mark(s(X)) 14: div(mark(X1),X2) -> mark(div(X1,X2)) 15: if(mark(X1),X2,X3) -> mark(if(X1,X2,X3)) 16: proper(minus(X1,X2)) -> minus(proper(X1),proper(X2)) 17: proper(0()) -> ok(0()) 18: proper(s(X)) -> s(proper(X)) 19: proper(geq(X1,X2)) -> geq(proper(X1),proper(X2)) 20: proper(true()) -> ok(true()) 21: proper(false()) -> ok(false()) 22: proper(div(X1,X2)) -> div(proper(X1),proper(X2)) 23: proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3)) 24: minus(ok(X1),ok(X2)) -> ok(minus(X1,X2)) 25: s(ok(X)) -> ok(s(X)) 26: geq(ok(X1),ok(X2)) -> ok(geq(X1,X2)) 27: div(ok(X1),ok(X2)) -> ok(div(X1,X2)) 28: if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3)) 29: top(mark(X)) -> top(proper(X)) 30: top(ok(X)) -> top(active(X)) Number of strict rules: 30 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #active(minus(s(X),s(Y))) -> #minus(X,Y) #2: #top(mark(X)) -> #top(proper(X)) #3: #top(mark(X)) -> #proper(X) #4: #s(mark(X)) -> #s(X) #5: #active(div(X1,X2)) -> #div(active(X1),X2) #6: #active(div(X1,X2)) -> #active(X1) #7: #minus(ok(X1),ok(X2)) -> #minus(X1,X2) #8: #proper(if(X1,X2,X3)) -> #if(proper(X1),proper(X2),proper(X3)) #9: #proper(if(X1,X2,X3)) -> #proper(X1) #10: #proper(if(X1,X2,X3)) -> #proper(X2) #11: #proper(if(X1,X2,X3)) -> #proper(X3) #12: #active(if(X1,X2,X3)) -> #if(active(X1),X2,X3) #13: #active(if(X1,X2,X3)) -> #active(X1) #14: #div(mark(X1),X2) -> #div(X1,X2) #15: #top(ok(X)) -> #top(active(X)) #16: #top(ok(X)) -> #active(X) #17: #s(ok(X)) -> #s(X) #18: #active(div(s(X),s(Y))) -> #if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()) #19: #active(div(s(X),s(Y))) -> #geq(X,Y) #20: #active(div(s(X),s(Y))) -> #s(div(minus(X,Y),s(Y))) #21: #active(div(s(X),s(Y))) -> #div(minus(X,Y),s(Y)) #22: #active(div(s(X),s(Y))) -> #minus(X,Y) #23: #active(s(X)) -> #s(active(X)) #24: #active(s(X)) -> #active(X) #25: #active(geq(s(X),s(Y))) -> #geq(X,Y) #26: #if(ok(X1),ok(X2),ok(X3)) -> #if(X1,X2,X3) #27: #proper(div(X1,X2)) -> #div(proper(X1),proper(X2)) #28: #proper(div(X1,X2)) -> #proper(X1) #29: #proper(div(X1,X2)) -> #proper(X2) #30: #div(ok(X1),ok(X2)) -> #div(X1,X2) #31: #proper(geq(X1,X2)) -> #geq(proper(X1),proper(X2)) #32: #proper(geq(X1,X2)) -> #proper(X1) #33: #proper(geq(X1,X2)) -> #proper(X2) #34: #geq(ok(X1),ok(X2)) -> #geq(X1,X2) #35: #proper(minus(X1,X2)) -> #minus(proper(X1),proper(X2)) #36: #proper(minus(X1,X2)) -> #proper(X1) #37: #proper(minus(X1,X2)) -> #proper(X2) #38: #if(mark(X1),X2,X3) -> #if(X1,X2,X3) #39: #proper(s(X)) -> #s(proper(X)) #40: #proper(s(X)) -> #proper(X) Number of SCCs: 8, DPs: 23, edges: 127 SCC { #34 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #div(x1,x2) weight: 0 s(x1) weight: 0 minus(x1,x2) weight: 0 #geq(x1,x2) weight: x2 top(x1) weight: 0 false() weight: 0 #top(x1) weight: 0 div(x1,x2) weight: 0 geq(x1,x2) weight: 0 true() weight: 0 proper(x1) weight: 0 ok(x1) weight: (/ 1 2) + x1 0() weight: 0 if(x1,x2,x3) weight: 0 #s(x1) weight: 0 mark(x1) weight: 0 #minus(x1,x2) weight: 0 #proper(x1) weight: 0 active(x1) weight: 0 #if(x1,x2,x3) weight: 0 #active(x1) weight: 0 Usable rules: { } Removed DPs: #34 Number of SCCs: 7, DPs: 22, edges: 126 SCC { #7 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #div(x1,x2) weight: 0 s(x1) weight: 0 minus(x1,x2) weight: 0 #geq(x1,x2) weight: 0 top(x1) weight: 0 false() weight: 0 #top(x1) weight: 0 div(x1,x2) weight: 0 geq(x1,x2) weight: 0 true() weight: 0 proper(x1) weight: 0 ok(x1) weight: (/ 1 2) + x1 0() weight: 0 if(x1,x2,x3) weight: 0 #s(x1) weight: 0 mark(x1) weight: 0 #minus(x1,x2) weight: x2 #proper(x1) weight: 0 active(x1) weight: 0 #if(x1,x2,x3) weight: 0 #active(x1) weight: 0 Usable rules: { } Removed DPs: #7 Number of SCCs: 6, DPs: 21, edges: 125 SCC { #4 #17 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #div(x1,x2) weight: 0 s(x1) weight: 0 minus(x1,x2) weight: 0 #geq(x1,x2) weight: 0 top(x1) weight: 0 false() weight: 0 #top(x1) weight: 0 div(x1,x2) weight: 0 geq(x1,x2) weight: 0 true() weight: 0 proper(x1) weight: 0 ok(x1) weight: (/ 1 2) + x1 0() weight: 0 if(x1,x2,x3) weight: 0 #s(x1) weight: x1 mark(x1) weight: (/ 1 2) + x1 #minus(x1,x2) weight: 0 #proper(x1) weight: 0 active(x1) weight: 0 #if(x1,x2,x3) weight: 0 #active(x1) weight: 0 Usable rules: { } Removed DPs: #4 #17 Number of SCCs: 5, DPs: 19, edges: 121 SCC { #2 #15 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded. #div(x1,x2) status: [] precedence above: s(x1) status: [x1] precedence above: minus false geq true mark active minus(x1,x2) status: [x1] precedence above: mark #geq(x1,x2) status: [x2,x1] precedence above: top(x1) status: [] precedence above: false() status: [] precedence above: #top(x1) status: [x1] precedence above: div(x1,x2) status: [x1] precedence above: s minus false geq true 0 if mark active geq(x1,x2) status: [x1] precedence above: false true mark true() status: [] precedence above: proper(x1) status: x1 ok(x1) status: x1 0() status: [] precedence above: if(x1,x2,x3) status: [x3,x2,x1] precedence above: mark #s(x1) status: [] precedence above: mark(x1) status: [x1] precedence above: #minus(x1,x2) status: [x2] precedence above: #proper(x1) status: [] precedence above: active(x1) status: x1 #if(x1,x2,x3) status: [x1,x3,x2] precedence above: #active(x1) status: [] precedence above: Usable rules: { 1..28 } Removed DPs: #2 Number of SCCs: 5, DPs: 18, edges: 118 SCC { #15 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #div(x1,x2) weight: 0 s(x1) weight: x1 minus(x1,x2) weight: (/ 1 2) #geq(x1,x2) weight: 0 top(x1) weight: 0 false() weight: 0 #top(x1) weight: x1 div(x1,x2) weight: x1 geq(x1,x2) weight: (/ 1 2) true() weight: 0 proper(x1) weight: (/ 1 2) ok(x1) weight: (/ 1 2) 0() weight: 0 if(x1,x2,x3) weight: x1 #s(x1) weight: 0 mark(x1) weight: (/ 1 4) #minus(x1,x2) weight: 0 #proper(x1) weight: 0 active(x1) weight: (/ 1 4) #if(x1,x2,x3) weight: 0 #active(x1) weight: 0 Usable rules: { 1..15 24..28 } Removed DPs: #15 Number of SCCs: 4, DPs: 17, edges: 117 SCC { #14 #30 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #div(x1,x2) weight: x2 s(x1) weight: x1 minus(x1,x2) weight: (/ 1 4) #geq(x1,x2) weight: 0 top(x1) weight: 0 false() weight: 0 #top(x1) weight: 0 div(x1,x2) weight: x1 geq(x1,x2) weight: (/ 1 4) true() weight: 0 proper(x1) weight: (/ 1 2) ok(x1) weight: (/ 1 2) + x1 0() weight: 0 if(x1,x2,x3) weight: x1 #s(x1) weight: 0 mark(x1) weight: (/ 1 4) #minus(x1,x2) weight: 0 #proper(x1) weight: 0 active(x1) weight: (/ 1 4) #if(x1,x2,x3) weight: 0 #active(x1) weight: 0 Usable rules: { } Removed DPs: #30 Number of SCCs: 5, DPs: 16, edges: 114 SCC { #14 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #div(x1,x2) weight: x1 s(x1) weight: x1 minus(x1,x2) weight: (/ 1 4) #geq(x1,x2) weight: 0 top(x1) weight: 0 false() weight: 0 #top(x1) weight: 0 div(x1,x2) weight: x1 geq(x1,x2) weight: (/ 1 4) true() weight: 0 proper(x1) weight: (/ 1 2) ok(x1) weight: (/ 1 2) + x1 0() weight: 0 if(x1,x2,x3) weight: x1 #s(x1) weight: 0 mark(x1) weight: (/ 1 4) + x1 #minus(x1,x2) weight: 0 #proper(x1) weight: 0 active(x1) weight: (/ 1 2) #if(x1,x2,x3) weight: 0 #active(x1) weight: 0 Usable rules: { } Removed DPs: #14 Number of SCCs: 4, DPs: 15, edges: 113 SCC { #6 #13 #24 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #div(x1,x2) weight: 0 s(x1) weight: x1 minus(x1,x2) weight: (/ 1 4) #geq(x1,x2) weight: 0 top(x1) weight: 0 false() weight: 0 #top(x1) weight: 0 div(x1,x2) weight: x1 geq(x1,x2) weight: (/ 1 4) true() weight: 0 proper(x1) weight: (/ 1 2) ok(x1) weight: (/ 1 2) + x1 0() weight: 0 if(x1,x2,x3) weight: (/ 1 4) + x1 #s(x1) weight: 0 mark(x1) weight: (/ 1 4) + x1 #minus(x1,x2) weight: 0 #proper(x1) weight: 0 active(x1) weight: (/ 3 4) #if(x1,x2,x3) weight: 0 #active(x1) weight: x1 Usable rules: { } Removed DPs: #13 Number of SCCs: 5, DPs: 14, edges: 108 SCC { #6 #24 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #div(x1,x2) weight: 0 s(x1) weight: x1 minus(x1,x2) weight: (/ 1 4) #geq(x1,x2) weight: 0 top(x1) weight: 0 false() weight: 0 #top(x1) weight: 0 div(x1,x2) weight: (/ 1 4) + x1 geq(x1,x2) weight: (/ 1 4) true() weight: 0 proper(x1) weight: (/ 1 2) ok(x1) weight: (/ 1 2) + x1 0() weight: 0 if(x1,x2,x3) weight: (/ 1 4) + x1 #s(x1) weight: 0 mark(x1) weight: (/ 1 4) + x1 #minus(x1,x2) weight: 0 #proper(x1) weight: 0 active(x1) weight: (/ 3 4) #if(x1,x2,x3) weight: 0 #active(x1) weight: x1 Usable rules: { } Removed DPs: #6 Number of SCCs: 5, DPs: 13, edges: 105 SCC { #24 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #div(x1,x2) weight: 0 s(x1) weight: (/ 1 4) + x1 minus(x1,x2) weight: (/ 1 4) #geq(x1,x2) weight: 0 top(x1) weight: 0 false() weight: 0 #top(x1) weight: 0 div(x1,x2) weight: (/ 1 4) + x1 geq(x1,x2) weight: (/ 1 4) true() weight: 0 proper(x1) weight: (/ 1 2) ok(x1) weight: (/ 1 2) + x1 0() weight: 0 if(x1,x2,x3) weight: (/ 1 4) + x1 #s(x1) weight: 0 mark(x1) weight: (/ 1 4) + x1 #minus(x1,x2) weight: 0 #proper(x1) weight: 0 active(x1) weight: (/ 3 4) #if(x1,x2,x3) weight: 0 #active(x1) weight: x1 Usable rules: { } Removed DPs: #24 Number of SCCs: 4, DPs: 12, edges: 104 SCC { #26 #38 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #div(x1,x2) weight: 0 s(x1) weight: (/ 1 4) + x1 minus(x1,x2) weight: (/ 1 4) #geq(x1,x2) weight: 0 top(x1) weight: 0 false() weight: 0 #top(x1) weight: 0 div(x1,x2) weight: (/ 1 4) + x1 geq(x1,x2) weight: (/ 1 4) true() weight: 0 proper(x1) weight: (/ 1 4) ok(x1) weight: (/ 1 4) + x1 0() weight: 0 if(x1,x2,x3) weight: (/ 1 4) + x1 #s(x1) weight: 0 mark(x1) weight: (/ 1 4) + x1 #minus(x1,x2) weight: 0 #proper(x1) weight: 0 active(x1) weight: (/ 3 4) #if(x1,x2,x3) weight: x2 #active(x1) weight: 0 Usable rules: { } Removed DPs: #26 Number of SCCs: 5, DPs: 11, edges: 101 SCC { #38 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #div(x1,x2) weight: 0 s(x1) weight: (/ 1 4) + x1 minus(x1,x2) weight: (/ 1 4) #geq(x1,x2) weight: 0 top(x1) weight: 0 false() weight: 0 #top(x1) weight: 0 div(x1,x2) weight: (/ 1 4) + x1 geq(x1,x2) weight: (/ 1 4) true() weight: 0 proper(x1) weight: (/ 1 4) ok(x1) weight: (/ 1 4) + x1 0() weight: 0 if(x1,x2,x3) weight: (/ 1 4) + x1 #s(x1) weight: 0 mark(x1) weight: (/ 1 4) + x1 #minus(x1,x2) weight: 0 #proper(x1) weight: 0 active(x1) weight: (/ 3 4) #if(x1,x2,x3) weight: x1 #active(x1) weight: 0 Usable rules: { } Removed DPs: #38 Number of SCCs: 4, DPs: 10, edges: 100 SCC { #9..11 #28 #29 #32 #33 #36 #37 #40 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #div(x1,x2) weight: 0 s(x1) weight: (/ 1 8) + x1 minus(x1,x2) weight: (/ 1 8) + x1 + x2 #geq(x1,x2) weight: 0 top(x1) weight: 0 false() weight: 0 #top(x1) weight: 0 div(x1,x2) weight: (/ 1 8) + x1 + x2 geq(x1,x2) weight: (/ 1 8) + x1 + x2 true() weight: 0 proper(x1) weight: 0 ok(x1) weight: x1 0() weight: 0 if(x1,x2,x3) weight: (/ 1 8) + x1 + x2 + x3 #s(x1) weight: 0 mark(x1) weight: (/ 1 8) + x1 #minus(x1,x2) weight: 0 #proper(x1) weight: x1 active(x1) weight: (/ 7 8) #if(x1,x2,x3) weight: 0 #active(x1) weight: 0 Usable rules: { } Removed DPs: #9..11 #28 #29 #32 #33 #36 #37 #40 Number of SCCs: 4, DPs: 0, edges: 0 YES