↳ PROLOG
↳ PrologToPiTRSProof
With regard to the inferred argument filtering the predicates were used in the following modes:
normal2: (b,f)
rewrite2: (b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
normal_2_in_ga2(F, N) -> if_normal_2_in_1_ga3(F, N, rewrite_2_in_ga2(F, F1))
rewrite_2_in_ga2(op_22(op_22(A, B), C), op_22(A, op_22(B, C))) -> rewrite_2_out_ga2(op_22(op_22(A, B), C), op_22(A, op_22(B, C)))
rewrite_2_in_ga2(op_22(A, op_22(B, C)), op_22(A, L)) -> if_rewrite_2_in_1_ga5(A, B, C, L, rewrite_2_in_ga2(op_22(B, C), L))
if_rewrite_2_in_1_ga5(A, B, C, L, rewrite_2_out_ga2(op_22(B, C), L)) -> rewrite_2_out_ga2(op_22(A, op_22(B, C)), op_22(A, L))
if_normal_2_in_1_ga3(F, N, rewrite_2_out_ga2(F, F1)) -> if_normal_2_in_2_ga4(F, N, F1, normal_2_in_ga2(F1, N))
normal_2_in_ga2(F, F) -> normal_2_out_ga2(F, F)
if_normal_2_in_2_ga4(F, N, F1, normal_2_out_ga2(F1, N)) -> normal_2_out_ga2(F, N)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
normal_2_in_ga2(F, N) -> if_normal_2_in_1_ga3(F, N, rewrite_2_in_ga2(F, F1))
rewrite_2_in_ga2(op_22(op_22(A, B), C), op_22(A, op_22(B, C))) -> rewrite_2_out_ga2(op_22(op_22(A, B), C), op_22(A, op_22(B, C)))
rewrite_2_in_ga2(op_22(A, op_22(B, C)), op_22(A, L)) -> if_rewrite_2_in_1_ga5(A, B, C, L, rewrite_2_in_ga2(op_22(B, C), L))
if_rewrite_2_in_1_ga5(A, B, C, L, rewrite_2_out_ga2(op_22(B, C), L)) -> rewrite_2_out_ga2(op_22(A, op_22(B, C)), op_22(A, L))
if_normal_2_in_1_ga3(F, N, rewrite_2_out_ga2(F, F1)) -> if_normal_2_in_2_ga4(F, N, F1, normal_2_in_ga2(F1, N))
normal_2_in_ga2(F, F) -> normal_2_out_ga2(F, F)
if_normal_2_in_2_ga4(F, N, F1, normal_2_out_ga2(F1, N)) -> normal_2_out_ga2(F, N)
NORMAL_2_IN_GA2(F, N) -> IF_NORMAL_2_IN_1_GA3(F, N, rewrite_2_in_ga2(F, F1))
NORMAL_2_IN_GA2(F, N) -> REWRITE_2_IN_GA2(F, F1)
REWRITE_2_IN_GA2(op_22(A, op_22(B, C)), op_22(A, L)) -> IF_REWRITE_2_IN_1_GA5(A, B, C, L, rewrite_2_in_ga2(op_22(B, C), L))
REWRITE_2_IN_GA2(op_22(A, op_22(B, C)), op_22(A, L)) -> REWRITE_2_IN_GA2(op_22(B, C), L)
IF_NORMAL_2_IN_1_GA3(F, N, rewrite_2_out_ga2(F, F1)) -> IF_NORMAL_2_IN_2_GA4(F, N, F1, normal_2_in_ga2(F1, N))
IF_NORMAL_2_IN_1_GA3(F, N, rewrite_2_out_ga2(F, F1)) -> NORMAL_2_IN_GA2(F1, N)
normal_2_in_ga2(F, N) -> if_normal_2_in_1_ga3(F, N, rewrite_2_in_ga2(F, F1))
rewrite_2_in_ga2(op_22(op_22(A, B), C), op_22(A, op_22(B, C))) -> rewrite_2_out_ga2(op_22(op_22(A, B), C), op_22(A, op_22(B, C)))
rewrite_2_in_ga2(op_22(A, op_22(B, C)), op_22(A, L)) -> if_rewrite_2_in_1_ga5(A, B, C, L, rewrite_2_in_ga2(op_22(B, C), L))
if_rewrite_2_in_1_ga5(A, B, C, L, rewrite_2_out_ga2(op_22(B, C), L)) -> rewrite_2_out_ga2(op_22(A, op_22(B, C)), op_22(A, L))
if_normal_2_in_1_ga3(F, N, rewrite_2_out_ga2(F, F1)) -> if_normal_2_in_2_ga4(F, N, F1, normal_2_in_ga2(F1, N))
normal_2_in_ga2(F, F) -> normal_2_out_ga2(F, F)
if_normal_2_in_2_ga4(F, N, F1, normal_2_out_ga2(F1, N)) -> normal_2_out_ga2(F, N)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
NORMAL_2_IN_GA2(F, N) -> IF_NORMAL_2_IN_1_GA3(F, N, rewrite_2_in_ga2(F, F1))
NORMAL_2_IN_GA2(F, N) -> REWRITE_2_IN_GA2(F, F1)
REWRITE_2_IN_GA2(op_22(A, op_22(B, C)), op_22(A, L)) -> IF_REWRITE_2_IN_1_GA5(A, B, C, L, rewrite_2_in_ga2(op_22(B, C), L))
REWRITE_2_IN_GA2(op_22(A, op_22(B, C)), op_22(A, L)) -> REWRITE_2_IN_GA2(op_22(B, C), L)
IF_NORMAL_2_IN_1_GA3(F, N, rewrite_2_out_ga2(F, F1)) -> IF_NORMAL_2_IN_2_GA4(F, N, F1, normal_2_in_ga2(F1, N))
IF_NORMAL_2_IN_1_GA3(F, N, rewrite_2_out_ga2(F, F1)) -> NORMAL_2_IN_GA2(F1, N)
normal_2_in_ga2(F, N) -> if_normal_2_in_1_ga3(F, N, rewrite_2_in_ga2(F, F1))
rewrite_2_in_ga2(op_22(op_22(A, B), C), op_22(A, op_22(B, C))) -> rewrite_2_out_ga2(op_22(op_22(A, B), C), op_22(A, op_22(B, C)))
rewrite_2_in_ga2(op_22(A, op_22(B, C)), op_22(A, L)) -> if_rewrite_2_in_1_ga5(A, B, C, L, rewrite_2_in_ga2(op_22(B, C), L))
if_rewrite_2_in_1_ga5(A, B, C, L, rewrite_2_out_ga2(op_22(B, C), L)) -> rewrite_2_out_ga2(op_22(A, op_22(B, C)), op_22(A, L))
if_normal_2_in_1_ga3(F, N, rewrite_2_out_ga2(F, F1)) -> if_normal_2_in_2_ga4(F, N, F1, normal_2_in_ga2(F1, N))
normal_2_in_ga2(F, F) -> normal_2_out_ga2(F, F)
if_normal_2_in_2_ga4(F, N, F1, normal_2_out_ga2(F1, N)) -> normal_2_out_ga2(F, N)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
REWRITE_2_IN_GA2(op_22(A, op_22(B, C)), op_22(A, L)) -> REWRITE_2_IN_GA2(op_22(B, C), L)
normal_2_in_ga2(F, N) -> if_normal_2_in_1_ga3(F, N, rewrite_2_in_ga2(F, F1))
rewrite_2_in_ga2(op_22(op_22(A, B), C), op_22(A, op_22(B, C))) -> rewrite_2_out_ga2(op_22(op_22(A, B), C), op_22(A, op_22(B, C)))
rewrite_2_in_ga2(op_22(A, op_22(B, C)), op_22(A, L)) -> if_rewrite_2_in_1_ga5(A, B, C, L, rewrite_2_in_ga2(op_22(B, C), L))
if_rewrite_2_in_1_ga5(A, B, C, L, rewrite_2_out_ga2(op_22(B, C), L)) -> rewrite_2_out_ga2(op_22(A, op_22(B, C)), op_22(A, L))
if_normal_2_in_1_ga3(F, N, rewrite_2_out_ga2(F, F1)) -> if_normal_2_in_2_ga4(F, N, F1, normal_2_in_ga2(F1, N))
normal_2_in_ga2(F, F) -> normal_2_out_ga2(F, F)
if_normal_2_in_2_ga4(F, N, F1, normal_2_out_ga2(F1, N)) -> normal_2_out_ga2(F, N)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
REWRITE_2_IN_GA2(op_22(A, op_22(B, C)), op_22(A, L)) -> REWRITE_2_IN_GA2(op_22(B, C), L)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
REWRITE_2_IN_GA1(op_22(A, op_22(B, C))) -> REWRITE_2_IN_GA1(op_22(B, C))
From the DPs we obtained the following set of size-change graphs:
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
NORMAL_2_IN_GA2(F, N) -> IF_NORMAL_2_IN_1_GA3(F, N, rewrite_2_in_ga2(F, F1))
IF_NORMAL_2_IN_1_GA3(F, N, rewrite_2_out_ga2(F, F1)) -> NORMAL_2_IN_GA2(F1, N)
normal_2_in_ga2(F, N) -> if_normal_2_in_1_ga3(F, N, rewrite_2_in_ga2(F, F1))
rewrite_2_in_ga2(op_22(op_22(A, B), C), op_22(A, op_22(B, C))) -> rewrite_2_out_ga2(op_22(op_22(A, B), C), op_22(A, op_22(B, C)))
rewrite_2_in_ga2(op_22(A, op_22(B, C)), op_22(A, L)) -> if_rewrite_2_in_1_ga5(A, B, C, L, rewrite_2_in_ga2(op_22(B, C), L))
if_rewrite_2_in_1_ga5(A, B, C, L, rewrite_2_out_ga2(op_22(B, C), L)) -> rewrite_2_out_ga2(op_22(A, op_22(B, C)), op_22(A, L))
if_normal_2_in_1_ga3(F, N, rewrite_2_out_ga2(F, F1)) -> if_normal_2_in_2_ga4(F, N, F1, normal_2_in_ga2(F1, N))
normal_2_in_ga2(F, F) -> normal_2_out_ga2(F, F)
if_normal_2_in_2_ga4(F, N, F1, normal_2_out_ga2(F1, N)) -> normal_2_out_ga2(F, N)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
NORMAL_2_IN_GA2(F, N) -> IF_NORMAL_2_IN_1_GA3(F, N, rewrite_2_in_ga2(F, F1))
IF_NORMAL_2_IN_1_GA3(F, N, rewrite_2_out_ga2(F, F1)) -> NORMAL_2_IN_GA2(F1, N)
rewrite_2_in_ga2(op_22(op_22(A, B), C), op_22(A, op_22(B, C))) -> rewrite_2_out_ga2(op_22(op_22(A, B), C), op_22(A, op_22(B, C)))
rewrite_2_in_ga2(op_22(A, op_22(B, C)), op_22(A, L)) -> if_rewrite_2_in_1_ga5(A, B, C, L, rewrite_2_in_ga2(op_22(B, C), L))
if_rewrite_2_in_1_ga5(A, B, C, L, rewrite_2_out_ga2(op_22(B, C), L)) -> rewrite_2_out_ga2(op_22(A, op_22(B, C)), op_22(A, L))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
NORMAL_2_IN_GA1(F) -> IF_NORMAL_2_IN_1_GA1(rewrite_2_in_ga1(F))
IF_NORMAL_2_IN_1_GA1(rewrite_2_out_ga1(F1)) -> NORMAL_2_IN_GA1(F1)
rewrite_2_in_ga1(op_22(op_22(A, B), C)) -> rewrite_2_out_ga1(op_22(A, op_22(B, C)))
rewrite_2_in_ga1(op_22(A, op_22(B, C))) -> if_rewrite_2_in_1_ga2(A, rewrite_2_in_ga1(op_22(B, C)))
if_rewrite_2_in_1_ga2(A, rewrite_2_out_ga1(L)) -> rewrite_2_out_ga1(op_22(A, L))
rewrite_2_in_ga1(x0)
if_rewrite_2_in_1_ga2(x0, x1)
IF_NORMAL_2_IN_1_GA1(rewrite_2_out_ga1(F1)) -> NORMAL_2_IN_GA1(F1)
rewrite_2_in_ga1(op_22(op_22(A, B), C)) -> rewrite_2_out_ga1(op_22(A, op_22(B, C)))
POL(IF_NORMAL_2_IN_1_GA1(x1)) = x1
POL(if_rewrite_2_in_1_ga2(x1, x2)) = 2 + 2·x1 + x2
POL(op_22(x1, x2)) = 2 + 2·x1 + x2
POL(rewrite_2_out_ga1(x1)) = 1 + x1
POL(rewrite_2_in_ga1(x1)) = x1
POL(NORMAL_2_IN_GA1(x1)) = x1
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
NORMAL_2_IN_GA1(F) -> IF_NORMAL_2_IN_1_GA1(rewrite_2_in_ga1(F))
rewrite_2_in_ga1(op_22(A, op_22(B, C))) -> if_rewrite_2_in_1_ga2(A, rewrite_2_in_ga1(op_22(B, C)))
if_rewrite_2_in_1_ga2(A, rewrite_2_out_ga1(L)) -> rewrite_2_out_ga1(op_22(A, L))
rewrite_2_in_ga1(x0)
if_rewrite_2_in_1_ga2(x0, x1)
rewrite_2_in_ga1(op_22(A, op_22(B, C))) -> if_rewrite_2_in_1_ga2(A, rewrite_2_in_ga1(op_22(B, C)))
POL(IF_NORMAL_2_IN_1_GA1(x1)) = x1
POL(if_rewrite_2_in_1_ga2(x1, x2)) = 1 + x1 + x2
POL(op_22(x1, x2)) = 1 + x1 + x2
POL(rewrite_2_out_ga1(x1)) = x1
POL(rewrite_2_in_ga1(x1)) = 1 + 2·x1
POL(NORMAL_2_IN_GA1(x1)) = 1 + 2·x1
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ DependencyGraphProof
NORMAL_2_IN_GA1(F) -> IF_NORMAL_2_IN_1_GA1(rewrite_2_in_ga1(F))
if_rewrite_2_in_1_ga2(A, rewrite_2_out_ga1(L)) -> rewrite_2_out_ga1(op_22(A, L))
rewrite_2_in_ga1(x0)
if_rewrite_2_in_1_ga2(x0, x1)