(0) Obligation:

Clauses:

isNat(s(X)) :- isNat(X).
isNat(0).
notEq(s(X), s(Y)) :- notEq(X, Y).
notEq(s(X), 0).
notEq(0, s(X)).
lt(s(X), s(Y)) :- lt(X, Y).
lt(0, s(Y)).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(X), 0).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(Y)).
le(0, 0).
even(s(X)) :- odd(X).
even(0).
odd(s(X)) :- even(X).
odd(s(0)).
add(s(X), Y, s(Z)) :- add(X, Y, Z).
add(0, X, X).
mult(s(X), Y, R) :- ','(mult(X, Y, Z), add(Y, Z, R)).
mult(0, Y, 0).
factorial(s(X), R) :- ','(factorial(X, Y), mult(s(X), Y, R)).
factorial(0, s(0)).

Queries:

factorial(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

factorial10(s(T20), X53) :- factorial10(T20, X52).
factorial10(s(T20), X53) :- ','(factorialc10(T20, T22), mult18(T20, T22, X53)).
p22(s(T53), T54, X134, X101) :- p22(T53, T54, X133, X134).
p22(T38, T39, T42, X101) :- ','(multc23(T38, T39, T42), add24(T39, T42, X101)).
add24(s(T70), T71, s(X170)) :- add24(T70, T71, X170).
mult18(T38, T39, X101) :- p22(T38, T39, X100, X101).
add52(s(T127), T128, s(T130)) :- add52(T127, T128, T130).
factorial1(s(s(T12)), T7) :- factorial10(T12, X24).
factorial1(s(s(T12)), T7) :- ','(factorialc10(T12, T14), mult18(T12, T14, X25)).
factorial1(s(s(T103)), T106) :- ','(factorialc10(T103, T14), ','(multc18(T103, T14, T104), mult18(T103, T104, X224))).
factorial1(s(s(T103)), T106) :- ','(factorialc10(T103, T14), ','(multc18(T103, T14, T104), ','(multc18(T103, T104, T109), add52(T104, T109, T106)))).

Clauses:

factorialc10(s(T20), X53) :- ','(factorialc10(T20, T22), multc18(T20, T22, X53)).
factorialc10(0, s(0)).
qc22(T38, T39, T42, X101) :- ','(multc23(T38, T39, T42), addc24(T39, T42, X101)).
addc24(s(T70), T71, s(X170)) :- addc24(T70, T71, X170).
addc24(0, T76, T76).
multc18(T38, T39, X101) :- qc22(T38, T39, X100, X101).
addc52(s(T127), T128, s(T130)) :- addc52(T127, T128, T130).
addc52(0, T136, T136).
multc23(s(T53), T54, X134) :- qc22(T53, T54, X133, X134).
multc23(0, T59, 0).
multc70(0).

Afs:

factorial1(x1, x2)  =  factorial1(x1)

(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:
factorial1_in: (b,f)
factorial10_in: (b,f)
factorialc10_in: (b,f)
multc18_in: (b,b,f)
qc22_in: (b,b,f,f)
multc23_in: (b,b,f)
addc24_in: (b,b,f)
mult18_in: (b,b,f)
p22_in: (b,b,f,f)
add24_in: (b,b,f)
add52_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

FACTORIAL1_IN_GA(s(s(T12)), T7) → U10_GA(T12, T7, factorial10_in_ga(T12, X24))
FACTORIAL1_IN_GA(s(s(T12)), T7) → FACTORIAL10_IN_GA(T12, X24)
FACTORIAL10_IN_GA(s(T20), X53) → U1_GA(T20, X53, factorial10_in_ga(T20, X52))
FACTORIAL10_IN_GA(s(T20), X53) → FACTORIAL10_IN_GA(T20, X52)
FACTORIAL10_IN_GA(s(T20), X53) → U2_GA(T20, X53, factorialc10_in_ga(T20, T22))
U2_GA(T20, X53, factorialc10_out_ga(T20, T22)) → U3_GA(T20, X53, mult18_in_gga(T20, T22, X53))
U2_GA(T20, X53, factorialc10_out_ga(T20, T22)) → MULT18_IN_GGA(T20, T22, X53)
MULT18_IN_GGA(T38, T39, X101) → U8_GGA(T38, T39, X101, p22_in_ggaa(T38, T39, X100, X101))
MULT18_IN_GGA(T38, T39, X101) → P22_IN_GGAA(T38, T39, X100, X101)
P22_IN_GGAA(s(T53), T54, X134, X101) → U4_GGAA(T53, T54, X134, X101, p22_in_ggaa(T53, T54, X133, X134))
P22_IN_GGAA(s(T53), T54, X134, X101) → P22_IN_GGAA(T53, T54, X133, X134)
P22_IN_GGAA(T38, T39, T42, X101) → U5_GGAA(T38, T39, T42, X101, multc23_in_gga(T38, T39, T42))
U5_GGAA(T38, T39, T42, X101, multc23_out_gga(T38, T39, T42)) → U6_GGAA(T38, T39, T42, X101, add24_in_gga(T39, T42, X101))
U5_GGAA(T38, T39, T42, X101, multc23_out_gga(T38, T39, T42)) → ADD24_IN_GGA(T39, T42, X101)
ADD24_IN_GGA(s(T70), T71, s(X170)) → U7_GGA(T70, T71, X170, add24_in_gga(T70, T71, X170))
ADD24_IN_GGA(s(T70), T71, s(X170)) → ADD24_IN_GGA(T70, T71, X170)
FACTORIAL1_IN_GA(s(s(T12)), T7) → U11_GA(T12, T7, factorialc10_in_ga(T12, T14))
U11_GA(T12, T7, factorialc10_out_ga(T12, T14)) → U12_GA(T12, T7, mult18_in_gga(T12, T14, X25))
U11_GA(T12, T7, factorialc10_out_ga(T12, T14)) → MULT18_IN_GGA(T12, T14, X25)
FACTORIAL1_IN_GA(s(s(T103)), T106) → U13_GA(T103, T106, factorialc10_in_ga(T103, T14))
U13_GA(T103, T106, factorialc10_out_ga(T103, T14)) → U14_GA(T103, T106, multc18_in_gga(T103, T14, T104))
U14_GA(T103, T106, multc18_out_gga(T103, T14, T104)) → U15_GA(T103, T106, mult18_in_gga(T103, T104, X224))
U14_GA(T103, T106, multc18_out_gga(T103, T14, T104)) → MULT18_IN_GGA(T103, T104, X224)
U14_GA(T103, T106, multc18_out_gga(T103, T14, T104)) → U16_GA(T103, T106, T104, multc18_in_gga(T103, T104, T109))
U16_GA(T103, T106, T104, multc18_out_gga(T103, T104, T109)) → U17_GA(T103, T106, add52_in_gga(T104, T109, T106))
U16_GA(T103, T106, T104, multc18_out_gga(T103, T104, T109)) → ADD52_IN_GGA(T104, T109, T106)
ADD52_IN_GGA(s(T127), T128, s(T130)) → U9_GGA(T127, T128, T130, add52_in_gga(T127, T128, T130))
ADD52_IN_GGA(s(T127), T128, s(T130)) → ADD52_IN_GGA(T127, T128, T130)

The TRS R consists of the following rules:

factorialc10_in_ga(s(T20), X53) → U19_ga(T20, X53, factorialc10_in_ga(T20, T22))
factorialc10_in_ga(0, s(0)) → factorialc10_out_ga(0, s(0))
U19_ga(T20, X53, factorialc10_out_ga(T20, T22)) → U20_ga(T20, X53, multc18_in_gga(T20, T22, X53))
multc18_in_gga(T38, T39, X101) → U24_gga(T38, T39, X101, qc22_in_ggaa(T38, T39, X100, X101))
qc22_in_ggaa(T38, T39, T42, X101) → U21_ggaa(T38, T39, T42, X101, multc23_in_gga(T38, T39, T42))
multc23_in_gga(s(T53), T54, X134) → U26_gga(T53, T54, X134, qc22_in_ggaa(T53, T54, X133, X134))
U26_gga(T53, T54, X134, qc22_out_ggaa(T53, T54, X133, X134)) → multc23_out_gga(s(T53), T54, X134)
multc23_in_gga(0, T59, 0) → multc23_out_gga(0, T59, 0)
U21_ggaa(T38, T39, T42, X101, multc23_out_gga(T38, T39, T42)) → U22_ggaa(T38, T39, T42, X101, addc24_in_gga(T39, T42, X101))
addc24_in_gga(s(T70), T71, s(X170)) → U23_gga(T70, T71, X170, addc24_in_gga(T70, T71, X170))
addc24_in_gga(0, T76, T76) → addc24_out_gga(0, T76, T76)
U23_gga(T70, T71, X170, addc24_out_gga(T70, T71, X170)) → addc24_out_gga(s(T70), T71, s(X170))
U22_ggaa(T38, T39, T42, X101, addc24_out_gga(T39, T42, X101)) → qc22_out_ggaa(T38, T39, T42, X101)
U24_gga(T38, T39, X101, qc22_out_ggaa(T38, T39, X100, X101)) → multc18_out_gga(T38, T39, X101)
U20_ga(T20, X53, multc18_out_gga(T20, T22, X53)) → factorialc10_out_ga(s(T20), X53)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
factorial10_in_ga(x1, x2)  =  factorial10_in_ga(x1)
factorialc10_in_ga(x1, x2)  =  factorialc10_in_ga(x1)
U19_ga(x1, x2, x3)  =  U19_ga(x1, x3)
0  =  0
factorialc10_out_ga(x1, x2)  =  factorialc10_out_ga(x1, x2)
U20_ga(x1, x2, x3)  =  U20_ga(x1, x3)
multc18_in_gga(x1, x2, x3)  =  multc18_in_gga(x1, x2)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
qc22_in_ggaa(x1, x2, x3, x4)  =  qc22_in_ggaa(x1, x2)
U21_ggaa(x1, x2, x3, x4, x5)  =  U21_ggaa(x1, x2, x5)
multc23_in_gga(x1, x2, x3)  =  multc23_in_gga(x1, x2)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
qc22_out_ggaa(x1, x2, x3, x4)  =  qc22_out_ggaa(x1, x2, x3, x4)
multc23_out_gga(x1, x2, x3)  =  multc23_out_gga(x1, x2, x3)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x3, x5)
addc24_in_gga(x1, x2, x3)  =  addc24_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x1, x2, x4)
addc24_out_gga(x1, x2, x3)  =  addc24_out_gga(x1, x2, x3)
multc18_out_gga(x1, x2, x3)  =  multc18_out_gga(x1, x2, x3)
mult18_in_gga(x1, x2, x3)  =  mult18_in_gga(x1, x2)
p22_in_ggaa(x1, x2, x3, x4)  =  p22_in_ggaa(x1, x2)
add24_in_gga(x1, x2, x3)  =  add24_in_gga(x1, x2)
add52_in_gga(x1, x2, x3)  =  add52_in_gga(x1, x2)
FACTORIAL1_IN_GA(x1, x2)  =  FACTORIAL1_IN_GA(x1)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
FACTORIAL10_IN_GA(x1, x2)  =  FACTORIAL10_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
MULT18_IN_GGA(x1, x2, x3)  =  MULT18_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
P22_IN_GGAA(x1, x2, x3, x4)  =  P22_IN_GGAA(x1, x2)
U4_GGAA(x1, x2, x3, x4, x5)  =  U4_GGAA(x1, x2, x5)
U5_GGAA(x1, x2, x3, x4, x5)  =  U5_GGAA(x1, x2, x5)
U6_GGAA(x1, x2, x3, x4, x5)  =  U6_GGAA(x1, x2, x5)
ADD24_IN_GGA(x1, x2, x3)  =  ADD24_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
U13_GA(x1, x2, x3)  =  U13_GA(x1, x3)
U14_GA(x1, x2, x3)  =  U14_GA(x1, x3)
U15_GA(x1, x2, x3)  =  U15_GA(x1, x3)
U16_GA(x1, x2, x3, x4)  =  U16_GA(x1, x3, x4)
U17_GA(x1, x2, x3)  =  U17_GA(x1, x3)
ADD52_IN_GGA(x1, x2, x3)  =  ADD52_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, 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:

