(0) Obligation:

Clauses:

log2(X, Y) :- log2(X, 0, s(0), Y).
log2(s(s(X)), Half, Acc, Y) :- log2(X, s(Half), Acc, Y).
log2(X, s(s(Half)), Acc, Y) :- ','(small(X), log2(Half, s(0), s(Acc), Y)).
log2(X, Half, Y, Y) :- ','(small(X), small(Half)).
small(0).
small(s(0)).

Queries:

log2(a,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

log244(s(s(T131)), T129, T130) :- log244(T131, s(T129), T130).
log244(0, s(T148), T149) :- log257(T148, T149).
log244(s(0), s(T148), T149) :- log257(T148, T149).
log294(s(s(T255)), T256, T257) :- log294(T255, s(T256), T257).
log294(0, s(T274), T275) :- log2107(T274, T275).
log294(s(0), s(T274), T275) :- log2107(T274, T275).
log2144(s(s(T380)), T381, T382) :- log2144(T380, s(T381), T382).
log2144(0, s(T399), T400) :- log2157(T399, T400).
log2144(s(0), s(T399), T400) :- log2157(T399, T400).
log2194(s(s(T505)), T506, T507) :- log2194(T505, s(T506), T507).
log2194(0, s(T524), T525) :- log2207(T524, T525).
log2194(s(0), s(T524), T525) :- log2207(T524, T525).
log2244(s(s(T630)), T631, T632) :- log2244(T630, s(T631), T632).
log2244(0, s(T649), T650) :- log2257(T649, T650).
log2244(s(0), s(T649), T650) :- log2257(T649, T650).
log2294(s(s(T755)), T756, T757) :- log2294(T755, s(T756), T757).
log2294(0, s(T774), T775) :- log2307(T774, T775).
log2294(s(0), s(T774), T775) :- log2307(T774, T775).
log2344(s(s(T880)), T881, T882) :- log2344(T880, s(T881), T882).
log2344(0, s(T899), T900) :- log2359(T899, s(s(s(s(s(s(s(0))))))), T900).
log2344(s(0), s(T899), T900) :- log2359(T899, s(s(s(s(s(s(s(0))))))), T900).
log2395(s(s(T1056)), T1057, T1058, T1059) :- log2395(T1056, s(T1057), T1058, T1059).
log2395(0, s(T1081), T1082, T1083) :- log2359(T1081, s(T1082), T1083).
log2395(s(0), s(T1081), T1082, T1083) :- log2359(T1081, s(T1082), T1083).
log2359(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1029)))))))))))))), T1030, T1031) :- log2395(T1029, s(s(s(s(s(s(s(0))))))), T1030, T1031).
log2359(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T1119, T1120) :- log2437(T1119, T1120).
log2359(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T1119, T1120) :- log2437(T1119, T1120).
log2359(s(s(s(s(s(s(s(s(s(s(0)))))))))), T1222, T1223) :- log2515(T1222, T1223).
log2359(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T1222, T1223) :- log2515(T1222, T1223).
log2359(s(s(s(s(s(s(s(s(0)))))))), T1323, T1324) :- log2585(T1323, T1324).
log2359(s(s(s(s(s(s(s(s(s(0))))))))), T1323, T1324) :- log2585(T1323, T1324).
log2359(s(s(s(s(s(s(0)))))), T1394, T1395) :- log2650(T1394, T1395).
log2359(s(s(s(s(s(s(s(0))))))), T1394, T1395) :- log2650(T1394, T1395).
log2359(s(s(s(s(0)))), T1461, T1462) :- log2705(T1461, T1462).
log2359(s(s(s(s(s(0))))), T1461, T1462) :- log2705(T1461, T1462).
log2359(s(s(0)), T1490, T1491) :- log2742(T1490, T1491).
log2359(s(s(s(0))), T1490, T1491) :- log2742(T1490, T1491).
log2437(T1167, T1168) :- log2454(T1167, T1168).
log2515(T1270, T1271) :- log2454(T1270, T1271).
log2585(T1355, T1356) :- log2598(T1355, T1356).
log2650(T1426, T1427) :- log2598(T1426, T1427).
log2307(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T860)))))))))))))), T861) :- log2344(T860, s(s(s(s(s(s(s(0))))))), T861).
log2307(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T1530) :- log2822(s(s(s(s(s(s(s(0))))))), T1530).
log2307(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T1530) :- log2822(s(s(s(s(s(s(s(0))))))), T1530).
log2307(s(s(s(s(s(s(s(s(s(s(0)))))))))), T1620) :- log2889(s(s(s(s(s(s(s(0))))))), T1620).
log2307(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T1620) :- log2889(s(s(s(s(s(s(s(0))))))), T1620).
log2307(s(s(s(s(s(s(s(s(0)))))))), T1711) :- log2960(s(s(s(s(s(s(s(0))))))), T1711).
log2307(s(s(s(s(s(s(s(s(s(0))))))))), T1711) :- log2960(s(s(s(s(s(s(s(0))))))), T1711).
log2307(s(s(s(s(s(s(0)))))), T1769) :- log21012(s(s(s(s(s(s(s(0))))))), T1769).
log2307(s(s(s(s(s(s(s(0))))))), T1769) :- log21012(s(s(s(s(s(s(s(0))))))), T1769).
log2307(s(s(s(s(0)))), T1826) :- log21068(s(s(s(s(s(s(s(0))))))), T1826).
log2307(s(s(s(s(s(0))))), T1826) :- log21068(s(s(s(s(s(s(s(0))))))), T1826).
log2307(s(s(0)), T1844) :- log21106(s(s(s(s(s(s(s(0))))))), T1844).
log2307(s(s(s(0))), T1844) :- log21106(s(s(s(s(s(s(s(0))))))), T1844).
log21183(T1899) :- log21068(s(s(s(s(s(s(s(0))))))), T1899).
log21249(T1943) :- log21068(s(s(s(s(s(s(s(0))))))), T1943).
log21319(T1979) :- log21106(s(s(s(s(s(s(s(0))))))), T1979).
log21370(T2010) :- log21106(s(s(s(s(s(s(s(0))))))), T2010).
log2257(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T735)))))))))))))), T736) :- log2294(T735, s(s(s(s(s(s(s(0))))))), T736).
log2257(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T1876) :- log21183(T1876).
log2257(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T1876) :- log21183(T1876).
log2257(s(s(s(s(s(s(s(s(s(s(0)))))))))), T1920) :- log21249(T1920).
log2257(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T1920) :- log21249(T1920).
log2257(s(s(s(s(s(s(s(s(0)))))))), T1964) :- log21319(T1964).
log2257(s(s(s(s(s(s(s(s(s(0))))))))), T1964) :- log21319(T1964).
log2257(s(s(s(s(s(s(0)))))), T1995) :- log21370(T1995).
log2257(s(s(s(s(s(s(s(0))))))), T1995) :- log21370(T1995).
log2257(s(s(s(s(0)))), T2024) :- log21425(T2024).
log2257(s(s(s(s(s(0))))), T2024) :- log21425(T2024).
log2257(s(s(0)), T2037) :- log21462(T2037).
log2257(s(s(s(0))), T2037) :- log21462(T2037).
log21540(T2087) :- log21425(T2087).
log21606(T2131) :- log21425(T2131).
log21676(T2167) :- log21462(T2167).
log21727(T2198) :- log21462(T2198).
log2207(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T610)))))))))))))), T611) :- log2244(T610, s(s(s(s(s(s(s(0))))))), T611).
log2207(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2064) :- log21540(T2064).
log2207(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2064) :- log21540(T2064).
log2207(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2108) :- log21606(T2108).
log2207(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2108) :- log21606(T2108).
log2207(s(s(s(s(s(s(s(s(0)))))))), T2152) :- log21676(T2152).
log2207(s(s(s(s(s(s(s(s(s(0))))))))), T2152) :- log21676(T2152).
log2207(s(s(s(s(s(s(0)))))), T2183) :- log21727(T2183).
log2207(s(s(s(s(s(s(s(0))))))), T2183) :- log21727(T2183).
log2207(s(s(s(s(0)))), T2212) :- log21782(T2212).
log2207(s(s(s(s(s(0))))), T2212) :- log21782(T2212).
log2207(s(s(0)), T2225) :- log21819(T2225).
log2207(s(s(s(0))), T2225) :- log21819(T2225).
log21897(T2275) :- log21782(T2275).
log21963(T2319) :- log21782(T2319).
log22033(T2355) :- log21819(T2355).
log22084(T2386) :- log21819(T2386).
log2157(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T485)))))))))))))), T486) :- log2194(T485, s(s(s(s(s(s(s(0))))))), T486).
log2157(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2252) :- log21897(T2252).
log2157(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2252) :- log21897(T2252).
log2157(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2296) :- log21963(T2296).
log2157(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2296) :- log21963(T2296).
log2157(s(s(s(s(s(s(s(s(0)))))))), T2340) :- log22033(T2340).
log2157(s(s(s(s(s(s(s(s(s(0))))))))), T2340) :- log22033(T2340).
log2157(s(s(s(s(s(s(0)))))), T2371) :- log22084(T2371).
log2157(s(s(s(s(s(s(s(0))))))), T2371) :- log22084(T2371).
log2157(s(s(s(s(0)))), T2400) :- log22139(T2400).
log2157(s(s(s(s(s(0))))), T2400) :- log22139(T2400).
log2157(s(s(0)), T2413) :- log22176(T2413).
log2157(s(s(s(0))), T2413) :- log22176(T2413).
log22254(T2463) :- log22139(T2463).
log22320(T2507) :- log22139(T2507).
log22390(T2543) :- log22176(T2543).
log22441(T2574) :- log22176(T2574).
log2107(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T360)))))))))))))), T361) :- log2144(T360, s(s(s(s(s(s(s(0))))))), T361).
log2107(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2440) :- log22254(T2440).
log2107(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2440) :- log22254(T2440).
log2107(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2484) :- log22320(T2484).
log2107(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2484) :- log22320(T2484).
log2107(s(s(s(s(s(s(s(s(0)))))))), T2528) :- log22390(T2528).
log2107(s(s(s(s(s(s(s(s(s(0))))))))), T2528) :- log22390(T2528).
log2107(s(s(s(s(s(s(0)))))), T2559) :- log22441(T2559).
log2107(s(s(s(s(s(s(s(0))))))), T2559) :- log22441(T2559).
log2107(s(s(s(s(0)))), T2588) :- log22496(T2588).
log2107(s(s(s(s(s(0))))), T2588) :- log22496(T2588).
log2107(s(s(0)), T2601) :- log22533(T2601).
log2107(s(s(s(0))), T2601) :- log22533(T2601).
log22611(T2651) :- log22496(T2651).
log22677(T2695) :- log22496(T2695).
log22747(T2731) :- log22533(T2731).
log22798(T2762) :- log22533(T2762).
log257(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T235)))))))))))))), T236) :- log294(T235, s(s(s(s(s(s(s(0))))))), T236).
log257(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2628) :- log22611(T2628).
log257(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2628) :- log22611(T2628).
log257(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2672) :- log22677(T2672).
log257(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2672) :- log22677(T2672).
log257(s(s(s(s(s(s(s(s(0)))))))), T2716) :- log22747(T2716).
log257(s(s(s(s(s(s(s(s(s(0))))))))), T2716) :- log22747(T2716).
log257(s(s(s(s(s(s(0)))))), T2747) :- log22798(T2747).
log257(s(s(s(s(s(s(s(0))))))), T2747) :- log22798(T2747).
log257(s(s(s(s(0)))), T2776) :- log22853(T2776).
log257(s(s(s(s(s(0))))), T2776) :- log22853(T2776).
log257(s(s(0)), T2789) :- log22890(T2789).
log257(s(s(s(0))), T2789) :- log22890(T2789).
log22968(T2843) :- log22853(T2843).
log23034(T2891) :- log22853(T2891).
log23104(T2931) :- log22890(T2931).
log23155(T2966) :- log22890(T2966).
log2822(T1578, T1579) :- log2705(T1578, T1579).
log2889(T1668, T1669) :- log2705(T1668, T1669).
log2960(T1743, T1744) :- log2742(T1743, T1744).
log21012(T1801, T1802) :- log2742(T1801, T1802).
log21(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T109)))))))))))))))), T108) :- log244(T109, s(s(s(s(s(s(s(0))))))), T108).
log21(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))), T2819) :- log22968(T2819).
log21(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))), T2819) :- log22968(T2819).
log21(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2867) :- log23034(T2867).
log21(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2867) :- log23034(T2867).
log21(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2915) :- log23104(T2915).
log21(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2915) :- log23104(T2915).
log21(s(s(s(s(s(s(s(s(0)))))))), T2950) :- log23155(T2950).
log21(s(s(s(s(s(s(s(s(s(0))))))))), T2950) :- log23155(T2950).
log21(s(s(s(s(s(s(0)))))), T2983) :- log23210(T2983).
log21(s(s(s(s(s(s(s(0))))))), T2983) :- log23210(T2983).
log21(s(s(s(s(0)))), T3000) :- log23247(T3000).
log21(s(s(s(s(s(0))))), T3000) :- log23247(T3000).

