Left Termination proof of /tmp/tmp3T6QU9/flatten.pl

Left Termination of the query pattern
flatten(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 93 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 10 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 5 ms)

↳6 PiDP

↳7 UsableRulesProof (⇔, 0 ms)

↳8 PiDP

↳9 PiDPToQDPProof (⇒, 0 ms)

↳10 QDP

↳11 UsableRulesReductionPairsProof (⇔, 61 ms)

↳12 QDP

↳13 MRRProof (⇔, 0 ms)

↳14 QDP

↳15 PisEmptyProof (⇔, 0 ms)

↳16 YES

(0) Obligation:

Clauses:

flatten(atom(X), .(X, [])).
flatten(cons(atom(X), U), .(X, Y)) :- flatten(U, Y).
flatten(cons(cons(U, V), W), X) :- flatten(cons(U, cons(V, W)), X).

Query: flatten(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: flatten(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: flatten(T1, T2), SCOPE: 1, CLAUSE: 0 | flatten(T1, T2), SCOPE: 1, CLAUSE: 1 | flatten(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | flatten(atom(T4), T2), SCOPE: 1, CLAUSE: 1 | flatten(atom(T4), T2), SCOPE: 1, CLAUSE: 2\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: flatten(T1, T2), SCOPE: 1, CLAUSE: 1 | flatten(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX2 is free\nflatten(T1, T2) !=? flatten(atom(X2), .(X2, []))", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: flatten(atom(T4), T2), SCOPE: 1, CLAUSE: 1 | flatten(atom(T4), T2), SCOPE: 1, CLAUSE: 2\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: flatten(atom(T4), T2), SCOPE: 1, CLAUSE: 2\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: flatten(T9, T11) | flatten(cons(atom(T8), T9), T2), SCOPE: 1, CLAUSE: 2\n\nT8 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: flatten(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX2 is free\nX13 is free\nX14 is free\nX15 is free\nflatten(T1, T2) !=? flatten(atom(X2), .(X2, []))\nflatten(T1, T2) !=? flatten(cons(atom(X13), X14), .(X13, X15))", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: flatten(T9, T11), SCOPE: 2, CLAUSE: 0 | flatten(T9, T11), SCOPE: 2, CLAUSE: 1 | flatten(T9, T11), SCOPE: 2, CLAUSE: 2 | ?_2 | flatten(cons(atom(T8), T9), T2), SCOPE: 1, CLAUSE: 2\n\nT8 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: flatten(T9, T11), SCOPE: 2, CLAUSE: 0\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: flatten(T9, T11), SCOPE: 2, CLAUSE: 1 | flatten(T9, T11), SCOPE: 2, CLAUSE: 2 | ?_2 | flatten(cons(atom(T8), T9), T2), SCOPE: 1, CLAUSE: 2\n\nT8 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: flatten(T9, T11), SCOPE: 2, CLAUSE: 1\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: flatten(T9, T11), SCOPE: 2, CLAUSE: 2 | ?_2 | flatten(cons(atom(T8), T9), T2), SCOPE: 1, CLAUSE: 2\n\nT8 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: flatten(T30, T32)\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: flatten(T9, T11), SCOPE: 2, CLAUSE: 2\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ?_2 | flatten(cons(atom(T8), T9), T2), SCOPE: 1, CLAUSE: 2\n\nT8 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: flatten(cons(T51, cons(T52, T53)), T55)\n\nT51 is ground\nT52 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: flatten(cons(atom(T8), T9), T2), SCOPE: 1, CLAUSE: 2\n\nT8 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: flatten(cons(T60, cons(T61, T62)), T64)\n\nT60 is ground\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: flatten(cons(T60, cons(T61, T62)), T64), SCOPE: 3, CLAUSE: 0 | flatten(cons(T60, cons(T61, T62)), T64), SCOPE: 3, CLAUSE: 1 | flatten(cons(T60, cons(T61, T62)), T64), SCOPE: 3, CLAUSE: 2\n\nT60 is ground\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: flatten(cons(T60, cons(T61, T62)), T64), SCOPE: 3, CLAUSE: 1 | flatten(cons(T60, cons(T61, T62)), T64), SCOPE: 3, CLAUSE: 2\n\nT60 is ground\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: flatten(cons(T60, cons(T61, T62)), T64), SCOPE: 3, CLAUSE: 1\n\nT60 is ground\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: flatten(cons(T60, cons(T61, T62)), T64), SCOPE: 3, CLAUSE: 2\n\nT60 is ground\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: flatten(cons(T82, T83), T85)\n\nT82 is ground\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: flatten(cons(T96, cons(T97, cons(T98, T99))), T101)\n\nT96 is ground\nT97 is ground\nT98 is ground\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 84 [arrowhead = none ];
84 -> 6;

85 [label="EVAL with clause\nflatten(atom(X2), .(X2, [])).\nand substitutionX2 -> T4,\nT1 -> atom(T4),\nT2 -> .(T4, [])", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 85 [arrowhead = none ];
85 -> 10;

86 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 86 [arrowhead = none ];
86 -> 15;

87 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 87 [arrowhead = none ];
87 -> 17;

88 [label="EVAL with clause\nflatten(cons(atom(X13), X14), .(X13, X15)) :- flatten(X14, X15).\nand substitutionX13 -> T8,\nX14 -> T9,\nT1 -> cons(atom(T8), T9),\nX15 -> T11,\nT2 -> .(T8, T11),\nT10 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 88 [arrowhead = none ];
88 -> 25;

89 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 89 [arrowhead = none ];
89 -> 30;

90 [label="BACKTRACK\nfor clause: flatten(cons(atom(X), U), .(X, Y)) :- flatten(U, Y)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 90 [arrowhead = none ];
90 -> 19;

91 [label="BACKTRACK\nfor clause: flatten(cons(cons(U, V), W), X) :- flatten(cons(U, cons(V, W)), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 91 [arrowhead = none ];
91 -> 22;

92 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
25 -> 92 [arrowhead = none ];
92 -> 31;

93 [label="EVAL with clause\nflatten(cons(cons(X68, X69), X70), X71) :- flatten(cons(X68, cons(X69, X70)), X71).\nand substitutionX68 -> T60,\nX69 -> T61,\nX70 -> T62,\nT1 -> cons(cons(T60, T61), T62),\nT2 -> T64,\nX71 -> T64,\nT63 -> T64", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 93 [arrowhead = none ];
93 -> 74;

94 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 94 [arrowhead = none ];
94 -> 75;

95 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
31 -> 95 [arrowhead = none ];
95 -> 34;

96 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
31 -> 96 [arrowhead = none ];
96 -> 35;

97 [label="EVAL with clause\nflatten(atom(X20), .(X20, [])).\nand substitutionX20 -> T16,\nT9 -> atom(T16),\nT11 -> .(T16, [])", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 97 [arrowhead = none ];
97 -> 39;

98 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 98 [arrowhead = none ];
98 -> 40;

99 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
35 -> 99 [arrowhead = none ];
99 -> 44;

100 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
35 -> 100 [arrowhead = none ];
100 -> 45;

101 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 101 [arrowhead = none ];
101 -> 41;

102 [label="EVAL with clause\nflatten(cons(atom(X33), X34), .(X33, X35)) :- flatten(X34, X35).\nand substitutionX33 -> T29,\nX34 -> T30,\nT9 -> cons(atom(T29), T30),\nX35 -> T32,\nT11 -> .(T29, T32),\nT31 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 102 [arrowhead = none ];
102 -> 50;

103 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 103 [arrowhead = none ];
103 -> 51;

104 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 104 [arrowhead = none ];
104 -> 64;

105 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 105 [arrowhead = none ];
105 -> 65;

106 [label="INSTANCE with matching:\nT1 -> T30\nT2 -> T32", fontsize=14, style = filled, fillcolor = lightgrey];
50 -> 106 [arrowhead = none , style=dashed];
106 -> 2[style=dashed];

107 [label="EVAL with clause\nflatten(cons(cons(X54, X55), X56), X57) :- flatten(cons(X54, cons(X55, X56)), X57).\nand substitutionX54 -> T51,\nX55 -> T52,\nX56 -> T53,\nT9 -> cons(cons(T51, T52), T53),\nT11 -> T55,\nX57 -> T55,\nT54 -> T55", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 107 [arrowhead = none ];
107 -> 70;

108 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 108 [arrowhead = none ];
108 -> 71;

109 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 109 [arrowhead = none ];
109 -> 72;

110 [label="INSTANCE with matching:\nT1 -> cons(T51, cons(T52, T53))\nT2 -> T55", fontsize=14, style = filled, fillcolor = lightgrey];
70 -> 110 [arrowhead = none , style=dashed];
110 -> 2[style=dashed];

111 [label="BACKTRACK\nfor clause: flatten(cons(cons(U, V), W), X) :- flatten(cons(U, cons(V, W)), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 111 [arrowhead = none ];
111 -> 73;

112 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
74 -> 112 [arrowhead = none ];
112 -> 76;

113 [label="BACKTRACK\nfor clause: flatten(atom(X), .(X, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 113 [arrowhead = none ];
113 -> 77;

114 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
77 -> 114 [arrowhead = none ];
114 -> 78;

115 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
77 -> 115 [arrowhead = none ];
115 -> 79;

116 [label="EVAL with clause\nflatten(cons(atom(X85), X86), .(X85, X87)) :- flatten(X86, X87).\nand substitutionX85 -> T81,\nT60 -> atom(T81),\nT61 -> T82,\nT62 -> T83,\nX86 -> cons(T82, T83),\nX87 -> T85,\nT64 -> .(T81, T85),\nT84 -> T85", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 116 [arrowhead = none ];
116 -> 80;

117 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
78 -> 117 [arrowhead = none ];
117 -> 81;

118 [label="EVAL with clause\nflatten(cons(cons(X98, X99), X100), X101) :- flatten(cons(X98, cons(X99, X100)), X101).\nand substitutionX98 -> T96,\nX99 -> T97,\nT60 -> cons(T96, T97),\nT61 -> T98,\nT62 -> T99,\nX100 -> cons(T98, T99),\nT64 -> T101,\nX101 -> T101,\nT100 -> T101", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 118 [arrowhead = none ];
118 -> 82;

119 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
79 -> 119 [arrowhead = none ];
119 -> 83;

120 [label="INSTANCE with matching:\nT1 -> cons(T82, T83)\nT2 -> T85", fontsize=14, style = filled, fillcolor = lightgrey];
80 -> 120 [arrowhead = none , style=dashed];
120 -> 2[style=dashed];

121 [label="INSTANCE with matching:\nT1 -> cons(T96, cons(T97, cons(T98, T99)))\nT2 -> T101", fontsize=14, style = filled, fillcolor = lightgrey];
82 -> 121 [arrowhead = none , style=dashed];
121 -> 2[style=dashed];

}

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

flattenA_in_ga(atom(T4), .(T4, [])) → flattenA_out_ga(atom(T4), .(T4, []))
flattenA_in_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, []))) → flattenA_out_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, [])))
flattenA_in_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → U1_ga(T8, T29, T30, T32, flattenA_in_ga(T30, T32))
flattenA_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → U2_ga(T8, T51, T52, T53, T55, flattenA_in_ga(cons(T51, cons(T52, T53)), T55))
flattenA_in_ga(cons(cons(atom(T81), T82), T83), .(T81, T85)) → U3_ga(T81, T82, T83, T85, flattenA_in_ga(cons(T82, T83), T85))
flattenA_in_ga(cons(cons(cons(T96, T97), T98), T99), T101) → U4_ga(T96, T97, T98, T99, T101, flattenA_in_ga(cons(T96, cons(T97, cons(T98, T99))), T101))
U4_ga(T96, T97, T98, T99, T101, flattenA_out_ga(cons(T96, cons(T97, cons(T98, T99))), T101)) → flattenA_out_ga(cons(cons(cons(T96, T97), T98), T99), T101)
U3_ga(T81, T82, T83, T85, flattenA_out_ga(cons(T82, T83), T85)) → flattenA_out_ga(cons(cons(atom(T81), T82), T83), .(T81, T85))
U2_ga(T8, T51, T52, T53, T55, flattenA_out_ga(cons(T51, cons(T52, T53)), T55)) → flattenA_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55))
U1_ga(T8, T29, T30, T32, flattenA_out_ga(T30, T32)) → flattenA_out_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32)))

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → U1_GA(T8, T29, T30, T32, flattenA_in_ga(T30, T32))
FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → FLATTENA_IN_GA(T30, T32)
FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → U2_GA(T8, T51, T52, T53, T55, flattenA_in_ga(cons(T51, cons(T52, T53)), T55))
FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → FLATTENA_IN_GA(cons(T51, cons(T52, T53)), T55)
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83), .(T81, T85)) → U3_GA(T81, T82, T83, T85, flattenA_in_ga(cons(T82, T83), T85))
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83), .(T81, T85)) → FLATTENA_IN_GA(cons(T82, T83), T85)
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99), T101) → U4_GA(T96, T97, T98, T99, T101, flattenA_in_ga(cons(T96, cons(T97, cons(T98, T99))), T101))
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99), T101) → FLATTENA_IN_GA(cons(T96, cons(T97, cons(T98, T99))), T101)