FACTORIAL1_IN_GA(s(s(T12)), T7) → U10_GA(T12, T7, factorial10_in_ga(T12, X24))
FACTORIAL1_IN_GA(s(s(T12)), T7) → FACTORIAL10_IN_GA(T12, X24)
FACTORIAL10_IN_GA(s(T20), X53) → U1_GA(T20, X53, factorial10_in_ga(T20, X52))
FACTORIAL10_IN_GA(s(T20), X53) → FACTORIAL10_IN_GA(T20, X52)
FACTORIAL10_IN_GA(s(T20), X53) → U2_GA(T20, X53, factorialc10_in_ga(T20, T22))
U2_GA(T20, X53, factorialc10_out_ga(T20, T22)) → U3_GA(T20, X53, mult18_in_gga(T20, T22, X53))
U2_GA(T20, X53, factorialc10_out_ga(T20, T22)) → MULT18_IN_GGA(T20, T22, X53)
MULT18_IN_GGA(T38, T39, X101) → U8_GGA(T38, T39, X101, p22_in_ggaa(T38, T39, X100, X101))
MULT18_IN_GGA(T38, T39, X101) → P22_IN_GGAA(T38, T39, X100, X101)
P22_IN_GGAA(s(T53), T54, X134, X101) → U4_GGAA(T53, T54, X134, X101, p22_in_ggaa(T53, T54, X133, X134))
P22_IN_GGAA(s(T53), T54, X134, X101) → P22_IN_GGAA(T53, T54, X133, X134)
P22_IN_GGAA(T38, T39, T42, X101) → U5_GGAA(T38, T39, T42, X101, multc23_in_gga(T38, T39, T42))
U5_GGAA(T38, T39, T42, X101, multc23_out_gga(T38, T39, T42)) → U6_GGAA(T38, T39, T42, X101, add24_in_gga(T39, T42, X101))
U5_GGAA(T38, T39, T42, X101, multc23_out_gga(T38, T39, T42)) → ADD24_IN_GGA(T39, T42, X101)
ADD24_IN_GGA(s(T70), T71, s(X170)) → U7_GGA(T70, T71, X170, add24_in_gga(T70, T71, X170))
ADD24_IN_GGA(s(T70), T71, s(X170)) → ADD24_IN_GGA(T70, T71, X170)
FACTORIAL1_IN_GA(s(s(T12)), T7) → U11_GA(T12, T7, factorialc10_in_ga(T12, T14))
U11_GA(T12, T7, factorialc10_out_ga(T12, T14)) → U12_GA(T12, T7, mult18_in_gga(T12, T14, X25))
U11_GA(T12, T7, factorialc10_out_ga(T12, T14)) → MULT18_IN_GGA(T12, T14, X25)
FACTORIAL1_IN_GA(s(s(T103)), T106) → U13_GA(T103, T106, factorialc10_in_ga(T103, T14))
U13_GA(T103, T106, factorialc10_out_ga(T103, T14)) → U14_GA(T103, T106, multc18_in_gga(T103, T14, T104))
U14_GA(T103, T106, multc18_out_gga(T103, T14, T104)) → U15_GA(T103, T106, mult18_in_gga(T103, T104, X224))
U14_GA(T103, T106, multc18_out_gga(T103, T14, T104)) → MULT18_IN_GGA(T103, T104, X224)
U14_GA(T103, T106, multc18_out_gga(T103, T14, T104)) → U16_GA(T103, T106, T104, multc18_in_gga(T103, T104, T109))
U16_GA(T103, T106, T104, multc18_out_gga(T103, T104, T109)) → U17_GA(T103, T106, add52_in_gga(T104, T109, T106))
U16_GA(T103, T106, T104, multc18_out_gga(T103, T104, T109)) → ADD52_IN_GGA(T104, T109, T106)
ADD52_IN_GGA(s(T127), T128, s(T130)) → U9_GGA(T127, T128, T130, add52_in_gga(T127, T128, T130))
ADD52_IN_GGA(s(T127), T128, s(T130)) → ADD52_IN_GGA(T127, T128, T130)