Clauses:

log2c44(s(s(T131)), T129, T130) :- log2c44(T131, s(T129), T130).
log2c44(0, s(T148), T149) :- log2c57(T148, T149).
log2c44(s(0), s(T148), T149) :- log2c57(T148, T149).
log2c44(0, 0, s(0)).
log2c44(s(0), 0, s(0)).
log2c94(s(s(T255)), T256, T257) :- log2c94(T255, s(T256), T257).
log2c94(0, s(T274), T275) :- log2c107(T274, T275).
log2c94(s(0), s(T274), T275) :- log2c107(T274, T275).
log2c94(0, 0, s(s(0))).
log2c94(s(0), 0, s(s(0))).
log2c144(s(s(T380)), T381, T382) :- log2c144(T380, s(T381), T382).
log2c144(0, s(T399), T400) :- log2c157(T399, T400).
log2c144(s(0), s(T399), T400) :- log2c157(T399, T400).
log2c144(0, 0, s(s(s(0)))).
log2c144(s(0), 0, s(s(s(0)))).
log2c194(s(s(T505)), T506, T507) :- log2c194(T505, s(T506), T507).
log2c194(0, s(T524), T525) :- log2c207(T524, T525).
log2c194(s(0), s(T524), T525) :- log2c207(T524, T525).
log2c194(0, 0, s(s(s(s(0))))).
log2c194(s(0), 0, s(s(s(s(0))))).
log2c244(s(s(T630)), T631, T632) :- log2c244(T630, s(T631), T632).
log2c244(0, s(T649), T650) :- log2c257(T649, T650).
log2c244(s(0), s(T649), T650) :- log2c257(T649, T650).
log2c244(0, 0, s(s(s(s(s(0)))))).
log2c244(s(0), 0, s(s(s(s(s(0)))))).
log2c294(s(s(T755)), T756, T757) :- log2c294(T755, s(T756), T757).
log2c294(0, s(T774), T775) :- log2c307(T774, T775).
log2c294(s(0), s(T774), T775) :- log2c307(T774, T775).
log2c294(0, 0, s(s(s(s(s(s(0))))))).
log2c294(s(0), 0, s(s(s(s(s(s(0))))))).
log2c344(s(s(T880)), T881, T882) :- log2c344(T880, s(T881), T882).
log2c344(0, s(T899), T900) :- log2c359(T899, s(s(s(s(s(s(s(0))))))), T900).
log2c344(s(0), s(T899), T900) :- log2c359(T899, s(s(s(s(s(s(s(0))))))), T900).
log2c344(0, 0, s(s(s(s(s(s(s(0)))))))).
log2c344(s(0), 0, s(s(s(s(s(s(s(0)))))))).
log2c395(s(s(T1056)), T1057, T1058, T1059) :- log2c395(T1056, s(T1057), T1058, T1059).
log2c395(0, s(T1081), T1082, T1083) :- log2c359(T1081, s(T1082), T1083).
log2c395(s(0), s(T1081), T1082, T1083) :- log2c359(T1081, s(T1082), T1083).
log2c395(0, 0, T1101, s(T1101)).
log2c395(s(0), 0, T1101, s(T1101)).
log2c359(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1029)))))))))))))), T1030, T1031) :- log2c395(T1029, s(s(s(s(s(s(s(0))))))), T1030, T1031).
log2c359(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T1119, T1120) :- log2c437(T1119, T1120).
log2c359(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T1119, T1120) :- log2c437(T1119, T1120).
log2c359(s(s(s(s(s(s(s(s(s(s(0)))))))))), T1222, T1223) :- log2c515(T1222, T1223).
log2c359(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T1222, T1223) :- log2c515(T1222, T1223).
log2c359(s(s(s(s(s(s(s(s(0)))))))), T1323, T1324) :- log2c585(T1323, T1324).
log2c359(s(s(s(s(s(s(s(s(s(0))))))))), T1323, T1324) :- log2c585(T1323, T1324).
log2c359(s(s(s(s(s(s(0)))))), T1394, T1395) :- log2c650(T1394, T1395).
log2c359(s(s(s(s(s(s(s(0))))))), T1394, T1395) :- log2c650(T1394, T1395).
log2c359(s(s(s(s(0)))), T1461, T1462) :- log2c705(T1461, T1462).
log2c359(s(s(s(s(s(0))))), T1461, T1462) :- log2c705(T1461, T1462).
log2c359(s(s(0)), T1490, T1491) :- log2c742(T1490, T1491).
log2c359(s(s(s(0))), T1490, T1491) :- log2c742(T1490, T1491).
log2c359(0, T1510, s(T1510)).
log2c359(s(0), T1510, s(T1510)).
log2c437(T1167, T1168) :- log2c454(T1167, T1168).
log2c454(T1174, s(s(s(T1174)))).
log2c515(T1270, T1271) :- log2c454(T1270, T1271).
log2c585(T1355, T1356) :- log2c598(T1355, T1356).
log2c598(T1362, s(s(s(T1362)))).
log2c650(T1426, T1427) :- log2c598(T1426, T1427).
log2c705(T1467, s(s(T1467))).
log2c742(T1496, s(s(T1496))).
log2c307(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T860)))))))))))))), T861) :- log2c344(T860, s(s(s(s(s(s(s(0))))))), T861).
log2c307(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T1530) :- log2c822(s(s(s(s(s(s(s(0))))))), T1530).
log2c307(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T1530) :- log2c822(s(s(s(s(s(s(s(0))))))), T1530).
log2c307(s(s(s(s(s(s(s(s(s(s(0)))))))))), T1620) :- log2c889(s(s(s(s(s(s(s(0))))))), T1620).
log2c307(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T1620) :- log2c889(s(s(s(s(s(s(s(0))))))), T1620).
log2c307(s(s(s(s(s(s(s(s(0)))))))), T1711) :- log2c960(s(s(s(s(s(s(s(0))))))), T1711).
log2c307(s(s(s(s(s(s(s(s(s(0))))))))), T1711) :- log2c960(s(s(s(s(s(s(s(0))))))), T1711).
log2c307(s(s(s(s(s(s(0)))))), T1769) :- log2c1012(s(s(s(s(s(s(s(0))))))), T1769).
log2c307(s(s(s(s(s(s(s(0))))))), T1769) :- log2c1012(s(s(s(s(s(s(s(0))))))), T1769).
log2c307(s(s(s(s(0)))), T1826) :- log2c1068(s(s(s(s(s(s(s(0))))))), T1826).
log2c307(s(s(s(s(s(0))))), T1826) :- log2c1068(s(s(s(s(s(s(s(0))))))), T1826).
log2c307(s(s(0)), T1844) :- log2c1106(s(s(s(s(s(s(s(0))))))), T1844).
log2c307(s(s(s(0))), T1844) :- log2c1106(s(s(s(s(s(s(s(0))))))), T1844).
log2c307(0, s(s(s(s(s(s(s(0)))))))).
log2c307(s(0), s(s(s(s(s(s(s(0)))))))).
log2c1183(T1899) :- log2c1068(s(s(s(s(s(s(s(0))))))), T1899).
log2c1249(T1943) :- log2c1068(s(s(s(s(s(s(s(0))))))), T1943).
log2c1319(T1979) :- log2c1106(s(s(s(s(s(s(s(0))))))), T1979).
log2c1370(T2010) :- log2c1106(s(s(s(s(s(s(s(0))))))), T2010).
log2c1425(s(s(s(s(s(s(s(0)))))))).
log2c1462(s(s(s(s(s(s(s(0)))))))).
log2c257(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T735)))))))))))))), T736) :- log2c294(T735, s(s(s(s(s(s(s(0))))))), T736).
log2c257(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T1876) :- log2c1183(T1876).
log2c257(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T1876) :- log2c1183(T1876).
log2c257(s(s(s(s(s(s(s(s(s(s(0)))))))))), T1920) :- log2c1249(T1920).
log2c257(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T1920) :- log2c1249(T1920).
log2c257(s(s(s(s(s(s(s(s(0)))))))), T1964) :- log2c1319(T1964).
log2c257(s(s(s(s(s(s(s(s(s(0))))))))), T1964) :- log2c1319(T1964).
log2c257(s(s(s(s(s(s(0)))))), T1995) :- log2c1370(T1995).
log2c257(s(s(s(s(s(s(s(0))))))), T1995) :- log2c1370(T1995).
log2c257(s(s(s(s(0)))), T2024) :- log2c1425(T2024).
log2c257(s(s(s(s(s(0))))), T2024) :- log2c1425(T2024).
log2c257(s(s(0)), T2037) :- log2c1462(T2037).
log2c257(s(s(s(0))), T2037) :- log2c1462(T2037).
log2c257(0, s(s(s(s(s(s(0))))))).
log2c257(s(0), s(s(s(s(s(s(0))))))).
log2c1540(T2087) :- log2c1425(T2087).
log2c1606(T2131) :- log2c1425(T2131).
log2c1676(T2167) :- log2c1462(T2167).
log2c1727(T2198) :- log2c1462(T2198).
log2c1782(s(s(s(s(s(s(0))))))).
log2c1819(s(s(s(s(s(s(0))))))).
log2c207(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T610)))))))))))))), T611) :- log2c244(T610, s(s(s(s(s(s(s(0))))))), T611).
log2c207(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2064) :- log2c1540(T2064).
log2c207(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2064) :- log2c1540(T2064).
log2c207(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2108) :- log2c1606(T2108).
log2c207(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2108) :- log2c1606(T2108).
log2c207(s(s(s(s(s(s(s(s(0)))))))), T2152) :- log2c1676(T2152).
log2c207(s(s(s(s(s(s(s(s(s(0))))))))), T2152) :- log2c1676(T2152).
log2c207(s(s(s(s(s(s(0)))))), T2183) :- log2c1727(T2183).
log2c207(s(s(s(s(s(s(s(0))))))), T2183) :- log2c1727(T2183).
log2c207(s(s(s(s(0)))), T2212) :- log2c1782(T2212).
log2c207(s(s(s(s(s(0))))), T2212) :- log2c1782(T2212).
log2c207(s(s(0)), T2225) :- log2c1819(T2225).
log2c207(s(s(s(0))), T2225) :- log2c1819(T2225).
log2c207(0, s(s(s(s(s(0)))))).
log2c207(s(0), s(s(s(s(s(0)))))).
log2c1897(T2275) :- log2c1782(T2275).
log2c1963(T2319) :- log2c1782(T2319).
log2c2033(T2355) :- log2c1819(T2355).
log2c2084(T2386) :- log2c1819(T2386).
log2c2139(s(s(s(s(s(0)))))).
log2c2176(s(s(s(s(s(0)))))).
log2c157(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T485)))))))))))))), T486) :- log2c194(T485, s(s(s(s(s(s(s(0))))))), T486).
log2c157(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2252) :- log2c1897(T2252).
log2c157(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2252) :- log2c1897(T2252).
log2c157(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2296) :- log2c1963(T2296).
log2c157(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2296) :- log2c1963(T2296).
log2c157(s(s(s(s(s(s(s(s(0)))))))), T2340) :- log2c2033(T2340).
log2c157(s(s(s(s(s(s(s(s(s(0))))))))), T2340) :- log2c2033(T2340).
log2c157(s(s(s(s(s(s(0)))))), T2371) :- log2c2084(T2371).
log2c157(s(s(s(s(s(s(s(0))))))), T2371) :- log2c2084(T2371).
log2c157(s(s(s(s(0)))), T2400) :- log2c2139(T2400).
log2c157(s(s(s(s(s(0))))), T2400) :- log2c2139(T2400).
log2c157(s(s(0)), T2413) :- log2c2176(T2413).
log2c157(s(s(s(0))), T2413) :- log2c2176(T2413).
log2c157(0, s(s(s(s(0))))).
log2c157(s(0), s(s(s(s(0))))).
log2c2254(T2463) :- log2c2139(T2463).
log2c2320(T2507) :- log2c2139(T2507).
log2c2390(T2543) :- log2c2176(T2543).
log2c2441(T2574) :- log2c2176(T2574).
log2c2496(s(s(s(s(0))))).
log2c2533(s(s(s(s(0))))).
log2c107(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T360)))))))))))))), T361) :- log2c144(T360, s(s(s(s(s(s(s(0))))))), T361).
log2c107(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2440) :- log2c2254(T2440).
log2c107(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2440) :- log2c2254(T2440).
log2c107(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2484) :- log2c2320(T2484).
log2c107(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2484) :- log2c2320(T2484).
log2c107(s(s(s(s(s(s(s(s(0)))))))), T2528) :- log2c2390(T2528).
log2c107(s(s(s(s(s(s(s(s(s(0))))))))), T2528) :- log2c2390(T2528).
log2c107(s(s(s(s(s(s(0)))))), T2559) :- log2c2441(T2559).
log2c107(s(s(s(s(s(s(s(0))))))), T2559) :- log2c2441(T2559).
log2c107(s(s(s(s(0)))), T2588) :- log2c2496(T2588).
log2c107(s(s(s(s(s(0))))), T2588) :- log2c2496(T2588).
log2c107(s(s(0)), T2601) :- log2c2533(T2601).
log2c107(s(s(s(0))), T2601) :- log2c2533(T2601).
log2c107(0, s(s(s(0)))).
log2c107(s(0), s(s(s(0)))).
log2c2611(T2651) :- log2c2496(T2651).
log2c2677(T2695) :- log2c2496(T2695).
log2c2747(T2731) :- log2c2533(T2731).
log2c2798(T2762) :- log2c2533(T2762).
log2c2853(s(s(s(0)))).
log2c2890(s(s(s(0)))).
log2c57(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T235)))))))))))))), T236) :- log2c94(T235, s(s(s(s(s(s(s(0))))))), T236).
log2c57(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2628) :- log2c2611(T2628).
log2c57(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2628) :- log2c2611(T2628).
log2c57(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2672) :- log2c2677(T2672).
log2c57(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2672) :- log2c2677(T2672).
log2c57(s(s(s(s(s(s(s(s(0)))))))), T2716) :- log2c2747(T2716).
log2c57(s(s(s(s(s(s(s(s(s(0))))))))), T2716) :- log2c2747(T2716).
log2c57(s(s(s(s(s(s(0)))))), T2747) :- log2c2798(T2747).
log2c57(s(s(s(s(s(s(s(0))))))), T2747) :- log2c2798(T2747).
log2c57(s(s(s(s(0)))), T2776) :- log2c2853(T2776).
log2c57(s(s(s(s(s(0))))), T2776) :- log2c2853(T2776).
log2c57(s(s(0)), T2789) :- log2c2890(T2789).
log2c57(s(s(s(0))), T2789) :- log2c2890(T2789).
log2c57(0, s(s(0))).
log2c57(s(0), s(s(0))).
log2c2968(T2843) :- log2c2853(T2843).
log2c3034(T2891) :- log2c2853(T2891).
log2c3104(T2931) :- log2c2890(T2931).
log2c3155(T2966) :- log2c2890(T2966).
log2c3210(s(s(0))).
log2c3247(s(s(0))).
log2c822(T1578, T1579) :- log2c705(T1578, T1579).
log2c889(T1668, T1669) :- log2c705(T1668, T1669).
log2c960(T1743, T1744) :- log2c742(T1743, T1744).
log2c1012(T1801, T1802) :- log2c742(T1801, T1802).
log2c1068(T1831, s(T1831)).
log2c1106(T1849, s(T1849)).