The TRS R consists of the following rules:

flattenA_in_ga(atom(T4), .(T4, [])) → flattenA_out_ga(atom(T4), .(T4, []))
flattenA_in_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, []))) → flattenA_out_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, [])))
flattenA_in_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → U1_ga(T8, T29, T30, T32, flattenA_in_ga(T30, T32))
flattenA_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → U2_ga(T8, T51, T52, T53, T55, flattenA_in_ga(cons(T51, cons(T52, T53)), T55))
flattenA_in_ga(cons(cons(atom(T81), T82), T83), .(T81, T85)) → U3_ga(T81, T82, T83, T85, flattenA_in_ga(cons(T82, T83), T85))
flattenA_in_ga(cons(cons(cons(T96, T97), T98), T99), T101) → U4_ga(T96, T97, T98, T99, T101, flattenA_in_ga(cons(T96, cons(T97, cons(T98, T99))), T101))
U4_ga(T96, T97, T98, T99, T101, flattenA_out_ga(cons(T96, cons(T97, cons(T98, T99))), T101)) → flattenA_out_ga(cons(cons(cons(T96, T97), T98), T99), T101)
U3_ga(T81, T82, T83, T85, flattenA_out_ga(cons(T82, T83), T85)) → flattenA_out_ga(cons(cons(atom(T81), T82), T83), .(T81, T85))
U2_ga(T8, T51, T52, T53, T55, flattenA_out_ga(cons(T51, cons(T52, T53)), T55)) → flattenA_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55))
U1_ga(T8, T29, T30, T32, flattenA_out_ga(T30, T32)) → flattenA_out_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32)))

