0 QTRS
↳1 AAECC Innermost (⇔)
↳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 NonInfProof (⇔)
↳20 QDP
↳21 DependencyGraphProof (⇔)
↳22 AND
↳23 QDP
↳24 UsableRulesProof (⇔)
↳25 QDP
↳26 QReductionProof (⇔)
↳27 QDP
↳28 QDPOrderProof (⇔)
↳29 QDP
↳30 PisEmptyProof (⇔)
↳31 TRUE
↳32 QDP
↳33 UsableRulesProof (⇔)
↳34 QDP
↳35 QReductionProof (⇔)
↳36 QDP
↳37 QDPOrderProof (⇔)
↳38 QDP
↳39 PisEmptyProof (⇔)
↳40 TRUE
cond1(true, x, y) → cond2(gr(x, y), x, y)
cond2(true, x, y) → cond3(gr(x, 0), x, y)
cond2(false, x, y) → cond4(gr(y, 0), x, y)
cond3(true, x, y) → cond3(gr(x, 0), p(x), y)
cond3(false, x, y) → cond1(and(gr(x, 0), gr(y, 0)), x, y)
cond4(true, x, y) → cond4(gr(y, 0), x, p(y))
cond4(false, x, y) → cond1(and(gr(x, 0), gr(y, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
p(0) → 0
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
p(0) → 0
p(s(x)) → x
cond1(true, x, y) → cond2(gr(x, y), x, y)
cond2(true, x, y) → cond3(gr(x, 0), x, y)
cond2(false, x, y) → cond4(gr(y, 0), x, y)
cond3(true, x, y) → cond3(gr(x, 0), p(x), y)
cond3(false, x, y) → cond1(and(gr(x, 0), gr(y, 0)), x, y)
cond4(true, x, y) → cond4(gr(y, 0), x, p(y))
cond4(false, x, y) → cond1(and(gr(x, 0), gr(y, 0)), x, y)
cond1(true, x, y) → cond2(gr(x, y), x, y)
cond2(true, x, y) → cond3(gr(x, 0), x, y)
cond2(false, x, y) → cond4(gr(y, 0), x, y)
cond3(true, x, y) → cond3(gr(x, 0), p(x), y)
cond3(false, x, y) → cond1(and(gr(x, 0), gr(y, 0)), x, y)
cond4(true, x, y) → cond4(gr(y, 0), x, p(y))
cond4(false, x, y) → cond1(and(gr(x, 0), gr(y, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
cond3(true, x0, x1)
cond3(false, x0, x1)
cond4(true, x0, x1)
cond4(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
p(0)
p(s(x0))
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND1(true, x, y) → GR(x, y)
COND2(true, x, y) → COND3(gr(x, 0), x, y)
COND2(true, x, y) → GR(x, 0)
COND2(false, x, y) → COND4(gr(y, 0), x, y)
COND2(false, x, y) → GR(y, 0)
COND3(true, x, y) → COND3(gr(x, 0), p(x), y)
COND3(true, x, y) → GR(x, 0)
COND3(true, x, y) → P(x)
COND3(false, x, y) → COND1(and(gr(x, 0), gr(y, 0)), x, y)
COND3(false, x, y) → AND(gr(x, 0), gr(y, 0))
COND3(false, x, y) → GR(x, 0)
COND3(false, x, y) → GR(y, 0)
COND4(true, x, y) → COND4(gr(y, 0), x, p(y))
COND4(true, x, y) → GR(y, 0)
COND4(true, x, y) → P(y)
COND4(false, x, y) → COND1(and(gr(x, 0), gr(y, 0)), x, y)
COND4(false, x, y) → AND(gr(x, 0), gr(y, 0))
COND4(false, x, y) → GR(x, 0)
COND4(false, x, y) → GR(y, 0)
GR(s(x), s(y)) → GR(x, y)
cond1(true, x, y) → cond2(gr(x, y), x, y)
cond2(true, x, y) → cond3(gr(x, 0), x, y)
cond2(false, x, y) → cond4(gr(y, 0), x, y)
cond3(true, x, y) → cond3(gr(x, 0), p(x), y)
cond3(false, x, y) → cond1(and(gr(x, 0), gr(y, 0)), x, y)
cond4(true, x, y) → cond4(gr(y, 0), x, p(y))
cond4(false, x, y) → cond1(and(gr(x, 0), gr(y, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
cond3(true, x0, x1)
cond3(false, x0, x1)
cond4(true, x0, x1)
cond4(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
p(0)
p(s(x0))
GR(s(x), s(y)) → GR(x, y)
cond1(true, x, y) → cond2(gr(x, y), x, y)
cond2(true, x, y) → cond3(gr(x, 0), x, y)
cond2(false, x, y) → cond4(gr(y, 0), x, y)
cond3(true, x, y) → cond3(gr(x, 0), p(x), y)
cond3(false, x, y) → cond1(and(gr(x, 0), gr(y, 0)), x, y)
cond4(true, x, y) → cond4(gr(y, 0), x, p(y))
cond4(false, x, y) → cond1(and(gr(x, 0), gr(y, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
cond3(true, x0, x1)
cond3(false, x0, x1)
cond4(true, x0, x1)
cond4(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
p(0)
p(s(x0))
GR(s(x), s(y)) → GR(x, y)
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
cond3(true, x0, x1)
cond3(false, x0, x1)
cond4(true, x0, x1)
cond4(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
p(0)
p(s(x0))
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
cond3(true, x0, x1)
cond3(false, x0, x1)
cond4(true, x0, x1)
cond4(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
p(0)
p(s(x0))
GR(s(x), s(y)) → GR(x, y)
From the DPs we obtained the following set of size-change graphs:
COND2(true, x, y) → COND3(gr(x, 0), x, y)
COND3(true, x, y) → COND3(gr(x, 0), p(x), y)
COND3(false, x, y) → COND1(and(gr(x, 0), gr(y, 0)), x, y)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, x, y) → COND4(gr(y, 0), x, y)
COND4(true, x, y) → COND4(gr(y, 0), x, p(y))
COND4(false, x, y) → COND1(and(gr(x, 0), gr(y, 0)), x, y)
cond1(true, x, y) → cond2(gr(x, y), x, y)
cond2(true, x, y) → cond3(gr(x, 0), x, y)
cond2(false, x, y) → cond4(gr(y, 0), x, y)
cond3(true, x, y) → cond3(gr(x, 0), p(x), y)
cond3(false, x, y) → cond1(and(gr(x, 0), gr(y, 0)), x, y)
cond4(true, x, y) → cond4(gr(y, 0), x, p(y))
cond4(false, x, y) → cond1(and(gr(x, 0), gr(y, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
cond3(true, x0, x1)
cond3(false, x0, x1)
cond4(true, x0, x1)
cond4(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
p(0)
p(s(x0))
COND2(true, x, y) → COND3(gr(x, 0), x, y)
COND3(true, x, y) → COND3(gr(x, 0), p(x), y)
COND3(false, x, y) → COND1(and(gr(x, 0), gr(y, 0)), x, y)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, x, y) → COND4(gr(y, 0), x, y)
COND4(true, x, y) → COND4(gr(y, 0), x, p(y))
COND4(false, x, y) → COND1(and(gr(x, 0), gr(y, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
and(true, true) → true
and(false, x) → false
and(x, false) → false
p(0) → 0
p(s(x)) → x
gr(s(x), s(y)) → gr(x, y)
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
cond3(true, x0, x1)
cond3(false, x0, x1)
cond4(true, x0, x1)
cond4(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
p(0)
p(s(x0))
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
cond3(true, x0, x1)
cond3(false, x0, x1)
cond4(true, x0, x1)
cond4(false, x0, x1)
COND2(true, x, y) → COND3(gr(x, 0), x, y)
COND3(true, x, y) → COND3(gr(x, 0), p(x), y)
COND3(false, x, y) → COND1(and(gr(x, 0), gr(y, 0)), x, y)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, x, y) → COND4(gr(y, 0), x, y)
COND4(true, x, y) → COND4(gr(y, 0), x, p(y))
COND4(false, x, y) → COND1(and(gr(x, 0), gr(y, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
and(true, true) → true
and(false, x) → false
and(x, false) → false
p(0) → 0
p(s(x)) → x
gr(s(x), s(y)) → gr(x, y)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
p(0)
p(s(x0))
(1) (COND1(and(gr(x56, 0), gr(x57, 0)), x56, x57)=COND1(true, x58, x59)∧COND2(gr(x58, x59), x58, x59)=COND2(true, x60, x61) ⇒ COND2(true, x60, x61)≥COND3(gr(x60, 0), x60, x61))
(2) (0=x896∧gr(x56, x896)=x894∧0=x897∧gr(x57, x897)=x895∧and(x894, x895)=true∧x56=x58∧x57=x59∧gr(x58, x59)=true ⇒ COND2(true, x58, x59)≥COND3(gr(x58, 0), x58, x59))
(3) (true=true∧0=x896∧gr(x56, x896)=true∧0=x897∧gr(x57, x897)=true∧x56=x58∧x57=x59∧gr(x58, x59)=true ⇒ COND2(true, x58, x59)≥COND3(gr(x58, 0), x58, x59))
(4) (0=x896∧gr(x56, x896)=true∧0=x897∧gr(x57, x897)=true∧x56=x58∧x57=x59∧gr(x58, x59)=true ⇒ COND2(true, x58, x59)≥COND3(gr(x58, 0), x58, x59))
(5) (true=true∧0=x896∧gr(x56, x896)=true∧0=x897∧gr(x57, x897)=true∧x56=s(x901)∧x57=0 ⇒ COND2(true, s(x901), 0)≥COND3(gr(s(x901), 0), s(x901), 0))
(6) (gr(x903, x902)=true∧0=x896∧gr(x56, x896)=true∧0=x897∧gr(x57, x897)=true∧x56=s(x903)∧x57=s(x902)∧(∀x904,x905,x906,x907:gr(x903, x902)=true∧0=x904∧gr(x905, x904)=true∧0=x906∧gr(x907, x906)=true∧x905=x903∧x907=x902 ⇒ COND2(true, x903, x902)≥COND3(gr(x903, 0), x903, x902)) ⇒ COND2(true, s(x903), s(x902))≥COND3(gr(s(x903), 0), s(x903), s(x902)))
(7) (0=x896∧s(x901)=x908∧gr(x908, x896)=true∧0=x897∧0=x909∧gr(x909, x897)=true ⇒ COND2(true, s(x901), 0)≥COND3(gr(s(x901), 0), s(x901), 0))
(8) (gr(x903, x902)=true∧0=x896∧s(x903)=x922∧gr(x922, x896)=true∧0=x897∧s(x902)=x923∧gr(x923, x897)=true∧(∀x904,x905,x906,x907:gr(x903, x902)=true∧0=x904∧gr(x905, x904)=true∧0=x906∧gr(x907, x906)=true∧x905=x903∧x907=x902 ⇒ COND2(true, x903, x902)≥COND3(gr(x903, 0), x903, x902)) ⇒ COND2(true, s(x903), s(x902))≥COND3(gr(s(x903), 0), s(x903), s(x902)))
(9) (true=true∧0=0∧s(x901)=s(x911)∧0=x897∧0=x909∧gr(x909, x897)=true ⇒ COND2(true, s(x901), 0)≥COND3(gr(s(x901), 0), s(x901), 0))
(10) (gr(x913, x912)=true∧0=s(x912)∧s(x901)=s(x913)∧0=x897∧0=x909∧gr(x909, x897)=true∧(∀x914,x915,x916:gr(x913, x912)=true∧0=x912∧s(x914)=x913∧0=x915∧0=x916∧gr(x916, x915)=true ⇒ COND2(true, s(x914), 0)≥COND3(gr(s(x914), 0), s(x914), 0)) ⇒ COND2(true, s(x901), 0)≥COND3(gr(s(x901), 0), s(x901), 0))
(11) (0=x897∧0=x909∧gr(x909, x897)=true ⇒ COND2(true, s(x901), 0)≥COND3(gr(s(x901), 0), s(x901), 0))
(12) (true=true∧0=0∧0=s(x918) ⇒ COND2(true, s(x901), 0)≥COND3(gr(s(x901), 0), s(x901), 0))
(13) (gr(x920, x919)=true∧0=s(x919)∧0=s(x920)∧(∀x921:gr(x920, x919)=true∧0=x919∧0=x920 ⇒ COND2(true, s(x921), 0)≥COND3(gr(s(x921), 0), s(x921), 0)) ⇒ COND2(true, s(x901), 0)≥COND3(gr(s(x901), 0), s(x901), 0))
(14) (true=true∧gr(x903, x902)=true∧0=0∧s(x903)=s(x925)∧0=x897∧s(x902)=x923∧gr(x923, x897)=true∧(∀x904,x905,x906,x907:gr(x903, x902)=true∧0=x904∧gr(x905, x904)=true∧0=x906∧gr(x907, x906)=true∧x905=x903∧x907=x902 ⇒ COND2(true, x903, x902)≥COND3(gr(x903, 0), x903, x902)) ⇒ COND2(true, s(x903), s(x902))≥COND3(gr(s(x903), 0), s(x903), s(x902)))
(15) (gr(x927, x926)=true∧gr(x903, x902)=true∧0=s(x926)∧s(x903)=s(x927)∧0=x897∧s(x902)=x923∧gr(x923, x897)=true∧(∀x904,x905,x906,x907:gr(x903, x902)=true∧0=x904∧gr(x905, x904)=true∧0=x906∧gr(x907, x906)=true∧x905=x903∧x907=x902 ⇒ COND2(true, x903, x902)≥COND3(gr(x903, 0), x903, x902))∧(∀x928,x929,x930,x931,x932,x933,x934,x935:gr(x927, x926)=true∧gr(x928, x929)=true∧0=x926∧s(x928)=x927∧0=x930∧s(x929)=x931∧gr(x931, x930)=true∧(∀x932,x933,x934,x935:gr(x928, x929)=true∧0=x932∧gr(x933, x932)=true∧0=x934∧gr(x935, x934)=true∧x933=x928∧x935=x929 ⇒ COND2(true, x928, x929)≥COND3(gr(x928, 0), x928, x929)) ⇒ COND2(true, s(x928), s(x929))≥COND3(gr(s(x928), 0), s(x928), s(x929))) ⇒ COND2(true, s(x903), s(x902))≥COND3(gr(s(x903), 0), s(x903), s(x902)))
(16) (gr(x903, x902)=true∧0=x897∧s(x902)=x923∧gr(x923, x897)=true∧(∀x904,x905,x906,x907:gr(x903, x902)=true∧0=x904∧gr(x905, x904)=true∧0=x906∧gr(x907, x906)=true∧x905=x903∧x907=x902 ⇒ COND2(true, x903, x902)≥COND3(gr(x903, 0), x903, x902)) ⇒ COND2(true, s(x903), s(x902))≥COND3(gr(s(x903), 0), s(x903), s(x902)))
(17) (true=true∧gr(x903, x902)=true∧0=0∧s(x902)=s(x937)∧(∀x904,x905,x906,x907:gr(x903, x902)=true∧0=x904∧gr(x905, x904)=true∧0=x906∧gr(x907, x906)=true∧x905=x903∧x907=x902 ⇒ COND2(true, x903, x902)≥COND3(gr(x903, 0), x903, x902)) ⇒ COND2(true, s(x903), s(x902))≥COND3(gr(s(x903), 0), s(x903), s(x902)))
(18) (gr(x939, x938)=true∧gr(x903, x902)=true∧0=s(x938)∧s(x902)=s(x939)∧(∀x904,x905,x906,x907:gr(x903, x902)=true∧0=x904∧gr(x905, x904)=true∧0=x906∧gr(x907, x906)=true∧x905=x903∧x907=x902 ⇒ COND2(true, x903, x902)≥COND3(gr(x903, 0), x903, x902))∧(∀x940,x941,x942,x943,x944,x945:gr(x939, x938)=true∧gr(x940, x941)=true∧0=x938∧s(x941)=x939∧(∀x942,x943,x944,x945:gr(x940, x941)=true∧0=x942∧gr(x943, x942)=true∧0=x944∧gr(x945, x944)=true∧x943=x940∧x945=x941 ⇒ COND2(true, x940, x941)≥COND3(gr(x940, 0), x940, x941)) ⇒ COND2(true, s(x940), s(x941))≥COND3(gr(s(x940), 0), s(x940), s(x941))) ⇒ COND2(true, s(x903), s(x902))≥COND3(gr(s(x903), 0), s(x903), s(x902)))
(19) (gr(x903, x902)=true ⇒ COND2(true, s(x903), s(x902))≥COND3(gr(s(x903), 0), s(x903), s(x902)))
(20) (true=true ⇒ COND2(true, s(s(x947)), s(0))≥COND3(gr(s(s(x947)), 0), s(s(x947)), s(0)))
(21) (gr(x949, x948)=true∧(gr(x949, x948)=true ⇒ COND2(true, s(x949), s(x948))≥COND3(gr(s(x949), 0), s(x949), s(x948))) ⇒ COND2(true, s(s(x949)), s(s(x948)))≥COND3(gr(s(s(x949)), 0), s(s(x949)), s(s(x948))))
(22) (COND2(true, s(s(x947)), s(0))≥COND3(gr(s(s(x947)), 0), s(s(x947)), s(0)))
(23) (COND2(true, s(x949), s(x948))≥COND3(gr(s(x949), 0), s(x949), s(x948)) ⇒ COND2(true, s(s(x949)), s(s(x948)))≥COND3(gr(s(s(x949)), 0), s(s(x949)), s(s(x948))))
(24) (COND1(and(gr(x68, 0), gr(x69, 0)), x68, x69)=COND1(true, x70, x71)∧COND2(gr(x70, x71), x70, x71)=COND2(true, x72, x73) ⇒ COND2(true, x72, x73)≥COND3(gr(x72, 0), x72, x73))
(25) (0=x952∧gr(x68, x952)=x950∧0=x953∧gr(x69, x953)=x951∧and(x950, x951)=true∧x68=x70∧x69=x71∧gr(x70, x71)=true ⇒ COND2(true, x70, x71)≥COND3(gr(x70, 0), x70, x71))
(26) (true=true∧0=x952∧gr(x68, x952)=true∧0=x953∧gr(x69, x953)=true∧x68=x70∧x69=x71∧gr(x70, x71)=true ⇒ COND2(true, x70, x71)≥COND3(gr(x70, 0), x70, x71))
(27) (0=x952∧gr(x68, x952)=true∧0=x953∧gr(x69, x953)=true∧x68=x70∧x69=x71∧gr(x70, x71)=true ⇒ COND2(true, x70, x71)≥COND3(gr(x70, 0), x70, x71))
(28) (true=true∧0=x952∧gr(x68, x952)=true∧0=x953∧gr(x69, x953)=true∧x68=s(x957)∧x69=0 ⇒ COND2(true, s(x957), 0)≥COND3(gr(s(x957), 0), s(x957), 0))
(29) (gr(x959, x958)=true∧0=x952∧gr(x68, x952)=true∧0=x953∧gr(x69, x953)=true∧x68=s(x959)∧x69=s(x958)∧(∀x960,x961,x962,x963:gr(x959, x958)=true∧0=x960∧gr(x961, x960)=true∧0=x962∧gr(x963, x962)=true∧x961=x959∧x963=x958 ⇒ COND2(true, x959, x958)≥COND3(gr(x959, 0), x959, x958)) ⇒ COND2(true, s(x959), s(x958))≥COND3(gr(s(x959), 0), s(x959), s(x958)))
(30) (0=x952∧s(x957)=x964∧gr(x964, x952)=true∧0=x953∧0=x965∧gr(x965, x953)=true ⇒ COND2(true, s(x957), 0)≥COND3(gr(s(x957), 0), s(x957), 0))
(31) (gr(x959, x958)=true∧0=x952∧s(x959)=x978∧gr(x978, x952)=true∧0=x953∧s(x958)=x979∧gr(x979, x953)=true∧(∀x960,x961,x962,x963:gr(x959, x958)=true∧0=x960∧gr(x961, x960)=true∧0=x962∧gr(x963, x962)=true∧x961=x959∧x963=x958 ⇒ COND2(true, x959, x958)≥COND3(gr(x959, 0), x959, x958)) ⇒ COND2(true, s(x959), s(x958))≥COND3(gr(s(x959), 0), s(x959), s(x958)))
(32) (true=true∧0=0∧s(x957)=s(x967)∧0=x953∧0=x965∧gr(x965, x953)=true ⇒ COND2(true, s(x957), 0)≥COND3(gr(s(x957), 0), s(x957), 0))
(33) (gr(x969, x968)=true∧0=s(x968)∧s(x957)=s(x969)∧0=x953∧0=x965∧gr(x965, x953)=true∧(∀x970,x971,x972:gr(x969, x968)=true∧0=x968∧s(x970)=x969∧0=x971∧0=x972∧gr(x972, x971)=true ⇒ COND2(true, s(x970), 0)≥COND3(gr(s(x970), 0), s(x970), 0)) ⇒ COND2(true, s(x957), 0)≥COND3(gr(s(x957), 0), s(x957), 0))
(34) (0=x953∧0=x965∧gr(x965, x953)=true ⇒ COND2(true, s(x957), 0)≥COND3(gr(s(x957), 0), s(x957), 0))
(35) (true=true∧0=0∧0=s(x974) ⇒ COND2(true, s(x957), 0)≥COND3(gr(s(x957), 0), s(x957), 0))
(36) (gr(x976, x975)=true∧0=s(x975)∧0=s(x976)∧(∀x977:gr(x976, x975)=true∧0=x975∧0=x976 ⇒ COND2(true, s(x977), 0)≥COND3(gr(s(x977), 0), s(x977), 0)) ⇒ COND2(true, s(x957), 0)≥COND3(gr(s(x957), 0), s(x957), 0))
(37) (true=true∧gr(x959, x958)=true∧0=0∧s(x959)=s(x981)∧0=x953∧s(x958)=x979∧gr(x979, x953)=true∧(∀x960,x961,x962,x963:gr(x959, x958)=true∧0=x960∧gr(x961, x960)=true∧0=x962∧gr(x963, x962)=true∧x961=x959∧x963=x958 ⇒ COND2(true, x959, x958)≥COND3(gr(x959, 0), x959, x958)) ⇒ COND2(true, s(x959), s(x958))≥COND3(gr(s(x959), 0), s(x959), s(x958)))
(38) (gr(x983, x982)=true∧gr(x959, x958)=true∧0=s(x982)∧s(x959)=s(x983)∧0=x953∧s(x958)=x979∧gr(x979, x953)=true∧(∀x960,x961,x962,x963:gr(x959, x958)=true∧0=x960∧gr(x961, x960)=true∧0=x962∧gr(x963, x962)=true∧x961=x959∧x963=x958 ⇒ COND2(true, x959, x958)≥COND3(gr(x959, 0), x959, x958))∧(∀x984,x985,x986,x987,x988,x989,x990,x991:gr(x983, x982)=true∧gr(x984, x985)=true∧0=x982∧s(x984)=x983∧0=x986∧s(x985)=x987∧gr(x987, x986)=true∧(∀x988,x989,x990,x991:gr(x984, x985)=true∧0=x988∧gr(x989, x988)=true∧0=x990∧gr(x991, x990)=true∧x989=x984∧x991=x985 ⇒ COND2(true, x984, x985)≥COND3(gr(x984, 0), x984, x985)) ⇒ COND2(true, s(x984), s(x985))≥COND3(gr(s(x984), 0), s(x984), s(x985))) ⇒ COND2(true, s(x959), s(x958))≥COND3(gr(s(x959), 0), s(x959), s(x958)))
(39) (gr(x959, x958)=true∧0=x953∧s(x958)=x979∧gr(x979, x953)=true∧(∀x960,x961,x962,x963:gr(x959, x958)=true∧0=x960∧gr(x961, x960)=true∧0=x962∧gr(x963, x962)=true∧x961=x959∧x963=x958 ⇒ COND2(true, x959, x958)≥COND3(gr(x959, 0), x959, x958)) ⇒ COND2(true, s(x959), s(x958))≥COND3(gr(s(x959), 0), s(x959), s(x958)))
(40) (true=true∧gr(x959, x958)=true∧0=0∧s(x958)=s(x993)∧(∀x960,x961,x962,x963:gr(x959, x958)=true∧0=x960∧gr(x961, x960)=true∧0=x962∧gr(x963, x962)=true∧x961=x959∧x963=x958 ⇒ COND2(true, x959, x958)≥COND3(gr(x959, 0), x959, x958)) ⇒ COND2(true, s(x959), s(x958))≥COND3(gr(s(x959), 0), s(x959), s(x958)))
(41) (gr(x995, x994)=true∧gr(x959, x958)=true∧0=s(x994)∧s(x958)=s(x995)∧(∀x960,x961,x962,x963:gr(x959, x958)=true∧0=x960∧gr(x961, x960)=true∧0=x962∧gr(x963, x962)=true∧x961=x959∧x963=x958 ⇒ COND2(true, x959, x958)≥COND3(gr(x959, 0), x959, x958))∧(∀x996,x997,x998,x999,x1000,x1001:gr(x995, x994)=true∧gr(x996, x997)=true∧0=x994∧s(x997)=x995∧(∀x998,x999,x1000,x1001:gr(x996, x997)=true∧0=x998∧gr(x999, x998)=true∧0=x1000∧gr(x1001, x1000)=true∧x999=x996∧x1001=x997 ⇒ COND2(true, x996, x997)≥COND3(gr(x996, 0), x996, x997)) ⇒ COND2(true, s(x996), s(x997))≥COND3(gr(s(x996), 0), s(x996), s(x997))) ⇒ COND2(true, s(x959), s(x958))≥COND3(gr(s(x959), 0), s(x959), s(x958)))
(42) (gr(x959, x958)=true ⇒ COND2(true, s(x959), s(x958))≥COND3(gr(s(x959), 0), s(x959), s(x958)))
(43) (true=true ⇒ COND2(true, s(s(x1003)), s(0))≥COND3(gr(s(s(x1003)), 0), s(s(x1003)), s(0)))
(44) (gr(x1005, x1004)=true∧(gr(x1005, x1004)=true ⇒ COND2(true, s(x1005), s(x1004))≥COND3(gr(s(x1005), 0), s(x1005), s(x1004))) ⇒ COND2(true, s(s(x1005)), s(s(x1004)))≥COND3(gr(s(s(x1005)), 0), s(s(x1005)), s(s(x1004))))
(45) (COND2(true, s(s(x1003)), s(0))≥COND3(gr(s(s(x1003)), 0), s(s(x1003)), s(0)))
(46) (COND2(true, s(x1005), s(x1004))≥COND3(gr(s(x1005), 0), s(x1005), s(x1004)) ⇒ COND2(true, s(s(x1005)), s(s(x1004)))≥COND3(gr(s(s(x1005)), 0), s(s(x1005)), s(s(x1004))))
(47) (COND2(gr(x132, x133), x132, x133)=COND2(true, x134, x135)∧COND3(gr(x134, 0), x134, x135)=COND3(true, x136, x137) ⇒ COND3(true, x136, x137)≥COND3(gr(x136, 0), p(x136), x137))
(48) (gr(x132, x133)=true∧x132=x134∧0=x1006∧gr(x134, x1006)=true ⇒ COND3(true, x134, x133)≥COND3(gr(x134, 0), p(x134), x133))
(49) (true=true∧s(x1008)=x134∧0=x1006∧gr(x134, x1006)=true ⇒ COND3(true, x134, 0)≥COND3(gr(x134, 0), p(x134), 0))
(50) (gr(x1010, x1009)=true∧s(x1010)=x134∧0=x1006∧gr(x134, x1006)=true∧(∀x1011,x1012:gr(x1010, x1009)=true∧x1010=x1011∧0=x1012∧gr(x1011, x1012)=true ⇒ COND3(true, x1011, x1009)≥COND3(gr(x1011, 0), p(x1011), x1009)) ⇒ COND3(true, x134, s(x1009))≥COND3(gr(x134, 0), p(x134), s(x1009)))
(51) (s(x1008)=x134∧0=x1006∧gr(x134, x1006)=true ⇒ COND3(true, x134, 0)≥COND3(gr(x134, 0), p(x134), 0))
(52) (true=true∧gr(x1010, x1009)=true∧s(x1010)=s(x1019)∧0=0∧(∀x1011,x1012:gr(x1010, x1009)=true∧x1010=x1011∧0=x1012∧gr(x1011, x1012)=true ⇒ COND3(true, x1011, x1009)≥COND3(gr(x1011, 0), p(x1011), x1009)) ⇒ COND3(true, s(x1019), s(x1009))≥COND3(gr(s(x1019), 0), p(s(x1019)), s(x1009)))
(53) (gr(x1021, x1020)=true∧gr(x1010, x1009)=true∧s(x1010)=s(x1021)∧0=s(x1020)∧(∀x1011,x1012:gr(x1010, x1009)=true∧x1010=x1011∧0=x1012∧gr(x1011, x1012)=true ⇒ COND3(true, x1011, x1009)≥COND3(gr(x1011, 0), p(x1011), x1009))∧(∀x1022,x1023,x1024,x1025:gr(x1021, x1020)=true∧gr(x1022, x1023)=true∧s(x1022)=x1021∧0=x1020∧(∀x1024,x1025:gr(x1022, x1023)=true∧x1022=x1024∧0=x1025∧gr(x1024, x1025)=true ⇒ COND3(true, x1024, x1023)≥COND3(gr(x1024, 0), p(x1024), x1023)) ⇒ COND3(true, x1021, s(x1023))≥COND3(gr(x1021, 0), p(x1021), s(x1023))) ⇒ COND3(true, s(x1021), s(x1009))≥COND3(gr(s(x1021), 0), p(s(x1021)), s(x1009)))
(54) (true=true∧s(x1008)=s(x1014)∧0=0 ⇒ COND3(true, s(x1014), 0)≥COND3(gr(s(x1014), 0), p(s(x1014)), 0))
(55) (gr(x1016, x1015)=true∧s(x1008)=s(x1016)∧0=s(x1015)∧(∀x1017:gr(x1016, x1015)=true∧s(x1017)=x1016∧0=x1015 ⇒ COND3(true, x1016, 0)≥COND3(gr(x1016, 0), p(x1016), 0)) ⇒ COND3(true, s(x1016), 0)≥COND3(gr(s(x1016), 0), p(s(x1016)), 0))
(56) (COND3(true, s(x1008), 0)≥COND3(gr(s(x1008), 0), p(s(x1008)), 0))
(57) (gr(x1010, x1009)=true ⇒ COND3(true, s(x1010), s(x1009))≥COND3(gr(s(x1010), 0), p(s(x1010)), s(x1009)))
(58) (true=true ⇒ COND3(true, s(s(x1027)), s(0))≥COND3(gr(s(s(x1027)), 0), p(s(s(x1027))), s(0)))
(59) (gr(x1029, x1028)=true∧(gr(x1029, x1028)=true ⇒ COND3(true, s(x1029), s(x1028))≥COND3(gr(s(x1029), 0), p(s(x1029)), s(x1028))) ⇒ COND3(true, s(s(x1029)), s(s(x1028)))≥COND3(gr(s(s(x1029)), 0), p(s(s(x1029))), s(s(x1028))))
(60) (COND3(true, s(s(x1027)), s(0))≥COND3(gr(s(s(x1027)), 0), p(s(s(x1027))), s(0)))
(61) (COND3(true, s(x1029), s(x1028))≥COND3(gr(s(x1029), 0), p(s(x1029)), s(x1028)) ⇒ COND3(true, s(s(x1029)), s(s(x1028)))≥COND3(gr(s(s(x1029)), 0), p(s(s(x1029))), s(s(x1028))))
(62) (COND3(gr(x144, 0), x144, x145)=COND3(true, x146, x147)∧COND3(gr(x146, 0), p(x146), x147)=COND3(true, x148, x149) ⇒ COND3(true, x148, x149)≥COND3(gr(x148, 0), p(x148), x149))
(63) (0=x1030∧gr(x144, x1030)=true∧x144=x146∧0=x1031∧gr(x146, x1031)=true∧p(x146)=x148 ⇒ COND3(true, x148, x145)≥COND3(gr(x148, 0), p(x148), x145))
(64) (true=true∧0=0∧s(x1033)=x146∧0=x1031∧gr(x146, x1031)=true∧p(x146)=x148 ⇒ COND3(true, x148, x145)≥COND3(gr(x148, 0), p(x148), x145))
(65) (gr(x1035, x1034)=true∧0=s(x1034)∧s(x1035)=x146∧0=x1031∧gr(x146, x1031)=true∧p(x146)=x148∧(∀x1036,x1037,x1038,x1039:gr(x1035, x1034)=true∧0=x1034∧x1035=x1036∧0=x1037∧gr(x1036, x1037)=true∧p(x1036)=x1038 ⇒ COND3(true, x1038, x1039)≥COND3(gr(x1038, 0), p(x1038), x1039)) ⇒ COND3(true, x148, x145)≥COND3(gr(x148, 0), p(x148), x145))
(66) (s(x1033)=x146∧0=x1031∧gr(x146, x1031)=true∧p(x146)=x148 ⇒ COND3(true, x148, x145)≥COND3(gr(x148, 0), p(x148), x145))
(67) (true=true∧s(x1033)=s(x1041)∧0=0∧p(s(x1041))=x148 ⇒ COND3(true, x148, x145)≥COND3(gr(x148, 0), p(x148), x145))
(68) (gr(x1043, x1042)=true∧s(x1033)=s(x1043)∧0=s(x1042)∧p(s(x1043))=x148∧(∀x1044,x1045,x1046:gr(x1043, x1042)=true∧s(x1044)=x1043∧0=x1042∧p(x1043)=x1045 ⇒ COND3(true, x1045, x1046)≥COND3(gr(x1045, 0), p(x1045), x1046)) ⇒ COND3(true, x148, x145)≥COND3(gr(x148, 0), p(x148), x145))
(69) (COND3(true, x148, x145)≥COND3(gr(x148, 0), p(x148), x145))
(70) (COND3(gr(x150, 0), p(x150), x151)=COND3(true, x152, x153)∧COND3(gr(x152, 0), p(x152), x153)=COND3(true, x154, x155) ⇒ COND3(true, x154, x155)≥COND3(gr(x154, 0), p(x154), x155))
(71) (0=x1048∧gr(x150, x1048)=true∧p(x150)=x152∧0=x1049∧gr(x152, x1049)=true∧p(x152)=x154 ⇒ COND3(true, x154, x151)≥COND3(gr(x154, 0), p(x154), x151))
(72) (true=true∧0=0∧p(s(x1051))=x152∧0=x1049∧gr(x152, x1049)=true∧p(x152)=x154 ⇒ COND3(true, x154, x151)≥COND3(gr(x154, 0), p(x154), x151))
(73) (gr(x1053, x1052)=true∧0=s(x1052)∧p(s(x1053))=x152∧0=x1049∧gr(x152, x1049)=true∧p(x152)=x154∧(∀x1054,x1055,x1056,x1057:gr(x1053, x1052)=true∧0=x1052∧p(x1053)=x1054∧0=x1055∧gr(x1054, x1055)=true∧p(x1054)=x1056 ⇒ COND3(true, x1056, x1057)≥COND3(gr(x1056, 0), p(x1056), x1057)) ⇒ COND3(true, x154, x151)≥COND3(gr(x154, 0), p(x154), x151))
(74) (s(x1051)=x1058∧p(x1058)=x152∧0=x1049∧gr(x152, x1049)=true∧p(x152)=x154 ⇒ COND3(true, x154, x151)≥COND3(gr(x154, 0), p(x154), x151))
(75) (true=true∧s(x1051)=x1058∧p(x1058)=s(x1060)∧0=0∧p(s(x1060))=x154 ⇒ COND3(true, x154, x151)≥COND3(gr(x154, 0), p(x154), x151))
(76) (gr(x1062, x1061)=true∧s(x1051)=x1058∧p(x1058)=s(x1062)∧0=s(x1061)∧p(s(x1062))=x154∧(∀x1063,x1064,x1065,x1066:gr(x1062, x1061)=true∧s(x1063)=x1064∧p(x1064)=x1062∧0=x1061∧p(x1062)=x1065 ⇒ COND3(true, x1065, x1066)≥COND3(gr(x1065, 0), p(x1065), x1066)) ⇒ COND3(true, x154, x151)≥COND3(gr(x154, 0), p(x154), x151))
(77) (s(x1051)=x1058∧p(x1058)=s(x1060)∧s(x1060)=x1067∧p(x1067)=x154 ⇒ COND3(true, x154, x151)≥COND3(gr(x154, 0), p(x154), x151))
(78) (x1068=s(x1060)∧s(x1051)=s(x1068)∧s(x1060)=x1067∧p(x1067)=x154 ⇒ COND3(true, x154, x151)≥COND3(gr(x154, 0), p(x154), x151))
(79) (COND3(true, x154, x151)≥COND3(gr(x154, 0), p(x154), x151))
(80) (COND2(gr(x260, x261), x260, x261)=COND2(true, x262, x263)∧COND3(gr(x262, 0), x262, x263)=COND3(false, x264, x265) ⇒ COND3(false, x264, x265)≥COND1(and(gr(x264, 0), gr(x265, 0)), x264, x265))
(81) (gr(x260, x261)=true∧x260=x262∧0=x1069∧gr(x262, x1069)=false ⇒ COND3(false, x262, x261)≥COND1(and(gr(x262, 0), gr(x261, 0)), x262, x261))
(82) (true=true∧s(x1071)=x262∧0=x1069∧gr(x262, x1069)=false ⇒ COND3(false, x262, 0)≥COND1(and(gr(x262, 0), gr(0, 0)), x262, 0))
(83) (gr(x1073, x1072)=true∧s(x1073)=x262∧0=x1069∧gr(x262, x1069)=false∧(∀x1074,x1075:gr(x1073, x1072)=true∧x1073=x1074∧0=x1075∧gr(x1074, x1075)=false ⇒ COND3(false, x1074, x1072)≥COND1(and(gr(x1074, 0), gr(x1072, 0)), x1074, x1072)) ⇒ COND3(false, x262, s(x1072))≥COND1(and(gr(x262, 0), gr(s(x1072), 0)), x262, s(x1072)))
(84) (s(x1071)=x262∧0=x1069∧gr(x262, x1069)=false ⇒ COND3(false, x262, 0)≥COND1(and(gr(x262, 0), gr(0, 0)), x262, 0))
(85) (false=false∧gr(x1073, x1072)=true∧s(x1073)=0∧0=x1081∧(∀x1074,x1075:gr(x1073, x1072)=true∧x1073=x1074∧0=x1075∧gr(x1074, x1075)=false ⇒ COND3(false, x1074, x1072)≥COND1(and(gr(x1074, 0), gr(x1072, 0)), x1074, x1072)) ⇒ COND3(false, 0, s(x1072))≥COND1(and(gr(0, 0), gr(s(x1072), 0)), 0, s(x1072)))
(86) (gr(x1084, x1083)=false∧gr(x1073, x1072)=true∧s(x1073)=s(x1084)∧0=s(x1083)∧(∀x1074,x1075:gr(x1073, x1072)=true∧x1073=x1074∧0=x1075∧gr(x1074, x1075)=false ⇒ COND3(false, x1074, x1072)≥COND1(and(gr(x1074, 0), gr(x1072, 0)), x1074, x1072))∧(∀x1085,x1086,x1087,x1088:gr(x1084, x1083)=false∧gr(x1085, x1086)=true∧s(x1085)=x1084∧0=x1083∧(∀x1087,x1088:gr(x1085, x1086)=true∧x1085=x1087∧0=x1088∧gr(x1087, x1088)=false ⇒ COND3(false, x1087, x1086)≥COND1(and(gr(x1087, 0), gr(x1086, 0)), x1087, x1086)) ⇒ COND3(false, x1084, s(x1086))≥COND1(and(gr(x1084, 0), gr(s(x1086), 0)), x1084, s(x1086))) ⇒ COND3(false, s(x1084), s(x1072))≥COND1(and(gr(s(x1084), 0), gr(s(x1072), 0)), s(x1084), s(x1072)))
(87) (false=false∧s(x1071)=0∧0=x1076 ⇒ COND3(false, 0, 0)≥COND1(and(gr(0, 0), gr(0, 0)), 0, 0))
(88) (gr(x1079, x1078)=false∧s(x1071)=s(x1079)∧0=s(x1078)∧(∀x1080:gr(x1079, x1078)=false∧s(x1080)=x1079∧0=x1078 ⇒ COND3(false, x1079, 0)≥COND1(and(gr(x1079, 0), gr(0, 0)), x1079, 0)) ⇒ COND3(false, s(x1079), 0)≥COND1(and(gr(s(x1079), 0), gr(0, 0)), s(x1079), 0))
(89) (COND3(gr(x272, 0), x272, x273)=COND3(true, x274, x275)∧COND3(gr(x274, 0), p(x274), x275)=COND3(false, x276, x277) ⇒ COND3(false, x276, x277)≥COND1(and(gr(x276, 0), gr(x277, 0)), x276, x277))
(90) (0=x1089∧gr(x272, x1089)=true∧x272=x274∧0=x1090∧gr(x274, x1090)=false∧p(x274)=x276 ⇒ COND3(false, x276, x273)≥COND1(and(gr(x276, 0), gr(x273, 0)), x276, x273))
(91) (true=true∧0=0∧s(x1092)=x274∧0=x1090∧gr(x274, x1090)=false∧p(x274)=x276 ⇒ COND3(false, x276, x273)≥COND1(and(gr(x276, 0), gr(x273, 0)), x276, x273))
(92) (gr(x1094, x1093)=true∧0=s(x1093)∧s(x1094)=x274∧0=x1090∧gr(x274, x1090)=false∧p(x274)=x276∧(∀x1095,x1096,x1097,x1098:gr(x1094, x1093)=true∧0=x1093∧x1094=x1095∧0=x1096∧gr(x1095, x1096)=false∧p(x1095)=x1097 ⇒ COND3(false, x1097, x1098)≥COND1(and(gr(x1097, 0), gr(x1098, 0)), x1097, x1098)) ⇒ COND3(false, x276, x273)≥COND1(and(gr(x276, 0), gr(x273, 0)), x276, x273))
(93) (s(x1092)=x274∧0=x1090∧gr(x274, x1090)=false∧p(x274)=x276 ⇒ COND3(false, x276, x273)≥COND1(and(gr(x276, 0), gr(x273, 0)), x276, x273))
(94) (false=false∧s(x1092)=0∧0=x1099∧p(0)=x276 ⇒ COND3(false, x276, x273)≥COND1(and(gr(x276, 0), gr(x273, 0)), x276, x273))
(95) (gr(x1102, x1101)=false∧s(x1092)=s(x1102)∧0=s(x1101)∧p(s(x1102))=x276∧(∀x1103,x1104,x1105:gr(x1102, x1101)=false∧s(x1103)=x1102∧0=x1101∧p(x1102)=x1104 ⇒ COND3(false, x1104, x1105)≥COND1(and(gr(x1104, 0), gr(x1105, 0)), x1104, x1105)) ⇒ COND3(false, x276, x273)≥COND1(and(gr(x276, 0), gr(x273, 0)), x276, x273))
(96) (COND3(gr(x278, 0), p(x278), x279)=COND3(true, x280, x281)∧COND3(gr(x280, 0), p(x280), x281)=COND3(false, x282, x283) ⇒ COND3(false, x282, x283)≥COND1(and(gr(x282, 0), gr(x283, 0)), x282, x283))
(97) (0=x1106∧gr(x278, x1106)=true∧p(x278)=x280∧0=x1107∧gr(x280, x1107)=false∧p(x280)=x282 ⇒ COND3(false, x282, x279)≥COND1(and(gr(x282, 0), gr(x279, 0)), x282, x279))
(98) (true=true∧0=0∧p(s(x1109))=x280∧0=x1107∧gr(x280, x1107)=false∧p(x280)=x282 ⇒ COND3(false, x282, x279)≥COND1(and(gr(x282, 0), gr(x279, 0)), x282, x279))
(99) (gr(x1111, x1110)=true∧0=s(x1110)∧p(s(x1111))=x280∧0=x1107∧gr(x280, x1107)=false∧p(x280)=x282∧(∀x1112,x1113,x1114,x1115:gr(x1111, x1110)=true∧0=x1110∧p(x1111)=x1112∧0=x1113∧gr(x1112, x1113)=false∧p(x1112)=x1114 ⇒ COND3(false, x1114, x1115)≥COND1(and(gr(x1114, 0), gr(x1115, 0)), x1114, x1115)) ⇒ COND3(false, x282, x279)≥COND1(and(gr(x282, 0), gr(x279, 0)), x282, x279))
(100) (s(x1109)=x1116∧p(x1116)=x280∧0=x1107∧gr(x280, x1107)=false∧p(x280)=x282 ⇒ COND3(false, x282, x279)≥COND1(and(gr(x282, 0), gr(x279, 0)), x282, x279))
(101) (false=false∧s(x1109)=x1116∧p(x1116)=0∧0=x1117∧p(0)=x282 ⇒ COND3(false, x282, x279)≥COND1(and(gr(x282, 0), gr(x279, 0)), x282, x279))
(102) (gr(x1120, x1119)=false∧s(x1109)=x1116∧p(x1116)=s(x1120)∧0=s(x1119)∧p(s(x1120))=x282∧(∀x1121,x1122,x1123,x1124:gr(x1120, x1119)=false∧s(x1121)=x1122∧p(x1122)=x1120∧0=x1119∧p(x1120)=x1123 ⇒ COND3(false, x1123, x1124)≥COND1(and(gr(x1123, 0), gr(x1124, 0)), x1123, x1124)) ⇒ COND3(false, x282, x279)≥COND1(and(gr(x282, 0), gr(x279, 0)), x282, x279))
(103) (s(x1109)=x1116∧p(x1116)=0∧0=x1125∧p(x1125)=x282 ⇒ COND3(false, x282, x279)≥COND1(and(gr(x282, 0), gr(x279, 0)), x282, x279))
(104) (0=0∧s(x1109)=0∧0=x1125∧p(x1125)=x282 ⇒ COND3(false, x282, x279)≥COND1(and(gr(x282, 0), gr(x279, 0)), x282, x279))
(105) (x1126=0∧s(x1109)=s(x1126)∧0=x1125∧p(x1125)=x282 ⇒ COND3(false, x282, x279)≥COND1(and(gr(x282, 0), gr(x279, 0)), x282, x279))
(106) (COND3(false, x282, x279)≥COND1(and(gr(x282, 0), gr(x279, 0)), x282, x279))
(107) (COND3(gr(x416, 0), x416, x417)=COND3(false, x418, x419)∧COND1(and(gr(x418, 0), gr(x419, 0)), x418, x419)=COND1(true, x420, x421) ⇒ COND1(true, x420, x421)≥COND2(gr(x420, x421), x420, x421))
(108) (0=x1127∧gr(x416, x1127)=false∧x416=x418∧0=x1130∧gr(x418, x1130)=x1128∧0=x1131∧gr(x419, x1131)=x1129∧and(x1128, x1129)=true ⇒ COND1(true, x418, x419)≥COND2(gr(x418, x419), x418, x419))
(109) (true=true∧0=x1127∧gr(x416, x1127)=false∧x416=x418∧0=x1130∧gr(x418, x1130)=true∧0=x1131∧gr(x419, x1131)=true ⇒ COND1(true, x418, x419)≥COND2(gr(x418, x419), x418, x419))
(110) (0=x1127∧gr(x416, x1127)=false∧x416=x418∧0=x1130∧gr(x418, x1130)=true∧0=x1131∧gr(x419, x1131)=true ⇒ COND1(true, x418, x419)≥COND2(gr(x418, x419), x418, x419))
(111) (false=false∧0=x1134∧0=x418∧0=x1130∧gr(x418, x1130)=true∧0=x1131∧gr(x419, x1131)=true ⇒ COND1(true, x418, x419)≥COND2(gr(x418, x419), x418, x419))
(112) (gr(x1137, x1136)=false∧0=s(x1136)∧s(x1137)=x418∧0=x1130∧gr(x418, x1130)=true∧0=x1131∧gr(x419, x1131)=true∧(∀x1138,x1139,x1140,x1141:gr(x1137, x1136)=false∧0=x1136∧x1137=x1138∧0=x1139∧gr(x1138, x1139)=true∧0=x1140∧gr(x1141, x1140)=true ⇒ COND1(true, x1138, x1141)≥COND2(gr(x1138, x1141), x1138, x1141)) ⇒ COND1(true, x418, x419)≥COND2(gr(x418, x419), x418, x419))
(113) (0=x418∧0=x1130∧gr(x418, x1130)=true∧0=x1131∧gr(x419, x1131)=true ⇒ COND1(true, x418, x419)≥COND2(gr(x418, x419), x418, x419))
(114) (true=true∧0=s(x1143)∧0=0∧0=x1131∧gr(x419, x1131)=true ⇒ COND1(true, s(x1143), x419)≥COND2(gr(s(x1143), x419), s(x1143), x419))
(115) (gr(x1145, x1144)=true∧0=s(x1145)∧0=s(x1144)∧0=x1131∧gr(x419, x1131)=true∧(∀x1146,x1147:gr(x1145, x1144)=true∧0=x1145∧0=x1144∧0=x1146∧gr(x1147, x1146)=true ⇒ COND1(true, x1145, x1147)≥COND2(gr(x1145, x1147), x1145, x1147)) ⇒ COND1(true, s(x1145), x419)≥COND2(gr(s(x1145), x419), s(x1145), x419))
(116) (COND3(gr(x422, 0), p(x422), x423)=COND3(false, x424, x425)∧COND1(and(gr(x424, 0), gr(x425, 0)), x424, x425)=COND1(true, x426, x427) ⇒ COND1(true, x426, x427)≥COND2(gr(x426, x427), x426, x427))
(117) (0=x1148∧gr(x422, x1148)=false∧p(x422)=x424∧0=x1151∧gr(x424, x1151)=x1149∧0=x1152∧gr(x425, x1152)=x1150∧and(x1149, x1150)=true ⇒ COND1(true, x424, x425)≥COND2(gr(x424, x425), x424, x425))
(118) (true=true∧0=x1148∧gr(x422, x1148)=false∧p(x422)=x424∧0=x1151∧gr(x424, x1151)=true∧0=x1152∧gr(x425, x1152)=true ⇒ COND1(true, x424, x425)≥COND2(gr(x424, x425), x424, x425))
(119) (0=x1148∧gr(x422, x1148)=false∧p(x422)=x424∧0=x1151∧gr(x424, x1151)=true∧0=x1152∧gr(x425, x1152)=true ⇒ COND1(true, x424, x425)≥COND2(gr(x424, x425), x424, x425))
(120) (false=false∧0=x1155∧p(0)=x424∧0=x1151∧gr(x424, x1151)=true∧0=x1152∧gr(x425, x1152)=true ⇒ COND1(true, x424, x425)≥COND2(gr(x424, x425), x424, x425))
(121) (gr(x1158, x1157)=false∧0=s(x1157)∧p(s(x1158))=x424∧0=x1151∧gr(x424, x1151)=true∧0=x1152∧gr(x425, x1152)=true∧(∀x1159,x1160,x1161,x1162:gr(x1158, x1157)=false∧0=x1157∧p(x1158)=x1159∧0=x1160∧gr(x1159, x1160)=true∧0=x1161∧gr(x1162, x1161)=true ⇒ COND1(true, x1159, x1162)≥COND2(gr(x1159, x1162), x1159, x1162)) ⇒ COND1(true, x424, x425)≥COND2(gr(x424, x425), x424, x425))
(122) (0=x1163∧p(x1163)=x424∧0=x1151∧gr(x424, x1151)=true∧0=x1152∧gr(x425, x1152)=true ⇒ COND1(true, x424, x425)≥COND2(gr(x424, x425), x424, x425))
(123) (true=true∧0=x1163∧p(x1163)=s(x1165)∧0=0∧0=x1152∧gr(x425, x1152)=true ⇒ COND1(true, s(x1165), x425)≥COND2(gr(s(x1165), x425), s(x1165), x425))
(124) (gr(x1167, x1166)=true∧0=x1163∧p(x1163)=s(x1167)∧0=s(x1166)∧0=x1152∧gr(x425, x1152)=true∧(∀x1168,x1169,x1170:gr(x1167, x1166)=true∧0=x1168∧p(x1168)=x1167∧0=x1166∧0=x1169∧gr(x1170, x1169)=true ⇒ COND1(true, x1167, x1170)≥COND2(gr(x1167, x1170), x1167, x1170)) ⇒ COND1(true, s(x1167), x425)≥COND2(gr(s(x1167), x425), s(x1167), x425))
(125) (0=x1163∧p(x1163)=s(x1165)∧0=x1152∧gr(x425, x1152)=true ⇒ COND1(true, s(x1165), x425)≥COND2(gr(s(x1165), x425), s(x1165), x425))
(126) (x1171=s(x1165)∧0=s(x1171)∧0=x1152∧gr(x425, x1152)=true ⇒ COND1(true, s(x1165), x425)≥COND2(gr(s(x1165), x425), s(x1165), x425))
(127) (COND4(gr(x499, 0), x498, x499)=COND4(false, x500, x501)∧COND1(and(gr(x500, 0), gr(x501, 0)), x500, x501)=COND1(true, x502, x503) ⇒ COND1(true, x502, x503)≥COND2(gr(x502, x503), x502, x503))
(128) (0=x1172∧gr(x499, x1172)=false∧x499=x501∧0=x1175∧gr(x500, x1175)=x1173∧0=x1176∧gr(x501, x1176)=x1174∧and(x1173, x1174)=true ⇒ COND1(true, x500, x501)≥COND2(gr(x500, x501), x500, x501))
(129) (true=true∧0=x1172∧gr(x499, x1172)=false∧x499=x501∧0=x1175∧gr(x500, x1175)=true∧0=x1176∧gr(x501, x1176)=true ⇒ COND1(true, x500, x501)≥COND2(gr(x500, x501), x500, x501))
(130) (0=x1172∧gr(x499, x1172)=false∧x499=x501∧0=x1175∧gr(x500, x1175)=true∧0=x1176∧gr(x501, x1176)=true ⇒ COND1(true, x500, x501)≥COND2(gr(x500, x501), x500, x501))
(131) (false=false∧0=x1179∧0=x501∧0=x1175∧gr(x500, x1175)=true∧0=x1176∧gr(x501, x1176)=true ⇒ COND1(true, x500, x501)≥COND2(gr(x500, x501), x500, x501))
(132) (gr(x1182, x1181)=false∧0=s(x1181)∧s(x1182)=x501∧0=x1175∧gr(x500, x1175)=true∧0=x1176∧gr(x501, x1176)=true∧(∀x1183,x1184,x1185,x1186:gr(x1182, x1181)=false∧0=x1181∧x1182=x1183∧0=x1184∧gr(x1185, x1184)=true∧0=x1186∧gr(x1183, x1186)=true ⇒ COND1(true, x1185, x1183)≥COND2(gr(x1185, x1183), x1185, x1183)) ⇒ COND1(true, x500, x501)≥COND2(gr(x500, x501), x500, x501))
(133) (0=x501∧0=x1175∧gr(x500, x1175)=true∧0=x1176∧gr(x501, x1176)=true ⇒ COND1(true, x500, x501)≥COND2(gr(x500, x501), x500, x501))
(134) (true=true∧0=x501∧0=0∧0=x1176∧gr(x501, x1176)=true ⇒ COND1(true, s(x1188), x501)≥COND2(gr(s(x1188), x501), s(x1188), x501))
(135) (gr(x1190, x1189)=true∧0=x501∧0=s(x1189)∧0=x1176∧gr(x501, x1176)=true∧(∀x1191,x1192:gr(x1190, x1189)=true∧0=x1191∧0=x1189∧0=x1192∧gr(x1191, x1192)=true ⇒ COND1(true, x1190, x1191)≥COND2(gr(x1190, x1191), x1190, x1191)) ⇒ COND1(true, s(x1190), x501)≥COND2(gr(s(x1190), x501), s(x1190), x501))
(136) (0=x501∧0=x1176∧gr(x501, x1176)=true ⇒ COND1(true, s(x1188), x501)≥COND2(gr(s(x1188), x501), s(x1188), x501))
(137) (true=true∧0=s(x1194)∧0=0 ⇒ COND1(true, s(x1188), s(x1194))≥COND2(gr(s(x1188), s(x1194)), s(x1188), s(x1194)))
(138) (gr(x1196, x1195)=true∧0=s(x1196)∧0=s(x1195)∧(∀x1197:gr(x1196, x1195)=true∧0=x1196∧0=x1195 ⇒ COND1(true, s(x1197), x1196)≥COND2(gr(s(x1197), x1196), s(x1197), x1196)) ⇒ COND1(true, s(x1188), s(x1196))≥COND2(gr(s(x1188), s(x1196)), s(x1188), s(x1196)))
(139) (COND4(gr(x505, 0), x504, p(x505))=COND4(false, x506, x507)∧COND1(and(gr(x506, 0), gr(x507, 0)), x506, x507)=COND1(true, x508, x509) ⇒ COND1(true, x508, x509)≥COND2(gr(x508, x509), x508, x509))
(140) (0=x1198∧gr(x505, x1198)=false∧p(x505)=x507∧0=x1201∧gr(x506, x1201)=x1199∧0=x1202∧gr(x507, x1202)=x1200∧and(x1199, x1200)=true ⇒ COND1(true, x506, x507)≥COND2(gr(x506, x507), x506, x507))
(141) (true=true∧0=x1198∧gr(x505, x1198)=false∧p(x505)=x507∧0=x1201∧gr(x506, x1201)=true∧0=x1202∧gr(x507, x1202)=true ⇒ COND1(true, x506, x507)≥COND2(gr(x506, x507), x506, x507))
(142) (0=x1198∧gr(x505, x1198)=false∧p(x505)=x507∧0=x1201∧gr(x506, x1201)=true∧0=x1202∧gr(x507, x1202)=true ⇒ COND1(true, x506, x507)≥COND2(gr(x506, x507), x506, x507))
(143) (false=false∧0=x1205∧p(0)=x507∧0=x1201∧gr(x506, x1201)=true∧0=x1202∧gr(x507, x1202)=true ⇒ COND1(true, x506, x507)≥COND2(gr(x506, x507), x506, x507))
(144) (gr(x1208, x1207)=false∧0=s(x1207)∧p(s(x1208))=x507∧0=x1201∧gr(x506, x1201)=true∧0=x1202∧gr(x507, x1202)=true∧(∀x1209,x1210,x1211,x1212:gr(x1208, x1207)=false∧0=x1207∧p(x1208)=x1209∧0=x1210∧gr(x1211, x1210)=true∧0=x1212∧gr(x1209, x1212)=true ⇒ COND1(true, x1211, x1209)≥COND2(gr(x1211, x1209), x1211, x1209)) ⇒ COND1(true, x506, x507)≥COND2(gr(x506, x507), x506, x507))
(145) (0=x1213∧p(x1213)=x507∧0=x1201∧gr(x506, x1201)=true∧0=x1202∧gr(x507, x1202)=true ⇒ COND1(true, x506, x507)≥COND2(gr(x506, x507), x506, x507))
(146) (true=true∧0=x1213∧p(x1213)=x507∧0=0∧0=x1202∧gr(x507, x1202)=true ⇒ COND1(true, s(x1215), x507)≥COND2(gr(s(x1215), x507), s(x1215), x507))
(147) (gr(x1217, x1216)=true∧0=x1213∧p(x1213)=x507∧0=s(x1216)∧0=x1202∧gr(x507, x1202)=true∧(∀x1218,x1219,x1220:gr(x1217, x1216)=true∧0=x1218∧p(x1218)=x1219∧0=x1216∧0=x1220∧gr(x1219, x1220)=true ⇒ COND1(true, x1217, x1219)≥COND2(gr(x1217, x1219), x1217, x1219)) ⇒ COND1(true, s(x1217), x507)≥COND2(gr(s(x1217), x507), s(x1217), x507))
(148) (0=x1213∧p(x1213)=x507∧0=x1202∧gr(x507, x1202)=true ⇒ COND1(true, s(x1215), x507)≥COND2(gr(s(x1215), x507), s(x1215), x507))
(149) (true=true∧0=x1213∧p(x1213)=s(x1222)∧0=0 ⇒ COND1(true, s(x1215), s(x1222))≥COND2(gr(s(x1215), s(x1222)), s(x1215), s(x1222)))
(150) (gr(x1224, x1223)=true∧0=x1213∧p(x1213)=s(x1224)∧0=s(x1223)∧(∀x1225,x1226:gr(x1224, x1223)=true∧0=x1225∧p(x1225)=x1224∧0=x1223 ⇒ COND1(true, s(x1226), x1224)≥COND2(gr(s(x1226), x1224), s(x1226), x1224)) ⇒ COND1(true, s(x1215), s(x1224))≥COND2(gr(s(x1215), s(x1224)), s(x1215), s(x1224)))
(151) (0=x1213∧p(x1213)=s(x1222) ⇒ COND1(true, s(x1215), s(x1222))≥COND2(gr(s(x1215), s(x1222)), s(x1215), s(x1222)))
(152) (x1227=s(x1222)∧0=s(x1227) ⇒ COND1(true, s(x1215), s(x1222))≥COND2(gr(s(x1215), s(x1222)), s(x1215), s(x1222)))
(153) (COND1(and(gr(x568, 0), gr(x569, 0)), x568, x569)=COND1(true, x570, x571)∧COND2(gr(x570, x571), x570, x571)=COND2(false, x572, x573) ⇒ COND2(false, x572, x573)≥COND4(gr(x573, 0), x572, x573))
(154) (0=x1230∧gr(x568, x1230)=x1228∧0=x1231∧gr(x569, x1231)=x1229∧and(x1228, x1229)=true∧x568=x570∧x569=x571∧gr(x570, x571)=false ⇒ COND2(false, x570, x571)≥COND4(gr(x571, 0), x570, x571))
(155) (true=true∧0=x1230∧gr(x568, x1230)=true∧0=x1231∧gr(x569, x1231)=true∧x568=x570∧x569=x571∧gr(x570, x571)=false ⇒ COND2(false, x570, x571)≥COND4(gr(x571, 0), x570, x571))
(156) (0=x1230∧gr(x568, x1230)=true∧0=x1231∧gr(x569, x1231)=true∧x568=x570∧x569=x571∧gr(x570, x571)=false ⇒ COND2(false, x570, x571)≥COND4(gr(x571, 0), x570, x571))
(157) (false=false∧0=x1230∧gr(x568, x1230)=true∧0=x1231∧gr(x569, x1231)=true∧x568=0∧x569=x1234 ⇒ COND2(false, 0, x1234)≥COND4(gr(x1234, 0), 0, x1234))
(158) (gr(x1237, x1236)=false∧0=x1230∧gr(x568, x1230)=true∧0=x1231∧gr(x569, x1231)=true∧x568=s(x1237)∧x569=s(x1236)∧(∀x1238,x1239,x1240,x1241:gr(x1237, x1236)=false∧0=x1238∧gr(x1239, x1238)=true∧0=x1240∧gr(x1241, x1240)=true∧x1239=x1237∧x1241=x1236 ⇒ COND2(false, x1237, x1236)≥COND4(gr(x1236, 0), x1237, x1236)) ⇒ COND2(false, s(x1237), s(x1236))≥COND4(gr(s(x1236), 0), s(x1237), s(x1236)))
(159) (0=x1230∧0=x1242∧gr(x1242, x1230)=true∧0=x1231∧gr(x569, x1231)=true ⇒ COND2(false, 0, x569)≥COND4(gr(x569, 0), 0, x569))
(160) (gr(x1237, x1236)=false∧0=x1230∧s(x1237)=x1249∧gr(x1249, x1230)=true∧0=x1231∧s(x1236)=x1250∧gr(x1250, x1231)=true∧(∀x1238,x1239,x1240,x1241:gr(x1237, x1236)=false∧0=x1238∧gr(x1239, x1238)=true∧0=x1240∧gr(x1241, x1240)=true∧x1239=x1237∧x1241=x1236 ⇒ COND2(false, x1237, x1236)≥COND4(gr(x1236, 0), x1237, x1236)) ⇒ COND2(false, s(x1237), s(x1236))≥COND4(gr(s(x1236), 0), s(x1237), s(x1236)))
(161) (true=true∧0=0∧0=s(x1244)∧0=x1231∧gr(x569, x1231)=true ⇒ COND2(false, 0, x569)≥COND4(gr(x569, 0), 0, x569))
(162) (gr(x1246, x1245)=true∧0=s(x1245)∧0=s(x1246)∧0=x1231∧gr(x569, x1231)=true∧(∀x1247,x1248:gr(x1246, x1245)=true∧0=x1245∧0=x1246∧0=x1247∧gr(x1248, x1247)=true ⇒ COND2(false, 0, x1248)≥COND4(gr(x1248, 0), 0, x1248)) ⇒ COND2(false, 0, x569)≥COND4(gr(x569, 0), 0, x569))
(163) (true=true∧gr(x1237, x1236)=false∧0=0∧s(x1237)=s(x1252)∧0=x1231∧s(x1236)=x1250∧gr(x1250, x1231)=true∧(∀x1238,x1239,x1240,x1241:gr(x1237, x1236)=false∧0=x1238∧gr(x1239, x1238)=true∧0=x1240∧gr(x1241, x1240)=true∧x1239=x1237∧x1241=x1236 ⇒ COND2(false, x1237, x1236)≥COND4(gr(x1236, 0), x1237, x1236)) ⇒ COND2(false, s(x1237), s(x1236))≥COND4(gr(s(x1236), 0), s(x1237), s(x1236)))
(164) (gr(x1254, x1253)=true∧gr(x1237, x1236)=false∧0=s(x1253)∧s(x1237)=s(x1254)∧0=x1231∧s(x1236)=x1250∧gr(x1250, x1231)=true∧(∀x1238,x1239,x1240,x1241:gr(x1237, x1236)=false∧0=x1238∧gr(x1239, x1238)=true∧0=x1240∧gr(x1241, x1240)=true∧x1239=x1237∧x1241=x1236 ⇒ COND2(false, x1237, x1236)≥COND4(gr(x1236, 0), x1237, x1236))∧(∀x1255,x1256,x1257,x1258,x1259,x1260,x1261,x1262:gr(x1254, x1253)=true∧gr(x1255, x1256)=false∧0=x1253∧s(x1255)=x1254∧0=x1257∧s(x1256)=x1258∧gr(x1258, x1257)=true∧(∀x1259,x1260,x1261,x1262:gr(x1255, x1256)=false∧0=x1259∧gr(x1260, x1259)=true∧0=x1261∧gr(x1262, x1261)=true∧x1260=x1255∧x1262=x1256 ⇒ COND2(false, x1255, x1256)≥COND4(gr(x1256, 0), x1255, x1256)) ⇒ COND2(false, s(x1255), s(x1256))≥COND4(gr(s(x1256), 0), s(x1255), s(x1256))) ⇒ COND2(false, s(x1237), s(x1236))≥COND4(gr(s(x1236), 0), s(x1237), s(x1236)))
(165) (gr(x1237, x1236)=false∧0=x1231∧s(x1236)=x1250∧gr(x1250, x1231)=true∧(∀x1238,x1239,x1240,x1241:gr(x1237, x1236)=false∧0=x1238∧gr(x1239, x1238)=true∧0=x1240∧gr(x1241, x1240)=true∧x1239=x1237∧x1241=x1236 ⇒ COND2(false, x1237, x1236)≥COND4(gr(x1236, 0), x1237, x1236)) ⇒ COND2(false, s(x1237), s(x1236))≥COND4(gr(s(x1236), 0), s(x1237), s(x1236)))
(166) (true=true∧gr(x1237, x1236)=false∧0=0∧s(x1236)=s(x1264)∧(∀x1238,x1239,x1240,x1241:gr(x1237, x1236)=false∧0=x1238∧gr(x1239, x1238)=true∧0=x1240∧gr(x1241, x1240)=true∧x1239=x1237∧x1241=x1236 ⇒ COND2(false, x1237, x1236)≥COND4(gr(x1236, 0), x1237, x1236)) ⇒ COND2(false, s(x1237), s(x1236))≥COND4(gr(s(x1236), 0), s(x1237), s(x1236)))
(167) (gr(x1266, x1265)=true∧gr(x1237, x1236)=false∧0=s(x1265)∧s(x1236)=s(x1266)∧(∀x1238,x1239,x1240,x1241:gr(x1237, x1236)=false∧0=x1238∧gr(x1239, x1238)=true∧0=x1240∧gr(x1241, x1240)=true∧x1239=x1237∧x1241=x1236 ⇒ COND2(false, x1237, x1236)≥COND4(gr(x1236, 0), x1237, x1236))∧(∀x1267,x1268,x1269,x1270,x1271,x1272:gr(x1266, x1265)=true∧gr(x1267, x1268)=false∧0=x1265∧s(x1268)=x1266∧(∀x1269,x1270,x1271,x1272:gr(x1267, x1268)=false∧0=x1269∧gr(x1270, x1269)=true∧0=x1271∧gr(x1272, x1271)=true∧x1270=x1267∧x1272=x1268 ⇒ COND2(false, x1267, x1268)≥COND4(gr(x1268, 0), x1267, x1268)) ⇒ COND2(false, s(x1267), s(x1268))≥COND4(gr(s(x1268), 0), s(x1267), s(x1268))) ⇒ COND2(false, s(x1237), s(x1236))≥COND4(gr(s(x1236), 0), s(x1237), s(x1236)))
(168) (gr(x1237, x1236)=false ⇒ COND2(false, s(x1237), s(x1236))≥COND4(gr(s(x1236), 0), s(x1237), s(x1236)))
(169) (false=false ⇒ COND2(false, s(0), s(x1273))≥COND4(gr(s(x1273), 0), s(0), s(x1273)))
(170) (gr(x1276, x1275)=false∧(gr(x1276, x1275)=false ⇒ COND2(false, s(x1276), s(x1275))≥COND4(gr(s(x1275), 0), s(x1276), s(x1275))) ⇒ COND2(false, s(s(x1276)), s(s(x1275)))≥COND4(gr(s(s(x1275)), 0), s(s(x1276)), s(s(x1275))))
(171) (COND2(false, s(0), s(x1273))≥COND4(gr(s(x1273), 0), s(0), s(x1273)))
(172) (COND2(false, s(x1276), s(x1275))≥COND4(gr(s(x1275), 0), s(x1276), s(x1275)) ⇒ COND2(false, s(s(x1276)), s(s(x1275)))≥COND4(gr(s(s(x1275)), 0), s(s(x1276)), s(s(x1275))))
(173) (COND1(and(gr(x580, 0), gr(x581, 0)), x580, x581)=COND1(true, x582, x583)∧COND2(gr(x582, x583), x582, x583)=COND2(false, x584, x585) ⇒ COND2(false, x584, x585)≥COND4(gr(x585, 0), x584, x585))
(174) (0=x1279∧gr(x580, x1279)=x1277∧0=x1280∧gr(x581, x1280)=x1278∧and(x1277, x1278)=true∧x580=x582∧x581=x583∧gr(x582, x583)=false ⇒ COND2(false, x582, x583)≥COND4(gr(x583, 0), x582, x583))
(175) (true=true∧0=x1279∧gr(x580, x1279)=true∧0=x1280∧gr(x581, x1280)=true∧x580=x582∧x581=x583∧gr(x582, x583)=false ⇒ COND2(false, x582, x583)≥COND4(gr(x583, 0), x582, x583))
(176) (0=x1279∧gr(x580, x1279)=true∧0=x1280∧gr(x581, x1280)=true∧x580=x582∧x581=x583∧gr(x582, x583)=false ⇒ COND2(false, x582, x583)≥COND4(gr(x583, 0), x582, x583))
(177) (false=false∧0=x1279∧gr(x580, x1279)=true∧0=x1280∧gr(x581, x1280)=true∧x580=0∧x581=x1283 ⇒ COND2(false, 0, x1283)≥COND4(gr(x1283, 0), 0, x1283))
(178) (gr(x1286, x1285)=false∧0=x1279∧gr(x580, x1279)=true∧0=x1280∧gr(x581, x1280)=true∧x580=s(x1286)∧x581=s(x1285)∧(∀x1287,x1288,x1289,x1290:gr(x1286, x1285)=false∧0=x1287∧gr(x1288, x1287)=true∧0=x1289∧gr(x1290, x1289)=true∧x1288=x1286∧x1290=x1285 ⇒ COND2(false, x1286, x1285)≥COND4(gr(x1285, 0), x1286, x1285)) ⇒ COND2(false, s(x1286), s(x1285))≥COND4(gr(s(x1285), 0), s(x1286), s(x1285)))
(179) (0=x1279∧0=x1291∧gr(x1291, x1279)=true∧0=x1280∧gr(x581, x1280)=true ⇒ COND2(false, 0, x581)≥COND4(gr(x581, 0), 0, x581))
(180) (gr(x1286, x1285)=false∧0=x1279∧s(x1286)=x1298∧gr(x1298, x1279)=true∧0=x1280∧s(x1285)=x1299∧gr(x1299, x1280)=true∧(∀x1287,x1288,x1289,x1290:gr(x1286, x1285)=false∧0=x1287∧gr(x1288, x1287)=true∧0=x1289∧gr(x1290, x1289)=true∧x1288=x1286∧x1290=x1285 ⇒ COND2(false, x1286, x1285)≥COND4(gr(x1285, 0), x1286, x1285)) ⇒ COND2(false, s(x1286), s(x1285))≥COND4(gr(s(x1285), 0), s(x1286), s(x1285)))
(181) (true=true∧0=0∧0=s(x1293)∧0=x1280∧gr(x581, x1280)=true ⇒ COND2(false, 0, x581)≥COND4(gr(x581, 0), 0, x581))
(182) (gr(x1295, x1294)=true∧0=s(x1294)∧0=s(x1295)∧0=x1280∧gr(x581, x1280)=true∧(∀x1296,x1297:gr(x1295, x1294)=true∧0=x1294∧0=x1295∧0=x1296∧gr(x1297, x1296)=true ⇒ COND2(false, 0, x1297)≥COND4(gr(x1297, 0), 0, x1297)) ⇒ COND2(false, 0, x581)≥COND4(gr(x581, 0), 0, x581))
(183) (true=true∧gr(x1286, x1285)=false∧0=0∧s(x1286)=s(x1301)∧0=x1280∧s(x1285)=x1299∧gr(x1299, x1280)=true∧(∀x1287,x1288,x1289,x1290:gr(x1286, x1285)=false∧0=x1287∧gr(x1288, x1287)=true∧0=x1289∧gr(x1290, x1289)=true∧x1288=x1286∧x1290=x1285 ⇒ COND2(false, x1286, x1285)≥COND4(gr(x1285, 0), x1286, x1285)) ⇒ COND2(false, s(x1286), s(x1285))≥COND4(gr(s(x1285), 0), s(x1286), s(x1285)))
(184) (gr(x1303, x1302)=true∧gr(x1286, x1285)=false∧0=s(x1302)∧s(x1286)=s(x1303)∧0=x1280∧s(x1285)=x1299∧gr(x1299, x1280)=true∧(∀x1287,x1288,x1289,x1290:gr(x1286, x1285)=false∧0=x1287∧gr(x1288, x1287)=true∧0=x1289∧gr(x1290, x1289)=true∧x1288=x1286∧x1290=x1285 ⇒ COND2(false, x1286, x1285)≥COND4(gr(x1285, 0), x1286, x1285))∧(∀x1304,x1305,x1306,x1307,x1308,x1309,x1310,x1311:gr(x1303, x1302)=true∧gr(x1304, x1305)=false∧0=x1302∧s(x1304)=x1303∧0=x1306∧s(x1305)=x1307∧gr(x1307, x1306)=true∧(∀x1308,x1309,x1310,x1311:gr(x1304, x1305)=false∧0=x1308∧gr(x1309, x1308)=true∧0=x1310∧gr(x1311, x1310)=true∧x1309=x1304∧x1311=x1305 ⇒ COND2(false, x1304, x1305)≥COND4(gr(x1305, 0), x1304, x1305)) ⇒ COND2(false, s(x1304), s(x1305))≥COND4(gr(s(x1305), 0), s(x1304), s(x1305))) ⇒ COND2(false, s(x1286), s(x1285))≥COND4(gr(s(x1285), 0), s(x1286), s(x1285)))
(185) (gr(x1286, x1285)=false∧0=x1280∧s(x1285)=x1299∧gr(x1299, x1280)=true∧(∀x1287,x1288,x1289,x1290:gr(x1286, x1285)=false∧0=x1287∧gr(x1288, x1287)=true∧0=x1289∧gr(x1290, x1289)=true∧x1288=x1286∧x1290=x1285 ⇒ COND2(false, x1286, x1285)≥COND4(gr(x1285, 0), x1286, x1285)) ⇒ COND2(false, s(x1286), s(x1285))≥COND4(gr(s(x1285), 0), s(x1286), s(x1285)))
(186) (true=true∧gr(x1286, x1285)=false∧0=0∧s(x1285)=s(x1313)∧(∀x1287,x1288,x1289,x1290:gr(x1286, x1285)=false∧0=x1287∧gr(x1288, x1287)=true∧0=x1289∧gr(x1290, x1289)=true∧x1288=x1286∧x1290=x1285 ⇒ COND2(false, x1286, x1285)≥COND4(gr(x1285, 0), x1286, x1285)) ⇒ COND2(false, s(x1286), s(x1285))≥COND4(gr(s(x1285), 0), s(x1286), s(x1285)))
(187) (gr(x1315, x1314)=true∧gr(x1286, x1285)=false∧0=s(x1314)∧s(x1285)=s(x1315)∧(∀x1287,x1288,x1289,x1290:gr(x1286, x1285)=false∧0=x1287∧gr(x1288, x1287)=true∧0=x1289∧gr(x1290, x1289)=true∧x1288=x1286∧x1290=x1285 ⇒ COND2(false, x1286, x1285)≥COND4(gr(x1285, 0), x1286, x1285))∧(∀x1316,x1317,x1318,x1319,x1320,x1321:gr(x1315, x1314)=true∧gr(x1316, x1317)=false∧0=x1314∧s(x1317)=x1315∧(∀x1318,x1319,x1320,x1321:gr(x1316, x1317)=false∧0=x1318∧gr(x1319, x1318)=true∧0=x1320∧gr(x1321, x1320)=true∧x1319=x1316∧x1321=x1317 ⇒ COND2(false, x1316, x1317)≥COND4(gr(x1317, 0), x1316, x1317)) ⇒ COND2(false, s(x1316), s(x1317))≥COND4(gr(s(x1317), 0), s(x1316), s(x1317))) ⇒ COND2(false, s(x1286), s(x1285))≥COND4(gr(s(x1285), 0), s(x1286), s(x1285)))
(188) (gr(x1286, x1285)=false ⇒ COND2(false, s(x1286), s(x1285))≥COND4(gr(s(x1285), 0), s(x1286), s(x1285)))
(189) (false=false ⇒ COND2(false, s(0), s(x1322))≥COND4(gr(s(x1322), 0), s(0), s(x1322)))
(190) (gr(x1325, x1324)=false∧(gr(x1325, x1324)=false ⇒ COND2(false, s(x1325), s(x1324))≥COND4(gr(s(x1324), 0), s(x1325), s(x1324))) ⇒ COND2(false, s(s(x1325)), s(s(x1324)))≥COND4(gr(s(s(x1324)), 0), s(s(x1325)), s(s(x1324))))
(191) (COND2(false, s(0), s(x1322))≥COND4(gr(s(x1322), 0), s(0), s(x1322)))
(192) (COND2(false, s(x1325), s(x1324))≥COND4(gr(s(x1324), 0), s(x1325), s(x1324)) ⇒ COND2(false, s(s(x1325)), s(s(x1324)))≥COND4(gr(s(s(x1324)), 0), s(s(x1325)), s(s(x1324))))
(193) (COND2(gr(x714, x715), x714, x715)=COND2(false, x716, x717)∧COND4(gr(x717, 0), x716, x717)=COND4(true, x718, x719) ⇒ COND4(true, x718, x719)≥COND4(gr(x719, 0), x718, p(x719)))
(194) (gr(x714, x715)=false∧x715=x717∧0=x1326∧gr(x717, x1326)=true ⇒ COND4(true, x714, x717)≥COND4(gr(x717, 0), x714, p(x717)))
(195) (false=false∧x1327=x717∧0=x1326∧gr(x717, x1326)=true ⇒ COND4(true, 0, x717)≥COND4(gr(x717, 0), 0, p(x717)))
(196) (gr(x1330, x1329)=false∧s(x1329)=x717∧0=x1326∧gr(x717, x1326)=true∧(∀x1331,x1332:gr(x1330, x1329)=false∧x1329=x1331∧0=x1332∧gr(x1331, x1332)=true ⇒ COND4(true, x1330, x1331)≥COND4(gr(x1331, 0), x1330, p(x1331))) ⇒ COND4(true, s(x1330), x717)≥COND4(gr(x717, 0), s(x1330), p(x717)))
(197) (0=x1326∧gr(x717, x1326)=true ⇒ COND4(true, 0, x717)≥COND4(gr(x717, 0), 0, p(x717)))
(198) (true=true∧gr(x1330, x1329)=false∧s(x1329)=s(x1338)∧0=0∧(∀x1331,x1332:gr(x1330, x1329)=false∧x1329=x1331∧0=x1332∧gr(x1331, x1332)=true ⇒ COND4(true, x1330, x1331)≥COND4(gr(x1331, 0), x1330, p(x1331))) ⇒ COND4(true, s(x1330), s(x1338))≥COND4(gr(s(x1338), 0), s(x1330), p(s(x1338))))
(199) (gr(x1340, x1339)=true∧gr(x1330, x1329)=false∧s(x1329)=s(x1340)∧0=s(x1339)∧(∀x1331,x1332:gr(x1330, x1329)=false∧x1329=x1331∧0=x1332∧gr(x1331, x1332)=true ⇒ COND4(true, x1330, x1331)≥COND4(gr(x1331, 0), x1330, p(x1331)))∧(∀x1341,x1342,x1343,x1344:gr(x1340, x1339)=true∧gr(x1341, x1342)=false∧s(x1342)=x1340∧0=x1339∧(∀x1343,x1344:gr(x1341, x1342)=false∧x1342=x1343∧0=x1344∧gr(x1343, x1344)=true ⇒ COND4(true, x1341, x1343)≥COND4(gr(x1343, 0), x1341, p(x1343))) ⇒ COND4(true, s(x1341), x1340)≥COND4(gr(x1340, 0), s(x1341), p(x1340))) ⇒ COND4(true, s(x1330), s(x1340))≥COND4(gr(s(x1340), 0), s(x1330), p(s(x1340))))
(200) (true=true∧0=0 ⇒ COND4(true, 0, s(x1334))≥COND4(gr(s(x1334), 0), 0, p(s(x1334))))
(201) (gr(x1336, x1335)=true∧0=s(x1335)∧(gr(x1336, x1335)=true∧0=x1335 ⇒ COND4(true, 0, x1336)≥COND4(gr(x1336, 0), 0, p(x1336))) ⇒ COND4(true, 0, s(x1336))≥COND4(gr(s(x1336), 0), 0, p(s(x1336))))
(202) (COND4(true, 0, s(x1334))≥COND4(gr(s(x1334), 0), 0, p(s(x1334))))
(203) (gr(x1330, x1329)=false ⇒ COND4(true, s(x1330), s(x1329))≥COND4(gr(s(x1329), 0), s(x1330), p(s(x1329))))
(204) (false=false ⇒ COND4(true, s(0), s(x1345))≥COND4(gr(s(x1345), 0), s(0), p(s(x1345))))
(205) (gr(x1348, x1347)=false∧(gr(x1348, x1347)=false ⇒ COND4(true, s(x1348), s(x1347))≥COND4(gr(s(x1347), 0), s(x1348), p(s(x1347)))) ⇒ COND4(true, s(s(x1348)), s(s(x1347)))≥COND4(gr(s(s(x1347)), 0), s(s(x1348)), p(s(s(x1347)))))
(206) (COND4(true, s(0), s(x1345))≥COND4(gr(s(x1345), 0), s(0), p(s(x1345))))
(207) (COND4(true, s(x1348), s(x1347))≥COND4(gr(s(x1347), 0), s(x1348), p(s(x1347))) ⇒ COND4(true, s(s(x1348)), s(s(x1347)))≥COND4(gr(s(s(x1347)), 0), s(s(x1348)), p(s(s(x1347)))))
(208) (COND4(gr(x735, 0), x734, x735)=COND4(true, x736, x737)∧COND4(gr(x737, 0), x736, p(x737))=COND4(true, x738, x739) ⇒ COND4(true, x738, x739)≥COND4(gr(x739, 0), x738, p(x739)))
(209) (0=x1349∧gr(x735, x1349)=true∧x735=x737∧0=x1350∧gr(x737, x1350)=true∧p(x737)=x739 ⇒ COND4(true, x734, x739)≥COND4(gr(x739, 0), x734, p(x739)))
(210) (true=true∧0=0∧s(x1352)=x737∧0=x1350∧gr(x737, x1350)=true∧p(x737)=x739 ⇒ COND4(true, x734, x739)≥COND4(gr(x739, 0), x734, p(x739)))
(211) (gr(x1354, x1353)=true∧0=s(x1353)∧s(x1354)=x737∧0=x1350∧gr(x737, x1350)=true∧p(x737)=x739∧(∀x1355,x1356,x1357,x1358:gr(x1354, x1353)=true∧0=x1353∧x1354=x1355∧0=x1356∧gr(x1355, x1356)=true∧p(x1355)=x1357 ⇒ COND4(true, x1358, x1357)≥COND4(gr(x1357, 0), x1358, p(x1357))) ⇒ COND4(true, x734, x739)≥COND4(gr(x739, 0), x734, p(x739)))
(212) (s(x1352)=x737∧0=x1350∧gr(x737, x1350)=true∧p(x737)=x739 ⇒ COND4(true, x734, x739)≥COND4(gr(x739, 0), x734, p(x739)))
(213) (true=true∧s(x1352)=s(x1360)∧0=0∧p(s(x1360))=x739 ⇒ COND4(true, x734, x739)≥COND4(gr(x739, 0), x734, p(x739)))
(214) (gr(x1362, x1361)=true∧s(x1352)=s(x1362)∧0=s(x1361)∧p(s(x1362))=x739∧(∀x1363,x1364,x1365:gr(x1362, x1361)=true∧s(x1363)=x1362∧0=x1361∧p(x1362)=x1364 ⇒ COND4(true, x1365, x1364)≥COND4(gr(x1364, 0), x1365, p(x1364))) ⇒ COND4(true, x734, x739)≥COND4(gr(x739, 0), x734, p(x739)))
(215) (COND4(true, x734, x739)≥COND4(gr(x739, 0), x734, p(x739)))
(216) (COND4(gr(x741, 0), x740, p(x741))=COND4(true, x742, x743)∧COND4(gr(x743, 0), x742, p(x743))=COND4(true, x744, x745) ⇒ COND4(true, x744, x745)≥COND4(gr(x745, 0), x744, p(x745)))
(217) (0=x1367∧gr(x741, x1367)=true∧p(x741)=x743∧0=x1368∧gr(x743, x1368)=true∧p(x743)=x745 ⇒ COND4(true, x740, x745)≥COND4(gr(x745, 0), x740, p(x745)))
(218) (true=true∧0=0∧p(s(x1370))=x743∧0=x1368∧gr(x743, x1368)=true∧p(x743)=x745 ⇒ COND4(true, x740, x745)≥COND4(gr(x745, 0), x740, p(x745)))
(219) (gr(x1372, x1371)=true∧0=s(x1371)∧p(s(x1372))=x743∧0=x1368∧gr(x743, x1368)=true∧p(x743)=x745∧(∀x1373,x1374,x1375,x1376:gr(x1372, x1371)=true∧0=x1371∧p(x1372)=x1373∧0=x1374∧gr(x1373, x1374)=true∧p(x1373)=x1375 ⇒ COND4(true, x1376, x1375)≥COND4(gr(x1375, 0), x1376, p(x1375))) ⇒ COND4(true, x740, x745)≥COND4(gr(x745, 0), x740, p(x745)))
(220) (s(x1370)=x1377∧p(x1377)=x743∧0=x1368∧gr(x743, x1368)=true∧p(x743)=x745 ⇒ COND4(true, x740, x745)≥COND4(gr(x745, 0), x740, p(x745)))
(221) (true=true∧s(x1370)=x1377∧p(x1377)=s(x1379)∧0=0∧p(s(x1379))=x745 ⇒ COND4(true, x740, x745)≥COND4(gr(x745, 0), x740, p(x745)))
(222) (gr(x1381, x1380)=true∧s(x1370)=x1377∧p(x1377)=s(x1381)∧0=s(x1380)∧p(s(x1381))=x745∧(∀x1382,x1383,x1384,x1385:gr(x1381, x1380)=true∧s(x1382)=x1383∧p(x1383)=x1381∧0=x1380∧p(x1381)=x1384 ⇒ COND4(true, x1385, x1384)≥COND4(gr(x1384, 0), x1385, p(x1384))) ⇒ COND4(true, x740, x745)≥COND4(gr(x745, 0), x740, p(x745)))
(223) (s(x1370)=x1377∧p(x1377)=s(x1379)∧s(x1379)=x1386∧p(x1386)=x745 ⇒ COND4(true, x740, x745)≥COND4(gr(x745, 0), x740, p(x745)))
(224) (x1387=s(x1379)∧s(x1370)=s(x1387)∧s(x1379)=x1386∧p(x1386)=x745 ⇒ COND4(true, x740, x745)≥COND4(gr(x745, 0), x740, p(x745)))
(225) (COND4(true, x740, x745)≥COND4(gr(x745, 0), x740, p(x745)))
(226) (COND2(gr(x842, x843), x842, x843)=COND2(false, x844, x845)∧COND4(gr(x845, 0), x844, x845)=COND4(false, x846, x847) ⇒ COND4(false, x846, x847)≥COND1(and(gr(x846, 0), gr(x847, 0)), x846, x847))
(227) (gr(x842, x843)=false∧x843=x845∧0=x1388∧gr(x845, x1388)=false ⇒ COND4(false, x842, x845)≥COND1(and(gr(x842, 0), gr(x845, 0)), x842, x845))
(228) (false=false∧x1389=x845∧0=x1388∧gr(x845, x1388)=false ⇒ COND4(false, 0, x845)≥COND1(and(gr(0, 0), gr(x845, 0)), 0, x845))
(229) (gr(x1392, x1391)=false∧s(x1391)=x845∧0=x1388∧gr(x845, x1388)=false∧(∀x1393,x1394:gr(x1392, x1391)=false∧x1391=x1393∧0=x1394∧gr(x1393, x1394)=false ⇒ COND4(false, x1392, x1393)≥COND1(and(gr(x1392, 0), gr(x1393, 0)), x1392, x1393)) ⇒ COND4(false, s(x1392), x845)≥COND1(and(gr(s(x1392), 0), gr(x845, 0)), s(x1392), x845))
(230) (0=x1388∧gr(x845, x1388)=false ⇒ COND4(false, 0, x845)≥COND1(and(gr(0, 0), gr(x845, 0)), 0, x845))
(231) (false=false∧gr(x1392, x1391)=false∧s(x1391)=0∧0=x1399∧(∀x1393,x1394:gr(x1392, x1391)=false∧x1391=x1393∧0=x1394∧gr(x1393, x1394)=false ⇒ COND4(false, x1392, x1393)≥COND1(and(gr(x1392, 0), gr(x1393, 0)), x1392, x1393)) ⇒ COND4(false, s(x1392), 0)≥COND1(and(gr(s(x1392), 0), gr(0, 0)), s(x1392), 0))
(232) (gr(x1402, x1401)=false∧gr(x1392, x1391)=false∧s(x1391)=s(x1402)∧0=s(x1401)∧(∀x1393,x1394:gr(x1392, x1391)=false∧x1391=x1393∧0=x1394∧gr(x1393, x1394)=false ⇒ COND4(false, x1392, x1393)≥COND1(and(gr(x1392, 0), gr(x1393, 0)), x1392, x1393))∧(∀x1403,x1404,x1405,x1406:gr(x1402, x1401)=false∧gr(x1403, x1404)=false∧s(x1404)=x1402∧0=x1401∧(∀x1405,x1406:gr(x1403, x1404)=false∧x1404=x1405∧0=x1406∧gr(x1405, x1406)=false ⇒ COND4(false, x1403, x1405)≥COND1(and(gr(x1403, 0), gr(x1405, 0)), x1403, x1405)) ⇒ COND4(false, s(x1403), x1402)≥COND1(and(gr(s(x1403), 0), gr(x1402, 0)), s(x1403), x1402)) ⇒ COND4(false, s(x1392), s(x1402))≥COND1(and(gr(s(x1392), 0), gr(s(x1402), 0)), s(x1392), s(x1402)))
(233) (false=false∧0=x1395 ⇒ COND4(false, 0, 0)≥COND1(and(gr(0, 0), gr(0, 0)), 0, 0))
(234) (gr(x1398, x1397)=false∧0=s(x1397)∧(gr(x1398, x1397)=false∧0=x1397 ⇒ COND4(false, 0, x1398)≥COND1(and(gr(0, 0), gr(x1398, 0)), 0, x1398)) ⇒ COND4(false, 0, s(x1398))≥COND1(and(gr(0, 0), gr(s(x1398), 0)), 0, s(x1398)))
(235) (COND4(false, 0, 0)≥COND1(and(gr(0, 0), gr(0, 0)), 0, 0))
(236) (COND4(gr(x863, 0), x862, x863)=COND4(true, x864, x865)∧COND4(gr(x865, 0), x864, p(x865))=COND4(false, x866, x867) ⇒ COND4(false, x866, x867)≥COND1(and(gr(x866, 0), gr(x867, 0)), x866, x867))
(237) (0=x1407∧gr(x863, x1407)=true∧x863=x865∧0=x1408∧gr(x865, x1408)=false∧p(x865)=x867 ⇒ COND4(false, x862, x867)≥COND1(and(gr(x862, 0), gr(x867, 0)), x862, x867))
(238) (true=true∧0=0∧s(x1410)=x865∧0=x1408∧gr(x865, x1408)=false∧p(x865)=x867 ⇒ COND4(false, x862, x867)≥COND1(and(gr(x862, 0), gr(x867, 0)), x862, x867))
(239) (gr(x1412, x1411)=true∧0=s(x1411)∧s(x1412)=x865∧0=x1408∧gr(x865, x1408)=false∧p(x865)=x867∧(∀x1413,x1414,x1415,x1416:gr(x1412, x1411)=true∧0=x1411∧x1412=x1413∧0=x1414∧gr(x1413, x1414)=false∧p(x1413)=x1415 ⇒ COND4(false, x1416, x1415)≥COND1(and(gr(x1416, 0), gr(x1415, 0)), x1416, x1415)) ⇒ COND4(false, x862, x867)≥COND1(and(gr(x862, 0), gr(x867, 0)), x862, x867))
(240) (s(x1410)=x865∧0=x1408∧gr(x865, x1408)=false∧p(x865)=x867 ⇒ COND4(false, x862, x867)≥COND1(and(gr(x862, 0), gr(x867, 0)), x862, x867))
(241) (false=false∧s(x1410)=0∧0=x1417∧p(0)=x867 ⇒ COND4(false, x862, x867)≥COND1(and(gr(x862, 0), gr(x867, 0)), x862, x867))
(242) (gr(x1420, x1419)=false∧s(x1410)=s(x1420)∧0=s(x1419)∧p(s(x1420))=x867∧(∀x1421,x1422,x1423:gr(x1420, x1419)=false∧s(x1421)=x1420∧0=x1419∧p(x1420)=x1422 ⇒ COND4(false, x1423, x1422)≥COND1(and(gr(x1423, 0), gr(x1422, 0)), x1423, x1422)) ⇒ COND4(false, x862, x867)≥COND1(and(gr(x862, 0), gr(x867, 0)), x862, x867))
(243) (COND4(gr(x869, 0), x868, p(x869))=COND4(true, x870, x871)∧COND4(gr(x871, 0), x870, p(x871))=COND4(false, x872, x873) ⇒ COND4(false, x872, x873)≥COND1(and(gr(x872, 0), gr(x873, 0)), x872, x873))
(244) (0=x1424∧gr(x869, x1424)=true∧p(x869)=x871∧0=x1425∧gr(x871, x1425)=false∧p(x871)=x873 ⇒ COND4(false, x868, x873)≥COND1(and(gr(x868, 0), gr(x873, 0)), x868, x873))
(245) (true=true∧0=0∧p(s(x1427))=x871∧0=x1425∧gr(x871, x1425)=false∧p(x871)=x873 ⇒ COND4(false, x868, x873)≥COND1(and(gr(x868, 0), gr(x873, 0)), x868, x873))
(246) (gr(x1429, x1428)=true∧0=s(x1428)∧p(s(x1429))=x871∧0=x1425∧gr(x871, x1425)=false∧p(x871)=x873∧(∀x1430,x1431,x1432,x1433:gr(x1429, x1428)=true∧0=x1428∧p(x1429)=x1430∧0=x1431∧gr(x1430, x1431)=false∧p(x1430)=x1432 ⇒ COND4(false, x1433, x1432)≥COND1(and(gr(x1433, 0), gr(x1432, 0)), x1433, x1432)) ⇒ COND4(false, x868, x873)≥COND1(and(gr(x868, 0), gr(x873, 0)), x868, x873))
(247) (s(x1427)=x1434∧p(x1434)=x871∧0=x1425∧gr(x871, x1425)=false∧p(x871)=x873 ⇒ COND4(false, x868, x873)≥COND1(and(gr(x868, 0), gr(x873, 0)), x868, x873))
(248) (false=false∧s(x1427)=x1434∧p(x1434)=0∧0=x1435∧p(0)=x873 ⇒ COND4(false, x868, x873)≥COND1(and(gr(x868, 0), gr(x873, 0)), x868, x873))
(249) (gr(x1438, x1437)=false∧s(x1427)=x1434∧p(x1434)=s(x1438)∧0=s(x1437)∧p(s(x1438))=x873∧(∀x1439,x1440,x1441,x1442:gr(x1438, x1437)=false∧s(x1439)=x1440∧p(x1440)=x1438∧0=x1437∧p(x1438)=x1441 ⇒ COND4(false, x1442, x1441)≥COND1(and(gr(x1442, 0), gr(x1441, 0)), x1442, x1441)) ⇒ COND4(false, x868, x873)≥COND1(and(gr(x868, 0), gr(x873, 0)), x868, x873))
(250) (s(x1427)=x1434∧p(x1434)=0∧0=x1443∧p(x1443)=x873 ⇒ COND4(false, x868, x873)≥COND1(and(gr(x868, 0), gr(x873, 0)), x868, x873))
(251) (0=0∧s(x1427)=0∧0=x1443∧p(x1443)=x873 ⇒ COND4(false, x868, x873)≥COND1(and(gr(x868, 0), gr(x873, 0)), x868, x873))
(252) (x1444=0∧s(x1427)=s(x1444)∧0=x1443∧p(x1443)=x873 ⇒ COND4(false, x868, x873)≥COND1(and(gr(x868, 0), gr(x873, 0)), x868, x873))
(253) (COND4(false, x868, x873)≥COND1(and(gr(x868, 0), gr(x873, 0)), x868, x873))
POL(0) = 0
POL(COND1(x1, x2, x3)) = -1 + 2·x2·x3 + x22 + x32
POL(COND2(x1, x2, x3)) = 1 - 2·x2·x3 + x22 + x32
POL(COND3(x1, x2, x3)) = 2·x2·x3 + x22 + x32
POL(COND4(x1, x2, x3)) = 2·x2·x3 + x22 + x32
POL(and(x1, x2)) = 0
POL(c) = -1
POL(false) = 0
POL(gr(x1, x2)) = x1
POL(p(x1)) = x1
POL(s(x1)) = x1
POL(true) = 0
The following pairs are in Pbound:
COND2(true, x, y) → COND3(gr(x, 0), x, y)
COND3(false, x, y) → COND1(and(gr(x, 0), gr(y, 0)), x, y)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, x, y) → COND4(gr(y, 0), x, y)
COND4(false, x, y) → COND1(and(gr(x, 0), gr(y, 0)), x, y)
The following rules are usable:
COND2(true, x, y) → COND3(gr(x, 0), x, y)
COND3(true, x, y) → COND3(gr(x, 0), p(x), y)
COND3(false, x, y) → COND1(and(gr(x, 0), gr(y, 0)), x, y)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, x, y) → COND4(gr(y, 0), x, y)
COND4(true, x, y) → COND4(gr(y, 0), x, p(y))
COND4(false, x, y) → COND1(and(gr(x, 0), gr(y, 0)), x, y)
p(s(x)) → x
p(0) → 0
COND3(true, x, y) → COND3(gr(x, 0), p(x), y)
COND4(true, x, y) → COND4(gr(y, 0), x, p(y))
gr(0, x) → false
gr(s(x), 0) → true
and(true, true) → true
and(false, x) → false
and(x, false) → false
p(0) → 0
p(s(x)) → x
gr(s(x), s(y)) → gr(x, y)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
p(0)
p(s(x0))
COND4(true, x, y) → COND4(gr(y, 0), x, p(y))
gr(0, x) → false
gr(s(x), 0) → true
and(true, true) → true
and(false, x) → false
and(x, false) → false
p(0) → 0
p(s(x)) → x
gr(s(x), s(y)) → gr(x, y)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
p(0)
p(s(x0))
COND4(true, x, y) → COND4(gr(y, 0), x, p(y))
gr(0, x) → false
gr(s(x), 0) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
p(0)
p(s(x0))
and(true, true)
and(false, x0)
and(x0, false)
COND4(true, x, y) → COND4(gr(y, 0), x, p(y))
gr(0, x) → false
gr(s(x), 0) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
COND4(true, x, y) → COND4(gr(y, 0), x, p(y))
The value of delta used in the strict ordering is 2.
POL(COND4(x1, x2, x3)) = (2)x1 + x3
POL(true) = 1
POL(gr(x1, x2)) = (1/4)x1
POL(0) = 0
POL(p(x1)) = (1/2)x1
POL(false) = 0
POL(s(x1)) = 4 + (2)x1
gr(0, x) → false
gr(s(x), 0) → true
p(0) → 0
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
COND3(true, x, y) → COND3(gr(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
and(true, true) → true
and(false, x) → false
and(x, false) → false
p(0) → 0
p(s(x)) → x
gr(s(x), s(y)) → gr(x, y)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
p(0)
p(s(x0))
COND3(true, x, y) → COND3(gr(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
p(0)
p(s(x0))
and(true, true)
and(false, x0)
and(x0, false)
COND3(true, x, y) → COND3(gr(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
COND3(true, x, y) → COND3(gr(x, 0), p(x), y)
The value of delta used in the strict ordering is 4.
POL(COND3(x1, x2, x3)) = x1 + (4)x2
POL(true) = 4
POL(gr(x1, x2)) = (2)x1
POL(0) = 0
POL(p(x1)) = (1/4)x1
POL(s(x1)) = 2 + (4)x1
POL(false) = 0
p(0) → 0
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
gr(0, x) → false
gr(s(x), 0) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))