Left Termination proof of /tmp/tmpsLmfae/shuffle.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 115 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 54 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 4 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 0 ms)

        ↳25 QDP

        ↳26 QDPOrderProof (⇔, 111 ms)

        ↳27 QDP

        ↳28 DependencyGraphProof (⇔, 0 ms)

        ↳29 TRUE

(0) Obligation:

Clauses:

append(nil, XS, XS).
append(cons(X, XS), YS, cons(X, ZS)) :- append(XS, YS, ZS).
reverse(nil, nil).
reverse(cons(X, nil), cons(X, nil)).
reverse(cons(X, XS), YS) :- ','(reverse(XS, ZS), append(ZS, cons(X, nil), YS)).
shuffle(nil, nil).
shuffle(cons(X, XS), cons(X, YS)) :- ','(reverse(XS, ZS), shuffle(ZS, YS)).
query(XS) :- shuffle(cons(X, XS), YS).

Query: query(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: query(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: query(T1), SCOPE: 1, CLAUSE: 7\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: shuffle(cons(X3, T3), X4)\n\nT3 is ground\nX3 is free\nX4 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: shuffle(cons(X3, T3), X4), SCOPE: 2, CLAUSE: 5 | shuffle(cons(X3, T3), X4), SCOPE: 2, CLAUSE: 6\n\nT3 is ground\nX3 is free\nX4 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: shuffle(cons(X3, T3), X4), SCOPE: 2, CLAUSE: 6\n\nT3 is ground\nX3 is free\nX4 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="B: ','(reverse(T6, X19), shuffle(X19, X21))\n\nT6 is ground\nX21 is free\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="C: reverse(T6, X19)\n\nT6 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="F: shuffle(T7, X21)\n\nT7 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: reverse(T6, X19), SCOPE: 3, CLAUSE: 2 | reverse(T6, X19), SCOPE: 3, CLAUSE: 3 | reverse(T6, X19), SCOPE: 3, CLAUSE: 4\n\nT6 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: reverse(T6, X19), SCOPE: 3, CLAUSE: 2\n\nT6 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: reverse(T6, X19), SCOPE: 3, CLAUSE: 3 | reverse(T6, X19), SCOPE: 3, CLAUSE: 4\n\nT6 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: reverse(T6, X19), SCOPE: 3, CLAUSE: 3\n\nT6 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: reverse(T6, X19), SCOPE: 3, CLAUSE: 4\n\nT6 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="D: ','(reverse(T18, X39), append(X39, cons(T17, nil), X40))\n\nT17 is ground\nT18 is ground\nX40 is free\nX39 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: reverse(T18, X39)\n\nT18 is ground\nX39 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="E: append(T19, cons(T17, nil), X40)\n\nT17 is ground\nT19 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: append(T19, cons(T17, nil), X40), SCOPE: 4, CLAUSE: 0 | append(T19, cons(T17, nil), X40), SCOPE: 4, CLAUSE: 1\n\nT17 is ground\nT19 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: append(T19, cons(T17, nil), X40), SCOPE: 4, CLAUSE: 0\n\nT17 is ground\nT19 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: append(T19, cons(T17, nil), X40), SCOPE: 4, CLAUSE: 1\n\nT17 is ground\nT19 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: append(T34, cons(T35, nil), X62)\n\nT34 is ground\nT35 is ground\nX62 is free", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: shuffle(T7, X21), SCOPE: 5, CLAUSE: 5 | shuffle(T7, X21), SCOPE: 5, CLAUSE: 6\n\nT7 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: shuffle(T7, X21), SCOPE: 5, CLAUSE: 5\n\nT7 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: shuffle(T7, X21), SCOPE: 5, CLAUSE: 6\n\nT7 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(reverse(T43, X77), shuffle(X77, X78))\n\nT43 is ground\nX78 is free\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 118 [arrowhead = none ];
118 -> 5;

119 [label="ONLY EVAL with clause\nquery(X2) :- shuffle(cons(X3, X2), X4).\nand substitutionT1 -> T3,\nX2 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 119 [arrowhead = none ];
119 -> 8;

120 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
8 -> 120 [arrowhead = none ];
120 -> 10;

121 [label="BACKTRACK\nfor clause: shuffle(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 121 [arrowhead = none ];
121 -> 12;

122 [label="ONLY EVAL with clause\nshuffle(cons(X16, X17), cons(X16, X18)) :- ','(reverse(X17, X19), shuffle(X19, X18)).\nand substitutionX3 -> X20,\nX16 -> X20,\nT3 -> T6,\nX17 -> T6,\nX18 -> X21,\nX4 -> cons(X20, X21)", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 122 [arrowhead = none ];
122 -> 17;

123 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
17 -> 123 [arrowhead = none ];
123 -> 19;

124 [label="SPLIT 2\nnew knowledge:\nT6 is ground\nT7 is ground\nreplacements:X19 -> T7", fontsize=14, style = filled, fillcolor = violet];
17 -> 124 [arrowhead = none ];
124 -> 21;

125 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
19 -> 125 [arrowhead = none ];
125 -> 26;

126 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
21 -> 126 [arrowhead = none ];
126 -> 110;

127 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 127 [arrowhead = none ];
127 -> 30;

128 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 128 [arrowhead = none ];
128 -> 33;

129 [label="EVAL with clause\nreverse(nil, nil).\nand substitutionT6 -> nil,\nX19 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 129 [arrowhead = none ];
129 -> 36;

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

131 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
33 -> 131 [arrowhead = none ];
131 -> 46;

132 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
33 -> 132 [arrowhead = none ];
132 -> 48;

133 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 133 [arrowhead = none ];
133 -> 42;

134 [label="EVAL with clause\nreverse(cons(X26, nil), cons(X26, nil)).\nand substitutionX26 -> T12,\nT6 -> cons(T12, nil),\nX19 -> cons(T12, nil)", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 134 [arrowhead = none ];
134 -> 52;

135 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 135 [arrowhead = none ];
135 -> 56;

136 [label="EVAL with clause\nreverse(cons(X36, X37), X38) :- ','(reverse(X37, X39), append(X39, cons(X36, nil), X38)).\nand substitutionX36 -> T17,\nX37 -> T18,\nT6 -> cons(T17, T18),\nX19 -> X40,\nX38 -> X40", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 136 [arrowhead = none ];
136 -> 65;

137 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 137 [arrowhead = none ];
137 -> 67;

138 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 138 [arrowhead = none ];
138 -> 57;

139 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
65 -> 139 [arrowhead = none ];
139 -> 70;

140 [label="SPLIT 2\nnew knowledge:\nT18 is ground\nT19 is ground\nreplacements:X39 -> T19", fontsize=14, style = filled, fillcolor = violet];
65 -> 140 [arrowhead = none ];
140 -> 75;

141 [label="INSTANCE with matching:\nT6 -> T18\nX19 -> X39", fontsize=14, style = filled, fillcolor = lightgrey];
70 -> 141 [arrowhead = none , style=dashed];
141 -> 19[style=dashed];

142 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
75 -> 142 [arrowhead = none ];
142 -> 82;

143 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
82 -> 143 [arrowhead = none ];
143 -> 83;

144 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
82 -> 144 [arrowhead = none ];
144 -> 84;

145 [label="EVAL with clause\nappend(nil, X47, X47).\nand substitutionT19 -> nil,\nT17 -> T26,\nX47 -> cons(T26, nil),\nX40 -> cons(T26, nil)", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 145 [arrowhead = none ];
145 -> 95;

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

147 [label="EVAL with clause\nappend(cons(X58, X59), X60, cons(X58, X61)) :- append(X59, X60, X61).\nand substitutionX58 -> T33,\nX59 -> T34,\nT19 -> cons(T33, T34),\nT17 -> T35,\nX60 -> cons(T35, nil),\nX61 -> X62,\nX40 -> cons(T33, X62)", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 147 [arrowhead = none ];
147 -> 108;

148 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 148 [arrowhead = none ];
148 -> 109;

149 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 149 [arrowhead = none ];
149 -> 100;

150 [label="INSTANCE with matching:\nT19 -> T34\nT17 -> T35\nX40 -> X62", fontsize=14, style = filled, fillcolor = lightgrey];
108 -> 150 [arrowhead = none , style=dashed];
150 -> 75[style=dashed];

151 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
110 -> 151 [arrowhead = none ];
151 -> 111;

152 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
110 -> 152 [arrowhead = none ];
152 -> 112;

153 [label="EVAL with clause\nshuffle(nil, nil).\nand substitutionT7 -> nil,\nX21 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
111 -> 153 [arrowhead = none ];
153 -> 113;

154 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 154 [arrowhead = none ];
154 -> 114;

155 [label="EVAL with clause\nshuffle(cons(X74, X75), cons(X74, X76)) :- ','(reverse(X75, X77), shuffle(X77, X76)).\nand substitutionX74 -> T42,\nX75 -> T43,\nT7 -> cons(T42, T43),\nX76 -> X78,\nX21 -> cons(T42, X78)", fontsize=14, style = filled, fillcolor = lightblue];
112 -> 155 [arrowhead = none ];
155 -> 116;

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

157 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
113 -> 157 [arrowhead = none ];
157 -> 115;

158 [label="INSTANCE with matching:\nT6 -> T43\nX19 -> X77\nX21 -> X78", fontsize=14, style = filled, fillcolor = lightgrey];
116 -> 158 [arrowhead = none , style=dashed];
158 -> 17[style=dashed];

}

(2) Obligation:

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

queryA_in_g(T6) → U1_g(T6, pB_in_gaa(T6, X19, X21))
pB_in_gaa(T6, T7, X21) → U5_gaa(T6, T7, X21, reverseC_in_ga(T6, T7))
reverseC_in_ga(nil, nil) → reverseC_out_ga(nil, nil)
reverseC_in_ga(cons(T12, nil), cons(T12, nil)) → reverseC_out_ga(cons(T12, nil), cons(T12, nil))
reverseC_in_ga(cons(T17, T18), X40) → U2_ga(T17, T18, X40, pD_in_gaga(T18, X39, T17, X40))
pD_in_gaga(T18, T19, T17, X40) → U7_gaga(T18, T19, T17, X40, reverseC_in_ga(T18, T19))
U7_gaga(T18, T19, T17, X40, reverseC_out_ga(T18, T19)) → U8_gaga(T18, T19, T17, X40, appendE_in_gga(T19, T17, X40))
appendE_in_gga(nil, T26, cons(T26, nil)) → appendE_out_gga(nil, T26, cons(T26, nil))
appendE_in_gga(cons(T33, T34), T35, cons(T33, X62)) → U3_gga(T33, T34, T35, X62, appendE_in_gga(T34, T35, X62))
U3_gga(T33, T34, T35, X62, appendE_out_gga(T34, T35, X62)) → appendE_out_gga(cons(T33, T34), T35, cons(T33, X62))
U8_gaga(T18, T19, T17, X40, appendE_out_gga(T19, T17, X40)) → pD_out_gaga(T18, T19, T17, X40)
U2_ga(T17, T18, X40, pD_out_gaga(T18, X39, T17, X40)) → reverseC_out_ga(cons(T17, T18), X40)
U5_gaa(T6, T7, X21, reverseC_out_ga(T6, T7)) → U6_gaa(T6, T7, X21, shuffleF_in_ga(T7, X21))
shuffleF_in_ga(nil, nil) → shuffleF_out_ga(nil, nil)
shuffleF_in_ga(cons(T42, T43), cons(T42, X78)) → U4_ga(T42, T43, X78, pB_in_gaa(T43, X77, X78))
U4_ga(T42, T43, X78, pB_out_gaa(T43, X77, X78)) → shuffleF_out_ga(cons(T42, T43), cons(T42, X78))
U6_gaa(T6, T7, X21, shuffleF_out_ga(T7, X21)) → pB_out_gaa(T6, T7, X21)
U1_g(T6, pB_out_gaa(T6, X19, X21)) → queryA_out_g(T6)

(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:

QUERYA_IN_G(T6) → U1_G(T6, pB_in_gaa(T6, X19, X21))
QUERYA_IN_G(T6) → PB_IN_GAA(T6, X19, X21)
PB_IN_GAA(T6, T7, X21) → U5_GAA(T6, T7, X21, reverseC_in_ga(T6, T7))
PB_IN_GAA(T6, T7, X21) → REVERSEC_IN_GA(T6, T7)
REVERSEC_IN_GA(cons(T17, T18), X40) → U2_GA(T17, T18, X40, pD_in_gaga(T18, X39, T17, X40))
REVERSEC_IN_GA(cons(T17, T18), X40) → PD_IN_GAGA(T18, X39, T17, X40)
PD_IN_GAGA(T18, T19, T17, X40) → U7_GAGA(T18, T19, T17, X40, reverseC_in_ga(T18, T19))
PD_IN_GAGA(T18, T19, T17, X40) → REVERSEC_IN_GA(T18, T19)
U7_GAGA(T18, T19, T17, X40, reverseC_out_ga(T18, T19)) → U8_GAGA(T18, T19, T17, X40, appendE_in_gga(T19, T17, X40))
U7_GAGA(T18, T19, T17, X40, reverseC_out_ga(T18, T19)) → APPENDE_IN_GGA(T19, T17, X40)
APPENDE_IN_GGA(cons(T33, T34), T35, cons(T33, X62)) → U3_GGA(T33, T34, T35, X62, appendE_in_gga(T34, T35, X62))
APPENDE_IN_GGA(cons(T33, T34), T35, cons(T33, X62)) → APPENDE_IN_GGA(T34, T35, X62)
U5_GAA(T6, T7, X21, reverseC_out_ga(T6, T7)) → U6_GAA(T6, T7, X21, shuffleF_in_ga(T7, X21))
U5_GAA(T6, T7, X21, reverseC_out_ga(T6, T7)) → SHUFFLEF_IN_GA(T7, X21)
SHUFFLEF_IN_GA(cons(T42, T43), cons(T42, X78)) → U4_GA(T42, T43, X78, pB_in_gaa(T43, X77, X78))
SHUFFLEF_IN_GA(cons(T42, T43), cons(T42, X78)) → PB_IN_GAA(T43, X77, X78)

The TRS R consists of the following rules:

queryA_in_g(T6) → U1_g(T6, pB_in_gaa(T6, X19, X21))
pB_in_gaa(T6, T7, X21) → U5_gaa(T6, T7, X21, reverseC_in_ga(T6, T7))
reverseC_in_ga(nil, nil) → reverseC_out_ga(nil, nil)
reverseC_in_ga(cons(T12, nil), cons(T12, nil)) → reverseC_out_ga(cons(T12, nil), cons(T12, nil))
reverseC_in_ga(cons(T17, T18), X40) → U2_ga(T17, T18, X40, pD_in_gaga(T18, X39, T17, X40))
pD_in_gaga(T18, T19, T17, X40) → U7_gaga(T18, T19, T17, X40, reverseC_in_ga(T18, T19))
U7_gaga(T18, T19, T17, X40, reverseC_out_ga(T18, T19)) → U8_gaga(T18, T19, T17, X40, appendE_in_gga(T19, T17, X40))
appendE_in_gga(nil, T26, cons(T26, nil)) → appendE_out_gga(nil, T26, cons(T26, nil))
appendE_in_gga(cons(T33, T34), T35, cons(T33, X62)) → U3_gga(T33, T34, T35, X62, appendE_in_gga(T34, T35, X62))
U3_gga(T33, T34, T35, X62, appendE_out_gga(T34, T35, X62)) → appendE_out_gga(cons(T33, T34), T35, cons(T33, X62))
U8_gaga(T18, T19, T17, X40, appendE_out_gga(T19, T17, X40)) → pD_out_gaga(T18, T19, T17, X40)
U2_ga(T17, T18, X40, pD_out_gaga(T18, X39, T17, X40)) → reverseC_out_ga(cons(T17, T18), X40)
U5_gaa(T6, T7, X21, reverseC_out_ga(T6, T7)) → U6_gaa(T6, T7, X21, shuffleF_in_ga(T7, X21))
shuffleF_in_ga(nil, nil) → shuffleF_out_ga(nil, nil)
shuffleF_in_ga(cons(T42, T43), cons(T42, X78)) → U4_ga(T42, T43, X78, pB_in_gaa(T43, X77, X78))
U4_ga(T42, T43, X78, pB_out_gaa(T43, X77, X78)) → shuffleF_out_ga(cons(T42, T43), cons(T42, X78))
U6_gaa(T6, T7, X21, shuffleF_out_ga(T7, X21)) → pB_out_gaa(T6, T7, X21)
U1_g(T6, pB_out_gaa(T6, X19, X21)) → queryA_out_g(T6)

The argument filtering Pi contains the following mapping:
queryA_in_g(x1) = queryA_in_g(x1)
U1_g(x1, x2) = U1_g(x1, x2)
pB_in_gaa(x1, x2, x3) = pB_in_gaa(x1)
U5_gaa(x1, x2, x3, x4) = U5_gaa(x1, x4)
reverseC_in_ga(x1, x2) = reverseC_in_ga(x1)
nil = nil
reverseC_out_ga(x1, x2) = reverseC_out_ga(x1, x2)
cons(x1, x2) = cons(x1, x2)
U2_ga(x1, x2, x3, x4) = U2_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4) = pD_in_gaga(x1, x3)
U7_gaga(x1, x2, x3, x4, x5) = U7_gaga(x1, x3, x5)
U8_gaga(x1, x2, x3, x4, x5) = U8_gaga(x1, x2, x3, x5)
appendE_in_gga(x1, x2, x3) = appendE_in_gga(x1, x2)
appendE_out_gga(x1, x2, x3) = appendE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5) = U3_gga(x1, x2, x3, x5)
pD_out_gaga(x1, x2, x3, x4) = pD_out_gaga(x1, x2, x3, x4)
U6_gaa(x1, x2, x3, x4) = U6_gaa(x1, x2, x4)
shuffleF_in_ga(x1, x2) = shuffleF_in_ga(x1)
shuffleF_out_ga(x1, x2) = shuffleF_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4) = U4_ga(x1, x2, x4)
pB_out_gaa(x1, x2, x3) = pB_out_gaa(x1, x2, x3)
queryA_out_g(x1) = queryA_out_g(x1)
QUERYA_IN_G(x1) = QUERYA_IN_G(x1)
U1_G(x1, x2) = U1_G(x1, x2)
PB_IN_GAA(x1, x2, x3) = PB_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4) = U5_GAA(x1, x4)
REVERSEC_IN_GA(x1, x2) = REVERSEC_IN_GA(x1)
U2_GA(x1, x2, x3, x4) = U2_GA(x1, x2, x4)
PD_IN_GAGA(x1, x2, x3, x4) = PD_IN_GAGA(x1, x3)
U7_GAGA(x1, x2, x3, x4, x5) = U7_GAGA(x1, x3, x5)
U8_GAGA(x1, x2, x3, x4, x5) = U8_GAGA(x1, x2, x3, x5)
APPENDE_IN_GGA(x1, x2, x3) = APPENDE_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4, x5) = U3_GGA(x1, x2, x3, x5)
U6_GAA(x1, x2, x3, x4) = U6_GAA(x1, x2, x4)
SHUFFLEF_IN_GA(x1, x2) = SHUFFLEF_IN_GA(x1)
U4_GA(x1, x2, x3, x4) = U4_GA(x1, x2, x4)

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

(4) Obligation:

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

QUERYA_IN_G(T6) → U1_G(T6, pB_in_gaa(T6, X19, X21))
QUERYA_IN_G(T6) → PB_IN_GAA(T6, X19, X21)
PB_IN_GAA(T6, T7, X21) → U5_GAA(T6, T7, X21, reverseC_in_ga(T6, T7))
PB_IN_GAA(T6, T7, X21) → REVERSEC_IN_GA(T6, T7)
REVERSEC_IN_GA(cons(T17, T18), X40) → U2_GA(T17, T18, X40, pD_in_gaga(T18, X39, T17, X40))
REVERSEC_IN_GA(cons(T17, T18), X40) → PD_IN_GAGA(T18, X39, T17, X40)
PD_IN_GAGA(T18, T19, T17, X40) → U7_GAGA(T18, T19, T17, X40, reverseC_in_ga(T18, T19))
PD_IN_GAGA(T18, T19, T17, X40) → REVERSEC_IN_GA(T18, T19)
U7_GAGA(T18, T19, T17, X40, reverseC_out_ga(T18, T19)) → U8_GAGA(T18, T19, T17, X40, appendE_in_gga(T19, T17, X40))
U7_GAGA(T18, T19, T17, X40, reverseC_out_ga(T18, T19)) → APPENDE_IN_GGA(T19, T17, X40)
APPENDE_IN_GGA(cons(T33, T34), T35, cons(T33, X62)) → U3_GGA(T33, T34, T35, X62, appendE_in_gga(T34, T35, X62))
APPENDE_IN_GGA(cons(T33, T34), T35, cons(T33, X62)) → APPENDE_IN_GGA(T34, T35, X62)
U5_GAA(T6, T7, X21, reverseC_out_ga(T6, T7)) → U6_GAA(T6, T7, X21, shuffleF_in_ga(T7, X21))
U5_GAA(T6, T7, X21, reverseC_out_ga(T6, T7)) → SHUFFLEF_IN_GA(T7, X21)
SHUFFLEF_IN_GA(cons(T42, T43), cons(T42, X78)) → U4_GA(T42, T43, X78, pB_in_gaa(T43, X77, X78))
SHUFFLEF_IN_GA(cons(T42, T43), cons(T42, X78)) → PB_IN_GAA(T43, X77, X78)

The TRS R consists of the following rules:

queryA_in_g(T6) → U1_g(T6, pB_in_gaa(T6, X19, X21))
pB_in_gaa(T6, T7, X21) → U5_gaa(T6, T7, X21, reverseC_in_ga(T6, T7))
reverseC_in_ga(nil, nil) → reverseC_out_ga(nil, nil)
reverseC_in_ga(cons(T12, nil), cons(T12, nil)) → reverseC_out_ga(cons(T12, nil), cons(T12, nil))
reverseC_in_ga(cons(T17, T18), X40) → U2_ga(T17, T18, X40, pD_in_gaga(T18, X39, T17, X40))
pD_in_gaga(T18, T19, T17, X40) → U7_gaga(T18, T19, T17, X40, reverseC_in_ga(T18, T19))
U7_gaga(T18, T19, T17, X40, reverseC_out_ga(T18, T19)) → U8_gaga(T18, T19, T17, X40, appendE_in_gga(T19, T17, X40))
appendE_in_gga(nil, T26, cons(T26, nil)) → appendE_out_gga(nil, T26, cons(T26, nil))
appendE_in_gga(cons(T33, T34), T35, cons(T33, X62)) → U3_gga(T33, T34, T35, X62, appendE_in_gga(T34, T35, X62))
U3_gga(T33, T34, T35, X62, appendE_out_gga(T34, T35, X62)) → appendE_out_gga(cons(T33, T34), T35, cons(T33, X62))
U8_gaga(T18, T19, T17, X40, appendE_out_gga(T19, T17, X40)) → pD_out_gaga(T18, T19, T17, X40)
U2_ga(T17, T18, X40, pD_out_gaga(T18, X39, T17, X40)) → reverseC_out_ga(cons(T17, T18), X40)
U5_gaa(T6, T7, X21, reverseC_out_ga(T6, T7)) → U6_gaa(T6, T7, X21, shuffleF_in_ga(T7, X21))
shuffleF_in_ga(nil, nil) → shuffleF_out_ga(nil, nil)
shuffleF_in_ga(cons(T42, T43), cons(T42, X78)) → U4_ga(T42, T43, X78, pB_in_gaa(T43, X77, X78))
U4_ga(T42, T43, X78, pB_out_gaa(T43, X77, X78)) → shuffleF_out_ga(cons(T42, T43), cons(T42, X78))
U6_gaa(T6, T7, X21, shuffleF_out_ga(T7, X21)) → pB_out_gaa(T6, T7, X21)
U1_g(T6, pB_out_gaa(T6, X19, X21)) → queryA_out_g(T6)

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 10 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

APPENDE_IN_GGA(cons(T33, T34), T35, cons(T33, X62)) → APPENDE_IN_GGA(T34, T35, X62)

The TRS R consists of the following rules:

queryA_in_g(T6) → U1_g(T6, pB_in_gaa(T6, X19, X21))
pB_in_gaa(T6, T7, X21) → U5_gaa(T6, T7, X21, reverseC_in_ga(T6, T7))
reverseC_in_ga(nil, nil) → reverseC_out_ga(nil, nil)
reverseC_in_ga(cons(T12, nil), cons(T12, nil)) → reverseC_out_ga(cons(T12, nil), cons(T12, nil))
reverseC_in_ga(cons(T17, T18), X40) → U2_ga(T17, T18, X40, pD_in_gaga(T18, X39, T17, X40))
pD_in_gaga(T18, T19, T17, X40) → U7_gaga(T18, T19, T17, X40, reverseC_in_ga(T18, T19))
U7_gaga(T18, T19, T17, X40, reverseC_out_ga(T18, T19)) → U8_gaga(T18, T19, T17, X40, appendE_in_gga(T19, T17, X40))
appendE_in_gga(nil, T26, cons(T26, nil)) → appendE_out_gga(nil, T26, cons(T26, nil))
appendE_in_gga(cons(T33, T34), T35, cons(T33, X62)) → U3_gga(T33, T34, T35, X62, appendE_in_gga(T34, T35, X62))
U3_gga(T33, T34, T35, X62, appendE_out_gga(T34, T35, X62)) → appendE_out_gga(cons(T33, T34), T35, cons(T33, X62))
U8_gaga(T18, T19, T17, X40, appendE_out_gga(T19, T17, X40)) → pD_out_gaga(T18, T19, T17, X40)
U2_ga(T17, T18, X40, pD_out_gaga(T18, X39, T17, X40)) → reverseC_out_ga(cons(T17, T18), X40)
U5_gaa(T6, T7, X21, reverseC_out_ga(T6, T7)) → U6_gaa(T6, T7, X21, shuffleF_in_ga(T7, X21))
shuffleF_in_ga(nil, nil) → shuffleF_out_ga(nil, nil)
shuffleF_in_ga(cons(T42, T43), cons(T42, X78)) → U4_ga(T42, T43, X78, pB_in_gaa(T43, X77, X78))
U4_ga(T42, T43, X78, pB_out_gaa(T43, X77, X78)) → shuffleF_out_ga(cons(T42, T43), cons(T42, X78))
U6_gaa(T6, T7, X21, shuffleF_out_ga(T7, X21)) → pB_out_gaa(T6, T7, X21)
U1_g(T6, pB_out_gaa(T6, X19, X21)) → queryA_out_g(T6)

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

APPENDE_IN_GGA(cons(T33, T34), T35, cons(T33, X62)) → APPENDE_IN_GGA(T34, T35, X62)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

APPENDE_IN_GGA(cons(T33, T34), T35) → APPENDE_IN_GGA(T34, T35)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

APPENDE_IN_GGA(cons(T33, T34), T35) → APPENDE_IN_GGA(T34, T35)
The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

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

REVERSEC_IN_GA(cons(T17, T18), X40) → PD_IN_GAGA(T18, X39, T17, X40)
PD_IN_GAGA(T18, T19, T17, X40) → REVERSEC_IN_GA(T18, T19)

The TRS R consists of the following rules:

queryA_in_g(T6) → U1_g(T6, pB_in_gaa(T6, X19, X21))
pB_in_gaa(T6, T7, X21) → U5_gaa(T6, T7, X21, reverseC_in_ga(T6, T7))
reverseC_in_ga(nil, nil) → reverseC_out_ga(nil, nil)
reverseC_in_ga(cons(T12, nil), cons(T12, nil)) → reverseC_out_ga(cons(T12, nil), cons(T12, nil))
reverseC_in_ga(cons(T17, T18), X40) → U2_ga(T17, T18, X40, pD_in_gaga(T18, X39, T17, X40))
pD_in_gaga(T18, T19, T17, X40) → U7_gaga(T18, T19, T17, X40, reverseC_in_ga(T18, T19))
U7_gaga(T18, T19, T17, X40, reverseC_out_ga(T18, T19)) → U8_gaga(T18, T19, T17, X40, appendE_in_gga(T19, T17, X40))
appendE_in_gga(nil, T26, cons(T26, nil)) → appendE_out_gga(nil, T26, cons(T26, nil))
appendE_in_gga(cons(T33, T34), T35, cons(T33, X62)) → U3_gga(T33, T34, T35, X62, appendE_in_gga(T34, T35, X62))
U3_gga(T33, T34, T35, X62, appendE_out_gga(T34, T35, X62)) → appendE_out_gga(cons(T33, T34), T35, cons(T33, X62))
U8_gaga(T18, T19, T17, X40, appendE_out_gga(T19, T17, X40)) → pD_out_gaga(T18, T19, T17, X40)
U2_ga(T17, T18, X40, pD_out_gaga(T18, X39, T17, X40)) → reverseC_out_ga(cons(T17, T18), X40)
U5_gaa(T6, T7, X21, reverseC_out_ga(T6, T7)) → U6_gaa(T6, T7, X21, shuffleF_in_ga(T7, X21))
shuffleF_in_ga(nil, nil) → shuffleF_out_ga(nil, nil)
shuffleF_in_ga(cons(T42, T43), cons(T42, X78)) → U4_ga(T42, T43, X78, pB_in_gaa(T43, X77, X78))
U4_ga(T42, T43, X78, pB_out_gaa(T43, X77, X78)) → shuffleF_out_ga(cons(T42, T43), cons(T42, X78))
U6_gaa(T6, T7, X21, shuffleF_out_ga(T7, X21)) → pB_out_gaa(T6, T7, X21)
U1_g(T6, pB_out_gaa(T6, X19, X21)) → queryA_out_g(T6)

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

REVERSEC_IN_GA(cons(T17, T18), X40) → PD_IN_GAGA(T18, X39, T17, X40)
PD_IN_GAGA(T18, T19, T17, X40) → REVERSEC_IN_GA(T18, T19)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
REVERSEC_IN_GA(x1, x2) = REVERSEC_IN_GA(x1)
PD_IN_GAGA(x1, x2, x3, x4) = PD_IN_GAGA(x1, x3)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

REVERSEC_IN_GA(cons(T17, T18)) → PD_IN_GAGA(T18, T17)
PD_IN_GAGA(T18, T17) → REVERSEC_IN_GA(T18)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

PD_IN_GAGA(T18, T17) → REVERSEC_IN_GA(T18)
The graph contains the following edges 1 >= 1
REVERSEC_IN_GA(cons(T17, T18)) → PD_IN_GAGA(T18, T17)
The graph contains the following edges 1 > 1, 1 > 2

(20) YES

(21) Obligation:

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

U5_GAA(T6, T7, X21, reverseC_out_ga(T6, T7)) → SHUFFLEF_IN_GA(T7, X21)
SHUFFLEF_IN_GA(cons(T42, T43), cons(T42, X78)) → PB_IN_GAA(T43, X77, X78)
PB_IN_GAA(T6, T7, X21) → U5_GAA(T6, T7, X21, reverseC_in_ga(T6, T7))

The TRS R consists of the following rules:

queryA_in_g(T6) → U1_g(T6, pB_in_gaa(T6, X19, X21))
pB_in_gaa(T6, T7, X21) → U5_gaa(T6, T7, X21, reverseC_in_ga(T6, T7))
reverseC_in_ga(nil, nil) → reverseC_out_ga(nil, nil)
reverseC_in_ga(cons(T12, nil), cons(T12, nil)) → reverseC_out_ga(cons(T12, nil), cons(T12, nil))
reverseC_in_ga(cons(T17, T18), X40) → U2_ga(T17, T18, X40, pD_in_gaga(T18, X39, T17, X40))
pD_in_gaga(T18, T19, T17, X40) → U7_gaga(T18, T19, T17, X40, reverseC_in_ga(T18, T19))
U7_gaga(T18, T19, T17, X40, reverseC_out_ga(T18, T19)) → U8_gaga(T18, T19, T17, X40, appendE_in_gga(T19, T17, X40))
appendE_in_gga(nil, T26, cons(T26, nil)) → appendE_out_gga(nil, T26, cons(T26, nil))
appendE_in_gga(cons(T33, T34), T35, cons(T33, X62)) → U3_gga(T33, T34, T35, X62, appendE_in_gga(T34, T35, X62))
U3_gga(T33, T34, T35, X62, appendE_out_gga(T34, T35, X62)) → appendE_out_gga(cons(T33, T34), T35, cons(T33, X62))
U8_gaga(T18, T19, T17, X40, appendE_out_gga(T19, T17, X40)) → pD_out_gaga(T18, T19, T17, X40)
U2_ga(T17, T18, X40, pD_out_gaga(T18, X39, T17, X40)) → reverseC_out_ga(cons(T17, T18), X40)
U5_gaa(T6, T7, X21, reverseC_out_ga(T6, T7)) → U6_gaa(T6, T7, X21, shuffleF_in_ga(T7, X21))
shuffleF_in_ga(nil, nil) → shuffleF_out_ga(nil, nil)
shuffleF_in_ga(cons(T42, T43), cons(T42, X78)) → U4_ga(T42, T43, X78, pB_in_gaa(T43, X77, X78))
U4_ga(T42, T43, X78, pB_out_gaa(T43, X77, X78)) → shuffleF_out_ga(cons(T42, T43), cons(T42, X78))
U6_gaa(T6, T7, X21, shuffleF_out_ga(T7, X21)) → pB_out_gaa(T6, T7, X21)
U1_g(T6, pB_out_gaa(T6, X19, X21)) → queryA_out_g(T6)

The argument filtering Pi contains the following mapping:
queryA_in_g(x1) = queryA_in_g(x1)
U1_g(x1, x2) = U1_g(x1, x2)
pB_in_gaa(x1, x2, x3) = pB_in_gaa(x1)
U5_gaa(x1, x2, x3, x4) = U5_gaa(x1, x4)
reverseC_in_ga(x1, x2) = reverseC_in_ga(x1)
nil = nil
reverseC_out_ga(x1, x2) = reverseC_out_ga(x1, x2)
cons(x1, x2) = cons(x1, x2)
U2_ga(x1, x2, x3, x4) = U2_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4) = pD_in_gaga(x1, x3)
U7_gaga(x1, x2, x3, x4, x5) = U7_gaga(x1, x3, x5)
U8_gaga(x1, x2, x3, x4, x5) = U8_gaga(x1, x2, x3, x5)
appendE_in_gga(x1, x2, x3) = appendE_in_gga(x1, x2)
appendE_out_gga(x1, x2, x3) = appendE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5) = U3_gga(x1, x2, x3, x5)
pD_out_gaga(x1, x2, x3, x4) = pD_out_gaga(x1, x2, x3, x4)
U6_gaa(x1, x2, x3, x4) = U6_gaa(x1, x2, x4)
shuffleF_in_ga(x1, x2) = shuffleF_in_ga(x1)
shuffleF_out_ga(x1, x2) = shuffleF_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4) = U4_ga(x1, x2, x4)
pB_out_gaa(x1, x2, x3) = pB_out_gaa(x1, x2, x3)
queryA_out_g(x1) = queryA_out_g(x1)
PB_IN_GAA(x1, x2, x3) = PB_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4) = U5_GAA(x1, x4)
SHUFFLEF_IN_GA(x1, x2) = SHUFFLEF_IN_GA(x1)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

U5_GAA(T6, T7, X21, reverseC_out_ga(T6, T7)) → SHUFFLEF_IN_GA(T7, X21)
SHUFFLEF_IN_GA(cons(T42, T43), cons(T42, X78)) → PB_IN_GAA(T43, X77, X78)
PB_IN_GAA(T6, T7, X21) → U5_GAA(T6, T7, X21, reverseC_in_ga(T6, T7))

The TRS R consists of the following rules:

reverseC_in_ga(nil, nil) → reverseC_out_ga(nil, nil)
reverseC_in_ga(cons(T12, nil), cons(T12, nil)) → reverseC_out_ga(cons(T12, nil), cons(T12, nil))
reverseC_in_ga(cons(T17, T18), X40) → U2_ga(T17, T18, X40, pD_in_gaga(T18, X39, T17, X40))
U2_ga(T17, T18, X40, pD_out_gaga(T18, X39, T17, X40)) → reverseC_out_ga(cons(T17, T18), X40)
pD_in_gaga(T18, T19, T17, X40) → U7_gaga(T18, T19, T17, X40, reverseC_in_ga(T18, T19))
U7_gaga(T18, T19, T17, X40, reverseC_out_ga(T18, T19)) → U8_gaga(T18, T19, T17, X40, appendE_in_gga(T19, T17, X40))
U8_gaga(T18, T19, T17, X40, appendE_out_gga(T19, T17, X40)) → pD_out_gaga(T18, T19, T17, X40)
appendE_in_gga(nil, T26, cons(T26, nil)) → appendE_out_gga(nil, T26, cons(T26, nil))
appendE_in_gga(cons(T33, T34), T35, cons(T33, X62)) → U3_gga(T33, T34, T35, X62, appendE_in_gga(T34, T35, X62))
U3_gga(T33, T34, T35, X62, appendE_out_gga(T34, T35, X62)) → appendE_out_gga(cons(T33, T34), T35, cons(T33, X62))

The argument filtering Pi contains the following mapping:
reverseC_in_ga(x1, x2) = reverseC_in_ga(x1)
nil = nil
reverseC_out_ga(x1, x2) = reverseC_out_ga(x1, x2)
cons(x1, x2) = cons(x1, x2)
U2_ga(x1, x2, x3, x4) = U2_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4) = pD_in_gaga(x1, x3)
U7_gaga(x1, x2, x3, x4, x5) = U7_gaga(x1, x3, x5)
U8_gaga(x1, x2, x3, x4, x5) = U8_gaga(x1, x2, x3, x5)
appendE_in_gga(x1, x2, x3) = appendE_in_gga(x1, x2)
appendE_out_gga(x1, x2, x3) = appendE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5) = U3_gga(x1, x2, x3, x5)
pD_out_gaga(x1, x2, x3, x4) = pD_out_gaga(x1, x2, x3, x4)
PB_IN_GAA(x1, x2, x3) = PB_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4) = U5_GAA(x1, x4)
SHUFFLEF_IN_GA(x1, x2) = SHUFFLEF_IN_GA(x1)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