The TRS R consists of the following rules:

factorialc10_in_ga(s(T20), X53) → U19_ga(T20, X53, factorialc10_in_ga(T20, T22))
factorialc10_in_ga(0, s(0)) → factorialc10_out_ga(0, s(0))
U19_ga(T20, X53, factorialc10_out_ga(T20, T22)) → U20_ga(T20, X53, multc18_in_gga(T20, T22, X53))
multc18_in_gga(T38, T39, X101) → U24_gga(T38, T39, X101, qc22_in_ggaa(T38, T39, X100, X101))
qc22_in_ggaa(T38, T39, T42, X101) → U21_ggaa(T38, T39, T42, X101, multc23_in_gga(T38, T39, T42))
multc23_in_gga(s(T53), T54, X134) → U26_gga(T53, T54, X134, qc22_in_ggaa(T53, T54, X133, X134))
U26_gga(T53, T54, X134, qc22_out_ggaa(T53, T54, X133, X134)) → multc23_out_gga(s(T53), T54, X134)
multc23_in_gga(0, T59, 0) → multc23_out_gga(0, T59, 0)
U21_ggaa(T38, T39, T42, X101, multc23_out_gga(T38, T39, T42)) → U22_ggaa(T38, T39, T42, X101, addc24_in_gga(T39, T42, X101))
addc24_in_gga(s(T70), T71, s(X170)) → U23_gga(T70, T71, X170, addc24_in_gga(T70, T71, X170))
addc24_in_gga(0, T76, T76) → addc24_out_gga(0, T76, T76)
U23_gga(T70, T71, X170, addc24_out_gga(T70, T71, X170)) → addc24_out_gga(s(T70), T71, s(X170))
U22_ggaa(T38, T39, T42, X101, addc24_out_gga(T39, T42, X101)) → qc22_out_ggaa(T38, T39, T42, X101)
U24_gga(T38, T39, X101, qc22_out_ggaa(T38, T39, X100, X101)) → multc18_out_gga(T38, T39, X101)
U20_ga(T20, X53, multc18_out_gga(T20, T22, X53)) → factorialc10_out_ga(s(T20), X53)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
factorial10_in_ga(x1, x2)  =  factorial10_in_ga(x1)
factorialc10_in_ga(x1, x2)  =  factorialc10_in_ga(x1)
U19_ga(x1, x2, x3)  =  U19_ga(x1, x3)
0  =  0
factorialc10_out_ga(x1, x2)  =  factorialc10_out_ga(x1, x2)
U20_ga(x1, x2, x3)  =  U20_ga(x1, x3)
multc18_in_gga(x1, x2, x3)  =  multc18_in_gga(x1, x2)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
qc22_in_ggaa(x1, x2, x3, x4)  =  qc22_in_ggaa(x1, x2)
U21_ggaa(x1, x2, x3, x4, x5)  =  U21_ggaa(x1, x2, x5)
multc23_in_gga(x1, x2, x3)  =  multc23_in_gga(x1, x2)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
qc22_out_ggaa(x1, x2, x3, x4)  =  qc22_out_ggaa(x1, x2, x3, x4)
multc23_out_gga(x1, x2, x3)  =  multc23_out_gga(x1, x2, x3)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x3, x5)
addc24_in_gga(x1, x2, x3)  =  addc24_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x1, x2, x4)
addc24_out_gga(x1, x2, x3)  =  addc24_out_gga(x1, x2, x3)
multc18_out_gga(x1, x2, x3)  =  multc18_out_gga(x1, x2, x3)
mult18_in_gga(x1, x2, x3)  =  mult18_in_gga(x1, x2)
p22_in_ggaa(x1, x2, x3, x4)  =  p22_in_ggaa(x1, x2)
add24_in_gga(x1, x2, x3)  =  add24_in_gga(x1, x2)
add52_in_gga(x1, x2, x3)  =  add52_in_gga(x1, x2)
FACTORIAL1_IN_GA(x1, x2)  =  FACTORIAL1_IN_GA(x1)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
FACTORIAL10_IN_GA(x1, x2)  =  FACTORIAL10_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
MULT18_IN_GGA(x1, x2, x3)  =  MULT18_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
P22_IN_GGAA(x1, x2, x3, x4)  =  P22_IN_GGAA(x1, x2)
U4_GGAA(x1, x2, x3, x4, x5)  =  U4_GGAA(x1, x2, x5)
U5_GGAA(x1, x2, x3, x4, x5)  =  U5_GGAA(x1, x2, x5)
U6_GGAA(x1, x2, x3, x4, x5)  =  U6_GGAA(x1, x2, x5)
ADD24_IN_GGA(x1, x2, x3)  =  ADD24_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
U13_GA(x1, x2, x3)  =  U13_GA(x1, x3)
U14_GA(x1, x2, x3)  =  U14_GA(x1, x3)
U15_GA(x1, x2, x3)  =  U15_GA(x1, x3)
U16_GA(x1, x2, x3, x4)  =  U16_GA(x1, x3, x4)
U17_GA(x1, x2, x3)  =  U17_GA(x1, x3)
ADD52_IN_GGA(x1, x2, x3)  =  ADD52_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, 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 24 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

