Input TRS: 1: le(|0|(),y) -> true() 2: le(s(x),|0|()) -> false() 3: le(s(x),s(y)) -> le(x,y) 4: minus(x,|0|()) -> x 5: minus(s(x),s(y)) -> minus(x,y) 6: gcd(|0|(),y) -> y 7: gcd(s(x),|0|()) -> s(x) 8: gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) 9: if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) 10: if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) 11: gcdL(nil()) -> |0|() 12: gcdL(cons(x,nil())) -> x 13: gcdL(cons(x,cons(y,xs))) -> gcdL(cons(gcd(x,y),xs)) 14: gcdL(cons(x,cons(y,xs))) ->= gcdL(cons(y,cons(x,xs))) Number of strict rules: 13 Direct Order(PosReal,>,Poly) ... failed. Freezing gcdL 1: le(|0|(),y) -> true() 2: le(s(x),|0|()) -> false() 3: le(s(x),s(y)) -> le(x,y) 4: minus(x,|0|()) -> x 5: minus(s(x),s(y)) -> minus(x,y) 6: gcd(|0|(),y) -> y 7: gcd(s(x),|0|()) -> s(x) 8: gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) 9: if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) 10: if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) 11: gcdL❆1_nil() -> |0|() 12: gcdL❆1_cons(x,nil()) -> x 13: gcdL❆1_cons(x,cons(y,xs)) -> gcdL❆1_cons(gcd(x,y),xs) 14: gcdL❆1_cons(x,cons(y,xs)) ->= gcdL❆1_cons(y,cons(x,xs)) 15: gcdL(cons(_1,_2)) ->= gcdL❆1_cons(_1,_2) 16: gcdL(nil()) ->= gcdL❆1_nil() Number of strict rules: 13 Direct Order(PosReal,>,Poly) ... failed. Dependency Pairs: #1: #gcdL❆1_cons(x,cons(y,xs)) -> #gcdL❆1_cons(gcd(x,y),xs) #2: #gcdL❆1_cons(x,cons(y,xs)) -> #gcd(x,y) #3: #if_gcd(true(),s(x),s(y)) -> #gcd(minus(x,y),s(y)) #4: #if_gcd(true(),s(x),s(y)) -> #minus(x,y) #5: #gcdL❆1_cons(x,cons(y,xs)) ->? #gcdL❆1_cons(y,cons(x,xs)) #6: #if_gcd(false(),s(x),s(y)) -> #gcd(minus(y,x),s(x)) #7: #if_gcd(false(),s(x),s(y)) -> #minus(y,x) #8: #minus(s(x),s(y)) -> #minus(x,y) #9: #gcdL(nil()) ->? #gcdL❆1_nil() #10: #le(s(x),s(y)) -> #le(x,y) #11: #gcd(s(x),s(y)) -> #if_gcd(le(y,x),s(x),s(y)) #12: #gcd(s(x),s(y)) -> #le(y,x) #13: #gcdL(cons(_1,_2)) ->? #gcdL❆1_cons(_1,_2) Number of SCCs: 4, DPs: 7, edges: 10 SCC { #10 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 le(x1,x2) weight: 0 s(x1) weight: (/ 1 2) + x1 #le(x1,x2) weight: x2 minus(x1,x2) weight: 0 gcd(x1,x2) weight: 0 false() weight: 0 #gcdL❆1_nil() weight: 0 true() weight: 0 #gcdL(x1) weight: 0 #gcdL❆1_cons(x1,x2) weight: 0 nil() weight: 0 #minus(x1,x2) weight: 0 gcdL(x1) weight: 0 cons(x1,x2) weight: 0 if_gcd(x1,x2,x3) weight: 0 #if_gcd(x1,x2,x3) weight: 0 gcdL❆1_nil() weight: 0 gcdL❆1_cons(x1,x2) weight: 0 #gcd(x1,x2) weight: 0 Usable rules: { } Removed DPs: #10 Number of SCCs: 3, DPs: 6, edges: 9 SCC { #8 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 le(x1,x2) weight: 0 s(x1) weight: (/ 1 2) + x1 #le(x1,x2) weight: 0 minus(x1,x2) weight: 0 gcd(x1,x2) weight: 0 false() weight: 0 #gcdL❆1_nil() weight: 0 true() weight: 0 #gcdL(x1) weight: 0 #gcdL❆1_cons(x1,x2) weight: 0 nil() weight: 0 #minus(x1,x2) weight: x2 gcdL(x1) weight: 0 cons(x1,x2) weight: 0 if_gcd(x1,x2,x3) weight: 0 #if_gcd(x1,x2,x3) weight: 0 gcdL❆1_nil() weight: 0 gcdL❆1_cons(x1,x2) weight: 0 #gcd(x1,x2) weight: 0 Usable rules: { } Removed DPs: #8 Number of SCCs: 2, DPs: 5, edges: 8 SCC { #1 #5 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 le(x1,x2) weight: (/ 1 4) s(x1) weight: (/ 1 4) + x1 #le(x1,x2) weight: 0 minus(x1,x2) weight: (/ 3 4) + x2 gcd(x1,x2) weight: (/ 1 4) + x1 + x2 false() weight: 0 #gcdL❆1_nil() weight: 0 true() weight: 0 #gcdL(x1) weight: 0 #gcdL❆1_cons(x1,x2) weight: x2 nil() weight: 0 #minus(x1,x2) weight: 0 gcdL(x1) weight: 0 cons(x1,x2) weight: (/ 1 4) + x2 if_gcd(x1,x2,x3) weight: (/ 1 2) + x2 + x3 #if_gcd(x1,x2,x3) weight: 0 gcdL❆1_nil() weight: 0 gcdL❆1_cons(x1,x2) weight: 0 #gcd(x1,x2) weight: 0 Usable rules: { } Removed DPs: #1 Number of SCCs: 2, DPs: 4, edges: 5 SCC { #5 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed. Removing edges: failed. Finding a loop... failed. MAYBE