U5_GAA(T6, reverseC_out_ga(T6, T7)) → SHUFFLEF_IN_GA(T7)
SHUFFLEF_IN_GA(cons(T42, T43)) → PB_IN_GAA(T43)
PB_IN_GAA(T6) → U5_GAA(T6, reverseC_in_ga(T6))

The TRS R consists of the following rules:

reverseC_in_ga(nil) → reverseC_out_ga(nil, nil)
reverseC_in_ga(cons(T12, nil)) → reverseC_out_ga(cons(T12, nil), cons(T12, nil))
reverseC_in_ga(cons(T17, T18)) → U2_ga(T17, T18, pD_in_gaga(T18, T17))
U2_ga(T17, T18, pD_out_gaga(T18, X39, T17, X40)) → reverseC_out_ga(cons(T17, T18), X40)
pD_in_gaga(T18, T17) → U7_gaga(T18, T17, reverseC_in_ga(T18))
U7_gaga(T18, T17, reverseC_out_ga(T18, T19)) → U8_gaga(T18, T19, T17, appendE_in_gga(T19, T17))
U8_gaga(T18, T19, T17, appendE_out_gga(T19, T17, X40)) → pD_out_gaga(T18, T19, T17, X40)
appendE_in_gga(nil, T26) → appendE_out_gga(nil, T26, cons(T26, nil))
appendE_in_gga(cons(T33, T34), T35) → U3_gga(T33, T34, T35, appendE_in_gga(T34, T35))
U3_gga(T33, T34, T35, appendE_out_gga(T34, T35, X62)) → appendE_out_gga(cons(T33, T34), T35, cons(T33, X62))

