↳ PROLOG
↳ PrologToPiTRSProof
With regard to the inferred argument filtering the predicates were used in the following modes:
tc2: (b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
tc_2_in_ga2(X, X) -> tc_2_out_ga2(X, X)
tc_2_in_ga2(X, Y) -> if_tc_2_in_1_ga3(X, Y, p_2_in_ga2(X, Z))
p_2_in_ga2(a_0, b_0) -> p_2_out_ga2(a_0, b_0)
p_2_in_ga2(b_0, c_0) -> p_2_out_ga2(b_0, c_0)
if_tc_2_in_1_ga3(X, Y, p_2_out_ga2(X, Z)) -> if_tc_2_in_2_ga4(X, Y, Z, tc_2_in_ga2(Z, Y))
if_tc_2_in_2_ga4(X, Y, Z, tc_2_out_ga2(Z, Y)) -> tc_2_out_ga2(X, Y)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
tc_2_in_ga2(X, X) -> tc_2_out_ga2(X, X)
tc_2_in_ga2(X, Y) -> if_tc_2_in_1_ga3(X, Y, p_2_in_ga2(X, Z))
p_2_in_ga2(a_0, b_0) -> p_2_out_ga2(a_0, b_0)
p_2_in_ga2(b_0, c_0) -> p_2_out_ga2(b_0, c_0)
if_tc_2_in_1_ga3(X, Y, p_2_out_ga2(X, Z)) -> if_tc_2_in_2_ga4(X, Y, Z, tc_2_in_ga2(Z, Y))
if_tc_2_in_2_ga4(X, Y, Z, tc_2_out_ga2(Z, Y)) -> tc_2_out_ga2(X, Y)
TC_2_IN_GA2(X, Y) -> IF_TC_2_IN_1_GA3(X, Y, p_2_in_ga2(X, Z))
TC_2_IN_GA2(X, Y) -> P_2_IN_GA2(X, Z)
IF_TC_2_IN_1_GA3(X, Y, p_2_out_ga2(X, Z)) -> IF_TC_2_IN_2_GA4(X, Y, Z, tc_2_in_ga2(Z, Y))
IF_TC_2_IN_1_GA3(X, Y, p_2_out_ga2(X, Z)) -> TC_2_IN_GA2(Z, Y)
tc_2_in_ga2(X, X) -> tc_2_out_ga2(X, X)
tc_2_in_ga2(X, Y) -> if_tc_2_in_1_ga3(X, Y, p_2_in_ga2(X, Z))
p_2_in_ga2(a_0, b_0) -> p_2_out_ga2(a_0, b_0)
p_2_in_ga2(b_0, c_0) -> p_2_out_ga2(b_0, c_0)
if_tc_2_in_1_ga3(X, Y, p_2_out_ga2(X, Z)) -> if_tc_2_in_2_ga4(X, Y, Z, tc_2_in_ga2(Z, Y))
if_tc_2_in_2_ga4(X, Y, Z, tc_2_out_ga2(Z, Y)) -> tc_2_out_ga2(X, Y)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
TC_2_IN_GA2(X, Y) -> IF_TC_2_IN_1_GA3(X, Y, p_2_in_ga2(X, Z))
TC_2_IN_GA2(X, Y) -> P_2_IN_GA2(X, Z)
IF_TC_2_IN_1_GA3(X, Y, p_2_out_ga2(X, Z)) -> IF_TC_2_IN_2_GA4(X, Y, Z, tc_2_in_ga2(Z, Y))
IF_TC_2_IN_1_GA3(X, Y, p_2_out_ga2(X, Z)) -> TC_2_IN_GA2(Z, Y)
tc_2_in_ga2(X, X) -> tc_2_out_ga2(X, X)
tc_2_in_ga2(X, Y) -> if_tc_2_in_1_ga3(X, Y, p_2_in_ga2(X, Z))
p_2_in_ga2(a_0, b_0) -> p_2_out_ga2(a_0, b_0)
p_2_in_ga2(b_0, c_0) -> p_2_out_ga2(b_0, c_0)
if_tc_2_in_1_ga3(X, Y, p_2_out_ga2(X, Z)) -> if_tc_2_in_2_ga4(X, Y, Z, tc_2_in_ga2(Z, Y))
if_tc_2_in_2_ga4(X, Y, Z, tc_2_out_ga2(Z, Y)) -> tc_2_out_ga2(X, Y)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
TC_2_IN_GA2(X, Y) -> IF_TC_2_IN_1_GA3(X, Y, p_2_in_ga2(X, Z))
IF_TC_2_IN_1_GA3(X, Y, p_2_out_ga2(X, Z)) -> TC_2_IN_GA2(Z, Y)
tc_2_in_ga2(X, X) -> tc_2_out_ga2(X, X)
tc_2_in_ga2(X, Y) -> if_tc_2_in_1_ga3(X, Y, p_2_in_ga2(X, Z))
p_2_in_ga2(a_0, b_0) -> p_2_out_ga2(a_0, b_0)
p_2_in_ga2(b_0, c_0) -> p_2_out_ga2(b_0, c_0)
if_tc_2_in_1_ga3(X, Y, p_2_out_ga2(X, Z)) -> if_tc_2_in_2_ga4(X, Y, Z, tc_2_in_ga2(Z, Y))
if_tc_2_in_2_ga4(X, Y, Z, tc_2_out_ga2(Z, Y)) -> tc_2_out_ga2(X, Y)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
TC_2_IN_GA2(X, Y) -> IF_TC_2_IN_1_GA3(X, Y, p_2_in_ga2(X, Z))
IF_TC_2_IN_1_GA3(X, Y, p_2_out_ga2(X, Z)) -> TC_2_IN_GA2(Z, Y)
p_2_in_ga2(a_0, b_0) -> p_2_out_ga2(a_0, b_0)
p_2_in_ga2(b_0, c_0) -> p_2_out_ga2(b_0, c_0)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
TC_2_IN_GA1(X) -> IF_TC_2_IN_1_GA1(p_2_in_ga1(X))
IF_TC_2_IN_1_GA1(p_2_out_ga1(Z)) -> TC_2_IN_GA1(Z)
p_2_in_ga1(a_0) -> p_2_out_ga1(b_0)
p_2_in_ga1(b_0) -> p_2_out_ga1(c_0)
p_2_in_ga1(x0)
IF_TC_2_IN_1_GA1(p_2_out_ga1(Z)) -> TC_2_IN_GA1(Z)
p_2_in_ga1(a_0) -> p_2_out_ga1(b_0)
p_2_in_ga1(b_0) -> p_2_out_ga1(c_0)
POL(p_2_out_ga1(x1)) = 1 + 2·x1
POL(a_0) = 2
POL(IF_TC_2_IN_1_GA1(x1)) = x1
POL(c_0) = 0
POL(TC_2_IN_GA1(x1)) = 2·x1
POL(p_2_in_ga1(x1)) = 2·x1
POL(b_0) = 1
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ DependencyGraphProof
TC_2_IN_GA1(X) -> IF_TC_2_IN_1_GA1(p_2_in_ga1(X))
p_2_in_ga1(x0)