(0) Obligation:

Clauses:

add(b, b, b).
add(X, b, X) :- binaryZ(X).
add(b, Y, Y) :- binaryZ(Y).
add(X, Y, Z) :- addz(X, Y, Z).
addx(one(X), b, one(X)) :- binary(X).
addx(zero(X), b, zero(X)) :- binaryZ(X).
addx(X, Y, Z) :- addz(X, Y, Z).
addy(b, one(Y), one(Y)) :- binary(Y).
addy(b, zero(Y), zero(Y)) :- binaryZ(Y).
addy(X, Y, Z) :- addz(X, Y, Z).
addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z).
addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z).
addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z).
addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z).
addc(b, b, one(b)).
addc(X, b, Z) :- succZ(X, Z).
addc(b, Y, Z) :- succZ(Y, Z).
addc(X, Y, Z) :- addC(X, Y, Z).
addX(zero(X), b, one(X)) :- binaryZ(X).
addX(one(X), b, zero(Z)) :- succ(X, Z).
addX(X, Y, Z) :- addC(X, Y, Z).
addY(b, zero(Y), one(Y)) :- binaryZ(Y).
addY(b, one(Y), zero(Z)) :- succ(Y, Z).
addY(X, Y, Z) :- addC(X, Y, Z).
addC(zero(X), zero(Y), one(Z)) :- addz(X, Y, Z).
addC(zero(X), one(Y), zero(Z)) :- addX(X, Y, Z).
addC(one(X), zero(Y), zero(Z)) :- addY(X, Y, Z).
addC(one(X), one(Y), one(Z)) :- addc(X, Y, Z).
binary(b).
binary(zero(X)) :- binaryZ(X).
binary(one(X)) :- binary(X).
binaryZ(zero(X)) :- binaryZ(X).
binaryZ(one(X)) :- binary(X).
succ(b, one(b)).
succ(zero(X), one(X)) :- binaryZ(X).
succ(one(X), zero(Z)) :- succ(X, Z).
succZ(zero(X), one(X)) :- binaryZ(X).
succZ(one(X), zero(Z)) :- succ(X, Z).
times(one(b), X, X).
times(zero(R), S, zero(RS)) :- times(R, S, RS).
times(one(R), S, RSS) :- ','(times(R, S, RS), add(S, zero(RS), RSS)).

Queries:

add(g,g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

binaryZ43(zero(T29)) :- binaryZ43(T29).
binaryZ43(one(T33)) :- binary50(T33).
binary50(zero(T38)) :- binaryZ43(T38).
binary50(one(T42)) :- binary50(T42).
addz101(zero(T127), zero(T128), zero(T130)) :- addz101(T127, T128, T130).
addz101(zero(T146), one(T147), one(T149)) :- addx110(T146, T147, T149).
addz101(one(T191), zero(T192), one(T194)) :- addy124(T191, T192, T194).
addz101(one(T230), one(T231), zero(T233)) :- addc136(T230, T231, T233).
succ153(zero(T263), one(T263)) :- binaryZ43(T263).
succ153(one(T269), zero(T271)) :- succ153(T269, T271).
succZ146(zero(T250), one(T250)) :- binaryZ43(T250).
succZ146(one(T256), zero(T258)) :- succ153(T256, T258).
addC171(zero(T313), zero(T314), one(T316)) :- addz101(T313, T314, T316).
addC171(zero(zero(T341)), one(b), zero(one(T341))) :- binaryZ43(T341).
addC171(zero(one(T351)), one(b), zero(zero(T353))) :- succ153(T351, T353).
addC171(zero(T364), one(T365), zero(T367)) :- addC171(T364, T365, T367).
addC171(one(b), zero(zero(T392)), zero(one(T392))) :- binaryZ43(T392).
addC171(one(b), zero(one(T402)), zero(zero(T404))) :- succ153(T402, T404).
addC171(one(T415), zero(T416), zero(T418)) :- addC171(T415, T416, T418).
addC171(one(T428), one(T429), one(T431)) :- addc136(T428, T429, T431).
addc136(T242, b, T244) :- succZ146(T242, T244).
addc136(b, T280, T282) :- succZ146(T280, T282).
addc136(T294, T295, T297) :- addC171(T294, T295, T297).
addx110(one(T155), b, one(T155)) :- binary50(T155).
addx110(zero(T160), b, zero(T160)) :- binaryZ43(T160).
addx110(T172, T173, T175) :- addz101(T172, T173, T175).
addy124(b, one(T200), one(T200)) :- binary50(T200).
addy124(b, zero(T205), zero(T205)) :- binaryZ43(T205).
addy124(T217, T218, T220) :- addz101(T217, T218, T220).
add1(b, b, b) :- binaryZ14.
add1(b, b, T8) :- addz19(T8).
add1(b, b, T13) :- addz19(T13).
add1(zero(T23), b, zero(T23)) :- binaryZ43(T23).
add1(one(T47), b, one(T47)) :- binary50(T47).
add1(b, b, b) :- binaryZ14.
add1(b, zero(T74), zero(T74)) :- binaryZ43(T74).
add1(b, one(T80), one(T80)) :- binary50(T80).
add1(zero(T108), zero(T109), zero(T111)) :- addz101(T108, T109, T111).
add1(zero(T444), one(T445), one(T447)) :- addx110(T444, T445, T447).
add1(one(T461), zero(T462), one(T464)) :- addy124(T461, T462, T464).
add1(one(T472), one(T473), zero(T475)) :- addc136(T472, T473, T475).

Clauses:

binaryZc43(zero(T29)) :- binaryZc43(T29).
binaryZc43(one(T33)) :- binaryc50(T33).
binaryc50(b).
binaryc50(zero(T38)) :- binaryZc43(T38).
binaryc50(one(T42)) :- binaryc50(T42).
addzc101(zero(T127), zero(T128), zero(T130)) :- addzc101(T127, T128, T130).
addzc101(zero(T146), one(T147), one(T149)) :- addxc110(T146, T147, T149).
addzc101(one(T191), zero(T192), one(T194)) :- addyc124(T191, T192, T194).
addzc101(one(T230), one(T231), zero(T233)) :- addcc136(T230, T231, T233).
succc153(b, one(b)).
succc153(zero(T263), one(T263)) :- binaryZc43(T263).
succc153(one(T269), zero(T271)) :- succc153(T269, T271).
succZc146(zero(T250), one(T250)) :- binaryZc43(T250).
succZc146(one(T256), zero(T258)) :- succc153(T256, T258).
addCc171(zero(T313), zero(T314), one(T316)) :- addzc101(T313, T314, T316).
addCc171(zero(zero(T341)), one(b), zero(one(T341))) :- binaryZc43(T341).
addCc171(zero(one(T351)), one(b), zero(zero(T353))) :- succc153(T351, T353).
addCc171(zero(T364), one(T365), zero(T367)) :- addCc171(T364, T365, T367).
addCc171(one(b), zero(zero(T392)), zero(one(T392))) :- binaryZc43(T392).
addCc171(one(b), zero(one(T402)), zero(zero(T404))) :- succc153(T402, T404).
addCc171(one(T415), zero(T416), zero(T418)) :- addCc171(T415, T416, T418).
addCc171(one(T428), one(T429), one(T431)) :- addcc136(T428, T429, T431).
addcc136(b, b, one(b)).
addcc136(T242, b, T244) :- succZc146(T242, T244).
addcc136(b, T280, T282) :- succZc146(T280, T282).
addcc136(T294, T295, T297) :- addCc171(T294, T295, T297).
addxc110(one(T155), b, one(T155)) :- binaryc50(T155).
addxc110(zero(T160), b, zero(T160)) :- binaryZc43(T160).
addxc110(T172, T173, T175) :- addzc101(T172, T173, T175).
addyc124(b, one(T200), one(T200)) :- binaryc50(T200).
addyc124(b, zero(T205), zero(T205)) :- binaryZc43(T205).
addyc124(T217, T218, T220) :- addzc101(T217, T218, T220).

Afs:

add1(x1, x2, x3)  =  add1(x1, x2)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

binaryZ43(zero(T29)) :- binaryZ43(T29).
binaryZ43(one(T33)) :- binary50(T33).
binary50(zero(T38)) :- binaryZ43(T38).
binary50(one(T42)) :- binary50(T42).
addz101(zero(T127), zero(T128), zero(T130)) :- addz101(T127, T128, T130).
addz101(zero(T146), one(T147), one(T149)) :- addx110(T146, T147, T149).
addz101(one(T191), zero(T192), one(T194)) :- addy124(T191, T192, T194).
addz101(one(T230), one(T231), zero(T233)) :- addc136(T230, T231, T233).
succ153(zero(T263), one(T263)) :- binaryZ43(T263).
succ153(one(T269), zero(T271)) :- succ153(T269, T271).
succZ146(zero(T250), one(T250)) :- binaryZ43(T250).
succZ146(one(T256), zero(T258)) :- succ153(T256, T258).
addC171(zero(T313), zero(T314), one(T316)) :- addz101(T313, T314, T316).
addC171(zero(zero(T341)), one(b), zero(one(T341))) :- binaryZ43(T341).
addC171(zero(one(T351)), one(b), zero(zero(T353))) :- succ153(T351, T353).
addC171(zero(T364), one(T365), zero(T367)) :- addC171(T364, T365, T367).
addC171(one(b), zero(zero(T392)), zero(one(T392))) :- binaryZ43(T392).
addC171(one(b), zero(one(T402)), zero(zero(T404))) :- succ153(T402, T404).
addC171(one(T415), zero(T416), zero(T418)) :- addC171(T415, T416, T418).
addC171(one(T428), one(T429), one(T431)) :- addc136(T428, T429, T431).
addc136(T242, b, T244) :- succZ146(T242, T244).
addc136(b, T280, T282) :- succZ146(T280, T282).
addc136(T294, T295, T297) :- addC171(T294, T295, T297).
addx110(one(T155), b, one(T155)) :- binary50(T155).
addx110(zero(T160), b, zero(T160)) :- binaryZ43(T160).
addx110(T172, T173, T175) :- addz101(T172, T173, T175).
addy124(b, one(T200), one(T200)) :- binary50(T200).
addy124(b, zero(T205), zero(T205)) :- binaryZ43(T205).
addy124(T217, T218, T220) :- addz101(T217, T218, T220).
add1(zero(T23), b, zero(T23)) :- binaryZ43(T23).
add1(one(T47), b, one(T47)) :- binary50(T47).
add1(b, zero(T74), zero(T74)) :- binaryZ43(T74).
add1(b, one(T80), one(T80)) :- binary50(T80).
add1(zero(T108), zero(T109), zero(T111)) :- addz101(T108, T109, T111).
add1(zero(T444), one(T445), one(T447)) :- addx110(T444, T445, T447).
add1(one(T461), zero(T462), one(T464)) :- addy124(T461, T462, T464).
add1(one(T472), one(T473), zero(T475)) :- addc136(T472, T473, T475).

Clauses:

binaryZc43(zero(T29)) :- binaryZc43(T29).
binaryZc43(one(T33)) :- binaryc50(T33).
binaryc50(b).
binaryc50(zero(T38)) :- binaryZc43(T38).
binaryc50(one(T42)) :- binaryc50(T42).
addzc101(zero(T127), zero(T128), zero(T130)) :- addzc101(T127, T128, T130).
addzc101(zero(T146), one(T147), one(T149)) :- addxc110(T146, T147, T149).
addzc101(one(T191), zero(T192), one(T194)) :- addyc124(T191, T192, T194).
addzc101(one(T230), one(T231), zero(T233)) :- addcc136(T230, T231, T233).
succc153(b, one(b)).
succc153(zero(T263), one(T263)) :- binaryZc43(T263).
succc153(one(T269), zero(T271)) :- succc153(T269, T271).
succZc146(zero(T250), one(T250)) :- binaryZc43(T250).
succZc146(one(T256), zero(T258)) :- succc153(T256, T258).
addCc171(zero(T313), zero(T314), one(T316)) :- addzc101(T313, T314, T316).
addCc171(zero(zero(T341)), one(b), zero(one(T341))) :- binaryZc43(T341).
addCc171(zero(one(T351)), one(b), zero(zero(T353))) :- succc153(T351, T353).
addCc171(zero(T364), one(T365), zero(T367)) :- addCc171(T364, T365, T367).
addCc171(one(b), zero(zero(T392)), zero(one(T392))) :- binaryZc43(T392).
addCc171(one(b), zero(one(T402)), zero(zero(T404))) :- succc153(T402, T404).
addCc171(one(T415), zero(T416), zero(T418)) :- addCc171(T415, T416, T418).
addCc171(one(T428), one(T429), one(T431)) :- addcc136(T428, T429, T431).
addcc136(b, b, one(b)).
addcc136(T242, b, T244) :- succZc146(T242, T244).
addcc136(b, T280, T282) :- succZc146(T280, T282).
addcc136(T294, T295, T297) :- addCc171(T294, T295, T297).
addxc110(one(T155), b, one(T155)) :- binaryc50(T155).
addxc110(zero(T160), b, zero(T160)) :- binaryZc43(T160).
addxc110(T172, T173, T175) :- addzc101(T172, T173, T175).
addyc124(b, one(T200), one(T200)) :- binaryc50(T200).
addyc124(b, zero(T205), zero(T205)) :- binaryZc43(T205).
addyc124(T217, T218, T220) :- addzc101(T217, T218, T220).

Afs:

add1(x1, x2, x3)  =  add1(x1, x2)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
add1_in: (b,b,f)
binaryZ43_in: (b)
binary50_in: (b)
addz101_in: (b,b,f)
addx110_in: (b,b,f)
addy124_in: (b,b,f)
addc136_in: (b,b,f)
succZ146_in: (b,f)
succ153_in: (b,f)
addC171_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

ADD1_IN_GGA(zero(T23), b, zero(T23)) → U30_GGA(T23, binaryZ43_in_g(T23))
ADD1_IN_GGA(zero(T23), b, zero(T23)) → BINARYZ43_IN_G(T23)
BINARYZ43_IN_G(zero(T29)) → U1_G(T29, binaryZ43_in_g(T29))
BINARYZ43_IN_G(zero(T29)) → BINARYZ43_IN_G(T29)
BINARYZ43_IN_G(one(T33)) → U2_G(T33, binary50_in_g(T33))
BINARYZ43_IN_G(one(T33)) → BINARY50_IN_G(T33)
BINARY50_IN_G(zero(T38)) → U3_G(T38, binaryZ43_in_g(T38))
BINARY50_IN_G(zero(T38)) → BINARYZ43_IN_G(T38)
BINARY50_IN_G(one(T42)) → U4_G(T42, binary50_in_g(T42))
BINARY50_IN_G(one(T42)) → BINARY50_IN_G(T42)
ADD1_IN_GGA(one(T47), b, one(T47)) → U31_GGA(T47, binary50_in_g(T47))
ADD1_IN_GGA(one(T47), b, one(T47)) → BINARY50_IN_G(T47)
ADD1_IN_GGA(b, zero(T74), zero(T74)) → U32_GGA(T74, binaryZ43_in_g(T74))
ADD1_IN_GGA(b, zero(T74), zero(T74)) → BINARYZ43_IN_G(T74)
ADD1_IN_GGA(b, one(T80), one(T80)) → U33_GGA(T80, binary50_in_g(T80))
ADD1_IN_GGA(b, one(T80), one(T80)) → BINARY50_IN_G(T80)
ADD1_IN_GGA(zero(T108), zero(T109), zero(T111)) → U34_GGA(T108, T109, T111, addz101_in_gga(T108, T109, T111))
ADD1_IN_GGA(zero(T108), zero(T109), zero(T111)) → ADDZ101_IN_GGA(T108, T109, T111)
ADDZ101_IN_GGA(zero(T127), zero(T128), zero(T130)) → U5_GGA(T127, T128, T130, addz101_in_gga(T127, T128, T130))
ADDZ101_IN_GGA(zero(T127), zero(T128), zero(T130)) → ADDZ101_IN_GGA(T127, T128, T130)
ADDZ101_IN_GGA(zero(T146), one(T147), one(T149)) → U6_GGA(T146, T147, T149, addx110_in_gga(T146, T147, T149))
ADDZ101_IN_GGA(zero(T146), one(T147), one(T149)) → ADDX110_IN_GGA(T146, T147, T149)
ADDX110_IN_GGA(one(T155), b, one(T155)) → U24_GGA(T155, binary50_in_g(T155))
ADDX110_IN_GGA(one(T155), b, one(T155)) → BINARY50_IN_G(T155)
ADDX110_IN_GGA(zero(T160), b, zero(T160)) → U25_GGA(T160, binaryZ43_in_g(T160))
ADDX110_IN_GGA(zero(T160), b, zero(T160)) → BINARYZ43_IN_G(T160)
ADDX110_IN_GGA(T172, T173, T175) → U26_GGA(T172, T173, T175, addz101_in_gga(T172, T173, T175))
ADDX110_IN_GGA(T172, T173, T175) → ADDZ101_IN_GGA(T172, T173, T175)
ADDZ101_IN_GGA(one(T191), zero(T192), one(T194)) → U7_GGA(T191, T192, T194, addy124_in_gga(T191, T192, T194))
ADDZ101_IN_GGA(one(T191), zero(T192), one(T194)) → ADDY124_IN_GGA(T191, T192, T194)
ADDY124_IN_GGA(b, one(T200), one(T200)) → U27_GGA(T200, binary50_in_g(T200))
ADDY124_IN_GGA(b, one(T200), one(T200)) → BINARY50_IN_G(T200)
ADDY124_IN_GGA(b, zero(T205), zero(T205)) → U28_GGA(T205, binaryZ43_in_g(T205))
ADDY124_IN_GGA(b, zero(T205), zero(T205)) → BINARYZ43_IN_G(T205)
ADDY124_IN_GGA(T217, T218, T220) → U29_GGA(T217, T218, T220, addz101_in_gga(T217, T218, T220))
ADDY124_IN_GGA(T217, T218, T220) → ADDZ101_IN_GGA(T217, T218, T220)
ADDZ101_IN_GGA(one(T230), one(T231), zero(T233)) → U8_GGA(T230, T231, T233, addc136_in_gga(T230, T231, T233))
ADDZ101_IN_GGA(one(T230), one(T231), zero(T233)) → ADDC136_IN_GGA(T230, T231, T233)
ADDC136_IN_GGA(T242, b, T244) → U21_GGA(T242, T244, succZ146_in_ga(T242, T244))
ADDC136_IN_GGA(T242, b, T244) → SUCCZ146_IN_GA(T242, T244)
SUCCZ146_IN_GA(zero(T250), one(T250)) → U11_GA(T250, binaryZ43_in_g(T250))
SUCCZ146_IN_GA(zero(T250), one(T250)) → BINARYZ43_IN_G(T250)
SUCCZ146_IN_GA(one(T256), zero(T258)) → U12_GA(T256, T258, succ153_in_ga(T256, T258))
SUCCZ146_IN_GA(one(T256), zero(T258)) → SUCC153_IN_GA(T256, T258)
SUCC153_IN_GA(zero(T263), one(T263)) → U9_GA(T263, binaryZ43_in_g(T263))
SUCC153_IN_GA(zero(T263), one(T263)) → BINARYZ43_IN_G(T263)
SUCC153_IN_GA(one(T269), zero(T271)) → U10_GA(T269, T271, succ153_in_ga(T269, T271))
SUCC153_IN_GA(one(T269), zero(T271)) → SUCC153_IN_GA(T269, T271)
ADDC136_IN_GGA(b, T280, T282) → U22_GGA(T280, T282, succZ146_in_ga(T280, T282))
ADDC136_IN_GGA(b, T280, T282) → SUCCZ146_IN_GA(T280, T282)
ADDC136_IN_GGA(T294, T295, T297) → U23_GGA(T294, T295, T297, addC171_in_gga(T294, T295, T297))
ADDC136_IN_GGA(T294, T295, T297) → ADDC171_IN_GGA(T294, T295, T297)
ADDC171_IN_GGA(zero(T313), zero(T314), one(T316)) → U13_GGA(T313, T314, T316, addz101_in_gga(T313, T314, T316))
ADDC171_IN_GGA(zero(T313), zero(T314), one(T316)) → ADDZ101_IN_GGA(T313, T314, T316)
ADDC171_IN_GGA(zero(zero(T341)), one(b), zero(one(T341))) → U14_GGA(T341, binaryZ43_in_g(T341))
ADDC171_IN_GGA(zero(zero(T341)), one(b), zero(one(T341))) → BINARYZ43_IN_G(T341)
ADDC171_IN_GGA(zero(one(T351)), one(b), zero(zero(T353))) → U15_GGA(T351, T353, succ153_in_ga(T351, T353))
ADDC171_IN_GGA(zero(one(T351)), one(b), zero(zero(T353))) → SUCC153_IN_GA(T351, T353)
ADDC171_IN_GGA(zero(T364), one(T365), zero(T367)) → U16_GGA(T364, T365, T367, addC171_in_gga(T364, T365, T367))
ADDC171_IN_GGA(zero(T364), one(T365), zero(T367)) → ADDC171_IN_GGA(T364, T365, T367)
ADDC171_IN_GGA(one(b), zero(zero(T392)), zero(one(T392))) → U17_GGA(T392, binaryZ43_in_g(T392))
ADDC171_IN_GGA(one(b), zero(zero(T392)), zero(one(T392))) → BINARYZ43_IN_G(T392)
ADDC171_IN_GGA(one(b), zero(one(T402)), zero(zero(T404))) → U18_GGA(T402, T404, succ153_in_ga(T402, T404))
ADDC171_IN_GGA(one(b), zero(one(T402)), zero(zero(T404))) → SUCC153_IN_GA(T402, T404)
ADDC171_IN_GGA(one(T415), zero(T416), zero(T418)) → U19_GGA(T415, T416, T418, addC171_in_gga(T415, T416, T418))
ADDC171_IN_GGA(one(T415), zero(T416), zero(T418)) → ADDC171_IN_GGA(T415, T416, T418)
ADDC171_IN_GGA(one(T428), one(T429), one(T431)) → U20_GGA(T428, T429, T431, addc136_in_gga(T428, T429, T431))
ADDC171_IN_GGA(one(T428), one(T429), one(T431)) → ADDC136_IN_GGA(T428, T429, T431)
ADD1_IN_GGA(zero(T444), one(T445), one(T447)) → U35_GGA(T444, T445, T447, addx110_in_gga(T444, T445, T447))
ADD1_IN_GGA(zero(T444), one(T445), one(T447)) → ADDX110_IN_GGA(T444, T445, T447)
ADD1_IN_GGA(one(T461), zero(T462), one(T464)) → U36_GGA(T461, T462, T464, addy124_in_gga(T461, T462, T464))
ADD1_IN_GGA(one(T461), zero(T462), one(T464)) → ADDY124_IN_GGA(T461, T462, T464)
ADD1_IN_GGA(one(T472), one(T473), zero(T475)) → U37_GGA(T472, T473, T475, addc136_in_gga(T472, T473, T475))
ADD1_IN_GGA(one(T472), one(T473), zero(T475)) → ADDC136_IN_GGA(T472, T473, T475)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1)  =  zero(x1)
b  =  b
binaryZ43_in_g(x1)  =  binaryZ43_in_g(x1)
one(x1)  =  one(x1)
binary50_in_g(x1)  =  binary50_in_g(x1)
addz101_in_gga(x1, x2, x3)  =  addz101_in_gga(x1, x2)
addx110_in_gga(x1, x2, x3)  =  addx110_in_gga(x1, x2)
addy124_in_gga(x1, x2, x3)  =  addy124_in_gga(x1, x2)
addc136_in_gga(x1, x2, x3)  =  addc136_in_gga(x1, x2)
succZ146_in_ga(x1, x2)  =  succZ146_in_ga(x1)
succ153_in_ga(x1, x2)  =  succ153_in_ga(x1)
addC171_in_gga(x1, x2, x3)  =  addC171_in_gga(x1, x2)
ADD1_IN_GGA(x1, x2, x3)  =  ADD1_IN_GGA(x1, x2)
U30_GGA(x1, x2)  =  U30_GGA(x1, x2)
BINARYZ43_IN_G(x1)  =  BINARYZ43_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
U2_G(x1, x2)  =  U2_G(x1, x2)
BINARY50_IN_G(x1)  =  BINARY50_IN_G(x1)
U3_G(x1, x2)  =  U3_G(x1, x2)
U4_G(x1, x2)  =  U4_G(x1, x2)
U31_GGA(x1, x2)  =  U31_GGA(x1, x2)
U32_GGA(x1, x2)  =  U32_GGA(x1, x2)
U33_GGA(x1, x2)  =  U33_GGA(x1, x2)
U34_GGA(x1, x2, x3, x4)  =  U34_GGA(x1, x2, x4)
ADDZ101_IN_GGA(x1, x2, x3)  =  ADDZ101_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
ADDX110_IN_GGA(x1, x2, x3)  =  ADDX110_IN_GGA(x1, x2)
U24_GGA(x1, x2)  =  U24_GGA(x1, x2)
U25_GGA(x1, x2)  =  U25_GGA(x1, x2)
U26_GGA(x1, x2, x3, x4)  =  U26_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
ADDY124_IN_GGA(x1, x2, x3)  =  ADDY124_IN_GGA(x1, x2)
U27_GGA(x1, x2)  =  U27_GGA(x1, x2)
U28_GGA(x1, x2)  =  U28_GGA(x1, x2)
U29_GGA(x1, x2, x3, x4)  =  U29_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
ADDC136_IN_GGA(x1, x2, x3)  =  ADDC136_IN_GGA(x1, x2)
U21_GGA(x1, x2, x3)  =  U21_GGA(x1, x3)
SUCCZ146_IN_GA(x1, x2)  =  SUCCZ146_IN_GA(x1)
U11_GA(x1, x2)  =  U11_GA(x1, x2)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
SUCC153_IN_GA(x1, x2)  =  SUCC153_IN_GA(x1)
U9_GA(x1, x2)  =  U9_GA(x1, x2)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
U22_GGA(x1, x2, x3)  =  U22_GGA(x1, x3)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x1, x2, x4)
ADDC171_IN_GGA(x1, x2, x3)  =  ADDC171_IN_GGA(x1, x2)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)
U14_GGA(x1, x2)  =  U14_GGA(x1, x2)
U15_GGA(x1, x2, x3)  =  U15_GGA(x1, x3)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
U17_GGA(x1, x2)  =  U17_GGA(x1, x2)
U18_GGA(x1, x2, x3)  =  U18_GGA(x1, x3)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x2, x4)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x1, x2, x4)
U35_GGA(x1, x2, x3, x4)  =  U35_GGA(x1, x2, x4)
U36_GGA(x1, x2, x3, x4)  =  U36_GGA(x1, x2, x4)
U37_GGA(x1, x2, x3, x4)  =  U37_GGA(x1, x2, x4)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

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

