(0) Obligation:

Clauses:

ackermann(0, N, s(N)).
ackermann(s(M), 0, Val) :- ackermann(M, s(0), Val).
ackermann(s(M), s(N), Val) :- ','(ackermann(s(M), N, Val1), ackermann(M, Val1, Val)).

Queries:

ackermann(g,a,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

ackermann21(T28, X73) :- ackermann27(T28, X73).
ackermann27(s(T32), X97) :- ackermann21(T32, X96).
ackermann27(s(T32), X97) :- ','(ackermannc21(T32, T34), ackermann38(T32, T34, X97)).
ackermann38(s(T47), 0, X133) :- ackermann27(T47, X133).
ackermann38(s(T52), s(T53), X151) :- ackermann38(s(T52), T53, X150).
ackermann38(s(T52), s(T53), X151) :- ','(ackermannc38(s(T52), T53, T55), ackermann38(T52, T55, X151)).
ackermann57(T79, 0, X211) :- ackermann27(T79, X211).
ackermann57(T84, s(T86), X229) :- p65(T84, T86, X228, X229).
p65(T84, T86, X228, X229) :- ackermann57(T84, T86, X228).
p65(T84, T86, T88, X229) :- ','(ackermannc57(T84, T86, T88), ackermann68(T84, T88, X229)).
ackermann68(s(T101), 0, X265) :- ackermann27(T101, X265).
ackermann68(s(T106), s(T108), X283) :- p65(T106, T108, X282, X283).
ackermann1(s(s(T19)), 0, T20) :- ackermann21(T19, X40).
ackermann1(s(s(T19)), 0, T20) :- ','(ackermannc21(T19, T22), ackermann1(T19, T22, T20)).
ackermann1(s(T68), s(T71), T70) :- ackermann57(T68, T71, X182).
ackermann1(s(T68), s(T71), T70) :- ','(ackermannc57(T68, T71, T73), ackermann1(T68, T73, T70)).
ackermann1(s(T123), s(0), T117) :- ackermann27(T123, X319).
ackermann1(s(T123), s(0), T117) :- ','(ackermannc27(T123, T124), ackermann1(T123, T124, T117)).
ackermann1(s(T131), s(s(T133)), T117) :- ackermann57(T131, T133, X340).
ackermann1(s(T131), s(s(T133)), T117) :- ','(ackermannc57(T131, T133, T135), ackermann68(T131, T135, X341)).
ackermann1(s(T131), s(s(T133)), T117) :- ','(ackermannc57(T131, T133, T135), ','(ackermannc68(T131, T135, T139), ackermann1(T131, T139, T117))).

Clauses:

ackermannc1(0, T5, s(T5)).
ackermannc1(s(0), 0, s(s(0))).
ackermannc1(s(s(T19)), 0, T20) :- ','(ackermannc21(T19, T22), ackermannc1(T19, T22, T20)).
ackermannc1(s(T68), s(T71), T70) :- ','(ackermannc57(T68, T71, T73), ackermannc1(T68, T73, T70)).
ackermannc1(s(T123), s(0), T117) :- ','(ackermannc27(T123, T124), ackermannc1(T123, T124, T117)).
ackermannc1(s(T131), s(s(T133)), T117) :- ','(ackermannc57(T131, T133, T135), ','(ackermannc68(T131, T135, T139), ackermannc1(T131, T139, T117))).
ackermannc21(T28, X73) :- ackermannc27(T28, X73).
ackermannc27(0, s(s(0))).
ackermannc27(s(T32), X97) :- ','(ackermannc21(T32, T34), ackermannc38(T32, T34, X97)).
ackermannc38(0, T42, s(T42)).
ackermannc38(s(T47), 0, X133) :- ackermannc27(T47, X133).
ackermannc38(s(T52), s(T53), X151) :- ','(ackermannc38(s(T52), T53, T55), ackermannc38(T52, T55, X151)).
ackermannc57(T79, 0, X211) :- ackermannc27(T79, X211).
ackermannc57(T84, s(T86), X229) :- qc65(T84, T86, X228, X229).
qc65(T84, T86, T88, X229) :- ','(ackermannc57(T84, T86, T88), ackermannc68(T84, T88, X229)).
ackermannc68(0, T96, s(T96)).
ackermannc68(s(T101), 0, X265) :- ackermannc27(T101, X265).
ackermannc68(s(T106), s(T108), X283) :- qc65(T106, T108, X282, X283).

Afs:

ackermann1(x1, x2, x3)  =  ackermann1(x1, x3)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
ackermann1_in: (b,f,b) (b,b,b)
ackermann21_in: (b,f)
ackermann27_in: (b,f)
ackermannc21_in: (b,f)
ackermannc27_in: (b,f)
ackermannc38_in: (b,b,f)
ackermann38_in: (b,b,f)
ackermann57_in: (b,b,f) (b,f,f)
p65_in: (b,b,f,f) (b,f,f,f)
ackermannc57_in: (b,b,f) (b,f,f)
qc65_in: (b,b,f,f) (b,f,f,f)
ackermannc68_in: (b,b,f)
ackermann68_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

ACKERMANN1_IN_GAG(s(s(T19)), 0, T20) → U16_GAG(T19, T20, ackermann21_in_ga(T19, X40))
ACKERMANN1_IN_GAG(s(s(T19)), 0, T20) → ACKERMANN21_IN_GA(T19, X40)
ACKERMANN21_IN_GA(T28, X73) → U1_GA(T28, X73, ackermann27_in_ga(T28, X73))
ACKERMANN21_IN_GA(T28, X73) → ACKERMANN27_IN_GA(T28, X73)
ACKERMANN27_IN_GA(s(T32), X97) → U2_GA(T32, X97, ackermann21_in_ga(T32, X96))
ACKERMANN27_IN_GA(s(T32), X97) → ACKERMANN21_IN_GA(T32, X96)
ACKERMANN27_IN_GA(s(T32), X97) → U3_GA(T32, X97, ackermannc21_in_ga(T32, T34))
U3_GA(T32, X97, ackermannc21_out_ga(T32, T34)) → U4_GA(T32, X97, ackermann38_in_gga(T32, T34, X97))
U3_GA(T32, X97, ackermannc21_out_ga(T32, T34)) → ACKERMANN38_IN_GGA(T32, T34, X97)
ACKERMANN38_IN_GGA(s(T47), 0, X133) → U5_GGA(T47, X133, ackermann27_in_ga(T47, X133))
ACKERMANN38_IN_GGA(s(T47), 0, X133) → ACKERMANN27_IN_GA(T47, X133)
ACKERMANN38_IN_GGA(s(T52), s(T53), X151) → U6_GGA(T52, T53, X151, ackermann38_in_gga(s(T52), T53, X150))
ACKERMANN38_IN_GGA(s(T52), s(T53), X151) → ACKERMANN38_IN_GGA(s(T52), T53, X150)
ACKERMANN38_IN_GGA(s(T52), s(T53), X151) → U7_GGA(T52, T53, X151, ackermannc38_in_gga(s(T52), T53, T55))
U7_GGA(T52, T53, X151, ackermannc38_out_gga(s(T52), T53, T55)) → U8_GGA(T52, T53, X151, ackermann38_in_gga(T52, T55, X151))
U7_GGA(T52, T53, X151, ackermannc38_out_gga(s(T52), T53, T55)) → ACKERMANN38_IN_GGA(T52, T55, X151)
ACKERMANN1_IN_GAG(s(s(T19)), 0, T20) → U17_GAG(T19, T20, ackermannc21_in_ga(T19, T22))
U17_GAG(T19, T20, ackermannc21_out_ga(T19, T22)) → U18_GAG(T19, T20, ackermann1_in_ggg(T19, T22, T20))
U17_GAG(T19, T20, ackermannc21_out_ga(T19, T22)) → ACKERMANN1_IN_GGG(T19, T22, T20)
ACKERMANN1_IN_GGG(s(s(T19)), 0, T20) → U16_GGG(T19, T20, ackermann21_in_ga(T19, X40))
ACKERMANN1_IN_GGG(s(s(T19)), 0, T20) → ACKERMANN21_IN_GA(T19, X40)
ACKERMANN1_IN_GGG(s(s(T19)), 0, T20) → U17_GGG(T19, T20, ackermannc21_in_ga(T19, T22))
U17_GGG(T19, T20, ackermannc21_out_ga(T19, T22)) → U18_GGG(T19, T20, ackermann1_in_ggg(T19, T22, T20))
U17_GGG(T19, T20, ackermannc21_out_ga(T19, T22)) → ACKERMANN1_IN_GGG(T19, T22, T20)
ACKERMANN1_IN_GGG(s(T68), s(T71), T70) → U19_GGG(T68, T71, T70, ackermann57_in_gga(T68, T71, X182))
ACKERMANN1_IN_GGG(s(T68), s(T71), T70) → ACKERMANN57_IN_GGA(T68, T71, X182)
ACKERMANN57_IN_GGA(T79, 0, X211) → U9_GGA(T79, X211, ackermann27_in_ga(T79, X211))
ACKERMANN57_IN_GGA(T79, 0, X211) → ACKERMANN27_IN_GA(T79, X211)
ACKERMANN57_IN_GGA(T84, s(T86), X229) → U10_GGA(T84, T86, X229, p65_in_ggaa(T84, T86, X228, X229))
ACKERMANN57_IN_GGA(T84, s(T86), X229) → P65_IN_GGAA(T84, T86, X228, X229)
P65_IN_GGAA(T84, T86, X228, X229) → U11_GGAA(T84, T86, X228, X229, ackermann57_in_gga(T84, T86, X228))
P65_IN_GGAA(T84, T86, X228, X229) → ACKERMANN57_IN_GGA(T84, T86, X228)
P65_IN_GGAA(T84, T86, T88, X229) → U12_GGAA(T84, T86, T88, X229, ackermannc57_in_gga(T84, T86, T88))
U12_GGAA(T84, T86, T88, X229, ackermannc57_out_gga(T84, T86, T88)) → U13_GGAA(T84, T86, T88, X229, ackermann68_in_gga(T84, T88, X229))
U12_GGAA(T84, T86, T88, X229, ackermannc57_out_gga(T84, T86, T88)) → ACKERMANN68_IN_GGA(T84, T88, X229)
ACKERMANN68_IN_GGA(s(T101), 0, X265) → U14_GGA(T101, X265, ackermann27_in_ga(T101, X265))
ACKERMANN68_IN_GGA(s(T101), 0, X265) → ACKERMANN27_IN_GA(T101, X265)
ACKERMANN68_IN_GGA(s(T106), s(T108), X283) → U15_GGA(T106, T108, X283, p65_in_ggaa(T106, T108, X282, X283))
ACKERMANN68_IN_GGA(s(T106), s(T108), X283) → P65_IN_GGAA(T106, T108, X282, X283)
ACKERMANN1_IN_GGG(s(T68), s(T71), T70) → U20_GGG(T68, T71, T70, ackermannc57_in_gga(T68, T71, T73))
U20_GGG(T68, T71, T70, ackermannc57_out_gga(T68, T71, T73)) → U21_GGG(T68, T71, T70, ackermann1_in_ggg(T68, T73, T70))
U20_GGG(T68, T71, T70, ackermannc57_out_gga(T68, T71, T73)) → ACKERMANN1_IN_GGG(T68, T73, T70)
ACKERMANN1_IN_GGG(s(T123), s(0), T117) → U22_GGG(T123, T117, ackermann27_in_ga(T123, X319))
ACKERMANN1_IN_GGG(s(T123), s(0), T117) → ACKERMANN27_IN_GA(T123, X319)
ACKERMANN1_IN_GGG(s(T123), s(0), T117) → U23_GGG(T123, T117, ackermannc27_in_ga(T123, T124))
U23_GGG(T123, T117, ackermannc27_out_ga(T123, T124)) → U24_GGG(T123, T117, ackermann1_in_ggg(T123, T124, T117))
U23_GGG(T123, T117, ackermannc27_out_ga(T123, T124)) → ACKERMANN1_IN_GGG(T123, T124, T117)
ACKERMANN1_IN_GGG(s(T131), s(s(T133)), T117) → U25_GGG(T131, T133, T117, ackermann57_in_gga(T131, T133, X340))
ACKERMANN1_IN_GGG(s(T131), s(s(T133)), T117) → ACKERMANN57_IN_GGA(T131, T133, X340)
ACKERMANN1_IN_GGG(s(T131), s(s(T133)), T117) → U26_GGG(T131, T133, T117, ackermannc57_in_gga(T131, T133, T135))
U26_GGG(T131, T133, T117, ackermannc57_out_gga(T131, T133, T135)) → U27_GGG(T131, T133, T117, ackermann68_in_gga(T131, T135, X341))
U26_GGG(T131, T133, T117, ackermannc57_out_gga(T131, T133, T135)) → ACKERMANN68_IN_GGA(T131, T135, X341)
U26_GGG(T131, T133, T117, ackermannc57_out_gga(T131, T133, T135)) → U28_GGG(T131, T133, T117, ackermannc68_in_gga(T131, T135, T139))
U28_GGG(T131, T133, T117, ackermannc68_out_gga(T131, T135, T139)) → U29_GGG(T131, T133, T117, ackermann1_in_ggg(T131, T139, T117))
U28_GGG(T131, T133, T117, ackermannc68_out_gga(T131, T135, T139)) → ACKERMANN1_IN_GGG(T131, T139, T117)
ACKERMANN1_IN_GAG(s(T68), s(T71), T70) → U19_GAG(T68, T71, T70, ackermann57_in_gaa(T68, T71, X182))
ACKERMANN1_IN_GAG(s(T68), s(T71), T70) → ACKERMANN57_IN_GAA(T68, T71, X182)
ACKERMANN57_IN_GAA(T79, 0, X211) → U9_GAA(T79, X211, ackermann27_in_ga(T79, X211))
ACKERMANN57_IN_GAA(T79, 0, X211) → ACKERMANN27_IN_GA(T79, X211)
ACKERMANN57_IN_GAA(T84, s(T86), X229) → U10_GAA(T84, T86, X229, p65_in_gaaa(T84, T86, X228, X229))
ACKERMANN57_IN_GAA(T84, s(T86), X229) → P65_IN_GAAA(T84, T86, X228, X229)
P65_IN_GAAA(T84, T86, X228, X229) → U11_GAAA(T84, T86, X228, X229, ackermann57_in_gaa(T84, T86, X228))
P65_IN_GAAA(T84, T86, X228, X229) → ACKERMANN57_IN_GAA(T84, T86, X228)
P65_IN_GAAA(T84, T86, T88, X229) → U12_GAAA(T84, T86, T88, X229, ackermannc57_in_gaa(T84, T86, T88))
U12_GAAA(T84, T86, T88, X229, ackermannc57_out_gaa(T84, T86, T88)) → U13_GAAA(T84, T86, T88, X229, ackermann68_in_gga(T84, T88, X229))
U12_GAAA(T84, T86, T88, X229, ackermannc57_out_gaa(T84, T86, T88)) → ACKERMANN68_IN_GGA(T84, T88, X229)
ACKERMANN1_IN_GAG(s(T68), s(T71), T70) → U20_GAG(T68, T71, T70, ackermannc57_in_gaa(T68, T71, T73))
U20_GAG(T68, T71, T70, ackermannc57_out_gaa(T68, T71, T73)) → U21_GAG(T68, T71, T70, ackermann1_in_ggg(T68, T73, T70))
U20_GAG(T68, T71, T70, ackermannc57_out_gaa(T68, T71, T73)) → ACKERMANN1_IN_GGG(T68, T73, T70)
ACKERMANN1_IN_GAG(s(T123), s(0), T117) → U22_GAG(T123, T117, ackermann27_in_ga(T123, X319))
ACKERMANN1_IN_GAG(s(T123), s(0), T117) → ACKERMANN27_IN_GA(T123, X319)
ACKERMANN1_IN_GAG(s(T123), s(0), T117) → U23_GAG(T123, T117, ackermannc27_in_ga(T123, T124))
U23_GAG(T123, T117, ackermannc27_out_ga(T123, T124)) → U24_GAG(T123, T117, ackermann1_in_ggg(T123, T124, T117))
U23_GAG(T123, T117, ackermannc27_out_ga(T123, T124)) → ACKERMANN1_IN_GGG(T123, T124, T117)
ACKERMANN1_IN_GAG(s(T131), s(s(T133)), T117) → U25_GAG(T131, T133, T117, ackermann57_in_gaa(T131, T133, X340))
ACKERMANN1_IN_GAG(s(T131), s(s(T133)), T117) → ACKERMANN57_IN_GAA(T131, T133, X340)
ACKERMANN1_IN_GAG(s(T131), s(s(T133)), T117) → U26_GAG(T131, T133, T117, ackermannc57_in_gaa(T131, T133, T135))
U26_GAG(T131, T133, T117, ackermannc57_out_gaa(T131, T133, T135)) → U27_GAG(T131, T133, T117, ackermann68_in_gga(T131, T135, X341))
U26_GAG(T131, T133, T117, ackermannc57_out_gaa(T131, T133, T135)) → ACKERMANN68_IN_GGA(T131, T135, X341)
U26_GAG(T131, T133, T117, ackermannc57_out_gaa(T131, T133, T135)) → U28_GAG(T131, T133, T117, ackermannc68_in_gga(T131, T135, T139))
U28_GAG(T131, T133, T117, ackermannc68_out_gga(T131, T135, T139)) → U29_GAG(T131, T133, T117, ackermann1_in_ggg(T131, T139, T117))
U28_GAG(T131, T133, T117, ackermannc68_out_gga(T131, T135, T139)) → ACKERMANN1_IN_GGG(T131, T139, T117)

The TRS R consists of the following rules:

ackermannc21_in_ga(T28, X73) → U40_ga(T28, X73, ackermannc27_in_ga(T28, X73))
ackermannc27_in_ga(0, s(s(0))) → ackermannc27_out_ga(0, s(s(0)))
ackermannc27_in_ga(s(T32), X97) → U41_ga(T32, X97, ackermannc21_in_ga(T32, T34))
U41_ga(T32, X97, ackermannc21_out_ga(T32, T34)) → U42_ga(T32, X97, ackermannc38_in_gga(T32, T34, X97))
ackermannc38_in_gga(0, T42, s(T42)) → ackermannc38_out_gga(0, T42, s(T42))
ackermannc38_in_gga(s(T47), 0, X133) → U43_gga(T47, X133, ackermannc27_in_ga(T47, X133))
U43_gga(T47, X133, ackermannc27_out_ga(T47, X133)) → ackermannc38_out_gga(s(T47), 0, X133)
ackermannc38_in_gga(s(T52), s(T53), X151) → U44_gga(T52, T53, X151, ackermannc38_in_gga(s(T52), T53, T55))
U44_gga(T52, T53, X151, ackermannc38_out_gga(s(T52), T53, T55)) → U45_gga(T52, T53, X151, ackermannc38_in_gga(T52, T55, X151))
U45_gga(T52, T53, X151, ackermannc38_out_gga(T52, T55, X151)) → ackermannc38_out_gga(s(T52), s(T53), X151)
U42_ga(T32, X97, ackermannc38_out_gga(T32, T34, X97)) → ackermannc27_out_ga(s(T32), X97)
U40_ga(T28, X73, ackermannc27_out_ga(T28, X73)) → ackermannc21_out_ga(T28, X73)
ackermannc57_in_gga(T79, 0, X211) → U46_gga(T79, X211, ackermannc27_in_ga(T79, X211))
U46_gga(T79, X211, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gga(T79, 0, X211)
ackermannc57_in_gga(T84, s(T86), X229) → U47_gga(T84, T86, X229, qc65_in_ggaa(T84, T86, X228, X229))
qc65_in_ggaa(T84, T86, T88, X229) → U48_ggaa(T84, T86, T88, X229, ackermannc57_in_gga(T84, T86, T88))
U48_ggaa(T84, T86, T88, X229, ackermannc57_out_gga(T84, T86, T88)) → U49_ggaa(T84, T86, T88, X229, ackermannc68_in_gga(T84, T88, X229))
ackermannc68_in_gga(0, T96, s(T96)) → ackermannc68_out_gga(0, T96, s(T96))
ackermannc68_in_gga(s(T101), 0, X265) → U50_gga(T101, X265, ackermannc27_in_ga(T101, X265))
U50_gga(T101, X265, ackermannc27_out_ga(T101, X265)) → ackermannc68_out_gga(s(T101), 0, X265)
ackermannc68_in_gga(s(T106), s(T108), X283) → U51_gga(T106, T108, X283, qc65_in_ggaa(T106, T108, X282, X283))
U51_gga(T106, T108, X283, qc65_out_ggaa(T106, T108, X282, X283)) → ackermannc68_out_gga(s(T106), s(T108), X283)
U49_ggaa(T84, T86, T88, X229, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_ggaa(T84, T86, T88, X229)
U47_gga(T84, T86, X229, qc65_out_ggaa(T84, T86, X228, X229)) → ackermannc57_out_gga(T84, s(T86), X229)
ackermannc57_in_gaa(T79, 0, X211) → U46_gaa(T79, X211, ackermannc27_in_ga(T79, X211))
U46_gaa(T79, X211, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gaa(T79, 0, X211)
ackermannc57_in_gaa(T84, s(T86), X229) → U47_gaa(T84, T86, X229, qc65_in_gaaa(T84, T86, X228, X229))
qc65_in_gaaa(T84, T86, T88, X229) → U48_gaaa(T84, T86, T88, X229, ackermannc57_in_gaa(T84, T86, T88))
U48_gaaa(T84, T86, T88, X229, ackermannc57_out_gaa(T84, T86, T88)) → U49_gaaa(T84, T86, T88, X229, ackermannc68_in_gga(T84, T88, X229))
U49_gaaa(T84, T86, T88, X229, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_gaaa(T84, T86, T88, X229)
U47_gaa(T84, T86, X229, qc65_out_gaaa(T84, T86, X228, X229)) → ackermannc57_out_gaa(T84, s(T86), X229)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ackermann21_in_ga(x1, x2)  =  ackermann21_in_ga(x1)
ackermann27_in_ga(x1, x2)  =  ackermann27_in_ga(x1)
ackermannc21_in_ga(x1, x2)  =  ackermannc21_in_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
ackermannc27_in_ga(x1, x2)  =  ackermannc27_in_ga(x1)
0  =  0
ackermannc27_out_ga(x1, x2)  =  ackermannc27_out_ga(x1, x2)
U41_ga(x1, x2, x3)  =  U41_ga(x1, x3)
ackermannc21_out_ga(x1, x2)  =  ackermannc21_out_ga(x1, x2)
U42_ga(x1, x2, x3)  =  U42_ga(x1, x3)
ackermannc38_in_gga(x1, x2, x3)  =  ackermannc38_in_gga(x1, x2)
ackermannc38_out_gga(x1, x2, x3)  =  ackermannc38_out_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x3)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
ackermann38_in_gga(x1, x2, x3)  =  ackermann38_in_gga(x1, x2)
ackermann1_in_ggg(x1, x2, x3)  =  ackermann1_in_ggg(x1, x2, x3)
ackermann57_in_gga(x1, x2, x3)  =  ackermann57_in_gga(x1, x2)
p65_in_ggaa(x1, x2, x3, x4)  =  p65_in_ggaa(x1, x2)
ackermannc57_in_gga(x1, x2, x3)  =  ackermannc57_in_gga(x1, x2)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x3)
ackermannc57_out_gga(x1, x2, x3)  =  ackermannc57_out_gga(x1, x2, x3)
U47_gga(x1, x2, x3, x4)  =  U47_gga(x1, x2, x4)
qc65_in_ggaa(x1, x2, x3, x4)  =  qc65_in_ggaa(x1, x2)
U48_ggaa(x1, x2, x3, x4, x5)  =  U48_ggaa(x1, x2, x5)
U49_ggaa(x1, x2, x3, x4, x5)  =  U49_ggaa(x1, x2, x3, x5)
ackermannc68_in_gga(x1, x2, x3)  =  ackermannc68_in_gga(x1, x2)
ackermannc68_out_gga(x1, x2, x3)  =  ackermannc68_out_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x3)
U51_gga(x1, x2, x3, x4)  =  U51_gga(x1, x2, x4)
qc65_out_ggaa(x1, x2, x3, x4)  =  qc65_out_ggaa(x1, x2, x3, x4)
ackermann68_in_gga(x1, x2, x3)  =  ackermann68_in_gga(x1, x2)
ackermann57_in_gaa(x1, x2, x3)  =  ackermann57_in_gaa(x1)
p65_in_gaaa(x1, x2, x3, x4)  =  p65_in_gaaa(x1)
ackermannc57_in_gaa(x1, x2, x3)  =  ackermannc57_in_gaa(x1)
U46_gaa(x1, x2, x3)  =  U46_gaa(x1, x3)
ackermannc57_out_gaa(x1, x2, x3)  =  ackermannc57_out_gaa(x1, x2, x3)
U47_gaa(x1, x2, x3, x4)  =  U47_gaa(x1, x4)
qc65_in_gaaa(x1, x2, x3, x4)  =  qc65_in_gaaa(x1)
U48_gaaa(x1, x2, x3, x4, x5)  =  U48_gaaa(x1, x5)
U49_gaaa(x1, x2, x3, x4, x5)  =  U49_gaaa(x1, x2, x3, x5)
qc65_out_gaaa(x1, x2, x3, x4)  =  qc65_out_gaaa(x1, x2, x3, x4)
ACKERMANN1_IN_GAG(x1, x2, x3)  =  ACKERMANN1_IN_GAG(x1, x3)
U16_GAG(x1, x2, x3)  =  U16_GAG(x1, x2, x3)
ACKERMANN21_IN_GA(x1, x2)  =  ACKERMANN21_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
ACKERMANN27_IN_GA(x1, x2)  =  ACKERMANN27_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
ACKERMANN38_IN_GGA(x1, x2, x3)  =  ACKERMANN38_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3)  =  U5_GGA(x1, x3)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U17_GAG(x1, x2, x3)  =  U17_GAG(x1, x2, x3)
U18_GAG(x1, x2, x3)  =  U18_GAG(x1, x2, x3)
ACKERMANN1_IN_GGG(x1, x2, x3)  =  ACKERMANN1_IN_GGG(x1, x2, x3)
U16_GGG(x1, x2, x3)  =  U16_GGG(x1, x2, x3)
U17_GGG(x1, x2, x3)  =  U17_GGG(x1, x2, x3)
U18_GGG(x1, x2, x3)  =  U18_GGG(x1, x2, x3)
U19_GGG(x1, x2, x3, x4)  =  U19_GGG(x1, x2, x3, x4)
ACKERMANN57_IN_GGA(x1, x2, x3)  =  ACKERMANN57_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
P65_IN_GGAA(x1, x2, x3, x4)  =  P65_IN_GGAA(x1, x2)
U11_GGAA(x1, x2, x3, x4, x5)  =  U11_GGAA(x1, x2, x5)
U12_GGAA(x1, x2, x3, x4, x5)  =  U12_GGAA(x1, x2, x5)
U13_GGAA(x1, x2, x3, x4, x5)  =  U13_GGAA(x1, x2, x5)
ACKERMANN68_IN_GGA(x1, x2, x3)  =  ACKERMANN68_IN_GGA(x1, x2)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)
U20_GGG(x1, x2, x3, x4)  =  U20_GGG(x1, x2, x3, x4)
U21_GGG(x1, x2, x3, x4)  =  U21_GGG(x1, x2, x3, x4)
U22_GGG(x1, x2, x3)  =  U22_GGG(x1, x2, x3)
U23_GGG(x1, x2, x3)  =  U23_GGG(x1, x2, x3)
U24_GGG(x1, x2, x3)  =  U24_GGG(x1, x2, x3)
U25_GGG(x1, x2, x3, x4)  =  U25_GGG(x1, x2, x3, x4)
U26_GGG(x1, x2, x3, x4)  =  U26_GGG(x1, x2, x3, x4)
U27_GGG(x1, x2, x3, x4)  =  U27_GGG(x1, x2, x3, x4)
U28_GGG(x1, x2, x3, x4)  =  U28_GGG(x1, x2, x3, x4)
U29_GGG(x1, x2, x3, x4)  =  U29_GGG(x1, x2, x3, x4)
U19_GAG(x1, x2, x3, x4)  =  U19_GAG(x1, x3, x4)
ACKERMANN57_IN_GAA(x1, x2, x3)  =  ACKERMANN57_IN_GAA(x1)
U9_GAA(x1, x2, x3)  =  U9_GAA(x1, x3)
U10_GAA(x1, x2, x3, x4)  =  U10_GAA(x1, x4)
P65_IN_GAAA(x1, x2, x3, x4)  =  P65_IN_GAAA(x1)
U11_GAAA(x1, x2, x3, x4, x5)  =  U11_GAAA(x1, x5)
U12_GAAA(x1, x2, x3, x4, x5)  =  U12_GAAA(x1, x5)
U13_GAAA(x1, x2, x3, x4, x5)  =  U13_GAAA(x1, x2, x5)
U20_GAG(x1, x2, x3, x4)  =  U20_GAG(x1, x3, x4)
U21_GAG(x1, x2, x3, x4)  =  U21_GAG(x1, x2, x3, x4)
U22_GAG(x1, x2, x3)  =  U22_GAG(x1, x2, x3)
U23_GAG(x1, x2, x3)  =  U23_GAG(x1, x2, x3)
U24_GAG(x1, x2, x3)  =  U24_GAG(x1, x2, x3)
U25_GAG(x1, x2, x3, x4)  =  U25_GAG(x1, x3, x4)
U26_GAG(x1, x2, x3, x4)  =  U26_GAG(x1, x3, x4)
U27_GAG(x1, x2, x3, x4)  =  U27_GAG(x1, x2, x3, x4)
U28_GAG(x1, x2, x3, x4)  =  U28_GAG(x1, x2, x3, x4)
U29_GAG(x1, x2, x3, x4)  =  U29_GAG(x1, x2, x3, x4)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