Afs:

log21(x1, x2)  =  log21(x2)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

log244(s(s(T131)), T129, T130) :- log244(T131, s(T129), T130).
log244(0, s(T148), T149) :- log257(T148, T149).
log244(s(0), s(T148), T149) :- log257(T148, T149).
log294(s(s(T255)), T256, T257) :- log294(T255, s(T256), T257).
log294(0, s(T274), T275) :- log2107(T274, T275).
log294(s(0), s(T274), T275) :- log2107(T274, T275).
log2144(s(s(T380)), T381, T382) :- log2144(T380, s(T381), T382).
log2144(0, s(T399), T400) :- log2157(T399, T400).
log2144(s(0), s(T399), T400) :- log2157(T399, T400).
log2194(s(s(T505)), T506, T507) :- log2194(T505, s(T506), T507).
log2194(0, s(T524), T525) :- log2207(T524, T525).
log2194(s(0), s(T524), T525) :- log2207(T524, T525).
log2244(s(s(T630)), T631, T632) :- log2244(T630, s(T631), T632).
log2244(0, s(T649), T650) :- log2257(T649, T650).
log2244(s(0), s(T649), T650) :- log2257(T649, T650).
log2294(s(s(T755)), T756, T757) :- log2294(T755, s(T756), T757).
log2294(0, s(T774), T775) :- log2307(T774, T775).
log2294(s(0), s(T774), T775) :- log2307(T774, T775).
log2344(s(s(T880)), T881, T882) :- log2344(T880, s(T881), T882).
log2344(0, s(T899), T900) :- log2359(T899, s(s(s(s(s(s(s(0))))))), T900).
log2344(s(0), s(T899), T900) :- log2359(T899, s(s(s(s(s(s(s(0))))))), T900).
log2395(s(s(T1056)), T1057, T1058, T1059) :- log2395(T1056, s(T1057), T1058, T1059).
log2395(0, s(T1081), T1082, T1083) :- log2359(T1081, s(T1082), T1083).
log2395(s(0), s(T1081), T1082, T1083) :- log2359(T1081, s(T1082), T1083).
log2359(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1029)))))))))))))), T1030, T1031) :- log2395(T1029, s(s(s(s(s(s(s(0))))))), T1030, T1031).
log2307(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T860)))))))))))))), T861) :- log2344(T860, s(s(s(s(s(s(s(0))))))), T861).
log2257(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T735)))))))))))))), T736) :- log2294(T735, s(s(s(s(s(s(s(0))))))), T736).
log2207(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T610)))))))))))))), T611) :- log2244(T610, s(s(s(s(s(s(s(0))))))), T611).
log2157(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T485)))))))))))))), T486) :- log2194(T485, s(s(s(s(s(s(s(0))))))), T486).
log2107(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T360)))))))))))))), T361) :- log2144(T360, s(s(s(s(s(s(s(0))))))), T361).
log257(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T235)))))))))))))), T236) :- log294(T235, s(s(s(s(s(s(s(0))))))), T236).
log21(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T109)))))))))))))))), T108) :- log244(T109, s(s(s(s(s(s(s(0))))))), T108).

Clauses:

