(0) Obligation:

Clauses:

log2(X, Y) :- log2(X, 0, Y).
log2(0, I, I).
log2(s(0), I, I).
log2(s(s(X)), I, Y) :- ','(half(s(s(X)), X1), log2(X1, s(I), Y)).
half(0, 0).
half(s(0), 0).
half(s(s(X)), s(Y)) :- half(X, Y).

Queries:

log2(a,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

half22(s(s(T26)), s(X55)) :- half22(T26, X55).
half17(T22, s(X46)) :- half22(T22, X46).
p139(T85, X286, T88, T86) :- half17(T85, X286).
p139(T85, s(s(T110)), T111, T112) :- ','(halfc17(T85, s(s(T110))), p139(T110, X323, s(T111), T112)).
log21(s(s(T14)), T13) :- half17(T14, X28).
log21(s(s(T14)), T32) :- ','(halfc17(T14, s(s(T31))), half17(T31, X82)).
log21(s(s(T14)), T41) :- ','(halfc17(T14, s(s(T31))), ','(halfc17(T31, s(s(T40))), half17(T40, X116))).
log21(s(s(T14)), T50) :- ','(halfc17(T14, s(s(T31))), ','(halfc17(T31, s(s(T40))), ','(halfc17(T40, s(s(T49))), half17(T49, X150)))).
log21(s(s(T14)), T59) :- ','(halfc17(T14, s(s(T31))), ','(halfc17(T31, s(s(T40))), ','(halfc17(T40, s(s(T49))), ','(halfc17(T49, s(s(T58))), half17(T58, X184))))).
log21(s(s(T14)), T68) :- ','(halfc17(T14, s(s(T31))), ','(halfc17(T31, s(s(T40))), ','(halfc17(T40, s(s(T49))), ','(halfc17(T49, s(s(T58))), ','(halfc17(T58, s(s(T67))), half17(T67, X218)))))).
log21(s(s(T14)), T77) :- ','(halfc17(T14, s(s(T31))), ','(halfc17(T31, s(s(T40))), ','(halfc17(T40, s(s(T49))), ','(halfc17(T49, s(s(T58))), ','(halfc17(T58, s(s(T67))), ','(halfc17(T67, s(s(T76))), half17(T76, X252))))))).
log21(s(s(T14)), T86) :- ','(halfc17(T14, s(s(T31))), ','(halfc17(T31, s(s(T40))), ','(halfc17(T40, s(s(T49))), ','(halfc17(T49, s(s(T58))), ','(halfc17(T58, s(s(T67))), ','(halfc17(T67, s(s(T76))), ','(halfc17(T76, s(s(T85))), p139(T85, X286, s(s(s(s(s(s(s(0))))))), T86)))))))).

Clauses:

halfc22(0, 0).
halfc22(s(0), 0).
halfc22(s(s(T26)), s(X55)) :- halfc22(T26, X55).
halfc17(T22, s(X46)) :- halfc22(T22, X46).
qc139(T85, 0, T98, s(T98)) :- halfc17(T85, 0).
qc139(T85, s(0), T103, s(T103)) :- halfc17(T85, s(0)).
qc139(T85, s(s(T110)), T111, T112) :- ','(halfc17(T85, s(s(T110))), qc139(T110, X323, s(T111), T112)).

Afs:

log21(x1, x2)  =  log21(x2)

(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:
log21_in: (f,b)
half17_in: (f,f) (b,f)
half22_in: (f,f) (b,f)
halfc17_in: (f,f) (b,f)
halfc22_in: (f,f) (b,f)
p139_in: (b,f,b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

LOG21_IN_AG(s(s(T14)), T13) → U6_AG(T14, T13, half17_in_aa(T14, X28))
LOG21_IN_AG(s(s(T14)), T13) → HALF17_IN_AA(T14, X28)
HALF17_IN_AA(T22, s(X46)) → U2_AA(T22, X46, half22_in_aa(T22, X46))
HALF17_IN_AA(T22, s(X46)) → HALF22_IN_AA(T22, X46)
HALF22_IN_AA(s(s(T26)), s(X55)) → U1_AA(T26, X55, half22_in_aa(T26, X55))
HALF22_IN_AA(s(s(T26)), s(X55)) → HALF22_IN_AA(T26, X55)
LOG21_IN_AG(s(s(T14)), T32) → U7_AG(T14, T32, halfc17_in_aa(T14, s(s(T31))))
U7_AG(T14, T32, halfc17_out_aa(T14, s(s(T31)))) → U8_AG(T14, T32, half17_in_ga(T31, X82))
U7_AG(T14, T32, halfc17_out_aa(T14, s(s(T31)))) → HALF17_IN_GA(T31, X82)
HALF17_IN_GA(T22, s(X46)) → U2_GA(T22, X46, half22_in_ga(T22, X46))
HALF17_IN_GA(T22, s(X46)) → HALF22_IN_GA(T22, X46)
HALF22_IN_GA(s(s(T26)), s(X55)) → U1_GA(T26, X55, half22_in_ga(T26, X55))
HALF22_IN_GA(s(s(T26)), s(X55)) → HALF22_IN_GA(T26, X55)
LOG21_IN_AG(s(s(T14)), T41) → U9_AG(T14, T41, halfc17_in_aa(T14, s(s(T31))))
U9_AG(T14, T41, halfc17_out_aa(T14, s(s(T31)))) → U10_AG(T14, T41, halfc17_in_ga(T31, s(s(T40))))
U10_AG(T14, T41, halfc17_out_ga(T31, s(s(T40)))) → U11_AG(T14, T41, half17_in_ga(T40, X116))
U10_AG(T14, T41, halfc17_out_ga(T31, s(s(T40)))) → HALF17_IN_GA(T40, X116)
LOG21_IN_AG(s(s(T14)), T50) → U12_AG(T14, T50, halfc17_in_aa(T14, s(s(T31))))
U12_AG(T14, T50, halfc17_out_aa(T14, s(s(T31)))) → U13_AG(T14, T50, halfc17_in_ga(T31, s(s(T40))))
U13_AG(T14, T50, halfc17_out_ga(T31, s(s(T40)))) → U14_AG(T14, T50, halfc17_in_ga(T40, s(s(T49))))
U14_AG(T14, T50, halfc17_out_ga(T40, s(s(T49)))) → U15_AG(T14, T50, half17_in_ga(T49, X150))
U14_AG(T14, T50, halfc17_out_ga(T40, s(s(T49)))) → HALF17_IN_GA(T49, X150)
LOG21_IN_AG(s(s(T14)), T59) → U16_AG(T14, T59, halfc17_in_aa(T14, s(s(T31))))
U16_AG(T14, T59, halfc17_out_aa(T14, s(s(T31)))) → U17_AG(T14, T59, halfc17_in_ga(T31, s(s(T40))))
U17_AG(T14, T59, halfc17_out_ga(T31, s(s(T40)))) → U18_AG(T14, T59, halfc17_in_ga(T40, s(s(T49))))
U18_AG(T14, T59, halfc17_out_ga(T40, s(s(T49)))) → U19_AG(T14, T59, halfc17_in_ga(T49, s(s(T58))))
U19_AG(T14, T59, halfc17_out_ga(T49, s(s(T58)))) → U20_AG(T14, T59, half17_in_ga(T58, X184))
U19_AG(T14, T59, halfc17_out_ga(T49, s(s(T58)))) → HALF17_IN_GA(T58, X184)
LOG21_IN_AG(s(s(T14)), T68) → U21_AG(T14, T68, halfc17_in_aa(T14, s(s(T31))))
U21_AG(T14, T68, halfc17_out_aa(T14, s(s(T31)))) → U22_AG(T14, T68, halfc17_in_ga(T31, s(s(T40))))
U22_AG(T14, T68, halfc17_out_ga(T31, s(s(T40)))) → U23_AG(T14, T68, halfc17_in_ga(T40, s(s(T49))))
U23_AG(T14, T68, halfc17_out_ga(T40, s(s(T49)))) → U24_AG(T14, T68, halfc17_in_ga(T49, s(s(T58))))
U24_AG(T14, T68, halfc17_out_ga(T49, s(s(T58)))) → U25_AG(T14, T68, halfc17_in_ga(T58, s(s(T67))))
U25_AG(T14, T68, halfc17_out_ga(T58, s(s(T67)))) → U26_AG(T14, T68, half17_in_ga(T67, X218))
U25_AG(T14, T68, halfc17_out_ga(T58, s(s(T67)))) → HALF17_IN_GA(T67, X218)
LOG21_IN_AG(s(s(T14)), T77) → U27_AG(T14, T77, halfc17_in_aa(T14, s(s(T31))))
U27_AG(T14, T77, halfc17_out_aa(T14, s(s(T31)))) → U28_AG(T14, T77, halfc17_in_ga(T31, s(s(T40))))
U28_AG(T14, T77, halfc17_out_ga(T31, s(s(T40)))) → U29_AG(T14, T77, halfc17_in_ga(T40, s(s(T49))))
U29_AG(T14, T77, halfc17_out_ga(T40, s(s(T49)))) → U30_AG(T14, T77, halfc17_in_ga(T49, s(s(T58))))
U30_AG(T14, T77, halfc17_out_ga(T49, s(s(T58)))) → U31_AG(T14, T77, halfc17_in_ga(T58, s(s(T67))))
U31_AG(T14, T77, halfc17_out_ga(T58, s(s(T67)))) → U32_AG(T14, T77, halfc17_in_ga(T67, s(s(T76))))
U32_AG(T14, T77, halfc17_out_ga(T67, s(s(T76)))) → U33_AG(T14, T77, half17_in_ga(T76, X252))
U32_AG(T14, T77, halfc17_out_ga(T67, s(s(T76)))) → HALF17_IN_GA(T76, X252)
LOG21_IN_AG(s(s(T14)), T86) → U34_AG(T14, T86, halfc17_in_aa(T14, s(s(T31))))
U34_AG(T14, T86, halfc17_out_aa(T14, s(s(T31)))) → U35_AG(T14, T86, halfc17_in_ga(T31, s(s(T40))))
U35_AG(T14, T86, halfc17_out_ga(T31, s(s(T40)))) → U36_AG(T14, T86, halfc17_in_ga(T40, s(s(T49))))
U36_AG(T14, T86, halfc17_out_ga(T40, s(s(T49)))) → U37_AG(T14, T86, halfc17_in_ga(T49, s(s(T58))))
U37_AG(T14, T86, halfc17_out_ga(T49, s(s(T58)))) → U38_AG(T14, T86, halfc17_in_ga(T58, s(s(T67))))
U38_AG(T14, T86, halfc17_out_ga(T58, s(s(T67)))) → U39_AG(T14, T86, halfc17_in_ga(T67, s(s(T76))))
U39_AG(T14, T86, halfc17_out_ga(T67, s(s(T76)))) → U40_AG(T14, T86, halfc17_in_ga(T76, s(s(T85))))
U40_AG(T14, T86, halfc17_out_ga(T76, s(s(T85)))) → U41_AG(T14, T86, p139_in_gagg(T85, X286, s(s(s(s(s(s(s(0))))))), T86))
U40_AG(T14, T86, halfc17_out_ga(T76, s(s(T85)))) → P139_IN_GAGG(T85, X286, s(s(s(s(s(s(s(0))))))), T86)
P139_IN_GAGG(T85, X286, T88, T86) → U3_GAGG(T85, X286, T88, T86, half17_in_ga(T85, X286))
P139_IN_GAGG(T85, X286, T88, T86) → HALF17_IN_GA(T85, X286)
P139_IN_GAGG(T85, s(s(T110)), T111, T112) → U4_GAGG(T85, T110, T111, T112, halfc17_in_ga(T85, s(s(T110))))
U4_GAGG(T85, T110, T111, T112, halfc17_out_ga(T85, s(s(T110)))) → U5_GAGG(T85, T110, T111, T112, p139_in_gagg(T110, X323, s(T111), T112))
U4_GAGG(T85, T110, T111, T112, halfc17_out_ga(T85, s(s(T110)))) → P139_IN_GAGG(T110, X323, s(T111), T112)

The TRS R consists of the following rules:

halfc17_in_aa(T22, s(X46)) → U44_aa(T22, X46, halfc22_in_aa(T22, X46))
halfc22_in_aa(0, 0) → halfc22_out_aa(0, 0)
halfc22_in_aa(s(0), 0) → halfc22_out_aa(s(0), 0)
halfc22_in_aa(s(s(T26)), s(X55)) → U43_aa(T26, X55, halfc22_in_aa(T26, X55))
U43_aa(T26, X55, halfc22_out_aa(T26, X55)) → halfc22_out_aa(s(s(T26)), s(X55))
U44_aa(T22, X46, halfc22_out_aa(T22, X46)) → halfc17_out_aa(T22, s(X46))
halfc17_in_ga(T22, s(X46)) → U44_ga(T22, X46, halfc22_in_ga(T22, X46))
halfc22_in_ga(0, 0) → halfc22_out_ga(0, 0)
halfc22_in_ga(s(0), 0) → halfc22_out_ga(s(0), 0)
halfc22_in_ga(s(s(T26)), s(X55)) → U43_ga(T26, X55, halfc22_in_ga(T26, X55))
U43_ga(T26, X55, halfc22_out_ga(T26, X55)) → halfc22_out_ga(s(s(T26)), s(X55))
U44_ga(T22, X46, halfc22_out_ga(T22, X46)) → halfc17_out_ga(T22, s(X46))

The argument filtering Pi contains the following mapping:
half17_in_aa(x1, x2)  =  half17_in_aa
half22_in_aa(x1, x2)  =  half22_in_aa
halfc17_in_aa(x1, x2)  =  halfc17_in_aa
U44_aa(x1, x2, x3)  =  U44_aa(x3)
halfc22_in_aa(x1, x2)  =  halfc22_in_aa
halfc22_out_aa(x1, x2)  =  halfc22_out_aa(x1, x2)
U43_aa(x1, x2, x3)  =  U43_aa(x3)
halfc17_out_aa(x1, x2)  =  halfc17_out_aa(x1, x2)
s(x1)  =  s(x1)
half17_in_ga(x1, x2)  =  half17_in_ga(x1)
half22_in_ga(x1, x2)  =  half22_in_ga(x1)
halfc17_in_ga(x1, x2)  =  halfc17_in_ga(x1)
U44_ga(x1, x2, x3)  =  U44_ga(x1, x3)
halfc22_in_ga(x1, x2)  =  halfc22_in_ga(x1)
0  =  0
halfc22_out_ga(x1, x2)  =  halfc22_out_ga(x1, x2)
U43_ga(x1, x2, x3)  =  U43_ga(x1, x3)
halfc17_out_ga(x1, x2)  =  halfc17_out_ga(x1, x2)
p139_in_gagg(x1, x2, x3, x4)  =  p139_in_gagg(x1, x3, x4)
LOG21_IN_AG(x1, x2)  =  LOG21_IN_AG(x2)
U6_AG(x1, x2, x3)  =  U6_AG(x2, x3)
HALF17_IN_AA(x1, x2)  =  HALF17_IN_AA
U2_AA(x1, x2, x3)  =  U2_AA(x3)
HALF22_IN_AA(x1, x2)  =  HALF22_IN_AA
U1_AA(x1, x2, x3)  =  U1_AA(x3)
U7_AG(x1, x2, x3)  =  U7_AG(x2, x3)
U8_AG(x1, x2, x3)  =  U8_AG(x1, x2, x3)
HALF17_IN_GA(x1, x2)  =  HALF17_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
HALF22_IN_GA(x1, x2)  =  HALF22_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U9_AG(x1, x2, x3)  =  U9_AG(x2, x3)
U10_AG(x1, x2, x3)  =  U10_AG(x1, x2, x3)
U11_AG(x1, x2, x3)  =  U11_AG(x1, x2, x3)
U12_AG(x1, x2, x3)  =  U12_AG(x2, x3)
U13_AG(x1, x2, x3)  =  U13_AG(x1, x2, x3)
U14_AG(x1, x2, x3)  =  U14_AG(x1, x2, x3)
U15_AG(x1, x2, x3)  =  U15_AG(x1, x2, x3)
U16_AG(x1, x2, x3)  =  U16_AG(x2, x3)
U17_AG(x1, x2, x3)  =  U17_AG(x1, x2, x3)
U18_AG(x1, x2, x3)  =  U18_AG(x1, x2, x3)
U19_AG(x1, x2, x3)  =  U19_AG(x1, x2, x3)
U20_AG(x1, x2, x3)  =  U20_AG(x1, x2, x3)
U21_AG(x1, x2, x3)  =  U21_AG(x2, x3)
U22_AG(x1, x2, x3)  =  U22_AG(x1, x2, x3)
U23_AG(x1, x2, x3)  =  U23_AG(x1, x2, x3)
U24_AG(x1, x2, x3)  =  U24_AG(x1, x2, x3)
U25_AG(x1, x2, x3)  =  U25_AG(x1, x2, x3)
U26_AG(x1, x2, x3)  =  U26_AG(x1, x2, x3)
U27_AG(x1, x2, x3)  =  U27_AG(x2, x3)
U28_AG(x1, x2, x3)  =  U28_AG(x1, x2, x3)
U29_AG(x1, x2, x3)  =  U29_AG(x1, x2, x3)
U30_AG(x1, x2, x3)  =  U30_AG(x1, x2, x3)
U31_AG(x1, x2, x3)  =  U31_AG(x1, x2, x3)
U32_AG(x1, x2, x3)  =  U32_AG(x1, x2, x3)
U33_AG(x1, x2, x3)  =  U33_AG(x1, x2, x3)
U34_AG(x1, x2, x3)  =  U34_AG(x2, x3)
U35_AG(x1, x2, x3)  =  U35_AG(x1, x2, x3)
U36_AG(x1, x2, x3)  =  U36_AG(x1, x2, x3)
U37_AG(x1, x2, x3)  =  U37_AG(x1, x2, x3)
U38_AG(x1, x2, x3)  =  U38_AG(x1, x2, x3)
U39_AG(x1, x2, x3)  =  U39_AG(x1, x2, x3)
U40_AG(x1, x2, x3)  =  U40_AG(x1, x2, x3)
U41_AG(x1, x2, x3)  =  U41_AG(x1, x2, x3)
P139_IN_GAGG(x1, x2, x3, x4)  =  P139_IN_GAGG(x1, x3, x4)
U3_GAGG(x1, x2, x3, x4, x5)  =  U3_GAGG(x1, x3, x4, x5)
U4_GAGG(x1, x2, x3, x4, x5)  =  U4_GAGG(x1, x3, x4, x5)
U5_GAGG(x1, x2, x3, x4, x5)  =  U5_GAGG(x1, x2, x3, x4, x5)

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:

LOG21_IN_AG(s(s(T14)), T13) → U6_AG(T14, T13, half17_in_aa(T14, X28))
LOG21_IN_AG(s(s(T14)), T13) → HALF17_IN_AA(T14, X28)
HALF17_IN_AA(T22, s(X46)) → U2_AA(T22, X46, half22_in_aa(T22, X46))
HALF17_IN_AA(T22, s(X46)) → HALF22_IN_AA(T22, X46)
HALF22_IN_AA(s(s(T26)), s(X55)) → U1_AA(T26, X55, half22_in_aa(T26, X55))
HALF22_IN_AA(s(s(T26)), s(X55)) → HALF22_IN_AA(T26, X55)
LOG21_IN_AG(s(s(T14)), T32) → U7_AG(T14, T32, halfc17_in_aa(T14, s(s(T31))))
U7_AG(T14, T32, halfc17_out_aa(T14, s(s(T31)))) → U8_AG(T14, T32, half17_in_ga(T31, X82))
U7_AG(T14, T32, halfc17_out_aa(T14, s(s(T31)))) → HALF17_IN_GA(T31, X82)
HALF17_IN_GA(T22, s(X46)) → U2_GA(T22, X46, half22_in_ga(T22, X46))
HALF17_IN_GA(T22, s(X46)) → HALF22_IN_GA(T22, X46)
HALF22_IN_GA(s(s(T26)), s(X55)) → U1_GA(T26, X55, half22_in_ga(T26, X55))
HALF22_IN_GA(s(s(T26)), s(X55)) → HALF22_IN_GA(T26, X55)
LOG21_IN_AG(s(s(T14)), T41) → U9_AG(T14, T41, halfc17_in_aa(T14, s(s(T31))))
U9_AG(T14, T41, halfc17_out_aa(T14, s(s(T31)))) → U10_AG(T14, T41, halfc17_in_ga(T31, s(s(T40))))
U10_AG(T14, T41, halfc17_out_ga(T31, s(s(T40)))) → U11_AG(T14, T41, half17_in_ga(T40, X116))
U10_AG(T14, T41, halfc17_out_ga(T31, s(s(T40)))) → HALF17_IN_GA(T40, X116)
LOG21_IN_AG(s(s(T14)), T50) → U12_AG(T14, T50, halfc17_in_aa(T14, s(s(T31))))
U12_AG(T14, T50, halfc17_out_aa(T14, s(s(T31)))) → U13_AG(T14, T50, halfc17_in_ga(T31, s(s(T40))))
U13_AG(T14, T50, halfc17_out_ga(T31, s(s(T40)))) → U14_AG(T14, T50, halfc17_in_ga(T40, s(s(T49))))
U14_AG(T14, T50, halfc17_out_ga(T40, s(s(T49)))) → U15_AG(T14, T50, half17_in_ga(T49, X150))
U14_AG(T14, T50, halfc17_out_ga(T40, s(s(T49)))) → HALF17_IN_GA(T49, X150)
LOG21_IN_AG(s(s(T14)), T59) → U16_AG(T14, T59, halfc17_in_aa(T14, s(s(T31))))
U16_AG(T14, T59, halfc17_out_aa(T14, s(s(T31)))) → U17_AG(T14, T59, halfc17_in_ga(T31, s(s(T40))))
U17_AG(T14, T59, halfc17_out_ga(T31, s(s(T40)))) → U18_AG(T14, T59, halfc17_in_ga(T40, s(s(T49))))
U18_AG(T14, T59, halfc17_out_ga(T40, s(s(T49)))) → U19_AG(T14, T59, halfc17_in_ga(T49, s(s(T58))))
U19_AG(T14, T59, halfc17_out_ga(T49, s(s(T58)))) → U20_AG(T14, T59, half17_in_ga(T58, X184))
U19_AG(T14, T59, halfc17_out_ga(T49, s(s(T58)))) → HALF17_IN_GA(T58, X184)
LOG21_IN_AG(s(s(T14)), T68) → U21_AG(T14, T68, halfc17_in_aa(T14, s(s(T31))))
U21_AG(T14, T68, halfc17_out_aa(T14, s(s(T31)))) → U22_AG(T14, T68, halfc17_in_ga(T31, s(s(T40))))
U22_AG(T14, T68, halfc17_out_ga(T31, s(s(T40)))) → U23_AG(T14, T68, halfc17_in_ga(T40, s(s(T49))))
U23_AG(T14, T68, halfc17_out_ga(T40, s(s(T49)))) → U24_AG(T14, T68, halfc17_in_ga(T49, s(s(T58))))
U24_AG(T14, T68, halfc17_out_ga(T49, s(s(T58)))) → U25_AG(T14, T68, halfc17_in_ga(T58, s(s(T67))))
U25_AG(T14, T68, halfc17_out_ga(T58, s(s(T67)))) → U26_AG(T14, T68, half17_in_ga(T67, X218))
U25_AG(T14, T68, halfc17_out_ga(T58, s(s(T67)))) → HALF17_IN_GA(T67, X218)
LOG21_IN_AG(s(s(T14)), T77) → U27_AG(T14, T77, halfc17_in_aa(T14, s(s(T31))))
U27_AG(T14, T77, halfc17_out_aa(T14, s(s(T31)))) → U28_AG(T14, T77, halfc17_in_ga(T31, s(s(T40))))
U28_AG(T14, T77, halfc17_out_ga(T31, s(s(T40)))) → U29_AG(T14, T77, halfc17_in_ga(T40, s(s(T49))))
U29_AG(T14, T77, halfc17_out_ga(T40, s(s(T49)))) → U30_AG(T14, T77, halfc17_in_ga(T49, s(s(T58))))
U30_AG(T14, T77, halfc17_out_ga(T49, s(s(T58)))) → U31_AG(T14, T77, halfc17_in_ga(T58, s(s(T67))))
U31_AG(T14, T77, halfc17_out_ga(T58, s(s(T67)))) → U32_AG(T14, T77, halfc17_in_ga(T67, s(s(T76))))
U32_AG(T14, T77, halfc17_out_ga(T67, s(s(T76)))) → U33_AG(T14, T77, half17_in_ga(T76, X252))
U32_AG(T14, T77, halfc17_out_ga(T67, s(s(T76)))) → HALF17_IN_GA(T76, X252)
LOG21_IN_AG(s(s(T14)), T86) → U34_AG(T14, T86, halfc17_in_aa(T14, s(s(T31))))
U34_AG(T14, T86, halfc17_out_aa(T14, s(s(T31)))) → U35_AG(T14, T86, halfc17_in_ga(T31, s(s(T40))))
U35_AG(T14, T86, halfc17_out_ga(T31, s(s(T40)))) → U36_AG(T14, T86, halfc17_in_ga(T40, s(s(T49))))
U36_AG(T14, T86, halfc17_out_ga(T40, s(s(T49)))) → U37_AG(T14, T86, halfc17_in_ga(T49, s(s(T58))))
U37_AG(T14, T86, halfc17_out_ga(T49, s(s(T58)))) → U38_AG(T14, T86, halfc17_in_ga(T58, s(s(T67))))
U38_AG(T14, T86, halfc17_out_ga(T58, s(s(T67)))) → U39_AG(T14, T86, halfc17_in_ga(T67, s(s(T76))))
U39_AG(T14, T86, halfc17_out_ga(T67, s(s(T76)))) → U40_AG(T14, T86, halfc17_in_ga(T76, s(s(T85))))
U40_AG(T14, T86, halfc17_out_ga(T76, s(s(T85)))) → U41_AG(T14, T86, p139_in_gagg(T85, X286, s(s(s(s(s(s(s(0))))))), T86))
U40_AG(T14, T86, halfc17_out_ga(T76, s(s(T85)))) → P139_IN_GAGG(T85, X286, s(s(s(s(s(s(s(0))))))), T86)
P139_IN_GAGG(T85, X286, T88, T86) → U3_GAGG(T85, X286, T88, T86, half17_in_ga(T85, X286))
P139_IN_GAGG(T85, X286, T88, T86) → HALF17_IN_GA(T85, X286)
P139_IN_GAGG(T85, s(s(T110)), T111, T112) → U4_GAGG(T85, T110, T111, T112, halfc17_in_ga(T85, s(s(T110))))
U4_GAGG(T85, T110, T111, T112, halfc17_out_ga(T85, s(s(T110)))) → U5_GAGG(T85, T110, T111, T112, p139_in_gagg(T110, X323, s(T111), T112))
U4_GAGG(T85, T110, T111, T112, halfc17_out_ga(T85, s(s(T110)))) → P139_IN_GAGG(T110, X323, s(T111), T112)

The TRS R consists of the following rules:

halfc17_in_aa(T22, s(X46)) → U44_aa(T22, X46, halfc22_in_aa(T22, X46))
halfc22_in_aa(0, 0) → halfc22_out_aa(0, 0)
halfc22_in_aa(s(0), 0) → halfc22_out_aa(s(0), 0)
halfc22_in_aa(s(s(T26)), s(X55)) → U43_aa(T26, X55, halfc22_in_aa(T26, X55))
U43_aa(T26, X55, halfc22_out_aa(T26, X55)) → halfc22_out_aa(s(s(T26)), s(X55))
U44_aa(T22, X46, halfc22_out_aa(T22, X46)) → halfc17_out_aa(T22, s(X46))
halfc17_in_ga(T22, s(X46)) → U44_ga(T22, X46, halfc22_in_ga(T22, X46))
halfc22_in_ga(0, 0) → halfc22_out_ga(0, 0)
halfc22_in_ga(s(0), 0) → halfc22_out_ga(s(0), 0)
halfc22_in_ga(s(s(T26)), s(X55)) → U43_ga(T26, X55, halfc22_in_ga(T26, X55))
U43_ga(T26, X55, halfc22_out_ga(T26, X55)) → halfc22_out_ga(s(s(T26)), s(X55))
U44_ga(T22, X46, halfc22_out_ga(T22, X46)) → halfc17_out_ga(T22, s(X46))

The argument filtering Pi contains the following mapping:
half17_in_aa(x1, x2)  =  half17_in_aa
half22_in_aa(x1, x2)  =  half22_in_aa
halfc17_in_aa(x1, x2)  =  halfc17_in_aa
U44_aa(x1, x2, x3)  =  U44_aa(x3)
halfc22_in_aa(x1, x2)  =  halfc22_in_aa
halfc22_out_aa(x1, x2)  =  halfc22_out_aa(x1, x2)
U43_aa(x1, x2, x3)  =  U43_aa(x3)
halfc17_out_aa(x1, x2)  =  halfc17_out_aa(x1, x2)
s(x1)  =  s(x1)
half17_in_ga(x1, x2)  =  half17_in_ga(x1)
half22_in_ga(x1, x2)  =  half22_in_ga(x1)
halfc17_in_ga(x1, x2)  =  halfc17_in_ga(x1)
U44_ga(x1, x2, x3)  =  U44_ga(x1, x3)
halfc22_in_ga(x1, x2)  =  halfc22_in_ga(x1)
0  =  0
halfc22_out_ga(x1, x2)  =  halfc22_out_ga(x1, x2)
U43_ga(x1, x2, x3)  =  U43_ga(x1, x3)
halfc17_out_ga(x1, x2)  =  halfc17_out_ga(x1, x2)
p139_in_gagg(x1, x2, x3, x4)  =  p139_in_gagg(x1, x3, x4)
LOG21_IN_AG(x1, x2)  =  LOG21_IN_AG(x2)
U6_AG(x1, x2, x3)  =  U6_AG(x2, x3)
HALF17_IN_AA(x1, x2)  =  HALF17_IN_AA
U2_AA(x1, x2, x3)  =  U2_AA(x3)
HALF22_IN_AA(x1, x2)  =  HALF22_IN_AA
U1_AA(x1, x2, x3)  =  U1_AA(x3)
U7_AG(x1, x2, x3)  =  U7_AG(x2, x3)
U8_AG(x1, x2, x3)  =  U8_AG(x1, x2, x3)
HALF17_IN_GA(x1, x2)  =  HALF17_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
HALF22_IN_GA(x1, x2)  =  HALF22_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U9_AG(x1, x2, x3)  =  U9_AG(x2, x3)
U10_AG(x1, x2, x3)  =  U10_AG(x1, x2, x3)
U11_AG(x1, x2, x3)  =  U11_AG(x1, x2, x3)
U12_AG(x1, x2, x3)  =  U12_AG(x2, x3)
U13_AG(x1, x2, x3)  =  U13_AG(x1, x2, x3)
U14_AG(x1, x2, x3)  =  U14_AG(x1, x2, x3)
U15_AG(x1, x2, x3)  =  U15_AG(x1, x2, x3)
U16_AG(x1, x2, x3)  =  U16_AG(x2, x3)
U17_AG(x1, x2, x3)  =  U17_AG(x1, x2, x3)
U18_AG(x1, x2, x3)  =  U18_AG(x1, x2, x3)
U19_AG(x1, x2, x3)  =  U19_AG(x1, x2, x3)
U20_AG(x1, x2, x3)  =  U20_AG(x1, x2, x3)
U21_AG(x1, x2, x3)  =  U21_AG(x2, x3)
U22_AG(x1, x2, x3)  =  U22_AG(x1, x2, x3)
U23_AG(x1, x2, x3)  =  U23_AG(x1, x2, x3)
U24_AG(x1, x2, x3)  =  U24_AG(x1, x2, x3)
U25_AG(x1, x2, x3)  =  U25_AG(x1, x2, x3)
U26_AG(x1, x2, x3)  =  U26_AG(x1, x2, x3)
U27_AG(x1, x2, x3)  =  U27_AG(x2, x3)
U28_AG(x1, x2, x3)  =  U28_AG(x1, x2, x3)
U29_AG(x1, x2, x3)  =  U29_AG(x1, x2, x3)
U30_AG(x1, x2, x3)  =  U30_AG(x1, x2, x3)
U31_AG(x1, x2, x3)  =  U31_AG(x1, x2, x3)
U32_AG(x1, x2, x3)  =  U32_AG(x1, x2, x3)
U33_AG(x1, x2, x3)  =  U33_AG(x1, x2, x3)
U34_AG(x1, x2, x3)  =  U34_AG(x2, x3)
U35_AG(x1, x2, x3)  =  U35_AG(x1, x2, x3)
U36_AG(x1, x2, x3)  =  U36_AG(x1, x2, x3)
U37_AG(x1, x2, x3)  =  U37_AG(x1, x2, x3)
U38_AG(x1, x2, x3)  =  U38_AG(x1, x2, x3)
U39_AG(x1, x2, x3)  =  U39_AG(x1, x2, x3)
U40_AG(x1, x2, x3)  =  U40_AG(x1, x2, x3)
U41_AG(x1, x2, x3)  =  U41_AG(x1, x2, x3)
P139_IN_GAGG(x1, x2, x3, x4)  =  P139_IN_GAGG(x1, x3, x4)
U3_GAGG(x1, x2, x3, x4, x5)  =  U3_GAGG(x1, x3, x4, x5)
U4_GAGG(x1, x2, x3, x4, x5)  =  U4_GAGG(x1, x3, x4, x5)
U5_GAGG(x1, x2, x3, x4, x5)  =  U5_GAGG(x1, x2, x3, x4, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

HALF22_IN_GA(s(s(T26)), s(X55)) → HALF22_IN_GA(T26, X55)

The TRS R consists of the following rules:

halfc17_in_aa(T22, s(X46)) → U44_aa(T22, X46, halfc22_in_aa(T22, X46))
halfc22_in_aa(0, 0) → halfc22_out_aa(0, 0)
halfc22_in_aa(s(0), 0) → halfc22_out_aa(s(0), 0)
halfc22_in_aa(s(s(T26)), s(X55)) → U43_aa(T26, X55, halfc22_in_aa(T26, X55))
U43_aa(T26, X55, halfc22_out_aa(T26, X55)) → halfc22_out_aa(s(s(T26)), s(X55))
U44_aa(T22, X46, halfc22_out_aa(T22, X46)) → halfc17_out_aa(T22, s(X46))
halfc17_in_ga(T22, s(X46)) → U44_ga(T22, X46, halfc22_in_ga(T22, X46))
halfc22_in_ga(0, 0) → halfc22_out_ga(0, 0)
halfc22_in_ga(s(0), 0) → halfc22_out_ga(s(0), 0)
halfc22_in_ga(s(s(T26)), s(X55)) → U43_ga(T26, X55, halfc22_in_ga(T26, X55))
U43_ga(T26, X55, halfc22_out_ga(T26, X55)) → halfc22_out_ga(s(s(T26)), s(X55))
U44_ga(T22, X46, halfc22_out_ga(T22, X46)) → halfc17_out_ga(T22, s(X46))

The argument filtering Pi contains the following mapping:
halfc17_in_aa(x1, x2)  =  halfc17_in_aa
U44_aa(x1, x2, x3)  =  U44_aa(x3)
halfc22_in_aa(x1, x2)  =  halfc22_in_aa
halfc22_out_aa(x1, x2)  =  halfc22_out_aa(x1, x2)
U43_aa(x1, x2, x3)  =  U43_aa(x3)
halfc17_out_aa(x1, x2)  =  halfc17_out_aa(x1, x2)
s(x1)  =  s(x1)
halfc17_in_ga(x1, x2)  =  halfc17_in_ga(x1)
U44_ga(x1, x2, x3)  =  U44_ga(x1, x3)
halfc22_in_ga(x1, x2)  =  halfc22_in_ga(x1)
0  =  0
halfc22_out_ga(x1, x2)  =  halfc22_out_ga(x1, x2)
U43_ga(x1, x2, x3)  =  U43_ga(x1, x3)
halfc17_out_ga(x1, x2)  =  halfc17_out_ga(x1, x2)
HALF22_IN_GA(x1, x2)  =  HALF22_IN_GA(x1)

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:

HALF22_IN_GA(s(s(T26)), s(X55)) → HALF22_IN_GA(T26, X55)

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

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:

HALF22_IN_GA(s(s(T26))) → HALF22_IN_GA(T26)

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:

  • HALF22_IN_GA(s(s(T26))) → HALF22_IN_GA(T26)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

P139_IN_GAGG(T85, s(s(T110)), T111, T112) → U4_GAGG(T85, T110, T111, T112, halfc17_in_ga(T85, s(s(T110))))
U4_GAGG(T85, T110, T111, T112, halfc17_out_ga(T85, s(s(T110)))) → P139_IN_GAGG(T110, X323, s(T111), T112)

The TRS R consists of the following rules:

halfc17_in_aa(T22, s(X46)) → U44_aa(T22, X46, halfc22_in_aa(T22, X46))
halfc22_in_aa(0, 0) → halfc22_out_aa(0, 0)
halfc22_in_aa(s(0), 0) → halfc22_out_aa(s(0), 0)
halfc22_in_aa(s(s(T26)), s(X55)) → U43_aa(T26, X55, halfc22_in_aa(T26, X55))
U43_aa(T26, X55, halfc22_out_aa(T26, X55)) → halfc22_out_aa(s(s(T26)), s(X55))
U44_aa(T22, X46, halfc22_out_aa(T22, X46)) → halfc17_out_aa(T22, s(X46))
halfc17_in_ga(T22, s(X46)) → U44_ga(T22, X46, halfc22_in_ga(T22, X46))
halfc22_in_ga(0, 0) → halfc22_out_ga(0, 0)
halfc22_in_ga(s(0), 0) → halfc22_out_ga(s(0), 0)
halfc22_in_ga(s(s(T26)), s(X55)) → U43_ga(T26, X55, halfc22_in_ga(T26, X55))
U43_ga(T26, X55, halfc22_out_ga(T26, X55)) → halfc22_out_ga(s(s(T26)), s(X55))
U44_ga(T22, X46, halfc22_out_ga(T22, X46)) → halfc17_out_ga(T22, s(X46))

The argument filtering Pi contains the following mapping:
halfc17_in_aa(x1, x2)  =  halfc17_in_aa
U44_aa(x1, x2, x3)  =  U44_aa(x3)
halfc22_in_aa(x1, x2)  =  halfc22_in_aa
halfc22_out_aa(x1, x2)  =  halfc22_out_aa(x1, x2)
U43_aa(x1, x2, x3)  =  U43_aa(x3)
halfc17_out_aa(x1, x2)  =  halfc17_out_aa(x1, x2)
s(x1)  =  s(x1)
halfc17_in_ga(x1, x2)  =  halfc17_in_ga(x1)
U44_ga(x1, x2, x3)  =  U44_ga(x1, x3)
halfc22_in_ga(x1, x2)  =  halfc22_in_ga(x1)
0  =  0
halfc22_out_ga(x1, x2)  =  halfc22_out_ga(x1, x2)
U43_ga(x1, x2, x3)  =  U43_ga(x1, x3)
halfc17_out_ga(x1, x2)  =  halfc17_out_ga(x1, x2)
P139_IN_GAGG(x1, x2, x3, x4)  =  P139_IN_GAGG(x1, x3, x4)
U4_GAGG(x1, x2, x3, x4, x5)  =  U4_GAGG(x1, x3, x4, x5)

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:

P139_IN_GAGG(T85, s(s(T110)), T111, T112) → U4_GAGG(T85, T110, T111, T112, halfc17_in_ga(T85, s(s(T110))))
U4_GAGG(T85, T110, T111, T112, halfc17_out_ga(T85, s(s(T110)))) → P139_IN_GAGG(T110, X323, s(T111), T112)

The TRS R consists of the following rules:

halfc17_in_ga(T22, s(X46)) → U44_ga(T22, X46, halfc22_in_ga(T22, X46))
U44_ga(T22, X46, halfc22_out_ga(T22, X46)) → halfc17_out_ga(T22, s(X46))
halfc22_in_ga(0, 0) → halfc22_out_ga(0, 0)
halfc22_in_ga(s(0), 0) → halfc22_out_ga(s(0), 0)
halfc22_in_ga(s(s(T26)), s(X55)) → U43_ga(T26, X55, halfc22_in_ga(T26, X55))
U43_ga(T26, X55, halfc22_out_ga(T26, X55)) → halfc22_out_ga(s(s(T26)), s(X55))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
halfc17_in_ga(x1, x2)  =  halfc17_in_ga(x1)
U44_ga(x1, x2, x3)  =  U44_ga(x1, x3)
halfc22_in_ga(x1, x2)  =  halfc22_in_ga(x1)
0  =  0
halfc22_out_ga(x1, x2)  =  halfc22_out_ga(x1, x2)
U43_ga(x1, x2, x3)  =  U43_ga(x1, x3)
halfc17_out_ga(x1, x2)  =  halfc17_out_ga(x1, x2)
P139_IN_GAGG(x1, x2, x3, x4)  =  P139_IN_GAGG(x1, x3, x4)
U4_GAGG(x1, x2, x3, x4, x5)  =  U4_GAGG(x1, x3, x4, x5)

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:

P139_IN_GAGG(T85, T111, T112) → U4_GAGG(T85, T111, T112, halfc17_in_ga(T85))
U4_GAGG(T85, T111, T112, halfc17_out_ga(T85, s(s(T110)))) → P139_IN_GAGG(T110, s(T111), T112)

The TRS R consists of the following rules:

halfc17_in_ga(T22) → U44_ga(T22, halfc22_in_ga(T22))
U44_ga(T22, halfc22_out_ga(T22, X46)) → halfc17_out_ga(T22, s(X46))
halfc22_in_ga(0) → halfc22_out_ga(0, 0)
halfc22_in_ga(s(0)) → halfc22_out_ga(s(0), 0)
halfc22_in_ga(s(s(T26))) → U43_ga(T26, halfc22_in_ga(T26))
U43_ga(T26, halfc22_out_ga(T26, X55)) → halfc22_out_ga(s(s(T26)), s(X55))

The set Q consists of the following terms:

halfc17_in_ga(x0)
U44_ga(x0, x1)
halfc22_in_ga(x0)
U43_ga(x0, x1)

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

(19) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule P139_IN_GAGG(T85, T111, T112) → U4_GAGG(T85, T111, T112, halfc17_in_ga(T85)) at position [3] we obtained the following new rules [LPAR04]:

P139_IN_GAGG(T85, T111, T112) → U4_GAGG(T85, T111, T112, U44_ga(T85, halfc22_in_ga(T85)))

(20) Obligation:

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

U4_GAGG(T85, T111, T112, halfc17_out_ga(T85, s(s(T110)))) → P139_IN_GAGG(T110, s(T111), T112)
P139_IN_GAGG(T85, T111, T112) → U4_GAGG(T85, T111, T112, U44_ga(T85, halfc22_in_ga(T85)))

The TRS R consists of the following rules:

halfc17_in_ga(T22) → U44_ga(T22, halfc22_in_ga(T22))
U44_ga(T22, halfc22_out_ga(T22, X46)) → halfc17_out_ga(T22, s(X46))
halfc22_in_ga(0) → halfc22_out_ga(0, 0)
halfc22_in_ga(s(0)) → halfc22_out_ga(s(0), 0)
halfc22_in_ga(s(s(T26))) → U43_ga(T26, halfc22_in_ga(T26))
U43_ga(T26, halfc22_out_ga(T26, X55)) → halfc22_out_ga(s(s(T26)), s(X55))

The set Q consists of the following terms:

halfc17_in_ga(x0)
U44_ga(x0, x1)
halfc22_in_ga(x0)
U43_ga(x0, x1)

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

(21) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(22) Obligation:

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

U4_GAGG(T85, T111, T112, halfc17_out_ga(T85, s(s(T110)))) → P139_IN_GAGG(T110, s(T111), T112)
P139_IN_GAGG(T85, T111, T112) → U4_GAGG(T85, T111, T112, U44_ga(T85, halfc22_in_ga(T85)))

The TRS R consists of the following rules:

halfc22_in_ga(0) → halfc22_out_ga(0, 0)
halfc22_in_ga(s(0)) → halfc22_out_ga(s(0), 0)
halfc22_in_ga(s(s(T26))) → U43_ga(T26, halfc22_in_ga(T26))
U44_ga(T22, halfc22_out_ga(T22, X46)) → halfc17_out_ga(T22, s(X46))
U43_ga(T26, halfc22_out_ga(T26, X55)) → halfc22_out_ga(s(s(T26)), s(X55))

The set Q consists of the following terms:

halfc17_in_ga(x0)
U44_ga(x0, x1)
halfc22_in_ga(x0)
U43_ga(x0, x1)

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

(23) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

halfc17_in_ga(x0)

(24) Obligation:

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

U4_GAGG(T85, T111, T112, halfc17_out_ga(T85, s(s(T110)))) → P139_IN_GAGG(T110, s(T111), T112)
P139_IN_GAGG(T85, T111, T112) → U4_GAGG(T85, T111, T112, U44_ga(T85, halfc22_in_ga(T85)))

The TRS R consists of the following rules:

halfc22_in_ga(0) → halfc22_out_ga(0, 0)
halfc22_in_ga(s(0)) → halfc22_out_ga(s(0), 0)
halfc22_in_ga(s(s(T26))) → U43_ga(T26, halfc22_in_ga(T26))
U44_ga(T22, halfc22_out_ga(T22, X46)) → halfc17_out_ga(T22, s(X46))
U43_ga(T26, halfc22_out_ga(T26, X55)) → halfc22_out_ga(s(s(T26)), s(X55))

The set Q consists of the following terms:

U44_ga(x0, x1)
halfc22_in_ga(x0)
U43_ga(x0, x1)

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

(25) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U4_GAGG(T85, T111, T112, halfc17_out_ga(T85, s(s(T110)))) → P139_IN_GAGG(T110, s(T111), T112)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(P139_IN_GAGG(x1, x2, x3)) = 1 + x1   
POL(U43_ga(x1, x2)) = 1 + x2   
POL(U44_ga(x1, x2)) = x2   
POL(U4_GAGG(x1, x2, x3, x4)) = x4   
POL(halfc17_out_ga(x1, x2)) = x2   
POL(halfc22_in_ga(x1)) = 1 + x1   
POL(halfc22_out_ga(x1, x2)) = 1 + x2   
POL(s(x1)) = 1 + x1   

The following usable rules [FROCOS05] were oriented:

halfc22_in_ga(0) → halfc22_out_ga(0, 0)
halfc22_in_ga(s(0)) → halfc22_out_ga(s(0), 0)
halfc22_in_ga(s(s(T26))) → U43_ga(T26, halfc22_in_ga(T26))
U44_ga(T22, halfc22_out_ga(T22, X46)) → halfc17_out_ga(T22, s(X46))
U43_ga(T26, halfc22_out_ga(T26, X55)) → halfc22_out_ga(s(s(T26)), s(X55))

(26) Obligation:

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

P139_IN_GAGG(T85, T111, T112) → U4_GAGG(T85, T111, T112, U44_ga(T85, halfc22_in_ga(T85)))

The TRS R consists of the following rules:

halfc22_in_ga(0) → halfc22_out_ga(0, 0)
halfc22_in_ga(s(0)) → halfc22_out_ga(s(0), 0)
halfc22_in_ga(s(s(T26))) → U43_ga(T26, halfc22_in_ga(T26))
U44_ga(T22, halfc22_out_ga(T22, X46)) → halfc17_out_ga(T22, s(X46))
U43_ga(T26, halfc22_out_ga(T26, X55)) → halfc22_out_ga(s(s(T26)), s(X55))

The set Q consists of the following terms:

U44_ga(x0, x1)
halfc22_in_ga(x0)
U43_ga(x0, x1)

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

(27) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(28) TRUE

(29) Obligation:

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

HALF22_IN_AA(s(s(T26)), s(X55)) → HALF22_IN_AA(T26, X55)

The TRS R consists of the following rules:

halfc17_in_aa(T22, s(X46)) → U44_aa(T22, X46, halfc22_in_aa(T22, X46))
halfc22_in_aa(0, 0) → halfc22_out_aa(0, 0)
halfc22_in_aa(s(0), 0) → halfc22_out_aa(s(0), 0)
halfc22_in_aa(s(s(T26)), s(X55)) → U43_aa(T26, X55, halfc22_in_aa(T26, X55))
U43_aa(T26, X55, halfc22_out_aa(T26, X55)) → halfc22_out_aa(s(s(T26)), s(X55))
U44_aa(T22, X46, halfc22_out_aa(T22, X46)) → halfc17_out_aa(T22, s(X46))
halfc17_in_ga(T22, s(X46)) → U44_ga(T22, X46, halfc22_in_ga(T22, X46))
halfc22_in_ga(0, 0) → halfc22_out_ga(0, 0)
halfc22_in_ga(s(0), 0) → halfc22_out_ga(s(0), 0)
halfc22_in_ga(s(s(T26)), s(X55)) → U43_ga(T26, X55, halfc22_in_ga(T26, X55))
U43_ga(T26, X55, halfc22_out_ga(T26, X55)) → halfc22_out_ga(s(s(T26)), s(X55))
U44_ga(T22, X46, halfc22_out_ga(T22, X46)) → halfc17_out_ga(T22, s(X46))

The argument filtering Pi contains the following mapping:
halfc17_in_aa(x1, x2)  =  halfc17_in_aa
U44_aa(x1, x2, x3)  =  U44_aa(x3)
halfc22_in_aa(x1, x2)  =  halfc22_in_aa
halfc22_out_aa(x1, x2)  =  halfc22_out_aa(x1, x2)
U43_aa(x1, x2, x3)  =  U43_aa(x3)
halfc17_out_aa(x1, x2)  =  halfc17_out_aa(x1, x2)
s(x1)  =  s(x1)
halfc17_in_ga(x1, x2)  =  halfc17_in_ga(x1)
U44_ga(x1, x2, x3)  =  U44_ga(x1, x3)
halfc22_in_ga(x1, x2)  =  halfc22_in_ga(x1)
0  =  0
halfc22_out_ga(x1, x2)  =  halfc22_out_ga(x1, x2)
U43_ga(x1, x2, x3)  =  U43_ga(x1, x3)
halfc17_out_ga(x1, x2)  =  halfc17_out_ga(x1, x2)
HALF22_IN_AA(x1, x2)  =  HALF22_IN_AA

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

(30) UsableRulesProof (EQUIVALENT transformation)

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

(31) Obligation:

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

HALF22_IN_AA(s(s(T26)), s(X55)) → HALF22_IN_AA(T26, X55)

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

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

(32) PiDPToQDPProof (SOUND transformation)

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

(33) Obligation:

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

HALF22_IN_AAHALF22_IN_AA

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

(34) NonTerminationProof (EQUIVALENT transformation)

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

s = HALF22_IN_AA evaluates to t =HALF22_IN_AA

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




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from HALF22_IN_AA to HALF22_IN_AA.



(35) NO