ACKERMANN1_IN_GAG(s(s(T19)), 0, T20) → U16_GAG(T19, T20, ackermann21_in_ga(T19, X40))
ACKERMANN1_IN_GAG(s(s(T19)), 0, T20) → ACKERMANN21_IN_GA(T19, X40)
ACKERMANN21_IN_GA(T28, X73) → U1_GA(T28, X73, ackermann27_in_ga(T28, X73))
ACKERMANN21_IN_GA(T28, X73) → ACKERMANN27_IN_GA(T28, X73)
ACKERMANN27_IN_GA(s(T32), X97) → U2_GA(T32, X97, ackermann21_in_ga(T32, X96))
ACKERMANN27_IN_GA(s(T32), X97) → ACKERMANN21_IN_GA(T32, X96)
ACKERMANN27_IN_GA(s(T32), X97) → U3_GA(T32, X97, ackermannc21_in_ga(T32, T34))
U3_GA(T32, X97, ackermannc21_out_ga(T32, T34)) → U4_GA(T32, X97, ackermann38_in_gga(T32, T34, X97))
U3_GA(T32, X97, ackermannc21_out_ga(T32, T34)) → ACKERMANN38_IN_GGA(T32, T34, X97)
ACKERMANN38_IN_GGA(s(T47), 0, X133) → U5_GGA(T47, X133, ackermann27_in_ga(T47, X133))
ACKERMANN38_IN_GGA(s(T47), 0, X133) → ACKERMANN27_IN_GA(T47, X133)
ACKERMANN38_IN_GGA(s(T52), s(T53), X151) → U6_GGA(T52, T53, X151, ackermann38_in_gga(s(T52), T53, X150))
ACKERMANN38_IN_GGA(s(T52), s(T53), X151) → ACKERMANN38_IN_GGA(s(T52), T53, X150)
ACKERMANN38_IN_GGA(s(T52), s(T53), X151) → U7_GGA(T52, T53, X151, ackermannc38_in_gga(s(T52), T53, T55))
U7_GGA(T52, T53, X151, ackermannc38_out_gga(s(T52), T53, T55)) → U8_GGA(T52, T53, X151, ackermann38_in_gga(T52, T55, X151))
U7_GGA(T52, T53, X151, ackermannc38_out_gga(s(T52), T53, T55)) → ACKERMANN38_IN_GGA(T52, T55, X151)
ACKERMANN1_IN_GAG(s(s(T19)), 0, T20) → U17_GAG(T19, T20, ackermannc21_in_ga(T19, T22))
U17_GAG(T19, T20, ackermannc21_out_ga(T19, T22)) → U18_GAG(T19, T20, ackermann1_in_ggg(T19, T22, T20))
U17_GAG(T19, T20, ackermannc21_out_ga(T19, T22)) → ACKERMANN1_IN_GGG(T19, T22, T20)
ACKERMANN1_IN_GGG(s(s(T19)), 0, T20) → U16_GGG(T19, T20, ackermann21_in_ga(T19, X40))
ACKERMANN1_IN_GGG(s(s(T19)), 0, T20) → ACKERMANN21_IN_GA(T19, X40)
ACKERMANN1_IN_GGG(s(s(T19)), 0, T20) → U17_GGG(T19, T20, ackermannc21_in_ga(T19, T22))
U17_GGG(T19, T20, ackermannc21_out_ga(T19, T22)) → U18_GGG(T19, T20, ackermann1_in_ggg(T19, T22, T20))
U17_GGG(T19, T20, ackermannc21_out_ga(T19, T22)) → ACKERMANN1_IN_GGG(T19, T22, T20)
ACKERMANN1_IN_GGG(s(T68), s(T71), T70) → U19_GGG(T68, T71, T70, ackermann57_in_gga(T68, T71, X182))
ACKERMANN1_IN_GGG(s(T68), s(T71), T70) → ACKERMANN57_IN_GGA(T68, T71, X182)
ACKERMANN57_IN_GGA(T79, 0, X211) → U9_GGA(T79, X211, ackermann27_in_ga(T79, X211))
ACKERMANN57_IN_GGA(T79, 0, X211) → ACKERMANN27_IN_GA(T79, X211)
ACKERMANN57_IN_GGA(T84, s(T86), X229) → U10_GGA(T84, T86, X229, p65_in_ggaa(T84, T86, X228, X229))
ACKERMANN57_IN_GGA(T84, s(T86), X229) → P65_IN_GGAA(T84, T86, X228, X229)
P65_IN_GGAA(T84, T86, X228, X229) → U11_GGAA(T84, T86, X228, X229, ackermann57_in_gga(T84, T86, X228))
P65_IN_GGAA(T84, T86, X228, X229) → ACKERMANN57_IN_GGA(T84, T86, X228)
P65_IN_GGAA(T84, T86, T88, X229) → U12_GGAA(T84, T86, T88, X229, ackermannc57_in_gga(T84, T86, T88))
U12_GGAA(T84, T86, T88, X229, ackermannc57_out_gga(T84, T86, T88)) → U13_GGAA(T84, T86, T88, X229, ackermann68_in_gga(T84, T88, X229))
U12_GGAA(T84, T86, T88, X229, ackermannc57_out_gga(T84, T86, T88)) → ACKERMANN68_IN_GGA(T84, T88, X229)
ACKERMANN68_IN_GGA(s(T101), 0, X265) → U14_GGA(T101, X265, ackermann27_in_ga(T101, X265))
ACKERMANN68_IN_GGA(s(T101), 0, X265) → ACKERMANN27_IN_GA(T101, X265)
ACKERMANN68_IN_GGA(s(T106), s(T108), X283) → U15_GGA(T106, T108, X283, p65_in_ggaa(T106, T108, X282, X283))
ACKERMANN68_IN_GGA(s(T106), s(T108), X283) → P65_IN_GGAA(T106, T108, X282, X283)
ACKERMANN1_IN_GGG(s(T68), s(T71), T70) → U20_GGG(T68, T71, T70, ackermannc57_in_gga(T68, T71, T73))
U20_GGG(T68, T71, T70, ackermannc57_out_gga(T68, T71, T73)) → U21_GGG(T68, T71, T70, ackermann1_in_ggg(T68, T73, T70))
U20_GGG(T68, T71, T70, ackermannc57_out_gga(T68, T71, T73)) → ACKERMANN1_IN_GGG(T68, T73, T70)
ACKERMANN1_IN_GGG(s(T123), s(0), T117) → U22_GGG(T123, T117, ackermann27_in_ga(T123, X319))
ACKERMANN1_IN_GGG(s(T123), s(0), T117) → ACKERMANN27_IN_GA(T123, X319)
ACKERMANN1_IN_GGG(s(T123), s(0), T117) → U23_GGG(T123, T117, ackermannc27_in_ga(T123, T124))
U23_GGG(T123, T117, ackermannc27_out_ga(T123, T124)) → U24_GGG(T123, T117, ackermann1_in_ggg(T123, T124, T117))
U23_GGG(T123, T117, ackermannc27_out_ga(T123, T124)) → ACKERMANN1_IN_GGG(T123, T124, T117)
ACKERMANN1_IN_GGG(s(T131), s(s(T133)), T117) → U25_GGG(T131, T133, T117, ackermann57_in_gga(T131, T133, X340))
ACKERMANN1_IN_GGG(s(T131), s(s(T133)), T117) → ACKERMANN57_IN_GGA(T131, T133, X340)
ACKERMANN1_IN_GGG(s(T131), s(s(T133)), T117) → U26_GGG(T131, T133, T117, ackermannc57_in_gga(T131, T133, T135))
U26_GGG(T131, T133, T117, ackermannc57_out_gga(T131, T133, T135)) → U27_GGG(T131, T133, T117, ackermann68_in_gga(T131, T135, X341))
U26_GGG(T131, T133, T117, ackermannc57_out_gga(T131, T133, T135)) → ACKERMANN68_IN_GGA(T131, T135, X341)
U26_GGG(T131, T133, T117, ackermannc57_out_gga(T131, T133, T135)) → U28_GGG(T131, T133, T117, ackermannc68_in_gga(T131, T135, T139))
U28_GGG(T131, T133, T117, ackermannc68_out_gga(T131, T135, T139)) → U29_GGG(T131, T133, T117, ackermann1_in_ggg(T131, T139, T117))
U28_GGG(T131, T133, T117, ackermannc68_out_gga(T131, T135, T139)) → ACKERMANN1_IN_GGG(T131, T139, T117)
ACKERMANN1_IN_GAG(s(T68), s(T71), T70) → U19_GAG(T68, T71, T70, ackermann57_in_gaa(T68, T71, X182))
ACKERMANN1_IN_GAG(s(T68), s(T71), T70) → ACKERMANN57_IN_GAA(T68, T71, X182)
ACKERMANN57_IN_GAA(T79, 0, X211) → U9_GAA(T79, X211, ackermann27_in_ga(T79, X211))
ACKERMANN57_IN_GAA(T79, 0, X211) → ACKERMANN27_IN_GA(T79, X211)
ACKERMANN57_IN_GAA(T84, s(T86), X229) → U10_GAA(T84, T86, X229, p65_in_gaaa(T84, T86, X228, X229))
ACKERMANN57_IN_GAA(T84, s(T86), X229) → P65_IN_GAAA(T84, T86, X228, X229)
P65_IN_GAAA(T84, T86, X228, X229) → U11_GAAA(T84, T86, X228, X229, ackermann57_in_gaa(T84, T86, X228))
P65_IN_GAAA(T84, T86, X228, X229) → ACKERMANN57_IN_GAA(T84, T86, X228)
P65_IN_GAAA(T84, T86, T88, X229) → U12_GAAA(T84, T86, T88, X229, ackermannc57_in_gaa(T84, T86, T88))
U12_GAAA(T84, T86, T88, X229, ackermannc57_out_gaa(T84, T86, T88)) → U13_GAAA(T84, T86, T88, X229, ackermann68_in_gga(T84, T88, X229))
U12_GAAA(T84, T86, T88, X229, ackermannc57_out_gaa(T84, T86, T88)) → ACKERMANN68_IN_GGA(T84, T88, X229)
ACKERMANN1_IN_GAG(s(T68), s(T71), T70) → U20_GAG(T68, T71, T70, ackermannc57_in_gaa(T68, T71, T73))
U20_GAG(T68, T71, T70, ackermannc57_out_gaa(T68, T71, T73)) → U21_GAG(T68, T71, T70, ackermann1_in_ggg(T68, T73, T70))
U20_GAG(T68, T71, T70, ackermannc57_out_gaa(T68, T71, T73)) → ACKERMANN1_IN_GGG(T68, T73, T70)
ACKERMANN1_IN_GAG(s(T123), s(0), T117) → U22_GAG(T123, T117, ackermann27_in_ga(T123, X319))
ACKERMANN1_IN_GAG(s(T123), s(0), T117) → ACKERMANN27_IN_GA(T123, X319)
ACKERMANN1_IN_GAG(s(T123), s(0), T117) → U23_GAG(T123, T117, ackermannc27_in_ga(T123, T124))
U23_GAG(T123, T117, ackermannc27_out_ga(T123, T124)) → U24_GAG(T123, T117, ackermann1_in_ggg(T123, T124, T117))
U23_GAG(T123, T117, ackermannc27_out_ga(T123, T124)) → ACKERMANN1_IN_GGG(T123, T124, T117)
ACKERMANN1_IN_GAG(s(T131), s(s(T133)), T117) → U25_GAG(T131, T133, T117, ackermann57_in_gaa(T131, T133, X340))
ACKERMANN1_IN_GAG(s(T131), s(s(T133)), T117) → ACKERMANN57_IN_GAA(T131, T133, X340)
ACKERMANN1_IN_GAG(s(T131), s(s(T133)), T117) → U26_GAG(T131, T133, T117, ackermannc57_in_gaa(T131, T133, T135))
U26_GAG(T131, T133, T117, ackermannc57_out_gaa(T131, T133, T135)) → U27_GAG(T131, T133, T117, ackermann68_in_gga(T131, T135, X341))
U26_GAG(T131, T133, T117, ackermannc57_out_gaa(T131, T133, T135)) → ACKERMANN68_IN_GGA(T131, T135, X341)
U26_GAG(T131, T133, T117, ackermannc57_out_gaa(T131, T133, T135)) → U28_GAG(T131, T133, T117, ackermannc68_in_gga(T131, T135, T139))
U28_GAG(T131, T133, T117, ackermannc68_out_gga(T131, T135, T139)) → U29_GAG(T131, T133, T117, ackermann1_in_ggg(T131, T139, T117))
U28_GAG(T131, T133, T117, ackermannc68_out_gga(T131, T135, T139)) → ACKERMANN1_IN_GGG(T131, T139, T117)