log2c44(s(s(T131)), T129, T130) :- log2c44(T131, s(T129), T130).
log2c44(0, s(T148), T149) :- log2c57(T148, T149).
log2c44(s(0), s(T148), T149) :- log2c57(T148, T149).
log2c44(0, 0, s(0)).
log2c44(s(0), 0, s(0)).
log2c94(s(s(T255)), T256, T257) :- log2c94(T255, s(T256), T257).
log2c94(0, s(T274), T275) :- log2c107(T274, T275).
log2c94(s(0), s(T274), T275) :- log2c107(T274, T275).
log2c94(0, 0, s(s(0))).
log2c94(s(0), 0, s(s(0))).
log2c144(s(s(T380)), T381, T382) :- log2c144(T380, s(T381), T382).
log2c144(0, s(T399), T400) :- log2c157(T399, T400).
log2c144(s(0), s(T399), T400) :- log2c157(T399, T400).
log2c144(0, 0, s(s(s(0)))).
log2c144(s(0), 0, s(s(s(0)))).
log2c194(s(s(T505)), T506, T507) :- log2c194(T505, s(T506), T507).
log2c194(0, s(T524), T525) :- log2c207(T524, T525).
log2c194(s(0), s(T524), T525) :- log2c207(T524, T525).
log2c194(0, 0, s(s(s(s(0))))).
log2c194(s(0), 0, s(s(s(s(0))))).
log2c244(s(s(T630)), T631, T632) :- log2c244(T630, s(T631), T632).
log2c244(0, s(T649), T650) :- log2c257(T649, T650).
log2c244(s(0), s(T649), T650) :- log2c257(T649, T650).
log2c244(0, 0, s(s(s(s(s(0)))))).
log2c244(s(0), 0, s(s(s(s(s(0)))))).
log2c294(s(s(T755)), T756, T757) :- log2c294(T755, s(T756), T757).
log2c294(0, s(T774), T775) :- log2c307(T774, T775).
log2c294(s(0), s(T774), T775) :- log2c307(T774, T775).
log2c294(0, 0, s(s(s(s(s(s(0))))))).
log2c294(s(0), 0, s(s(s(s(s(s(0))))))).
log2c344(s(s(T880)), T881, T882) :- log2c344(T880, s(T881), T882).
log2c344(0, s(T899), T900) :- log2c359(T899, s(s(s(s(s(s(s(0))))))), T900).
log2c344(s(0), s(T899), T900) :- log2c359(T899, s(s(s(s(s(s(s(0))))))), T900).
log2c344(0, 0, s(s(s(s(s(s(s(0)))))))).
log2c344(s(0), 0, s(s(s(s(s(s(s(0)))))))).
log2c395(s(s(T1056)), T1057, T1058, T1059) :- log2c395(T1056, s(T1057), T1058, T1059).
log2c395(0, s(T1081), T1082, T1083) :- log2c359(T1081, s(T1082), T1083).
log2c395(s(0), s(T1081), T1082, T1083) :- log2c359(T1081, s(T1082), T1083).
log2c395(0, 0, T1101, s(T1101)).
log2c395(s(0), 0, T1101, s(T1101)).
log2c359(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1029)))))))))))))), T1030, T1031) :- log2c395(T1029, s(s(s(s(s(s(s(0))))))), T1030, T1031).
log2c359(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T1119, T1120) :- log2c437(T1119, T1120).
log2c359(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T1119, T1120) :- log2c437(T1119, T1120).
log2c359(s(s(s(s(s(s(s(s(s(s(0)))))))))), T1222, T1223) :- log2c515(T1222, T1223).
log2c359(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T1222, T1223) :- log2c515(T1222, T1223).
log2c359(s(s(s(s(s(s(s(s(0)))))))), T1323, T1324) :- log2c585(T1323, T1324).
log2c359(s(s(s(s(s(s(s(s(s(0))))))))), T1323, T1324) :- log2c585(T1323, T1324).
log2c359(s(s(s(s(s(s(0)))))), T1394, T1395) :- log2c650(T1394, T1395).
log2c359(s(s(s(s(s(s(s(0))))))), T1394, T1395) :- log2c650(T1394, T1395).
log2c359(s(s(s(s(0)))), T1461, T1462) :- log2c705(T1461, T1462).
log2c359(s(s(s(s(s(0))))), T1461, T1462) :- log2c705(T1461, T1462).
log2c359(s(s(0)), T1490, T1491) :- log2c742(T1490, T1491).
log2c359(s(s(s(0))), T1490, T1491) :- log2c742(T1490, T1491).
log2c359(0, T1510, s(T1510)).
log2c359(s(0), T1510, s(T1510)).
log2c437(T1167, T1168) :- log2c454(T1167, T1168).
log2c454(T1174, s(s(s(T1174)))).
log2c515(T1270, T1271) :- log2c454(T1270, T1271).
log2c585(T1355, T1356) :- log2c598(T1355, T1356).
log2c598(T1362, s(s(s(T1362)))).
log2c650(T1426, T1427) :- log2c598(T1426, T1427).
log2c705(T1467, s(s(T1467))).
log2c742(T1496, s(s(T1496))).
log2c307(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T860)))))))))))))), T861) :- log2c344(T860, s(s(s(s(s(s(s(0))))))), T861).
log2c307(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T1530) :- log2c822(s(s(s(s(s(s(s(0))))))), T1530).
log2c307(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T1530) :- log2c822(s(s(s(s(s(s(s(0))))))), T1530).
log2c307(s(s(s(s(s(s(s(s(s(s(0)))))))))), T1620) :- log2c889(s(s(s(s(s(s(s(0))))))), T1620).
log2c307(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T1620) :- log2c889(s(s(s(s(s(s(s(0))))))), T1620).
log2c307(s(s(s(s(s(s(s(s(0)))))))), T1711) :- log2c960(s(s(s(s(s(s(s(0))))))), T1711).
log2c307(s(s(s(s(s(s(s(s(s(0))))))))), T1711) :- log2c960(s(s(s(s(s(s(s(0))))))), T1711).
log2c307(s(s(s(s(s(s(0)))))), T1769) :- log2c1012(s(s(s(s(s(s(s(0))))))), T1769).
log2c307(s(s(s(s(s(s(s(0))))))), T1769) :- log2c1012(s(s(s(s(s(s(s(0))))))), T1769).
log2c307(s(s(s(s(0)))), T1826) :- log2c1068(s(s(s(s(s(s(s(0))))))), T1826).
log2c307(s(s(s(s(s(0))))), T1826) :- log2c1068(s(s(s(s(s(s(s(0))))))), T1826).
log2c307(s(s(0)), T1844) :- log2c1106(s(s(s(s(s(s(s(0))))))), T1844).
log2c307(s(s(s(0))), T1844) :- log2c1106(s(s(s(s(s(s(s(0))))))), T1844).
log2c307(0, s(s(s(s(s(s(s(0)))))))).
log2c307(s(0), s(s(s(s(s(s(s(0)))))))).
log2c1183(T1899) :- log2c1068(s(s(s(s(s(s(s(0))))))), T1899).
log2c1249(T1943) :- log2c1068(s(s(s(s(s(s(s(0))))))), T1943).
log2c1319(T1979) :- log2c1106(s(s(s(s(s(s(s(0))))))), T1979).
log2c1370(T2010) :- log2c1106(s(s(s(s(s(s(s(0))))))), T2010).
log2c1425(s(s(s(s(s(s(s(0)))))))).
log2c1462(s(s(s(s(s(s(s(0)))))))).
log2c257(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T735)))))))))))))), T736) :- log2c294(T735, s(s(s(s(s(s(s(0))))))), T736).
log2c257(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T1876) :- log2c1183(T1876).
log2c257(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T1876) :- log2c1183(T1876).
log2c257(s(s(s(s(s(s(s(s(s(s(0)))))))))), T1920) :- log2c1249(T1920).
log2c257(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T1920) :- log2c1249(T1920).
log2c257(s(s(s(s(s(s(s(s(0)))))))), T1964) :- log2c1319(T1964).
log2c257(s(s(s(s(s(s(s(s(s(0))))))))), T1964) :- log2c1319(T1964).
log2c257(s(s(s(s(s(s(0)))))), T1995) :- log2c1370(T1995).
log2c257(s(s(s(s(s(s(s(0))))))), T1995) :- log2c1370(T1995).
log2c257(s(s(s(s(0)))), T2024) :- log2c1425(T2024).
log2c257(s(s(s(s(s(0))))), T2024) :- log2c1425(T2024).
log2c257(s(s(0)), T2037) :- log2c1462(T2037).
log2c257(s(s(s(0))), T2037) :- log2c1462(T2037).
log2c257(0, s(s(s(s(s(s(0))))))).
log2c257(s(0), s(s(s(s(s(s(0))))))).
log2c1540(T2087) :- log2c1425(T2087).
log2c1606(T2131) :- log2c1425(T2131).
log2c1676(T2167) :- log2c1462(T2167).
log2c1727(T2198) :- log2c1462(T2198).
log2c1782(s(s(s(s(s(s(0))))))).
log2c1819(s(s(s(s(s(s(0))))))).
log2c207(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T610)))))))))))))), T611) :- log2c244(T610, s(s(s(s(s(s(s(0))))))), T611).
log2c207(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2064) :- log2c1540(T2064).
log2c207(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2064) :- log2c1540(T2064).
log2c207(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2108) :- log2c1606(T2108).
log2c207(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2108) :- log2c1606(T2108).
log2c207(s(s(s(s(s(s(s(s(0)))))))), T2152) :- log2c1676(T2152).
log2c207(s(s(s(s(s(s(s(s(s(0))))))))), T2152) :- log2c1676(T2152).
log2c207(s(s(s(s(s(s(0)))))), T2183) :- log2c1727(T2183).
log2c207(s(s(s(s(s(s(s(0))))))), T2183) :- log2c1727(T2183).
log2c207(s(s(s(s(0)))), T2212) :- log2c1782(T2212).
log2c207(s(s(s(s(s(0))))), T2212) :- log2c1782(T2212).
log2c207(s(s(0)), T2225) :- log2c1819(T2225).
log2c207(s(s(s(0))), T2225) :- log2c1819(T2225).
log2c207(0, s(s(s(s(s(0)))))).
log2c207(s(0), s(s(s(s(s(0)))))).
log2c1897(T2275) :- log2c1782(T2275).
log2c1963(T2319) :- log2c1782(T2319).
log2c2033(T2355) :- log2c1819(T2355).
log2c2084(T2386) :- log2c1819(T2386).
log2c2139(s(s(s(s(s(0)))))).
log2c2176(s(s(s(s(s(0)))))).
log2c157(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T485)))))))))))))), T486) :- log2c194(T485, s(s(s(s(s(s(s(0))))))), T486).
log2c157(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2252) :- log2c1897(T2252).
log2c157(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2252) :- log2c1897(T2252).
log2c157(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2296) :- log2c1963(T2296).
log2c157(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2296) :- log2c1963(T2296).
log2c157(s(s(s(s(s(s(s(s(0)))))))), T2340) :- log2c2033(T2340).
log2c157(s(s(s(s(s(s(s(s(s(0))))))))), T2340) :- log2c2033(T2340).
log2c157(s(s(s(s(s(s(0)))))), T2371) :- log2c2084(T2371).
log2c157(s(s(s(s(s(s(s(0))))))), T2371) :- log2c2084(T2371).
log2c157(s(s(s(s(0)))), T2400) :- log2c2139(T2400).
log2c157(s(s(s(s(s(0))))), T2400) :- log2c2139(T2400).
log2c157(s(s(0)), T2413) :- log2c2176(T2413).
log2c157(s(s(s(0))), T2413) :- log2c2176(T2413).
log2c157(0, s(s(s(s(0))))).
log2c157(s(0), s(s(s(s(0))))).
log2c2254(T2463) :- log2c2139(T2463).
log2c2320(T2507) :- log2c2139(T2507).
log2c2390(T2543) :- log2c2176(T2543).
log2c2441(T2574) :- log2c2176(T2574).
log2c2496(s(s(s(s(0))))).
log2c2533(s(s(s(s(0))))).
log2c107(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T360)))))))))))))), T361) :- log2c144(T360, s(s(s(s(s(s(s(0))))))), T361).
log2c107(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2440) :- log2c2254(T2440).
log2c107(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2440) :- log2c2254(T2440).
log2c107(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2484) :- log2c2320(T2484).
log2c107(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2484) :- log2c2320(T2484).
log2c107(s(s(s(s(s(s(s(s(0)))))))), T2528) :- log2c2390(T2528).
log2c107(s(s(s(s(s(s(s(s(s(0))))))))), T2528) :- log2c2390(T2528).
log2c107(s(s(s(s(s(s(0)))))), T2559) :- log2c2441(T2559).
log2c107(s(s(s(s(s(s(s(0))))))), T2559) :- log2c2441(T2559).
log2c107(s(s(s(s(0)))), T2588) :- log2c2496(T2588).
log2c107(s(s(s(s(s(0))))), T2588) :- log2c2496(T2588).
log2c107(s(s(0)), T2601) :- log2c2533(T2601).
log2c107(s(s(s(0))), T2601) :- log2c2533(T2601).
log2c107(0, s(s(s(0)))).
log2c107(s(0), s(s(s(0)))).
log2c2611(T2651) :- log2c2496(T2651).
log2c2677(T2695) :- log2c2496(T2695).
log2c2747(T2731) :- log2c2533(T2731).
log2c2798(T2762) :- log2c2533(T2762).
log2c2853(s(s(s(0)))).
log2c2890(s(s(s(0)))).
log2c57(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T235)))))))))))))), T236) :- log2c94(T235, s(s(s(s(s(s(s(0))))))), T236).
log2c57(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2628) :- log2c2611(T2628).
log2c57(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2628) :- log2c2611(T2628).
log2c57(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2672) :- log2c2677(T2672).
log2c57(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2672) :- log2c2677(T2672).
log2c57(s(s(s(s(s(s(s(s(0)))))))), T2716) :- log2c2747(T2716).
log2c57(s(s(s(s(s(s(s(s(s(0))))))))), T2716) :- log2c2747(T2716).
log2c57(s(s(s(s(s(s(0)))))), T2747) :- log2c2798(T2747).
log2c57(s(s(s(s(s(s(s(0))))))), T2747) :- log2c2798(T2747).
log2c57(s(s(s(s(0)))), T2776) :- log2c2853(T2776).
log2c57(s(s(s(s(s(0))))), T2776) :- log2c2853(T2776).
log2c57(s(s(0)), T2789) :- log2c2890(T2789).
log2c57(s(s(s(0))), T2789) :- log2c2890(T2789).
log2c57(0, s(s(0))).
log2c57(s(0), s(s(0))).
log2c2968(T2843) :- log2c2853(T2843).
log2c3034(T2891) :- log2c2853(T2891).
log2c3104(T2931) :- log2c2890(T2931).
log2c3155(T2966) :- log2c2890(T2966).
log2c3210(s(s(0))).
log2c3247(s(s(0))).
log2c822(T1578, T1579) :- log2c705(T1578, T1579).
log2c889(T1668, T1669) :- log2c705(T1668, T1669).
log2c960(T1743, T1744) :- log2c742(T1743, T1744).
log2c1012(T1801, T1802) :- log2c742(T1801, T1802).
log2c1068(T1831, s(T1831)).
log2c1106(T1849, s(T1849)).