The set Q consists of the following terms:

reverseC_in_ga(x0)
U2_ga(x0, x1, x2)
pD_in_gaga(x0, x1)
U7_gaga(x0, x1, x2)
U8_gaga(x0, x1, x2, x3)
appendE_in_gga(x0, x1)
U3_gga(x0, x1, x2, x3)

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

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

PB_IN_GAA(T6) → U5_GAA(T6, reverseC_in_ga(T6))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(PB_IN_GAA(x₁)) = 1 + x₁
POL(SHUFFLEF_IN_GA(x₁)) = x₁
POL(U2_ga(x₁, x₂, x₃)) = x₃
POL(U3_gga(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(U5_GAA(x₁, x₂)) = x₂
POL(U7_gaga(x₁, x₂, x₃)) = 1 + x₃
POL(U8_gaga(x₁, x₂, x₃, x₄)) = x₄
POL(appendE_in_gga(x₁, x₂)) = 1 + x₁
POL(appendE_out_gga(x₁, x₂, x₃)) = x₃
POL(cons(x₁, x₂)) = 1 + x₂
POL(nil) = 1
POL(pD_in_gaga(x₁, x₂)) = 1 + x₁
POL(pD_out_gaga(x₁, x₂, x₃, x₄)) = x₄
POL(reverseC_in_ga(x₁)) = x₁
POL(reverseC_out_ga(x₁, x₂)) = x₂

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

reverseC_in_ga(nil) → reverseC_out_ga(nil, nil)
reverseC_in_ga(cons(T12, nil)) → reverseC_out_ga(cons(T12, nil), cons(T12, nil))
reverseC_in_ga(cons(T17, T18)) → U2_ga(T17, T18, pD_in_gaga(T18, T17))
U2_ga(T17, T18, pD_out_gaga(T18, X39, T17, X40)) → reverseC_out_ga(cons(T17, T18), X40)
pD_in_gaga(T18, T17) → U7_gaga(T18, T17, reverseC_in_ga(T18))
U7_gaga(T18, T17, reverseC_out_ga(T18, T19)) → U8_gaga(T18, T19, T17, appendE_in_gga(T19, T17))
appendE_in_gga(nil, T26) → appendE_out_gga(nil, T26, cons(T26, nil))
appendE_in_gga(cons(T33, T34), T35) → U3_gga(T33, T34, T35, appendE_in_gga(T34, T35))
U8_gaga(T18, T19, T17, appendE_out_gga(T19, T17, X40)) → pD_out_gaga(T18, T19, T17, X40)
U3_gga(T33, T34, T35, appendE_out_gga(T34, T35, X62)) → appendE_out_gga(cons(T33, T34), T35, cons(T33, X62))

(27) Obligation:

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

U5_GAA(T6, reverseC_out_ga(T6, T7)) → SHUFFLEF_IN_GA(T7)
SHUFFLEF_IN_GA(cons(T42, T43)) → PB_IN_GAA(T43)

The TRS R consists of the following rules:

reverseC_in_ga(nil) → reverseC_out_ga(nil, nil)
reverseC_in_ga(cons(T12, nil)) → reverseC_out_ga(cons(T12, nil), cons(T12, nil))
reverseC_in_ga(cons(T17, T18)) → U2_ga(T17, T18, pD_in_gaga(T18, T17))
U2_ga(T17, T18, pD_out_gaga(T18, X39, T17, X40)) → reverseC_out_ga(cons(T17, T18), X40)
pD_in_gaga(T18, T17) → U7_gaga(T18, T17, reverseC_in_ga(T18))
U7_gaga(T18, T17, reverseC_out_ga(T18, T19)) → U8_gaga(T18, T19, T17, appendE_in_gga(T19, T17))
U8_gaga(T18, T19, T17, appendE_out_gga(T19, T17, X40)) → pD_out_gaga(T18, T19, T17, X40)
appendE_in_gga(nil, T26) → appendE_out_gga(nil, T26, cons(T26, nil))
appendE_in_gga(cons(T33, T34), T35) → U3_gga(T33, T34, T35, appendE_in_gga(T34, T35))
U3_gga(T33, T34, T35, appendE_out_gga(T34, T35, X62)) → appendE_out_gga(cons(T33, T34), T35, cons(T33, X62))

The set Q consists of the following terms:

reverseC_in_ga(x0)
U2_ga(x0, x1, x2)
pD_in_gaga(x0, x1)
U7_gaga(x0, x1, x2)
U8_gaga(x0, x1, x2, x3)
appendE_in_gga(x0, x1)
U3_gga(x0, x1, x2, x3)

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

(28) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) QDPOrderProof (EQUIVALENT transformation)

(27) Obligation:

(28) DependencyGraphProof (EQUIVALENT transformation)

(29) TRUE