The TRS R consists of the following rules:

ackermannc21_in_ga(T28, X73) → U40_ga(T28, X73, ackermannc27_in_ga(T28, X73))
ackermannc27_in_ga(0, s(s(0))) → ackermannc27_out_ga(0, s(s(0)))
ackermannc27_in_ga(s(T32), X97) → U41_ga(T32, X97, ackermannc21_in_ga(T32, T34))
U41_ga(T32, X97, ackermannc21_out_ga(T32, T34)) → U42_ga(T32, X97, ackermannc38_in_gga(T32, T34, X97))
ackermannc38_in_gga(0, T42, s(T42)) → ackermannc38_out_gga(0, T42, s(T42))
ackermannc38_in_gga(s(T47), 0, X133) → U43_gga(T47, X133, ackermannc27_in_ga(T47, X133))
U43_gga(T47, X133, ackermannc27_out_ga(T47, X133)) → ackermannc38_out_gga(s(T47), 0, X133)
ackermannc38_in_gga(s(T52), s(T53), X151) → U44_gga(T52, T53, X151, ackermannc38_in_gga(s(T52), T53, T55))
U44_gga(T52, T53, X151, ackermannc38_out_gga(s(T52), T53, T55)) → U45_gga(T52, T53, X151, ackermannc38_in_gga(T52, T55, X151))
U45_gga(T52, T53, X151, ackermannc38_out_gga(T52, T55, X151)) → ackermannc38_out_gga(s(T52), s(T53), X151)
U42_ga(T32, X97, ackermannc38_out_gga(T32, T34, X97)) → ackermannc27_out_ga(s(T32), X97)
U40_ga(T28, X73, ackermannc27_out_ga(T28, X73)) → ackermannc21_out_ga(T28, X73)
ackermannc57_in_gga(T79, 0, X211) → U46_gga(T79, X211, ackermannc27_in_ga(T79, X211))
U46_gga(T79, X211, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gga(T79, 0, X211)
ackermannc57_in_gga(T84, s(T86), X229) → U47_gga(T84, T86, X229, qc65_in_ggaa(T84, T86, X228, X229))
qc65_in_ggaa(T84, T86, T88, X229) → U48_ggaa(T84, T86, T88, X229, ackermannc57_in_gga(T84, T86, T88))
U48_ggaa(T84, T86, T88, X229, ackermannc57_out_gga(T84, T86, T88)) → U49_ggaa(T84, T86, T88, X229, ackermannc68_in_gga(T84, T88, X229))
ackermannc68_in_gga(0, T96, s(T96)) → ackermannc68_out_gga(0, T96, s(T96))
ackermannc68_in_gga(s(T101), 0, X265) → U50_gga(T101, X265, ackermannc27_in_ga(T101, X265))
U50_gga(T101, X265, ackermannc27_out_ga(T101, X265)) → ackermannc68_out_gga(s(T101), 0, X265)
ackermannc68_in_gga(s(T106), s(T108), X283) → U51_gga(T106, T108, X283, qc65_in_ggaa(T106, T108, X282, X283))
U51_gga(T106, T108, X283, qc65_out_ggaa(T106, T108, X282, X283)) → ackermannc68_out_gga(s(T106), s(T108), X283)
U49_ggaa(T84, T86, T88, X229, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_ggaa(T84, T86, T88, X229)
U47_gga(T84, T86, X229, qc65_out_ggaa(T84, T86, X228, X229)) → ackermannc57_out_gga(T84, s(T86), X229)
ackermannc57_in_gaa(T79, 0, X211) → U46_gaa(T79, X211, ackermannc27_in_ga(T79, X211))
U46_gaa(T79, X211, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gaa(T79, 0, X211)
ackermannc57_in_gaa(T84, s(T86), X229) → U47_gaa(T84, T86, X229, qc65_in_gaaa(T84, T86, X228, X229))
qc65_in_gaaa(T84, T86, T88, X229) → U48_gaaa(T84, T86, T88, X229, ackermannc57_in_gaa(T84, T86, T88))
U48_gaaa(T84, T86, T88, X229, ackermannc57_out_gaa(T84, T86, T88)) → U49_gaaa(T84, T86, T88, X229, ackermannc68_in_gga(T84, T88, X229))
U49_gaaa(T84, T86, T88, X229, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_gaaa(T84, T86, T88, X229)
U47_gaa(T84, T86, X229, qc65_out_gaaa(T84, T86, X228, X229)) → ackermannc57_out_gaa(T84, s(T86), X229)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ackermann21_in_ga(x1, x2)  =  ackermann21_in_ga(x1)
ackermann27_in_ga(x1, x2)  =  ackermann27_in_ga(x1)
ackermannc21_in_ga(x1, x2)  =  ackermannc21_in_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
ackermannc27_in_ga(x1, x2)  =  ackermannc27_in_ga(x1)
0  =  0
ackermannc27_out_ga(x1, x2)  =  ackermannc27_out_ga(x1, x2)
U41_ga(x1, x2, x3)  =  U41_ga(x1, x3)
ackermannc21_out_ga(x1, x2)  =  ackermannc21_out_ga(x1, x2)
U42_ga(x1, x2, x3)  =  U42_ga(x1, x3)
ackermannc38_in_gga(x1, x2, x3)  =  ackermannc38_in_gga(x1, x2)
ackermannc38_out_gga(x1, x2, x3)  =  ackermannc38_out_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x3)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
ackermann38_in_gga(x1, x2, x3)  =  ackermann38_in_gga(x1, x2)
ackermann1_in_ggg(x1, x2, x3)  =  ackermann1_in_ggg(x1, x2, x3)
ackermann57_in_gga(x1, x2, x3)  =  ackermann57_in_gga(x1, x2)
p65_in_ggaa(x1, x2, x3, x4)  =  p65_in_ggaa(x1, x2)
ackermannc57_in_gga(x1, x2, x3)  =  ackermannc57_in_gga(x1, x2)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x3)
ackermannc57_out_gga(x1, x2, x3)  =  ackermannc57_out_gga(x1, x2, x3)
U47_gga(x1, x2, x3, x4)  =  U47_gga(x1, x2, x4)
qc65_in_ggaa(x1, x2, x3, x4)  =  qc65_in_ggaa(x1, x2)
U48_ggaa(x1, x2, x3, x4, x5)  =  U48_ggaa(x1, x2, x5)
U49_ggaa(x1, x2, x3, x4, x5)  =  U49_ggaa(x1, x2, x3, x5)
ackermannc68_in_gga(x1, x2, x3)  =  ackermannc68_in_gga(x1, x2)
ackermannc68_out_gga(x1, x2, x3)  =  ackermannc68_out_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x3)
U51_gga(x1, x2, x3, x4)  =  U51_gga(x1, x2, x4)
qc65_out_ggaa(x1, x2, x3, x4)  =  qc65_out_ggaa(x1, x2, x3, x4)
ackermann68_in_gga(x1, x2, x3)  =  ackermann68_in_gga(x1, x2)
ackermann57_in_gaa(x1, x2, x3)  =  ackermann57_in_gaa(x1)
p65_in_gaaa(x1, x2, x3, x4)  =  p65_in_gaaa(x1)
ackermannc57_in_gaa(x1, x2, x3)  =  ackermannc57_in_gaa(x1)
U46_gaa(x1, x2, x3)  =  U46_gaa(x1, x3)
ackermannc57_out_gaa(x1, x2, x3)  =  ackermannc57_out_gaa(x1, x2, x3)
U47_gaa(x1, x2, x3, x4)  =  U47_gaa(x1, x4)
qc65_in_gaaa(x1, x2, x3, x4)  =  qc65_in_gaaa(x1)
U48_gaaa(x1, x2, x3, x4, x5)  =  U48_gaaa(x1, x5)
U49_gaaa(x1, x2, x3, x4, x5)  =  U49_gaaa(x1, x2, x3, x5)
qc65_out_gaaa(x1, x2, x3, x4)  =  qc65_out_gaaa(x1, x2, x3, x4)
ACKERMANN1_IN_GAG(x1, x2, x3)  =  ACKERMANN1_IN_GAG(x1, x3)
U16_GAG(x1, x2, x3)  =  U16_GAG(x1, x2, x3)
ACKERMANN21_IN_GA(x1, x2)  =  ACKERMANN21_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
ACKERMANN27_IN_GA(x1, x2)  =  ACKERMANN27_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
ACKERMANN38_IN_GGA(x1, x2, x3)  =  ACKERMANN38_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3)  =  U5_GGA(x1, x3)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U17_GAG(x1, x2, x3)  =  U17_GAG(x1, x2, x3)
U18_GAG(x1, x2, x3)  =  U18_GAG(x1, x2, x3)
ACKERMANN1_IN_GGG(x1, x2, x3)  =  ACKERMANN1_IN_GGG(x1, x2, x3)
U16_GGG(x1, x2, x3)  =  U16_GGG(x1, x2, x3)
U17_GGG(x1, x2, x3)  =  U17_GGG(x1, x2, x3)
U18_GGG(x1, x2, x3)  =  U18_GGG(x1, x2, x3)
U19_GGG(x1, x2, x3, x4)  =  U19_GGG(x1, x2, x3, x4)
ACKERMANN57_IN_GGA(x1, x2, x3)  =  ACKERMANN57_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
P65_IN_GGAA(x1, x2, x3, x4)  =  P65_IN_GGAA(x1, x2)
U11_GGAA(x1, x2, x3, x4, x5)  =  U11_GGAA(x1, x2, x5)
U12_GGAA(x1, x2, x3, x4, x5)  =  U12_GGAA(x1, x2, x5)
U13_GGAA(x1, x2, x3, x4, x5)  =  U13_GGAA(x1, x2, x5)
ACKERMANN68_IN_GGA(x1, x2, x3)  =  ACKERMANN68_IN_GGA(x1, x2)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)
U20_GGG(x1, x2, x3, x4)  =  U20_GGG(x1, x2, x3, x4)
U21_GGG(x1, x2, x3, x4)  =  U21_GGG(x1, x2, x3, x4)
U22_GGG(x1, x2, x3)  =  U22_GGG(x1, x2, x3)
U23_GGG(x1, x2, x3)  =  U23_GGG(x1, x2, x3)
U24_GGG(x1, x2, x3)  =  U24_GGG(x1, x2, x3)
U25_GGG(x1, x2, x3, x4)  =  U25_GGG(x1, x2, x3, x4)
U26_GGG(x1, x2, x3, x4)  =  U26_GGG(x1, x2, x3, x4)
U27_GGG(x1, x2, x3, x4)  =  U27_GGG(x1, x2, x3, x4)
U28_GGG(x1, x2, x3, x4)  =  U28_GGG(x1, x2, x3, x4)
U29_GGG(x1, x2, x3, x4)  =  U29_GGG(x1, x2, x3, x4)
U19_GAG(x1, x2, x3, x4)  =  U19_GAG(x1, x3, x4)
ACKERMANN57_IN_GAA(x1, x2, x3)  =  ACKERMANN57_IN_GAA(x1)
U9_GAA(x1, x2, x3)  =  U9_GAA(x1, x3)
U10_GAA(x1, x2, x3, x4)  =  U10_GAA(x1, x4)
P65_IN_GAAA(x1, x2, x3, x4)  =  P65_IN_GAAA(x1)
U11_GAAA(x1, x2, x3, x4, x5)  =  U11_GAAA(x1, x5)
U12_GAAA(x1, x2, x3, x4, x5)  =  U12_GAAA(x1, x5)
U13_GAAA(x1, x2, x3, x4, x5)  =  U13_GAAA(x1, x2, x5)
U20_GAG(x1, x2, x3, x4)  =  U20_GAG(x1, x3, x4)
U21_GAG(x1, x2, x3, x4)  =  U21_GAG(x1, x2, x3, x4)
U22_GAG(x1, x2, x3)  =  U22_GAG(x1, x2, x3)
U23_GAG(x1, x2, x3)  =  U23_GAG(x1, x2, x3)
U24_GAG(x1, x2, x3)  =  U24_GAG(x1, x2, x3)
U25_GAG(x1, x2, x3, x4)  =  U25_GAG(x1, x3, x4)
U26_GAG(x1, x2, x3, x4)  =  U26_GAG(x1, x3, x4)
U27_GAG(x1, x2, x3, x4)  =  U27_GAG(x1, x2, x3, x4)
U28_GAG(x1, x2, x3, x4)  =  U28_GAG(x1, x2, x3, x4)
U29_GAG(x1, x2, x3, x4)  =  U29_GAG(x1, x2, x3, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 58 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

ACKERMANN21_IN_GA(T28, X73) → ACKERMANN27_IN_GA(T28, X73)
ACKERMANN27_IN_GA(s(T32), X97) → ACKERMANN21_IN_GA(T32, X96)
ACKERMANN27_IN_GA(s(T32), X97) → U3_GA(T32, X97, ackermannc21_in_ga(T32, T34))
U3_GA(T32, X97, ackermannc21_out_ga(T32, T34)) → ACKERMANN38_IN_GGA(T32, T34, X97)
ACKERMANN38_IN_GGA(s(T47), 0, X133) → ACKERMANN27_IN_GA(T47, X133)
ACKERMANN38_IN_GGA(s(T52), s(T53), X151) → ACKERMANN38_IN_GGA(s(T52), T53, X150)
ACKERMANN38_IN_GGA(s(T52), s(T53), X151) → U7_GGA(T52, T53, X151, ackermannc38_in_gga(s(T52), T53, T55))
U7_GGA(T52, T53, X151, ackermannc38_out_gga(s(T52), T53, T55)) → ACKERMANN38_IN_GGA(T52, T55, X151)

The TRS R consists of the following rules:

ackermannc21_in_ga(T28, X73) → U40_ga(T28, X73, ackermannc27_in_ga(T28, X73))
ackermannc27_in_ga(0, s(s(0))) → ackermannc27_out_ga(0, s(s(0)))
ackermannc27_in_ga(s(T32), X97) → U41_ga(T32, X97, ackermannc21_in_ga(T32, T34))
U41_ga(T32, X97, ackermannc21_out_ga(T32, T34)) → U42_ga(T32, X97, ackermannc38_in_gga(T32, T34, X97))
ackermannc38_in_gga(0, T42, s(T42)) → ackermannc38_out_gga(0, T42, s(T42))
ackermannc38_in_gga(s(T47), 0, X133) → U43_gga(T47, X133, ackermannc27_in_ga(T47, X133))
U43_gga(T47, X133, ackermannc27_out_ga(T47, X133)) → ackermannc38_out_gga(s(T47), 0, X133)
ackermannc38_in_gga(s(T52), s(T53), X151) → U44_gga(T52, T53, X151, ackermannc38_in_gga(s(T52), T53, T55))
U44_gga(T52, T53, X151, ackermannc38_out_gga(s(T52), T53, T55)) → U45_gga(T52, T53, X151, ackermannc38_in_gga(T52, T55, X151))
U45_gga(T52, T53, X151, ackermannc38_out_gga(T52, T55, X151)) → ackermannc38_out_gga(s(T52), s(T53), X151)
U42_ga(T32, X97, ackermannc38_out_gga(T32, T34, X97)) → ackermannc27_out_ga(s(T32), X97)
U40_ga(T28, X73, ackermannc27_out_ga(T28, X73)) → ackermannc21_out_ga(T28, X73)
ackermannc57_in_gga(T79, 0, X211) → U46_gga(T79, X211, ackermannc27_in_ga(T79, X211))
U46_gga(T79, X211, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gga(T79, 0, X211)
ackermannc57_in_gga(T84, s(T86), X229) → U47_gga(T84, T86, X229, qc65_in_ggaa(T84, T86, X228, X229))
qc65_in_ggaa(T84, T86, T88, X229) → U48_ggaa(T84, T86, T88, X229, ackermannc57_in_gga(T84, T86, T88))
U48_ggaa(T84, T86, T88, X229, ackermannc57_out_gga(T84, T86, T88)) → U49_ggaa(T84, T86, T88, X229, ackermannc68_in_gga(T84, T88, X229))
ackermannc68_in_gga(0, T96, s(T96)) → ackermannc68_out_gga(0, T96, s(T96))
ackermannc68_in_gga(s(T101), 0, X265) → U50_gga(T101, X265, ackermannc27_in_ga(T101, X265))
U50_gga(T101, X265, ackermannc27_out_ga(T101, X265)) → ackermannc68_out_gga(s(T101), 0, X265)
ackermannc68_in_gga(s(T106), s(T108), X283) → U51_gga(T106, T108, X283, qc65_in_ggaa(T106, T108, X282, X283))
U51_gga(T106, T108, X283, qc65_out_ggaa(T106, T108, X282, X283)) → ackermannc68_out_gga(s(T106), s(T108), X283)
U49_ggaa(T84, T86, T88, X229, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_ggaa(T84, T86, T88, X229)
U47_gga(T84, T86, X229, qc65_out_ggaa(T84, T86, X228, X229)) → ackermannc57_out_gga(T84, s(T86), X229)
ackermannc57_in_gaa(T79, 0, X211) → U46_gaa(T79, X211, ackermannc27_in_ga(T79, X211))
U46_gaa(T79, X211, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gaa(T79, 0, X211)
ackermannc57_in_gaa(T84, s(T86), X229) → U47_gaa(T84, T86, X229, qc65_in_gaaa(T84, T86, X228, X229))
qc65_in_gaaa(T84, T86, T88, X229) → U48_gaaa(T84, T86, T88, X229, ackermannc57_in_gaa(T84, T86, T88))
U48_gaaa(T84, T86, T88, X229, ackermannc57_out_gaa(T84, T86, T88)) → U49_gaaa(T84, T86, T88, X229, ackermannc68_in_gga(T84, T88, X229))
U49_gaaa(T84, T86, T88, X229, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_gaaa(T84, T86, T88, X229)
U47_gaa(T84, T86, X229, qc65_out_gaaa(T84, T86, X228, X229)) → ackermannc57_out_gaa(T84, s(T86), X229)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ackermannc21_in_ga(x1, x2)  =  ackermannc21_in_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
ackermannc27_in_ga(x1, x2)  =  ackermannc27_in_ga(x1)
0  =  0
ackermannc27_out_ga(x1, x2)  =  ackermannc27_out_ga(x1, x2)
U41_ga(x1, x2, x3)  =  U41_ga(x1, x3)
ackermannc21_out_ga(x1, x2)  =  ackermannc21_out_ga(x1, x2)
U42_ga(x1, x2, x3)  =  U42_ga(x1, x3)
ackermannc38_in_gga(x1, x2, x3)  =  ackermannc38_in_gga(x1, x2)
ackermannc38_out_gga(x1, x2, x3)  =  ackermannc38_out_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x3)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
ackermannc57_in_gga(x1, x2, x3)  =  ackermannc57_in_gga(x1, x2)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x3)
ackermannc57_out_gga(x1, x2, x3)  =  ackermannc57_out_gga(x1, x2, x3)
U47_gga(x1, x2, x3, x4)  =  U47_gga(x1, x2, x4)
qc65_in_ggaa(x1, x2, x3, x4)  =  qc65_in_ggaa(x1, x2)
U48_ggaa(x1, x2, x3, x4, x5)  =  U48_ggaa(x1, x2, x5)
U49_ggaa(x1, x2, x3, x4, x5)  =  U49_ggaa(x1, x2, x3, x5)
ackermannc68_in_gga(x1, x2, x3)  =  ackermannc68_in_gga(x1, x2)
ackermannc68_out_gga(x1, x2, x3)  =  ackermannc68_out_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x3)
U51_gga(x1, x2, x3, x4)  =  U51_gga(x1, x2, x4)
qc65_out_ggaa(x1, x2, x3, x4)  =  qc65_out_ggaa(x1, x2, x3, x4)
ackermannc57_in_gaa(x1, x2, x3)  =  ackermannc57_in_gaa(x1)
U46_gaa(x1, x2, x3)  =  U46_gaa(x1, x3)
ackermannc57_out_gaa(x1, x2, x3)  =  ackermannc57_out_gaa(x1, x2, x3)
U47_gaa(x1, x2, x3, x4)  =  U47_gaa(x1, x4)
qc65_in_gaaa(x1, x2, x3, x4)  =  qc65_in_gaaa(x1)
U48_gaaa(x1, x2, x3, x4, x5)  =  U48_gaaa(x1, x5)
U49_gaaa(x1, x2, x3, x4, x5)  =  U49_gaaa(x1, x2, x3, x5)
qc65_out_gaaa(x1, x2, x3, x4)  =  qc65_out_gaaa(x1, x2, x3, x4)
ACKERMANN21_IN_GA(x1, x2)  =  ACKERMANN21_IN_GA(x1)
ACKERMANN27_IN_GA(x1, x2)  =  ACKERMANN27_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
ACKERMANN38_IN_GGA(x1, x2, x3)  =  ACKERMANN38_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

ACKERMANN21_IN_GA(T28, X73) → ACKERMANN27_IN_GA(T28, X73)
ACKERMANN27_IN_GA(s(T32), X97) → ACKERMANN21_IN_GA(T32, X96)
ACKERMANN27_IN_GA(s(T32), X97) → U3_GA(T32, X97, ackermannc21_in_ga(T32, T34))
U3_GA(T32, X97, ackermannc21_out_ga(T32, T34)) → ACKERMANN38_IN_GGA(T32, T34, X97)
ACKERMANN38_IN_GGA(s(T47), 0, X133) → ACKERMANN27_IN_GA(T47, X133)
ACKERMANN38_IN_GGA(s(T52), s(T53), X151) → ACKERMANN38_IN_GGA(s(T52), T53, X150)
ACKERMANN38_IN_GGA(s(T52), s(T53), X151) → U7_GGA(T52, T53, X151, ackermannc38_in_gga(s(T52), T53, T55))
U7_GGA(T52, T53, X151, ackermannc38_out_gga(s(T52), T53, T55)) → ACKERMANN38_IN_GGA(T52, T55, X151)

The TRS R consists of the following rules:

ackermannc21_in_ga(T28, X73) → U40_ga(T28, X73, ackermannc27_in_ga(T28, X73))
ackermannc38_in_gga(s(T47), 0, X133) → U43_gga(T47, X133, ackermannc27_in_ga(T47, X133))
ackermannc38_in_gga(s(T52), s(T53), X151) → U44_gga(T52, T53, X151, ackermannc38_in_gga(s(T52), T53, T55))
U40_ga(T28, X73, ackermannc27_out_ga(T28, X73)) → ackermannc21_out_ga(T28, X73)
U43_gga(T47, X133, ackermannc27_out_ga(T47, X133)) → ackermannc38_out_gga(s(T47), 0, X133)
U44_gga(T52, T53, X151, ackermannc38_out_gga(s(T52), T53, T55)) → U45_gga(T52, T53, X151, ackermannc38_in_gga(T52, T55, X151))
ackermannc27_in_ga(0, s(s(0))) → ackermannc27_out_ga(0, s(s(0)))
ackermannc27_in_ga(s(T32), X97) → U41_ga(T32, X97, ackermannc21_in_ga(T32, T34))
U45_gga(T52, T53, X151, ackermannc38_out_gga(T52, T55, X151)) → ackermannc38_out_gga(s(T52), s(T53), X151)
U41_ga(T32, X97, ackermannc21_out_ga(T32, T34)) → U42_ga(T32, X97, ackermannc38_in_gga(T32, T34, X97))
ackermannc38_in_gga(0, T42, s(T42)) → ackermannc38_out_gga(0, T42, s(T42))
U42_ga(T32, X97, ackermannc38_out_gga(T32, T34, X97)) → ackermannc27_out_ga(s(T32), X97)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ackermannc21_in_ga(x1, x2)  =  ackermannc21_in_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
ackermannc27_in_ga(x1, x2)  =  ackermannc27_in_ga(x1)
0  =  0
ackermannc27_out_ga(x1, x2)  =  ackermannc27_out_ga(x1, x2)
U41_ga(x1, x2, x3)  =  U41_ga(x1, x3)
ackermannc21_out_ga(x1, x2)  =  ackermannc21_out_ga(x1, x2)
U42_ga(x1, x2, x3)  =  U42_ga(x1, x3)
ackermannc38_in_gga(x1, x2, x3)  =  ackermannc38_in_gga(x1, x2)
ackermannc38_out_gga(x1, x2, x3)  =  ackermannc38_out_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x3)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
ACKERMANN21_IN_GA(x1, x2)  =  ACKERMANN21_IN_GA(x1)
ACKERMANN27_IN_GA(x1, x2)  =  ACKERMANN27_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
ACKERMANN38_IN_GGA(x1, x2, x3)  =  ACKERMANN38_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)

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:

ACKERMANN21_IN_GA(T28) → ACKERMANN27_IN_GA(T28)
ACKERMANN27_IN_GA(s(T32)) → ACKERMANN21_IN_GA(T32)
ACKERMANN27_IN_GA(s(T32)) → U3_GA(T32, ackermannc21_in_ga(T32))
U3_GA(T32, ackermannc21_out_ga(T32, T34)) → ACKERMANN38_IN_GGA(T32, T34)
ACKERMANN38_IN_GGA(s(T47), 0) → ACKERMANN27_IN_GA(T47)
ACKERMANN38_IN_GGA(s(T52), s(T53)) → ACKERMANN38_IN_GGA(s(T52), T53)
ACKERMANN38_IN_GGA(s(T52), s(T53)) → U7_GGA(T52, T53, ackermannc38_in_gga(s(T52), T53))
U7_GGA(T52, T53, ackermannc38_out_gga(s(T52), T53, T55)) → ACKERMANN38_IN_GGA(T52, T55)

The TRS R consists of the following rules:

ackermannc21_in_ga(T28) → U40_ga(T28, ackermannc27_in_ga(T28))
ackermannc38_in_gga(s(T47), 0) → U43_gga(T47, ackermannc27_in_ga(T47))
ackermannc38_in_gga(s(T52), s(T53)) → U44_gga(T52, T53, ackermannc38_in_gga(s(T52), T53))
U40_ga(T28, ackermannc27_out_ga(T28, X73)) → ackermannc21_out_ga(T28, X73)
U43_gga(T47, ackermannc27_out_ga(T47, X133)) → ackermannc38_out_gga(s(T47), 0, X133)
U44_gga(T52, T53, ackermannc38_out_gga(s(T52), T53, T55)) → U45_gga(T52, T53, ackermannc38_in_gga(T52, T55))
ackermannc27_in_ga(0) → ackermannc27_out_ga(0, s(s(0)))
ackermannc27_in_ga(s(T32)) → U41_ga(T32, ackermannc21_in_ga(T32))
U45_gga(T52, T53, ackermannc38_out_gga(T52, T55, X151)) → ackermannc38_out_gga(s(T52), s(T53), X151)
U41_ga(T32, ackermannc21_out_ga(T32, T34)) → U42_ga(T32, ackermannc38_in_gga(T32, T34))
ackermannc38_in_gga(0, T42) → ackermannc38_out_gga(0, T42, s(T42))
U42_ga(T32, ackermannc38_out_gga(T32, T34, X97)) → ackermannc27_out_ga(s(T32), X97)