Afs:

log21(x1, x2)  =  log21(x2)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
log21_in: (f,b)
log244_in: (f,b,b)
log257_in: (b,b)
log294_in: (b,b,b)
log2107_in: (b,b)
log2144_in: (b,b,b)
log2157_in: (b,b)
log2194_in: (b,b,b)
log2207_in: (b,b)
log2244_in: (b,b,b)
log2257_in: (b,b)
log2294_in: (b,b,b)
log2307_in: (b,b)
log2344_in: (b,b,b)
log2359_in: (b,b,b)
log2395_in: (b,b,b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

LOG21_IN_AG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T109)))))))))))))))), T108) → U32_AG(T109, T108, log244_in_agg(T109, s(s(s(s(s(s(s(0))))))), T108))
LOG21_IN_AG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T109)))))))))))))))), T108) → LOG244_IN_AGG(T109, s(s(s(s(s(s(s(0))))))), T108)
LOG244_IN_AGG(s(s(T131)), T129, T130) → U1_AGG(T131, T129, T130, log244_in_agg(T131, s(T129), T130))
LOG244_IN_AGG(s(s(T131)), T129, T130) → LOG244_IN_AGG(T131, s(T129), T130)
LOG244_IN_AGG(0, s(T148), T149) → U2_AGG(T148, T149, log257_in_gg(T148, T149))
LOG244_IN_AGG(0, s(T148), T149) → LOG257_IN_GG(T148, T149)
LOG257_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T235)))))))))))))), T236) → U31_GG(T235, T236, log294_in_ggg(T235, s(s(s(s(s(s(s(0))))))), T236))
LOG257_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T235)))))))))))))), T236) → LOG294_IN_GGG(T235, s(s(s(s(s(s(s(0))))))), T236)
LOG294_IN_GGG(s(s(T255)), T256, T257) → U4_GGG(T255, T256, T257, log294_in_ggg(T255, s(T256), T257))
LOG294_IN_GGG(s(s(T255)), T256, T257) → LOG294_IN_GGG(T255, s(T256), T257)
LOG294_IN_GGG(0, s(T274), T275) → U5_GGG(T274, T275, log2107_in_gg(T274, T275))
LOG294_IN_GGG(0, s(T274), T275) → LOG2107_IN_GG(T274, T275)
LOG2107_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T360)))))))))))))), T361) → U30_GG(T360, T361, log2144_in_ggg(T360, s(s(s(s(s(s(s(0))))))), T361))
LOG2107_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T360)))))))))))))), T361) → LOG2144_IN_GGG(T360, s(s(s(s(s(s(s(0))))))), T361)
LOG2144_IN_GGG(s(s(T380)), T381, T382) → U7_GGG(T380, T381, T382, log2144_in_ggg(T380, s(T381), T382))
LOG2144_IN_GGG(s(s(T380)), T381, T382) → LOG2144_IN_GGG(T380, s(T381), T382)
LOG2144_IN_GGG(0, s(T399), T400) → U8_GGG(T399, T400, log2157_in_gg(T399, T400))
LOG2144_IN_GGG(0, s(T399), T400) → LOG2157_IN_GG(T399, T400)
LOG2157_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T485)))))))))))))), T486) → U29_GG(T485, T486, log2194_in_ggg(T485, s(s(s(s(s(s(s(0))))))), T486))
LOG2157_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T485)))))))))))))), T486) → LOG2194_IN_GGG(T485, s(s(s(s(s(s(s(0))))))), T486)
LOG2194_IN_GGG(s(s(T505)), T506, T507) → U10_GGG(T505, T506, T507, log2194_in_ggg(T505, s(T506), T507))
LOG2194_IN_GGG(s(s(T505)), T506, T507) → LOG2194_IN_GGG(T505, s(T506), T507)
LOG2194_IN_GGG(0, s(T524), T525) → U11_GGG(T524, T525, log2207_in_gg(T524, T525))
LOG2194_IN_GGG(0, s(T524), T525) → LOG2207_IN_GG(T524, T525)
LOG2207_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T610)))))))))))))), T611) → U28_GG(T610, T611, log2244_in_ggg(T610, s(s(s(s(s(s(s(0))))))), T611))
LOG2207_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T610)))))))))))))), T611) → LOG2244_IN_GGG(T610, s(s(s(s(s(s(s(0))))))), T611)
LOG2244_IN_GGG(s(s(T630)), T631, T632) → U13_GGG(T630, T631, T632, log2244_in_ggg(T630, s(T631), T632))
LOG2244_IN_GGG(s(s(T630)), T631, T632) → LOG2244_IN_GGG(T630, s(T631), T632)
LOG2244_IN_GGG(0, s(T649), T650) → U14_GGG(T649, T650, log2257_in_gg(T649, T650))
LOG2244_IN_GGG(0, s(T649), T650) → LOG2257_IN_GG(T649, T650)
LOG2257_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T735)))))))))))))), T736) → U27_GG(T735, T736, log2294_in_ggg(T735, s(s(s(s(s(s(s(0))))))), T736))
LOG2257_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T735)))))))))))))), T736) → LOG2294_IN_GGG(T735, s(s(s(s(s(s(s(0))))))), T736)
LOG2294_IN_GGG(s(s(T755)), T756, T757) → U16_GGG(T755, T756, T757, log2294_in_ggg(T755, s(T756), T757))
LOG2294_IN_GGG(s(s(T755)), T756, T757) → LOG2294_IN_GGG(T755, s(T756), T757)
LOG2294_IN_GGG(0, s(T774), T775) → U17_GGG(T774, T775, log2307_in_gg(T774, T775))
LOG2294_IN_GGG(0, s(T774), T775) → LOG2307_IN_GG(T774, T775)
LOG2307_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T860)))))))))))))), T861) → U26_GG(T860, T861, log2344_in_ggg(T860, s(s(s(s(s(s(s(0))))))), T861))
LOG2307_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T860)))))))))))))), T861) → LOG2344_IN_GGG(T860, s(s(s(s(s(s(s(0))))))), T861)
LOG2344_IN_GGG(s(s(T880)), T881, T882) → U19_GGG(T880, T881, T882, log2344_in_ggg(T880, s(T881), T882))
LOG2344_IN_GGG(s(s(T880)), T881, T882) → LOG2344_IN_GGG(T880, s(T881), T882)
LOG2344_IN_GGG(0, s(T899), T900) → U20_GGG(T899, T900, log2359_in_ggg(T899, s(s(s(s(s(s(s(0))))))), T900))
LOG2344_IN_GGG(0, s(T899), T900) → LOG2359_IN_GGG(T899, s(s(s(s(s(s(s(0))))))), T900)
LOG2359_IN_GGG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1029)))))))))))))), T1030, T1031) → U25_GGG(T1029, T1030, T1031, log2395_in_gggg(T1029, s(s(s(s(s(s(s(0))))))), T1030, T1031))
LOG2359_IN_GGG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1029)))))))))))))), T1030, T1031) → LOG2395_IN_GGGG(T1029, s(s(s(s(s(s(s(0))))))), T1030, T1031)
LOG2395_IN_GGGG(s(s(T1056)), T1057, T1058, T1059) → U22_GGGG(T1056, T1057, T1058, T1059, log2395_in_gggg(T1056, s(T1057), T1058, T1059))
LOG2395_IN_GGGG(s(s(T1056)), T1057, T1058, T1059) → LOG2395_IN_GGGG(T1056, s(T1057), T1058, T1059)
LOG2395_IN_GGGG(0, s(T1081), T1082, T1083) → U23_GGGG(T1081, T1082, T1083, log2359_in_ggg(T1081, s(T1082), T1083))
LOG2395_IN_GGGG(0, s(T1081), T1082, T1083) → LOG2359_IN_GGG(T1081, s(T1082), T1083)
LOG2395_IN_GGGG(s(0), s(T1081), T1082, T1083) → U24_GGGG(T1081, T1082, T1083, log2359_in_ggg(T1081, s(T1082), T1083))
LOG2395_IN_GGGG(s(0), s(T1081), T1082, T1083) → LOG2359_IN_GGG(T1081, s(T1082), T1083)
LOG2344_IN_GGG(s(0), s(T899), T900) → U21_GGG(T899, T900, log2359_in_ggg(T899, s(s(s(s(s(s(s(0))))))), T900))
LOG2344_IN_GGG(s(0), s(T899), T900) → LOG2359_IN_GGG(T899, s(s(s(s(s(s(s(0))))))), T900)
LOG2294_IN_GGG(s(0), s(T774), T775) → U18_GGG(T774, T775, log2307_in_gg(T774, T775))
LOG2294_IN_GGG(s(0), s(T774), T775) → LOG2307_IN_GG(T774, T775)
LOG2244_IN_GGG(s(0), s(T649), T650) → U15_GGG(T649, T650, log2257_in_gg(T649, T650))
LOG2244_IN_GGG(s(0), s(T649), T650) → LOG2257_IN_GG(T649, T650)
LOG2194_IN_GGG(s(0), s(T524), T525) → U12_GGG(T524, T525, log2207_in_gg(T524, T525))
LOG2194_IN_GGG(s(0), s(T524), T525) → LOG2207_IN_GG(T524, T525)
LOG2144_IN_GGG(s(0), s(T399), T400) → U9_GGG(T399, T400, log2157_in_gg(T399, T400))
LOG2144_IN_GGG(s(0), s(T399), T400) → LOG2157_IN_GG(T399, T400)
LOG294_IN_GGG(s(0), s(T274), T275) → U6_GGG(T274, T275, log2107_in_gg(T274, T275))
LOG294_IN_GGG(s(0), s(T274), T275) → LOG2107_IN_GG(T274, T275)
LOG244_IN_AGG(s(0), s(T148), T149) → U3_AGG(T148, T149, log257_in_gg(T148, T149))
LOG244_IN_AGG(s(0), s(T148), T149) → LOG257_IN_GG(T148, T149)