The argument filtering Pi contains the following mapping:
flattenA_in_ga(x1, x2) = flattenA_in_ga(x1)
atom(x1) = atom(x1)
flattenA_out_ga(x1, x2) = flattenA_out_ga(x1, x2)
cons(x1, x2) = cons(x1, x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3, x4, x5, x6) = U2_ga(x1, x2, x3, x4, x6)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x1, x2, x3, x5)
U4_ga(x1, x2, x3, x4, x5, x6) = U4_ga(x1, x2, x3, x4, x6)
.(x1, x2) = .(x1, x2)
FLATTENA_IN_GA(x1, x2) = FLATTENA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x1, x2, x3, x5)
U2_GA(x1, x2, x3, x4, x5, x6) = U2_GA(x1, x2, x3, x4, x6)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x1, x2, x3, x5)
U4_GA(x1, x2, x3, x4, x5, x6) = U4_GA(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → U1_GA(T8, T29, T30, T32, flattenA_in_ga(T30, T32))
FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → FLATTENA_IN_GA(T30, T32)
FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → U2_GA(T8, T51, T52, T53, T55, flattenA_in_ga(cons(T51, cons(T52, T53)), T55))
FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → FLATTENA_IN_GA(cons(T51, cons(T52, T53)), T55)
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83), .(T81, T85)) → U3_GA(T81, T82, T83, T85, flattenA_in_ga(cons(T82, T83), T85))
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83), .(T81, T85)) → FLATTENA_IN_GA(cons(T82, T83), T85)
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99), T101) → U4_GA(T96, T97, T98, T99, T101, flattenA_in_ga(cons(T96, cons(T97, cons(T98, T99))), T101))
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99), T101) → FLATTENA_IN_GA(cons(T96, cons(T97, cons(T98, T99))), T101)