ADD52_IN_GGA(s(T127), T128, s(T130)) → ADD52_IN_GGA(T127, T128, T130)

The TRS R consists of the following rules:

factorialc10_in_ga(s(T20), X53) → U19_ga(T20, X53, factorialc10_in_ga(T20, T22))
factorialc10_in_ga(0, s(0)) → factorialc10_out_ga(0, s(0))
U19_ga(T20, X53, factorialc10_out_ga(T20, T22)) → U20_ga(T20, X53, multc18_in_gga(T20, T22, X53))
multc18_in_gga(T38, T39, X101) → U24_gga(T38, T39, X101, qc22_in_ggaa(T38, T39, X100, X101))
qc22_in_ggaa(T38, T39, T42, X101) → U21_ggaa(T38, T39, T42, X101, multc23_in_gga(T38, T39, T42))
multc23_in_gga(s(T53), T54, X134) → U26_gga(T53, T54, X134, qc22_in_ggaa(T53, T54, X133, X134))
U26_gga(T53, T54, X134, qc22_out_ggaa(T53, T54, X133, X134)) → multc23_out_gga(s(T53), T54, X134)
multc23_in_gga(0, T59, 0) → multc23_out_gga(0, T59, 0)
U21_ggaa(T38, T39, T42, X101, multc23_out_gga(T38, T39, T42)) → U22_ggaa(T38, T39, T42, X101, addc24_in_gga(T39, T42, X101))
addc24_in_gga(s(T70), T71, s(X170)) → U23_gga(T70, T71, X170, addc24_in_gga(T70, T71, X170))
addc24_in_gga(0, T76, T76) → addc24_out_gga(0, T76, T76)
U23_gga(T70, T71, X170, addc24_out_gga(T70, T71, X170)) → addc24_out_gga(s(T70), T71, s(X170))
U22_ggaa(T38, T39, T42, X101, addc24_out_gga(T39, T42, X101)) → qc22_out_ggaa(T38, T39, T42, X101)
U24_gga(T38, T39, X101, qc22_out_ggaa(T38, T39, X100, X101)) → multc18_out_gga(T38, T39, X101)
U20_ga(T20, X53, multc18_out_gga(T20, T22, X53)) → factorialc10_out_ga(s(T20), X53)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
factorialc10_in_ga(x1, x2)  =  factorialc10_in_ga(x1)
U19_ga(x1, x2, x3)  =  U19_ga(x1, x3)
0  =  0
factorialc10_out_ga(x1, x2)  =  factorialc10_out_ga(x1, x2)
U20_ga(x1, x2, x3)  =  U20_ga(x1, x3)
multc18_in_gga(x1, x2, x3)  =  multc18_in_gga(x1, x2)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
qc22_in_ggaa(x1, x2, x3, x4)  =  qc22_in_ggaa(x1, x2)
U21_ggaa(x1, x2, x3, x4, x5)  =  U21_ggaa(x1, x2, x5)
multc23_in_gga(x1, x2, x3)  =  multc23_in_gga(x1, x2)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
qc22_out_ggaa(x1, x2, x3, x4)  =  qc22_out_ggaa(x1, x2, x3, x4)
multc23_out_gga(x1, x2, x3)  =  multc23_out_gga(x1, x2, x3)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x3, x5)
addc24_in_gga(x1, x2, x3)  =  addc24_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x1, x2, x4)
addc24_out_gga(x1, x2, x3)  =  addc24_out_gga(x1, x2, x3)
multc18_out_gga(x1, x2, x3)  =  multc18_out_gga(x1, x2, x3)
ADD52_IN_GGA(x1, x2, x3)  =  ADD52_IN_GGA(x1, x2)

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:

ADD52_IN_GGA(s(T127), T128, s(T130)) → ADD52_IN_GGA(T127, T128, T130)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

ADD52_IN_GGA(s(T127), T128) → ADD52_IN_GGA(T127, T128)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • ADD52_IN_GGA(s(T127), T128) → ADD52_IN_GGA(T127, T128)
    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:

ADD24_IN_GGA(s(T70), T71, s(X170)) → ADD24_IN_GGA(T70, T71, X170)

The TRS R consists of the following rules:

factorialc10_in_ga(s(T20), X53) → U19_ga(T20, X53, factorialc10_in_ga(T20, T22))
factorialc10_in_ga(0, s(0)) → factorialc10_out_ga(0, s(0))
U19_ga(T20, X53, factorialc10_out_ga(T20, T22)) → U20_ga(T20, X53, multc18_in_gga(T20, T22, X53))
multc18_in_gga(T38, T39, X101) → U24_gga(T38, T39, X101, qc22_in_ggaa(T38, T39, X100, X101))
qc22_in_ggaa(T38, T39, T42, X101) → U21_ggaa(T38, T39, T42, X101, multc23_in_gga(T38, T39, T42))
multc23_in_gga(s(T53), T54, X134) → U26_gga(T53, T54, X134, qc22_in_ggaa(T53, T54, X133, X134))
U26_gga(T53, T54, X134, qc22_out_ggaa(T53, T54, X133, X134)) → multc23_out_gga(s(T53), T54, X134)
multc23_in_gga(0, T59, 0) → multc23_out_gga(0, T59, 0)
U21_ggaa(T38, T39, T42, X101, multc23_out_gga(T38, T39, T42)) → U22_ggaa(T38, T39, T42, X101, addc24_in_gga(T39, T42, X101))
addc24_in_gga(s(T70), T71, s(X170)) → U23_gga(T70, T71, X170, addc24_in_gga(T70, T71, X170))
addc24_in_gga(0, T76, T76) → addc24_out_gga(0, T76, T76)
U23_gga(T70, T71, X170, addc24_out_gga(T70, T71, X170)) → addc24_out_gga(s(T70), T71, s(X170))
U22_ggaa(T38, T39, T42, X101, addc24_out_gga(T39, T42, X101)) → qc22_out_ggaa(T38, T39, T42, X101)
U24_gga(T38, T39, X101, qc22_out_ggaa(T38, T39, X100, X101)) → multc18_out_gga(T38, T39, X101)
U20_ga(T20, X53, multc18_out_gga(T20, T22, X53)) → factorialc10_out_ga(s(T20), X53)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
factorialc10_in_ga(x1, x2)  =  factorialc10_in_ga(x1)
U19_ga(x1, x2, x3)  =  U19_ga(x1, x3)
0  =  0
factorialc10_out_ga(x1, x2)  =  factorialc10_out_ga(x1, x2)
U20_ga(x1, x2, x3)  =  U20_ga(x1, x3)
multc18_in_gga(x1, x2, x3)  =  multc18_in_gga(x1, x2)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
qc22_in_ggaa(x1, x2, x3, x4)  =  qc22_in_ggaa(x1, x2)
U21_ggaa(x1, x2, x3, x4, x5)  =  U21_ggaa(x1, x2, x5)
multc23_in_gga(x1, x2, x3)  =  multc23_in_gga(x1, x2)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
qc22_out_ggaa(x1, x2, x3, x4)  =  qc22_out_ggaa(x1, x2, x3, x4)
multc23_out_gga(x1, x2, x3)  =  multc23_out_gga(x1, x2, x3)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x3, x5)
addc24_in_gga(x1, x2, x3)  =  addc24_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x1, x2, x4)
addc24_out_gga(x1, x2, x3)  =  addc24_out_gga(x1, x2, x3)
multc18_out_gga(x1, x2, x3)  =  multc18_out_gga(x1, x2, x3)
ADD24_IN_GGA(x1, x2, x3)  =  ADD24_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:

ADD24_IN_GGA(s(T70), T71, s(X170)) → ADD24_IN_GGA(T70, T71, X170)

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

ADD24_IN_GGA(s(T70), T71) → ADD24_IN_GGA(T70, T71)

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:

  • ADD24_IN_GGA(s(T70), T71) → ADD24_IN_GGA(T70, T71)
    The graph contains the following edges 1 > 1, 2 >= 2

(20) YES

(21) Obligation:

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

P22_IN_GGAA(s(T53), T54, X134, X101) → P22_IN_GGAA(T53, T54, X133, X134)

The TRS R consists of the following rules:

factorialc10_in_ga(s(T20), X53) → U19_ga(T20, X53, factorialc10_in_ga(T20, T22))
factorialc10_in_ga(0, s(0)) → factorialc10_out_ga(0, s(0))
U19_ga(T20, X53, factorialc10_out_ga(T20, T22)) → U20_ga(T20, X53, multc18_in_gga(T20, T22, X53))
multc18_in_gga(T38, T39, X101) → U24_gga(T38, T39, X101, qc22_in_ggaa(T38, T39, X100, X101))
qc22_in_ggaa(T38, T39, T42, X101) → U21_ggaa(T38, T39, T42, X101, multc23_in_gga(T38, T39, T42))
multc23_in_gga(s(T53), T54, X134) → U26_gga(T53, T54, X134, qc22_in_ggaa(T53, T54, X133, X134))
U26_gga(T53, T54, X134, qc22_out_ggaa(T53, T54, X133, X134)) → multc23_out_gga(s(T53), T54, X134)
multc23_in_gga(0, T59, 0) → multc23_out_gga(0, T59, 0)
U21_ggaa(T38, T39, T42, X101, multc23_out_gga(T38, T39, T42)) → U22_ggaa(T38, T39, T42, X101, addc24_in_gga(T39, T42, X101))
addc24_in_gga(s(T70), T71, s(X170)) → U23_gga(T70, T71, X170, addc24_in_gga(T70, T71, X170))
addc24_in_gga(0, T76, T76) → addc24_out_gga(0, T76, T76)
U23_gga(T70, T71, X170, addc24_out_gga(T70, T71, X170)) → addc24_out_gga(s(T70), T71, s(X170))
U22_ggaa(T38, T39, T42, X101, addc24_out_gga(T39, T42, X101)) → qc22_out_ggaa(T38, T39, T42, X101)
U24_gga(T38, T39, X101, qc22_out_ggaa(T38, T39, X100, X101)) → multc18_out_gga(T38, T39, X101)
U20_ga(T20, X53, multc18_out_gga(T20, T22, X53)) → factorialc10_out_ga(s(T20), X53)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
factorialc10_in_ga(x1, x2)  =  factorialc10_in_ga(x1)
U19_ga(x1, x2, x3)  =  U19_ga(x1, x3)
0  =  0
factorialc10_out_ga(x1, x2)  =  factorialc10_out_ga(x1, x2)
U20_ga(x1, x2, x3)  =  U20_ga(x1, x3)
multc18_in_gga(x1, x2, x3)  =  multc18_in_gga(x1, x2)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
qc22_in_ggaa(x1, x2, x3, x4)  =  qc22_in_ggaa(x1, x2)
U21_ggaa(x1, x2, x3, x4, x5)  =  U21_ggaa(x1, x2, x5)
multc23_in_gga(x1, x2, x3)  =  multc23_in_gga(x1, x2)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
qc22_out_ggaa(x1, x2, x3, x4)  =  qc22_out_ggaa(x1, x2, x3, x4)
multc23_out_gga(x1, x2, x3)  =  multc23_out_gga(x1, x2, x3)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x3, x5)
addc24_in_gga(x1, x2, x3)  =  addc24_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x1, x2, x4)
addc24_out_gga(x1, x2, x3)  =  addc24_out_gga(x1, x2, x3)
multc18_out_gga(x1, x2, x3)  =  multc18_out_gga(x1, x2, x3)
P22_IN_GGAA(x1, x2, x3, x4)  =  P22_IN_GGAA(x1, x2)

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:

P22_IN_GGAA(s(T53), T54, X134, X101) → P22_IN_GGAA(T53, T54, X133, X134)

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

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:

P22_IN_GGAA(s(T53), T54) → P22_IN_GGAA(T53, T54)

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

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

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

(27) YES

(28) Obligation:

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

FACTORIAL10_IN_GA(s(T20), X53) → FACTORIAL10_IN_GA(T20, X52)

The TRS R consists of the following rules:

factorialc10_in_ga(s(T20), X53) → U19_ga(T20, X53, factorialc10_in_ga(T20, T22))
factorialc10_in_ga(0, s(0)) → factorialc10_out_ga(0, s(0))
U19_ga(T20, X53, factorialc10_out_ga(T20, T22)) → U20_ga(T20, X53, multc18_in_gga(T20, T22, X53))
multc18_in_gga(T38, T39, X101) → U24_gga(T38, T39, X101, qc22_in_ggaa(T38, T39, X100, X101))
qc22_in_ggaa(T38, T39, T42, X101) → U21_ggaa(T38, T39, T42, X101, multc23_in_gga(T38, T39, T42))
multc23_in_gga(s(T53), T54, X134) → U26_gga(T53, T54, X134, qc22_in_ggaa(T53, T54, X133, X134))
U26_gga(T53, T54, X134, qc22_out_ggaa(T53, T54, X133, X134)) → multc23_out_gga(s(T53), T54, X134)
multc23_in_gga(0, T59, 0) → multc23_out_gga(0, T59, 0)
U21_ggaa(T38, T39, T42, X101, multc23_out_gga(T38, T39, T42)) → U22_ggaa(T38, T39, T42, X101, addc24_in_gga(T39, T42, X101))
addc24_in_gga(s(T70), T71, s(X170)) → U23_gga(T70, T71, X170, addc24_in_gga(T70, T71, X170))
addc24_in_gga(0, T76, T76) → addc24_out_gga(0, T76, T76)
U23_gga(T70, T71, X170, addc24_out_gga(T70, T71, X170)) → addc24_out_gga(s(T70), T71, s(X170))
U22_ggaa(T38, T39, T42, X101, addc24_out_gga(T39, T42, X101)) → qc22_out_ggaa(T38, T39, T42, X101)
U24_gga(T38, T39, X101, qc22_out_ggaa(T38, T39, X100, X101)) → multc18_out_gga(T38, T39, X101)
U20_ga(T20, X53, multc18_out_gga(T20, T22, X53)) → factorialc10_out_ga(s(T20), X53)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
factorialc10_in_ga(x1, x2)  =  factorialc10_in_ga(x1)
U19_ga(x1, x2, x3)  =  U19_ga(x1, x3)
0  =  0
factorialc10_out_ga(x1, x2)  =  factorialc10_out_ga(x1, x2)
U20_ga(x1, x2, x3)  =  U20_ga(x1, x3)
multc18_in_gga(x1, x2, x3)  =  multc18_in_gga(x1, x2)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
qc22_in_ggaa(x1, x2, x3, x4)  =  qc22_in_ggaa(x1, x2)
U21_ggaa(x1, x2, x3, x4, x5)  =  U21_ggaa(x1, x2, x5)
multc23_in_gga(x1, x2, x3)  =  multc23_in_gga(x1, x2)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
qc22_out_ggaa(x1, x2, x3, x4)  =  qc22_out_ggaa(x1, x2, x3, x4)
multc23_out_gga(x1, x2, x3)  =  multc23_out_gga(x1, x2, x3)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x3, x5)
addc24_in_gga(x1, x2, x3)  =  addc24_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x1, x2, x4)
addc24_out_gga(x1, x2, x3)  =  addc24_out_gga(x1, x2, x3)
multc18_out_gga(x1, x2, x3)  =  multc18_out_gga(x1, x2, x3)
FACTORIAL10_IN_GA(x1, x2)  =  FACTORIAL10_IN_GA(x1)

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:

FACTORIAL10_IN_GA(s(T20), X53) → FACTORIAL10_IN_GA(T20, X52)

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

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:

FACTORIAL10_IN_GA(s(T20)) → FACTORIAL10_IN_GA(T20)

R is empty.
Q is empty.
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:

  • FACTORIAL10_IN_GA(s(T20)) → FACTORIAL10_IN_GA(T20)
    The graph contains the following edges 1 > 1

(34) YES