R is empty.
The argument filtering Pi contains the following mapping:
log244_in_agg(x1, x2, x3)  =  log244_in_agg(x2, x3)
s(x1)  =  s(x1)
log257_in_gg(x1, x2)  =  log257_in_gg(x1, x2)
log294_in_ggg(x1, x2, x3)  =  log294_in_ggg(x1, x2, x3)
0  =  0
log2107_in_gg(x1, x2)  =  log2107_in_gg(x1, x2)
log2144_in_ggg(x1, x2, x3)  =  log2144_in_ggg(x1, x2, x3)
log2157_in_gg(x1, x2)  =  log2157_in_gg(x1, x2)
log2194_in_ggg(x1, x2, x3)  =  log2194_in_ggg(x1, x2, x3)
log2207_in_gg(x1, x2)  =  log2207_in_gg(x1, x2)
log2244_in_ggg(x1, x2, x3)  =  log2244_in_ggg(x1, x2, x3)
log2257_in_gg(x1, x2)  =  log2257_in_gg(x1, x2)
log2294_in_ggg(x1, x2, x3)  =  log2294_in_ggg(x1, x2, x3)
log2307_in_gg(x1, x2)  =  log2307_in_gg(x1, x2)
log2344_in_ggg(x1, x2, x3)  =  log2344_in_ggg(x1, x2, x3)
log2359_in_ggg(x1, x2, x3)  =  log2359_in_ggg(x1, x2, x3)
log2395_in_gggg(x1, x2, x3, x4)  =  log2395_in_gggg(x1, x2, x3, x4)
LOG21_IN_AG(x1, x2)  =  LOG21_IN_AG(x2)
U32_AG(x1, x2, x3)  =  U32_AG(x2, x3)
LOG244_IN_AGG(x1, x2, x3)  =  LOG244_IN_AGG(x2, x3)
U1_AGG(x1, x2, x3, x4)  =  U1_AGG(x2, x3, x4)
U2_AGG(x1, x2, x3)  =  U2_AGG(x1, x2, x3)
LOG257_IN_GG(x1, x2)  =  LOG257_IN_GG(x1, x2)
U31_GG(x1, x2, x3)  =  U31_GG(x1, x2, x3)
LOG294_IN_GGG(x1, x2, x3)  =  LOG294_IN_GGG(x1, x2, x3)
U4_GGG(x1, x2, x3, x4)  =  U4_GGG(x1, x2, x3, x4)
U5_GGG(x1, x2, x3)  =  U5_GGG(x1, x2, x3)
LOG2107_IN_GG(x1, x2)  =  LOG2107_IN_GG(x1, x2)
U30_GG(x1, x2, x3)  =  U30_GG(x1, x2, x3)
LOG2144_IN_GGG(x1, x2, x3)  =  LOG2144_IN_GGG(x1, x2, x3)
U7_GGG(x1, x2, x3, x4)  =  U7_GGG(x1, x2, x3, x4)
U8_GGG(x1, x2, x3)  =  U8_GGG(x1, x2, x3)
LOG2157_IN_GG(x1, x2)  =  LOG2157_IN_GG(x1, x2)
U29_GG(x1, x2, x3)  =  U29_GG(x1, x2, x3)
LOG2194_IN_GGG(x1, x2, x3)  =  LOG2194_IN_GGG(x1, x2, x3)
U10_GGG(x1, x2, x3, x4)  =  U10_GGG(x1, x2, x3, x4)
U11_GGG(x1, x2, x3)  =  U11_GGG(x1, x2, x3)
LOG2207_IN_GG(x1, x2)  =  LOG2207_IN_GG(x1, x2)
U28_GG(x1, x2, x3)  =  U28_GG(x1, x2, x3)
LOG2244_IN_GGG(x1, x2, x3)  =  LOG2244_IN_GGG(x1, x2, x3)
U13_GGG(x1, x2, x3, x4)  =  U13_GGG(x1, x2, x3, x4)
U14_GGG(x1, x2, x3)  =  U14_GGG(x1, x2, x3)
LOG2257_IN_GG(x1, x2)  =  LOG2257_IN_GG(x1, x2)
U27_GG(x1, x2, x3)  =  U27_GG(x1, x2, x3)
LOG2294_IN_GGG(x1, x2, x3)  =  LOG2294_IN_GGG(x1, x2, x3)
U16_GGG(x1, x2, x3, x4)  =  U16_GGG(x1, x2, x3, x4)
U17_GGG(x1, x2, x3)  =  U17_GGG(x1, x2, x3)
LOG2307_IN_GG(x1, x2)  =  LOG2307_IN_GG(x1, x2)
U26_GG(x1, x2, x3)  =  U26_GG(x1, x2, x3)
LOG2344_IN_GGG(x1, x2, x3)  =  LOG2344_IN_GGG(x1, x2, x3)
U19_GGG(x1, x2, x3, x4)  =  U19_GGG(x1, x2, x3, x4)
U20_GGG(x1, x2, x3)  =  U20_GGG(x1, x2, x3)
LOG2359_IN_GGG(x1, x2, x3)  =  LOG2359_IN_GGG(x1, x2, x3)
U25_GGG(x1, x2, x3, x4)  =  U25_GGG(x1, x2, x3, x4)
LOG2395_IN_GGGG(x1, x2, x3, x4)  =  LOG2395_IN_GGGG(x1, x2, x3, x4)
U22_GGGG(x1, x2, x3, x4, x5)  =  U22_GGGG(x1, x2, x3, x4, x5)
U23_GGGG(x1, x2, x3, x4)  =  U23_GGGG(x1, x2, x3, x4)
U24_GGGG(x1, x2, x3, x4)  =  U24_GGGG(x1, x2, x3, x4)
U21_GGG(x1, x2, x3)  =  U21_GGG(x1, x2, x3)
U18_GGG(x1, x2, x3)  =  U18_GGG(x1, x2, x3)
U15_GGG(x1, x2, x3)  =  U15_GGG(x1, x2, x3)
U12_GGG(x1, x2, x3)  =  U12_GGG(x1, x2, x3)
U9_GGG(x1, x2, x3)  =  U9_GGG(x1, x2, x3)
U6_GGG(x1, x2, x3)  =  U6_GGG(x1, x2, x3)
U3_AGG(x1, x2, x3)  =  U3_AGG(x1, x2, x3)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

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

