↳ PROLOG
↳ PrologToPiTRSProof
With regard to the inferred argument filtering the predicates were used in the following modes:
flat2: (b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
flat_2_in_ga2(niltree_0, nil_0) -> flat_2_out_ga2(niltree_0, nil_0)
flat_2_in_ga2(tree_33(X, niltree_0, T), cons_22(X, Xs)) -> if_flat_2_in_1_ga4(X, T, Xs, flat_2_in_ga2(T, Xs))
flat_2_in_ga2(tree_33(X, tree_33(Y, T1, T2), T3), Xs) -> if_flat_2_in_2_ga7(X, Y, T1, T2, T3, Xs, flat_2_in_ga2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs))
if_flat_2_in_2_ga7(X, Y, T1, T2, T3, Xs, flat_2_out_ga2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs)) -> flat_2_out_ga2(tree_33(X, tree_33(Y, T1, T2), T3), Xs)
if_flat_2_in_1_ga4(X, T, Xs, flat_2_out_ga2(T, Xs)) -> flat_2_out_ga2(tree_33(X, niltree_0, T), cons_22(X, Xs))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
flat_2_in_ga2(niltree_0, nil_0) -> flat_2_out_ga2(niltree_0, nil_0)
flat_2_in_ga2(tree_33(X, niltree_0, T), cons_22(X, Xs)) -> if_flat_2_in_1_ga4(X, T, Xs, flat_2_in_ga2(T, Xs))
flat_2_in_ga2(tree_33(X, tree_33(Y, T1, T2), T3), Xs) -> if_flat_2_in_2_ga7(X, Y, T1, T2, T3, Xs, flat_2_in_ga2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs))
if_flat_2_in_2_ga7(X, Y, T1, T2, T3, Xs, flat_2_out_ga2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs)) -> flat_2_out_ga2(tree_33(X, tree_33(Y, T1, T2), T3), Xs)
if_flat_2_in_1_ga4(X, T, Xs, flat_2_out_ga2(T, Xs)) -> flat_2_out_ga2(tree_33(X, niltree_0, T), cons_22(X, Xs))
FLAT_2_IN_GA2(tree_33(X, niltree_0, T), cons_22(X, Xs)) -> IF_FLAT_2_IN_1_GA4(X, T, Xs, flat_2_in_ga2(T, Xs))
FLAT_2_IN_GA2(tree_33(X, niltree_0, T), cons_22(X, Xs)) -> FLAT_2_IN_GA2(T, Xs)
FLAT_2_IN_GA2(tree_33(X, tree_33(Y, T1, T2), T3), Xs) -> IF_FLAT_2_IN_2_GA7(X, Y, T1, T2, T3, Xs, flat_2_in_ga2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs))
FLAT_2_IN_GA2(tree_33(X, tree_33(Y, T1, T2), T3), Xs) -> FLAT_2_IN_GA2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs)
flat_2_in_ga2(niltree_0, nil_0) -> flat_2_out_ga2(niltree_0, nil_0)
flat_2_in_ga2(tree_33(X, niltree_0, T), cons_22(X, Xs)) -> if_flat_2_in_1_ga4(X, T, Xs, flat_2_in_ga2(T, Xs))
flat_2_in_ga2(tree_33(X, tree_33(Y, T1, T2), T3), Xs) -> if_flat_2_in_2_ga7(X, Y, T1, T2, T3, Xs, flat_2_in_ga2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs))
if_flat_2_in_2_ga7(X, Y, T1, T2, T3, Xs, flat_2_out_ga2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs)) -> flat_2_out_ga2(tree_33(X, tree_33(Y, T1, T2), T3), Xs)
if_flat_2_in_1_ga4(X, T, Xs, flat_2_out_ga2(T, Xs)) -> flat_2_out_ga2(tree_33(X, niltree_0, T), cons_22(X, Xs))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
FLAT_2_IN_GA2(tree_33(X, niltree_0, T), cons_22(X, Xs)) -> IF_FLAT_2_IN_1_GA4(X, T, Xs, flat_2_in_ga2(T, Xs))
FLAT_2_IN_GA2(tree_33(X, niltree_0, T), cons_22(X, Xs)) -> FLAT_2_IN_GA2(T, Xs)
FLAT_2_IN_GA2(tree_33(X, tree_33(Y, T1, T2), T3), Xs) -> IF_FLAT_2_IN_2_GA7(X, Y, T1, T2, T3, Xs, flat_2_in_ga2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs))
FLAT_2_IN_GA2(tree_33(X, tree_33(Y, T1, T2), T3), Xs) -> FLAT_2_IN_GA2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs)
flat_2_in_ga2(niltree_0, nil_0) -> flat_2_out_ga2(niltree_0, nil_0)
flat_2_in_ga2(tree_33(X, niltree_0, T), cons_22(X, Xs)) -> if_flat_2_in_1_ga4(X, T, Xs, flat_2_in_ga2(T, Xs))
flat_2_in_ga2(tree_33(X, tree_33(Y, T1, T2), T3), Xs) -> if_flat_2_in_2_ga7(X, Y, T1, T2, T3, Xs, flat_2_in_ga2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs))
if_flat_2_in_2_ga7(X, Y, T1, T2, T3, Xs, flat_2_out_ga2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs)) -> flat_2_out_ga2(tree_33(X, tree_33(Y, T1, T2), T3), Xs)
if_flat_2_in_1_ga4(X, T, Xs, flat_2_out_ga2(T, Xs)) -> flat_2_out_ga2(tree_33(X, niltree_0, T), cons_22(X, Xs))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
FLAT_2_IN_GA2(tree_33(X, niltree_0, T), cons_22(X, Xs)) -> FLAT_2_IN_GA2(T, Xs)
FLAT_2_IN_GA2(tree_33(X, tree_33(Y, T1, T2), T3), Xs) -> FLAT_2_IN_GA2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs)
flat_2_in_ga2(niltree_0, nil_0) -> flat_2_out_ga2(niltree_0, nil_0)
flat_2_in_ga2(tree_33(X, niltree_0, T), cons_22(X, Xs)) -> if_flat_2_in_1_ga4(X, T, Xs, flat_2_in_ga2(T, Xs))
flat_2_in_ga2(tree_33(X, tree_33(Y, T1, T2), T3), Xs) -> if_flat_2_in_2_ga7(X, Y, T1, T2, T3, Xs, flat_2_in_ga2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs))
if_flat_2_in_2_ga7(X, Y, T1, T2, T3, Xs, flat_2_out_ga2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs)) -> flat_2_out_ga2(tree_33(X, tree_33(Y, T1, T2), T3), Xs)
if_flat_2_in_1_ga4(X, T, Xs, flat_2_out_ga2(T, Xs)) -> flat_2_out_ga2(tree_33(X, niltree_0, T), cons_22(X, Xs))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
FLAT_2_IN_GA2(tree_33(X, niltree_0, T), cons_22(X, Xs)) -> FLAT_2_IN_GA2(T, Xs)
FLAT_2_IN_GA2(tree_33(X, tree_33(Y, T1, T2), T3), Xs) -> FLAT_2_IN_GA2(tree_33(Y, T1, tree_33(X, T2, T3)), Xs)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
FLAT_2_IN_GA1(tree_33(X, niltree_0, T)) -> FLAT_2_IN_GA1(T)
FLAT_2_IN_GA1(tree_33(X, tree_33(Y, T1, T2), T3)) -> FLAT_2_IN_GA1(tree_33(Y, T1, tree_33(X, T2, T3)))
FLAT_2_IN_GA1(tree_33(X, niltree_0, T)) -> FLAT_2_IN_GA1(T)
POL(niltree_0) = 1
POL(FLAT_2_IN_GA1(x1)) = 1 + x1
POL(tree_33(x1, x2, x3)) = x1 + x2 + x3
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ QDPSizeChangeProof
FLAT_2_IN_GA1(tree_33(X, tree_33(Y, T1, T2), T3)) -> FLAT_2_IN_GA1(tree_33(Y, T1, tree_33(X, T2, T3)))
Order:Homeomorphic Embedding Order
AFS:
tree_33(x1, x2, x3) = tree_31(x2)
From the DPs we obtained the following set of size-change graphs:
We oriented the following set of usable rules.
none