The TRS R consists of the following rules:

flattenA_in_ga(atom(T4), .(T4, [])) → flattenA_out_ga(atom(T4), .(T4, []))
flattenA_in_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, []))) → flattenA_out_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, [])))
flattenA_in_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → U1_ga(T8, T29, T30, T32, flattenA_in_ga(T30, T32))
flattenA_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → U2_ga(T8, T51, T52, T53, T55, flattenA_in_ga(cons(T51, cons(T52, T53)), T55))
flattenA_in_ga(cons(cons(atom(T81), T82), T83), .(T81, T85)) → U3_ga(T81, T82, T83, T85, flattenA_in_ga(cons(T82, T83), T85))
flattenA_in_ga(cons(cons(cons(T96, T97), T98), T99), T101) → U4_ga(T96, T97, T98, T99, T101, flattenA_in_ga(cons(T96, cons(T97, cons(T98, T99))), T101))
U4_ga(T96, T97, T98, T99, T101, flattenA_out_ga(cons(T96, cons(T97, cons(T98, T99))), T101)) → flattenA_out_ga(cons(cons(cons(T96, T97), T98), T99), T101)
U3_ga(T81, T82, T83, T85, flattenA_out_ga(cons(T82, T83), T85)) → flattenA_out_ga(cons(cons(atom(T81), T82), T83), .(T81, T85))
U2_ga(T8, T51, T52, T53, T55, flattenA_out_ga(cons(T51, cons(T52, T53)), T55)) → flattenA_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55))
U1_ga(T8, T29, T30, T32, flattenA_out_ga(T30, T32)) → flattenA_out_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32)))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 4 less nodes.

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → FLATTENA_IN_GA(cons(T51, cons(T52, T53)), T55)
FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → FLATTENA_IN_GA(T30, T32)
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83), .(T81, T85)) → FLATTENA_IN_GA(cons(T82, T83), T85)
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99), T101) → FLATTENA_IN_GA(cons(T96, cons(T97, cons(T98, T99))), T101)

