0 Prolog
↳1 PrologToTRSTransformerProof (⇒, 53 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 QDP
↳7 QDPOrderProof (⇔, 161 ms)
↳8 QDP
↳9 QDPOrderProof (⇔, 234 ms)
↳10 QDP
↳11 DependencyGraphProof (⇔, 0 ms)
↳12 QDP
↳13 UsableRulesProof (⇔, 0 ms)
↳14 QDP
↳15 UsableRulesReductionPairsProof (⇔, 21 ms)
↳16 QDP
↳17 DependencyGraphProof (⇔, 0 ms)
↳18 TRUE
f3_in(cons(T6, nil)) → f3_out1
f3_in(cons(s(s(T19)), cons(T20, T21))) → U1(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
U1(f34_out1, cons(s(s(T19)), cons(T20, T21))) → f3_out1
f3_in(cons(0, T30)) → U2(f3_in(T30), cons(0, T30))
U2(f3_out1, cons(0, T30)) → f3_out1
f34_in(T19, T20, T21) → U3(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U3(f3_out1, T19, T20, T21) → U4(f3_in(cons(s(s(s(s(T20)))), T21)), T19, T20, T21)
U4(f3_out1, T19, T20, T21) → f34_out1
F3_IN(cons(s(s(T19)), cons(T20, T21))) → U11(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
F3_IN(cons(s(s(T19)), cons(T20, T21))) → F34_IN(T19, T20, T21)
F3_IN(cons(0, T30)) → U21(f3_in(T30), cons(0, T30))
F3_IN(cons(0, T30)) → F3_IN(T30)
F34_IN(T19, T20, T21) → U31(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
F34_IN(T19, T20, T21) → F3_IN(cons(T19, cons(T20, T21)))
U31(f3_out1, T19, T20, T21) → U41(f3_in(cons(s(s(s(s(T20)))), T21)), T19, T20, T21)
U31(f3_out1, T19, T20, T21) → F3_IN(cons(s(s(s(s(T20)))), T21))
f3_in(cons(T6, nil)) → f3_out1
f3_in(cons(s(s(T19)), cons(T20, T21))) → U1(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
U1(f34_out1, cons(s(s(T19)), cons(T20, T21))) → f3_out1
f3_in(cons(0, T30)) → U2(f3_in(T30), cons(0, T30))
U2(f3_out1, cons(0, T30)) → f3_out1
f34_in(T19, T20, T21) → U3(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U3(f3_out1, T19, T20, T21) → U4(f3_in(cons(s(s(s(s(T20)))), T21)), T19, T20, T21)
U4(f3_out1, T19, T20, T21) → f34_out1
F3_IN(cons(s(s(T19)), cons(T20, T21))) → F34_IN(T19, T20, T21)
F34_IN(T19, T20, T21) → U31(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U31(f3_out1, T19, T20, T21) → F3_IN(cons(s(s(s(s(T20)))), T21))
F34_IN(T19, T20, T21) → F3_IN(cons(T19, cons(T20, T21)))
F3_IN(cons(0, T30)) → F3_IN(T30)
f3_in(cons(T6, nil)) → f3_out1
f3_in(cons(s(s(T19)), cons(T20, T21))) → U1(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
U1(f34_out1, cons(s(s(T19)), cons(T20, T21))) → f3_out1
f3_in(cons(0, T30)) → U2(f3_in(T30), cons(0, T30))
U2(f3_out1, cons(0, T30)) → f3_out1
f34_in(T19, T20, T21) → U3(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U3(f3_out1, T19, T20, T21) → U4(f3_in(cons(s(s(s(s(T20)))), T21)), T19, T20, T21)
U4(f3_out1, T19, T20, T21) → f34_out1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F3_IN(cons(0, T30)) → F3_IN(T30)
POL(0) = 1
POL(F34_IN(x1, x2, x3)) = x1 + x2 + x3
POL(F3_IN(x1)) = x1
POL(U1(x1, x2)) = 0
POL(U2(x1, x2)) = 0
POL(U3(x1, x2, x3, x4)) = 0
POL(U31(x1, x2, x3, x4)) = x2 + x3 + x4
POL(U4(x1, x2, x3, x4)) = 0
POL(cons(x1, x2)) = x1 + x2
POL(f34_in(x1, x2, x3)) = 0
POL(f34_out1) = 0
POL(f3_in(x1)) = 1 + x1
POL(f3_out1) = 1
POL(nil) = 1
POL(s(x1)) = x1
F3_IN(cons(s(s(T19)), cons(T20, T21))) → F34_IN(T19, T20, T21)
F34_IN(T19, T20, T21) → U31(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U31(f3_out1, T19, T20, T21) → F3_IN(cons(s(s(s(s(T20)))), T21))
F34_IN(T19, T20, T21) → F3_IN(cons(T19, cons(T20, T21)))
f3_in(cons(T6, nil)) → f3_out1
f3_in(cons(s(s(T19)), cons(T20, T21))) → U1(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
U1(f34_out1, cons(s(s(T19)), cons(T20, T21))) → f3_out1
f3_in(cons(0, T30)) → U2(f3_in(T30), cons(0, T30))
U2(f3_out1, cons(0, T30)) → f3_out1
f34_in(T19, T20, T21) → U3(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U3(f3_out1, T19, T20, T21) → U4(f3_in(cons(s(s(s(s(T20)))), T21)), T19, T20, T21)
U4(f3_out1, T19, T20, T21) → f34_out1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U31(f3_out1, T19, T20, T21) → F3_IN(cons(s(s(s(s(T20)))), T21))
POL( U31(x1, ..., x4) ) = 2x4 + 2
POL( f3_in(x1) ) = max{0, -2}
POL( cons(x1, x2) ) = x2 + 1
POL( s(x1) ) = 0
POL( U1(x1, x2) ) = max{0, 2x1 - 1}
POL( f34_in(x1, ..., x3) ) = x3
POL( 0 ) = 2
POL( U2(x1, x2) ) = 1
POL( f34_out1 ) = 2
POL( f3_out1 ) = 0
POL( U3(x1, ..., x4) ) = max{0, x2 + x4 - 2}
POL( U4(x1, ..., x4) ) = max{0, x1 - 1}
POL( nil ) = 0
POL( F3_IN(x1) ) = max{0, 2x1 - 2}
POL( F34_IN(x1, ..., x3) ) = 2x3 + 2
F3_IN(cons(s(s(T19)), cons(T20, T21))) → F34_IN(T19, T20, T21)
F34_IN(T19, T20, T21) → U31(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
F34_IN(T19, T20, T21) → F3_IN(cons(T19, cons(T20, T21)))
f3_in(cons(T6, nil)) → f3_out1
f3_in(cons(s(s(T19)), cons(T20, T21))) → U1(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
U1(f34_out1, cons(s(s(T19)), cons(T20, T21))) → f3_out1
f3_in(cons(0, T30)) → U2(f3_in(T30), cons(0, T30))
U2(f3_out1, cons(0, T30)) → f3_out1
f34_in(T19, T20, T21) → U3(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U3(f3_out1, T19, T20, T21) → U4(f3_in(cons(s(s(s(s(T20)))), T21)), T19, T20, T21)
U4(f3_out1, T19, T20, T21) → f34_out1
F34_IN(T19, T20, T21) → F3_IN(cons(T19, cons(T20, T21)))
F3_IN(cons(s(s(T19)), cons(T20, T21))) → F34_IN(T19, T20, T21)
f3_in(cons(T6, nil)) → f3_out1
f3_in(cons(s(s(T19)), cons(T20, T21))) → U1(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
U1(f34_out1, cons(s(s(T19)), cons(T20, T21))) → f3_out1
f3_in(cons(0, T30)) → U2(f3_in(T30), cons(0, T30))
U2(f3_out1, cons(0, T30)) → f3_out1
f34_in(T19, T20, T21) → U3(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U3(f3_out1, T19, T20, T21) → U4(f3_in(cons(s(s(s(s(T20)))), T21)), T19, T20, T21)
U4(f3_out1, T19, T20, T21) → f34_out1
F34_IN(T19, T20, T21) → F3_IN(cons(T19, cons(T20, T21)))
F3_IN(cons(s(s(T19)), cons(T20, T21))) → F34_IN(T19, T20, T21)
No rules are removed from R.
F3_IN(cons(s(s(T19)), cons(T20, T21))) → F34_IN(T19, T20, T21)
POL(F34_IN(x1, x2, x3)) = x1 + x2 + x3
POL(F3_IN(x1)) = x1
POL(cons(x1, x2)) = x1 + x2
POL(s(x1)) = 2·x1
F34_IN(T19, T20, T21) → F3_IN(cons(T19, cons(T20, T21)))