LOG21_IN_AG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T109)))))))))))))))), T108) → U32_AG(T109, T108, log244_in_agg(T109, s(s(s(s(s(s(s(0))))))), T108))
LOG21_IN_AG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T109)))))))))))))))), T108) → LOG244_IN_AGG(T109, s(s(s(s(s(s(s(0))))))), T108)
LOG244_IN_AGG(s(s(T131)), T129, T130) → U1_AGG(T131, T129, T130, log244_in_agg(T131, s(T129), T130))
LOG244_IN_AGG(s(s(T131)), T129, T130) → LOG244_IN_AGG(T131, s(T129), T130)
LOG244_IN_AGG(0, s(T148), T149) → U2_AGG(T148, T149, log257_in_gg(T148, T149))
LOG244_IN_AGG(0, s(T148), T149) → LOG257_IN_GG(T148, T149)
LOG257_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T235)))))))))))))), T236) → U31_GG(T235, T236, log294_in_ggg(T235, s(s(s(s(s(s(s(0))))))), T236))
LOG257_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T235)))))))))))))), T236) → LOG294_IN_GGG(T235, s(s(s(s(s(s(s(0))))))), T236)
LOG294_IN_GGG(s(s(T255)), T256, T257) → U4_GGG(T255, T256, T257, log294_in_ggg(T255, s(T256), T257))
LOG294_IN_GGG(s(s(T255)), T256, T257) → LOG294_IN_GGG(T255, s(T256), T257)
LOG294_IN_GGG(0, s(T274), T275) → U5_GGG(T274, T275, log2107_in_gg(T274, T275))
LOG294_IN_GGG(0, s(T274), T275) → LOG2107_IN_GG(T274, T275)
LOG2107_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T360)))))))))))))), T361) → U30_GG(T360, T361, log2144_in_ggg(T360, s(s(s(s(s(s(s(0))))))), T361))
LOG2107_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T360)))))))))))))), T361) → LOG2144_IN_GGG(T360, s(s(s(s(s(s(s(0))))))), T361)
LOG2144_IN_GGG(s(s(T380)), T381, T382) → U7_GGG(T380, T381, T382, log2144_in_ggg(T380, s(T381), T382))
LOG2144_IN_GGG(s(s(T380)), T381, T382) → LOG2144_IN_GGG(T380, s(T381), T382)
LOG2144_IN_GGG(0, s(T399), T400) → U8_GGG(T399, T400, log2157_in_gg(T399, T400))
LOG2144_IN_GGG(0, s(T399), T400) → LOG2157_IN_GG(T399, T400)
LOG2157_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T485)))))))))))))), T486) → U29_GG(T485, T486, log2194_in_ggg(T485, s(s(s(s(s(s(s(0))))))), T486))
LOG2157_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T485)))))))))))))), T486) → LOG2194_IN_GGG(T485, s(s(s(s(s(s(s(0))))))), T486)
LOG2194_IN_GGG(s(s(T505)), T506, T507) → U10_GGG(T505, T506, T507, log2194_in_ggg(T505, s(T506), T507))
LOG2194_IN_GGG(s(s(T505)), T506, T507) → LOG2194_IN_GGG(T505, s(T506), T507)
LOG2194_IN_GGG(0, s(T524), T525) → U11_GGG(T524, T525, log2207_in_gg(T524, T525))
LOG2194_IN_GGG(0, s(T524), T525) → LOG2207_IN_GG(T524, T525)
LOG2207_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T610)))))))))))))), T611) → U28_GG(T610, T611, log2244_in_ggg(T610, s(s(s(s(s(s(s(0))))))), T611))
LOG2207_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T610)))))))))))))), T611) → LOG2244_IN_GGG(T610, s(s(s(s(s(s(s(0))))))), T611)
LOG2244_IN_GGG(s(s(T630)), T631, T632) → U13_GGG(T630, T631, T632, log2244_in_ggg(T630, s(T631), T632))
LOG2244_IN_GGG(s(s(T630)), T631, T632) → LOG2244_IN_GGG(T630, s(T631), T632)
LOG2244_IN_GGG(0, s(T649), T650) → U14_GGG(T649, T650, log2257_in_gg(T649, T650))
LOG2244_IN_GGG(0, s(T649), T650) → LOG2257_IN_GG(T649, T650)
LOG2257_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T735)))))))))))))), T736) → U27_GG(T735, T736, log2294_in_ggg(T735, s(s(s(s(s(s(s(0))))))), T736))
LOG2257_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T735)))))))))))))), T736) → LOG2294_IN_GGG(T735, s(s(s(s(s(s(s(0))))))), T736)
LOG2294_IN_GGG(s(s(T755)), T756, T757) → U16_GGG(T755, T756, T757, log2294_in_ggg(T755, s(T756), T757))
LOG2294_IN_GGG(s(s(T755)), T756, T757) → LOG2294_IN_GGG(T755, s(T756), T757)
LOG2294_IN_GGG(0, s(T774), T775) → U17_GGG(T774, T775, log2307_in_gg(T774, T775))
LOG2294_IN_GGG(0, s(T774), T775) → LOG2307_IN_GG(T774, T775)
LOG2307_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T860)))))))))))))), T861) → U26_GG(T860, T861, log2344_in_ggg(T860, s(s(s(s(s(s(s(0))))))), T861))
LOG2307_IN_GG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T860)))))))))))))), T861) → LOG2344_IN_GGG(T860, s(s(s(s(s(s(s(0))))))), T861)
LOG2344_IN_GGG(s(s(T880)), T881, T882) → U19_GGG(T880, T881, T882, log2344_in_ggg(T880, s(T881), T882))
LOG2344_IN_GGG(s(s(T880)), T881, T882) → LOG2344_IN_GGG(T880, s(T881), T882)
LOG2344_IN_GGG(0, s(T899), T900) → U20_GGG(T899, T900, log2359_in_ggg(T899, s(s(s(s(s(s(s(0))))))), T900))
LOG2344_IN_GGG(0, s(T899), T900) → LOG2359_IN_GGG(T899, s(s(s(s(s(s(s(0))))))), T900)
LOG2359_IN_GGG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1029)))))))))))))), T1030, T1031) → U25_GGG(T1029, T1030, T1031, log2395_in_gggg(T1029, s(s(s(s(s(s(s(0))))))), T1030, T1031))
LOG2359_IN_GGG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1029)))))))))))))), T1030, T1031) → LOG2395_IN_GGGG(T1029, s(s(s(s(s(s(s(0))))))), T1030, T1031)
LOG2395_IN_GGGG(s(s(T1056)), T1057, T1058, T1059) → U22_GGGG(T1056, T1057, T1058, T1059, log2395_in_gggg(T1056, s(T1057), T1058, T1059))
LOG2395_IN_GGGG(s(s(T1056)), T1057, T1058, T1059) → LOG2395_IN_GGGG(T1056, s(T1057), T1058, T1059)
LOG2395_IN_GGGG(0, s(T1081), T1082, T1083) → U23_GGGG(T1081, T1082, T1083, log2359_in_ggg(T1081, s(T1082), T1083))
LOG2395_IN_GGGG(0, s(T1081), T1082, T1083) → LOG2359_IN_GGG(T1081, s(T1082), T1083)
LOG2395_IN_GGGG(s(0), s(T1081), T1082, T1083) → U24_GGGG(T1081, T1082, T1083, log2359_in_ggg(T1081, s(T1082), T1083))
LOG2395_IN_GGGG(s(0), s(T1081), T1082, T1083) → LOG2359_IN_GGG(T1081, s(T1082), T1083)
LOG2344_IN_GGG(s(0), s(T899), T900) → U21_GGG(T899, T900, log2359_in_ggg(T899, s(s(s(s(s(s(s(0))))))), T900))
LOG2344_IN_GGG(s(0), s(T899), T900) → LOG2359_IN_GGG(T899, s(s(s(s(s(s(s(0))))))), T900)
LOG2294_IN_GGG(s(0), s(T774), T775) → U18_GGG(T774, T775, log2307_in_gg(T774, T775))
LOG2294_IN_GGG(s(0), s(T774), T775) → LOG2307_IN_GG(T774, T775)
LOG2244_IN_GGG(s(0), s(T649), T650) → U15_GGG(T649, T650, log2257_in_gg(T649, T650))
LOG2244_IN_GGG(s(0), s(T649), T650) → LOG2257_IN_GG(T649, T650)
LOG2194_IN_GGG(s(0), s(T524), T525) → U12_GGG(T524, T525, log2207_in_gg(T524, T525))
LOG2194_IN_GGG(s(0), s(T524), T525) → LOG2207_IN_GG(T524, T525)
LOG2144_IN_GGG(s(0), s(T399), T400) → U9_GGG(T399, T400, log2157_in_gg(T399, T400))
LOG2144_IN_GGG(s(0), s(T399), T400) → LOG2157_IN_GG(T399, T400)
LOG294_IN_GGG(s(0), s(T274), T275) → U6_GGG(T274, T275, log2107_in_gg(T274, T275))
LOG294_IN_GGG(s(0), s(T274), T275) → LOG2107_IN_GG(T274, T275)
LOG244_IN_AGG(s(0), s(T148), T149) → U3_AGG(T148, T149, log257_in_gg(T148, T149))
LOG244_IN_AGG(s(0), s(T148), T149) → LOG257_IN_GG(T148, T149)