ADD1_IN_GGA(zero(T23), b, zero(T23)) → U30_GGA(T23, binaryZ43_in_g(T23))
ADD1_IN_GGA(zero(T23), b, zero(T23)) → BINARYZ43_IN_G(T23)
BINARYZ43_IN_G(zero(T29)) → U1_G(T29, binaryZ43_in_g(T29))
BINARYZ43_IN_G(zero(T29)) → BINARYZ43_IN_G(T29)
BINARYZ43_IN_G(one(T33)) → U2_G(T33, binary50_in_g(T33))
BINARYZ43_IN_G(one(T33)) → BINARY50_IN_G(T33)
BINARY50_IN_G(zero(T38)) → U3_G(T38, binaryZ43_in_g(T38))
BINARY50_IN_G(zero(T38)) → BINARYZ43_IN_G(T38)
BINARY50_IN_G(one(T42)) → U4_G(T42, binary50_in_g(T42))
BINARY50_IN_G(one(T42)) → BINARY50_IN_G(T42)
ADD1_IN_GGA(one(T47), b, one(T47)) → U31_GGA(T47, binary50_in_g(T47))
ADD1_IN_GGA(one(T47), b, one(T47)) → BINARY50_IN_G(T47)
ADD1_IN_GGA(b, zero(T74), zero(T74)) → U32_GGA(T74, binaryZ43_in_g(T74))
ADD1_IN_GGA(b, zero(T74), zero(T74)) → BINARYZ43_IN_G(T74)
ADD1_IN_GGA(b, one(T80), one(T80)) → U33_GGA(T80, binary50_in_g(T80))
ADD1_IN_GGA(b, one(T80), one(T80)) → BINARY50_IN_G(T80)
ADD1_IN_GGA(zero(T108), zero(T109), zero(T111)) → U34_GGA(T108, T109, T111, addz101_in_gga(T108, T109, T111))
ADD1_IN_GGA(zero(T108), zero(T109), zero(T111)) → ADDZ101_IN_GGA(T108, T109, T111)
ADDZ101_IN_GGA(zero(T127), zero(T128), zero(T130)) → U5_GGA(T127, T128, T130, addz101_in_gga(T127, T128, T130))
ADDZ101_IN_GGA(zero(T127), zero(T128), zero(T130)) → ADDZ101_IN_GGA(T127, T128, T130)
ADDZ101_IN_GGA(zero(T146), one(T147), one(T149)) → U6_GGA(T146, T147, T149, addx110_in_gga(T146, T147, T149))
ADDZ101_IN_GGA(zero(T146), one(T147), one(T149)) → ADDX110_IN_GGA(T146, T147, T149)
ADDX110_IN_GGA(one(T155), b, one(T155)) → U24_GGA(T155, binary50_in_g(T155))
ADDX110_IN_GGA(one(T155), b, one(T155)) → BINARY50_IN_G(T155)
ADDX110_IN_GGA(zero(T160), b, zero(T160)) → U25_GGA(T160, binaryZ43_in_g(T160))
ADDX110_IN_GGA(zero(T160), b, zero(T160)) → BINARYZ43_IN_G(T160)
ADDX110_IN_GGA(T172, T173, T175) → U26_GGA(T172, T173, T175, addz101_in_gga(T172, T173, T175))
ADDX110_IN_GGA(T172, T173, T175) → ADDZ101_IN_GGA(T172, T173, T175)
ADDZ101_IN_GGA(one(T191), zero(T192), one(T194)) → U7_GGA(T191, T192, T194, addy124_in_gga(T191, T192, T194))
ADDZ101_IN_GGA(one(T191), zero(T192), one(T194)) → ADDY124_IN_GGA(T191, T192, T194)
ADDY124_IN_GGA(b, one(T200), one(T200)) → U27_GGA(T200, binary50_in_g(T200))
ADDY124_IN_GGA(b, one(T200), one(T200)) → BINARY50_IN_G(T200)
ADDY124_IN_GGA(b, zero(T205), zero(T205)) → U28_GGA(T205, binaryZ43_in_g(T205))
ADDY124_IN_GGA(b, zero(T205), zero(T205)) → BINARYZ43_IN_G(T205)
ADDY124_IN_GGA(T217, T218, T220) → U29_GGA(T217, T218, T220, addz101_in_gga(T217, T218, T220))
ADDY124_IN_GGA(T217, T218, T220) → ADDZ101_IN_GGA(T217, T218, T220)
ADDZ101_IN_GGA(one(T230), one(T231), zero(T233)) → U8_GGA(T230, T231, T233, addc136_in_gga(T230, T231, T233))
ADDZ101_IN_GGA(one(T230), one(T231), zero(T233)) → ADDC136_IN_GGA(T230, T231, T233)
ADDC136_IN_GGA(T242, b, T244) → U21_GGA(T242, T244, succZ146_in_ga(T242, T244))
ADDC136_IN_GGA(T242, b, T244) → SUCCZ146_IN_GA(T242, T244)
SUCCZ146_IN_GA(zero(T250), one(T250)) → U11_GA(T250, binaryZ43_in_g(T250))
SUCCZ146_IN_GA(zero(T250), one(T250)) → BINARYZ43_IN_G(T250)
SUCCZ146_IN_GA(one(T256), zero(T258)) → U12_GA(T256, T258, succ153_in_ga(T256, T258))
SUCCZ146_IN_GA(one(T256), zero(T258)) → SUCC153_IN_GA(T256, T258)
SUCC153_IN_GA(zero(T263), one(T263)) → U9_GA(T263, binaryZ43_in_g(T263))
SUCC153_IN_GA(zero(T263), one(T263)) → BINARYZ43_IN_G(T263)
SUCC153_IN_GA(one(T269), zero(T271)) → U10_GA(T269, T271, succ153_in_ga(T269, T271))
SUCC153_IN_GA(one(T269), zero(T271)) → SUCC153_IN_GA(T269, T271)
ADDC136_IN_GGA(b, T280, T282) → U22_GGA(T280, T282, succZ146_in_ga(T280, T282))
ADDC136_IN_GGA(b, T280, T282) → SUCCZ146_IN_GA(T280, T282)
ADDC136_IN_GGA(T294, T295, T297) → U23_GGA(T294, T295, T297, addC171_in_gga(T294, T295, T297))
ADDC136_IN_GGA(T294, T295, T297) → ADDC171_IN_GGA(T294, T295, T297)
ADDC171_IN_GGA(zero(T313), zero(T314), one(T316)) → U13_GGA(T313, T314, T316, addz101_in_gga(T313, T314, T316))
ADDC171_IN_GGA(zero(T313), zero(T314), one(T316)) → ADDZ101_IN_GGA(T313, T314, T316)
ADDC171_IN_GGA(zero(zero(T341)), one(b), zero(one(T341))) → U14_GGA(T341, binaryZ43_in_g(T341))
ADDC171_IN_GGA(zero(zero(T341)), one(b), zero(one(T341))) → BINARYZ43_IN_G(T341)
ADDC171_IN_GGA(zero(one(T351)), one(b), zero(zero(T353))) → U15_GGA(T351, T353, succ153_in_ga(T351, T353))
ADDC171_IN_GGA(zero(one(T351)), one(b), zero(zero(T353))) → SUCC153_IN_GA(T351, T353)
ADDC171_IN_GGA(zero(T364), one(T365), zero(T367)) → U16_GGA(T364, T365, T367, addC171_in_gga(T364, T365, T367))
ADDC171_IN_GGA(zero(T364), one(T365), zero(T367)) → ADDC171_IN_GGA(T364, T365, T367)
ADDC171_IN_GGA(one(b), zero(zero(T392)), zero(one(T392))) → U17_GGA(T392, binaryZ43_in_g(T392))
ADDC171_IN_GGA(one(b), zero(zero(T392)), zero(one(T392))) → BINARYZ43_IN_G(T392)
ADDC171_IN_GGA(one(b), zero(one(T402)), zero(zero(T404))) → U18_GGA(T402, T404, succ153_in_ga(T402, T404))
ADDC171_IN_GGA(one(b), zero(one(T402)), zero(zero(T404))) → SUCC153_IN_GA(T402, T404)
ADDC171_IN_GGA(one(T415), zero(T416), zero(T418)) → U19_GGA(T415, T416, T418, addC171_in_gga(T415, T416, T418))
ADDC171_IN_GGA(one(T415), zero(T416), zero(T418)) → ADDC171_IN_GGA(T415, T416, T418)
ADDC171_IN_GGA(one(T428), one(T429), one(T431)) → U20_GGA(T428, T429, T431, addc136_in_gga(T428, T429, T431))
ADDC171_IN_GGA(one(T428), one(T429), one(T431)) → ADDC136_IN_GGA(T428, T429, T431)
ADD1_IN_GGA(zero(T444), one(T445), one(T447)) → U35_GGA(T444, T445, T447, addx110_in_gga(T444, T445, T447))
ADD1_IN_GGA(zero(T444), one(T445), one(T447)) → ADDX110_IN_GGA(T444, T445, T447)
ADD1_IN_GGA(one(T461), zero(T462), one(T464)) → U36_GGA(T461, T462, T464, addy124_in_gga(T461, T462, T464))
ADD1_IN_GGA(one(T461), zero(T462), one(T464)) → ADDY124_IN_GGA(T461, T462, T464)
ADD1_IN_GGA(one(T472), one(T473), zero(T475)) → U37_GGA(T472, T473, T475, addc136_in_gga(T472, T473, T475))
ADD1_IN_GGA(one(T472), one(T473), zero(T475)) → ADDC136_IN_GGA(T472, T473, T475)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1)  =  zero(x1)
b  =  b
binaryZ43_in_g(x1)  =  binaryZ43_in_g(x1)
one(x1)  =  one(x1)
binary50_in_g(x1)  =  binary50_in_g(x1)
addz101_in_gga(x1, x2, x3)  =  addz101_in_gga(x1, x2)
addx110_in_gga(x1, x2, x3)  =  addx110_in_gga(x1, x2)
addy124_in_gga(x1, x2, x3)  =  addy124_in_gga(x1, x2)
addc136_in_gga(x1, x2, x3)  =  addc136_in_gga(x1, x2)
succZ146_in_ga(x1, x2)  =  succZ146_in_ga(x1)
succ153_in_ga(x1, x2)  =  succ153_in_ga(x1)
addC171_in_gga(x1, x2, x3)  =  addC171_in_gga(x1, x2)
ADD1_IN_GGA(x1, x2, x3)  =  ADD1_IN_GGA(x1, x2)
U30_GGA(x1, x2)  =  U30_GGA(x1, x2)
BINARYZ43_IN_G(x1)  =  BINARYZ43_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
U2_G(x1, x2)  =  U2_G(x1, x2)
BINARY50_IN_G(x1)  =  BINARY50_IN_G(x1)
U3_G(x1, x2)  =  U3_G(x1, x2)
U4_G(x1, x2)  =  U4_G(x1, x2)
U31_GGA(x1, x2)  =  U31_GGA(x1, x2)
U32_GGA(x1, x2)  =  U32_GGA(x1, x2)
U33_GGA(x1, x2)  =  U33_GGA(x1, x2)
U34_GGA(x1, x2, x3, x4)  =  U34_GGA(x1, x2, x4)
ADDZ101_IN_GGA(x1, x2, x3)  =  ADDZ101_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
ADDX110_IN_GGA(x1, x2, x3)  =  ADDX110_IN_GGA(x1, x2)
U24_GGA(x1, x2)  =  U24_GGA(x1, x2)
U25_GGA(x1, x2)  =  U25_GGA(x1, x2)
U26_GGA(x1, x2, x3, x4)  =  U26_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
ADDY124_IN_GGA(x1, x2, x3)  =  ADDY124_IN_GGA(x1, x2)
U27_GGA(x1, x2)  =  U27_GGA(x1, x2)
U28_GGA(x1, x2)  =  U28_GGA(x1, x2)
U29_GGA(x1, x2, x3, x4)  =  U29_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
ADDC136_IN_GGA(x1, x2, x3)  =  ADDC136_IN_GGA(x1, x2)
U21_GGA(x1, x2, x3)  =  U21_GGA(x1, x3)
SUCCZ146_IN_GA(x1, x2)  =  SUCCZ146_IN_GA(x1)
U11_GA(x1, x2)  =  U11_GA(x1, x2)
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
SUCC153_IN_GA(x1, x2)  =  SUCC153_IN_GA(x1)
U9_GA(x1, x2)  =  U9_GA(x1, x2)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
U22_GGA(x1, x2, x3)  =  U22_GGA(x1, x3)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x1, x2, x4)
ADDC171_IN_GGA(x1, x2, x3)  =  ADDC171_IN_GGA(x1, x2)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)
U14_GGA(x1, x2)  =  U14_GGA(x1, x2)
U15_GGA(x1, x2, x3)  =  U15_GGA(x1, x3)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
U17_GGA(x1, x2)  =  U17_GGA(x1, x2)
U18_GGA(x1, x2, x3)  =  U18_GGA(x1, x3)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x2, x4)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x1, x2, x4)
U35_GGA(x1, x2, x3, x4)  =  U35_GGA(x1, x2, x4)
U36_GGA(x1, x2, x3, x4)  =  U36_GGA(x1, x2, x4)
U37_GGA(x1, x2, x3, x4)  =  U37_GGA(x1, x2, x4)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

