Left Termination proof of /tmp/tmpYjvVeZ/som.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 125 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 0 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 PiDP

↳7 UsableRulesProof (⇔, 0 ms)

↳8 PiDP

↳9 PiDPToQDPProof (⇒, 0 ms)

↳10 QDP

↳11 QDPSizeChangeProof (⇔, 0 ms)

↳12 YES

(0) Obligation:

Clauses:

som3([], Bs, Bs).
som3(As, [], As).
som3(.(A, As), .(B, Bs), .(+(A, B), Cs)) :- som3(As, Bs, Cs).
som4_1(As, Bs, Cs, Ds) :- ','(som3(As, Bs, Es), som3(Es, Cs, Ds)).
som4_2(As, Bs, Cs, Ds) :- ','(som3(Es, Cs, Ds), som3(As, Bs, Es)).

Query: som3(g,a,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: som3(T1, T2, T3)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: som3(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | som3(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | som3(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: true | som3([], T2, T3), SCOPE: 1, CLAUSE: 1 | som3([], T2, T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: som3(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | som3(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX2 is free\nsom3(T1, T2, T3) !=? som3([], X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: som3([], T2, T3), SCOPE: 1, CLAUSE: 1 | som3([], T2, T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: true | som3([], T2, T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: som3([], T2, T3), SCOPE: 1, CLAUSE: 2\n\nX4 is free\nsom3([], T2, T3) !=? som3(X4, [], X4)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: som3([], T2, T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: true | som3(T7, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT7 is ground\nX2 is free\nsom3(T7, T2, T3) !=? som3([], X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: som3(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX2 is free\nX16 is free\nsom3(T1, T2, T3) !=? som3([], X2, X2)\nsom3(T1, T2, T3) !=? som3(X16, [], X16)", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: som3(T7, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT7 is ground\nX2 is free\nsom3(T7, T2, T3) !=? som3([], X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: som3(T14, T18, T19)\n\nT14 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: som3(T14, T18, T19), SCOPE: 2, CLAUSE: 0 | som3(T14, T18, T19), SCOPE: 2, CLAUSE: 1 | som3(T14, T18, T19), SCOPE: 2, CLAUSE: 2\n\nT14 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: som3(T14, T18, T19), SCOPE: 2, CLAUSE: 0\n\nT14 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: som3(T14, T18, T19), SCOPE: 2, CLAUSE: 1 | som3(T14, T18, T19), SCOPE: 2, CLAUSE: 2\n\nT14 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: som3(T14, T18, T19), SCOPE: 2, CLAUSE: 1\n\nT14 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: som3(T14, T18, T19), SCOPE: 2, CLAUSE: 2\n\nT14 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: som3(T41, T45, T46)\n\nT41 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: som3(T55, T59, T60)\n\nT54 is ground\nT55 is ground\nX16 is free\nsom3(.(T54, T55), T2, T3) !=? som3(X16, [], X16)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: som3(T55, T59, T60), SCOPE: 3, CLAUSE: 0 | som3(T55, T59, T60), SCOPE: 3, CLAUSE: 1 | som3(T55, T59, T60), SCOPE: 3, CLAUSE: 2\n\nT54 is ground\nT55 is ground\nX16 is free\nsom3(.(T54, T55), T2, T3) !=? som3(X16, [], X16)", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: som3(T55, T59, T60), SCOPE: 3, CLAUSE: 0\n\nT54 is ground\nT55 is ground\nX16 is free\nsom3(.(T54, T55), T2, T3) !=? som3(X16, [], X16)", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: som3(T55, T59, T60), SCOPE: 3, CLAUSE: 1 | som3(T55, T59, T60), SCOPE: 3, CLAUSE: 2\n\nT54 is ground\nT55 is ground\nX16 is free\nsom3(.(T54, T55), T2, T3) !=? som3(X16, [], X16)", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: som3(T55, T59, T60), SCOPE: 3, CLAUSE: 1\n\nT54 is ground\nT55 is ground\nX16 is free\nsom3(.(T54, T55), T2, T3) !=? som3(X16, [], X16)", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: som3(T55, T59, T60), SCOPE: 3, CLAUSE: 2\n\nT54 is ground\nT55 is ground\nX16 is free\nsom3(.(T54, T55), T2, T3) !=? som3(X16, [], X16)", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: som3(T82, T86, T87)\n\nT54 is ground\nT81 is ground\nT82 is ground\nX16 is free\nsom3(.(T54, .(T81, T82)), T2, T3) !=? som3(X16, [], X16)", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 99 [arrowhead = none ];
99 -> 2;

100 [label="EVAL with clause\nsom3([], X2, X2).\nand substitutionT1 -> [],\nT2 -> T5,\nX2 -> T5,\nT3 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 100 [arrowhead = none ];
100 -> 16;

101 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
2 -> 101 [arrowhead = none ];
101 -> 19;

102 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 102 [arrowhead = none ];
102 -> 20;

103 [label="EVAL with clause\nsom3(X16, [], X16).\nand substitutionT1 -> T7,\nX16 -> T7,\nT2 -> [],\nT3 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 103 [arrowhead = none ];
103 -> 34;

104 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 104 [arrowhead = none ];
104 -> 37;

105 [label="EVAL with clause\nsom3(X4, [], X4).\nand substitutionX4 -> [],\nT2 -> [],\nT3 -> []", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 105 [arrowhead = none ];
105 -> 22;

106 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 106 [arrowhead = none ];
106 -> 26;

107 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 107 [arrowhead = none ];
107 -> 27;

108 [label="BACKTRACK\nfor clause: som3(.(A, As), .(B, Bs), .(+(A, B), Cs)) :- som3(As, Bs, Cs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 108 [arrowhead = none ];
108 -> 29;

109 [label="BACKTRACK\nfor clause: som3(.(A, As), .(B, Bs), .(+(A, B), Cs)) :- som3(As, Bs, Cs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 109 [arrowhead = none ];
109 -> 28;

110 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 110 [arrowhead = none ];
110 -> 38;

111 [label="EVAL with clause\nsom3(.(X59, X60), .(X61, X62), .(+(X59, X61), X63)) :- som3(X60, X62, X63).\nand substitutionX59 -> T54,\nX60 -> T55,\nT1 -> .(T54, T55),\nX61 -> T56,\nX62 -> T59,\nT2 -> .(T56, T59),\nX63 -> T60,\nT3 -> .(+(T54, T56), T60),\nT57 -> T59,\nT58 -> T60", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 111 [arrowhead = none ];
111 -> 81;

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

113 [label="EVAL with clause\nsom3(.(X22, X23), .(X24, X25), .(+(X22, X24), X26)) :- som3(X23, X25, X26).\nand substitutionX22 -> T13,\nX23 -> T14,\nT7 -> .(T13, T14),\nX24 -> T15,\nX25 -> T18,\nT2 -> .(T15, T18),\nX26 -> T19,\nT3 -> .(+(T13, T15), T19),\nT16 -> T18,\nT17 -> T19", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 113 [arrowhead = none ];
113 -> 40;

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

115 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
40 -> 115 [arrowhead = none ];
115 -> 44;

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

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

118 [label="EVAL with clause\nsom3([], X31, X31).\nand substitutionT14 -> [],\nT18 -> T24,\nX31 -> T24,\nT19 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 118 [arrowhead = none ];
118 -> 53;

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

120 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
49 -> 120 [arrowhead = none ];
120 -> 59;

121 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
49 -> 121 [arrowhead = none ];
121 -> 60;

122 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 122 [arrowhead = none ];
122 -> 56;

123 [label="EVAL with clause\nsom3(X36, [], X36).\nand substitutionT14 -> T29,\nX36 -> T29,\nT18 -> [],\nT19 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 123 [arrowhead = none ];
123 -> 62;

124 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 124 [arrowhead = none ];
124 -> 65;

125 [label="EVAL with clause\nsom3(.(X47, X48), .(X49, X50), .(+(X47, X49), X51)) :- som3(X48, X50, X51).\nand substitutionX47 -> T40,\nX48 -> T41,\nT14 -> .(T40, T41),\nX49 -> T42,\nX50 -> T45,\nT18 -> .(T42, T45),\nX51 -> T46,\nT19 -> .(+(T40, T42), T46),\nT43 -> T45,\nT44 -> T46", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 125 [arrowhead = none ];
125 -> 68;

126 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 126 [arrowhead = none ];
126 -> 69;

127 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 127 [arrowhead = none ];
127 -> 66;

128 [label="INSTANCE with matching:\nT1 -> T41\nT2 -> T45\nT3 -> T46", fontsize=14, style = filled, fillcolor = lightgrey];
68 -> 128 [arrowhead = none , style=dashed];
128 -> 1[style=dashed];

129 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
81 -> 129 [arrowhead = none ];
129 -> 86;

130 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
86 -> 130 [arrowhead = none ];
130 -> 87;

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

132 [label="EVAL with clause\nsom3([], X68, X68).\nand substitutionT55 -> [],\nT59 -> T65,\nX68 -> T65,\nT60 -> T65", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 132 [arrowhead = none ];
132 -> 89;

133 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
87 -> 133 [arrowhead = none ];
133 -> 90;

134 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
88 -> 134 [arrowhead = none ];
134 -> 92;

135 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
88 -> 135 [arrowhead = none ];
135 -> 93;

136 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 136 [arrowhead = none ];
136 -> 91;

137 [label="EVAL with clause\nsom3(X73, [], X73).\nand substitutionT55 -> T70,\nX73 -> T70,\nT59 -> [],\nT60 -> T70", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 137 [arrowhead = none ];
137 -> 94;

138 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
92 -> 138 [arrowhead = none ];
138 -> 95;

139 [label="EVAL with clause\nsom3(.(X84, X85), .(X86, X87), .(+(X84, X86), X88)) :- som3(X85, X87, X88).\nand substitutionX84 -> T81,\nX85 -> T82,\nT55 -> .(T81, T82),\nX86 -> T83,\nX87 -> T86,\nT59 -> .(T83, T86),\nX88 -> T87,\nT60 -> .(+(T81, T83), T87),\nT84 -> T86,\nT85 -> T87", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 139 [arrowhead = none ];
139 -> 97;

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

141 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
94 -> 141 [arrowhead = none ];
141 -> 96;

142 [label="INSTANCE with matching:\nT1 -> T82\nT2 -> T86\nT3 -> T87", fontsize=14, style = filled, fillcolor = lightgrey];
97 -> 142 [arrowhead = none , style=dashed];
142 -> 1[style=dashed];

}

(2) Obligation:

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

som3A_in_gaa([], T5, T5) → som3A_out_gaa([], T5, T5)
som3A_in_gaa([], [], []) → som3A_out_gaa([], [], [])
som3A_in_gaa(T7, [], T7) → som3A_out_gaa(T7, [], T7)
som3A_in_gaa(.(T13, []), .(T15, T24), .(+(T13, T15), T24)) → som3A_out_gaa(.(T13, []), .(T15, T24), .(+(T13, T15), T24))
som3A_in_gaa(.(T13, T29), .(T15, []), .(+(T13, T15), T29)) → som3A_out_gaa(.(T13, T29), .(T15, []), .(+(T13, T15), T29))
som3A_in_gaa(.(T13, .(T40, T41)), .(T15, .(T42, T45)), .(+(T13, T15), .(+(T40, T42), T46))) → U1_gaa(T13, T40, T41, T15, T42, T45, T46, som3A_in_gaa(T41, T45, T46))
som3A_in_gaa(.(T54, .(T81, T82)), .(T56, .(T83, T86)), .(+(T54, T56), .(+(T81, T83), T87))) → U2_gaa(T54, T81, T82, T56, T83, T86, T87, som3A_in_gaa(T82, T86, T87))
U2_gaa(T54, T81, T82, T56, T83, T86, T87, som3A_out_gaa(T82, T86, T87)) → som3A_out_gaa(.(T54, .(T81, T82)), .(T56, .(T83, T86)), .(+(T54, T56), .(+(T81, T83), T87)))
U1_gaa(T13, T40, T41, T15, T42, T45, T46, som3A_out_gaa(T41, T45, T46)) → som3A_out_gaa(.(T13, .(T40, T41)), .(T15, .(T42, T45)), .(+(T13, T15), .(+(T40, T42), T46)))

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

SOM3A_IN_GAA(.(T13, .(T40, T41)), .(T15, .(T42, T45)), .(+(T13, T15), .(+(T40, T42), T46))) → U1_GAA(T13, T40, T41, T15, T42, T45, T46, som3A_in_gaa(T41, T45, T46))
SOM3A_IN_GAA(.(T13, .(T40, T41)), .(T15, .(T42, T45)), .(+(T13, T15), .(+(T40, T42), T46))) → SOM3A_IN_GAA(T41, T45, T46)
SOM3A_IN_GAA(.(T54, .(T81, T82)), .(T56, .(T83, T86)), .(+(T54, T56), .(+(T81, T83), T87))) → U2_GAA(T54, T81, T82, T56, T83, T86, T87, som3A_in_gaa(T82, T86, T87))

The TRS R consists of the following rules:

som3A_in_gaa([], T5, T5) → som3A_out_gaa([], T5, T5)
som3A_in_gaa([], [], []) → som3A_out_gaa([], [], [])
som3A_in_gaa(T7, [], T7) → som3A_out_gaa(T7, [], T7)
som3A_in_gaa(.(T13, []), .(T15, T24), .(+(T13, T15), T24)) → som3A_out_gaa(.(T13, []), .(T15, T24), .(+(T13, T15), T24))
som3A_in_gaa(.(T13, T29), .(T15, []), .(+(T13, T15), T29)) → som3A_out_gaa(.(T13, T29), .(T15, []), .(+(T13, T15), T29))
som3A_in_gaa(.(T13, .(T40, T41)), .(T15, .(T42, T45)), .(+(T13, T15), .(+(T40, T42), T46))) → U1_gaa(T13, T40, T41, T15, T42, T45, T46, som3A_in_gaa(T41, T45, T46))
som3A_in_gaa(.(T54, .(T81, T82)), .(T56, .(T83, T86)), .(+(T54, T56), .(+(T81, T83), T87))) → U2_gaa(T54, T81, T82, T56, T83, T86, T87, som3A_in_gaa(T82, T86, T87))
U2_gaa(T54, T81, T82, T56, T83, T86, T87, som3A_out_gaa(T82, T86, T87)) → som3A_out_gaa(.(T54, .(T81, T82)), .(T56, .(T83, T86)), .(+(T54, T56), .(+(T81, T83), T87)))
U1_gaa(T13, T40, T41, T15, T42, T45, T46, som3A_out_gaa(T41, T45, T46)) → som3A_out_gaa(.(T13, .(T40, T41)), .(T15, .(T42, T45)), .(+(T13, T15), .(+(T40, T42), T46)))

The argument filtering Pi contains the following mapping:
som3A_in_gaa(x1, x2, x3) = som3A_in_gaa(x1)
[] = []
som3A_out_gaa(x1, x2, x3) = som3A_out_gaa(x1)
.(x1, x2) = .(x1, x2)
U1_gaa(x1, x2, x3, x4, x5, x6, x7, x8) = U1_gaa(x1, x2, x3, x8)
U2_gaa(x1, x2, x3, x4, x5, x6, x7, x8) = U2_gaa(x1, x2, x3, x8)
SOM3A_IN_GAA(x1, x2, x3) = SOM3A_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4, x5, x6, x7, x8) = U1_GAA(x1, x2, x3, x8)
U2_GAA(x1, x2, x3, x4, x5, x6, x7, x8) = U2_GAA(x1, x2, x3, x8)

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

(4) Obligation:

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

SOM3A_IN_GAA(.(T13, .(T40, T41)), .(T15, .(T42, T45)), .(+(T13, T15), .(+(T40, T42), T46))) → U1_GAA(T13, T40, T41, T15, T42, T45, T46, som3A_in_gaa(T41, T45, T46))
SOM3A_IN_GAA(.(T13, .(T40, T41)), .(T15, .(T42, T45)), .(+(T13, T15), .(+(T40, T42), T46))) → SOM3A_IN_GAA(T41, T45, T46)
SOM3A_IN_GAA(.(T54, .(T81, T82)), .(T56, .(T83, T86)), .(+(T54, T56), .(+(T81, T83), T87))) → U2_GAA(T54, T81, T82, T56, T83, T86, T87, som3A_in_gaa(T82, T86, T87))

The TRS R consists of the following rules:

som3A_in_gaa([], T5, T5) → som3A_out_gaa([], T5, T5)
som3A_in_gaa([], [], []) → som3A_out_gaa([], [], [])
som3A_in_gaa(T7, [], T7) → som3A_out_gaa(T7, [], T7)
som3A_in_gaa(.(T13, []), .(T15, T24), .(+(T13, T15), T24)) → som3A_out_gaa(.(T13, []), .(T15, T24), .(+(T13, T15), T24))
som3A_in_gaa(.(T13, T29), .(T15, []), .(+(T13, T15), T29)) → som3A_out_gaa(.(T13, T29), .(T15, []), .(+(T13, T15), T29))
som3A_in_gaa(.(T13, .(T40, T41)), .(T15, .(T42, T45)), .(+(T13, T15), .(+(T40, T42), T46))) → U1_gaa(T13, T40, T41, T15, T42, T45, T46, som3A_in_gaa(T41, T45, T46))
som3A_in_gaa(.(T54, .(T81, T82)), .(T56, .(T83, T86)), .(+(T54, T56), .(+(T81, T83), T87))) → U2_gaa(T54, T81, T82, T56, T83, T86, T87, som3A_in_gaa(T82, T86, T87))
U2_gaa(T54, T81, T82, T56, T83, T86, T87, som3A_out_gaa(T82, T86, T87)) → som3A_out_gaa(.(T54, .(T81, T82)), .(T56, .(T83, T86)), .(+(T54, T56), .(+(T81, T83), T87)))
U1_gaa(T13, T40, T41, T15, T42, T45, T46, som3A_out_gaa(T41, T45, T46)) → som3A_out_gaa(.(T13, .(T40, T41)), .(T15, .(T42, T45)), .(+(T13, T15), .(+(T40, T42), T46)))

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Obligation:

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

SOM3A_IN_GAA(.(T13, .(T40, T41)), .(T15, .(T42, T45)), .(+(T13, T15), .(+(T40, T42), T46))) → SOM3A_IN_GAA(T41, T45, T46)

The TRS R consists of the following rules:

som3A_in_gaa([], T5, T5) → som3A_out_gaa([], T5, T5)
som3A_in_gaa([], [], []) → som3A_out_gaa([], [], [])
som3A_in_gaa(T7, [], T7) → som3A_out_gaa(T7, [], T7)
som3A_in_gaa(.(T13, []), .(T15, T24), .(+(T13, T15), T24)) → som3A_out_gaa(.(T13, []), .(T15, T24), .(+(T13, T15), T24))
som3A_in_gaa(.(T13, T29), .(T15, []), .(+(T13, T15), T29)) → som3A_out_gaa(.(T13, T29), .(T15, []), .(+(T13, T15), T29))
som3A_in_gaa(.(T13, .(T40, T41)), .(T15, .(T42, T45)), .(+(T13, T15), .(+(T40, T42), T46))) → U1_gaa(T13, T40, T41, T15, T42, T45, T46, som3A_in_gaa(T41, T45, T46))
som3A_in_gaa(.(T54, .(T81, T82)), .(T56, .(T83, T86)), .(+(T54, T56), .(+(T81, T83), T87))) → U2_gaa(T54, T81, T82, T56, T83, T86, T87, som3A_in_gaa(T82, T86, T87))
U2_gaa(T54, T81, T82, T56, T83, T86, T87, som3A_out_gaa(T82, T86, T87)) → som3A_out_gaa(.(T54, .(T81, T82)), .(T56, .(T83, T86)), .(+(T54, T56), .(+(T81, T83), T87)))
U1_gaa(T13, T40, T41, T15, T42, T45, T46, som3A_out_gaa(T41, T45, T46)) → som3A_out_gaa(.(T13, .(T40, T41)), .(T15, .(T42, T45)), .(+(T13, T15), .(+(T40, T42), T46)))

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

SOM3A_IN_GAA(.(T13, .(T40, T41)), .(T15, .(T42, T45)), .(+(T13, T15), .(+(T40, T42), T46))) → SOM3A_IN_GAA(T41, T45, T46)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
SOM3A_IN_GAA(x1, x2, x3) = SOM3A_IN_GAA(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:

SOM3A_IN_GAA(.(T13, .(T40, T41))) → SOM3A_IN_GAA(T41)

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

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

SOM3A_IN_GAA(.(T13, .(T40, T41))) → SOM3A_IN_GAA(T41)
The graph contains the following edges 1 > 1

(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) QDPSizeChangeProof (EQUIVALENT transformation)

(12) YES