R is empty.
The argument filtering Pi contains the following mapping:
log244_in_agg(x1, x2, x3)  =  log244_in_agg(x2, x3)
s(x1)  =  s(x1)
log257_in_gg(x1, x2)  =  log257_in_gg(x1, x2)
log294_in_ggg(x1, x2, x3)  =  log294_in_ggg(x1, x2, x3)
0  =  0
log2107_in_gg(x1, x2)  =  log2107_in_gg(x1, x2)
log2144_in_ggg(x1, x2, x3)  =  log2144_in_ggg(x1, x2, x3)
log2157_in_gg(x1, x2)  =  log2157_in_gg(x1, x2)
log2194_in_ggg(x1, x2, x3)  =  log2194_in_ggg(x1, x2, x3)
log2207_in_gg(x1, x2)  =  log2207_in_gg(x1, x2)
log2244_in_ggg(x1, x2, x3)  =  log2244_in_ggg(x1, x2, x3)
log2257_in_gg(x1, x2)  =  log2257_in_gg(x1, x2)
log2294_in_ggg(x1, x2, x3)  =  log2294_in_ggg(x1, x2, x3)
log2307_in_gg(x1, x2)  =  log2307_in_gg(x1, x2)
log2344_in_ggg(x1, x2, x3)  =  log2344_in_ggg(x1, x2, x3)
log2359_in_ggg(x1, x2, x3)  =  log2359_in_ggg(x1, x2, x3)
log2395_in_gggg(x1, x2, x3, x4)  =  log2395_in_gggg(x1, x2, x3, x4)
LOG21_IN_AG(x1, x2)  =  LOG21_IN_AG(x2)
U32_AG(x1, x2, x3)  =  U32_AG(x2, x3)
LOG244_IN_AGG(x1, x2, x3)  =  LOG244_IN_AGG(x2, x3)
U1_AGG(x1, x2, x3, x4)  =  U1_AGG(x2, x3, x4)
U2_AGG(x1, x2, x3)  =  U2_AGG(x1, x2, x3)
LOG257_IN_GG(x1, x2)  =  LOG257_IN_GG(x1, x2)
U31_GG(x1, x2, x3)  =  U31_GG(x1, x2, x3)
LOG294_IN_GGG(x1, x2, x3)  =  LOG294_IN_GGG(x1, x2, x3)
U4_GGG(x1, x2, x3, x4)  =  U4_GGG(x1, x2, x3, x4)
U5_GGG(x1, x2, x3)  =  U5_GGG(x1, x2, x3)
LOG2107_IN_GG(x1, x2)  =  LOG2107_IN_GG(x1, x2)
U30_GG(x1, x2, x3)  =  U30_GG(x1, x2, x3)
LOG2144_IN_GGG(x1, x2, x3)  =  LOG2144_IN_GGG(x1, x2, x3)
U7_GGG(x1, x2, x3, x4)  =  U7_GGG(x1, x2, x3, x4)
U8_GGG(x1, x2, x3)  =  U8_GGG(x1, x2, x3)
LOG2157_IN_GG(x1, x2)  =  LOG2157_IN_GG(x1, x2)
U29_GG(x1, x2, x3)  =  U29_GG(x1, x2, x3)
LOG2194_IN_GGG(x1, x2, x3)  =  LOG2194_IN_GGG(x1, x2, x3)
U10_GGG(x1, x2, x3, x4)  =  U10_GGG(x1, x2, x3, x4)
U11_GGG(x1, x2, x3)  =  U11_GGG(x1, x2, x3)
LOG2207_IN_GG(x1, x2)  =  LOG2207_IN_GG(x1, x2)
U28_GG(x1, x2, x3)  =  U28_GG(x1, x2, x3)
LOG2244_IN_GGG(x1, x2, x3)  =  LOG2244_IN_GGG(x1, x2, x3)
U13_GGG(x1, x2, x3, x4)  =  U13_GGG(x1, x2, x3, x4)
U14_GGG(x1, x2, x3)  =  U14_GGG(x1, x2, x3)
LOG2257_IN_GG(x1, x2)  =  LOG2257_IN_GG(x1, x2)
U27_GG(x1, x2, x3)  =  U27_GG(x1, x2, x3)
LOG2294_IN_GGG(x1, x2, x3)  =  LOG2294_IN_GGG(x1, x2, x3)
U16_GGG(x1, x2, x3, x4)  =  U16_GGG(x1, x2, x3, x4)
U17_GGG(x1, x2, x3)  =  U17_GGG(x1, x2, x3)
LOG2307_IN_GG(x1, x2)  =  LOG2307_IN_GG(x1, x2)
U26_GG(x1, x2, x3)  =  U26_GG(x1, x2, x3)
LOG2344_IN_GGG(x1, x2, x3)  =  LOG2344_IN_GGG(x1, x2, x3)
U19_GGG(x1, x2, x3, x4)  =  U19_GGG(x1, x2, x3, x4)
U20_GGG(x1, x2, x3)  =  U20_GGG(x1, x2, x3)
LOG2359_IN_GGG(x1, x2, x3)  =  LOG2359_IN_GGG(x1, x2, x3)
U25_GGG(x1, x2, x3, x4)  =  U25_GGG(x1, x2, x3, x4)
LOG2395_IN_GGGG(x1, x2, x3, x4)  =  LOG2395_IN_GGGG(x1, x2, x3, x4)
U22_GGGG(x1, x2, x3, x4, x5)  =  U22_GGGG(x1, x2, x3, x4, x5)
U23_GGGG(x1, x2, x3, x4)  =  U23_GGGG(x1, x2, x3, x4)
U24_GGGG(x1, x2, x3, x4)  =  U24_GGGG(x1, x2, x3, x4)
U21_GGG(x1, x2, x3)  =  U21_GGG(x1, x2, x3)
U18_GGG(x1, x2, x3)  =  U18_GGG(x1, x2, x3)
U15_GGG(x1, x2, x3)  =  U15_GGG(x1, x2, x3)
U12_GGG(x1, x2, x3)  =  U12_GGG(x1, x2, x3)
U9_GGG(x1, x2, x3)  =  U9_GGG(x1, x2, x3)
U6_GGG(x1, x2, x3)  =  U6_GGG(x1, x2, x3)
U3_AGG(x1, x2, x3)  =  U3_AGG(x1, x2, x3)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 8 SCCs with 53 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

LOG2359_IN_GGG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1029)))))))))))))), T1030, T1031) → LOG2395_IN_GGGG(T1029, s(s(s(s(s(s(s(0))))))), T1030, T1031)
LOG2395_IN_GGGG(s(s(T1056)), T1057, T1058, T1059) → LOG2395_IN_GGGG(T1056, s(T1057), T1058, T1059)
LOG2395_IN_GGGG(0, s(T1081), T1082, T1083) → LOG2359_IN_GGG(T1081, s(T1082), T1083)
LOG2395_IN_GGGG(s(0), s(T1081), T1082, T1083) → LOG2359_IN_GGG(T1081, s(T1082), T1083)

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

(10) PiDPToQDPProof (EQUIVALENT 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:

LOG2359_IN_GGG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1029)))))))))))))), T1030, T1031) → LOG2395_IN_GGGG(T1029, s(s(s(s(s(s(s(0))))))), T1030, T1031)
LOG2395_IN_GGGG(s(s(T1056)), T1057, T1058, T1059) → LOG2395_IN_GGGG(T1056, s(T1057), T1058, T1059)
LOG2395_IN_GGGG(0, s(T1081), T1082, T1083) → LOG2359_IN_GGG(T1081, s(T1082), T1083)
LOG2395_IN_GGGG(s(0), s(T1081), T1082, T1083) → LOG2359_IN_GGG(T1081, s(T1082), T1083)

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

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

LOG2359_IN_GGG(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1029)))))))))))))), T1030, T1031) → LOG2395_IN_GGGG(T1029, s(s(s(s(s(s(s(0))))))), T1030, T1031)
LOG2395_IN_GGGG(s(s(T1056)), T1057, T1058, T1059) → LOG2395_IN_GGGG(T1056, s(T1057), T1058, T1059)
LOG2395_IN_GGGG(0, s(T1081), T1082, T1083) → LOG2359_IN_GGG(T1081, s(T1082), T1083)
LOG2395_IN_GGGG(s(0), s(T1081), T1082, T1083) → LOG2359_IN_GGG(T1081, s(T1082), T1083)


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(LOG2359_IN_GGG(x1, x2, x3)) = x1 + x2 + x3   
POL(LOG2395_IN_GGGG(x1, x2, x3, x4)) = 1 + x1 + x2 + x3 + x4   
POL(s(x1)) = 1 + x1   

(13) Obligation:

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

(14) PisEmptyProof (EQUIVALENT transformation)

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

(15) YES

(16) Obligation:

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

LOG2344_IN_GGG(s(s(T880)), T881, T882) → LOG2344_IN_GGG(T880, s(T881), T882)

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

(17) PiDPToQDPProof (EQUIVALENT 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:

LOG2344_IN_GGG(s(s(T880)), T881, T882) → LOG2344_IN_GGG(T880, s(T881), T882)

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:

  • LOG2344_IN_GGG(s(s(T880)), T881, T882) → LOG2344_IN_GGG(T880, s(T881), T882)
    The graph contains the following edges 1 > 1, 3 >= 3

(20) YES

(21) Obligation:

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

LOG2294_IN_GGG(s(s(T755)), T756, T757) → LOG2294_IN_GGG(T755, s(T756), T757)

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

(22) PiDPToQDPProof (EQUIVALENT transformation)

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

(23) Obligation:

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

LOG2294_IN_GGG(s(s(T755)), T756, T757) → LOG2294_IN_GGG(T755, s(T756), T757)

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

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

  • LOG2294_IN_GGG(s(s(T755)), T756, T757) → LOG2294_IN_GGG(T755, s(T756), T757)
    The graph contains the following edges 1 > 1, 3 >= 3

(25) YES

(26) Obligation:

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

LOG2244_IN_GGG(s(s(T630)), T631, T632) → LOG2244_IN_GGG(T630, s(T631), T632)

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

(27) PiDPToQDPProof (EQUIVALENT transformation)

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

(28) Obligation:

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

LOG2244_IN_GGG(s(s(T630)), T631, T632) → LOG2244_IN_GGG(T630, s(T631), T632)

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

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

  • LOG2244_IN_GGG(s(s(T630)), T631, T632) → LOG2244_IN_GGG(T630, s(T631), T632)
    The graph contains the following edges 1 > 1, 3 >= 3

(30) YES

(31) Obligation:

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

LOG2194_IN_GGG(s(s(T505)), T506, T507) → LOG2194_IN_GGG(T505, s(T506), T507)

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

(32) PiDPToQDPProof (EQUIVALENT transformation)

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

(33) Obligation:

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

LOG2194_IN_GGG(s(s(T505)), T506, T507) → LOG2194_IN_GGG(T505, s(T506), T507)

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

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

  • LOG2194_IN_GGG(s(s(T505)), T506, T507) → LOG2194_IN_GGG(T505, s(T506), T507)
    The graph contains the following edges 1 > 1, 3 >= 3

(35) YES

(36) Obligation:

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

LOG2144_IN_GGG(s(s(T380)), T381, T382) → LOG2144_IN_GGG(T380, s(T381), T382)

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

(37) PiDPToQDPProof (EQUIVALENT transformation)

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

(38) Obligation:

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

LOG2144_IN_GGG(s(s(T380)), T381, T382) → LOG2144_IN_GGG(T380, s(T381), T382)

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

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

  • LOG2144_IN_GGG(s(s(T380)), T381, T382) → LOG2144_IN_GGG(T380, s(T381), T382)
    The graph contains the following edges 1 > 1, 3 >= 3

(40) YES

(41) Obligation:

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

LOG294_IN_GGG(s(s(T255)), T256, T257) → LOG294_IN_GGG(T255, s(T256), T257)

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

(42) PiDPToQDPProof (EQUIVALENT transformation)

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

(43) Obligation:

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

LOG294_IN_GGG(s(s(T255)), T256, T257) → LOG294_IN_GGG(T255, s(T256), T257)

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

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

  • LOG294_IN_GGG(s(s(T255)), T256, T257) → LOG294_IN_GGG(T255, s(T256), T257)
    The graph contains the following edges 1 > 1, 3 >= 3

(45) YES

(46) Obligation:

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

LOG244_IN_AGG(s(s(T131)), T129, T130) → LOG244_IN_AGG(T131, s(T129), T130)

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

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

(47) PiDPToQDPProof (SOUND transformation)

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

(48) Obligation:

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

LOG244_IN_AGG(T129, T130) → LOG244_IN_AGG(s(T129), T130)

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

(49) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule LOG244_IN_AGG(T129, T130) → LOG244_IN_AGG(s(T129), T130) we obtained the following new rules [LPAR04]:

LOG244_IN_AGG(s(z0), z1) → LOG244_IN_AGG(s(s(z0)), z1)

(50) Obligation:

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

LOG244_IN_AGG(s(z0), z1) → LOG244_IN_AGG(s(s(z0)), z1)

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

(51) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule LOG244_IN_AGG(s(z0), z1) → LOG244_IN_AGG(s(s(z0)), z1) we obtained the following new rules [LPAR04]:

LOG244_IN_AGG(s(s(z0)), z1) → LOG244_IN_AGG(s(s(s(z0))), z1)

(52) Obligation:

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

LOG244_IN_AGG(s(s(z0)), z1) → LOG244_IN_AGG(s(s(s(z0))), z1)

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

(53) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = LOG244_IN_AGG(s(s(z0)), z1) evaluates to t =LOG244_IN_AGG(s(s(s(z0))), z1)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [z0 / s(z0)]
  • Semiunifier: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from LOG244_IN_AGG(s(s(z0)), z1) to LOG244_IN_AGG(s(s(s(z0))), z1).



(54) NO