(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(g,a).
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph.
(2) Obligation:
Triples:
log244(s(s(T128)), T129, T131) :- log244(T128, s(T129), T131).
log244(0, s(T148), T150) :- log257(T148, T150).
log244(s(0), s(T148), T150) :- log257(T148, T150).
log294(s(s(T262)), T263, T265) :- log294(T262, s(T263), T265).
log294(0, s(T282), T284) :- log2107(T282, T284).
log294(s(0), s(T282), T284) :- log2107(T282, T284).
log2144(s(s(T396)), T397, T399) :- log2144(T396, s(T397), T399).
log2144(0, s(T416), T418) :- log2157(T416, T418).
log2144(s(0), s(T416), T418) :- log2157(T416, T418).
log2194(s(s(T530)), T531, T533) :- log2194(T530, s(T531), T533).
log2194(0, s(T550), T552) :- log2207(T550, T552).
log2194(s(0), s(T550), T552) :- log2207(T550, T552).
log2244(s(s(T664)), T665, T667) :- log2244(T664, s(T665), T667).
log2244(0, s(T684), T686) :- log2257(T684, T686).
log2244(s(0), s(T684), T686) :- log2257(T684, T686).
log2294(s(s(T798)), T799, T801) :- log2294(T798, s(T799), T801).
log2294(0, s(T818), T820) :- log2307(T818, T820).
log2294(s(0), s(T818), T820) :- log2307(T818, T820).
log2344(s(s(T932)), T933, T935) :- log2344(T932, s(T933), T935).
log2344(0, s(T952), T954) :- log2359(T952, s(s(s(s(s(s(s(0))))))), T954).
log2344(s(0), s(T952), T954) :- log2359(T952, s(s(s(s(s(s(s(0))))))), T954).
log2395(s(s(T1117)), T1118, T1119, T1121) :- log2395(T1117, s(T1118), T1119, T1121).
log2395(0, s(T1143), T1144, T1146) :- log2359(T1143, s(T1144), T1146).
log2395(s(0), s(T1143), T1144, T1146) :- log2359(T1143, s(T1144), T1146).
log2359(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1089)))))))))))))), T1090, T1092) :- log2395(T1089, s(s(s(s(s(s(s(0))))))), T1090, T1092).
log2359(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T1184, T1186) :- log2437(T1184, T1186).
log2359(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T1184, T1186) :- log2437(T1184, T1186).
log2359(s(s(s(s(s(s(s(s(s(s(0)))))))))), T1302, T1304) :- log2515(T1302, T1304).
log2359(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T1302, T1304) :- log2515(T1302, T1304).
log2359(s(s(s(s(s(s(s(s(0)))))))), T1418, T1420) :- log2585(T1418, T1420).
log2359(s(s(s(s(s(s(s(s(s(0))))))))), T1418, T1420) :- log2585(T1418, T1420).
log2359(s(s(s(s(s(s(0)))))), T1498, T1500) :- log2650(T1498, T1500).
log2359(s(s(s(s(s(s(s(0))))))), T1498, T1500) :- log2650(T1498, T1500).
log2359(s(s(s(s(0)))), T1574, T1576) :- log2705(T1574, T1576).
log2359(s(s(s(s(s(0))))), T1574, T1576) :- log2705(T1574, T1576).
log2359(s(s(0)), T1606, T1608) :- log2742(T1606, T1608).
log2359(s(s(s(0))), T1606, T1608) :- log2742(T1606, T1608).
log2437(T1241, T1243) :- log2454(T1241, T1243).
log2515(T1359, T1361) :- log2454(T1359, T1361).
log2585(T1456, T1458) :- log2598(T1456, T1458).
log2650(T1536, T1538) :- log2598(T1536, T1538).
log2307(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T911)))))))))))))), T913) :- log2344(T911, s(s(s(s(s(s(s(0))))))), T913).
log2307(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T1650) :- log2822(s(s(s(s(s(s(s(0))))))), T1650).
log2307(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T1650) :- log2822(s(s(s(s(s(s(s(0))))))), T1650).
log2307(s(s(s(s(s(s(s(s(s(s(0)))))))))), T1755) :- log2889(s(s(s(s(s(s(s(0))))))), T1755).
log2307(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T1755) :- log2889(s(s(s(s(s(s(s(0))))))), T1755).
log2307(s(s(s(s(s(s(s(s(0)))))))), T1861) :- log2960(s(s(s(s(s(s(s(0))))))), T1861).
log2307(s(s(s(s(s(s(s(s(s(0))))))))), T1861) :- log2960(s(s(s(s(s(s(s(0))))))), T1861).
log2307(s(s(s(s(s(s(0)))))), T1928) :- log21012(s(s(s(s(s(s(s(0))))))), T1928).
log2307(s(s(s(s(s(s(s(0))))))), T1928) :- log21012(s(s(s(s(s(s(s(0))))))), T1928).
log2307(s(s(s(s(0)))), T1994) :- log21068(s(s(s(s(s(s(s(0))))))), T1994).
log2307(s(s(s(s(s(0))))), T1994) :- log21068(s(s(s(s(s(s(s(0))))))), T1994).
log2307(s(s(0)), T2015) :- log21106(s(s(s(s(s(s(s(0))))))), T2015).
log2307(s(s(s(0))), T2015) :- log21106(s(s(s(s(s(s(s(0))))))), T2015).
log21183(T2082) :- log21068(s(s(s(s(s(s(s(0))))))), T2082).
log21249(T2141) :- log21068(s(s(s(s(s(s(s(0))))))), T2141).
log21319(T2189) :- log21106(s(s(s(s(s(s(s(0))))))), T2189).
log21370(T2229) :- log21106(s(s(s(s(s(s(s(0))))))), T2229).
log2257(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T777)))))))))))))), T779) :- log2294(T777, s(s(s(s(s(s(s(0))))))), T779).
log2257(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2050) :- log21183(T2050).
log2257(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2050) :- log21183(T2050).
log2257(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2109) :- log21249(T2109).
log2257(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2109) :- log21249(T2109).
log2257(s(s(s(s(s(s(s(s(0)))))))), T2168) :- log21319(T2168).
log2257(s(s(s(s(s(s(s(s(s(0))))))))), T2168) :- log21319(T2168).
log2257(s(s(s(s(s(s(0)))))), T2208) :- log21370(T2208).
log2257(s(s(s(s(s(s(s(0))))))), T2208) :- log21370(T2208).
log2257(s(s(s(s(0)))), T2246) :- log21425(T2246).
log2257(s(s(s(s(s(0))))), T2246) :- log21425(T2246).
log2257(s(s(0)), T2262) :- log21462(T2262).
log2257(s(s(s(0))), T2262) :- log21462(T2262).
log21540(T2324) :- log21425(T2324).
log21606(T2383) :- log21425(T2383).
log21676(T2431) :- log21462(T2431).
log21727(T2471) :- log21462(T2471).
log2207(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T643)))))))))))))), T645) :- log2244(T643, s(s(s(s(s(s(s(0))))))), T645).
log2207(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2292) :- log21540(T2292).
log2207(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2292) :- log21540(T2292).
log2207(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2351) :- log21606(T2351).
log2207(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2351) :- log21606(T2351).
log2207(s(s(s(s(s(s(s(s(0)))))))), T2410) :- log21676(T2410).
log2207(s(s(s(s(s(s(s(s(s(0))))))))), T2410) :- log21676(T2410).
log2207(s(s(s(s(s(s(0)))))), T2450) :- log21727(T2450).
log2207(s(s(s(s(s(s(s(0))))))), T2450) :- log21727(T2450).
log2207(s(s(s(s(0)))), T2488) :- log21782(T2488).
log2207(s(s(s(s(s(0))))), T2488) :- log21782(T2488).
log2207(s(s(0)), T2504) :- log21819(T2504).
log2207(s(s(s(0))), T2504) :- log21819(T2504).
log21897(T2566) :- log21782(T2566).
log21963(T2625) :- log21782(T2625).
log22033(T2673) :- log21819(T2673).
log22084(T2713) :- log21819(T2713).
log2157(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T509)))))))))))))), T511) :- log2194(T509, s(s(s(s(s(s(s(0))))))), T511).
log2157(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2534) :- log21897(T2534).
log2157(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2534) :- log21897(T2534).
log2157(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2593) :- log21963(T2593).
log2157(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2593) :- log21963(T2593).
log2157(s(s(s(s(s(s(s(s(0)))))))), T2652) :- log22033(T2652).
log2157(s(s(s(s(s(s(s(s(s(0))))))))), T2652) :- log22033(T2652).
log2157(s(s(s(s(s(s(0)))))), T2692) :- log22084(T2692).
log2157(s(s(s(s(s(s(s(0))))))), T2692) :- log22084(T2692).
log2157(s(s(s(s(0)))), T2730) :- log22139(T2730).
log2157(s(s(s(s(s(0))))), T2730) :- log22139(T2730).
log2157(s(s(0)), T2746) :- log22176(T2746).
log2157(s(s(s(0))), T2746) :- log22176(T2746).
log22254(T2808) :- log22139(T2808).
log22320(T2867) :- log22139(T2867).
log22390(T2915) :- log22176(T2915).
log22441(T2955) :- log22176(T2955).
log2107(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T375)))))))))))))), T377) :- log2144(T375, s(s(s(s(s(s(s(0))))))), T377).
log2107(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2776) :- log22254(T2776).
log2107(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2776) :- log22254(T2776).
log2107(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2835) :- log22320(T2835).
log2107(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2835) :- log22320(T2835).
log2107(s(s(s(s(s(s(s(s(0)))))))), T2894) :- log22390(T2894).
log2107(s(s(s(s(s(s(s(s(s(0))))))))), T2894) :- log22390(T2894).
log2107(s(s(s(s(s(s(0)))))), T2934) :- log22441(T2934).
log2107(s(s(s(s(s(s(s(0))))))), T2934) :- log22441(T2934).
log2107(s(s(s(s(0)))), T2972) :- log22496(T2972).
log2107(s(s(s(s(s(0))))), T2972) :- log22496(T2972).
log2107(s(s(0)), T2988) :- log22533(T2988).
log2107(s(s(s(0))), T2988) :- log22533(T2988).
log22611(T3050) :- log22496(T3050).
log22677(T3109) :- log22496(T3109).
log22747(T3157) :- log22533(T3157).
log22798(T3197) :- log22533(T3197).
log257(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T241)))))))))))))), T243) :- log294(T241, s(s(s(s(s(s(s(0))))))), T243).
log257(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T3018) :- log22611(T3018).
log257(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T3018) :- log22611(T3018).
log257(s(s(s(s(s(s(s(s(s(s(0)))))))))), T3077) :- log22677(T3077).
log257(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T3077) :- log22677(T3077).
log257(s(s(s(s(s(s(s(s(0)))))))), T3136) :- log22747(T3136).
log257(s(s(s(s(s(s(s(s(s(0))))))))), T3136) :- log22747(T3136).
log257(s(s(s(s(s(s(0)))))), T3176) :- log22798(T3176).
log257(s(s(s(s(s(s(s(0))))))), T3176) :- log22798(T3176).
log257(s(s(s(s(0)))), T3214) :- log22853(T3214).
log257(s(s(s(s(s(0))))), T3214) :- log22853(T3214).
log257(s(s(0)), T3230) :- log22890(T3230).
log257(s(s(s(0))), T3230) :- log22890(T3230).
log22968(T3292) :- log22853(T3292).
log23034(T3351) :- log22853(T3351).
log23104(T3399) :- log22890(T3399).
log23155(T3439) :- log22890(T3439).
log2822(T1706, T1708) :- log2705(T1706, T1708).
log2889(T1811, T1813) :- log2705(T1811, T1813).
log2960(T1898, T1900) :- log2742(T1898, T1900).
log21012(T1965, T1967) :- log2742(T1965, T1967).
log21(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T107)))))))))))))))), T109) :- log244(T107, s(s(s(s(s(s(s(0))))))), T109).
log21(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))), T3260) :- log22968(T3260).
log21(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))), T3260) :- log22968(T3260).
log21(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T3319) :- log23034(T3319).
log21(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T3319) :- log23034(T3319).
log21(s(s(s(s(s(s(s(s(s(s(0)))))))))), T3378) :- log23104(T3378).
log21(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T3378) :- log23104(T3378).
log21(s(s(s(s(s(s(s(s(0)))))))), T3418) :- log23155(T3418).
log21(s(s(s(s(s(s(s(s(s(0))))))))), T3418) :- log23155(T3418).
log21(s(s(s(s(s(s(0)))))), T3456) :- log23210(T3456).
log21(s(s(s(s(s(s(s(0))))))), T3456) :- log23210(T3456).
log21(s(s(s(s(0)))), T3472) :- log23247(T3472).
log21(s(s(s(s(s(0))))), T3472) :- log23247(T3472).
Clauses:
log2c44(s(s(T128)), T129, T131) :- log2c44(T128, s(T129), T131).
log2c44(0, s(T148), T150) :- log2c57(T148, T150).
log2c44(s(0), s(T148), T150) :- log2c57(T148, T150).
log2c44(0, 0, s(0)).
log2c44(s(0), 0, s(0)).
log2c94(s(s(T262)), T263, T265) :- log2c94(T262, s(T263), T265).
log2c94(0, s(T282), T284) :- log2c107(T282, T284).
log2c94(s(0), s(T282), T284) :- log2c107(T282, T284).
log2c94(0, 0, s(s(0))).
log2c94(s(0), 0, s(s(0))).
log2c144(s(s(T396)), T397, T399) :- log2c144(T396, s(T397), T399).
log2c144(0, s(T416), T418) :- log2c157(T416, T418).
log2c144(s(0), s(T416), T418) :- log2c157(T416, T418).
log2c144(0, 0, s(s(s(0)))).
log2c144(s(0), 0, s(s(s(0)))).
log2c194(s(s(T530)), T531, T533) :- log2c194(T530, s(T531), T533).
log2c194(0, s(T550), T552) :- log2c207(T550, T552).
log2c194(s(0), s(T550), T552) :- log2c207(T550, T552).
log2c194(0, 0, s(s(s(s(0))))).
log2c194(s(0), 0, s(s(s(s(0))))).
log2c244(s(s(T664)), T665, T667) :- log2c244(T664, s(T665), T667).
log2c244(0, s(T684), T686) :- log2c257(T684, T686).
log2c244(s(0), s(T684), T686) :- log2c257(T684, T686).
log2c244(0, 0, s(s(s(s(s(0)))))).
log2c244(s(0), 0, s(s(s(s(s(0)))))).
log2c294(s(s(T798)), T799, T801) :- log2c294(T798, s(T799), T801).
log2c294(0, s(T818), T820) :- log2c307(T818, T820).
log2c294(s(0), s(T818), T820) :- log2c307(T818, T820).
log2c294(0, 0, s(s(s(s(s(s(0))))))).
log2c294(s(0), 0, s(s(s(s(s(s(0))))))).
log2c344(s(s(T932)), T933, T935) :- log2c344(T932, s(T933), T935).
log2c344(0, s(T952), T954) :- log2c359(T952, s(s(s(s(s(s(s(0))))))), T954).
log2c344(s(0), s(T952), T954) :- log2c359(T952, s(s(s(s(s(s(s(0))))))), T954).
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(T1117)), T1118, T1119, T1121) :- log2c395(T1117, s(T1118), T1119, T1121).
log2c395(0, s(T1143), T1144, T1146) :- log2c359(T1143, s(T1144), T1146).
log2c395(s(0), s(T1143), T1144, T1146) :- log2c359(T1143, s(T1144), T1146).
log2c395(0, 0, T1164, s(T1164)).
log2c395(s(0), 0, T1164, s(T1164)).
log2c359(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1089)))))))))))))), T1090, T1092) :- log2c395(T1089, s(s(s(s(s(s(s(0))))))), T1090, T1092).
log2c359(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T1184, T1186) :- log2c437(T1184, T1186).
log2c359(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T1184, T1186) :- log2c437(T1184, T1186).
log2c359(s(s(s(s(s(s(s(s(s(s(0)))))))))), T1302, T1304) :- log2c515(T1302, T1304).
log2c359(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T1302, T1304) :- log2c515(T1302, T1304).
log2c359(s(s(s(s(s(s(s(s(0)))))))), T1418, T1420) :- log2c585(T1418, T1420).
log2c359(s(s(s(s(s(s(s(s(s(0))))))))), T1418, T1420) :- log2c585(T1418, T1420).
log2c359(s(s(s(s(s(s(0)))))), T1498, T1500) :- log2c650(T1498, T1500).
log2c359(s(s(s(s(s(s(s(0))))))), T1498, T1500) :- log2c650(T1498, T1500).
log2c359(s(s(s(s(0)))), T1574, T1576) :- log2c705(T1574, T1576).
log2c359(s(s(s(s(s(0))))), T1574, T1576) :- log2c705(T1574, T1576).
log2c359(s(s(0)), T1606, T1608) :- log2c742(T1606, T1608).
log2c359(s(s(s(0))), T1606, T1608) :- log2c742(T1606, T1608).
log2c359(0, T1627, s(T1627)).
log2c359(s(0), T1627, s(T1627)).
log2c437(T1241, T1243) :- log2c454(T1241, T1243).
log2c454(T1249, s(s(s(T1249)))).
log2c515(T1359, T1361) :- log2c454(T1359, T1361).
log2c585(T1456, T1458) :- log2c598(T1456, T1458).
log2c598(T1464, s(s(s(T1464)))).
log2c650(T1536, T1538) :- log2c598(T1536, T1538).
log2c705(T1581, s(s(T1581))).
log2c742(T1613, s(s(T1613))).
log2c307(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T911)))))))))))))), T913) :- log2c344(T911, s(s(s(s(s(s(s(0))))))), T913).
log2c307(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T1650) :- log2c822(s(s(s(s(s(s(s(0))))))), T1650).
log2c307(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T1650) :- log2c822(s(s(s(s(s(s(s(0))))))), T1650).
log2c307(s(s(s(s(s(s(s(s(s(s(0)))))))))), T1755) :- log2c889(s(s(s(s(s(s(s(0))))))), T1755).
log2c307(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T1755) :- log2c889(s(s(s(s(s(s(s(0))))))), T1755).
log2c307(s(s(s(s(s(s(s(s(0)))))))), T1861) :- log2c960(s(s(s(s(s(s(s(0))))))), T1861).
log2c307(s(s(s(s(s(s(s(s(s(0))))))))), T1861) :- log2c960(s(s(s(s(s(s(s(0))))))), T1861).
log2c307(s(s(s(s(s(s(0)))))), T1928) :- log2c1012(s(s(s(s(s(s(s(0))))))), T1928).
log2c307(s(s(s(s(s(s(s(0))))))), T1928) :- log2c1012(s(s(s(s(s(s(s(0))))))), T1928).
log2c307(s(s(s(s(0)))), T1994) :- log2c1068(s(s(s(s(s(s(s(0))))))), T1994).
log2c307(s(s(s(s(s(0))))), T1994) :- log2c1068(s(s(s(s(s(s(s(0))))))), T1994).
log2c307(s(s(0)), T2015) :- log2c1106(s(s(s(s(s(s(s(0))))))), T2015).
log2c307(s(s(s(0))), T2015) :- log2c1106(s(s(s(s(s(s(s(0))))))), T2015).
log2c307(0, s(s(s(s(s(s(s(0)))))))).
log2c307(s(0), s(s(s(s(s(s(s(0)))))))).
log2c1183(T2082) :- log2c1068(s(s(s(s(s(s(s(0))))))), T2082).
log2c1249(T2141) :- log2c1068(s(s(s(s(s(s(s(0))))))), T2141).
log2c1319(T2189) :- log2c1106(s(s(s(s(s(s(s(0))))))), T2189).
log2c1370(T2229) :- log2c1106(s(s(s(s(s(s(s(0))))))), T2229).
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(T777)))))))))))))), T779) :- log2c294(T777, s(s(s(s(s(s(s(0))))))), T779).
log2c257(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2050) :- log2c1183(T2050).
log2c257(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2050) :- log2c1183(T2050).
log2c257(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2109) :- log2c1249(T2109).
log2c257(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2109) :- log2c1249(T2109).
log2c257(s(s(s(s(s(s(s(s(0)))))))), T2168) :- log2c1319(T2168).
log2c257(s(s(s(s(s(s(s(s(s(0))))))))), T2168) :- log2c1319(T2168).
log2c257(s(s(s(s(s(s(0)))))), T2208) :- log2c1370(T2208).
log2c257(s(s(s(s(s(s(s(0))))))), T2208) :- log2c1370(T2208).
log2c257(s(s(s(s(0)))), T2246) :- log2c1425(T2246).
log2c257(s(s(s(s(s(0))))), T2246) :- log2c1425(T2246).
log2c257(s(s(0)), T2262) :- log2c1462(T2262).
log2c257(s(s(s(0))), T2262) :- log2c1462(T2262).
log2c257(0, s(s(s(s(s(s(0))))))).
log2c257(s(0), s(s(s(s(s(s(0))))))).
log2c1540(T2324) :- log2c1425(T2324).
log2c1606(T2383) :- log2c1425(T2383).
log2c1676(T2431) :- log2c1462(T2431).
log2c1727(T2471) :- log2c1462(T2471).
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(T643)))))))))))))), T645) :- log2c244(T643, s(s(s(s(s(s(s(0))))))), T645).
log2c207(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2292) :- log2c1540(T2292).
log2c207(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2292) :- log2c1540(T2292).
log2c207(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2351) :- log2c1606(T2351).
log2c207(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2351) :- log2c1606(T2351).
log2c207(s(s(s(s(s(s(s(s(0)))))))), T2410) :- log2c1676(T2410).
log2c207(s(s(s(s(s(s(s(s(s(0))))))))), T2410) :- log2c1676(T2410).
log2c207(s(s(s(s(s(s(0)))))), T2450) :- log2c1727(T2450).
log2c207(s(s(s(s(s(s(s(0))))))), T2450) :- log2c1727(T2450).
log2c207(s(s(s(s(0)))), T2488) :- log2c1782(T2488).
log2c207(s(s(s(s(s(0))))), T2488) :- log2c1782(T2488).
log2c207(s(s(0)), T2504) :- log2c1819(T2504).
log2c207(s(s(s(0))), T2504) :- log2c1819(T2504).
log2c207(0, s(s(s(s(s(0)))))).
log2c207(s(0), s(s(s(s(s(0)))))).
log2c1897(T2566) :- log2c1782(T2566).
log2c1963(T2625) :- log2c1782(T2625).
log2c2033(T2673) :- log2c1819(T2673).
log2c2084(T2713) :- log2c1819(T2713).
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(T509)))))))))))))), T511) :- log2c194(T509, s(s(s(s(s(s(s(0))))))), T511).
log2c157(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2534) :- log2c1897(T2534).
log2c157(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2534) :- log2c1897(T2534).
log2c157(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2593) :- log2c1963(T2593).
log2c157(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2593) :- log2c1963(T2593).
log2c157(s(s(s(s(s(s(s(s(0)))))))), T2652) :- log2c2033(T2652).
log2c157(s(s(s(s(s(s(s(s(s(0))))))))), T2652) :- log2c2033(T2652).
log2c157(s(s(s(s(s(s(0)))))), T2692) :- log2c2084(T2692).
log2c157(s(s(s(s(s(s(s(0))))))), T2692) :- log2c2084(T2692).
log2c157(s(s(s(s(0)))), T2730) :- log2c2139(T2730).
log2c157(s(s(s(s(s(0))))), T2730) :- log2c2139(T2730).
log2c157(s(s(0)), T2746) :- log2c2176(T2746).
log2c157(s(s(s(0))), T2746) :- log2c2176(T2746).
log2c157(0, s(s(s(s(0))))).
log2c157(s(0), s(s(s(s(0))))).
log2c2254(T2808) :- log2c2139(T2808).
log2c2320(T2867) :- log2c2139(T2867).
log2c2390(T2915) :- log2c2176(T2915).
log2c2441(T2955) :- log2c2176(T2955).
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(T375)))))))))))))), T377) :- log2c144(T375, s(s(s(s(s(s(s(0))))))), T377).
log2c107(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2776) :- log2c2254(T2776).
log2c107(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2776) :- log2c2254(T2776).
log2c107(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2835) :- log2c2320(T2835).
log2c107(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2835) :- log2c2320(T2835).
log2c107(s(s(s(s(s(s(s(s(0)))))))), T2894) :- log2c2390(T2894).
log2c107(s(s(s(s(s(s(s(s(s(0))))))))), T2894) :- log2c2390(T2894).
log2c107(s(s(s(s(s(s(0)))))), T2934) :- log2c2441(T2934).
log2c107(s(s(s(s(s(s(s(0))))))), T2934) :- log2c2441(T2934).
log2c107(s(s(s(s(0)))), T2972) :- log2c2496(T2972).
log2c107(s(s(s(s(s(0))))), T2972) :- log2c2496(T2972).
log2c107(s(s(0)), T2988) :- log2c2533(T2988).
log2c107(s(s(s(0))), T2988) :- log2c2533(T2988).
log2c107(0, s(s(s(0)))).
log2c107(s(0), s(s(s(0)))).
log2c2611(T3050) :- log2c2496(T3050).
log2c2677(T3109) :- log2c2496(T3109).
log2c2747(T3157) :- log2c2533(T3157).
log2c2798(T3197) :- log2c2533(T3197).
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(T241)))))))))))))), T243) :- log2c94(T241, s(s(s(s(s(s(s(0))))))), T243).
log2c57(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T3018) :- log2c2611(T3018).
log2c57(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T3018) :- log2c2611(T3018).
log2c57(s(s(s(s(s(s(s(s(s(s(0)))))))))), T3077) :- log2c2677(T3077).
log2c57(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T3077) :- log2c2677(T3077).
log2c57(s(s(s(s(s(s(s(s(0)))))))), T3136) :- log2c2747(T3136).
log2c57(s(s(s(s(s(s(s(s(s(0))))))))), T3136) :- log2c2747(T3136).
log2c57(s(s(s(s(s(s(0)))))), T3176) :- log2c2798(T3176).
log2c57(s(s(s(s(s(s(s(0))))))), T3176) :- log2c2798(T3176).
log2c57(s(s(s(s(0)))), T3214) :- log2c2853(T3214).
log2c57(s(s(s(s(s(0))))), T3214) :- log2c2853(T3214).
log2c57(s(s(0)), T3230) :- log2c2890(T3230).
log2c57(s(s(s(0))), T3230) :- log2c2890(T3230).
log2c57(0, s(s(0))).
log2c57(s(0), s(s(0))).
log2c2968(T3292) :- log2c2853(T3292).
log2c3034(T3351) :- log2c2853(T3351).
log2c3104(T3399) :- log2c2890(T3399).
log2c3155(T3439) :- log2c2890(T3439).
log2c3210(s(s(0))).
log2c3247(s(s(0))).
log2c822(T1706, T1708) :- log2c705(T1706, T1708).
log2c889(T1811, T1813) :- log2c705(T1811, T1813).
log2c960(T1898, T1900) :- log2c742(T1898, T1900).
log2c1012(T1965, T1967) :- log2c742(T1965, T1967).
log2c1068(T1999, s(T1999)).
log2c1106(T2020, s(T2020)).
Afs:
log21(x1, x2) = log21(x1)
(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)
Deleted triples and predicates having undefined goals [UNKNOWN].
(4) Obligation:
Triples:
log244(s(s(T128)), T129, T131) :- log244(T128, s(T129), T131).
log244(0, s(T148), T150) :- log257(T148, T150).
log244(s(0), s(T148), T150) :- log257(T148, T150).
log294(s(s(T262)), T263, T265) :- log294(T262, s(T263), T265).
log294(0, s(T282), T284) :- log2107(T282, T284).
log294(s(0), s(T282), T284) :- log2107(T282, T284).
log2144(s(s(T396)), T397, T399) :- log2144(T396, s(T397), T399).
log2144(0, s(T416), T418) :- log2157(T416, T418).
log2144(s(0), s(T416), T418) :- log2157(T416, T418).
log2194(s(s(T530)), T531, T533) :- log2194(T530, s(T531), T533).
log2194(0, s(T550), T552) :- log2207(T550, T552).
log2194(s(0), s(T550), T552) :- log2207(T550, T552).
log2244(s(s(T664)), T665, T667) :- log2244(T664, s(T665), T667).
log2244(0, s(T684), T686) :- log2257(T684, T686).
log2244(s(0), s(T684), T686) :- log2257(T684, T686).
log2294(s(s(T798)), T799, T801) :- log2294(T798, s(T799), T801).
log2294(0, s(T818), T820) :- log2307(T818, T820).
log2294(s(0), s(T818), T820) :- log2307(T818, T820).
log2344(s(s(T932)), T933, T935) :- log2344(T932, s(T933), T935).
log2344(0, s(T952), T954) :- log2359(T952, s(s(s(s(s(s(s(0))))))), T954).
log2344(s(0), s(T952), T954) :- log2359(T952, s(s(s(s(s(s(s(0))))))), T954).
log2395(s(s(T1117)), T1118, T1119, T1121) :- log2395(T1117, s(T1118), T1119, T1121).
log2395(0, s(T1143), T1144, T1146) :- log2359(T1143, s(T1144), T1146).
log2395(s(0), s(T1143), T1144, T1146) :- log2359(T1143, s(T1144), T1146).
log2359(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1089)))))))))))))), T1090, T1092) :- log2395(T1089, s(s(s(s(s(s(s(0))))))), T1090, T1092).
log2307(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T911)))))))))))))), T913) :- log2344(T911, s(s(s(s(s(s(s(0))))))), T913).
log2257(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T777)))))))))))))), T779) :- log2294(T777, s(s(s(s(s(s(s(0))))))), T779).
log2207(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T643)))))))))))))), T645) :- log2244(T643, s(s(s(s(s(s(s(0))))))), T645).
log2157(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T509)))))))))))))), T511) :- log2194(T509, s(s(s(s(s(s(s(0))))))), T511).
log2107(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T375)))))))))))))), T377) :- log2144(T375, s(s(s(s(s(s(s(0))))))), T377).
log257(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T241)))))))))))))), T243) :- log294(T241, s(s(s(s(s(s(s(0))))))), T243).
log21(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T107)))))))))))))))), T109) :- log244(T107, s(s(s(s(s(s(s(0))))))), T109).
Clauses:
log2c44(s(s(T128)), T129, T131) :- log2c44(T128, s(T129), T131).
log2c44(0, s(T148), T150) :- log2c57(T148, T150).
log2c44(s(0), s(T148), T150) :- log2c57(T148, T150).
log2c44(0, 0, s(0)).
log2c44(s(0), 0, s(0)).
log2c94(s(s(T262)), T263, T265) :- log2c94(T262, s(T263), T265).
log2c94(0, s(T282), T284) :- log2c107(T282, T284).
log2c94(s(0), s(T282), T284) :- log2c107(T282, T284).
log2c94(0, 0, s(s(0))).
log2c94(s(0), 0, s(s(0))).
log2c144(s(s(T396)), T397, T399) :- log2c144(T396, s(T397), T399).
log2c144(0, s(T416), T418) :- log2c157(T416, T418).
log2c144(s(0), s(T416), T418) :- log2c157(T416, T418).
log2c144(0, 0, s(s(s(0)))).
log2c144(s(0), 0, s(s(s(0)))).
log2c194(s(s(T530)), T531, T533) :- log2c194(T530, s(T531), T533).
log2c194(0, s(T550), T552) :- log2c207(T550, T552).
log2c194(s(0), s(T550), T552) :- log2c207(T550, T552).
log2c194(0, 0, s(s(s(s(0))))).
log2c194(s(0), 0, s(s(s(s(0))))).
log2c244(s(s(T664)), T665, T667) :- log2c244(T664, s(T665), T667).
log2c244(0, s(T684), T686) :- log2c257(T684, T686).
log2c244(s(0), s(T684), T686) :- log2c257(T684, T686).
log2c244(0, 0, s(s(s(s(s(0)))))).
log2c244(s(0), 0, s(s(s(s(s(0)))))).
log2c294(s(s(T798)), T799, T801) :- log2c294(T798, s(T799), T801).
log2c294(0, s(T818), T820) :- log2c307(T818, T820).
log2c294(s(0), s(T818), T820) :- log2c307(T818, T820).
log2c294(0, 0, s(s(s(s(s(s(0))))))).
log2c294(s(0), 0, s(s(s(s(s(s(0))))))).
log2c344(s(s(T932)), T933, T935) :- log2c344(T932, s(T933), T935).
log2c344(0, s(T952), T954) :- log2c359(T952, s(s(s(s(s(s(s(0))))))), T954).
log2c344(s(0), s(T952), T954) :- log2c359(T952, s(s(s(s(s(s(s(0))))))), T954).
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(T1117)), T1118, T1119, T1121) :- log2c395(T1117, s(T1118), T1119, T1121).
log2c395(0, s(T1143), T1144, T1146) :- log2c359(T1143, s(T1144), T1146).
log2c395(s(0), s(T1143), T1144, T1146) :- log2c359(T1143, s(T1144), T1146).
log2c395(0, 0, T1164, s(T1164)).
log2c395(s(0), 0, T1164, s(T1164)).
log2c359(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1089)))))))))))))), T1090, T1092) :- log2c395(T1089, s(s(s(s(s(s(s(0))))))), T1090, T1092).
log2c359(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T1184, T1186) :- log2c437(T1184, T1186).
log2c359(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T1184, T1186) :- log2c437(T1184, T1186).
log2c359(s(s(s(s(s(s(s(s(s(s(0)))))))))), T1302, T1304) :- log2c515(T1302, T1304).
log2c359(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T1302, T1304) :- log2c515(T1302, T1304).
log2c359(s(s(s(s(s(s(s(s(0)))))))), T1418, T1420) :- log2c585(T1418, T1420).
log2c359(s(s(s(s(s(s(s(s(s(0))))))))), T1418, T1420) :- log2c585(T1418, T1420).
log2c359(s(s(s(s(s(s(0)))))), T1498, T1500) :- log2c650(T1498, T1500).
log2c359(s(s(s(s(s(s(s(0))))))), T1498, T1500) :- log2c650(T1498, T1500).
log2c359(s(s(s(s(0)))), T1574, T1576) :- log2c705(T1574, T1576).
log2c359(s(s(s(s(s(0))))), T1574, T1576) :- log2c705(T1574, T1576).
log2c359(s(s(0)), T1606, T1608) :- log2c742(T1606, T1608).
log2c359(s(s(s(0))), T1606, T1608) :- log2c742(T1606, T1608).
log2c359(0, T1627, s(T1627)).
log2c359(s(0), T1627, s(T1627)).
log2c437(T1241, T1243) :- log2c454(T1241, T1243).
log2c454(T1249, s(s(s(T1249)))).
log2c515(T1359, T1361) :- log2c454(T1359, T1361).
log2c585(T1456, T1458) :- log2c598(T1456, T1458).
log2c598(T1464, s(s(s(T1464)))).
log2c650(T1536, T1538) :- log2c598(T1536, T1538).
log2c705(T1581, s(s(T1581))).
log2c742(T1613, s(s(T1613))).
log2c307(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T911)))))))))))))), T913) :- log2c344(T911, s(s(s(s(s(s(s(0))))))), T913).
log2c307(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T1650) :- log2c822(s(s(s(s(s(s(s(0))))))), T1650).
log2c307(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T1650) :- log2c822(s(s(s(s(s(s(s(0))))))), T1650).
log2c307(s(s(s(s(s(s(s(s(s(s(0)))))))))), T1755) :- log2c889(s(s(s(s(s(s(s(0))))))), T1755).
log2c307(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T1755) :- log2c889(s(s(s(s(s(s(s(0))))))), T1755).
log2c307(s(s(s(s(s(s(s(s(0)))))))), T1861) :- log2c960(s(s(s(s(s(s(s(0))))))), T1861).
log2c307(s(s(s(s(s(s(s(s(s(0))))))))), T1861) :- log2c960(s(s(s(s(s(s(s(0))))))), T1861).
log2c307(s(s(s(s(s(s(0)))))), T1928) :- log2c1012(s(s(s(s(s(s(s(0))))))), T1928).
log2c307(s(s(s(s(s(s(s(0))))))), T1928) :- log2c1012(s(s(s(s(s(s(s(0))))))), T1928).
log2c307(s(s(s(s(0)))), T1994) :- log2c1068(s(s(s(s(s(s(s(0))))))), T1994).
log2c307(s(s(s(s(s(0))))), T1994) :- log2c1068(s(s(s(s(s(s(s(0))))))), T1994).
log2c307(s(s(0)), T2015) :- log2c1106(s(s(s(s(s(s(s(0))))))), T2015).
log2c307(s(s(s(0))), T2015) :- log2c1106(s(s(s(s(s(s(s(0))))))), T2015).
log2c307(0, s(s(s(s(s(s(s(0)))))))).
log2c307(s(0), s(s(s(s(s(s(s(0)))))))).
log2c1183(T2082) :- log2c1068(s(s(s(s(s(s(s(0))))))), T2082).
log2c1249(T2141) :- log2c1068(s(s(s(s(s(s(s(0))))))), T2141).
log2c1319(T2189) :- log2c1106(s(s(s(s(s(s(s(0))))))), T2189).
log2c1370(T2229) :- log2c1106(s(s(s(s(s(s(s(0))))))), T2229).
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(T777)))))))))))))), T779) :- log2c294(T777, s(s(s(s(s(s(s(0))))))), T779).
log2c257(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2050) :- log2c1183(T2050).
log2c257(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2050) :- log2c1183(T2050).
log2c257(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2109) :- log2c1249(T2109).
log2c257(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2109) :- log2c1249(T2109).
log2c257(s(s(s(s(s(s(s(s(0)))))))), T2168) :- log2c1319(T2168).
log2c257(s(s(s(s(s(s(s(s(s(0))))))))), T2168) :- log2c1319(T2168).
log2c257(s(s(s(s(s(s(0)))))), T2208) :- log2c1370(T2208).
log2c257(s(s(s(s(s(s(s(0))))))), T2208) :- log2c1370(T2208).
log2c257(s(s(s(s(0)))), T2246) :- log2c1425(T2246).
log2c257(s(s(s(s(s(0))))), T2246) :- log2c1425(T2246).
log2c257(s(s(0)), T2262) :- log2c1462(T2262).
log2c257(s(s(s(0))), T2262) :- log2c1462(T2262).
log2c257(0, s(s(s(s(s(s(0))))))).
log2c257(s(0), s(s(s(s(s(s(0))))))).
log2c1540(T2324) :- log2c1425(T2324).
log2c1606(T2383) :- log2c1425(T2383).
log2c1676(T2431) :- log2c1462(T2431).
log2c1727(T2471) :- log2c1462(T2471).
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(T643)))))))))))))), T645) :- log2c244(T643, s(s(s(s(s(s(s(0))))))), T645).
log2c207(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2292) :- log2c1540(T2292).
log2c207(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2292) :- log2c1540(T2292).
log2c207(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2351) :- log2c1606(T2351).
log2c207(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2351) :- log2c1606(T2351).
log2c207(s(s(s(s(s(s(s(s(0)))))))), T2410) :- log2c1676(T2410).
log2c207(s(s(s(s(s(s(s(s(s(0))))))))), T2410) :- log2c1676(T2410).
log2c207(s(s(s(s(s(s(0)))))), T2450) :- log2c1727(T2450).
log2c207(s(s(s(s(s(s(s(0))))))), T2450) :- log2c1727(T2450).
log2c207(s(s(s(s(0)))), T2488) :- log2c1782(T2488).
log2c207(s(s(s(s(s(0))))), T2488) :- log2c1782(T2488).
log2c207(s(s(0)), T2504) :- log2c1819(T2504).
log2c207(s(s(s(0))), T2504) :- log2c1819(T2504).
log2c207(0, s(s(s(s(s(0)))))).
log2c207(s(0), s(s(s(s(s(0)))))).
log2c1897(T2566) :- log2c1782(T2566).
log2c1963(T2625) :- log2c1782(T2625).
log2c2033(T2673) :- log2c1819(T2673).
log2c2084(T2713) :- log2c1819(T2713).
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(T509)))))))))))))), T511) :- log2c194(T509, s(s(s(s(s(s(s(0))))))), T511).
log2c157(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2534) :- log2c1897(T2534).
log2c157(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2534) :- log2c1897(T2534).
log2c157(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2593) :- log2c1963(T2593).
log2c157(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2593) :- log2c1963(T2593).
log2c157(s(s(s(s(s(s(s(s(0)))))))), T2652) :- log2c2033(T2652).
log2c157(s(s(s(s(s(s(s(s(s(0))))))))), T2652) :- log2c2033(T2652).
log2c157(s(s(s(s(s(s(0)))))), T2692) :- log2c2084(T2692).
log2c157(s(s(s(s(s(s(s(0))))))), T2692) :- log2c2084(T2692).
log2c157(s(s(s(s(0)))), T2730) :- log2c2139(T2730).
log2c157(s(s(s(s(s(0))))), T2730) :- log2c2139(T2730).
log2c157(s(s(0)), T2746) :- log2c2176(T2746).
log2c157(s(s(s(0))), T2746) :- log2c2176(T2746).
log2c157(0, s(s(s(s(0))))).
log2c157(s(0), s(s(s(s(0))))).
log2c2254(T2808) :- log2c2139(T2808).
log2c2320(T2867) :- log2c2139(T2867).
log2c2390(T2915) :- log2c2176(T2915).
log2c2441(T2955) :- log2c2176(T2955).
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(T375)))))))))))))), T377) :- log2c144(T375, s(s(s(s(s(s(s(0))))))), T377).
log2c107(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T2776) :- log2c2254(T2776).
log2c107(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T2776) :- log2c2254(T2776).
log2c107(s(s(s(s(s(s(s(s(s(s(0)))))))))), T2835) :- log2c2320(T2835).
log2c107(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T2835) :- log2c2320(T2835).
log2c107(s(s(s(s(s(s(s(s(0)))))))), T2894) :- log2c2390(T2894).
log2c107(s(s(s(s(s(s(s(s(s(0))))))))), T2894) :- log2c2390(T2894).
log2c107(s(s(s(s(s(s(0)))))), T2934) :- log2c2441(T2934).
log2c107(s(s(s(s(s(s(s(0))))))), T2934) :- log2c2441(T2934).
log2c107(s(s(s(s(0)))), T2972) :- log2c2496(T2972).
log2c107(s(s(s(s(s(0))))), T2972) :- log2c2496(T2972).
log2c107(s(s(0)), T2988) :- log2c2533(T2988).
log2c107(s(s(s(0))), T2988) :- log2c2533(T2988).
log2c107(0, s(s(s(0)))).
log2c107(s(0), s(s(s(0)))).
log2c2611(T3050) :- log2c2496(T3050).
log2c2677(T3109) :- log2c2496(T3109).
log2c2747(T3157) :- log2c2533(T3157).
log2c2798(T3197) :- log2c2533(T3197).
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(T241)))))))))))))), T243) :- log2c94(T241, s(s(s(s(s(s(s(0))))))), T243).
log2c57(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), T3018) :- log2c2611(T3018).
log2c57(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), T3018) :- log2c2611(T3018).
log2c57(s(s(s(s(s(s(s(s(s(s(0)))))))))), T3077) :- log2c2677(T3077).
log2c57(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), T3077) :- log2c2677(T3077).
log2c57(s(s(s(s(s(s(s(s(0)))))))), T3136) :- log2c2747(T3136).
log2c57(s(s(s(s(s(s(s(s(s(0))))))))), T3136) :- log2c2747(T3136).
log2c57(s(s(s(s(s(s(0)))))), T3176) :- log2c2798(T3176).
log2c57(s(s(s(s(s(s(s(0))))))), T3176) :- log2c2798(T3176).
log2c57(s(s(s(s(0)))), T3214) :- log2c2853(T3214).
log2c57(s(s(s(s(s(0))))), T3214) :- log2c2853(T3214).
log2c57(s(s(0)), T3230) :- log2c2890(T3230).
log2c57(s(s(s(0))), T3230) :- log2c2890(T3230).
log2c57(0, s(s(0))).
log2c57(s(0), s(s(0))).
log2c2968(T3292) :- log2c2853(T3292).
log2c3034(T3351) :- log2c2853(T3351).
log2c3104(T3399) :- log2c2890(T3399).
log2c3155(T3439) :- log2c2890(T3439).
log2c3210(s(s(0))).
log2c3247(s(s(0))).
log2c822(T1706, T1708) :- log2c705(T1706, T1708).
log2c889(T1811, T1813) :- log2c705(T1811, T1813).
log2c960(T1898, T1900) :- log2c742(T1898, T1900).
log2c1012(T1965, T1967) :- log2c742(T1965, T1967).
log2c1068(T1999, s(T1999)).
log2c1106(T2020, s(T2020)).
Afs:
log21(x1, x2) = log21(x1)
(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: (b,f)
log244_in: (b,b,f)
log257_in: (b,f)
log294_in: (b,b,f)
log2107_in: (b,f)
log2144_in: (b,b,f)
log2157_in: (b,f)
log2194_in: (b,b,f)
log2207_in: (b,f)
log2244_in: (b,b,f)
log2257_in: (b,f)
log2294_in: (b,b,f)
log2307_in: (b,f)
log2344_in: (b,b,f)
log2359_in: (b,b,f)
log2395_in: (b,b,b,f)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
LOG21_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T107)))))))))))))))), T109) → U32_GA(T107, T109, log244_in_gga(T107, s(s(s(s(s(s(s(0))))))), T109))
LOG21_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T107)))))))))))))))), T109) → LOG244_IN_GGA(T107, s(s(s(s(s(s(s(0))))))), T109)
LOG244_IN_GGA(s(s(T128)), T129, T131) → U1_GGA(T128, T129, T131, log244_in_gga(T128, s(T129), T131))
LOG244_IN_GGA(s(s(T128)), T129, T131) → LOG244_IN_GGA(T128, s(T129), T131)
LOG244_IN_GGA(0, s(T148), T150) → U2_GGA(T148, T150, log257_in_ga(T148, T150))
LOG244_IN_GGA(0, s(T148), T150) → LOG257_IN_GA(T148, T150)
LOG257_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T241)))))))))))))), T243) → U31_GA(T241, T243, log294_in_gga(T241, s(s(s(s(s(s(s(0))))))), T243))
LOG257_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T241)))))))))))))), T243) → LOG294_IN_GGA(T241, s(s(s(s(s(s(s(0))))))), T243)
LOG294_IN_GGA(s(s(T262)), T263, T265) → U4_GGA(T262, T263, T265, log294_in_gga(T262, s(T263), T265))
LOG294_IN_GGA(s(s(T262)), T263, T265) → LOG294_IN_GGA(T262, s(T263), T265)
LOG294_IN_GGA(0, s(T282), T284) → U5_GGA(T282, T284, log2107_in_ga(T282, T284))
LOG294_IN_GGA(0, s(T282), T284) → LOG2107_IN_GA(T282, T284)
LOG2107_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T375)))))))))))))), T377) → U30_GA(T375, T377, log2144_in_gga(T375, s(s(s(s(s(s(s(0))))))), T377))
LOG2107_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T375)))))))))))))), T377) → LOG2144_IN_GGA(T375, s(s(s(s(s(s(s(0))))))), T377)
LOG2144_IN_GGA(s(s(T396)), T397, T399) → U7_GGA(T396, T397, T399, log2144_in_gga(T396, s(T397), T399))
LOG2144_IN_GGA(s(s(T396)), T397, T399) → LOG2144_IN_GGA(T396, s(T397), T399)
LOG2144_IN_GGA(0, s(T416), T418) → U8_GGA(T416, T418, log2157_in_ga(T416, T418))
LOG2144_IN_GGA(0, s(T416), T418) → LOG2157_IN_GA(T416, T418)
LOG2157_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T509)))))))))))))), T511) → U29_GA(T509, T511, log2194_in_gga(T509, s(s(s(s(s(s(s(0))))))), T511))
LOG2157_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T509)))))))))))))), T511) → LOG2194_IN_GGA(T509, s(s(s(s(s(s(s(0))))))), T511)
LOG2194_IN_GGA(s(s(T530)), T531, T533) → U10_GGA(T530, T531, T533, log2194_in_gga(T530, s(T531), T533))
LOG2194_IN_GGA(s(s(T530)), T531, T533) → LOG2194_IN_GGA(T530, s(T531), T533)
LOG2194_IN_GGA(0, s(T550), T552) → U11_GGA(T550, T552, log2207_in_ga(T550, T552))
LOG2194_IN_GGA(0, s(T550), T552) → LOG2207_IN_GA(T550, T552)
LOG2207_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T643)))))))))))))), T645) → U28_GA(T643, T645, log2244_in_gga(T643, s(s(s(s(s(s(s(0))))))), T645))
LOG2207_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T643)))))))))))))), T645) → LOG2244_IN_GGA(T643, s(s(s(s(s(s(s(0))))))), T645)
LOG2244_IN_GGA(s(s(T664)), T665, T667) → U13_GGA(T664, T665, T667, log2244_in_gga(T664, s(T665), T667))
LOG2244_IN_GGA(s(s(T664)), T665, T667) → LOG2244_IN_GGA(T664, s(T665), T667)
LOG2244_IN_GGA(0, s(T684), T686) → U14_GGA(T684, T686, log2257_in_ga(T684, T686))
LOG2244_IN_GGA(0, s(T684), T686) → LOG2257_IN_GA(T684, T686)
LOG2257_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T777)))))))))))))), T779) → U27_GA(T777, T779, log2294_in_gga(T777, s(s(s(s(s(s(s(0))))))), T779))
LOG2257_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T777)))))))))))))), T779) → LOG2294_IN_GGA(T777, s(s(s(s(s(s(s(0))))))), T779)
LOG2294_IN_GGA(s(s(T798)), T799, T801) → U16_GGA(T798, T799, T801, log2294_in_gga(T798, s(T799), T801))
LOG2294_IN_GGA(s(s(T798)), T799, T801) → LOG2294_IN_GGA(T798, s(T799), T801)
LOG2294_IN_GGA(0, s(T818), T820) → U17_GGA(T818, T820, log2307_in_ga(T818, T820))
LOG2294_IN_GGA(0, s(T818), T820) → LOG2307_IN_GA(T818, T820)
LOG2307_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T911)))))))))))))), T913) → U26_GA(T911, T913, log2344_in_gga(T911, s(s(s(s(s(s(s(0))))))), T913))
LOG2307_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T911)))))))))))))), T913) → LOG2344_IN_GGA(T911, s(s(s(s(s(s(s(0))))))), T913)
LOG2344_IN_GGA(s(s(T932)), T933, T935) → U19_GGA(T932, T933, T935, log2344_in_gga(T932, s(T933), T935))
LOG2344_IN_GGA(s(s(T932)), T933, T935) → LOG2344_IN_GGA(T932, s(T933), T935)
LOG2344_IN_GGA(0, s(T952), T954) → U20_GGA(T952, T954, log2359_in_gga(T952, s(s(s(s(s(s(s(0))))))), T954))
LOG2344_IN_GGA(0, s(T952), T954) → LOG2359_IN_GGA(T952, s(s(s(s(s(s(s(0))))))), T954)
LOG2359_IN_GGA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1089)))))))))))))), T1090, T1092) → U25_GGA(T1089, T1090, T1092, log2395_in_ggga(T1089, s(s(s(s(s(s(s(0))))))), T1090, T1092))
LOG2359_IN_GGA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1089)))))))))))))), T1090, T1092) → LOG2395_IN_GGGA(T1089, s(s(s(s(s(s(s(0))))))), T1090, T1092)
LOG2395_IN_GGGA(s(s(T1117)), T1118, T1119, T1121) → U22_GGGA(T1117, T1118, T1119, T1121, log2395_in_ggga(T1117, s(T1118), T1119, T1121))
LOG2395_IN_GGGA(s(s(T1117)), T1118, T1119, T1121) → LOG2395_IN_GGGA(T1117, s(T1118), T1119, T1121)
LOG2395_IN_GGGA(0, s(T1143), T1144, T1146) → U23_GGGA(T1143, T1144, T1146, log2359_in_gga(T1143, s(T1144), T1146))
LOG2395_IN_GGGA(0, s(T1143), T1144, T1146) → LOG2359_IN_GGA(T1143, s(T1144), T1146)
LOG2395_IN_GGGA(s(0), s(T1143), T1144, T1146) → U24_GGGA(T1143, T1144, T1146, log2359_in_gga(T1143, s(T1144), T1146))
LOG2395_IN_GGGA(s(0), s(T1143), T1144, T1146) → LOG2359_IN_GGA(T1143, s(T1144), T1146)
LOG2344_IN_GGA(s(0), s(T952), T954) → U21_GGA(T952, T954, log2359_in_gga(T952, s(s(s(s(s(s(s(0))))))), T954))
LOG2344_IN_GGA(s(0), s(T952), T954) → LOG2359_IN_GGA(T952, s(s(s(s(s(s(s(0))))))), T954)
LOG2294_IN_GGA(s(0), s(T818), T820) → U18_GGA(T818, T820, log2307_in_ga(T818, T820))
LOG2294_IN_GGA(s(0), s(T818), T820) → LOG2307_IN_GA(T818, T820)
LOG2244_IN_GGA(s(0), s(T684), T686) → U15_GGA(T684, T686, log2257_in_ga(T684, T686))
LOG2244_IN_GGA(s(0), s(T684), T686) → LOG2257_IN_GA(T684, T686)
LOG2194_IN_GGA(s(0), s(T550), T552) → U12_GGA(T550, T552, log2207_in_ga(T550, T552))
LOG2194_IN_GGA(s(0), s(T550), T552) → LOG2207_IN_GA(T550, T552)
LOG2144_IN_GGA(s(0), s(T416), T418) → U9_GGA(T416, T418, log2157_in_ga(T416, T418))
LOG2144_IN_GGA(s(0), s(T416), T418) → LOG2157_IN_GA(T416, T418)
LOG294_IN_GGA(s(0), s(T282), T284) → U6_GGA(T282, T284, log2107_in_ga(T282, T284))
LOG294_IN_GGA(s(0), s(T282), T284) → LOG2107_IN_GA(T282, T284)
LOG244_IN_GGA(s(0), s(T148), T150) → U3_GGA(T148, T150, log257_in_ga(T148, T150))
LOG244_IN_GGA(s(0), s(T148), T150) → LOG257_IN_GA(T148, T150)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
log244_in_gga(
x1,
x2,
x3) =
log244_in_gga(
x1,
x2)
0 =
0
log257_in_ga(
x1,
x2) =
log257_in_ga(
x1)
log294_in_gga(
x1,
x2,
x3) =
log294_in_gga(
x1,
x2)
log2107_in_ga(
x1,
x2) =
log2107_in_ga(
x1)
log2144_in_gga(
x1,
x2,
x3) =
log2144_in_gga(
x1,
x2)
log2157_in_ga(
x1,
x2) =
log2157_in_ga(
x1)
log2194_in_gga(
x1,
x2,
x3) =
log2194_in_gga(
x1,
x2)
log2207_in_ga(
x1,
x2) =
log2207_in_ga(
x1)
log2244_in_gga(
x1,
x2,
x3) =
log2244_in_gga(
x1,
x2)
log2257_in_ga(
x1,
x2) =
log2257_in_ga(
x1)
log2294_in_gga(
x1,
x2,
x3) =
log2294_in_gga(
x1,
x2)
log2307_in_ga(
x1,
x2) =
log2307_in_ga(
x1)
log2344_in_gga(
x1,
x2,
x3) =
log2344_in_gga(
x1,
x2)
log2359_in_gga(
x1,
x2,
x3) =
log2359_in_gga(
x1,
x2)
log2395_in_ggga(
x1,
x2,
x3,
x4) =
log2395_in_ggga(
x1,
x2,
x3)
LOG21_IN_GA(
x1,
x2) =
LOG21_IN_GA(
x1)
U32_GA(
x1,
x2,
x3) =
U32_GA(
x1,
x3)
LOG244_IN_GGA(
x1,
x2,
x3) =
LOG244_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
U2_GGA(
x1,
x2,
x3) =
U2_GGA(
x1,
x3)
LOG257_IN_GA(
x1,
x2) =
LOG257_IN_GA(
x1)
U31_GA(
x1,
x2,
x3) =
U31_GA(
x1,
x3)
LOG294_IN_GGA(
x1,
x2,
x3) =
LOG294_IN_GGA(
x1,
x2)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x1,
x2,
x4)
U5_GGA(
x1,
x2,
x3) =
U5_GGA(
x1,
x3)
LOG2107_IN_GA(
x1,
x2) =
LOG2107_IN_GA(
x1)
U30_GA(
x1,
x2,
x3) =
U30_GA(
x1,
x3)
LOG2144_IN_GGA(
x1,
x2,
x3) =
LOG2144_IN_GGA(
x1,
x2)
U7_GGA(
x1,
x2,
x3,
x4) =
U7_GGA(
x1,
x2,
x4)
U8_GGA(
x1,
x2,
x3) =
U8_GGA(
x1,
x3)
LOG2157_IN_GA(
x1,
x2) =
LOG2157_IN_GA(
x1)
U29_GA(
x1,
x2,
x3) =
U29_GA(
x1,
x3)
LOG2194_IN_GGA(
x1,
x2,
x3) =
LOG2194_IN_GGA(
x1,
x2)
U10_GGA(
x1,
x2,
x3,
x4) =
U10_GGA(
x1,
x2,
x4)
U11_GGA(
x1,
x2,
x3) =
U11_GGA(
x1,
x3)
LOG2207_IN_GA(
x1,
x2) =
LOG2207_IN_GA(
x1)
U28_GA(
x1,
x2,
x3) =
U28_GA(
x1,
x3)
LOG2244_IN_GGA(
x1,
x2,
x3) =
LOG2244_IN_GGA(
x1,
x2)
U13_GGA(
x1,
x2,
x3,
x4) =
U13_GGA(
x1,
x2,
x4)
U14_GGA(
x1,
x2,
x3) =
U14_GGA(
x1,
x3)
LOG2257_IN_GA(
x1,
x2) =
LOG2257_IN_GA(
x1)
U27_GA(
x1,
x2,
x3) =
U27_GA(
x1,
x3)
LOG2294_IN_GGA(
x1,
x2,
x3) =
LOG2294_IN_GGA(
x1,
x2)
U16_GGA(
x1,
x2,
x3,
x4) =
U16_GGA(
x1,
x2,
x4)
U17_GGA(
x1,
x2,
x3) =
U17_GGA(
x1,
x3)
LOG2307_IN_GA(
x1,
x2) =
LOG2307_IN_GA(
x1)
U26_GA(
x1,
x2,
x3) =
U26_GA(
x1,
x3)
LOG2344_IN_GGA(
x1,
x2,
x3) =
LOG2344_IN_GGA(
x1,
x2)
U19_GGA(
x1,
x2,
x3,
x4) =
U19_GGA(
x1,
x2,
x4)
U20_GGA(
x1,
x2,
x3) =
U20_GGA(
x1,
x3)
LOG2359_IN_GGA(
x1,
x2,
x3) =
LOG2359_IN_GGA(
x1,
x2)
U25_GGA(
x1,
x2,
x3,
x4) =
U25_GGA(
x1,
x2,
x4)
LOG2395_IN_GGGA(
x1,
x2,
x3,
x4) =
LOG2395_IN_GGGA(
x1,
x2,
x3)
U22_GGGA(
x1,
x2,
x3,
x4,
x5) =
U22_GGGA(
x1,
x2,
x3,
x5)
U23_GGGA(
x1,
x2,
x3,
x4) =
U23_GGGA(
x1,
x2,
x4)
U24_GGGA(
x1,
x2,
x3,
x4) =
U24_GGGA(
x1,
x2,
x4)
U21_GGA(
x1,
x2,
x3) =
U21_GGA(
x1,
x3)
U18_GGA(
x1,
x2,
x3) =
U18_GGA(
x1,
x3)
U15_GGA(
x1,
x2,
x3) =
U15_GGA(
x1,
x3)
U12_GGA(
x1,
x2,
x3) =
U12_GGA(
x1,
x3)
U9_GGA(
x1,
x2,
x3) =
U9_GGA(
x1,
x3)
U6_GGA(
x1,
x2,
x3) =
U6_GGA(
x1,
x3)
U3_GGA(
x1,
x2,
x3) =
U3_GGA(
x1,
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_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T107)))))))))))))))), T109) → U32_GA(T107, T109, log244_in_gga(T107, s(s(s(s(s(s(s(0))))))), T109))
LOG21_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T107)))))))))))))))), T109) → LOG244_IN_GGA(T107, s(s(s(s(s(s(s(0))))))), T109)
LOG244_IN_GGA(s(s(T128)), T129, T131) → U1_GGA(T128, T129, T131, log244_in_gga(T128, s(T129), T131))
LOG244_IN_GGA(s(s(T128)), T129, T131) → LOG244_IN_GGA(T128, s(T129), T131)
LOG244_IN_GGA(0, s(T148), T150) → U2_GGA(T148, T150, log257_in_ga(T148, T150))
LOG244_IN_GGA(0, s(T148), T150) → LOG257_IN_GA(T148, T150)
LOG257_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T241)))))))))))))), T243) → U31_GA(T241, T243, log294_in_gga(T241, s(s(s(s(s(s(s(0))))))), T243))
LOG257_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T241)))))))))))))), T243) → LOG294_IN_GGA(T241, s(s(s(s(s(s(s(0))))))), T243)
LOG294_IN_GGA(s(s(T262)), T263, T265) → U4_GGA(T262, T263, T265, log294_in_gga(T262, s(T263), T265))
LOG294_IN_GGA(s(s(T262)), T263, T265) → LOG294_IN_GGA(T262, s(T263), T265)
LOG294_IN_GGA(0, s(T282), T284) → U5_GGA(T282, T284, log2107_in_ga(T282, T284))
LOG294_IN_GGA(0, s(T282), T284) → LOG2107_IN_GA(T282, T284)
LOG2107_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T375)))))))))))))), T377) → U30_GA(T375, T377, log2144_in_gga(T375, s(s(s(s(s(s(s(0))))))), T377))
LOG2107_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T375)))))))))))))), T377) → LOG2144_IN_GGA(T375, s(s(s(s(s(s(s(0))))))), T377)
LOG2144_IN_GGA(s(s(T396)), T397, T399) → U7_GGA(T396, T397, T399, log2144_in_gga(T396, s(T397), T399))
LOG2144_IN_GGA(s(s(T396)), T397, T399) → LOG2144_IN_GGA(T396, s(T397), T399)
LOG2144_IN_GGA(0, s(T416), T418) → U8_GGA(T416, T418, log2157_in_ga(T416, T418))
LOG2144_IN_GGA(0, s(T416), T418) → LOG2157_IN_GA(T416, T418)
LOG2157_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T509)))))))))))))), T511) → U29_GA(T509, T511, log2194_in_gga(T509, s(s(s(s(s(s(s(0))))))), T511))
LOG2157_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T509)))))))))))))), T511) → LOG2194_IN_GGA(T509, s(s(s(s(s(s(s(0))))))), T511)
LOG2194_IN_GGA(s(s(T530)), T531, T533) → U10_GGA(T530, T531, T533, log2194_in_gga(T530, s(T531), T533))
LOG2194_IN_GGA(s(s(T530)), T531, T533) → LOG2194_IN_GGA(T530, s(T531), T533)
LOG2194_IN_GGA(0, s(T550), T552) → U11_GGA(T550, T552, log2207_in_ga(T550, T552))
LOG2194_IN_GGA(0, s(T550), T552) → LOG2207_IN_GA(T550, T552)
LOG2207_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T643)))))))))))))), T645) → U28_GA(T643, T645, log2244_in_gga(T643, s(s(s(s(s(s(s(0))))))), T645))
LOG2207_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T643)))))))))))))), T645) → LOG2244_IN_GGA(T643, s(s(s(s(s(s(s(0))))))), T645)
LOG2244_IN_GGA(s(s(T664)), T665, T667) → U13_GGA(T664, T665, T667, log2244_in_gga(T664, s(T665), T667))
LOG2244_IN_GGA(s(s(T664)), T665, T667) → LOG2244_IN_GGA(T664, s(T665), T667)
LOG2244_IN_GGA(0, s(T684), T686) → U14_GGA(T684, T686, log2257_in_ga(T684, T686))
LOG2244_IN_GGA(0, s(T684), T686) → LOG2257_IN_GA(T684, T686)
LOG2257_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T777)))))))))))))), T779) → U27_GA(T777, T779, log2294_in_gga(T777, s(s(s(s(s(s(s(0))))))), T779))
LOG2257_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T777)))))))))))))), T779) → LOG2294_IN_GGA(T777, s(s(s(s(s(s(s(0))))))), T779)
LOG2294_IN_GGA(s(s(T798)), T799, T801) → U16_GGA(T798, T799, T801, log2294_in_gga(T798, s(T799), T801))
LOG2294_IN_GGA(s(s(T798)), T799, T801) → LOG2294_IN_GGA(T798, s(T799), T801)
LOG2294_IN_GGA(0, s(T818), T820) → U17_GGA(T818, T820, log2307_in_ga(T818, T820))
LOG2294_IN_GGA(0, s(T818), T820) → LOG2307_IN_GA(T818, T820)
LOG2307_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T911)))))))))))))), T913) → U26_GA(T911, T913, log2344_in_gga(T911, s(s(s(s(s(s(s(0))))))), T913))
LOG2307_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T911)))))))))))))), T913) → LOG2344_IN_GGA(T911, s(s(s(s(s(s(s(0))))))), T913)
LOG2344_IN_GGA(s(s(T932)), T933, T935) → U19_GGA(T932, T933, T935, log2344_in_gga(T932, s(T933), T935))
LOG2344_IN_GGA(s(s(T932)), T933, T935) → LOG2344_IN_GGA(T932, s(T933), T935)
LOG2344_IN_GGA(0, s(T952), T954) → U20_GGA(T952, T954, log2359_in_gga(T952, s(s(s(s(s(s(s(0))))))), T954))
LOG2344_IN_GGA(0, s(T952), T954) → LOG2359_IN_GGA(T952, s(s(s(s(s(s(s(0))))))), T954)
LOG2359_IN_GGA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1089)))))))))))))), T1090, T1092) → U25_GGA(T1089, T1090, T1092, log2395_in_ggga(T1089, s(s(s(s(s(s(s(0))))))), T1090, T1092))
LOG2359_IN_GGA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1089)))))))))))))), T1090, T1092) → LOG2395_IN_GGGA(T1089, s(s(s(s(s(s(s(0))))))), T1090, T1092)
LOG2395_IN_GGGA(s(s(T1117)), T1118, T1119, T1121) → U22_GGGA(T1117, T1118, T1119, T1121, log2395_in_ggga(T1117, s(T1118), T1119, T1121))
LOG2395_IN_GGGA(s(s(T1117)), T1118, T1119, T1121) → LOG2395_IN_GGGA(T1117, s(T1118), T1119, T1121)
LOG2395_IN_GGGA(0, s(T1143), T1144, T1146) → U23_GGGA(T1143, T1144, T1146, log2359_in_gga(T1143, s(T1144), T1146))
LOG2395_IN_GGGA(0, s(T1143), T1144, T1146) → LOG2359_IN_GGA(T1143, s(T1144), T1146)
LOG2395_IN_GGGA(s(0), s(T1143), T1144, T1146) → U24_GGGA(T1143, T1144, T1146, log2359_in_gga(T1143, s(T1144), T1146))
LOG2395_IN_GGGA(s(0), s(T1143), T1144, T1146) → LOG2359_IN_GGA(T1143, s(T1144), T1146)
LOG2344_IN_GGA(s(0), s(T952), T954) → U21_GGA(T952, T954, log2359_in_gga(T952, s(s(s(s(s(s(s(0))))))), T954))
LOG2344_IN_GGA(s(0), s(T952), T954) → LOG2359_IN_GGA(T952, s(s(s(s(s(s(s(0))))))), T954)
LOG2294_IN_GGA(s(0), s(T818), T820) → U18_GGA(T818, T820, log2307_in_ga(T818, T820))
LOG2294_IN_GGA(s(0), s(T818), T820) → LOG2307_IN_GA(T818, T820)
LOG2244_IN_GGA(s(0), s(T684), T686) → U15_GGA(T684, T686, log2257_in_ga(T684, T686))
LOG2244_IN_GGA(s(0), s(T684), T686) → LOG2257_IN_GA(T684, T686)
LOG2194_IN_GGA(s(0), s(T550), T552) → U12_GGA(T550, T552, log2207_in_ga(T550, T552))
LOG2194_IN_GGA(s(0), s(T550), T552) → LOG2207_IN_GA(T550, T552)
LOG2144_IN_GGA(s(0), s(T416), T418) → U9_GGA(T416, T418, log2157_in_ga(T416, T418))
LOG2144_IN_GGA(s(0), s(T416), T418) → LOG2157_IN_GA(T416, T418)
LOG294_IN_GGA(s(0), s(T282), T284) → U6_GGA(T282, T284, log2107_in_ga(T282, T284))
LOG294_IN_GGA(s(0), s(T282), T284) → LOG2107_IN_GA(T282, T284)
LOG244_IN_GGA(s(0), s(T148), T150) → U3_GGA(T148, T150, log257_in_ga(T148, T150))
LOG244_IN_GGA(s(0), s(T148), T150) → LOG257_IN_GA(T148, T150)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
log244_in_gga(
x1,
x2,
x3) =
log244_in_gga(
x1,
x2)
0 =
0
log257_in_ga(
x1,
x2) =
log257_in_ga(
x1)
log294_in_gga(
x1,
x2,
x3) =
log294_in_gga(
x1,
x2)
log2107_in_ga(
x1,
x2) =
log2107_in_ga(
x1)
log2144_in_gga(
x1,
x2,
x3) =
log2144_in_gga(
x1,
x2)
log2157_in_ga(
x1,
x2) =
log2157_in_ga(
x1)
log2194_in_gga(
x1,
x2,
x3) =
log2194_in_gga(
x1,
x2)
log2207_in_ga(
x1,
x2) =
log2207_in_ga(
x1)
log2244_in_gga(
x1,
x2,
x3) =
log2244_in_gga(
x1,
x2)
log2257_in_ga(
x1,
x2) =
log2257_in_ga(
x1)
log2294_in_gga(
x1,
x2,
x3) =
log2294_in_gga(
x1,
x2)
log2307_in_ga(
x1,
x2) =
log2307_in_ga(
x1)
log2344_in_gga(
x1,
x2,
x3) =
log2344_in_gga(
x1,
x2)
log2359_in_gga(
x1,
x2,
x3) =
log2359_in_gga(
x1,
x2)
log2395_in_ggga(
x1,
x2,
x3,
x4) =
log2395_in_ggga(
x1,
x2,
x3)
LOG21_IN_GA(
x1,
x2) =
LOG21_IN_GA(
x1)
U32_GA(
x1,
x2,
x3) =
U32_GA(
x1,
x3)
LOG244_IN_GGA(
x1,
x2,
x3) =
LOG244_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
U2_GGA(
x1,
x2,
x3) =
U2_GGA(
x1,
x3)
LOG257_IN_GA(
x1,
x2) =
LOG257_IN_GA(
x1)
U31_GA(
x1,
x2,
x3) =
U31_GA(
x1,
x3)
LOG294_IN_GGA(
x1,
x2,
x3) =
LOG294_IN_GGA(
x1,
x2)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x1,
x2,
x4)
U5_GGA(
x1,
x2,
x3) =
U5_GGA(
x1,
x3)
LOG2107_IN_GA(
x1,
x2) =
LOG2107_IN_GA(
x1)
U30_GA(
x1,
x2,
x3) =
U30_GA(
x1,
x3)
LOG2144_IN_GGA(
x1,
x2,
x3) =
LOG2144_IN_GGA(
x1,
x2)
U7_GGA(
x1,
x2,
x3,
x4) =
U7_GGA(
x1,
x2,
x4)
U8_GGA(
x1,
x2,
x3) =
U8_GGA(
x1,
x3)
LOG2157_IN_GA(
x1,
x2) =
LOG2157_IN_GA(
x1)
U29_GA(
x1,
x2,
x3) =
U29_GA(
x1,
x3)
LOG2194_IN_GGA(
x1,
x2,
x3) =
LOG2194_IN_GGA(
x1,
x2)
U10_GGA(
x1,
x2,
x3,
x4) =
U10_GGA(
x1,
x2,
x4)
U11_GGA(
x1,
x2,
x3) =
U11_GGA(
x1,
x3)
LOG2207_IN_GA(
x1,
x2) =
LOG2207_IN_GA(
x1)
U28_GA(
x1,
x2,
x3) =
U28_GA(
x1,
x3)
LOG2244_IN_GGA(
x1,
x2,
x3) =
LOG2244_IN_GGA(
x1,
x2)
U13_GGA(
x1,
x2,
x3,
x4) =
U13_GGA(
x1,
x2,
x4)
U14_GGA(
x1,
x2,
x3) =
U14_GGA(
x1,
x3)
LOG2257_IN_GA(
x1,
x2) =
LOG2257_IN_GA(
x1)
U27_GA(
x1,
x2,
x3) =
U27_GA(
x1,
x3)
LOG2294_IN_GGA(
x1,
x2,
x3) =
LOG2294_IN_GGA(
x1,
x2)
U16_GGA(
x1,
x2,
x3,
x4) =
U16_GGA(
x1,
x2,
x4)
U17_GGA(
x1,
x2,
x3) =
U17_GGA(
x1,
x3)
LOG2307_IN_GA(
x1,
x2) =
LOG2307_IN_GA(
x1)
U26_GA(
x1,
x2,
x3) =
U26_GA(
x1,
x3)
LOG2344_IN_GGA(
x1,
x2,
x3) =
LOG2344_IN_GGA(
x1,
x2)
U19_GGA(
x1,
x2,
x3,
x4) =
U19_GGA(
x1,
x2,
x4)
U20_GGA(
x1,
x2,
x3) =
U20_GGA(
x1,
x3)
LOG2359_IN_GGA(
x1,
x2,
x3) =
LOG2359_IN_GGA(
x1,
x2)
U25_GGA(
x1,
x2,
x3,
x4) =
U25_GGA(
x1,
x2,
x4)
LOG2395_IN_GGGA(
x1,
x2,
x3,
x4) =
LOG2395_IN_GGGA(
x1,
x2,
x3)
U22_GGGA(
x1,
x2,
x3,
x4,
x5) =
U22_GGGA(
x1,
x2,
x3,
x5)
U23_GGGA(
x1,
x2,
x3,
x4) =
U23_GGGA(
x1,
x2,
x4)
U24_GGGA(
x1,
x2,
x3,
x4) =
U24_GGGA(
x1,
x2,
x4)
U21_GGA(
x1,
x2,
x3) =
U21_GGA(
x1,
x3)
U18_GGA(
x1,
x2,
x3) =
U18_GGA(
x1,
x3)
U15_GGA(
x1,
x2,
x3) =
U15_GGA(
x1,
x3)
U12_GGA(
x1,
x2,
x3) =
U12_GGA(
x1,
x3)
U9_GGA(
x1,
x2,
x3) =
U9_GGA(
x1,
x3)
U6_GGA(
x1,
x2,
x3) =
U6_GGA(
x1,
x3)
U3_GGA(
x1,
x2,
x3) =
U3_GGA(
x1,
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_GGA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1089)))))))))))))), T1090, T1092) → LOG2395_IN_GGGA(T1089, s(s(s(s(s(s(s(0))))))), T1090, T1092)
LOG2395_IN_GGGA(s(s(T1117)), T1118, T1119, T1121) → LOG2395_IN_GGGA(T1117, s(T1118), T1119, T1121)
LOG2395_IN_GGGA(0, s(T1143), T1144, T1146) → LOG2359_IN_GGA(T1143, s(T1144), T1146)
LOG2395_IN_GGGA(s(0), s(T1143), T1144, T1146) → LOG2359_IN_GGA(T1143, s(T1144), T1146)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
0 =
0
LOG2359_IN_GGA(
x1,
x2,
x3) =
LOG2359_IN_GGA(
x1,
x2)
LOG2395_IN_GGGA(
x1,
x2,
x3,
x4) =
LOG2395_IN_GGGA(
x1,
x2,
x3)
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:
LOG2359_IN_GGA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1089)))))))))))))), T1090) → LOG2395_IN_GGGA(T1089, s(s(s(s(s(s(s(0))))))), T1090)
LOG2395_IN_GGGA(s(s(T1117)), T1118, T1119) → LOG2395_IN_GGGA(T1117, s(T1118), T1119)
LOG2395_IN_GGGA(0, s(T1143), T1144) → LOG2359_IN_GGA(T1143, s(T1144))
LOG2395_IN_GGGA(s(0), s(T1143), T1144) → LOG2359_IN_GGA(T1143, s(T1144))
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_GGA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(T1089)))))))))))))), T1090) → LOG2395_IN_GGGA(T1089, s(s(s(s(s(s(s(0))))))), T1090)
LOG2395_IN_GGGA(s(s(T1117)), T1118, T1119) → LOG2395_IN_GGGA(T1117, s(T1118), T1119)
LOG2395_IN_GGGA(0, s(T1143), T1144) → LOG2359_IN_GGA(T1143, s(T1144))
LOG2395_IN_GGGA(s(0), s(T1143), T1144) → LOG2359_IN_GGA(T1143, s(T1144))
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(LOG2359_IN_GGA(x1, x2)) = x1 + x2
POL(LOG2395_IN_GGGA(x1, x2, x3)) = 1 + x1 + x2 + x3
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_GGA(s(s(T932)), T933, T935) → LOG2344_IN_GGA(T932, s(T933), T935)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
LOG2344_IN_GGA(
x1,
x2,
x3) =
LOG2344_IN_GGA(
x1,
x2)
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:
LOG2344_IN_GGA(s(s(T932)), T933) → LOG2344_IN_GGA(T932, s(T933))
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_GGA(s(s(T932)), T933) → LOG2344_IN_GGA(T932, s(T933))
The graph contains the following edges 1 > 1
(20) YES
(21) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LOG2294_IN_GGA(s(s(T798)), T799, T801) → LOG2294_IN_GGA(T798, s(T799), T801)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
LOG2294_IN_GGA(
x1,
x2,
x3) =
LOG2294_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(22) PiDPToQDPProof (SOUND 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_GGA(s(s(T798)), T799) → LOG2294_IN_GGA(T798, s(T799))
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_GGA(s(s(T798)), T799) → LOG2294_IN_GGA(T798, s(T799))
The graph contains the following edges 1 > 1
(25) YES
(26) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LOG2244_IN_GGA(s(s(T664)), T665, T667) → LOG2244_IN_GGA(T664, s(T665), T667)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
LOG2244_IN_GGA(
x1,
x2,
x3) =
LOG2244_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(27) PiDPToQDPProof (SOUND 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_GGA(s(s(T664)), T665) → LOG2244_IN_GGA(T664, s(T665))
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_GGA(s(s(T664)), T665) → LOG2244_IN_GGA(T664, s(T665))
The graph contains the following edges 1 > 1
(30) YES
(31) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LOG2194_IN_GGA(s(s(T530)), T531, T533) → LOG2194_IN_GGA(T530, s(T531), T533)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
LOG2194_IN_GGA(
x1,
x2,
x3) =
LOG2194_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(32) PiDPToQDPProof (SOUND 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_GGA(s(s(T530)), T531) → LOG2194_IN_GGA(T530, s(T531))
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_GGA(s(s(T530)), T531) → LOG2194_IN_GGA(T530, s(T531))
The graph contains the following edges 1 > 1
(35) YES
(36) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LOG2144_IN_GGA(s(s(T396)), T397, T399) → LOG2144_IN_GGA(T396, s(T397), T399)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
LOG2144_IN_GGA(
x1,
x2,
x3) =
LOG2144_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(37) PiDPToQDPProof (SOUND 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_GGA(s(s(T396)), T397) → LOG2144_IN_GGA(T396, s(T397))
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_GGA(s(s(T396)), T397) → LOG2144_IN_GGA(T396, s(T397))
The graph contains the following edges 1 > 1
(40) YES
(41) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LOG294_IN_GGA(s(s(T262)), T263, T265) → LOG294_IN_GGA(T262, s(T263), T265)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
LOG294_IN_GGA(
x1,
x2,
x3) =
LOG294_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(42) PiDPToQDPProof (SOUND 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_GGA(s(s(T262)), T263) → LOG294_IN_GGA(T262, s(T263))
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_GGA(s(s(T262)), T263) → LOG294_IN_GGA(T262, s(T263))
The graph contains the following edges 1 > 1
(45) YES
(46) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LOG244_IN_GGA(s(s(T128)), T129, T131) → LOG244_IN_GGA(T128, s(T129), T131)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
LOG244_IN_GGA(
x1,
x2,
x3) =
LOG244_IN_GGA(
x1,
x2)
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_GGA(s(s(T128)), T129) → LOG244_IN_GGA(T128, s(T129))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(49) 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:
- LOG244_IN_GGA(s(s(T128)), T129) → LOG244_IN_GGA(T128, s(T129))
The graph contains the following edges 1 > 1
(50) YES