0 Prolog
↳1 PrologToTRSTransformerProof (⇒, 67 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QDPSizeChangeProof (⇔, 0 ms)
↳11 YES
↳12 QDP
↳13 UsableRulesProof (⇔, 0 ms)
↳14 QDP
↳15 QDPSizeChangeProof (⇔, 0 ms)
↳16 YES
↳17 QDP
↳18 QDPOrderProof (⇔, 110 ms)
↳19 QDP
↳20 DependencyGraphProof (⇔, 0 ms)
↳21 TRUE
f2_in([]) → f2_out1([])
f2_in(T9) → U1(f25_in(T9), T9)
U1(f25_out1(X13, T12, X14, X15, T13), T9) → f2_out1(.(T12, T13))
f36_in(.(T33, T34)) → f36_out1([], T33, T34)
f36_in(.(T42, T43)) → U2(f36_in(T43), .(T42, T43))
U2(f36_out1(X53, T44, X54), .(T42, T43)) → f36_out1(.(T42, X53), T44, X54)
f69_in([], T58) → f69_out1(T58)
f69_in(.(T65, T66), T67) → U3(f69_in(T66, T67), .(T65, T66), T67)
U3(f69_out1(X82), .(T65, T66), T67) → f69_out1(.(T65, X82))
f25_in(T9) → U4(f36_in(T9), T9)
U4(f36_out1(T18, T12, T19), T9) → U5(f37_in(T18, T19), T9, T18, T12, T19)
U5(f37_out1(X15, T20), T9, T18, T12, T19) → f25_out1(T18, T12, T19, X15, T20)
f37_in(T18, T19) → U6(f69_in(T18, T19), T18, T19)
U6(f69_out1(T51), T18, T19) → U7(f2_in(T51), T18, T19, T51)
U7(f2_out1(T20), T18, T19, T51) → f37_out1(T51, T20)
F2_IN(T9) → U11(f25_in(T9), T9)
F2_IN(T9) → F25_IN(T9)
F36_IN(.(T42, T43)) → U21(f36_in(T43), .(T42, T43))
F36_IN(.(T42, T43)) → F36_IN(T43)
F69_IN(.(T65, T66), T67) → U31(f69_in(T66, T67), .(T65, T66), T67)
F69_IN(.(T65, T66), T67) → F69_IN(T66, T67)
F25_IN(T9) → U41(f36_in(T9), T9)
F25_IN(T9) → F36_IN(T9)
U41(f36_out1(T18, T12, T19), T9) → U51(f37_in(T18, T19), T9, T18, T12, T19)
U41(f36_out1(T18, T12, T19), T9) → F37_IN(T18, T19)
F37_IN(T18, T19) → U61(f69_in(T18, T19), T18, T19)
F37_IN(T18, T19) → F69_IN(T18, T19)
U61(f69_out1(T51), T18, T19) → U71(f2_in(T51), T18, T19, T51)
U61(f69_out1(T51), T18, T19) → F2_IN(T51)
f2_in([]) → f2_out1([])
f2_in(T9) → U1(f25_in(T9), T9)
U1(f25_out1(X13, T12, X14, X15, T13), T9) → f2_out1(.(T12, T13))
f36_in(.(T33, T34)) → f36_out1([], T33, T34)
f36_in(.(T42, T43)) → U2(f36_in(T43), .(T42, T43))
U2(f36_out1(X53, T44, X54), .(T42, T43)) → f36_out1(.(T42, X53), T44, X54)
f69_in([], T58) → f69_out1(T58)
f69_in(.(T65, T66), T67) → U3(f69_in(T66, T67), .(T65, T66), T67)
U3(f69_out1(X82), .(T65, T66), T67) → f69_out1(.(T65, X82))
f25_in(T9) → U4(f36_in(T9), T9)
U4(f36_out1(T18, T12, T19), T9) → U5(f37_in(T18, T19), T9, T18, T12, T19)
U5(f37_out1(X15, T20), T9, T18, T12, T19) → f25_out1(T18, T12, T19, X15, T20)
f37_in(T18, T19) → U6(f69_in(T18, T19), T18, T19)
U6(f69_out1(T51), T18, T19) → U7(f2_in(T51), T18, T19, T51)
U7(f2_out1(T20), T18, T19, T51) → f37_out1(T51, T20)
F69_IN(.(T65, T66), T67) → F69_IN(T66, T67)
f2_in([]) → f2_out1([])
f2_in(T9) → U1(f25_in(T9), T9)
U1(f25_out1(X13, T12, X14, X15, T13), T9) → f2_out1(.(T12, T13))
f36_in(.(T33, T34)) → f36_out1([], T33, T34)
f36_in(.(T42, T43)) → U2(f36_in(T43), .(T42, T43))
U2(f36_out1(X53, T44, X54), .(T42, T43)) → f36_out1(.(T42, X53), T44, X54)
f69_in([], T58) → f69_out1(T58)
f69_in(.(T65, T66), T67) → U3(f69_in(T66, T67), .(T65, T66), T67)
U3(f69_out1(X82), .(T65, T66), T67) → f69_out1(.(T65, X82))
f25_in(T9) → U4(f36_in(T9), T9)
U4(f36_out1(T18, T12, T19), T9) → U5(f37_in(T18, T19), T9, T18, T12, T19)
U5(f37_out1(X15, T20), T9, T18, T12, T19) → f25_out1(T18, T12, T19, X15, T20)
f37_in(T18, T19) → U6(f69_in(T18, T19), T18, T19)
U6(f69_out1(T51), T18, T19) → U7(f2_in(T51), T18, T19, T51)
U7(f2_out1(T20), T18, T19, T51) → f37_out1(T51, T20)
F69_IN(.(T65, T66), T67) → F69_IN(T66, T67)
From the DPs we obtained the following set of size-change graphs:
F36_IN(.(T42, T43)) → F36_IN(T43)
f2_in([]) → f2_out1([])
f2_in(T9) → U1(f25_in(T9), T9)
U1(f25_out1(X13, T12, X14, X15, T13), T9) → f2_out1(.(T12, T13))
f36_in(.(T33, T34)) → f36_out1([], T33, T34)
f36_in(.(T42, T43)) → U2(f36_in(T43), .(T42, T43))
U2(f36_out1(X53, T44, X54), .(T42, T43)) → f36_out1(.(T42, X53), T44, X54)
f69_in([], T58) → f69_out1(T58)
f69_in(.(T65, T66), T67) → U3(f69_in(T66, T67), .(T65, T66), T67)
U3(f69_out1(X82), .(T65, T66), T67) → f69_out1(.(T65, X82))
f25_in(T9) → U4(f36_in(T9), T9)
U4(f36_out1(T18, T12, T19), T9) → U5(f37_in(T18, T19), T9, T18, T12, T19)
U5(f37_out1(X15, T20), T9, T18, T12, T19) → f25_out1(T18, T12, T19, X15, T20)
f37_in(T18, T19) → U6(f69_in(T18, T19), T18, T19)
U6(f69_out1(T51), T18, T19) → U7(f2_in(T51), T18, T19, T51)
U7(f2_out1(T20), T18, T19, T51) → f37_out1(T51, T20)
F36_IN(.(T42, T43)) → F36_IN(T43)
From the DPs we obtained the following set of size-change graphs:
F2_IN(T9) → F25_IN(T9)
F25_IN(T9) → U41(f36_in(T9), T9)
U41(f36_out1(T18, T12, T19), T9) → F37_IN(T18, T19)
F37_IN(T18, T19) → U61(f69_in(T18, T19), T18, T19)
U61(f69_out1(T51), T18, T19) → F2_IN(T51)
f2_in([]) → f2_out1([])
f2_in(T9) → U1(f25_in(T9), T9)
U1(f25_out1(X13, T12, X14, X15, T13), T9) → f2_out1(.(T12, T13))
f36_in(.(T33, T34)) → f36_out1([], T33, T34)
f36_in(.(T42, T43)) → U2(f36_in(T43), .(T42, T43))
U2(f36_out1(X53, T44, X54), .(T42, T43)) → f36_out1(.(T42, X53), T44, X54)
f69_in([], T58) → f69_out1(T58)
f69_in(.(T65, T66), T67) → U3(f69_in(T66, T67), .(T65, T66), T67)
U3(f69_out1(X82), .(T65, T66), T67) → f69_out1(.(T65, X82))
f25_in(T9) → U4(f36_in(T9), T9)
U4(f36_out1(T18, T12, T19), T9) → U5(f37_in(T18, T19), T9, T18, T12, T19)
U5(f37_out1(X15, T20), T9, T18, T12, T19) → f25_out1(T18, T12, T19, X15, T20)
f37_in(T18, T19) → U6(f69_in(T18, T19), T18, T19)
U6(f69_out1(T51), T18, T19) → U7(f2_in(T51), T18, T19, T51)
U7(f2_out1(T20), T18, T19, T51) → f37_out1(T51, T20)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F25_IN(T9) → U41(f36_in(T9), T9)
POL(.(x1, x2)) = 1 + x2
POL(F25_IN(x1)) = 1 + x1
POL(F2_IN(x1)) = 1 + x1
POL(F37_IN(x1, x2)) = x1 + x2
POL(U2(x1, x2)) = 1 + x1
POL(U3(x1, x2, x3)) = 1 + x1
POL(U41(x1, x2)) = x1
POL(U61(x1, x2, x3)) = x1
POL([]) = 1
POL(f36_in(x1)) = x1
POL(f36_out1(x1, x2, x3)) = x1 + x3
POL(f69_in(x1, x2)) = x1 + x2
POL(f69_out1(x1)) = 1 + x1
f36_in(.(T33, T34)) → f36_out1([], T33, T34)
f36_in(.(T42, T43)) → U2(f36_in(T43), .(T42, T43))
f69_in([], T58) → f69_out1(T58)
f69_in(.(T65, T66), T67) → U3(f69_in(T66, T67), .(T65, T66), T67)
U2(f36_out1(X53, T44, X54), .(T42, T43)) → f36_out1(.(T42, X53), T44, X54)
U3(f69_out1(X82), .(T65, T66), T67) → f69_out1(.(T65, X82))
F2_IN(T9) → F25_IN(T9)
U41(f36_out1(T18, T12, T19), T9) → F37_IN(T18, T19)
F37_IN(T18, T19) → U61(f69_in(T18, T19), T18, T19)
U61(f69_out1(T51), T18, T19) → F2_IN(T51)
f2_in([]) → f2_out1([])
f2_in(T9) → U1(f25_in(T9), T9)
U1(f25_out1(X13, T12, X14, X15, T13), T9) → f2_out1(.(T12, T13))
f36_in(.(T33, T34)) → f36_out1([], T33, T34)
f36_in(.(T42, T43)) → U2(f36_in(T43), .(T42, T43))
U2(f36_out1(X53, T44, X54), .(T42, T43)) → f36_out1(.(T42, X53), T44, X54)
f69_in([], T58) → f69_out1(T58)
f69_in(.(T65, T66), T67) → U3(f69_in(T66, T67), .(T65, T66), T67)
U3(f69_out1(X82), .(T65, T66), T67) → f69_out1(.(T65, X82))
f25_in(T9) → U4(f36_in(T9), T9)
U4(f36_out1(T18, T12, T19), T9) → U5(f37_in(T18, T19), T9, T18, T12, T19)
U5(f37_out1(X15, T20), T9, T18, T12, T19) → f25_out1(T18, T12, T19, X15, T20)
f37_in(T18, T19) → U6(f69_in(T18, T19), T18, T19)
U6(f69_out1(T51), T18, T19) → U7(f2_in(T51), T18, T19, T51)
U7(f2_out1(T20), T18, T19, T51) → f37_out1(T51, T20)