(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)).
Query: add(g,g,a)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
binaryZA(zero(X1)) :- binaryZA(X1).
binaryZA(one(X1)) :- binaryB(X1).
binaryB(zero(X1)) :- binaryZA(X1).
binaryB(one(X1)) :- binaryB(X1).
addzC(zero(X1), zero(X2), zero(X3)) :- addzC(X1, X2, X3).
addzC(zero(X1), one(X2), one(X3)) :- addxD(X1, X2, X3).
addzC(one(X1), zero(X2), one(X3)) :- addyE(X1, X2, X3).
addzC(one(X1), one(X2), zero(X3)) :- addcF(X1, X2, X3).
succG(zero(X1), one(X1)) :- binaryZA(X1).
succG(one(X1), zero(X2)) :- succG(X1, X2).
succZH(zero(X1), one(X1)) :- binaryZA(X1).
succZH(one(X1), zero(X2)) :- succG(X1, X2).
addCI(zero(X1), zero(X2), one(X3)) :- addzC(X1, X2, X3).
addCI(zero(zero(X1)), one(b), zero(one(X1))) :- binaryZA(X1).
addCI(zero(one(X1)), one(b), zero(zero(X2))) :- succG(X1, X2).
addCI(zero(X1), one(X2), zero(X3)) :- addCI(X1, X2, X3).
addCI(one(b), zero(zero(X1)), zero(one(X1))) :- binaryZA(X1).
addCI(one(b), zero(one(X1)), zero(zero(X2))) :- succG(X1, X2).
addCI(one(X1), zero(X2), zero(X3)) :- addCI(X1, X2, X3).
addCI(one(X1), one(X2), one(X3)) :- addcF(X1, X2, X3).
addcF(X1, b, X2) :- succZH(X1, X2).
addcF(b, X1, X2) :- succZH(X1, X2).
addcF(X1, X2, X3) :- addCI(X1, X2, X3).
addxD(one(X1), b, one(X1)) :- binaryB(X1).
addxD(zero(X1), b, zero(X1)) :- binaryZA(X1).
addxD(X1, X2, X3) :- addzC(X1, X2, X3).
addyE(b, one(X1), one(X1)) :- binaryB(X1).
addyE(b, zero(X1), zero(X1)) :- binaryZA(X1).
addyE(X1, X2, X3) :- addzC(X1, X2, X3).
addJ(b, b, b) :- binaryZK.
addJ(b, b, X1) :- addzL(X1).
addJ(b, b, X1) :- addzL(X1).
addJ(zero(X1), b, zero(X1)) :- binaryZA(X1).
addJ(one(X1), b, one(X1)) :- binaryB(X1).
addJ(b, b, b) :- binaryZK.
addJ(b, zero(X1), zero(X1)) :- binaryZA(X1).
addJ(b, one(X1), one(X1)) :- binaryB(X1).
addJ(zero(X1), zero(X2), zero(X3)) :- addzC(X1, X2, X3).
addJ(zero(X1), one(X2), one(X3)) :- addxD(X1, X2, X3).
addJ(one(X1), zero(X2), one(X3)) :- addyE(X1, X2, X3).
addJ(one(X1), one(X2), zero(X3)) :- addcF(X1, X2, X3).
Clauses:
binaryZcA(zero(X1)) :- binaryZcA(X1).
binaryZcA(one(X1)) :- binarycB(X1).
binarycB(b).
binarycB(zero(X1)) :- binaryZcA(X1).
binarycB(one(X1)) :- binarycB(X1).
addzcC(zero(X1), zero(X2), zero(X3)) :- addzcC(X1, X2, X3).
addzcC(zero(X1), one(X2), one(X3)) :- addxcD(X1, X2, X3).
addzcC(one(X1), zero(X2), one(X3)) :- addycE(X1, X2, X3).
addzcC(one(X1), one(X2), zero(X3)) :- addccF(X1, X2, X3).
succcG(b, one(b)).
succcG(zero(X1), one(X1)) :- binaryZcA(X1).
succcG(one(X1), zero(X2)) :- succcG(X1, X2).
succZcH(zero(X1), one(X1)) :- binaryZcA(X1).
succZcH(one(X1), zero(X2)) :- succcG(X1, X2).
addCcI(zero(X1), zero(X2), one(X3)) :- addzcC(X1, X2, X3).
addCcI(zero(zero(X1)), one(b), zero(one(X1))) :- binaryZcA(X1).
addCcI(zero(one(X1)), one(b), zero(zero(X2))) :- succcG(X1, X2).
addCcI(zero(X1), one(X2), zero(X3)) :- addCcI(X1, X2, X3).
addCcI(one(b), zero(zero(X1)), zero(one(X1))) :- binaryZcA(X1).
addCcI(one(b), zero(one(X1)), zero(zero(X2))) :- succcG(X1, X2).
addCcI(one(X1), zero(X2), zero(X3)) :- addCcI(X1, X2, X3).
addCcI(one(X1), one(X2), one(X3)) :- addccF(X1, X2, X3).
addccF(b, b, one(b)).
addccF(X1, b, X2) :- succZcH(X1, X2).
addccF(b, X1, X2) :- succZcH(X1, X2).
addccF(X1, X2, X3) :- addCcI(X1, X2, X3).
addxcD(one(X1), b, one(X1)) :- binarycB(X1).
addxcD(zero(X1), b, zero(X1)) :- binaryZcA(X1).
addxcD(X1, X2, X3) :- addzcC(X1, X2, X3).
addycE(b, one(X1), one(X1)) :- binarycB(X1).
addycE(b, zero(X1), zero(X1)) :- binaryZcA(X1).
addycE(X1, X2, X3) :- addzcC(X1, X2, X3).
Afs:
addJ(x1, x2, x3) = addJ(x1, x2)
(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)
Deleted triples and predicates having undefined goals [DT09].
(4) Obligation:
Triples:
binaryZA(zero(X1)) :- binaryZA(X1).
binaryZA(one(X1)) :- binaryB(X1).
binaryB(zero(X1)) :- binaryZA(X1).
binaryB(one(X1)) :- binaryB(X1).
addzC(zero(X1), zero(X2), zero(X3)) :- addzC(X1, X2, X3).
addzC(zero(X1), one(X2), one(X3)) :- addxD(X1, X2, X3).
addzC(one(X1), zero(X2), one(X3)) :- addyE(X1, X2, X3).
addzC(one(X1), one(X2), zero(X3)) :- addcF(X1, X2, X3).
succG(zero(X1), one(X1)) :- binaryZA(X1).
succG(one(X1), zero(X2)) :- succG(X1, X2).
succZH(zero(X1), one(X1)) :- binaryZA(X1).
succZH(one(X1), zero(X2)) :- succG(X1, X2).
addCI(zero(X1), zero(X2), one(X3)) :- addzC(X1, X2, X3).
addCI(zero(zero(X1)), one(b), zero(one(X1))) :- binaryZA(X1).
addCI(zero(one(X1)), one(b), zero(zero(X2))) :- succG(X1, X2).
addCI(zero(X1), one(X2), zero(X3)) :- addCI(X1, X2, X3).
addCI(one(b), zero(zero(X1)), zero(one(X1))) :- binaryZA(X1).
addCI(one(b), zero(one(X1)), zero(zero(X2))) :- succG(X1, X2).
addCI(one(X1), zero(X2), zero(X3)) :- addCI(X1, X2, X3).
addCI(one(X1), one(X2), one(X3)) :- addcF(X1, X2, X3).
addcF(X1, b, X2) :- succZH(X1, X2).
addcF(b, X1, X2) :- succZH(X1, X2).
addcF(X1, X2, X3) :- addCI(X1, X2, X3).
addxD(one(X1), b, one(X1)) :- binaryB(X1).
addxD(zero(X1), b, zero(X1)) :- binaryZA(X1).
addxD(X1, X2, X3) :- addzC(X1, X2, X3).
addyE(b, one(X1), one(X1)) :- binaryB(X1).
addyE(b, zero(X1), zero(X1)) :- binaryZA(X1).
addyE(X1, X2, X3) :- addzC(X1, X2, X3).
addJ(zero(X1), b, zero(X1)) :- binaryZA(X1).
addJ(one(X1), b, one(X1)) :- binaryB(X1).
addJ(b, zero(X1), zero(X1)) :- binaryZA(X1).
addJ(b, one(X1), one(X1)) :- binaryB(X1).
addJ(zero(X1), zero(X2), zero(X3)) :- addzC(X1, X2, X3).
addJ(zero(X1), one(X2), one(X3)) :- addxD(X1, X2, X3).
addJ(one(X1), zero(X2), one(X3)) :- addyE(X1, X2, X3).
addJ(one(X1), one(X2), zero(X3)) :- addcF(X1, X2, X3).
Clauses:
binaryZcA(zero(X1)) :- binaryZcA(X1).
binaryZcA(one(X1)) :- binarycB(X1).
binarycB(b).
binarycB(zero(X1)) :- binaryZcA(X1).
binarycB(one(X1)) :- binarycB(X1).
addzcC(zero(X1), zero(X2), zero(X3)) :- addzcC(X1, X2, X3).
addzcC(zero(X1), one(X2), one(X3)) :- addxcD(X1, X2, X3).
addzcC(one(X1), zero(X2), one(X3)) :- addycE(X1, X2, X3).
addzcC(one(X1), one(X2), zero(X3)) :- addccF(X1, X2, X3).
succcG(b, one(b)).
succcG(zero(X1), one(X1)) :- binaryZcA(X1).
succcG(one(X1), zero(X2)) :- succcG(X1, X2).
succZcH(zero(X1), one(X1)) :- binaryZcA(X1).
succZcH(one(X1), zero(X2)) :- succcG(X1, X2).
addCcI(zero(X1), zero(X2), one(X3)) :- addzcC(X1, X2, X3).
addCcI(zero(zero(X1)), one(b), zero(one(X1))) :- binaryZcA(X1).
addCcI(zero(one(X1)), one(b), zero(zero(X2))) :- succcG(X1, X2).
addCcI(zero(X1), one(X2), zero(X3)) :- addCcI(X1, X2, X3).
addCcI(one(b), zero(zero(X1)), zero(one(X1))) :- binaryZcA(X1).
addCcI(one(b), zero(one(X1)), zero(zero(X2))) :- succcG(X1, X2).
addCcI(one(X1), zero(X2), zero(X3)) :- addCcI(X1, X2, X3).
addCcI(one(X1), one(X2), one(X3)) :- addccF(X1, X2, X3).
addccF(b, b, one(b)).
addccF(X1, b, X2) :- succZcH(X1, X2).
addccF(b, X1, X2) :- succZcH(X1, X2).
addccF(X1, X2, X3) :- addCcI(X1, X2, X3).
addxcD(one(X1), b, one(X1)) :- binarycB(X1).
addxcD(zero(X1), b, zero(X1)) :- binaryZcA(X1).
addxcD(X1, X2, X3) :- addzcC(X1, X2, X3).
addycE(b, one(X1), one(X1)) :- binarycB(X1).
addycE(b, zero(X1), zero(X1)) :- binaryZcA(X1).
addycE(X1, X2, X3) :- addzcC(X1, X2, X3).
Afs:
addJ(x1, x2, x3) = addJ(x1, x2)
(5) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
addJ_in: (b,b,f)
binaryZA_in: (b)
binaryB_in: (b)
addzC_in: (b,b,f)
addxD_in: (b,b,f)
addyE_in: (b,b,f)
addcF_in: (b,b,f)
succZH_in: (b,f)
succG_in: (b,f)
addCI_in: (b,b,f)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
ADDJ_IN_GGA(zero(X1), b, zero(X1)) → U30_GGA(X1, binaryZA_in_g(X1))
ADDJ_IN_GGA(zero(X1), b, zero(X1)) → BINARYZA_IN_G(X1)
BINARYZA_IN_G(zero(X1)) → U1_G(X1, binaryZA_in_g(X1))
BINARYZA_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYZA_IN_G(one(X1)) → U2_G(X1, binaryB_in_g(X1))
BINARYZA_IN_G(one(X1)) → BINARYB_IN_G(X1)
BINARYB_IN_G(zero(X1)) → U3_G(X1, binaryZA_in_g(X1))
BINARYB_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYB_IN_G(one(X1)) → U4_G(X1, binaryB_in_g(X1))
BINARYB_IN_G(one(X1)) → BINARYB_IN_G(X1)
ADDJ_IN_GGA(one(X1), b, one(X1)) → U31_GGA(X1, binaryB_in_g(X1))
ADDJ_IN_GGA(one(X1), b, one(X1)) → BINARYB_IN_G(X1)
ADDJ_IN_GGA(b, zero(X1), zero(X1)) → U32_GGA(X1, binaryZA_in_g(X1))
ADDJ_IN_GGA(b, zero(X1), zero(X1)) → BINARYZA_IN_G(X1)
ADDJ_IN_GGA(b, one(X1), one(X1)) → U33_GGA(X1, binaryB_in_g(X1))
ADDJ_IN_GGA(b, one(X1), one(X1)) → BINARYB_IN_G(X1)
ADDJ_IN_GGA(zero(X1), zero(X2), zero(X3)) → U34_GGA(X1, X2, X3, addzC_in_gga(X1, X2, X3))
ADDJ_IN_GGA(zero(X1), zero(X2), zero(X3)) → ADDZC_IN_GGA(X1, X2, X3)
ADDZC_IN_GGA(zero(X1), zero(X2), zero(X3)) → U5_GGA(X1, X2, X3, addzC_in_gga(X1, X2, X3))
ADDZC_IN_GGA(zero(X1), zero(X2), zero(X3)) → ADDZC_IN_GGA(X1, X2, X3)
ADDZC_IN_GGA(zero(X1), one(X2), one(X3)) → U6_GGA(X1, X2, X3, addxD_in_gga(X1, X2, X3))
ADDZC_IN_GGA(zero(X1), one(X2), one(X3)) → ADDXD_IN_GGA(X1, X2, X3)
ADDXD_IN_GGA(one(X1), b, one(X1)) → U24_GGA(X1, binaryB_in_g(X1))
ADDXD_IN_GGA(one(X1), b, one(X1)) → BINARYB_IN_G(X1)
ADDXD_IN_GGA(zero(X1), b, zero(X1)) → U25_GGA(X1, binaryZA_in_g(X1))
ADDXD_IN_GGA(zero(X1), b, zero(X1)) → BINARYZA_IN_G(X1)
ADDXD_IN_GGA(X1, X2, X3) → U26_GGA(X1, X2, X3, addzC_in_gga(X1, X2, X3))
ADDXD_IN_GGA(X1, X2, X3) → ADDZC_IN_GGA(X1, X2, X3)
ADDZC_IN_GGA(one(X1), zero(X2), one(X3)) → U7_GGA(X1, X2, X3, addyE_in_gga(X1, X2, X3))
ADDZC_IN_GGA(one(X1), zero(X2), one(X3)) → ADDYE_IN_GGA(X1, X2, X3)
ADDYE_IN_GGA(b, one(X1), one(X1)) → U27_GGA(X1, binaryB_in_g(X1))
ADDYE_IN_GGA(b, one(X1), one(X1)) → BINARYB_IN_G(X1)
ADDYE_IN_GGA(b, zero(X1), zero(X1)) → U28_GGA(X1, binaryZA_in_g(X1))
ADDYE_IN_GGA(b, zero(X1), zero(X1)) → BINARYZA_IN_G(X1)
ADDYE_IN_GGA(X1, X2, X3) → U29_GGA(X1, X2, X3, addzC_in_gga(X1, X2, X3))
ADDYE_IN_GGA(X1, X2, X3) → ADDZC_IN_GGA(X1, X2, X3)
ADDZC_IN_GGA(one(X1), one(X2), zero(X3)) → U8_GGA(X1, X2, X3, addcF_in_gga(X1, X2, X3))
ADDZC_IN_GGA(one(X1), one(X2), zero(X3)) → ADDCF_IN_GGA(X1, X2, X3)
ADDCF_IN_GGA(X1, b, X2) → U21_GGA(X1, X2, succZH_in_ga(X1, X2))
ADDCF_IN_GGA(X1, b, X2) → SUCCZH_IN_GA(X1, X2)
SUCCZH_IN_GA(zero(X1), one(X1)) → U11_GA(X1, binaryZA_in_g(X1))
SUCCZH_IN_GA(zero(X1), one(X1)) → BINARYZA_IN_G(X1)
SUCCZH_IN_GA(one(X1), zero(X2)) → U12_GA(X1, X2, succG_in_ga(X1, X2))
SUCCZH_IN_GA(one(X1), zero(X2)) → SUCCG_IN_GA(X1, X2)
SUCCG_IN_GA(zero(X1), one(X1)) → U9_GA(X1, binaryZA_in_g(X1))
SUCCG_IN_GA(zero(X1), one(X1)) → BINARYZA_IN_G(X1)
SUCCG_IN_GA(one(X1), zero(X2)) → U10_GA(X1, X2, succG_in_ga(X1, X2))
SUCCG_IN_GA(one(X1), zero(X2)) → SUCCG_IN_GA(X1, X2)
ADDCF_IN_GGA(b, X1, X2) → U22_GGA(X1, X2, succZH_in_ga(X1, X2))
ADDCF_IN_GGA(b, X1, X2) → SUCCZH_IN_GA(X1, X2)
ADDCF_IN_GGA(X1, X2, X3) → U23_GGA(X1, X2, X3, addCI_in_gga(X1, X2, X3))
ADDCF_IN_GGA(X1, X2, X3) → ADDCI_IN_GGA(X1, X2, X3)
ADDCI_IN_GGA(zero(X1), zero(X2), one(X3)) → U13_GGA(X1, X2, X3, addzC_in_gga(X1, X2, X3))
ADDCI_IN_GGA(zero(X1), zero(X2), one(X3)) → ADDZC_IN_GGA(X1, X2, X3)
ADDCI_IN_GGA(zero(zero(X1)), one(b), zero(one(X1))) → U14_GGA(X1, binaryZA_in_g(X1))
ADDCI_IN_GGA(zero(zero(X1)), one(b), zero(one(X1))) → BINARYZA_IN_G(X1)
ADDCI_IN_GGA(zero(one(X1)), one(b), zero(zero(X2))) → U15_GGA(X1, X2, succG_in_ga(X1, X2))
ADDCI_IN_GGA(zero(one(X1)), one(b), zero(zero(X2))) → SUCCG_IN_GA(X1, X2)
ADDCI_IN_GGA(zero(X1), one(X2), zero(X3)) → U16_GGA(X1, X2, X3, addCI_in_gga(X1, X2, X3))
ADDCI_IN_GGA(zero(X1), one(X2), zero(X3)) → ADDCI_IN_GGA(X1, X2, X3)
ADDCI_IN_GGA(one(b), zero(zero(X1)), zero(one(X1))) → U17_GGA(X1, binaryZA_in_g(X1))
ADDCI_IN_GGA(one(b), zero(zero(X1)), zero(one(X1))) → BINARYZA_IN_G(X1)
ADDCI_IN_GGA(one(b), zero(one(X1)), zero(zero(X2))) → U18_GGA(X1, X2, succG_in_ga(X1, X2))
ADDCI_IN_GGA(one(b), zero(one(X1)), zero(zero(X2))) → SUCCG_IN_GA(X1, X2)
ADDCI_IN_GGA(one(X1), zero(X2), zero(X3)) → U19_GGA(X1, X2, X3, addCI_in_gga(X1, X2, X3))
ADDCI_IN_GGA(one(X1), zero(X2), zero(X3)) → ADDCI_IN_GGA(X1, X2, X3)
ADDCI_IN_GGA(one(X1), one(X2), one(X3)) → U20_GGA(X1, X2, X3, addcF_in_gga(X1, X2, X3))
ADDCI_IN_GGA(one(X1), one(X2), one(X3)) → ADDCF_IN_GGA(X1, X2, X3)
ADDJ_IN_GGA(zero(X1), one(X2), one(X3)) → U35_GGA(X1, X2, X3, addxD_in_gga(X1, X2, X3))
ADDJ_IN_GGA(zero(X1), one(X2), one(X3)) → ADDXD_IN_GGA(X1, X2, X3)
ADDJ_IN_GGA(one(X1), zero(X2), one(X3)) → U36_GGA(X1, X2, X3, addyE_in_gga(X1, X2, X3))
ADDJ_IN_GGA(one(X1), zero(X2), one(X3)) → ADDYE_IN_GGA(X1, X2, X3)
ADDJ_IN_GGA(one(X1), one(X2), zero(X3)) → U37_GGA(X1, X2, X3, addcF_in_gga(X1, X2, X3))
ADDJ_IN_GGA(one(X1), one(X2), zero(X3)) → ADDCF_IN_GGA(X1, X2, X3)
R is empty.
The argument filtering Pi contains the following mapping:
zero(
x1) =
zero(
x1)
b =
b
binaryZA_in_g(
x1) =
binaryZA_in_g(
x1)
one(
x1) =
one(
x1)
binaryB_in_g(
x1) =
binaryB_in_g(
x1)
addzC_in_gga(
x1,
x2,
x3) =
addzC_in_gga(
x1,
x2)
addxD_in_gga(
x1,
x2,
x3) =
addxD_in_gga(
x1,
x2)
addyE_in_gga(
x1,
x2,
x3) =
addyE_in_gga(
x1,
x2)
addcF_in_gga(
x1,
x2,
x3) =
addcF_in_gga(
x1,
x2)
succZH_in_ga(
x1,
x2) =
succZH_in_ga(
x1)
succG_in_ga(
x1,
x2) =
succG_in_ga(
x1)
addCI_in_gga(
x1,
x2,
x3) =
addCI_in_gga(
x1,
x2)
ADDJ_IN_GGA(
x1,
x2,
x3) =
ADDJ_IN_GGA(
x1,
x2)
U30_GGA(
x1,
x2) =
U30_GGA(
x1,
x2)
BINARYZA_IN_G(
x1) =
BINARYZA_IN_G(
x1)
U1_G(
x1,
x2) =
U1_G(
x1,
x2)
U2_G(
x1,
x2) =
U2_G(
x1,
x2)
BINARYB_IN_G(
x1) =
BINARYB_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)
ADDZC_IN_GGA(
x1,
x2,
x3) =
ADDZC_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)
ADDXD_IN_GGA(
x1,
x2,
x3) =
ADDXD_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)
ADDYE_IN_GGA(
x1,
x2,
x3) =
ADDYE_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)
ADDCF_IN_GGA(
x1,
x2,
x3) =
ADDCF_IN_GGA(
x1,
x2)
U21_GGA(
x1,
x2,
x3) =
U21_GGA(
x1,
x3)
SUCCZH_IN_GA(
x1,
x2) =
SUCCZH_IN_GA(
x1)
U11_GA(
x1,
x2) =
U11_GA(
x1,
x2)
U12_GA(
x1,
x2,
x3) =
U12_GA(
x1,
x3)
SUCCG_IN_GA(
x1,
x2) =
SUCCG_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)
ADDCI_IN_GGA(
x1,
x2,
x3) =
ADDCI_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:
ADDJ_IN_GGA(zero(X1), b, zero(X1)) → U30_GGA(X1, binaryZA_in_g(X1))
ADDJ_IN_GGA(zero(X1), b, zero(X1)) → BINARYZA_IN_G(X1)
BINARYZA_IN_G(zero(X1)) → U1_G(X1, binaryZA_in_g(X1))
BINARYZA_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYZA_IN_G(one(X1)) → U2_G(X1, binaryB_in_g(X1))
BINARYZA_IN_G(one(X1)) → BINARYB_IN_G(X1)
BINARYB_IN_G(zero(X1)) → U3_G(X1, binaryZA_in_g(X1))
BINARYB_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYB_IN_G(one(X1)) → U4_G(X1, binaryB_in_g(X1))
BINARYB_IN_G(one(X1)) → BINARYB_IN_G(X1)
ADDJ_IN_GGA(one(X1), b, one(X1)) → U31_GGA(X1, binaryB_in_g(X1))
ADDJ_IN_GGA(one(X1), b, one(X1)) → BINARYB_IN_G(X1)
ADDJ_IN_GGA(b, zero(X1), zero(X1)) → U32_GGA(X1, binaryZA_in_g(X1))
ADDJ_IN_GGA(b, zero(X1), zero(X1)) → BINARYZA_IN_G(X1)
ADDJ_IN_GGA(b, one(X1), one(X1)) → U33_GGA(X1, binaryB_in_g(X1))
ADDJ_IN_GGA(b, one(X1), one(X1)) → BINARYB_IN_G(X1)
ADDJ_IN_GGA(zero(X1), zero(X2), zero(X3)) → U34_GGA(X1, X2, X3, addzC_in_gga(X1, X2, X3))
ADDJ_IN_GGA(zero(X1), zero(X2), zero(X3)) → ADDZC_IN_GGA(X1, X2, X3)
ADDZC_IN_GGA(zero(X1), zero(X2), zero(X3)) → U5_GGA(X1, X2, X3, addzC_in_gga(X1, X2, X3))
ADDZC_IN_GGA(zero(X1), zero(X2), zero(X3)) → ADDZC_IN_GGA(X1, X2, X3)
ADDZC_IN_GGA(zero(X1), one(X2), one(X3)) → U6_GGA(X1, X2, X3, addxD_in_gga(X1, X2, X3))
ADDZC_IN_GGA(zero(X1), one(X2), one(X3)) → ADDXD_IN_GGA(X1, X2, X3)
ADDXD_IN_GGA(one(X1), b, one(X1)) → U24_GGA(X1, binaryB_in_g(X1))
ADDXD_IN_GGA(one(X1), b, one(X1)) → BINARYB_IN_G(X1)
ADDXD_IN_GGA(zero(X1), b, zero(X1)) → U25_GGA(X1, binaryZA_in_g(X1))
ADDXD_IN_GGA(zero(X1), b, zero(X1)) → BINARYZA_IN_G(X1)
ADDXD_IN_GGA(X1, X2, X3) → U26_GGA(X1, X2, X3, addzC_in_gga(X1, X2, X3))
ADDXD_IN_GGA(X1, X2, X3) → ADDZC_IN_GGA(X1, X2, X3)
ADDZC_IN_GGA(one(X1), zero(X2), one(X3)) → U7_GGA(X1, X2, X3, addyE_in_gga(X1, X2, X3))
ADDZC_IN_GGA(one(X1), zero(X2), one(X3)) → ADDYE_IN_GGA(X1, X2, X3)
ADDYE_IN_GGA(b, one(X1), one(X1)) → U27_GGA(X1, binaryB_in_g(X1))
ADDYE_IN_GGA(b, one(X1), one(X1)) → BINARYB_IN_G(X1)
ADDYE_IN_GGA(b, zero(X1), zero(X1)) → U28_GGA(X1, binaryZA_in_g(X1))
ADDYE_IN_GGA(b, zero(X1), zero(X1)) → BINARYZA_IN_G(X1)
ADDYE_IN_GGA(X1, X2, X3) → U29_GGA(X1, X2, X3, addzC_in_gga(X1, X2, X3))
ADDYE_IN_GGA(X1, X2, X3) → ADDZC_IN_GGA(X1, X2, X3)
ADDZC_IN_GGA(one(X1), one(X2), zero(X3)) → U8_GGA(X1, X2, X3, addcF_in_gga(X1, X2, X3))
ADDZC_IN_GGA(one(X1), one(X2), zero(X3)) → ADDCF_IN_GGA(X1, X2, X3)
ADDCF_IN_GGA(X1, b, X2) → U21_GGA(X1, X2, succZH_in_ga(X1, X2))
ADDCF_IN_GGA(X1, b, X2) → SUCCZH_IN_GA(X1, X2)
SUCCZH_IN_GA(zero(X1), one(X1)) → U11_GA(X1, binaryZA_in_g(X1))
SUCCZH_IN_GA(zero(X1), one(X1)) → BINARYZA_IN_G(X1)
SUCCZH_IN_GA(one(X1), zero(X2)) → U12_GA(X1, X2, succG_in_ga(X1, X2))
SUCCZH_IN_GA(one(X1), zero(X2)) → SUCCG_IN_GA(X1, X2)
SUCCG_IN_GA(zero(X1), one(X1)) → U9_GA(X1, binaryZA_in_g(X1))
SUCCG_IN_GA(zero(X1), one(X1)) → BINARYZA_IN_G(X1)
SUCCG_IN_GA(one(X1), zero(X2)) → U10_GA(X1, X2, succG_in_ga(X1, X2))
SUCCG_IN_GA(one(X1), zero(X2)) → SUCCG_IN_GA(X1, X2)
ADDCF_IN_GGA(b, X1, X2) → U22_GGA(X1, X2, succZH_in_ga(X1, X2))
ADDCF_IN_GGA(b, X1, X2) → SUCCZH_IN_GA(X1, X2)
ADDCF_IN_GGA(X1, X2, X3) → U23_GGA(X1, X2, X3, addCI_in_gga(X1, X2, X3))
ADDCF_IN_GGA(X1, X2, X3) → ADDCI_IN_GGA(X1, X2, X3)
ADDCI_IN_GGA(zero(X1), zero(X2), one(X3)) → U13_GGA(X1, X2, X3, addzC_in_gga(X1, X2, X3))
ADDCI_IN_GGA(zero(X1), zero(X2), one(X3)) → ADDZC_IN_GGA(X1, X2, X3)
ADDCI_IN_GGA(zero(zero(X1)), one(b), zero(one(X1))) → U14_GGA(X1, binaryZA_in_g(X1))
ADDCI_IN_GGA(zero(zero(X1)), one(b), zero(one(X1))) → BINARYZA_IN_G(X1)
ADDCI_IN_GGA(zero(one(X1)), one(b), zero(zero(X2))) → U15_GGA(X1, X2, succG_in_ga(X1, X2))
ADDCI_IN_GGA(zero(one(X1)), one(b), zero(zero(X2))) → SUCCG_IN_GA(X1, X2)
ADDCI_IN_GGA(zero(X1), one(X2), zero(X3)) → U16_GGA(X1, X2, X3, addCI_in_gga(X1, X2, X3))
ADDCI_IN_GGA(zero(X1), one(X2), zero(X3)) → ADDCI_IN_GGA(X1, X2, X3)
ADDCI_IN_GGA(one(b), zero(zero(X1)), zero(one(X1))) → U17_GGA(X1, binaryZA_in_g(X1))
ADDCI_IN_GGA(one(b), zero(zero(X1)), zero(one(X1))) → BINARYZA_IN_G(X1)
ADDCI_IN_GGA(one(b), zero(one(X1)), zero(zero(X2))) → U18_GGA(X1, X2, succG_in_ga(X1, X2))
ADDCI_IN_GGA(one(b), zero(one(X1)), zero(zero(X2))) → SUCCG_IN_GA(X1, X2)
ADDCI_IN_GGA(one(X1), zero(X2), zero(X3)) → U19_GGA(X1, X2, X3, addCI_in_gga(X1, X2, X3))
ADDCI_IN_GGA(one(X1), zero(X2), zero(X3)) → ADDCI_IN_GGA(X1, X2, X3)
ADDCI_IN_GGA(one(X1), one(X2), one(X3)) → U20_GGA(X1, X2, X3, addcF_in_gga(X1, X2, X3))
ADDCI_IN_GGA(one(X1), one(X2), one(X3)) → ADDCF_IN_GGA(X1, X2, X3)
ADDJ_IN_GGA(zero(X1), one(X2), one(X3)) → U35_GGA(X1, X2, X3, addxD_in_gga(X1, X2, X3))
ADDJ_IN_GGA(zero(X1), one(X2), one(X3)) → ADDXD_IN_GGA(X1, X2, X3)
ADDJ_IN_GGA(one(X1), zero(X2), one(X3)) → U36_GGA(X1, X2, X3, addyE_in_gga(X1, X2, X3))
ADDJ_IN_GGA(one(X1), zero(X2), one(X3)) → ADDYE_IN_GGA(X1, X2, X3)
ADDJ_IN_GGA(one(X1), one(X2), zero(X3)) → U37_GGA(X1, X2, X3, addcF_in_gga(X1, X2, X3))
ADDJ_IN_GGA(one(X1), one(X2), zero(X3)) → ADDCF_IN_GGA(X1, X2, X3)
R is empty.
The argument filtering Pi contains the following mapping:
zero(
x1) =
zero(
x1)
b =
b
binaryZA_in_g(
x1) =
binaryZA_in_g(
x1)
one(
x1) =
one(
x1)
binaryB_in_g(
x1) =
binaryB_in_g(
x1)
addzC_in_gga(
x1,
x2,
x3) =
addzC_in_gga(
x1,
x2)
addxD_in_gga(
x1,
x2,
x3) =
addxD_in_gga(
x1,
x2)
addyE_in_gga(
x1,
x2,
x3) =
addyE_in_gga(
x1,
x2)
addcF_in_gga(
x1,
x2,
x3) =
addcF_in_gga(
x1,
x2)
succZH_in_ga(
x1,
x2) =
succZH_in_ga(
x1)
succG_in_ga(
x1,
x2) =
succG_in_ga(
x1)
addCI_in_gga(
x1,
x2,
x3) =
addCI_in_gga(
x1,
x2)
ADDJ_IN_GGA(
x1,
x2,
x3) =
ADDJ_IN_GGA(
x1,
x2)
U30_GGA(
x1,
x2) =
U30_GGA(
x1,
x2)
BINARYZA_IN_G(
x1) =
BINARYZA_IN_G(
x1)
U1_G(
x1,
x2) =
U1_G(
x1,
x2)
U2_G(
x1,
x2) =
U2_G(
x1,
x2)
BINARYB_IN_G(
x1) =
BINARYB_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)
ADDZC_IN_GGA(
x1,
x2,
x3) =
ADDZC_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)
ADDXD_IN_GGA(
x1,
x2,
x3) =
ADDXD_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)
ADDYE_IN_GGA(
x1,
x2,
x3) =
ADDYE_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)
ADDCF_IN_GGA(
x1,
x2,
x3) =
ADDCF_IN_GGA(
x1,
x2)
U21_GGA(
x1,
x2,
x3) =
U21_GGA(
x1,
x3)
SUCCZH_IN_GA(
x1,
x2) =
SUCCZH_IN_GA(
x1)
U11_GA(
x1,
x2) =
U11_GA(
x1,
x2)
U12_GA(
x1,
x2,
x3) =
U12_GA(
x1,
x3)
SUCCG_IN_GA(
x1,
x2) =
SUCCG_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)
ADDCI_IN_GGA(
x1,
x2,
x3) =
ADDCI_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:
BINARYZA_IN_G(one(X1)) → BINARYB_IN_G(X1)
BINARYB_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYZA_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYB_IN_G(one(X1)) → BINARYB_IN_G(X1)
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:
BINARYZA_IN_G(one(X1)) → BINARYB_IN_G(X1)
BINARYB_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYZA_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYB_IN_G(one(X1)) → BINARYB_IN_G(X1)
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:
- BINARYB_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
The graph contains the following edges 1 > 1
- BINARYB_IN_G(one(X1)) → BINARYB_IN_G(X1)
The graph contains the following edges 1 > 1
- BINARYZA_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
The graph contains the following edges 1 > 1
- BINARYZA_IN_G(one(X1)) → BINARYB_IN_G(X1)
The graph contains the following edges 1 > 1
(13) YES
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
SUCCG_IN_GA(one(X1), zero(X2)) → SUCCG_IN_GA(X1, X2)
R is empty.
The argument filtering Pi contains the following mapping:
zero(
x1) =
zero(
x1)
one(
x1) =
one(
x1)
SUCCG_IN_GA(
x1,
x2) =
SUCCG_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:
SUCCG_IN_GA(one(X1)) → SUCCG_IN_GA(X1)
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:
- SUCCG_IN_GA(one(X1)) → SUCCG_IN_GA(X1)
The graph contains the following edges 1 > 1
(18) YES
(19) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
ADDXD_IN_GGA(X1, X2, X3) → ADDZC_IN_GGA(X1, X2, X3)
ADDZC_IN_GGA(zero(X1), zero(X2), zero(X3)) → ADDZC_IN_GGA(X1, X2, X3)
ADDZC_IN_GGA(zero(X1), one(X2), one(X3)) → ADDXD_IN_GGA(X1, X2, X3)
ADDZC_IN_GGA(one(X1), zero(X2), one(X3)) → ADDYE_IN_GGA(X1, X2, X3)
ADDYE_IN_GGA(X1, X2, X3) → ADDZC_IN_GGA(X1, X2, X3)
ADDZC_IN_GGA(one(X1), one(X2), zero(X3)) → ADDCF_IN_GGA(X1, X2, X3)
ADDCF_IN_GGA(X1, X2, X3) → ADDCI_IN_GGA(X1, X2, X3)
ADDCI_IN_GGA(zero(X1), zero(X2), one(X3)) → ADDZC_IN_GGA(X1, X2, X3)
ADDCI_IN_GGA(zero(X1), one(X2), zero(X3)) → ADDCI_IN_GGA(X1, X2, X3)
ADDCI_IN_GGA(one(X1), zero(X2), zero(X3)) → ADDCI_IN_GGA(X1, X2, X3)
ADDCI_IN_GGA(one(X1), one(X2), one(X3)) → ADDCF_IN_GGA(X1, X2, X3)
R is empty.
The argument filtering Pi contains the following mapping:
zero(
x1) =
zero(
x1)
one(
x1) =
one(
x1)
ADDZC_IN_GGA(
x1,
x2,
x3) =
ADDZC_IN_GGA(
x1,
x2)
ADDXD_IN_GGA(
x1,
x2,
x3) =
ADDXD_IN_GGA(
x1,
x2)
ADDYE_IN_GGA(
x1,
x2,
x3) =
ADDYE_IN_GGA(
x1,
x2)
ADDCF_IN_GGA(
x1,
x2,
x3) =
ADDCF_IN_GGA(
x1,
x2)
ADDCI_IN_GGA(
x1,
x2,
x3) =
ADDCI_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:
ADDXD_IN_GGA(X1, X2) → ADDZC_IN_GGA(X1, X2)
ADDZC_IN_GGA(zero(X1), zero(X2)) → ADDZC_IN_GGA(X1, X2)
ADDZC_IN_GGA(zero(X1), one(X2)) → ADDXD_IN_GGA(X1, X2)
ADDZC_IN_GGA(one(X1), zero(X2)) → ADDYE_IN_GGA(X1, X2)
ADDYE_IN_GGA(X1, X2) → ADDZC_IN_GGA(X1, X2)
ADDZC_IN_GGA(one(X1), one(X2)) → ADDCF_IN_GGA(X1, X2)
ADDCF_IN_GGA(X1, X2) → ADDCI_IN_GGA(X1, X2)
ADDCI_IN_GGA(zero(X1), zero(X2)) → ADDZC_IN_GGA(X1, X2)
ADDCI_IN_GGA(zero(X1), one(X2)) → ADDCI_IN_GGA(X1, X2)
ADDCI_IN_GGA(one(X1), zero(X2)) → ADDCI_IN_GGA(X1, X2)
ADDCI_IN_GGA(one(X1), one(X2)) → ADDCF_IN_GGA(X1, X2)
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:
- ADDZC_IN_GGA(zero(X1), one(X2)) → ADDXD_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
- ADDZC_IN_GGA(zero(X1), zero(X2)) → ADDZC_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
- ADDXD_IN_GGA(X1, X2) → ADDZC_IN_GGA(X1, X2)
The graph contains the following edges 1 >= 1, 2 >= 2
- ADDYE_IN_GGA(X1, X2) → ADDZC_IN_GGA(X1, X2)
The graph contains the following edges 1 >= 1, 2 >= 2
- ADDCI_IN_GGA(zero(X1), zero(X2)) → ADDZC_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
- ADDZC_IN_GGA(one(X1), zero(X2)) → ADDYE_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
- ADDZC_IN_GGA(one(X1), one(X2)) → ADDCF_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
- ADDCF_IN_GGA(X1, X2) → ADDCI_IN_GGA(X1, X2)
The graph contains the following edges 1 >= 1, 2 >= 2
- ADDCI_IN_GGA(one(X1), one(X2)) → ADDCF_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
- ADDCI_IN_GGA(zero(X1), one(X2)) → ADDCI_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
- ADDCI_IN_GGA(one(X1), zero(X2)) → ADDCI_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
(23) YES