The TRS R consists of the following rules:

flattenA_in_ga(atom(T4), .(T4, [])) → flattenA_out_ga(atom(T4), .(T4, []))
flattenA_in_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, []))) → flattenA_out_ga(cons(atom(T8), atom(T16)), .(T8, .(T16, [])))
flattenA_in_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → U1_ga(T8, T29, T30, T32, flattenA_in_ga(T30, T32))
flattenA_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → U2_ga(T8, T51, T52, T53, T55, flattenA_in_ga(cons(T51, cons(T52, T53)), T55))
flattenA_in_ga(cons(cons(atom(T81), T82), T83), .(T81, T85)) → U3_ga(T81, T82, T83, T85, flattenA_in_ga(cons(T82, T83), T85))
flattenA_in_ga(cons(cons(cons(T96, T97), T98), T99), T101) → U4_ga(T96, T97, T98, T99, T101, flattenA_in_ga(cons(T96, cons(T97, cons(T98, T99))), T101))
U4_ga(T96, T97, T98, T99, T101, flattenA_out_ga(cons(T96, cons(T97, cons(T98, T99))), T101)) → flattenA_out_ga(cons(cons(cons(T96, T97), T98), T99), T101)
U3_ga(T81, T82, T83, T85, flattenA_out_ga(cons(T82, T83), T85)) → flattenA_out_ga(cons(cons(atom(T81), T82), T83), .(T81, T85))
U2_ga(T8, T51, T52, T53, T55, flattenA_out_ga(cons(T51, cons(T52, T53)), T55)) → flattenA_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55))
U1_ga(T8, T29, T30, T32, flattenA_out_ga(T30, T32)) → flattenA_out_ga(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32)))

(7) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(8) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), .(T8, T55)) → FLATTENA_IN_GA(cons(T51, cons(T52, T53)), T55)
FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), .(T8, .(T29, T32))) → FLATTENA_IN_GA(T30, T32)
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83), .(T81, T85)) → FLATTENA_IN_GA(cons(T82, T83), T85)
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99), T101) → FLATTENA_IN_GA(cons(T96, cons(T97, cons(T98, T99))), T101)

R is empty.
The argument filtering Pi contains the following mapping:
atom(x1) = atom(x1)
cons(x1, x2) = cons(x1, x2)
.(x1, x2) = .(x1, x2)
FLATTENA_IN_GA(x1, x2) = FLATTENA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(9) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53))) → FLATTENA_IN_GA(cons(T51, cons(T52, T53)))
FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30))) → FLATTENA_IN_GA(T30)
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83)) → FLATTENA_IN_GA(cons(T82, T83))
FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99)) → FLATTENA_IN_GA(cons(T96, cons(T97, cons(T98, T99))))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(11) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

FLATTENA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53))) → FLATTENA_IN_GA(cons(T51, cons(T52, T53)))
FLATTENA_IN_GA(cons(atom(T8), cons(atom(T29), T30))) → FLATTENA_IN_GA(T30)
FLATTENA_IN_GA(cons(cons(atom(T81), T82), T83)) → FLATTENA_IN_GA(cons(T82, T83))

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(FLATTENA_IN_GA(x₁)) = 2·x₁
POL(atom(x₁)) = x₁
POL(cons(x₁, x₂)) = x₁ + x₂

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99)) → FLATTENA_IN_GA(cons(T96, cons(T97, cons(T98, T99))))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(13) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

FLATTENA_IN_GA(cons(cons(cons(T96, T97), T98), T99)) → FLATTENA_IN_GA(cons(T96, cons(T97, cons(T98, T99))))

Used ordering: Knuth-Bendix order [KBO] with precedence:

cons₂ > FLATTENA_{IN_GA₁}

and weight map:

FLATTENA_IN_GA_1=1
cons_2=0

The variable weight is 1

(14) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(15) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Obligation:

(7) UsableRulesProof (EQUIVALENT transformation)

(8) Obligation:

(9) PiDPToQDPProof (SOUND transformation)

(10) Obligation:

(11) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(12) Obligation:

(13) MRRProof (EQUIVALENT transformation)

(14) Obligation:

(15) PisEmptyProof (EQUIVALENT transformation)

(16) YES