0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 QDP
↳22 UsableRulesProof (⇔)
↳23 QDP
↳24 QReductionProof (⇔)
↳25 QDP
↳26 Instantiation (⇔)
↳27 QDP
↳28 NonInfProof (⇔)
↳29 QDP
↳30 DependencyGraphProof (⇔)
↳31 TRUE
diff(x, y) → cond1(equal(x, y), x, y)
cond1(true, x, y) → 0
cond1(false, x, y) → cond2(gt(x, y), x, y)
cond2(true, x, y) → s(diff(x, s(y)))
cond2(false, x, y) → s(diff(s(x), y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
diff(x, y) → cond1(equal(x, y), x, y)
cond1(true, x, y) → 0
cond1(false, x, y) → cond2(gt(x, y), x, y)
cond2(true, x, y) → s(diff(x, s(y)))
cond2(false, x, y) → s(diff(s(x), y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
diff(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
DIFF(x, y) → COND1(equal(x, y), x, y)
DIFF(x, y) → EQUAL(x, y)
COND1(false, x, y) → COND2(gt(x, y), x, y)
COND1(false, x, y) → GT(x, y)
COND2(true, x, y) → DIFF(x, s(y))
COND2(false, x, y) → DIFF(s(x), y)
GT(s(u), s(v)) → GT(u, v)
EQUAL(s(x), s(y)) → EQUAL(x, y)
diff(x, y) → cond1(equal(x, y), x, y)
cond1(true, x, y) → 0
cond1(false, x, y) → cond2(gt(x, y), x, y)
cond2(true, x, y) → s(diff(x, s(y)))
cond2(false, x, y) → s(diff(s(x), y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
diff(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
EQUAL(s(x), s(y)) → EQUAL(x, y)
diff(x, y) → cond1(equal(x, y), x, y)
cond1(true, x, y) → 0
cond1(false, x, y) → cond2(gt(x, y), x, y)
cond2(true, x, y) → s(diff(x, s(y)))
cond2(false, x, y) → s(diff(s(x), y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
diff(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
EQUAL(s(x), s(y)) → EQUAL(x, y)
diff(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
diff(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
EQUAL(s(x), s(y)) → EQUAL(x, y)
From the DPs we obtained the following set of size-change graphs:
GT(s(u), s(v)) → GT(u, v)
diff(x, y) → cond1(equal(x, y), x, y)
cond1(true, x, y) → 0
cond1(false, x, y) → cond2(gt(x, y), x, y)
cond2(true, x, y) → s(diff(x, s(y)))
cond2(false, x, y) → s(diff(s(x), y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
diff(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
GT(s(u), s(v)) → GT(u, v)
diff(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
diff(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
GT(s(u), s(v)) → GT(u, v)
From the DPs we obtained the following set of size-change graphs:
COND1(false, x, y) → COND2(gt(x, y), x, y)
COND2(true, x, y) → DIFF(x, s(y))
DIFF(x, y) → COND1(equal(x, y), x, y)
COND2(false, x, y) → DIFF(s(x), y)
diff(x, y) → cond1(equal(x, y), x, y)
cond1(true, x, y) → 0
cond1(false, x, y) → cond2(gt(x, y), x, y)
cond2(true, x, y) → s(diff(x, s(y)))
cond2(false, x, y) → s(diff(s(x), y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
diff(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
COND1(false, x, y) → COND2(gt(x, y), x, y)
COND2(true, x, y) → DIFF(x, s(y))
DIFF(x, y) → COND1(equal(x, y), x, y)
COND2(false, x, y) → DIFF(s(x), y)
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
diff(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
diff(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
COND1(false, x, y) → COND2(gt(x, y), x, y)
COND2(true, x, y) → DIFF(x, s(y))
DIFF(x, y) → COND1(equal(x, y), x, y)
COND2(false, x, y) → DIFF(s(x), y)
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
DIFF(z0, s(z1)) → COND1(equal(z0, s(z1)), z0, s(z1))
DIFF(s(z0), z1) → COND1(equal(s(z0), z1), s(z0), z1)
COND1(false, x, y) → COND2(gt(x, y), x, y)
COND2(true, x, y) → DIFF(x, s(y))
COND2(false, x, y) → DIFF(s(x), y)
DIFF(z0, s(z1)) → COND1(equal(z0, s(z1)), z0, s(z1))
DIFF(s(z0), z1) → COND1(equal(s(z0), z1), s(z0), z1)
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
(1) (DIFF(x22, s(x23))=DIFF(x24, x25)∧COND1(equal(x24, x25), x24, x25)=COND1(false, x26, x27) ⇒ COND1(false, x26, x27)≥COND2(gt(x26, x27), x26, x27))
(2) (s(x23)=x25∧equal(x24, x25)=false ⇒ COND1(false, x24, x25)≥COND2(gt(x24, x25), x24, x25))
(3) (false=false∧s(x23)=0 ⇒ COND1(false, s(x180), 0)≥COND2(gt(s(x180), 0), s(x180), 0))
(4) (false=false∧s(x23)=s(x181) ⇒ COND1(false, 0, s(x181))≥COND2(gt(0, s(x181)), 0, s(x181)))
(5) (equal(x183, x182)=false∧s(x23)=s(x182)∧(∀x184:equal(x183, x182)=false∧s(x184)=x182 ⇒ COND1(false, x183, x182)≥COND2(gt(x183, x182), x183, x182)) ⇒ COND1(false, s(x183), s(x182))≥COND2(gt(s(x183), s(x182)), s(x183), s(x182)))
(6) (COND1(false, 0, s(x23))≥COND2(gt(0, s(x23)), 0, s(x23)))
(7) (equal(x183, x182)=false ⇒ COND1(false, s(x183), s(x182))≥COND2(gt(s(x183), s(x182)), s(x183), s(x182)))
(8) (false=false ⇒ COND1(false, s(s(x185)), s(0))≥COND2(gt(s(s(x185)), s(0)), s(s(x185)), s(0)))
(9) (false=false ⇒ COND1(false, s(0), s(s(x186)))≥COND2(gt(s(0), s(s(x186))), s(0), s(s(x186))))
(10) (equal(x188, x187)=false∧(equal(x188, x187)=false ⇒ COND1(false, s(x188), s(x187))≥COND2(gt(s(x188), s(x187)), s(x188), s(x187))) ⇒ COND1(false, s(s(x188)), s(s(x187)))≥COND2(gt(s(s(x188)), s(s(x187))), s(s(x188)), s(s(x187))))
(11) (COND1(false, s(s(x185)), s(0))≥COND2(gt(s(s(x185)), s(0)), s(s(x185)), s(0)))
(12) (COND1(false, s(0), s(s(x186)))≥COND2(gt(s(0), s(s(x186))), s(0), s(s(x186))))
(13) (COND1(false, s(x188), s(x187))≥COND2(gt(s(x188), s(x187)), s(x188), s(x187)) ⇒ COND1(false, s(s(x188)), s(s(x187)))≥COND2(gt(s(s(x188)), s(s(x187))), s(s(x188)), s(s(x187))))
(14) (DIFF(s(x30), x31)=DIFF(x32, x33)∧COND1(equal(x32, x33), x32, x33)=COND1(false, x34, x35) ⇒ COND1(false, x34, x35)≥COND2(gt(x34, x35), x34, x35))
(15) (s(x30)=x32∧equal(x32, x33)=false ⇒ COND1(false, x32, x33)≥COND2(gt(x32, x33), x32, x33))
(16) (false=false∧s(x30)=s(x189) ⇒ COND1(false, s(x189), 0)≥COND2(gt(s(x189), 0), s(x189), 0))
(17) (false=false∧s(x30)=0 ⇒ COND1(false, 0, s(x190))≥COND2(gt(0, s(x190)), 0, s(x190)))
(18) (equal(x192, x191)=false∧s(x30)=s(x192)∧(∀x193:equal(x192, x191)=false∧s(x193)=x192 ⇒ COND1(false, x192, x191)≥COND2(gt(x192, x191), x192, x191)) ⇒ COND1(false, s(x192), s(x191))≥COND2(gt(s(x192), s(x191)), s(x192), s(x191)))
(19) (COND1(false, s(x30), 0)≥COND2(gt(s(x30), 0), s(x30), 0))
(20) (equal(x192, x191)=false ⇒ COND1(false, s(x192), s(x191))≥COND2(gt(s(x192), s(x191)), s(x192), s(x191)))
(21) (false=false ⇒ COND1(false, s(s(x194)), s(0))≥COND2(gt(s(s(x194)), s(0)), s(s(x194)), s(0)))
(22) (false=false ⇒ COND1(false, s(0), s(s(x195)))≥COND2(gt(s(0), s(s(x195))), s(0), s(s(x195))))
(23) (equal(x197, x196)=false∧(equal(x197, x196)=false ⇒ COND1(false, s(x197), s(x196))≥COND2(gt(s(x197), s(x196)), s(x197), s(x196))) ⇒ COND1(false, s(s(x197)), s(s(x196)))≥COND2(gt(s(s(x197)), s(s(x196))), s(s(x197)), s(s(x196))))
(24) (COND1(false, s(s(x194)), s(0))≥COND2(gt(s(s(x194)), s(0)), s(s(x194)), s(0)))
(25) (COND1(false, s(0), s(s(x195)))≥COND2(gt(s(0), s(s(x195))), s(0), s(s(x195))))
(26) (COND1(false, s(x197), s(x196))≥COND2(gt(s(x197), s(x196)), s(x197), s(x196)) ⇒ COND1(false, s(s(x197)), s(s(x196)))≥COND2(gt(s(s(x197)), s(s(x196))), s(s(x197)), s(s(x196))))
(27) (COND1(equal(x50, x51), x50, x51)=COND1(false, x52, x53)∧COND2(gt(x52, x53), x52, x53)=COND2(true, x54, x55) ⇒ COND2(true, x54, x55)≥DIFF(x54, s(x55)))
(28) (equal(x50, x51)=false∧x50=x52∧x51=x53∧gt(x52, x53)=true ⇒ COND2(true, x52, x53)≥DIFF(x52, s(x53)))
(29) (false=false∧s(x198)=x52∧0=x53∧gt(x52, x53)=true ⇒ COND2(true, x52, x53)≥DIFF(x52, s(x53)))
(30) (false=false∧0=x52∧s(x199)=x53∧gt(x52, x53)=true ⇒ COND2(true, x52, x53)≥DIFF(x52, s(x53)))
(31) (equal(x201, x200)=false∧s(x201)=x52∧s(x200)=x53∧gt(x52, x53)=true∧(∀x202,x203:equal(x201, x200)=false∧x201=x202∧x200=x203∧gt(x202, x203)=true ⇒ COND2(true, x202, x203)≥DIFF(x202, s(x203))) ⇒ COND2(true, x52, x53)≥DIFF(x52, s(x53)))
(32) (s(x198)=x52∧0=x53∧gt(x52, x53)=true ⇒ COND2(true, x52, x53)≥DIFF(x52, s(x53)))
(33) (0=x52∧s(x199)=x53∧gt(x52, x53)=true ⇒ COND2(true, x52, x53)≥DIFF(x52, s(x53)))
(34) (true=true∧equal(x201, x200)=false∧s(x201)=s(x215)∧s(x200)=0∧(∀x202,x203:equal(x201, x200)=false∧x201=x202∧x200=x203∧gt(x202, x203)=true ⇒ COND2(true, x202, x203)≥DIFF(x202, s(x203))) ⇒ COND2(true, s(x215), 0)≥DIFF(s(x215), s(0)))
(35) (gt(x217, x216)=true∧equal(x201, x200)=false∧s(x201)=s(x217)∧s(x200)=s(x216)∧(∀x202,x203:equal(x201, x200)=false∧x201=x202∧x200=x203∧gt(x202, x203)=true ⇒ COND2(true, x202, x203)≥DIFF(x202, s(x203)))∧(∀x218,x219,x220,x221:gt(x217, x216)=true∧equal(x218, x219)=false∧s(x218)=x217∧s(x219)=x216∧(∀x220,x221:equal(x218, x219)=false∧x218=x220∧x219=x221∧gt(x220, x221)=true ⇒ COND2(true, x220, x221)≥DIFF(x220, s(x221))) ⇒ COND2(true, x217, x216)≥DIFF(x217, s(x216))) ⇒ COND2(true, s(x217), s(x216))≥DIFF(s(x217), s(s(x216))))
(36) (true=true∧s(x198)=s(x205)∧0=0 ⇒ COND2(true, s(x205), 0)≥DIFF(s(x205), s(0)))
(37) (gt(x207, x206)=true∧s(x198)=s(x207)∧0=s(x206)∧(∀x208:gt(x207, x206)=true∧s(x208)=x207∧0=x206 ⇒ COND2(true, x207, x206)≥DIFF(x207, s(x206))) ⇒ COND2(true, s(x207), s(x206))≥DIFF(s(x207), s(s(x206))))
(38) (COND2(true, s(x198), 0)≥DIFF(s(x198), s(0)))
(39) (true=true∧0=s(x210)∧s(x199)=0 ⇒ COND2(true, s(x210), 0)≥DIFF(s(x210), s(0)))
(40) (gt(x212, x211)=true∧0=s(x212)∧s(x199)=s(x211)∧(∀x213:gt(x212, x211)=true∧0=x212∧s(x213)=x211 ⇒ COND2(true, x212, x211)≥DIFF(x212, s(x211))) ⇒ COND2(true, s(x212), s(x211))≥DIFF(s(x212), s(s(x211))))
(41) (gt(x217, x216)=true∧equal(x201, x200)=false∧x201=x217∧x200=x216∧(∀x202,x203:equal(x201, x200)=false∧x201=x202∧x200=x203∧gt(x202, x203)=true ⇒ COND2(true, x202, x203)≥DIFF(x202, s(x203)))∧(∀x218,x219,x220,x221:gt(x217, x216)=true∧equal(x218, x219)=false∧s(x218)=x217∧s(x219)=x216∧(∀x220,x221:equal(x218, x219)=false∧x218=x220∧x219=x221∧gt(x220, x221)=true ⇒ COND2(true, x220, x221)≥DIFF(x220, s(x221))) ⇒ COND2(true, x217, x216)≥DIFF(x217, s(x216))) ⇒ COND2(true, s(x217), s(x216))≥DIFF(s(x217), s(s(x216))))
(42) (COND2(true, x217, x216)≥DIFF(x217, s(x216))∧(∀x218,x219,x220,x221:gt(x217, x216)=true∧equal(x218, x219)=false∧s(x218)=x217∧s(x219)=x216∧(∀x220,x221:equal(x218, x219)=false∧x218=x220∧x219=x221∧gt(x220, x221)=true ⇒ COND2(true, x220, x221)≥DIFF(x220, s(x221))) ⇒ COND2(true, x217, x216)≥DIFF(x217, s(x216))) ⇒ COND2(true, s(x217), s(x216))≥DIFF(s(x217), s(s(x216))))
(43) (COND2(true, x217, x216)≥DIFF(x217, s(x216)) ⇒ COND2(true, s(x217), s(x216))≥DIFF(s(x217), s(s(x216))))
(44) (COND2(gt(x100, x101), x100, x101)=COND2(true, x102, x103)∧DIFF(x102, s(x103))=DIFF(x104, x105) ⇒ DIFF(x104, x105)≥COND1(equal(x104, x105), x104, x105))
(45) (gt(x100, x101)=true ⇒ DIFF(x100, s(x101))≥COND1(equal(x100, s(x101)), x100, s(x101)))
(46) (true=true ⇒ DIFF(s(x223), s(0))≥COND1(equal(s(x223), s(0)), s(x223), s(0)))
(47) (gt(x225, x224)=true∧(gt(x225, x224)=true ⇒ DIFF(x225, s(x224))≥COND1(equal(x225, s(x224)), x225, s(x224))) ⇒ DIFF(s(x225), s(s(x224)))≥COND1(equal(s(x225), s(s(x224))), s(x225), s(s(x224))))
(48) (DIFF(s(x223), s(0))≥COND1(equal(s(x223), s(0)), s(x223), s(0)))
(49) (DIFF(x225, s(x224))≥COND1(equal(x225, s(x224)), x225, s(x224)) ⇒ DIFF(s(x225), s(s(x224)))≥COND1(equal(s(x225), s(s(x224))), s(x225), s(s(x224))))
(50) (COND2(gt(x124, x125), x124, x125)=COND2(false, x126, x127)∧DIFF(s(x126), x127)=DIFF(x128, x129) ⇒ DIFF(x128, x129)≥COND1(equal(x128, x129), x128, x129))
(51) (gt(x124, x125)=false ⇒ DIFF(s(x124), x125)≥COND1(equal(s(x124), x125), s(x124), x125))
(52) (false=false ⇒ DIFF(s(0), x226)≥COND1(equal(s(0), x226), s(0), x226))
(53) (gt(x229, x228)=false∧(gt(x229, x228)=false ⇒ DIFF(s(x229), x228)≥COND1(equal(s(x229), x228), s(x229), x228)) ⇒ DIFF(s(s(x229)), s(x228))≥COND1(equal(s(s(x229)), s(x228)), s(s(x229)), s(x228)))
(54) (DIFF(s(0), x226)≥COND1(equal(s(0), x226), s(0), x226))
(55) (DIFF(s(x229), x228)≥COND1(equal(s(x229), x228), s(x229), x228) ⇒ DIFF(s(s(x229)), s(x228))≥COND1(equal(s(s(x229)), s(x228)), s(s(x229)), s(x228)))
(56) (COND1(equal(x140, x141), x140, x141)=COND1(false, x142, x143)∧COND2(gt(x142, x143), x142, x143)=COND2(false, x144, x145) ⇒ COND2(false, x144, x145)≥DIFF(s(x144), x145))
(57) (equal(x140, x141)=false∧x140=x142∧x141=x143∧gt(x142, x143)=false ⇒ COND2(false, x142, x143)≥DIFF(s(x142), x143))
(58) (false=false∧s(x230)=x142∧0=x143∧gt(x142, x143)=false ⇒ COND2(false, x142, x143)≥DIFF(s(x142), x143))
(59) (false=false∧0=x142∧s(x231)=x143∧gt(x142, x143)=false ⇒ COND2(false, x142, x143)≥DIFF(s(x142), x143))
(60) (equal(x233, x232)=false∧s(x233)=x142∧s(x232)=x143∧gt(x142, x143)=false∧(∀x234,x235:equal(x233, x232)=false∧x233=x234∧x232=x235∧gt(x234, x235)=false ⇒ COND2(false, x234, x235)≥DIFF(s(x234), x235)) ⇒ COND2(false, x142, x143)≥DIFF(s(x142), x143))
(61) (s(x230)=x142∧0=x143∧gt(x142, x143)=false ⇒ COND2(false, x142, x143)≥DIFF(s(x142), x143))
(62) (0=x142∧s(x231)=x143∧gt(x142, x143)=false ⇒ COND2(false, x142, x143)≥DIFF(s(x142), x143))
(63) (false=false∧equal(x233, x232)=false∧s(x233)=0∧s(x232)=x246∧(∀x234,x235:equal(x233, x232)=false∧x233=x234∧x232=x235∧gt(x234, x235)=false ⇒ COND2(false, x234, x235)≥DIFF(s(x234), x235)) ⇒ COND2(false, 0, x246)≥DIFF(s(0), x246))
(64) (gt(x249, x248)=false∧equal(x233, x232)=false∧s(x233)=s(x249)∧s(x232)=s(x248)∧(∀x234,x235:equal(x233, x232)=false∧x233=x234∧x232=x235∧gt(x234, x235)=false ⇒ COND2(false, x234, x235)≥DIFF(s(x234), x235))∧(∀x250,x251,x252,x253:gt(x249, x248)=false∧equal(x250, x251)=false∧s(x250)=x249∧s(x251)=x248∧(∀x252,x253:equal(x250, x251)=false∧x250=x252∧x251=x253∧gt(x252, x253)=false ⇒ COND2(false, x252, x253)≥DIFF(s(x252), x253)) ⇒ COND2(false, x249, x248)≥DIFF(s(x249), x248)) ⇒ COND2(false, s(x249), s(x248))≥DIFF(s(s(x249)), s(x248)))
(65) (false=false∧s(x230)=0∧0=x236 ⇒ COND2(false, 0, x236)≥DIFF(s(0), x236))
(66) (gt(x239, x238)=false∧s(x230)=s(x239)∧0=s(x238)∧(∀x240:gt(x239, x238)=false∧s(x240)=x239∧0=x238 ⇒ COND2(false, x239, x238)≥DIFF(s(x239), x238)) ⇒ COND2(false, s(x239), s(x238))≥DIFF(s(s(x239)), s(x238)))
(67) (false=false∧0=0∧s(x231)=x241 ⇒ COND2(false, 0, x241)≥DIFF(s(0), x241))
(68) (gt(x244, x243)=false∧0=s(x244)∧s(x231)=s(x243)∧(∀x245:gt(x244, x243)=false∧0=x244∧s(x245)=x243 ⇒ COND2(false, x244, x243)≥DIFF(s(x244), x243)) ⇒ COND2(false, s(x244), s(x243))≥DIFF(s(s(x244)), s(x243)))
(69) (COND2(false, 0, s(x231))≥DIFF(s(0), s(x231)))
(70) (gt(x249, x248)=false∧equal(x233, x232)=false∧x233=x249∧x232=x248∧(∀x234,x235:equal(x233, x232)=false∧x233=x234∧x232=x235∧gt(x234, x235)=false ⇒ COND2(false, x234, x235)≥DIFF(s(x234), x235))∧(∀x250,x251,x252,x253:gt(x249, x248)=false∧equal(x250, x251)=false∧s(x250)=x249∧s(x251)=x248∧(∀x252,x253:equal(x250, x251)=false∧x250=x252∧x251=x253∧gt(x252, x253)=false ⇒ COND2(false, x252, x253)≥DIFF(s(x252), x253)) ⇒ COND2(false, x249, x248)≥DIFF(s(x249), x248)) ⇒ COND2(false, s(x249), s(x248))≥DIFF(s(s(x249)), s(x248)))
(71) (COND2(false, x249, x248)≥DIFF(s(x249), x248)∧(∀x250,x251,x252,x253:gt(x249, x248)=false∧equal(x250, x251)=false∧s(x250)=x249∧s(x251)=x248∧(∀x252,x253:equal(x250, x251)=false∧x250=x252∧x251=x253∧gt(x252, x253)=false ⇒ COND2(false, x252, x253)≥DIFF(s(x252), x253)) ⇒ COND2(false, x249, x248)≥DIFF(s(x249), x248)) ⇒ COND2(false, s(x249), s(x248))≥DIFF(s(s(x249)), s(x248)))
(72) (COND2(false, x249, x248)≥DIFF(s(x249), x248) ⇒ COND2(false, s(x249), s(x248))≥DIFF(s(s(x249)), s(x248)))
POL(0) = 0
POL(COND1(x1, x2, x3)) = -1 + 2·x1·x2 - 2·x1·x3 + x12 - 2·x2·x3 + x22 + x32
POL(COND2(x1, x2, x3)) = -1 + 2·x1·x2 - 2·x1·x3 + x12 - 2·x2·x3 + x22 + x32
POL(DIFF(x1, x2)) = -1 - 2·x1·x2 + x12 + x22
POL(c) = -1
POL(equal(x1, x2)) = 0
POL(false) = 0
POL(gt(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in Pbound:
COND2(true, x, y) → DIFF(x, s(y))
COND2(false, x, y) → DIFF(s(x), y)
The following rules are usable:
COND1(false, x, y) → COND2(gt(x, y), x, y)
COND2(true, x, y) → DIFF(x, s(y))
DIFF(x, y) → COND1(equal(x, y), x, y)
COND2(false, x, y) → DIFF(s(x), y)
equal(0, 0) ↔ true
equal(s(x), 0) ↔ false
equal(0, s(y)) ↔ false
gt(0, v) ↔ false
equal(s(x), s(y)) ↔ equal(x, y)
gt(s(u), s(v)) ↔ gt(u, v)
gt(s(u), 0) ↔ true
COND1(false, x, y) → COND2(gt(x, y), x, y)
DIFF(x, y) → COND1(equal(x, y), x, y)
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))