BINARYZ43_IN_G(one(T33)) → BINARY50_IN_G(T33)
BINARY50_IN_G(zero(T38)) → BINARYZ43_IN_G(T38)
BINARYZ43_IN_G(zero(T29)) → BINARYZ43_IN_G(T29)
BINARY50_IN_G(one(T42)) → BINARY50_IN_G(T42)

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

(10) PiDPToQDPProof (EQUIVALENT transformation)

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

(11) Obligation:

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

BINARYZ43_IN_G(one(T33)) → BINARY50_IN_G(T33)
BINARY50_IN_G(zero(T38)) → BINARYZ43_IN_G(T38)
BINARYZ43_IN_G(zero(T29)) → BINARYZ43_IN_G(T29)
BINARY50_IN_G(one(T42)) → BINARY50_IN_G(T42)

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:

  • BINARY50_IN_G(zero(T38)) → BINARYZ43_IN_G(T38)
    The graph contains the following edges 1 > 1

  • BINARY50_IN_G(one(T42)) → BINARY50_IN_G(T42)
    The graph contains the following edges 1 > 1

  • BINARYZ43_IN_G(zero(T29)) → BINARYZ43_IN_G(T29)
    The graph contains the following edges 1 > 1

  • BINARYZ43_IN_G(one(T33)) → BINARY50_IN_G(T33)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