The set Q consists of the following terms:

ackermannc21_in_ga(x0)
ackermannc38_in_gga(x0, x1)
U40_ga(x0, x1)
U43_gga(x0, x1)
U44_gga(x0, x1, x2)
ackermannc27_in_ga(x0)
U45_gga(x0, x1, x2)
U41_ga(x0, x1)
U42_ga(x0, x1)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • ACKERMANN27_IN_GA(s(T32)) → ACKERMANN21_IN_GA(T32)
    The graph contains the following edges 1 > 1

  • ACKERMANN27_IN_GA(s(T32)) → U3_GA(T32, ackermannc21_in_ga(T32))
    The graph contains the following edges 1 > 1

  • ACKERMANN21_IN_GA(T28) → ACKERMANN27_IN_GA(T28)
    The graph contains the following edges 1 >= 1

  • ACKERMANN38_IN_GGA(s(T47), 0) → ACKERMANN27_IN_GA(T47)
    The graph contains the following edges 1 > 1

  • U3_GA(T32, ackermannc21_out_ga(T32, T34)) → ACKERMANN38_IN_GGA(T32, T34)
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • U7_GGA(T52, T53, ackermannc38_out_gga(s(T52), T53, T55)) → ACKERMANN38_IN_GGA(T52, T55)
    The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2

  • ACKERMANN38_IN_GGA(s(T52), s(T53)) → ACKERMANN38_IN_GGA(s(T52), T53)
    The graph contains the following edges 1 >= 1, 2 > 2

  • ACKERMANN38_IN_GGA(s(T52), s(T53)) → U7_GGA(T52, T53, ackermannc38_in_gga(s(T52), T53))
    The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

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

ACKERMANN57_IN_GGA(T84, s(T86), X229) → P65_IN_GGAA(T84, T86, X228, X229)
P65_IN_GGAA(T84, T86, X228, X229) → ACKERMANN57_IN_GGA(T84, T86, X228)
P65_IN_GGAA(T84, T86, T88, X229) → U12_GGAA(T84, T86, T88, X229, ackermannc57_in_gga(T84, T86, T88))
U12_GGAA(T84, T86, T88, X229, ackermannc57_out_gga(T84, T86, T88)) → ACKERMANN68_IN_GGA(T84, T88, X229)
ACKERMANN68_IN_GGA(s(T106), s(T108), X283) → P65_IN_GGAA(T106, T108, X282, X283)

The TRS R consists of the following rules:

ackermannc21_in_ga(T28, X73) → U40_ga(T28, X73, ackermannc27_in_ga(T28, X73))
ackermannc27_in_ga(0, s(s(0))) → ackermannc27_out_ga(0, s(s(0)))
ackermannc27_in_ga(s(T32), X97) → U41_ga(T32, X97, ackermannc21_in_ga(T32, T34))
U41_ga(T32, X97, ackermannc21_out_ga(T32, T34)) → U42_ga(T32, X97, ackermannc38_in_gga(T32, T34, X97))
ackermannc38_in_gga(0, T42, s(T42)) → ackermannc38_out_gga(0, T42, s(T42))
ackermannc38_in_gga(s(T47), 0, X133) → U43_gga(T47, X133, ackermannc27_in_ga(T47, X133))
U43_gga(T47, X133, ackermannc27_out_ga(T47, X133)) → ackermannc38_out_gga(s(T47), 0, X133)
ackermannc38_in_gga(s(T52), s(T53), X151) → U44_gga(T52, T53, X151, ackermannc38_in_gga(s(T52), T53, T55))
U44_gga(T52, T53, X151, ackermannc38_out_gga(s(T52), T53, T55)) → U45_gga(T52, T53, X151, ackermannc38_in_gga(T52, T55, X151))
U45_gga(T52, T53, X151, ackermannc38_out_gga(T52, T55, X151)) → ackermannc38_out_gga(s(T52), s(T53), X151)
U42_ga(T32, X97, ackermannc38_out_gga(T32, T34, X97)) → ackermannc27_out_ga(s(T32), X97)
U40_ga(T28, X73, ackermannc27_out_ga(T28, X73)) → ackermannc21_out_ga(T28, X73)
ackermannc57_in_gga(T79, 0, X211) → U46_gga(T79, X211, ackermannc27_in_ga(T79, X211))
U46_gga(T79, X211, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gga(T79, 0, X211)
ackermannc57_in_gga(T84, s(T86), X229) → U47_gga(T84, T86, X229, qc65_in_ggaa(T84, T86, X228, X229))
qc65_in_ggaa(T84, T86, T88, X229) → U48_ggaa(T84, T86, T88, X229, ackermannc57_in_gga(T84, T86, T88))
U48_ggaa(T84, T86, T88, X229, ackermannc57_out_gga(T84, T86, T88)) → U49_ggaa(T84, T86, T88, X229, ackermannc68_in_gga(T84, T88, X229))
ackermannc68_in_gga(0, T96, s(T96)) → ackermannc68_out_gga(0, T96, s(T96))
ackermannc68_in_gga(s(T101), 0, X265) → U50_gga(T101, X265, ackermannc27_in_ga(T101, X265))
U50_gga(T101, X265, ackermannc27_out_ga(T101, X265)) → ackermannc68_out_gga(s(T101), 0, X265)
ackermannc68_in_gga(s(T106), s(T108), X283) → U51_gga(T106, T108, X283, qc65_in_ggaa(T106, T108, X282, X283))
U51_gga(T106, T108, X283, qc65_out_ggaa(T106, T108, X282, X283)) → ackermannc68_out_gga(s(T106), s(T108), X283)
U49_ggaa(T84, T86, T88, X229, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_ggaa(T84, T86, T88, X229)
U47_gga(T84, T86, X229, qc65_out_ggaa(T84, T86, X228, X229)) → ackermannc57_out_gga(T84, s(T86), X229)
ackermannc57_in_gaa(T79, 0, X211) → U46_gaa(T79, X211, ackermannc27_in_ga(T79, X211))
U46_gaa(T79, X211, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gaa(T79, 0, X211)
ackermannc57_in_gaa(T84, s(T86), X229) → U47_gaa(T84, T86, X229, qc65_in_gaaa(T84, T86, X228, X229))
qc65_in_gaaa(T84, T86, T88, X229) → U48_gaaa(T84, T86, T88, X229, ackermannc57_in_gaa(T84, T86, T88))
U48_gaaa(T84, T86, T88, X229, ackermannc57_out_gaa(T84, T86, T88)) → U49_gaaa(T84, T86, T88, X229, ackermannc68_in_gga(T84, T88, X229))
U49_gaaa(T84, T86, T88, X229, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_gaaa(T84, T86, T88, X229)
U47_gaa(T84, T86, X229, qc65_out_gaaa(T84, T86, X228, X229)) → ackermannc57_out_gaa(T84, s(T86), X229)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ackermannc21_in_ga(x1, x2)  =  ackermannc21_in_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
ackermannc27_in_ga(x1, x2)  =  ackermannc27_in_ga(x1)
0  =  0
ackermannc27_out_ga(x1, x2)  =  ackermannc27_out_ga(x1, x2)
U41_ga(x1, x2, x3)  =  U41_ga(x1, x3)
ackermannc21_out_ga(x1, x2)  =  ackermannc21_out_ga(x1, x2)
U42_ga(x1, x2, x3)  =  U42_ga(x1, x3)
ackermannc38_in_gga(x1, x2, x3)  =  ackermannc38_in_gga(x1, x2)
ackermannc38_out_gga(x1, x2, x3)  =  ackermannc38_out_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x3)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
ackermannc57_in_gga(x1, x2, x3)  =  ackermannc57_in_gga(x1, x2)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x3)
ackermannc57_out_gga(x1, x2, x3)  =  ackermannc57_out_gga(x1, x2, x3)
U47_gga(x1, x2, x3, x4)  =  U47_gga(x1, x2, x4)
qc65_in_ggaa(x1, x2, x3, x4)  =  qc65_in_ggaa(x1, x2)
U48_ggaa(x1, x2, x3, x4, x5)  =  U48_ggaa(x1, x2, x5)
U49_ggaa(x1, x2, x3, x4, x5)  =  U49_ggaa(x1, x2, x3, x5)
ackermannc68_in_gga(x1, x2, x3)  =  ackermannc68_in_gga(x1, x2)
ackermannc68_out_gga(x1, x2, x3)  =  ackermannc68_out_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x3)
U51_gga(x1, x2, x3, x4)  =  U51_gga(x1, x2, x4)
qc65_out_ggaa(x1, x2, x3, x4)  =  qc65_out_ggaa(x1, x2, x3, x4)
ackermannc57_in_gaa(x1, x2, x3)  =  ackermannc57_in_gaa(x1)
U46_gaa(x1, x2, x3)  =  U46_gaa(x1, x3)
ackermannc57_out_gaa(x1, x2, x3)  =  ackermannc57_out_gaa(x1, x2, x3)
U47_gaa(x1, x2, x3, x4)  =  U47_gaa(x1, x4)
qc65_in_gaaa(x1, x2, x3, x4)  =  qc65_in_gaaa(x1)
U48_gaaa(x1, x2, x3, x4, x5)  =  U48_gaaa(x1, x5)
U49_gaaa(x1, x2, x3, x4, x5)  =  U49_gaaa(x1, x2, x3, x5)
qc65_out_gaaa(x1, x2, x3, x4)  =  qc65_out_gaaa(x1, x2, x3, x4)
ACKERMANN57_IN_GGA(x1, x2, x3)  =  ACKERMANN57_IN_GGA(x1, x2)
P65_IN_GGAA(x1, x2, x3, x4)  =  P65_IN_GGAA(x1, x2)
U12_GGAA(x1, x2, x3, x4, x5)  =  U12_GGAA(x1, x2, x5)
ACKERMANN68_IN_GGA(x1, x2, x3)  =  ACKERMANN68_IN_GGA(x1, x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

ACKERMANN57_IN_GGA(T84, s(T86), X229) → P65_IN_GGAA(T84, T86, X228, X229)
P65_IN_GGAA(T84, T86, X228, X229) → ACKERMANN57_IN_GGA(T84, T86, X228)
P65_IN_GGAA(T84, T86, T88, X229) → U12_GGAA(T84, T86, T88, X229, ackermannc57_in_gga(T84, T86, T88))
U12_GGAA(T84, T86, T88, X229, ackermannc57_out_gga(T84, T86, T88)) → ACKERMANN68_IN_GGA(T84, T88, X229)
ACKERMANN68_IN_GGA(s(T106), s(T108), X283) → P65_IN_GGAA(T106, T108, X282, X283)

The TRS R consists of the following rules:

ackermannc57_in_gga(T79, 0, X211) → U46_gga(T79, X211, ackermannc27_in_ga(T79, X211))
ackermannc57_in_gga(T84, s(T86), X229) → U47_gga(T84, T86, X229, qc65_in_ggaa(T84, T86, X228, X229))
U46_gga(T79, X211, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gga(T79, 0, X211)
U47_gga(T84, T86, X229, qc65_out_ggaa(T84, T86, X228, X229)) → ackermannc57_out_gga(T84, s(T86), X229)
ackermannc27_in_ga(0, s(s(0))) → ackermannc27_out_ga(0, s(s(0)))
ackermannc27_in_ga(s(T32), X97) → U41_ga(T32, X97, ackermannc21_in_ga(T32, T34))
qc65_in_ggaa(T84, T86, T88, X229) → U48_ggaa(T84, T86, T88, X229, ackermannc57_in_gga(T84, T86, T88))
U41_ga(T32, X97, ackermannc21_out_ga(T32, T34)) → U42_ga(T32, X97, ackermannc38_in_gga(T32, T34, X97))
U48_ggaa(T84, T86, T88, X229, ackermannc57_out_gga(T84, T86, T88)) → U49_ggaa(T84, T86, T88, X229, ackermannc68_in_gga(T84, T88, X229))
ackermannc21_in_ga(T28, X73) → U40_ga(T28, X73, ackermannc27_in_ga(T28, X73))
U42_ga(T32, X97, ackermannc38_out_gga(T32, T34, X97)) → ackermannc27_out_ga(s(T32), X97)
U49_ggaa(T84, T86, T88, X229, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_ggaa(T84, T86, T88, X229)
U40_ga(T28, X73, ackermannc27_out_ga(T28, X73)) → ackermannc21_out_ga(T28, X73)
ackermannc38_in_gga(0, T42, s(T42)) → ackermannc38_out_gga(0, T42, s(T42))
ackermannc38_in_gga(s(T47), 0, X133) → U43_gga(T47, X133, ackermannc27_in_ga(T47, X133))
ackermannc38_in_gga(s(T52), s(T53), X151) → U44_gga(T52, T53, X151, ackermannc38_in_gga(s(T52), T53, T55))
ackermannc68_in_gga(0, T96, s(T96)) → ackermannc68_out_gga(0, T96, s(T96))
ackermannc68_in_gga(s(T101), 0, X265) → U50_gga(T101, X265, ackermannc27_in_ga(T101, X265))
ackermannc68_in_gga(s(T106), s(T108), X283) → U51_gga(T106, T108, X283, qc65_in_ggaa(T106, T108, X282, X283))
U43_gga(T47, X133, ackermannc27_out_ga(T47, X133)) → ackermannc38_out_gga(s(T47), 0, X133)
U44_gga(T52, T53, X151, ackermannc38_out_gga(s(T52), T53, T55)) → U45_gga(T52, T53, X151, ackermannc38_in_gga(T52, T55, X151))
U50_gga(T101, X265, ackermannc27_out_ga(T101, X265)) → ackermannc68_out_gga(s(T101), 0, X265)
U51_gga(T106, T108, X283, qc65_out_ggaa(T106, T108, X282, X283)) → ackermannc68_out_gga(s(T106), s(T108), X283)
U45_gga(T52, T53, X151, ackermannc38_out_gga(T52, T55, X151)) → ackermannc38_out_gga(s(T52), s(T53), X151)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ackermannc21_in_ga(x1, x2)  =  ackermannc21_in_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
ackermannc27_in_ga(x1, x2)  =  ackermannc27_in_ga(x1)
0  =  0
ackermannc27_out_ga(x1, x2)  =  ackermannc27_out_ga(x1, x2)
U41_ga(x1, x2, x3)  =  U41_ga(x1, x3)
ackermannc21_out_ga(x1, x2)  =  ackermannc21_out_ga(x1, x2)
U42_ga(x1, x2, x3)  =  U42_ga(x1, x3)
ackermannc38_in_gga(x1, x2, x3)  =  ackermannc38_in_gga(x1, x2)
ackermannc38_out_gga(x1, x2, x3)  =  ackermannc38_out_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x3)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
ackermannc57_in_gga(x1, x2, x3)  =  ackermannc57_in_gga(x1, x2)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x3)
ackermannc57_out_gga(x1, x2, x3)  =  ackermannc57_out_gga(x1, x2, x3)
U47_gga(x1, x2, x3, x4)  =  U47_gga(x1, x2, x4)
qc65_in_ggaa(x1, x2, x3, x4)  =  qc65_in_ggaa(x1, x2)
U48_ggaa(x1, x2, x3, x4, x5)  =  U48_ggaa(x1, x2, x5)
U49_ggaa(x1, x2, x3, x4, x5)  =  U49_ggaa(x1, x2, x3, x5)
ackermannc68_in_gga(x1, x2, x3)  =  ackermannc68_in_gga(x1, x2)
ackermannc68_out_gga(x1, x2, x3)  =  ackermannc68_out_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x3)
U51_gga(x1, x2, x3, x4)  =  U51_gga(x1, x2, x4)
qc65_out_ggaa(x1, x2, x3, x4)  =  qc65_out_ggaa(x1, x2, x3, x4)
ACKERMANN57_IN_GGA(x1, x2, x3)  =  ACKERMANN57_IN_GGA(x1, x2)
P65_IN_GGAA(x1, x2, x3, x4)  =  P65_IN_GGAA(x1, x2)
U12_GGAA(x1, x2, x3, x4, x5)  =  U12_GGAA(x1, x2, x5)
ACKERMANN68_IN_GGA(x1, x2, x3)  =  ACKERMANN68_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:

ACKERMANN57_IN_GGA(T84, s(T86)) → P65_IN_GGAA(T84, T86)
P65_IN_GGAA(T84, T86) → ACKERMANN57_IN_GGA(T84, T86)
P65_IN_GGAA(T84, T86) → U12_GGAA(T84, T86, ackermannc57_in_gga(T84, T86))
U12_GGAA(T84, T86, ackermannc57_out_gga(T84, T86, T88)) → ACKERMANN68_IN_GGA(T84, T88)
ACKERMANN68_IN_GGA(s(T106), s(T108)) → P65_IN_GGAA(T106, T108)

The TRS R consists of the following rules:

ackermannc57_in_gga(T79, 0) → U46_gga(T79, ackermannc27_in_ga(T79))
ackermannc57_in_gga(T84, s(T86)) → U47_gga(T84, T86, qc65_in_ggaa(T84, T86))
U46_gga(T79, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gga(T79, 0, X211)
U47_gga(T84, T86, qc65_out_ggaa(T84, T86, X228, X229)) → ackermannc57_out_gga(T84, s(T86), X229)
ackermannc27_in_ga(0) → ackermannc27_out_ga(0, s(s(0)))
ackermannc27_in_ga(s(T32)) → U41_ga(T32, ackermannc21_in_ga(T32))
qc65_in_ggaa(T84, T86) → U48_ggaa(T84, T86, ackermannc57_in_gga(T84, T86))
U41_ga(T32, ackermannc21_out_ga(T32, T34)) → U42_ga(T32, ackermannc38_in_gga(T32, T34))
U48_ggaa(T84, T86, ackermannc57_out_gga(T84, T86, T88)) → U49_ggaa(T84, T86, T88, ackermannc68_in_gga(T84, T88))
ackermannc21_in_ga(T28) → U40_ga(T28, ackermannc27_in_ga(T28))
U42_ga(T32, ackermannc38_out_gga(T32, T34, X97)) → ackermannc27_out_ga(s(T32), X97)
U49_ggaa(T84, T86, T88, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_ggaa(T84, T86, T88, X229)
U40_ga(T28, ackermannc27_out_ga(T28, X73)) → ackermannc21_out_ga(T28, X73)
ackermannc38_in_gga(0, T42) → ackermannc38_out_gga(0, T42, s(T42))
ackermannc38_in_gga(s(T47), 0) → U43_gga(T47, ackermannc27_in_ga(T47))
ackermannc38_in_gga(s(T52), s(T53)) → U44_gga(T52, T53, ackermannc38_in_gga(s(T52), T53))
ackermannc68_in_gga(0, T96) → ackermannc68_out_gga(0, T96, s(T96))
ackermannc68_in_gga(s(T101), 0) → U50_gga(T101, ackermannc27_in_ga(T101))
ackermannc68_in_gga(s(T106), s(T108)) → U51_gga(T106, T108, qc65_in_ggaa(T106, T108))
U43_gga(T47, ackermannc27_out_ga(T47, X133)) → ackermannc38_out_gga(s(T47), 0, X133)
U44_gga(T52, T53, ackermannc38_out_gga(s(T52), T53, T55)) → U45_gga(T52, T53, ackermannc38_in_gga(T52, T55))
U50_gga(T101, ackermannc27_out_ga(T101, X265)) → ackermannc68_out_gga(s(T101), 0, X265)
U51_gga(T106, T108, qc65_out_ggaa(T106, T108, X282, X283)) → ackermannc68_out_gga(s(T106), s(T108), X283)
U45_gga(T52, T53, ackermannc38_out_gga(T52, T55, X151)) → ackermannc38_out_gga(s(T52), s(T53), X151)

The set Q consists of the following terms:

ackermannc57_in_gga(x0, x1)
U46_gga(x0, x1)
U47_gga(x0, x1, x2)
ackermannc27_in_ga(x0)
qc65_in_ggaa(x0, x1)
U41_ga(x0, x1)
U48_ggaa(x0, x1, x2)
ackermannc21_in_ga(x0)
U42_ga(x0, x1)
U49_ggaa(x0, x1, x2, x3)
U40_ga(x0, x1)
ackermannc38_in_gga(x0, x1)
ackermannc68_in_gga(x0, x1)
U43_gga(x0, x1)
U44_gga(x0, x1, x2)
U50_gga(x0, x1)
U51_gga(x0, x1, x2)
U45_gga(x0, x1, x2)

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:

  • P65_IN_GGAA(T84, T86) → ACKERMANN57_IN_GGA(T84, T86)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • P65_IN_GGAA(T84, T86) → U12_GGAA(T84, T86, ackermannc57_in_gga(T84, T86))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • ACKERMANN57_IN_GGA(T84, s(T86)) → P65_IN_GGAA(T84, T86)
    The graph contains the following edges 1 >= 1, 2 > 2

  • ACKERMANN68_IN_GGA(s(T106), s(T108)) → P65_IN_GGAA(T106, T108)
    The graph contains the following edges 1 > 1, 2 > 2

  • U12_GGAA(T84, T86, ackermannc57_out_gga(T84, T86, T88)) → ACKERMANN68_IN_GGA(T84, T88)
    The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2

(20) YES

(21) Obligation:

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

P65_IN_GAAA(T84, T86, X228, X229) → ACKERMANN57_IN_GAA(T84, T86, X228)
ACKERMANN57_IN_GAA(T84, s(T86), X229) → P65_IN_GAAA(T84, T86, X228, X229)

The TRS R consists of the following rules:

ackermannc21_in_ga(T28, X73) → U40_ga(T28, X73, ackermannc27_in_ga(T28, X73))
ackermannc27_in_ga(0, s(s(0))) → ackermannc27_out_ga(0, s(s(0)))
ackermannc27_in_ga(s(T32), X97) → U41_ga(T32, X97, ackermannc21_in_ga(T32, T34))
U41_ga(T32, X97, ackermannc21_out_ga(T32, T34)) → U42_ga(T32, X97, ackermannc38_in_gga(T32, T34, X97))
ackermannc38_in_gga(0, T42, s(T42)) → ackermannc38_out_gga(0, T42, s(T42))
ackermannc38_in_gga(s(T47), 0, X133) → U43_gga(T47, X133, ackermannc27_in_ga(T47, X133))
U43_gga(T47, X133, ackermannc27_out_ga(T47, X133)) → ackermannc38_out_gga(s(T47), 0, X133)
ackermannc38_in_gga(s(T52), s(T53), X151) → U44_gga(T52, T53, X151, ackermannc38_in_gga(s(T52), T53, T55))
U44_gga(T52, T53, X151, ackermannc38_out_gga(s(T52), T53, T55)) → U45_gga(T52, T53, X151, ackermannc38_in_gga(T52, T55, X151))
U45_gga(T52, T53, X151, ackermannc38_out_gga(T52, T55, X151)) → ackermannc38_out_gga(s(T52), s(T53), X151)
U42_ga(T32, X97, ackermannc38_out_gga(T32, T34, X97)) → ackermannc27_out_ga(s(T32), X97)
U40_ga(T28, X73, ackermannc27_out_ga(T28, X73)) → ackermannc21_out_ga(T28, X73)
ackermannc57_in_gga(T79, 0, X211) → U46_gga(T79, X211, ackermannc27_in_ga(T79, X211))
U46_gga(T79, X211, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gga(T79, 0, X211)
ackermannc57_in_gga(T84, s(T86), X229) → U47_gga(T84, T86, X229, qc65_in_ggaa(T84, T86, X228, X229))
qc65_in_ggaa(T84, T86, T88, X229) → U48_ggaa(T84, T86, T88, X229, ackermannc57_in_gga(T84, T86, T88))
U48_ggaa(T84, T86, T88, X229, ackermannc57_out_gga(T84, T86, T88)) → U49_ggaa(T84, T86, T88, X229, ackermannc68_in_gga(T84, T88, X229))
ackermannc68_in_gga(0, T96, s(T96)) → ackermannc68_out_gga(0, T96, s(T96))
ackermannc68_in_gga(s(T101), 0, X265) → U50_gga(T101, X265, ackermannc27_in_ga(T101, X265))
U50_gga(T101, X265, ackermannc27_out_ga(T101, X265)) → ackermannc68_out_gga(s(T101), 0, X265)
ackermannc68_in_gga(s(T106), s(T108), X283) → U51_gga(T106, T108, X283, qc65_in_ggaa(T106, T108, X282, X283))
U51_gga(T106, T108, X283, qc65_out_ggaa(T106, T108, X282, X283)) → ackermannc68_out_gga(s(T106), s(T108), X283)
U49_ggaa(T84, T86, T88, X229, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_ggaa(T84, T86, T88, X229)
U47_gga(T84, T86, X229, qc65_out_ggaa(T84, T86, X228, X229)) → ackermannc57_out_gga(T84, s(T86), X229)
ackermannc57_in_gaa(T79, 0, X211) → U46_gaa(T79, X211, ackermannc27_in_ga(T79, X211))
U46_gaa(T79, X211, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gaa(T79, 0, X211)
ackermannc57_in_gaa(T84, s(T86), X229) → U47_gaa(T84, T86, X229, qc65_in_gaaa(T84, T86, X228, X229))
qc65_in_gaaa(T84, T86, T88, X229) → U48_gaaa(T84, T86, T88, X229, ackermannc57_in_gaa(T84, T86, T88))
U48_gaaa(T84, T86, T88, X229, ackermannc57_out_gaa(T84, T86, T88)) → U49_gaaa(T84, T86, T88, X229, ackermannc68_in_gga(T84, T88, X229))
U49_gaaa(T84, T86, T88, X229, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_gaaa(T84, T86, T88, X229)
U47_gaa(T84, T86, X229, qc65_out_gaaa(T84, T86, X228, X229)) → ackermannc57_out_gaa(T84, s(T86), X229)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ackermannc21_in_ga(x1, x2)  =  ackermannc21_in_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
ackermannc27_in_ga(x1, x2)  =  ackermannc27_in_ga(x1)
0  =  0
ackermannc27_out_ga(x1, x2)  =  ackermannc27_out_ga(x1, x2)
U41_ga(x1, x2, x3)  =  U41_ga(x1, x3)
ackermannc21_out_ga(x1, x2)  =  ackermannc21_out_ga(x1, x2)
U42_ga(x1, x2, x3)  =  U42_ga(x1, x3)
ackermannc38_in_gga(x1, x2, x3)  =  ackermannc38_in_gga(x1, x2)
ackermannc38_out_gga(x1, x2, x3)  =  ackermannc38_out_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x3)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
ackermannc57_in_gga(x1, x2, x3)  =  ackermannc57_in_gga(x1, x2)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x3)
ackermannc57_out_gga(x1, x2, x3)  =  ackermannc57_out_gga(x1, x2, x3)
U47_gga(x1, x2, x3, x4)  =  U47_gga(x1, x2, x4)
qc65_in_ggaa(x1, x2, x3, x4)  =  qc65_in_ggaa(x1, x2)
U48_ggaa(x1, x2, x3, x4, x5)  =  U48_ggaa(x1, x2, x5)
U49_ggaa(x1, x2, x3, x4, x5)  =  U49_ggaa(x1, x2, x3, x5)
ackermannc68_in_gga(x1, x2, x3)  =  ackermannc68_in_gga(x1, x2)
ackermannc68_out_gga(x1, x2, x3)  =  ackermannc68_out_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x3)
U51_gga(x1, x2, x3, x4)  =  U51_gga(x1, x2, x4)
qc65_out_ggaa(x1, x2, x3, x4)  =  qc65_out_ggaa(x1, x2, x3, x4)
ackermannc57_in_gaa(x1, x2, x3)  =  ackermannc57_in_gaa(x1)
U46_gaa(x1, x2, x3)  =  U46_gaa(x1, x3)
ackermannc57_out_gaa(x1, x2, x3)  =  ackermannc57_out_gaa(x1, x2, x3)
U47_gaa(x1, x2, x3, x4)  =  U47_gaa(x1, x4)
qc65_in_gaaa(x1, x2, x3, x4)  =  qc65_in_gaaa(x1)
U48_gaaa(x1, x2, x3, x4, x5)  =  U48_gaaa(x1, x5)
U49_gaaa(x1, x2, x3, x4, x5)  =  U49_gaaa(x1, x2, x3, x5)
qc65_out_gaaa(x1, x2, x3, x4)  =  qc65_out_gaaa(x1, x2, x3, x4)
ACKERMANN57_IN_GAA(x1, x2, x3)  =  ACKERMANN57_IN_GAA(x1)
P65_IN_GAAA(x1, x2, x3, x4)  =  P65_IN_GAAA(x1)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

P65_IN_GAAA(T84, T86, X228, X229) → ACKERMANN57_IN_GAA(T84, T86, X228)
ACKERMANN57_IN_GAA(T84, s(T86), X229) → P65_IN_GAAA(T84, T86, X228, X229)

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

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

P65_IN_GAAA(T84) → ACKERMANN57_IN_GAA(T84)
ACKERMANN57_IN_GAA(T84) → P65_IN_GAAA(T84)

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

(26) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = ACKERMANN57_IN_GAA(T84') evaluates to t =ACKERMANN57_IN_GAA(T84')

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




Rewriting sequence

ACKERMANN57_IN_GAA(T84')P65_IN_GAAA(T84')
with rule ACKERMANN57_IN_GAA(T84'') → P65_IN_GAAA(T84'') at position [] and matcher [T84'' / T84']

P65_IN_GAAA(T84')ACKERMANN57_IN_GAA(T84')
with rule P65_IN_GAAA(T84) → ACKERMANN57_IN_GAA(T84)

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(27) NO

(28) Obligation:

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

ACKERMANN1_IN_GGG(s(s(T19)), 0, T20) → U17_GGG(T19, T20, ackermannc21_in_ga(T19, T22))
U17_GGG(T19, T20, ackermannc21_out_ga(T19, T22)) → ACKERMANN1_IN_GGG(T19, T22, T20)
ACKERMANN1_IN_GGG(s(T68), s(T71), T70) → U20_GGG(T68, T71, T70, ackermannc57_in_gga(T68, T71, T73))
U20_GGG(T68, T71, T70, ackermannc57_out_gga(T68, T71, T73)) → ACKERMANN1_IN_GGG(T68, T73, T70)
ACKERMANN1_IN_GGG(s(T123), s(0), T117) → U23_GGG(T123, T117, ackermannc27_in_ga(T123, T124))
U23_GGG(T123, T117, ackermannc27_out_ga(T123, T124)) → ACKERMANN1_IN_GGG(T123, T124, T117)
ACKERMANN1_IN_GGG(s(T131), s(s(T133)), T117) → U26_GGG(T131, T133, T117, ackermannc57_in_gga(T131, T133, T135))
U26_GGG(T131, T133, T117, ackermannc57_out_gga(T131, T133, T135)) → U28_GGG(T131, T133, T117, ackermannc68_in_gga(T131, T135, T139))
U28_GGG(T131, T133, T117, ackermannc68_out_gga(T131, T135, T139)) → ACKERMANN1_IN_GGG(T131, T139, T117)

The TRS R consists of the following rules:

ackermannc21_in_ga(T28, X73) → U40_ga(T28, X73, ackermannc27_in_ga(T28, X73))
ackermannc27_in_ga(0, s(s(0))) → ackermannc27_out_ga(0, s(s(0)))
ackermannc27_in_ga(s(T32), X97) → U41_ga(T32, X97, ackermannc21_in_ga(T32, T34))
U41_ga(T32, X97, ackermannc21_out_ga(T32, T34)) → U42_ga(T32, X97, ackermannc38_in_gga(T32, T34, X97))
ackermannc38_in_gga(0, T42, s(T42)) → ackermannc38_out_gga(0, T42, s(T42))
ackermannc38_in_gga(s(T47), 0, X133) → U43_gga(T47, X133, ackermannc27_in_ga(T47, X133))
U43_gga(T47, X133, ackermannc27_out_ga(T47, X133)) → ackermannc38_out_gga(s(T47), 0, X133)
ackermannc38_in_gga(s(T52), s(T53), X151) → U44_gga(T52, T53, X151, ackermannc38_in_gga(s(T52), T53, T55))
U44_gga(T52, T53, X151, ackermannc38_out_gga(s(T52), T53, T55)) → U45_gga(T52, T53, X151, ackermannc38_in_gga(T52, T55, X151))
U45_gga(T52, T53, X151, ackermannc38_out_gga(T52, T55, X151)) → ackermannc38_out_gga(s(T52), s(T53), X151)
U42_ga(T32, X97, ackermannc38_out_gga(T32, T34, X97)) → ackermannc27_out_ga(s(T32), X97)
U40_ga(T28, X73, ackermannc27_out_ga(T28, X73)) → ackermannc21_out_ga(T28, X73)
ackermannc57_in_gga(T79, 0, X211) → U46_gga(T79, X211, ackermannc27_in_ga(T79, X211))
U46_gga(T79, X211, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gga(T79, 0, X211)
ackermannc57_in_gga(T84, s(T86), X229) → U47_gga(T84, T86, X229, qc65_in_ggaa(T84, T86, X228, X229))
qc65_in_ggaa(T84, T86, T88, X229) → U48_ggaa(T84, T86, T88, X229, ackermannc57_in_gga(T84, T86, T88))
U48_ggaa(T84, T86, T88, X229, ackermannc57_out_gga(T84, T86, T88)) → U49_ggaa(T84, T86, T88, X229, ackermannc68_in_gga(T84, T88, X229))
ackermannc68_in_gga(0, T96, s(T96)) → ackermannc68_out_gga(0, T96, s(T96))
ackermannc68_in_gga(s(T101), 0, X265) → U50_gga(T101, X265, ackermannc27_in_ga(T101, X265))
U50_gga(T101, X265, ackermannc27_out_ga(T101, X265)) → ackermannc68_out_gga(s(T101), 0, X265)
ackermannc68_in_gga(s(T106), s(T108), X283) → U51_gga(T106, T108, X283, qc65_in_ggaa(T106, T108, X282, X283))
U51_gga(T106, T108, X283, qc65_out_ggaa(T106, T108, X282, X283)) → ackermannc68_out_gga(s(T106), s(T108), X283)
U49_ggaa(T84, T86, T88, X229, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_ggaa(T84, T86, T88, X229)
U47_gga(T84, T86, X229, qc65_out_ggaa(T84, T86, X228, X229)) → ackermannc57_out_gga(T84, s(T86), X229)
ackermannc57_in_gaa(T79, 0, X211) → U46_gaa(T79, X211, ackermannc27_in_ga(T79, X211))
U46_gaa(T79, X211, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gaa(T79, 0, X211)
ackermannc57_in_gaa(T84, s(T86), X229) → U47_gaa(T84, T86, X229, qc65_in_gaaa(T84, T86, X228, X229))
qc65_in_gaaa(T84, T86, T88, X229) → U48_gaaa(T84, T86, T88, X229, ackermannc57_in_gaa(T84, T86, T88))
U48_gaaa(T84, T86, T88, X229, ackermannc57_out_gaa(T84, T86, T88)) → U49_gaaa(T84, T86, T88, X229, ackermannc68_in_gga(T84, T88, X229))
U49_gaaa(T84, T86, T88, X229, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_gaaa(T84, T86, T88, X229)
U47_gaa(T84, T86, X229, qc65_out_gaaa(T84, T86, X228, X229)) → ackermannc57_out_gaa(T84, s(T86), X229)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ackermannc21_in_ga(x1, x2)  =  ackermannc21_in_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
ackermannc27_in_ga(x1, x2)  =  ackermannc27_in_ga(x1)
0  =  0
ackermannc27_out_ga(x1, x2)  =  ackermannc27_out_ga(x1, x2)
U41_ga(x1, x2, x3)  =  U41_ga(x1, x3)
ackermannc21_out_ga(x1, x2)  =  ackermannc21_out_ga(x1, x2)
U42_ga(x1, x2, x3)  =  U42_ga(x1, x3)
ackermannc38_in_gga(x1, x2, x3)  =  ackermannc38_in_gga(x1, x2)
ackermannc38_out_gga(x1, x2, x3)  =  ackermannc38_out_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x3)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
ackermannc57_in_gga(x1, x2, x3)  =  ackermannc57_in_gga(x1, x2)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x3)
ackermannc57_out_gga(x1, x2, x3)  =  ackermannc57_out_gga(x1, x2, x3)
U47_gga(x1, x2, x3, x4)  =  U47_gga(x1, x2, x4)
qc65_in_ggaa(x1, x2, x3, x4)  =  qc65_in_ggaa(x1, x2)
U48_ggaa(x1, x2, x3, x4, x5)  =  U48_ggaa(x1, x2, x5)
U49_ggaa(x1, x2, x3, x4, x5)  =  U49_ggaa(x1, x2, x3, x5)
ackermannc68_in_gga(x1, x2, x3)  =  ackermannc68_in_gga(x1, x2)
ackermannc68_out_gga(x1, x2, x3)  =  ackermannc68_out_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x3)
U51_gga(x1, x2, x3, x4)  =  U51_gga(x1, x2, x4)
qc65_out_ggaa(x1, x2, x3, x4)  =  qc65_out_ggaa(x1, x2, x3, x4)
ackermannc57_in_gaa(x1, x2, x3)  =  ackermannc57_in_gaa(x1)
U46_gaa(x1, x2, x3)  =  U46_gaa(x1, x3)
ackermannc57_out_gaa(x1, x2, x3)  =  ackermannc57_out_gaa(x1, x2, x3)
U47_gaa(x1, x2, x3, x4)  =  U47_gaa(x1, x4)
qc65_in_gaaa(x1, x2, x3, x4)  =  qc65_in_gaaa(x1)
U48_gaaa(x1, x2, x3, x4, x5)  =  U48_gaaa(x1, x5)
U49_gaaa(x1, x2, x3, x4, x5)  =  U49_gaaa(x1, x2, x3, x5)
qc65_out_gaaa(x1, x2, x3, x4)  =  qc65_out_gaaa(x1, x2, x3, x4)
ACKERMANN1_IN_GGG(x1, x2, x3)  =  ACKERMANN1_IN_GGG(x1, x2, x3)
U17_GGG(x1, x2, x3)  =  U17_GGG(x1, x2, x3)
U20_GGG(x1, x2, x3, x4)  =  U20_GGG(x1, x2, x3, x4)
U23_GGG(x1, x2, x3)  =  U23_GGG(x1, x2, x3)
U26_GGG(x1, x2, x3, x4)  =  U26_GGG(x1, x2, x3, x4)
U28_GGG(x1, x2, x3, x4)  =  U28_GGG(x1, x2, x3, x4)

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

ACKERMANN1_IN_GGG(s(s(T19)), 0, T20) → U17_GGG(T19, T20, ackermannc21_in_ga(T19, T22))
U17_GGG(T19, T20, ackermannc21_out_ga(T19, T22)) → ACKERMANN1_IN_GGG(T19, T22, T20)
ACKERMANN1_IN_GGG(s(T68), s(T71), T70) → U20_GGG(T68, T71, T70, ackermannc57_in_gga(T68, T71, T73))
U20_GGG(T68, T71, T70, ackermannc57_out_gga(T68, T71, T73)) → ACKERMANN1_IN_GGG(T68, T73, T70)
ACKERMANN1_IN_GGG(s(T123), s(0), T117) → U23_GGG(T123, T117, ackermannc27_in_ga(T123, T124))
U23_GGG(T123, T117, ackermannc27_out_ga(T123, T124)) → ACKERMANN1_IN_GGG(T123, T124, T117)
ACKERMANN1_IN_GGG(s(T131), s(s(T133)), T117) → U26_GGG(T131, T133, T117, ackermannc57_in_gga(T131, T133, T135))
U26_GGG(T131, T133, T117, ackermannc57_out_gga(T131, T133, T135)) → U28_GGG(T131, T133, T117, ackermannc68_in_gga(T131, T135, T139))
U28_GGG(T131, T133, T117, ackermannc68_out_gga(T131, T135, T139)) → ACKERMANN1_IN_GGG(T131, T139, T117)

The TRS R consists of the following rules:

ackermannc21_in_ga(T28, X73) → U40_ga(T28, X73, ackermannc27_in_ga(T28, X73))
ackermannc57_in_gga(T79, 0, X211) → U46_gga(T79, X211, ackermannc27_in_ga(T79, X211))
ackermannc57_in_gga(T84, s(T86), X229) → U47_gga(T84, T86, X229, qc65_in_ggaa(T84, T86, X228, X229))
ackermannc27_in_ga(0, s(s(0))) → ackermannc27_out_ga(0, s(s(0)))
ackermannc27_in_ga(s(T32), X97) → U41_ga(T32, X97, ackermannc21_in_ga(T32, T34))
ackermannc68_in_gga(0, T96, s(T96)) → ackermannc68_out_gga(0, T96, s(T96))
ackermannc68_in_gga(s(T101), 0, X265) → U50_gga(T101, X265, ackermannc27_in_ga(T101, X265))
ackermannc68_in_gga(s(T106), s(T108), X283) → U51_gga(T106, T108, X283, qc65_in_ggaa(T106, T108, X282, X283))
U40_ga(T28, X73, ackermannc27_out_ga(T28, X73)) → ackermannc21_out_ga(T28, X73)
U46_gga(T79, X211, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gga(T79, 0, X211)
U47_gga(T84, T86, X229, qc65_out_ggaa(T84, T86, X228, X229)) → ackermannc57_out_gga(T84, s(T86), X229)
U41_ga(T32, X97, ackermannc21_out_ga(T32, T34)) → U42_ga(T32, X97, ackermannc38_in_gga(T32, T34, X97))
U50_gga(T101, X265, ackermannc27_out_ga(T101, X265)) → ackermannc68_out_gga(s(T101), 0, X265)
U51_gga(T106, T108, X283, qc65_out_ggaa(T106, T108, X282, X283)) → ackermannc68_out_gga(s(T106), s(T108), X283)
qc65_in_ggaa(T84, T86, T88, X229) → U48_ggaa(T84, T86, T88, X229, ackermannc57_in_gga(T84, T86, T88))
U42_ga(T32, X97, ackermannc38_out_gga(T32, T34, X97)) → ackermannc27_out_ga(s(T32), X97)
U48_ggaa(T84, T86, T88, X229, ackermannc57_out_gga(T84, T86, T88)) → U49_ggaa(T84, T86, T88, X229, ackermannc68_in_gga(T84, T88, X229))
ackermannc38_in_gga(0, T42, s(T42)) → ackermannc38_out_gga(0, T42, s(T42))
ackermannc38_in_gga(s(T47), 0, X133) → U43_gga(T47, X133, ackermannc27_in_ga(T47, X133))
ackermannc38_in_gga(s(T52), s(T53), X151) → U44_gga(T52, T53, X151, ackermannc38_in_gga(s(T52), T53, T55))
U49_ggaa(T84, T86, T88, X229, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_ggaa(T84, T86, T88, X229)
U43_gga(T47, X133, ackermannc27_out_ga(T47, X133)) → ackermannc38_out_gga(s(T47), 0, X133)
U44_gga(T52, T53, X151, ackermannc38_out_gga(s(T52), T53, T55)) → U45_gga(T52, T53, X151, ackermannc38_in_gga(T52, T55, X151))
U45_gga(T52, T53, X151, ackermannc38_out_gga(T52, T55, X151)) → ackermannc38_out_gga(s(T52), s(T53), X151)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ackermannc21_in_ga(x1, x2)  =  ackermannc21_in_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
ackermannc27_in_ga(x1, x2)  =  ackermannc27_in_ga(x1)
0  =  0
ackermannc27_out_ga(x1, x2)  =  ackermannc27_out_ga(x1, x2)
U41_ga(x1, x2, x3)  =  U41_ga(x1, x3)
ackermannc21_out_ga(x1, x2)  =  ackermannc21_out_ga(x1, x2)
U42_ga(x1, x2, x3)  =  U42_ga(x1, x3)
ackermannc38_in_gga(x1, x2, x3)  =  ackermannc38_in_gga(x1, x2)
ackermannc38_out_gga(x1, x2, x3)  =  ackermannc38_out_gga(x1, x2, x3)
U43_gga(x1, x2, x3)  =  U43_gga(x1, x3)
U44_gga(x1, x2, x3, x4)  =  U44_gga(x1, x2, x4)
U45_gga(x1, x2, x3, x4)  =  U45_gga(x1, x2, x4)
ackermannc57_in_gga(x1, x2, x3)  =  ackermannc57_in_gga(x1, x2)
U46_gga(x1, x2, x3)  =  U46_gga(x1, x3)
ackermannc57_out_gga(x1, x2, x3)  =  ackermannc57_out_gga(x1, x2, x3)
U47_gga(x1, x2, x3, x4)  =  U47_gga(x1, x2, x4)
qc65_in_ggaa(x1, x2, x3, x4)  =  qc65_in_ggaa(x1, x2)
U48_ggaa(x1, x2, x3, x4, x5)  =  U48_ggaa(x1, x2, x5)
U49_ggaa(x1, x2, x3, x4, x5)  =  U49_ggaa(x1, x2, x3, x5)
ackermannc68_in_gga(x1, x2, x3)  =  ackermannc68_in_gga(x1, x2)
ackermannc68_out_gga(x1, x2, x3)  =  ackermannc68_out_gga(x1, x2, x3)
U50_gga(x1, x2, x3)  =  U50_gga(x1, x3)
U51_gga(x1, x2, x3, x4)  =  U51_gga(x1, x2, x4)
qc65_out_ggaa(x1, x2, x3, x4)  =  qc65_out_ggaa(x1, x2, x3, x4)
ACKERMANN1_IN_GGG(x1, x2, x3)  =  ACKERMANN1_IN_GGG(x1, x2, x3)
U17_GGG(x1, x2, x3)  =  U17_GGG(x1, x2, x3)
U20_GGG(x1, x2, x3, x4)  =  U20_GGG(x1, x2, x3, x4)
U23_GGG(x1, x2, x3)  =  U23_GGG(x1, x2, x3)
U26_GGG(x1, x2, x3, x4)  =  U26_GGG(x1, x2, x3, x4)
U28_GGG(x1, x2, x3, x4)  =  U28_GGG(x1, x2, x3, x4)

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

ACKERMANN1_IN_GGG(s(s(T19)), 0, T20) → U17_GGG(T19, T20, ackermannc21_in_ga(T19))
U17_GGG(T19, T20, ackermannc21_out_ga(T19, T22)) → ACKERMANN1_IN_GGG(T19, T22, T20)
ACKERMANN1_IN_GGG(s(T68), s(T71), T70) → U20_GGG(T68, T71, T70, ackermannc57_in_gga(T68, T71))
U20_GGG(T68, T71, T70, ackermannc57_out_gga(T68, T71, T73)) → ACKERMANN1_IN_GGG(T68, T73, T70)
ACKERMANN1_IN_GGG(s(T123), s(0), T117) → U23_GGG(T123, T117, ackermannc27_in_ga(T123))
U23_GGG(T123, T117, ackermannc27_out_ga(T123, T124)) → ACKERMANN1_IN_GGG(T123, T124, T117)
ACKERMANN1_IN_GGG(s(T131), s(s(T133)), T117) → U26_GGG(T131, T133, T117, ackermannc57_in_gga(T131, T133))
U26_GGG(T131, T133, T117, ackermannc57_out_gga(T131, T133, T135)) → U28_GGG(T131, T133, T117, ackermannc68_in_gga(T131, T135))
U28_GGG(T131, T133, T117, ackermannc68_out_gga(T131, T135, T139)) → ACKERMANN1_IN_GGG(T131, T139, T117)

The TRS R consists of the following rules:

ackermannc21_in_ga(T28) → U40_ga(T28, ackermannc27_in_ga(T28))
ackermannc57_in_gga(T79, 0) → U46_gga(T79, ackermannc27_in_ga(T79))
ackermannc57_in_gga(T84, s(T86)) → U47_gga(T84, T86, qc65_in_ggaa(T84, T86))
ackermannc27_in_ga(0) → ackermannc27_out_ga(0, s(s(0)))
ackermannc27_in_ga(s(T32)) → U41_ga(T32, ackermannc21_in_ga(T32))
ackermannc68_in_gga(0, T96) → ackermannc68_out_gga(0, T96, s(T96))
ackermannc68_in_gga(s(T101), 0) → U50_gga(T101, ackermannc27_in_ga(T101))
ackermannc68_in_gga(s(T106), s(T108)) → U51_gga(T106, T108, qc65_in_ggaa(T106, T108))
U40_ga(T28, ackermannc27_out_ga(T28, X73)) → ackermannc21_out_ga(T28, X73)
U46_gga(T79, ackermannc27_out_ga(T79, X211)) → ackermannc57_out_gga(T79, 0, X211)
U47_gga(T84, T86, qc65_out_ggaa(T84, T86, X228, X229)) → ackermannc57_out_gga(T84, s(T86), X229)
U41_ga(T32, ackermannc21_out_ga(T32, T34)) → U42_ga(T32, ackermannc38_in_gga(T32, T34))
U50_gga(T101, ackermannc27_out_ga(T101, X265)) → ackermannc68_out_gga(s(T101), 0, X265)
U51_gga(T106, T108, qc65_out_ggaa(T106, T108, X282, X283)) → ackermannc68_out_gga(s(T106), s(T108), X283)
qc65_in_ggaa(T84, T86) → U48_ggaa(T84, T86, ackermannc57_in_gga(T84, T86))
U42_ga(T32, ackermannc38_out_gga(T32, T34, X97)) → ackermannc27_out_ga(s(T32), X97)
U48_ggaa(T84, T86, ackermannc57_out_gga(T84, T86, T88)) → U49_ggaa(T84, T86, T88, ackermannc68_in_gga(T84, T88))
ackermannc38_in_gga(0, T42) → ackermannc38_out_gga(0, T42, s(T42))
ackermannc38_in_gga(s(T47), 0) → U43_gga(T47, ackermannc27_in_ga(T47))
ackermannc38_in_gga(s(T52), s(T53)) → U44_gga(T52, T53, ackermannc38_in_gga(s(T52), T53))
U49_ggaa(T84, T86, T88, ackermannc68_out_gga(T84, T88, X229)) → qc65_out_ggaa(T84, T86, T88, X229)
U43_gga(T47, ackermannc27_out_ga(T47, X133)) → ackermannc38_out_gga(s(T47), 0, X133)
U44_gga(T52, T53, ackermannc38_out_gga(s(T52), T53, T55)) → U45_gga(T52, T53, ackermannc38_in_gga(T52, T55))
U45_gga(T52, T53, ackermannc38_out_gga(T52, T55, X151)) → ackermannc38_out_gga(s(T52), s(T53), X151)

The set Q consists of the following terms:

ackermannc21_in_ga(x0)
ackermannc57_in_gga(x0, x1)
ackermannc27_in_ga(x0)
ackermannc68_in_gga(x0, x1)
U40_ga(x0, x1)
U46_gga(x0, x1)
U47_gga(x0, x1, x2)
U41_ga(x0, x1)
U50_gga(x0, x1)
U51_gga(x0, x1, x2)
qc65_in_ggaa(x0, x1)
U42_ga(x0, x1)
U48_ggaa(x0, x1, x2)
ackermannc38_in_gga(x0, x1)
U49_ggaa(x0, x1, x2, x3)
U43_gga(x0, x1)
U44_gga(x0, x1, x2)
U45_gga(x0, x1, x2)

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

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

  • U17_GGG(T19, T20, ackermannc21_out_ga(T19, T22)) → ACKERMANN1_IN_GGG(T19, T22, T20)
    The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2, 2 >= 3

  • ACKERMANN1_IN_GGG(s(s(T19)), 0, T20) → U17_GGG(T19, T20, ackermannc21_in_ga(T19))
    The graph contains the following edges 1 > 1, 3 >= 2

  • U26_GGG(T131, T133, T117, ackermannc57_out_gga(T131, T133, T135)) → U28_GGG(T131, T133, T117, ackermannc68_in_gga(T131, T135))
    The graph contains the following edges 1 >= 1, 4 > 1, 2 >= 2, 4 > 2, 3 >= 3

  • U20_GGG(T68, T71, T70, ackermannc57_out_gga(T68, T71, T73)) → ACKERMANN1_IN_GGG(T68, T73, T70)
    The graph contains the following edges 1 >= 1, 4 > 1, 4 > 2, 3 >= 3

  • ACKERMANN1_IN_GGG(s(T68), s(T71), T70) → U20_GGG(T68, T71, T70, ackermannc57_in_gga(T68, T71))
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

  • U23_GGG(T123, T117, ackermannc27_out_ga(T123, T124)) → ACKERMANN1_IN_GGG(T123, T124, T117)
    The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2, 2 >= 3

  • U28_GGG(T131, T133, T117, ackermannc68_out_gga(T131, T135, T139)) → ACKERMANN1_IN_GGG(T131, T139, T117)
    The graph contains the following edges 1 >= 1, 4 > 1, 4 > 2, 3 >= 3

  • ACKERMANN1_IN_GGG(s(T123), s(0), T117) → U23_GGG(T123, T117, ackermannc27_in_ga(T123))
    The graph contains the following edges 1 > 1, 3 >= 2

  • ACKERMANN1_IN_GGG(s(T131), s(s(T133)), T117) → U26_GGG(T131, T133, T117, ackermannc57_in_gga(T131, T133))
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

(34) YES