0 Prolog
↳1 PrologToTRSTransformerProof (⇒, 73 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 (⇔, 98 ms)
↳19 QDP
↳20 DependencyGraphProof (⇔, 0 ms)
↳21 TRUE
f3_in([]) → f3_out1([])
f3_in(T9) → U1(f23_in(T9), T9)
U1(f23_out1(X13, T12, X14, X15, T13), T9) → f3_out1(.(T12, T13))
f40_in(.(T33, T34)) → f40_out1([], T33, T34)
f40_in(.(T42, T43)) → U2(f40_in(T43), .(T42, T43))
U2(f40_out1(X53, T44, X54), .(T42, T43)) → f40_out1(.(T42, X53), T44, X54)
f71_in([], T58) → f71_out1(T58)
f71_in(.(T65, T66), T67) → U3(f71_in(T66, T67), .(T65, T66), T67)
U3(f71_out1(X82), .(T65, T66), T67) → f71_out1(.(T65, X82))
f23_in(T9) → U4(f40_in(T9), T9)
U4(f40_out1(T18, T12, T19), T9) → U5(f41_in(T18, T19), T9, T18, T12, T19)
U5(f41_out1(X15, T20), T9, T18, T12, T19) → f23_out1(T18, T12, T19, X15, T20)
f41_in(T18, T19) → U6(f71_in(T18, T19), T18, T19)
U6(f71_out1(T51), T18, T19) → U7(f3_in(T51), T18, T19, T51)
U7(f3_out1(T20), T18, T19, T51) → f41_out1(T51, T20)
F3_IN(T9) → U11(f23_in(T9), T9)
F3_IN(T9) → F23_IN(T9)
F40_IN(.(T42, T43)) → U21(f40_in(T43), .(T42, T43))
F40_IN(.(T42, T43)) → F40_IN(T43)
F71_IN(.(T65, T66), T67) → U31(f71_in(T66, T67), .(T65, T66), T67)
F71_IN(.(T65, T66), T67) → F71_IN(T66, T67)
F23_IN(T9) → U41(f40_in(T9), T9)
F23_IN(T9) → F40_IN(T9)
U41(f40_out1(T18, T12, T19), T9) → U51(f41_in(T18, T19), T9, T18, T12, T19)
U41(f40_out1(T18, T12, T19), T9) → F41_IN(T18, T19)
F41_IN(T18, T19) → U61(f71_in(T18, T19), T18, T19)
F41_IN(T18, T19) → F71_IN(T18, T19)
U61(f71_out1(T51), T18, T19) → U71(f3_in(T51), T18, T19, T51)
U61(f71_out1(T51), T18, T19) → F3_IN(T51)
f3_in([]) → f3_out1([])
f3_in(T9) → U1(f23_in(T9), T9)
U1(f23_out1(X13, T12, X14, X15, T13), T9) → f3_out1(.(T12, T13))
f40_in(.(T33, T34)) → f40_out1([], T33, T34)
f40_in(.(T42, T43)) → U2(f40_in(T43), .(T42, T43))
U2(f40_out1(X53, T44, X54), .(T42, T43)) → f40_out1(.(T42, X53), T44, X54)
f71_in([], T58) → f71_out1(T58)
f71_in(.(T65, T66), T67) → U3(f71_in(T66, T67), .(T65, T66), T67)
U3(f71_out1(X82), .(T65, T66), T67) → f71_out1(.(T65, X82))
f23_in(T9) → U4(f40_in(T9), T9)
U4(f40_out1(T18, T12, T19), T9) → U5(f41_in(T18, T19), T9, T18, T12, T19)
U5(f41_out1(X15, T20), T9, T18, T12, T19) → f23_out1(T18, T12, T19, X15, T20)
f41_in(T18, T19) → U6(f71_in(T18, T19), T18, T19)
U6(f71_out1(T51), T18, T19) → U7(f3_in(T51), T18, T19, T51)
U7(f3_out1(T20), T18, T19, T51) → f41_out1(T51, T20)
F71_IN(.(T65, T66), T67) → F71_IN(T66, T67)
f3_in([]) → f3_out1([])
f3_in(T9) → U1(f23_in(T9), T9)
U1(f23_out1(X13, T12, X14, X15, T13), T9) → f3_out1(.(T12, T13))
f40_in(.(T33, T34)) → f40_out1([], T33, T34)
f40_in(.(T42, T43)) → U2(f40_in(T43), .(T42, T43))
U2(f40_out1(X53, T44, X54), .(T42, T43)) → f40_out1(.(T42, X53), T44, X54)
f71_in([], T58) → f71_out1(T58)
f71_in(.(T65, T66), T67) → U3(f71_in(T66, T67), .(T65, T66), T67)
U3(f71_out1(X82), .(T65, T66), T67) → f71_out1(.(T65, X82))
f23_in(T9) → U4(f40_in(T9), T9)
U4(f40_out1(T18, T12, T19), T9) → U5(f41_in(T18, T19), T9, T18, T12, T19)
U5(f41_out1(X15, T20), T9, T18, T12, T19) → f23_out1(T18, T12, T19, X15, T20)
f41_in(T18, T19) → U6(f71_in(T18, T19), T18, T19)
U6(f71_out1(T51), T18, T19) → U7(f3_in(T51), T18, T19, T51)
U7(f3_out1(T20), T18, T19, T51) → f41_out1(T51, T20)
F71_IN(.(T65, T66), T67) → F71_IN(T66, T67)
From the DPs we obtained the following set of size-change graphs:
F40_IN(.(T42, T43)) → F40_IN(T43)
f3_in([]) → f3_out1([])
f3_in(T9) → U1(f23_in(T9), T9)
U1(f23_out1(X13, T12, X14, X15, T13), T9) → f3_out1(.(T12, T13))
f40_in(.(T33, T34)) → f40_out1([], T33, T34)
f40_in(.(T42, T43)) → U2(f40_in(T43), .(T42, T43))
U2(f40_out1(X53, T44, X54), .(T42, T43)) → f40_out1(.(T42, X53), T44, X54)
f71_in([], T58) → f71_out1(T58)
f71_in(.(T65, T66), T67) → U3(f71_in(T66, T67), .(T65, T66), T67)
U3(f71_out1(X82), .(T65, T66), T67) → f71_out1(.(T65, X82))
f23_in(T9) → U4(f40_in(T9), T9)
U4(f40_out1(T18, T12, T19), T9) → U5(f41_in(T18, T19), T9, T18, T12, T19)
U5(f41_out1(X15, T20), T9, T18, T12, T19) → f23_out1(T18, T12, T19, X15, T20)
f41_in(T18, T19) → U6(f71_in(T18, T19), T18, T19)
U6(f71_out1(T51), T18, T19) → U7(f3_in(T51), T18, T19, T51)
U7(f3_out1(T20), T18, T19, T51) → f41_out1(T51, T20)
F40_IN(.(T42, T43)) → F40_IN(T43)
From the DPs we obtained the following set of size-change graphs:
F3_IN(T9) → F23_IN(T9)
F23_IN(T9) → U41(f40_in(T9), T9)
U41(f40_out1(T18, T12, T19), T9) → F41_IN(T18, T19)
F41_IN(T18, T19) → U61(f71_in(T18, T19), T18, T19)
U61(f71_out1(T51), T18, T19) → F3_IN(T51)
f3_in([]) → f3_out1([])
f3_in(T9) → U1(f23_in(T9), T9)
U1(f23_out1(X13, T12, X14, X15, T13), T9) → f3_out1(.(T12, T13))
f40_in(.(T33, T34)) → f40_out1([], T33, T34)
f40_in(.(T42, T43)) → U2(f40_in(T43), .(T42, T43))
U2(f40_out1(X53, T44, X54), .(T42, T43)) → f40_out1(.(T42, X53), T44, X54)
f71_in([], T58) → f71_out1(T58)
f71_in(.(T65, T66), T67) → U3(f71_in(T66, T67), .(T65, T66), T67)
U3(f71_out1(X82), .(T65, T66), T67) → f71_out1(.(T65, X82))
f23_in(T9) → U4(f40_in(T9), T9)
U4(f40_out1(T18, T12, T19), T9) → U5(f41_in(T18, T19), T9, T18, T12, T19)
U5(f41_out1(X15, T20), T9, T18, T12, T19) → f23_out1(T18, T12, T19, X15, T20)
f41_in(T18, T19) → U6(f71_in(T18, T19), T18, T19)
U6(f71_out1(T51), T18, T19) → U7(f3_in(T51), T18, T19, T51)
U7(f3_out1(T20), T18, T19, T51) → f41_out1(T51, T20)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F23_IN(T9) → U41(f40_in(T9), T9)
POL(.(x1, x2)) = 1 + x2
POL(F23_IN(x1)) = 1 + x1
POL(F3_IN(x1)) = 1 + x1
POL(F41_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(f40_in(x1)) = x1
POL(f40_out1(x1, x2, x3)) = x1 + x3
POL(f71_in(x1, x2)) = x1 + x2
POL(f71_out1(x1)) = 1 + x1
f40_in(.(T33, T34)) → f40_out1([], T33, T34)
f40_in(.(T42, T43)) → U2(f40_in(T43), .(T42, T43))
f71_in([], T58) → f71_out1(T58)
f71_in(.(T65, T66), T67) → U3(f71_in(T66, T67), .(T65, T66), T67)
U2(f40_out1(X53, T44, X54), .(T42, T43)) → f40_out1(.(T42, X53), T44, X54)
U3(f71_out1(X82), .(T65, T66), T67) → f71_out1(.(T65, X82))
F3_IN(T9) → F23_IN(T9)
U41(f40_out1(T18, T12, T19), T9) → F41_IN(T18, T19)
F41_IN(T18, T19) → U61(f71_in(T18, T19), T18, T19)
U61(f71_out1(T51), T18, T19) → F3_IN(T51)
f3_in([]) → f3_out1([])
f3_in(T9) → U1(f23_in(T9), T9)
U1(f23_out1(X13, T12, X14, X15, T13), T9) → f3_out1(.(T12, T13))
f40_in(.(T33, T34)) → f40_out1([], T33, T34)
f40_in(.(T42, T43)) → U2(f40_in(T43), .(T42, T43))
U2(f40_out1(X53, T44, X54), .(T42, T43)) → f40_out1(.(T42, X53), T44, X54)
f71_in([], T58) → f71_out1(T58)
f71_in(.(T65, T66), T67) → U3(f71_in(T66, T67), .(T65, T66), T67)
U3(f71_out1(X82), .(T65, T66), T67) → f71_out1(.(T65, X82))
f23_in(T9) → U4(f40_in(T9), T9)
U4(f40_out1(T18, T12, T19), T9) → U5(f41_in(T18, T19), T9, T18, T12, T19)
U5(f41_out1(X15, T20), T9, T18, T12, T19) → f23_out1(T18, T12, T19, X15, T20)
f41_in(T18, T19) → U6(f71_in(T18, T19), T18, T19)
U6(f71_out1(T51), T18, T19) → U7(f3_in(T51), T18, T19, T51)
U7(f3_out1(T20), T18, T19, T51) → f41_out1(T51, T20)