SUCC153_IN_GA(one(T269), zero(T271)) → SUCC153_IN_GA(T269, T271)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1)  =  zero(x1)
one(x1)  =  one(x1)
SUCC153_IN_GA(x1, x2)  =  SUCC153_IN_GA(x1)

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

(15) PiDPToQDPProof (SOUND transformation)

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

(16) Obligation:

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

SUCC153_IN_GA(one(T269)) → SUCC153_IN_GA(T269)

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

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

  • SUCC153_IN_GA(one(T269)) → SUCC153_IN_GA(T269)
    The graph contains the following edges 1 > 1

(18) YES

(19) Obligation:

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

ADDX110_IN_GGA(T172, T173, T175) → ADDZ101_IN_GGA(T172, T173, T175)
ADDZ101_IN_GGA(zero(T127), zero(T128), zero(T130)) → ADDZ101_IN_GGA(T127, T128, T130)
ADDZ101_IN_GGA(zero(T146), one(T147), one(T149)) → ADDX110_IN_GGA(T146, T147, T149)
ADDZ101_IN_GGA(one(T191), zero(T192), one(T194)) → ADDY124_IN_GGA(T191, T192, T194)
ADDY124_IN_GGA(T217, T218, T220) → ADDZ101_IN_GGA(T217, T218, T220)
ADDZ101_IN_GGA(one(T230), one(T231), zero(T233)) → ADDC136_IN_GGA(T230, T231, T233)
ADDC136_IN_GGA(T294, T295, T297) → ADDC171_IN_GGA(T294, T295, T297)
ADDC171_IN_GGA(zero(T313), zero(T314), one(T316)) → ADDZ101_IN_GGA(T313, T314, T316)
ADDC171_IN_GGA(zero(T364), one(T365), zero(T367)) → ADDC171_IN_GGA(T364, T365, T367)
ADDC171_IN_GGA(one(T415), zero(T416), zero(T418)) → ADDC171_IN_GGA(T415, T416, T418)
ADDC171_IN_GGA(one(T428), one(T429), one(T431)) → ADDC136_IN_GGA(T428, T429, T431)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1)  =  zero(x1)
one(x1)  =  one(x1)
ADDZ101_IN_GGA(x1, x2, x3)  =  ADDZ101_IN_GGA(x1, x2)
ADDX110_IN_GGA(x1, x2, x3)  =  ADDX110_IN_GGA(x1, x2)
ADDY124_IN_GGA(x1, x2, x3)  =  ADDY124_IN_GGA(x1, x2)
ADDC136_IN_GGA(x1, x2, x3)  =  ADDC136_IN_GGA(x1, x2)
ADDC171_IN_GGA(x1, x2, x3)  =  ADDC171_IN_GGA(x1, x2)

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

