0 Prolog
↳1 PrologToTRSTransformerProof (⇒, 69 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 2 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 QDP
↳7 QDPOrderProof (⇔, 150 ms)
↳8 QDP
↳9 QDPOrderProof (⇔, 219 ms)
↳10 QDP
↳11 DependencyGraphProof (⇔, 0 ms)
↳12 QDP
↳13 UsableRulesProof (⇔, 0 ms)
↳14 QDP
↳15 UsableRulesReductionPairsProof (⇔, 0 ms)
↳16 QDP
↳17 DependencyGraphProof (⇔, 0 ms)
↳18 TRUE
f2_in(.(T6, [])) → f2_out1
f2_in(.(s(s(T19)), .(T20, T21))) → U1(f22_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
U1(f22_out1, .(s(s(T19)), .(T20, T21))) → f2_out1
f2_in(.(0, T30)) → U2(f2_in(T30), .(0, T30))
U2(f2_out1, .(0, T30)) → f2_out1
f22_in(T19, T20, T21) → U3(f2_in(.(T19, .(T20, T21))), T19, T20, T21)
U3(f2_out1, T19, T20, T21) → U4(f2_in(.(s(s(s(s(T20)))), T21)), T19, T20, T21)
U4(f2_out1, T19, T20, T21) → f22_out1
F2_IN(.(s(s(T19)), .(T20, T21))) → U11(f22_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
F2_IN(.(s(s(T19)), .(T20, T21))) → F22_IN(T19, T20, T21)
F2_IN(.(0, T30)) → U21(f2_in(T30), .(0, T30))
F2_IN(.(0, T30)) → F2_IN(T30)
F22_IN(T19, T20, T21) → U31(f2_in(.(T19, .(T20, T21))), T19, T20, T21)
F22_IN(T19, T20, T21) → F2_IN(.(T19, .(T20, T21)))
U31(f2_out1, T19, T20, T21) → U41(f2_in(.(s(s(s(s(T20)))), T21)), T19, T20, T21)
U31(f2_out1, T19, T20, T21) → F2_IN(.(s(s(s(s(T20)))), T21))
f2_in(.(T6, [])) → f2_out1
f2_in(.(s(s(T19)), .(T20, T21))) → U1(f22_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
U1(f22_out1, .(s(s(T19)), .(T20, T21))) → f2_out1
f2_in(.(0, T30)) → U2(f2_in(T30), .(0, T30))
U2(f2_out1, .(0, T30)) → f2_out1
f22_in(T19, T20, T21) → U3(f2_in(.(T19, .(T20, T21))), T19, T20, T21)
U3(f2_out1, T19, T20, T21) → U4(f2_in(.(s(s(s(s(T20)))), T21)), T19, T20, T21)
U4(f2_out1, T19, T20, T21) → f22_out1
F2_IN(.(s(s(T19)), .(T20, T21))) → F22_IN(T19, T20, T21)
F22_IN(T19, T20, T21) → U31(f2_in(.(T19, .(T20, T21))), T19, T20, T21)
U31(f2_out1, T19, T20, T21) → F2_IN(.(s(s(s(s(T20)))), T21))
F22_IN(T19, T20, T21) → F2_IN(.(T19, .(T20, T21)))
F2_IN(.(0, T30)) → F2_IN(T30)
f2_in(.(T6, [])) → f2_out1
f2_in(.(s(s(T19)), .(T20, T21))) → U1(f22_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
U1(f22_out1, .(s(s(T19)), .(T20, T21))) → f2_out1
f2_in(.(0, T30)) → U2(f2_in(T30), .(0, T30))
U2(f2_out1, .(0, T30)) → f2_out1
f22_in(T19, T20, T21) → U3(f2_in(.(T19, .(T20, T21))), T19, T20, T21)
U3(f2_out1, T19, T20, T21) → U4(f2_in(.(s(s(s(s(T20)))), T21)), T19, T20, T21)
U4(f2_out1, T19, T20, T21) → f22_out1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F2_IN(.(0, T30)) → F2_IN(T30)
POL(.(x1, x2)) = x1 + x2
POL(0) = 1
POL(F22_IN(x1, x2, x3)) = x1 + x2 + x3
POL(F2_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([]) = 1
POL(f22_in(x1, x2, x3)) = 0
POL(f22_out1) = 0
POL(f2_in(x1)) = 1 + x1
POL(f2_out1) = 1
POL(s(x1)) = x1
F2_IN(.(s(s(T19)), .(T20, T21))) → F22_IN(T19, T20, T21)
F22_IN(T19, T20, T21) → U31(f2_in(.(T19, .(T20, T21))), T19, T20, T21)
U31(f2_out1, T19, T20, T21) → F2_IN(.(s(s(s(s(T20)))), T21))
F22_IN(T19, T20, T21) → F2_IN(.(T19, .(T20, T21)))
f2_in(.(T6, [])) → f2_out1
f2_in(.(s(s(T19)), .(T20, T21))) → U1(f22_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
U1(f22_out1, .(s(s(T19)), .(T20, T21))) → f2_out1
f2_in(.(0, T30)) → U2(f2_in(T30), .(0, T30))
U2(f2_out1, .(0, T30)) → f2_out1
f22_in(T19, T20, T21) → U3(f2_in(.(T19, .(T20, T21))), T19, T20, T21)
U3(f2_out1, T19, T20, T21) → U4(f2_in(.(s(s(s(s(T20)))), T21)), T19, T20, T21)
U4(f2_out1, T19, T20, T21) → f22_out1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U31(f2_out1, T19, T20, T21) → F2_IN(.(s(s(s(s(T20)))), T21))
POL( U31(x1, ..., x4) ) = 2x4 + 2
POL( f2_in(x1) ) = max{0, -2}
POL( .(x1, x2) ) = x2 + 1
POL( s(x1) ) = 0
POL( U1(x1, x2) ) = max{0, 2x1 - 1}
POL( f22_in(x1, ..., x3) ) = x3
POL( 0 ) = 2
POL( U2(x1, x2) ) = 1
POL( f22_out1 ) = 2
POL( f2_out1 ) = 0
POL( U3(x1, ..., x4) ) = max{0, x2 + x4 - 2}
POL( U4(x1, ..., x4) ) = max{0, x1 - 1}
POL( [] ) = 0
POL( F2_IN(x1) ) = max{0, 2x1 - 2}
POL( F22_IN(x1, ..., x3) ) = 2x3 + 2
F2_IN(.(s(s(T19)), .(T20, T21))) → F22_IN(T19, T20, T21)
F22_IN(T19, T20, T21) → U31(f2_in(.(T19, .(T20, T21))), T19, T20, T21)
F22_IN(T19, T20, T21) → F2_IN(.(T19, .(T20, T21)))
f2_in(.(T6, [])) → f2_out1
f2_in(.(s(s(T19)), .(T20, T21))) → U1(f22_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
U1(f22_out1, .(s(s(T19)), .(T20, T21))) → f2_out1
f2_in(.(0, T30)) → U2(f2_in(T30), .(0, T30))
U2(f2_out1, .(0, T30)) → f2_out1
f22_in(T19, T20, T21) → U3(f2_in(.(T19, .(T20, T21))), T19, T20, T21)
U3(f2_out1, T19, T20, T21) → U4(f2_in(.(s(s(s(s(T20)))), T21)), T19, T20, T21)
U4(f2_out1, T19, T20, T21) → f22_out1
F22_IN(T19, T20, T21) → F2_IN(.(T19, .(T20, T21)))
F2_IN(.(s(s(T19)), .(T20, T21))) → F22_IN(T19, T20, T21)
f2_in(.(T6, [])) → f2_out1
f2_in(.(s(s(T19)), .(T20, T21))) → U1(f22_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
U1(f22_out1, .(s(s(T19)), .(T20, T21))) → f2_out1
f2_in(.(0, T30)) → U2(f2_in(T30), .(0, T30))
U2(f2_out1, .(0, T30)) → f2_out1
f22_in(T19, T20, T21) → U3(f2_in(.(T19, .(T20, T21))), T19, T20, T21)
U3(f2_out1, T19, T20, T21) → U4(f2_in(.(s(s(s(s(T20)))), T21)), T19, T20, T21)
U4(f2_out1, T19, T20, T21) → f22_out1
F22_IN(T19, T20, T21) → F2_IN(.(T19, .(T20, T21)))
F2_IN(.(s(s(T19)), .(T20, T21))) → F22_IN(T19, T20, T21)
No rules are removed from R.
F2_IN(.(s(s(T19)), .(T20, T21))) → F22_IN(T19, T20, T21)
POL(.(x1, x2)) = x1 + x2
POL(F22_IN(x1, x2, x3)) = x1 + x2 + x3
POL(F2_IN(x1)) = x1
POL(s(x1)) = 2·x1
F22_IN(T19, T20, T21) → F2_IN(.(T19, .(T20, T21)))