(20) PiDPToQDPProof (SOUND transformation)

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

(21) Obligation:

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

ADDX110_IN_GGA(T172, T173) → ADDZ101_IN_GGA(T172, T173)
ADDZ101_IN_GGA(zero(T127), zero(T128)) → ADDZ101_IN_GGA(T127, T128)
ADDZ101_IN_GGA(zero(T146), one(T147)) → ADDX110_IN_GGA(T146, T147)
ADDZ101_IN_GGA(one(T191), zero(T192)) → ADDY124_IN_GGA(T191, T192)
ADDY124_IN_GGA(T217, T218) → ADDZ101_IN_GGA(T217, T218)
ADDZ101_IN_GGA(one(T230), one(T231)) → ADDC136_IN_GGA(T230, T231)
ADDC136_IN_GGA(T294, T295) → ADDC171_IN_GGA(T294, T295)
ADDC171_IN_GGA(zero(T313), zero(T314)) → ADDZ101_IN_GGA(T313, T314)
ADDC171_IN_GGA(zero(T364), one(T365)) → ADDC171_IN_GGA(T364, T365)
ADDC171_IN_GGA(one(T415), zero(T416)) → ADDC171_IN_GGA(T415, T416)
ADDC171_IN_GGA(one(T428), one(T429)) → ADDC136_IN_GGA(T428, T429)

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

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

  • ADDZ101_IN_GGA(zero(T146), one(T147)) → ADDX110_IN_GGA(T146, T147)
    The graph contains the following edges 1 > 1, 2 > 2

  • ADDZ101_IN_GGA(zero(T127), zero(T128)) → ADDZ101_IN_GGA(T127, T128)
    The graph contains the following edges 1 > 1, 2 > 2

  • ADDX110_IN_GGA(T172, T173) → ADDZ101_IN_GGA(T172, T173)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • ADDY124_IN_GGA(T217, T218) → ADDZ101_IN_GGA(T217, T218)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • ADDC171_IN_GGA(zero(T313), zero(T314)) → ADDZ101_IN_GGA(T313, T314)
    The graph contains the following edges 1 > 1, 2 > 2

  • ADDZ101_IN_GGA(one(T191), zero(T192)) → ADDY124_IN_GGA(T191, T192)
    The graph contains the following edges 1 > 1, 2 > 2

  • ADDZ101_IN_GGA(one(T230), one(T231)) → ADDC136_IN_GGA(T230, T231)
    The graph contains the following edges 1 > 1, 2 > 2

  • ADDC136_IN_GGA(T294, T295) → ADDC171_IN_GGA(T294, T295)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • ADDC171_IN_GGA(one(T428), one(T429)) → ADDC136_IN_GGA(T428, T429)
    The graph contains the following edges 1 > 1, 2 > 2

  • ADDC171_IN_GGA(zero(T364), one(T365)) → ADDC171_IN_GGA(T364, T365)
    The graph contains the following edges 1 > 1, 2 > 2

  • ADDC171_IN_GGA(one(T415), zero(T416)) → ADDC171_IN_GGA(T415, T416)
    The graph contains the following edges 1 > 1, 2 > 2

(23) YES