Problem: +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(x,p(y)) -> p(+(x,y)) +(0(),y) -> y +(s(x),y) -> s(+(x,y)) +(p(x),y) -> p(+(x,y)) s(p(x)) -> x p(s(x)) -> x -(0()) -> 0() -(s(x)) -> p(-(x)) -(p(x)) -> s(-(x)) +(x,y) -> +(y,x) -(+(x,y)) -> +(-(x),-(y)) Proof: Church Rosser Transformation Processor (star): strict: weak: -(0)(+(0)(x)) -> +(0)(-(0)(x)) -(0)(+(1)(y)) -> +(1)(-(0)(y)) +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) -(0)(p(0)(x)) -> s(0)(-(0)(x)) -(0)(s(0)(x)) -> p(0)(-(0)(x)) p(0)(s(0)(x)) -> x s(0)(p(0)(x)) -> x +(0)(p(0)(x)) -> p(0)(+(0)(x)) +(1)(y) -> p(0)(+(1)(y)) +(0)(s(0)(x)) -> s(0)(+(0)(x)) +(1)(y) -> s(0)(+(1)(y)) +(1)(y) -> y +(0)(x) -> p(0)(+(0)(x)) +(1)(p(0)(y)) -> p(0)(+(1)(y)) +(0)(x) -> s(0)(+(0)(x)) +(1)(s(0)(y)) -> s(0)(+(1)(y)) +(0)(x) -> x critical peaks: 45 0() <-0|[]- +(0(),0()) -3|[]-> 0() s(x) <-0|[]- +(s(x),0()) -4|[]-> s(+(x,0())) p(x) <-0|[]- +(p(x),0()) -5|[]-> p(+(x,0())) x <-0|[]- +(x,0()) -11|[]-> +(0(),x) -(x) <-0|0[]- -(+(x,0())) -12|[]-> +(-(x),-(0())) s(+(0(),x459)) <-1|[]- +(0(),s(x459)) -3|[]-> s(x459) s(+(s(x),x461)) <-1|[]- +(s(x),s(x461)) -4|[]-> s(+(x,s(x461))) s(+(p(x),x463)) <-1|[]- +(p(x),s(x463)) -5|[]-> p(+(x,s(x463))) s(+(x,x465)) <-1|[]- +(x,s(x465)) -11|[]-> +(s(x465),x) -(s(+(x,x467))) <-1|0[]- -(+(x,s(x467))) -12|[]-> +(-(x),-(s(x467))) p(+(0(),x469)) <-2|[]- +(0(),p(x469)) -3|[]-> p(x469) p(+(s(x),x471)) <-2|[]- +(s(x),p(x471)) -4|[]-> s(+(x,p(x471))) p(+(p(x),x473)) <-2|[]- +(p(x),p(x473)) -5|[]-> p(+(x,p(x473))) p(+(x,x475)) <-2|[]- +(x,p(x475)) -11|[]-> +(p(x475),x) -(p(+(x,x477))) <-2|0[]- -(+(x,p(x477))) -12|[]-> +(-(x),-(p(x477))) 0() <-3|[]- +(0(),0()) -0|[]-> 0() s(y) <-3|[]- +(0(),s(y)) -1|[]-> s(+(0(),y)) p(y) <-3|[]- +(0(),p(y)) -2|[]-> p(+(0(),y)) y <-3|[]- +(0(),y) -11|[]-> +(y,0()) -(y) <-3|0[]- -(+(0(),y)) -12|[]-> +(-(0()),-(y)) s(+(x483,0())) <-4|[]- +(s(x483),0()) -0|[]-> s(x483) s(+(x485,s(y))) <-4|[]- +(s(x485),s(y)) -1|[]-> s(+(s(x485),y)) s(+(x487,p(y))) <-4|[]- +(s(x487),p(y)) -2|[]-> p(+(s(x487),y)) s(+(x489,y)) <-4|[]- +(s(x489),y) -11|[]-> +(y,s(x489)) -(s(+(x491,y))) <-4|0[]- -(+(s(x491),y)) -12|[]-> +(-(s(x491)),-(y)) p(+(x493,0())) <-5|[]- +(p(x493),0()) -0|[]-> p(x493) p(+(x495,s(y))) <-5|[]- +(p(x495),s(y)) -1|[]-> s(+(p(x495),y)) p(+(x497,p(y))) <-5|[]- +(p(x497),p(y)) -2|[]-> p(+(p(x497),y)) p(+(x499,y)) <-5|[]- +(p(x499),y) -11|[]-> +(y,p(x499)) -(p(+(x501,y))) <-5|0[]- -(+(p(x501),y)) -12|[]-> +(-(p(x501)),-(y)) +(x,x503) <-6|1[]- +(x,s(p(x503))) -1|[]-> s(+(x,p(x503))) +(x504,y) <-6|0[]- +(s(p(x504)),y) -4|[]-> s(+(p(x504),y)) p(x505) <-6|0[]- p(s(p(x505))) -7|[]-> p(x505) -(x506) <-6|0[]- -(s(p(x506))) -9|[]-> p(-(p(x506))) +(x,x507) <-7|1[]- +(x,p(s(x507))) -2|[]-> p(+(x,s(x507))) +(x508,y) <-7|0[]- +(p(s(x508)),y) -5|[]-> p(+(s(x508),y)) s(x509) <-7|0[]- s(p(s(x509))) -6|[]-> s(x509) -(x510) <-7|0[]- -(p(s(x510))) -10|[]-> s(-(s(x510))) +(0(),x) <-11|[]- +(x,0()) -0|[]-> x +(s(y),x) <-11|[]- +(x,s(y)) -1|[]-> s(+(x,y)) +(p(y),x) <-11|[]- +(x,p(y)) -2|[]-> p(+(x,y)) +(y,0()) <-11|[]- +(0(),y) -3|[]-> y +(y,s(x)) <-11|[]- +(s(x),y) -4|[]-> s(+(x,y)) +(y,p(x)) <-11|[]- +(p(x),y) -5|[]-> p(+(x,y)) -(+(y,x)) <-11|0[]- -(+(x,y)) -12|[]-> +(-(x),-(y)) Matrix Interpretation Processor: dim=1, lab=right interpretation: [s(0)](x0) = x0, [p(0)](x0) = x0, [+(1)](x0) = 2x0 + 2, [+(0)](x0) = 2x0 + 2, [-(0)](x0) = x0 orientation: -(0)(+(0)(x)) = 2x + 2 >= 2x + 2 = +(0)(-(0)(x)) -(0)(+(1)(y)) = 2y + 2 >= 2y + 2 = +(1)(-(0)(y)) +(0)(x) = 2x + 2 >= 2x + 2 = +(1)(x) +(1)(y) = 2y + 2 >= 2y + 2 = +(0)(y) -(0)(p(0)(x)) = x >= x = s(0)(-(0)(x)) -(0)(s(0)(x)) = x >= x = p(0)(-(0)(x)) p(0)(s(0)(x)) = x >= x = x s(0)(p(0)(x)) = x >= x = x +(0)(p(0)(x)) = 2x + 2 >= 2x + 2 = p(0)(+(0)(x)) +(1)(y) = 2y + 2 >= 2y + 2 = p(0)(+(1)(y)) +(0)(s(0)(x)) = 2x + 2 >= 2x + 2 = s(0)(+(0)(x)) +(1)(y) = 2y + 2 >= 2y + 2 = s(0)(+(1)(y)) +(1)(y) = 2y + 2 >= y = y +(0)(x) = 2x + 2 >= 2x + 2 = p(0)(+(0)(x)) +(1)(p(0)(y)) = 2y + 2 >= 2y + 2 = p(0)(+(1)(y)) +(0)(x) = 2x + 2 >= 2x + 2 = s(0)(+(0)(x)) +(1)(s(0)(y)) = 2y + 2 >= 2y + 2 = s(0)(+(1)(y)) +(0)(x) = 2x + 2 >= x = x problem: strict: weak: -(0)(+(0)(x)) -> +(0)(-(0)(x)) -(0)(+(1)(y)) -> +(1)(-(0)(y)) +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) -(0)(p(0)(x)) -> s(0)(-(0)(x)) -(0)(s(0)(x)) -> p(0)(-(0)(x)) p(0)(s(0)(x)) -> x s(0)(p(0)(x)) -> x +(0)(p(0)(x)) -> p(0)(+(0)(x)) +(1)(y) -> p(0)(+(1)(y)) +(0)(s(0)(x)) -> s(0)(+(0)(x)) +(1)(y) -> s(0)(+(1)(y)) +(0)(x) -> p(0)(+(0)(x)) +(1)(p(0)(y)) -> p(0)(+(1)(y)) +(0)(x) -> s(0)(+(0)(x)) +(1)(s(0)(y)) -> s(0)(+(1)(y)) Matrix Interpretation Processor: dim=1, lab=right interpretation: [s(0)](x0) = x0, [p(0)](x0) = x0, [+(1)](x0) = x0 + 1, [+(0)](x0) = x0 + 1, [-(0)](x0) = 2x0 orientation: -(0)(+(0)(x)) = 2x + 2 >= 2x + 1 = +(0)(-(0)(x)) -(0)(+(1)(y)) = 2y + 2 >= 2y + 1 = +(1)(-(0)(y)) +(0)(x) = x + 1 >= x + 1 = +(1)(x) +(1)(y) = y + 1 >= y + 1 = +(0)(y) -(0)(p(0)(x)) = 2x >= 2x = s(0)(-(0)(x)) -(0)(s(0)(x)) = 2x >= 2x = p(0)(-(0)(x)) p(0)(s(0)(x)) = x >= x = x s(0)(p(0)(x)) = x >= x = x +(0)(p(0)(x)) = x + 1 >= x + 1 = p(0)(+(0)(x)) +(1)(y) = y + 1 >= y + 1 = p(0)(+(1)(y)) +(0)(s(0)(x)) = x + 1 >= x + 1 = s(0)(+(0)(x)) +(1)(y) = y + 1 >= y + 1 = s(0)(+(1)(y)) +(0)(x) = x + 1 >= x + 1 = p(0)(+(0)(x)) +(1)(p(0)(y)) = y + 1 >= y + 1 = p(0)(+(1)(y)) +(0)(x) = x + 1 >= x + 1 = s(0)(+(0)(x)) +(1)(s(0)(y)) = y + 1 >= y + 1 = s(0)(+(1)(y)) problem: strict: weak: +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) -(0)(p(0)(x)) -> s(0)(-(0)(x)) -(0)(s(0)(x)) -> p(0)(-(0)(x)) p(0)(s(0)(x)) -> x s(0)(p(0)(x)) -> x +(0)(p(0)(x)) -> p(0)(+(0)(x)) +(1)(y) -> p(0)(+(1)(y)) +(0)(s(0)(x)) -> s(0)(+(0)(x)) +(1)(y) -> s(0)(+(1)(y)) +(0)(x) -> p(0)(+(0)(x)) +(1)(p(0)(y)) -> p(0)(+(1)(y)) +(0)(x) -> s(0)(+(0)(x)) +(1)(s(0)(y)) -> s(0)(+(1)(y)) Shift Processor lab=left (dd): strict: +(0(),0()) -> 0() +(0(),0()) -> 0() +(s(x),0()) -> s(x) +(s(x),0()) -> s(+(x,0())) s(+(x,0())) -> s(x) +(p(x),0()) -> p(x) +(p(x),0()) -> p(+(x,0())) p(+(x,0())) -> p(x) +(x,0()) -> x +(x,0()) -> +(0(),x) +(0(),x) -> x -(+(x,0())) -> -(x) -(+(x,0())) -> +(-(x),-(0())) +(-(x),-(0())) -> +(-(x),0()) +(-(x),0()) -> -(x) +(0(),s(x459)) -> s(+(0(),x459)) +(0(),s(x459)) -> s(x459) s(+(0(),x459)) -> s(x459) +(s(x),s(x461)) -> s(+(s(x),x461)) +(s(x),s(x461)) -> s(+(x,s(x461))) s(+(s(x),x461)) -> s(s(+(x,x461))) s(+(x,s(x461))) -> s(s(+(x,x461))) +(p(x),s(x463)) -> s(+(p(x),x463)) +(p(x),s(x463)) -> p(+(x,s(x463))) s(+(p(x),x463)) -> s(p(+(x,x463))) s(p(+(x,x463))) -> +(x,x463) p(+(x,s(x463))) -> p(s(+(x,x463))) p(s(+(x,x463))) -> +(x,x463) +(x,s(x465)) -> s(+(x,x465)) +(x,s(x465)) -> +(s(x465),x) s(+(x,x465)) -> s(+(x465,x)) +(s(x465),x) -> s(+(x465,x)) -(+(x,s(x467))) -> -(s(+(x,x467))) -(+(x,s(x467))) -> +(-(x),-(s(x467))) -(s(+(x,x467))) -> p(-(+(x,x467))) p(-(+(x,x467))) -> p(+(-(x),-(x467))) +(-(x),-(s(x467))) -> +(-(x),p(-(x467))) +(-(x),p(-(x467))) -> p(+(-(x),-(x467))) +(0(),p(x469)) -> p(+(0(),x469)) +(0(),p(x469)) -> p(x469) p(+(0(),x469)) -> p(x469) +(s(x),p(x471)) -> p(+(s(x),x471)) +(s(x),p(x471)) -> s(+(x,p(x471))) p(+(s(x),x471)) -> p(s(+(x,x471))) p(s(+(x,x471))) -> +(x,x471) s(+(x,p(x471))) -> s(p(+(x,x471))) s(p(+(x,x471))) -> +(x,x471) +(p(x),p(x473)) -> p(+(p(x),x473)) +(p(x),p(x473)) -> p(+(x,p(x473))) p(+(p(x),x473)) -> p(p(+(x,x473))) p(+(x,p(x473))) -> p(p(+(x,x473))) +(x,p(x475)) -> p(+(x,x475)) +(x,p(x475)) -> +(p(x475),x) p(+(x,x475)) -> p(+(x475,x)) +(p(x475),x) -> p(+(x475,x)) -(+(x,p(x477))) -> -(p(+(x,x477))) -(+(x,p(x477))) -> +(-(x),-(p(x477))) -(p(+(x,x477))) -> s(-(+(x,x477))) s(-(+(x,x477))) -> s(+(-(x),-(x477))) +(-(x),-(p(x477))) -> +(-(x),s(-(x477))) +(-(x),s(-(x477))) -> s(+(-(x),-(x477))) +(0(),0()) -> 0() +(0(),0()) -> 0() +(0(),s(y)) -> s(y) +(0(),s(y)) -> s(+(0(),y)) s(+(0(),y)) -> s(y) +(0(),p(y)) -> p(y) +(0(),p(y)) -> p(+(0(),y)) p(+(0(),y)) -> p(y) +(0(),y) -> y +(0(),y) -> +(y,0()) +(y,0()) -> y -(+(0(),y)) -> -(y) -(+(0(),y)) -> +(-(0()),-(y)) +(-(0()),-(y)) -> +(0(),-(y)) +(0(),-(y)) -> -(y) +(s(x483),0()) -> s(+(x483,0())) +(s(x483),0()) -> s(x483) s(+(x483,0())) -> s(x483) +(s(x485),s(y)) -> s(+(x485,s(y))) +(s(x485),s(y)) -> s(+(s(x485),y)) s(+(x485,s(y))) -> s(s(+(x485,y))) s(+(s(x485),y)) -> s(s(+(x485,y))) +(s(x487),p(y)) -> s(+(x487,p(y))) +(s(x487),p(y)) -> p(+(s(x487),y)) s(+(x487,p(y))) -> s(p(+(x487,y))) s(p(+(x487,y))) -> +(x487,y) p(+(s(x487),y)) -> p(s(+(x487,y))) p(s(+(x487,y))) -> +(x487,y) +(s(x489),y) -> s(+(x489,y)) +(s(x489),y) -> +(y,s(x489)) s(+(x489,y)) -> s(+(y,x489)) +(y,s(x489)) -> s(+(y,x489)) -(+(s(x491),y)) -> -(s(+(x491,y))) -(+(s(x491),y)) -> +(-(s(x491)),-(y)) -(s(+(x491,y))) -> p(-(+(x491,y))) p(-(+(x491,y))) -> p(+(-(x491),-(y))) +(-(s(x491)),-(y)) -> +(p(-(x491)),-(y)) +(p(-(x491)),-(y)) -> p(+(-(x491),-(y))) +(p(x493),0()) -> p(+(x493,0())) +(p(x493),0()) -> p(x493) p(+(x493,0())) -> p(x493) +(p(x495),s(y)) -> p(+(x495,s(y))) +(p(x495),s(y)) -> s(+(p(x495),y)) p(+(x495,s(y))) -> p(s(+(x495,y))) p(s(+(x495,y))) -> +(x495,y) s(+(p(x495),y)) -> s(p(+(x495,y))) s(p(+(x495,y))) -> +(x495,y) +(p(x497),p(y)) -> p(+(x497,p(y))) +(p(x497),p(y)) -> p(+(p(x497),y)) p(+(x497,p(y))) -> p(p(+(x497,y))) p(+(p(x497),y)) -> p(p(+(x497,y))) +(p(x499),y) -> p(+(x499,y)) +(p(x499),y) -> +(y,p(x499)) p(+(x499,y)) -> p(+(y,x499)) +(y,p(x499)) -> p(+(y,x499)) -(+(p(x501),y)) -> -(p(+(x501,y))) -(+(p(x501),y)) -> +(-(p(x501)),-(y)) -(p(+(x501,y))) -> s(-(+(x501,y))) s(-(+(x501,y))) -> s(+(-(x501),-(y))) +(-(p(x501)),-(y)) -> +(s(-(x501)),-(y)) +(s(-(x501)),-(y)) -> s(+(-(x501),-(y))) +(x,s(p(x503))) -> +(x,x503) +(x,s(p(x503))) -> s(+(x,p(x503))) s(+(x,p(x503))) -> s(p(+(x,x503))) s(p(+(x,x503))) -> +(x,x503) +(s(p(x504)),y) -> +(x504,y) +(s(p(x504)),y) -> s(+(p(x504),y)) s(+(p(x504),y)) -> s(p(+(x504,y))) s(p(+(x504,y))) -> +(x504,y) p(s(p(x505))) -> p(x505) p(s(p(x505))) -> p(x505) -(s(p(x506))) -> -(x506) -(s(p(x506))) -> p(-(p(x506))) p(-(p(x506))) -> p(s(-(x506))) p(s(-(x506))) -> -(x506) +(x,p(s(x507))) -> +(x,x507) +(x,p(s(x507))) -> p(+(x,s(x507))) p(+(x,s(x507))) -> p(s(+(x,x507))) p(s(+(x,x507))) -> +(x,x507) +(p(s(x508)),y) -> +(x508,y) +(p(s(x508)),y) -> p(+(s(x508),y)) p(+(s(x508),y)) -> p(s(+(x508,y))) p(s(+(x508,y))) -> +(x508,y) s(p(s(x509))) -> s(x509) s(p(s(x509))) -> s(x509) -(p(s(x510))) -> -(x510) -(p(s(x510))) -> s(-(s(x510))) s(-(s(x510))) -> s(p(-(x510))) s(p(-(x510))) -> -(x510) +(x,0()) -> +(0(),x) +(x,0()) -> x +(0(),x) -> x +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) +(x,p(y)) -> +(p(y),x) +(x,p(y)) -> p(+(x,y)) +(p(y),x) -> p(+(y,x)) p(+(x,y)) -> p(+(y,x)) +(0(),y) -> +(y,0()) +(0(),y) -> y +(y,0()) -> y +(s(x),y) -> +(y,s(x)) +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) +(p(x),y) -> +(y,p(x)) +(p(x),y) -> p(+(x,y)) +(y,p(x)) -> p(+(y,x)) p(+(x,y)) -> p(+(y,x)) -(+(x,y)) -> -(+(y,x)) -(+(x,y)) -> +(-(x),-(y)) -(+(y,x)) -> +(-(y),-(x)) +(-(x),-(y)) -> +(-(y),-(x)) weak: +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(x,p(y)) -> p(+(x,y)) +(0(),y) -> y +(s(x),y) -> s(+(x,y)) +(p(x),y) -> p(+(x,y)) s(p(x)) -> x p(s(x)) -> x -(0()) -> 0() -(s(x)) -> p(-(x)) -(p(x)) -> s(-(x)) +(x,y) -> +(y,x) -(+(x,y)) -> +(-(x),-(y)) Matrix Interpretation Processor: dim=1 interpretation: [-](x0) = x0, [p](x0) = x0 + 4, [s](x0) = x0 + 4, [+](x0, x1) = x0 + x1, [0] = 0 orientation: +(0(),0()) = 0 >= 0 = 0() +(0(),0()) = 0 >= 0 = 0() +(s(x),0()) = x + 4 >= x + 4 = s(x) +(s(x),0()) = x + 4 >= x + 4 = s(+(x,0())) s(+(x,0())) = x + 4 >= x + 4 = s(x) +(p(x),0()) = x + 4 >= x + 4 = p(x) +(p(x),0()) = x + 4 >= x + 4 = p(+(x,0())) p(+(x,0())) = x + 4 >= x + 4 = p(x) +(x,0()) = x >= x = x +(x,0()) = x >= x = +(0(),x) +(0(),x) = x >= x = x -(+(x,0())) = x >= x = -(x) -(+(x,0())) = x >= x = +(-(x),-(0())) +(-(x),-(0())) = x >= x = +(-(x),0()) +(-(x),0()) = x >= x = -(x) +(0(),s(x459)) = x459 + 4 >= x459 + 4 = s(+(0(),x459)) +(0(),s(x459)) = x459 + 4 >= x459 + 4 = s(x459) s(+(0(),x459)) = x459 + 4 >= x459 + 4 = s(x459) +(s(x),s(x461)) = x + x461 + 8 >= x + x461 + 8 = s(+(s(x),x461)) +(s(x),s(x461)) = x + x461 + 8 >= x + x461 + 8 = s(+(x,s(x461))) s(+(s(x),x461)) = x + x461 + 8 >= x + x461 + 8 = s(s(+(x,x461))) s(+(x,s(x461))) = x + x461 + 8 >= x + x461 + 8 = s(s(+(x,x461))) +(p(x),s(x463)) = x + x463 + 8 >= x + x463 + 8 = s(+(p(x),x463)) +(p(x),s(x463)) = x + x463 + 8 >= x + x463 + 8 = p(+(x,s(x463))) s(+(p(x),x463)) = x + x463 + 8 >= x + x463 + 8 = s(p(+(x,x463))) s(p(+(x,x463))) = x + x463 + 8 >= x + x463 = +(x,x463) p(+(x,s(x463))) = x + x463 + 8 >= x + x463 + 8 = p(s(+(x,x463))) p(s(+(x,x463))) = x + x463 + 8 >= x + x463 = +(x,x463) +(x,s(x465)) = x + x465 + 4 >= x + x465 + 4 = s(+(x,x465)) +(x,s(x465)) = x + x465 + 4 >= x + x465 + 4 = +(s(x465),x) s(+(x,x465)) = x + x465 + 4 >= x + x465 + 4 = s(+(x465,x)) +(s(x465),x) = x + x465 + 4 >= x + x465 + 4 = s(+(x465,x)) -(+(x,s(x467))) = x + x467 + 4 >= x + x467 + 4 = -(s(+(x,x467))) -(+(x,s(x467))) = x + x467 + 4 >= x + x467 + 4 = +(-(x),-(s(x467))) -(s(+(x,x467))) = x + x467 + 4 >= x + x467 + 4 = p(-(+(x,x467))) p(-(+(x,x467))) = x + x467 + 4 >= x + x467 + 4 = p(+(-(x),-(x467))) +(-(x),-(s(x467))) = x + x467 + 4 >= x + x467 + 4 = +(-(x),p(-(x467))) +(-(x),p(-(x467))) = x + x467 + 4 >= x + x467 + 4 = p(+(-(x),-(x467))) +(0(),p(x469)) = x469 + 4 >= x469 + 4 = p(+(0(),x469)) +(0(),p(x469)) = x469 + 4 >= x469 + 4 = p(x469) p(+(0(),x469)) = x469 + 4 >= x469 + 4 = p(x469) +(s(x),p(x471)) = x + x471 + 8 >= x + x471 + 8 = p(+(s(x),x471)) +(s(x),p(x471)) = x + x471 + 8 >= x + x471 + 8 = s(+(x,p(x471))) p(+(s(x),x471)) = x + x471 + 8 >= x + x471 + 8 = p(s(+(x,x471))) p(s(+(x,x471))) = x + x471 + 8 >= x + x471 = +(x,x471) s(+(x,p(x471))) = x + x471 + 8 >= x + x471 + 8 = s(p(+(x,x471))) s(p(+(x,x471))) = x + x471 + 8 >= x + x471 = +(x,x471) +(p(x),p(x473)) = x + x473 + 8 >= x + x473 + 8 = p(+(p(x),x473)) +(p(x),p(x473)) = x + x473 + 8 >= x + x473 + 8 = p(+(x,p(x473))) p(+(p(x),x473)) = x + x473 + 8 >= x + x473 + 8 = p(p(+(x,x473))) p(+(x,p(x473))) = x + x473 + 8 >= x + x473 + 8 = p(p(+(x,x473))) +(x,p(x475)) = x + x475 + 4 >= x + x475 + 4 = p(+(x,x475)) +(x,p(x475)) = x + x475 + 4 >= x + x475 + 4 = +(p(x475),x) p(+(x,x475)) = x + x475 + 4 >= x + x475 + 4 = p(+(x475,x)) +(p(x475),x) = x + x475 + 4 >= x + x475 + 4 = p(+(x475,x)) -(+(x,p(x477))) = x + x477 + 4 >= x + x477 + 4 = -(p(+(x,x477))) -(+(x,p(x477))) = x + x477 + 4 >= x + x477 + 4 = +(-(x),-(p(x477))) -(p(+(x,x477))) = x + x477 + 4 >= x + x477 + 4 = s(-(+(x,x477))) s(-(+(x,x477))) = x + x477 + 4 >= x + x477 + 4 = s(+(-(x),-(x477))) +(-(x),-(p(x477))) = x + x477 + 4 >= x + x477 + 4 = +(-(x),s(-(x477))) +(-(x),s(-(x477))) = x + x477 + 4 >= x + x477 + 4 = s(+(-(x),-(x477))) +(0(),0()) = 0 >= 0 = 0() +(0(),0()) = 0 >= 0 = 0() +(0(),s(y)) = y + 4 >= y + 4 = s(y) +(0(),s(y)) = y + 4 >= y + 4 = s(+(0(),y)) s(+(0(),y)) = y + 4 >= y + 4 = s(y) +(0(),p(y)) = y + 4 >= y + 4 = p(y) +(0(),p(y)) = y + 4 >= y + 4 = p(+(0(),y)) p(+(0(),y)) = y + 4 >= y + 4 = p(y) +(0(),y) = y >= y = y +(0(),y) = y >= y = +(y,0()) +(y,0()) = y >= y = y -(+(0(),y)) = y >= y = -(y) -(+(0(),y)) = y >= y = +(-(0()),-(y)) +(-(0()),-(y)) = y >= y = +(0(),-(y)) +(0(),-(y)) = y >= y = -(y) +(s(x483),0()) = x483 + 4 >= x483 + 4 = s(+(x483,0())) +(s(x483),0()) = x483 + 4 >= x483 + 4 = s(x483) s(+(x483,0())) = x483 + 4 >= x483 + 4 = s(x483) +(s(x485),s(y)) = x485 + y + 8 >= x485 + y + 8 = s(+(x485,s(y))) +(s(x485),s(y)) = x485 + y + 8 >= x485 + y + 8 = s(+(s(x485),y)) s(+(x485,s(y))) = x485 + y + 8 >= x485 + y + 8 = s(s(+(x485,y))) s(+(s(x485),y)) = x485 + y + 8 >= x485 + y + 8 = s(s(+(x485,y))) +(s(x487),p(y)) = x487 + y + 8 >= x487 + y + 8 = s(+(x487,p(y))) +(s(x487),p(y)) = x487 + y + 8 >= x487 + y + 8 = p(+(s(x487),y)) s(+(x487,p(y))) = x487 + y + 8 >= x487 + y + 8 = s(p(+(x487,y))) s(p(+(x487,y))) = x487 + y + 8 >= x487 + y = +(x487,y) p(+(s(x487),y)) = x487 + y + 8 >= x487 + y + 8 = p(s(+(x487,y))) p(s(+(x487,y))) = x487 + y + 8 >= x487 + y = +(x487,y) +(s(x489),y) = x489 + y + 4 >= x489 + y + 4 = s(+(x489,y)) +(s(x489),y) = x489 + y + 4 >= x489 + y + 4 = +(y,s(x489)) s(+(x489,y)) = x489 + y + 4 >= x489 + y + 4 = s(+(y,x489)) +(y,s(x489)) = x489 + y + 4 >= x489 + y + 4 = s(+(y,x489)) -(+(s(x491),y)) = x491 + y + 4 >= x491 + y + 4 = -(s(+(x491,y))) -(+(s(x491),y)) = x491 + y + 4 >= x491 + y + 4 = +(-(s(x491)),-(y)) -(s(+(x491,y))) = x491 + y + 4 >= x491 + y + 4 = p(-(+(x491,y))) p(-(+(x491,y))) = x491 + y + 4 >= x491 + y + 4 = p(+(-(x491),-(y))) +(-(s(x491)),-(y)) = x491 + y + 4 >= x491 + y + 4 = +(p(-(x491)),-(y)) +(p(-(x491)),-(y)) = x491 + y + 4 >= x491 + y + 4 = p(+(-(x491),-(y))) +(p(x493),0()) = x493 + 4 >= x493 + 4 = p(+(x493,0())) +(p(x493),0()) = x493 + 4 >= x493 + 4 = p(x493) p(+(x493,0())) = x493 + 4 >= x493 + 4 = p(x493) +(p(x495),s(y)) = x495 + y + 8 >= x495 + y + 8 = p(+(x495,s(y))) +(p(x495),s(y)) = x495 + y + 8 >= x495 + y + 8 = s(+(p(x495),y)) p(+(x495,s(y))) = x495 + y + 8 >= x495 + y + 8 = p(s(+(x495,y))) p(s(+(x495,y))) = x495 + y + 8 >= x495 + y = +(x495,y) s(+(p(x495),y)) = x495 + y + 8 >= x495 + y + 8 = s(p(+(x495,y))) s(p(+(x495,y))) = x495 + y + 8 >= x495 + y = +(x495,y) +(p(x497),p(y)) = x497 + y + 8 >= x497 + y + 8 = p(+(x497,p(y))) +(p(x497),p(y)) = x497 + y + 8 >= x497 + y + 8 = p(+(p(x497),y)) p(+(x497,p(y))) = x497 + y + 8 >= x497 + y + 8 = p(p(+(x497,y))) p(+(p(x497),y)) = x497 + y + 8 >= x497 + y + 8 = p(p(+(x497,y))) +(p(x499),y) = x499 + y + 4 >= x499 + y + 4 = p(+(x499,y)) +(p(x499),y) = x499 + y + 4 >= x499 + y + 4 = +(y,p(x499)) p(+(x499,y)) = x499 + y + 4 >= x499 + y + 4 = p(+(y,x499)) +(y,p(x499)) = x499 + y + 4 >= x499 + y + 4 = p(+(y,x499)) -(+(p(x501),y)) = x501 + y + 4 >= x501 + y + 4 = -(p(+(x501,y))) -(+(p(x501),y)) = x501 + y + 4 >= x501 + y + 4 = +(-(p(x501)),-(y)) -(p(+(x501,y))) = x501 + y + 4 >= x501 + y + 4 = s(-(+(x501,y))) s(-(+(x501,y))) = x501 + y + 4 >= x501 + y + 4 = s(+(-(x501),-(y))) +(-(p(x501)),-(y)) = x501 + y + 4 >= x501 + y + 4 = +(s(-(x501)),-(y)) +(s(-(x501)),-(y)) = x501 + y + 4 >= x501 + y + 4 = s(+(-(x501),-(y))) +(x,s(p(x503))) = x + x503 + 8 >= x + x503 = +(x,x503) +(x,s(p(x503))) = x + x503 + 8 >= x + x503 + 8 = s(+(x,p(x503))) s(+(x,p(x503))) = x + x503 + 8 >= x + x503 + 8 = s(p(+(x,x503))) s(p(+(x,x503))) = x + x503 + 8 >= x + x503 = +(x,x503) +(s(p(x504)),y) = x504 + y + 8 >= x504 + y = +(x504,y) +(s(p(x504)),y) = x504 + y + 8 >= x504 + y + 8 = s(+(p(x504),y)) s(+(p(x504),y)) = x504 + y + 8 >= x504 + y + 8 = s(p(+(x504,y))) s(p(+(x504,y))) = x504 + y + 8 >= x504 + y = +(x504,y) p(s(p(x505))) = x505 + 12 >= x505 + 4 = p(x505) p(s(p(x505))) = x505 + 12 >= x505 + 4 = p(x505) -(s(p(x506))) = x506 + 8 >= x506 = -(x506) -(s(p(x506))) = x506 + 8 >= x506 + 8 = p(-(p(x506))) p(-(p(x506))) = x506 + 8 >= x506 + 8 = p(s(-(x506))) p(s(-(x506))) = x506 + 8 >= x506 = -(x506) +(x,p(s(x507))) = x + x507 + 8 >= x + x507 = +(x,x507) +(x,p(s(x507))) = x + x507 + 8 >= x + x507 + 8 = p(+(x,s(x507))) p(+(x,s(x507))) = x + x507 + 8 >= x + x507 + 8 = p(s(+(x,x507))) p(s(+(x,x507))) = x + x507 + 8 >= x + x507 = +(x,x507) +(p(s(x508)),y) = x508 + y + 8 >= x508 + y = +(x508,y) +(p(s(x508)),y) = x508 + y + 8 >= x508 + y + 8 = p(+(s(x508),y)) p(+(s(x508),y)) = x508 + y + 8 >= x508 + y + 8 = p(s(+(x508,y))) p(s(+(x508,y))) = x508 + y + 8 >= x508 + y = +(x508,y) s(p(s(x509))) = x509 + 12 >= x509 + 4 = s(x509) s(p(s(x509))) = x509 + 12 >= x509 + 4 = s(x509) -(p(s(x510))) = x510 + 8 >= x510 = -(x510) -(p(s(x510))) = x510 + 8 >= x510 + 8 = s(-(s(x510))) s(-(s(x510))) = x510 + 8 >= x510 + 8 = s(p(-(x510))) s(p(-(x510))) = x510 + 8 >= x510 = -(x510) +(x,0()) = x >= x = +(0(),x) +(x,0()) = x >= x = x +(0(),x) = x >= x = x +(x,s(y)) = x + y + 4 >= x + y + 4 = +(s(y),x) +(x,s(y)) = x + y + 4 >= x + y + 4 = s(+(x,y)) +(s(y),x) = x + y + 4 >= x + y + 4 = s(+(y,x)) s(+(x,y)) = x + y + 4 >= x + y + 4 = s(+(y,x)) +(x,p(y)) = x + y + 4 >= x + y + 4 = +(p(y),x) +(x,p(y)) = x + y + 4 >= x + y + 4 = p(+(x,y)) +(p(y),x) = x + y + 4 >= x + y + 4 = p(+(y,x)) p(+(x,y)) = x + y + 4 >= x + y + 4 = p(+(y,x)) +(0(),y) = y >= y = +(y,0()) +(0(),y) = y >= y = y +(y,0()) = y >= y = y +(s(x),y) = x + y + 4 >= x + y + 4 = +(y,s(x)) +(s(x),y) = x + y + 4 >= x + y + 4 = s(+(x,y)) +(y,s(x)) = x + y + 4 >= x + y + 4 = s(+(y,x)) s(+(x,y)) = x + y + 4 >= x + y + 4 = s(+(y,x)) +(p(x),y) = x + y + 4 >= x + y + 4 = +(y,p(x)) +(p(x),y) = x + y + 4 >= x + y + 4 = p(+(x,y)) +(y,p(x)) = x + y + 4 >= x + y + 4 = p(+(y,x)) p(+(x,y)) = x + y + 4 >= x + y + 4 = p(+(y,x)) -(+(x,y)) = x + y >= x + y = -(+(y,x)) -(+(x,y)) = x + y >= x + y = +(-(x),-(y)) -(+(y,x)) = x + y >= x + y = +(-(y),-(x)) +(-(x),-(y)) = x + y >= x + y = +(-(y),-(x)) s(p(x)) = x + 8 >= x = x p(s(x)) = x + 8 >= x = x -(0()) = 0 >= 0 = 0() -(s(x)) = x + 4 >= x + 4 = p(-(x)) -(p(x)) = x + 4 >= x + 4 = s(-(x)) +(x,y) = x + y >= x + y = +(y,x) problem: strict: +(0(),0()) -> 0() +(0(),0()) -> 0() +(s(x),0()) -> s(x) +(s(x),0()) -> s(+(x,0())) s(+(x,0())) -> s(x) +(p(x),0()) -> p(x) +(p(x),0()) -> p(+(x,0())) p(+(x,0())) -> p(x) +(x,0()) -> x +(x,0()) -> +(0(),x) +(0(),x) -> x -(+(x,0())) -> -(x) -(+(x,0())) -> +(-(x),-(0())) +(-(x),-(0())) -> +(-(x),0()) +(-(x),0()) -> -(x) +(0(),s(x459)) -> s(+(0(),x459)) +(0(),s(x459)) -> s(x459) s(+(0(),x459)) -> s(x459) +(s(x),s(x461)) -> s(+(s(x),x461)) +(s(x),s(x461)) -> s(+(x,s(x461))) s(+(s(x),x461)) -> s(s(+(x,x461))) s(+(x,s(x461))) -> s(s(+(x,x461))) +(p(x),s(x463)) -> s(+(p(x),x463)) +(p(x),s(x463)) -> p(+(x,s(x463))) s(+(p(x),x463)) -> s(p(+(x,x463))) p(+(x,s(x463))) -> p(s(+(x,x463))) +(x,s(x465)) -> s(+(x,x465)) +(x,s(x465)) -> +(s(x465),x) s(+(x,x465)) -> s(+(x465,x)) +(s(x465),x) -> s(+(x465,x)) -(+(x,s(x467))) -> -(s(+(x,x467))) -(+(x,s(x467))) -> +(-(x),-(s(x467))) -(s(+(x,x467))) -> p(-(+(x,x467))) p(-(+(x,x467))) -> p(+(-(x),-(x467))) +(-(x),-(s(x467))) -> +(-(x),p(-(x467))) +(-(x),p(-(x467))) -> p(+(-(x),-(x467))) +(0(),p(x469)) -> p(+(0(),x469)) +(0(),p(x469)) -> p(x469) p(+(0(),x469)) -> p(x469) +(s(x),p(x471)) -> p(+(s(x),x471)) +(s(x),p(x471)) -> s(+(x,p(x471))) p(+(s(x),x471)) -> p(s(+(x,x471))) s(+(x,p(x471))) -> s(p(+(x,x471))) +(p(x),p(x473)) -> p(+(p(x),x473)) +(p(x),p(x473)) -> p(+(x,p(x473))) p(+(p(x),x473)) -> p(p(+(x,x473))) p(+(x,p(x473))) -> p(p(+(x,x473))) +(x,p(x475)) -> p(+(x,x475)) +(x,p(x475)) -> +(p(x475),x) p(+(x,x475)) -> p(+(x475,x)) +(p(x475),x) -> p(+(x475,x)) -(+(x,p(x477))) -> -(p(+(x,x477))) -(+(x,p(x477))) -> +(-(x),-(p(x477))) -(p(+(x,x477))) -> s(-(+(x,x477))) s(-(+(x,x477))) -> s(+(-(x),-(x477))) +(-(x),-(p(x477))) -> +(-(x),s(-(x477))) +(-(x),s(-(x477))) -> s(+(-(x),-(x477))) +(0(),0()) -> 0() +(0(),0()) -> 0() +(0(),s(y)) -> s(y) +(0(),s(y)) -> s(+(0(),y)) s(+(0(),y)) -> s(y) +(0(),p(y)) -> p(y) +(0(),p(y)) -> p(+(0(),y)) p(+(0(),y)) -> p(y) +(0(),y) -> y +(0(),y) -> +(y,0()) +(y,0()) -> y -(+(0(),y)) -> -(y) -(+(0(),y)) -> +(-(0()),-(y)) +(-(0()),-(y)) -> +(0(),-(y)) +(0(),-(y)) -> -(y) +(s(x483),0()) -> s(+(x483,0())) +(s(x483),0()) -> s(x483) s(+(x483,0())) -> s(x483) +(s(x485),s(y)) -> s(+(x485,s(y))) +(s(x485),s(y)) -> s(+(s(x485),y)) s(+(x485,s(y))) -> s(s(+(x485,y))) s(+(s(x485),y)) -> s(s(+(x485,y))) +(s(x487),p(y)) -> s(+(x487,p(y))) +(s(x487),p(y)) -> p(+(s(x487),y)) s(+(x487,p(y))) -> s(p(+(x487,y))) p(+(s(x487),y)) -> p(s(+(x487,y))) +(s(x489),y) -> s(+(x489,y)) +(s(x489),y) -> +(y,s(x489)) s(+(x489,y)) -> s(+(y,x489)) +(y,s(x489)) -> s(+(y,x489)) -(+(s(x491),y)) -> -(s(+(x491,y))) -(+(s(x491),y)) -> +(-(s(x491)),-(y)) -(s(+(x491,y))) -> p(-(+(x491,y))) p(-(+(x491,y))) -> p(+(-(x491),-(y))) +(-(s(x491)),-(y)) -> +(p(-(x491)),-(y)) +(p(-(x491)),-(y)) -> p(+(-(x491),-(y))) +(p(x493),0()) -> p(+(x493,0())) +(p(x493),0()) -> p(x493) p(+(x493,0())) -> p(x493) +(p(x495),s(y)) -> p(+(x495,s(y))) +(p(x495),s(y)) -> s(+(p(x495),y)) p(+(x495,s(y))) -> p(s(+(x495,y))) s(+(p(x495),y)) -> s(p(+(x495,y))) +(p(x497),p(y)) -> p(+(x497,p(y))) +(p(x497),p(y)) -> p(+(p(x497),y)) p(+(x497,p(y))) -> p(p(+(x497,y))) p(+(p(x497),y)) -> p(p(+(x497,y))) +(p(x499),y) -> p(+(x499,y)) +(p(x499),y) -> +(y,p(x499)) p(+(x499,y)) -> p(+(y,x499)) +(y,p(x499)) -> p(+(y,x499)) -(+(p(x501),y)) -> -(p(+(x501,y))) -(+(p(x501),y)) -> +(-(p(x501)),-(y)) -(p(+(x501,y))) -> s(-(+(x501,y))) s(-(+(x501,y))) -> s(+(-(x501),-(y))) +(-(p(x501)),-(y)) -> +(s(-(x501)),-(y)) +(s(-(x501)),-(y)) -> s(+(-(x501),-(y))) +(x,s(p(x503))) -> s(+(x,p(x503))) s(+(x,p(x503))) -> s(p(+(x,x503))) +(s(p(x504)),y) -> s(+(p(x504),y)) s(+(p(x504),y)) -> s(p(+(x504,y))) -(s(p(x506))) -> p(-(p(x506))) p(-(p(x506))) -> p(s(-(x506))) +(x,p(s(x507))) -> p(+(x,s(x507))) p(+(x,s(x507))) -> p(s(+(x,x507))) +(p(s(x508)),y) -> p(+(s(x508),y)) p(+(s(x508),y)) -> p(s(+(x508,y))) -(p(s(x510))) -> s(-(s(x510))) s(-(s(x510))) -> s(p(-(x510))) +(x,0()) -> +(0(),x) +(x,0()) -> x +(0(),x) -> x +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) +(x,p(y)) -> +(p(y),x) +(x,p(y)) -> p(+(x,y)) +(p(y),x) -> p(+(y,x)) p(+(x,y)) -> p(+(y,x)) +(0(),y) -> +(y,0()) +(0(),y) -> y +(y,0()) -> y +(s(x),y) -> +(y,s(x)) +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) +(p(x),y) -> +(y,p(x)) +(p(x),y) -> p(+(x,y)) +(y,p(x)) -> p(+(y,x)) p(+(x,y)) -> p(+(y,x)) -(+(x,y)) -> -(+(y,x)) -(+(x,y)) -> +(-(x),-(y)) -(+(y,x)) -> +(-(y),-(x)) +(-(x),-(y)) -> +(-(y),-(x)) weak: +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(x,p(y)) -> p(+(x,y)) +(0(),y) -> y +(s(x),y) -> s(+(x,y)) +(p(x),y) -> p(+(x,y)) -(0()) -> 0() -(s(x)) -> p(-(x)) -(p(x)) -> s(-(x)) +(x,y) -> +(y,x) -(+(x,y)) -> +(-(x),-(y)) Matrix Interpretation Processor: dim=1 interpretation: [-](x0) = x0, [p](x0) = x0, [s](x0) = x0, [+](x0, x1) = 2x0 + 2x1, [0] = 2 orientation: +(0(),0()) = 8 >= 2 = 0() +(0(),0()) = 8 >= 2 = 0() +(s(x),0()) = 2x + 4 >= x = s(x) +(s(x),0()) = 2x + 4 >= 2x + 4 = s(+(x,0())) s(+(x,0())) = 2x + 4 >= x = s(x) +(p(x),0()) = 2x + 4 >= x = p(x) +(p(x),0()) = 2x + 4 >= 2x + 4 = p(+(x,0())) p(+(x,0())) = 2x + 4 >= x = p(x) +(x,0()) = 2x + 4 >= x = x +(x,0()) = 2x + 4 >= 2x + 4 = +(0(),x) +(0(),x) = 2x + 4 >= x = x -(+(x,0())) = 2x + 4 >= x = -(x) -(+(x,0())) = 2x + 4 >= 2x + 4 = +(-(x),-(0())) +(-(x),-(0())) = 2x + 4 >= 2x + 4 = +(-(x),0()) +(-(x),0()) = 2x + 4 >= x = -(x) +(0(),s(x459)) = 2x459 + 4 >= 2x459 + 4 = s(+(0(),x459)) +(0(),s(x459)) = 2x459 + 4 >= x459 = s(x459) s(+(0(),x459)) = 2x459 + 4 >= x459 = s(x459) +(s(x),s(x461)) = 2x + 2x461 >= 2x + 2x461 = s(+(s(x),x461)) +(s(x),s(x461)) = 2x + 2x461 >= 2x + 2x461 = s(+(x,s(x461))) s(+(s(x),x461)) = 2x + 2x461 >= 2x + 2x461 = s(s(+(x,x461))) s(+(x,s(x461))) = 2x + 2x461 >= 2x + 2x461 = s(s(+(x,x461))) +(p(x),s(x463)) = 2x + 2x463 >= 2x + 2x463 = s(+(p(x),x463)) +(p(x),s(x463)) = 2x + 2x463 >= 2x + 2x463 = p(+(x,s(x463))) s(+(p(x),x463)) = 2x + 2x463 >= 2x + 2x463 = s(p(+(x,x463))) p(+(x,s(x463))) = 2x + 2x463 >= 2x + 2x463 = p(s(+(x,x463))) +(x,s(x465)) = 2x + 2x465 >= 2x + 2x465 = s(+(x,x465)) +(x,s(x465)) = 2x + 2x465 >= 2x + 2x465 = +(s(x465),x) s(+(x,x465)) = 2x + 2x465 >= 2x + 2x465 = s(+(x465,x)) +(s(x465),x) = 2x + 2x465 >= 2x + 2x465 = s(+(x465,x)) -(+(x,s(x467))) = 2x + 2x467 >= 2x + 2x467 = -(s(+(x,x467))) -(+(x,s(x467))) = 2x + 2x467 >= 2x + 2x467 = +(-(x),-(s(x467))) -(s(+(x,x467))) = 2x + 2x467 >= 2x + 2x467 = p(-(+(x,x467))) p(-(+(x,x467))) = 2x + 2x467 >= 2x + 2x467 = p(+(-(x),-(x467))) +(-(x),-(s(x467))) = 2x + 2x467 >= 2x + 2x467 = +(-(x),p(-(x467))) +(-(x),p(-(x467))) = 2x + 2x467 >= 2x + 2x467 = p(+(-(x),-(x467))) +(0(),p(x469)) = 2x469 + 4 >= 2x469 + 4 = p(+(0(),x469)) +(0(),p(x469)) = 2x469 + 4 >= x469 = p(x469) p(+(0(),x469)) = 2x469 + 4 >= x469 = p(x469) +(s(x),p(x471)) = 2x + 2x471 >= 2x + 2x471 = p(+(s(x),x471)) +(s(x),p(x471)) = 2x + 2x471 >= 2x + 2x471 = s(+(x,p(x471))) p(+(s(x),x471)) = 2x + 2x471 >= 2x + 2x471 = p(s(+(x,x471))) s(+(x,p(x471))) = 2x + 2x471 >= 2x + 2x471 = s(p(+(x,x471))) +(p(x),p(x473)) = 2x + 2x473 >= 2x + 2x473 = p(+(p(x),x473)) +(p(x),p(x473)) = 2x + 2x473 >= 2x + 2x473 = p(+(x,p(x473))) p(+(p(x),x473)) = 2x + 2x473 >= 2x + 2x473 = p(p(+(x,x473))) p(+(x,p(x473))) = 2x + 2x473 >= 2x + 2x473 = p(p(+(x,x473))) +(x,p(x475)) = 2x + 2x475 >= 2x + 2x475 = p(+(x,x475)) +(x,p(x475)) = 2x + 2x475 >= 2x + 2x475 = +(p(x475),x) p(+(x,x475)) = 2x + 2x475 >= 2x + 2x475 = p(+(x475,x)) +(p(x475),x) = 2x + 2x475 >= 2x + 2x475 = p(+(x475,x)) -(+(x,p(x477))) = 2x + 2x477 >= 2x + 2x477 = -(p(+(x,x477))) -(+(x,p(x477))) = 2x + 2x477 >= 2x + 2x477 = +(-(x),-(p(x477))) -(p(+(x,x477))) = 2x + 2x477 >= 2x + 2x477 = s(-(+(x,x477))) s(-(+(x,x477))) = 2x + 2x477 >= 2x + 2x477 = s(+(-(x),-(x477))) +(-(x),-(p(x477))) = 2x + 2x477 >= 2x + 2x477 = +(-(x),s(-(x477))) +(-(x),s(-(x477))) = 2x + 2x477 >= 2x + 2x477 = s(+(-(x),-(x477))) +(0(),0()) = 8 >= 2 = 0() +(0(),0()) = 8 >= 2 = 0() +(0(),s(y)) = 2y + 4 >= y = s(y) +(0(),s(y)) = 2y + 4 >= 2y + 4 = s(+(0(),y)) s(+(0(),y)) = 2y + 4 >= y = s(y) +(0(),p(y)) = 2y + 4 >= y = p(y) +(0(),p(y)) = 2y + 4 >= 2y + 4 = p(+(0(),y)) p(+(0(),y)) = 2y + 4 >= y = p(y) +(0(),y) = 2y + 4 >= y = y +(0(),y) = 2y + 4 >= 2y + 4 = +(y,0()) +(y,0()) = 2y + 4 >= y = y -(+(0(),y)) = 2y + 4 >= y = -(y) -(+(0(),y)) = 2y + 4 >= 2y + 4 = +(-(0()),-(y)) +(-(0()),-(y)) = 2y + 4 >= 2y + 4 = +(0(),-(y)) +(0(),-(y)) = 2y + 4 >= y = -(y) +(s(x483),0()) = 2x483 + 4 >= 2x483 + 4 = s(+(x483,0())) +(s(x483),0()) = 2x483 + 4 >= x483 = s(x483) s(+(x483,0())) = 2x483 + 4 >= x483 = s(x483) +(s(x485),s(y)) = 2x485 + 2y >= 2x485 + 2y = s(+(x485,s(y))) +(s(x485),s(y)) = 2x485 + 2y >= 2x485 + 2y = s(+(s(x485),y)) s(+(x485,s(y))) = 2x485 + 2y >= 2x485 + 2y = s(s(+(x485,y))) s(+(s(x485),y)) = 2x485 + 2y >= 2x485 + 2y = s(s(+(x485,y))) +(s(x487),p(y)) = 2x487 + 2y >= 2x487 + 2y = s(+(x487,p(y))) +(s(x487),p(y)) = 2x487 + 2y >= 2x487 + 2y = p(+(s(x487),y)) s(+(x487,p(y))) = 2x487 + 2y >= 2x487 + 2y = s(p(+(x487,y))) p(+(s(x487),y)) = 2x487 + 2y >= 2x487 + 2y = p(s(+(x487,y))) +(s(x489),y) = 2x489 + 2y >= 2x489 + 2y = s(+(x489,y)) +(s(x489),y) = 2x489 + 2y >= 2x489 + 2y = +(y,s(x489)) s(+(x489,y)) = 2x489 + 2y >= 2x489 + 2y = s(+(y,x489)) +(y,s(x489)) = 2x489 + 2y >= 2x489 + 2y = s(+(y,x489)) -(+(s(x491),y)) = 2x491 + 2y >= 2x491 + 2y = -(s(+(x491,y))) -(+(s(x491),y)) = 2x491 + 2y >= 2x491 + 2y = +(-(s(x491)),-(y)) -(s(+(x491,y))) = 2x491 + 2y >= 2x491 + 2y = p(-(+(x491,y))) p(-(+(x491,y))) = 2x491 + 2y >= 2x491 + 2y = p(+(-(x491),-(y))) +(-(s(x491)),-(y)) = 2x491 + 2y >= 2x491 + 2y = +(p(-(x491)),-(y)) +(p(-(x491)),-(y)) = 2x491 + 2y >= 2x491 + 2y = p(+(-(x491),-(y))) +(p(x493),0()) = 2x493 + 4 >= 2x493 + 4 = p(+(x493,0())) +(p(x493),0()) = 2x493 + 4 >= x493 = p(x493) p(+(x493,0())) = 2x493 + 4 >= x493 = p(x493) +(p(x495),s(y)) = 2x495 + 2y >= 2x495 + 2y = p(+(x495,s(y))) +(p(x495),s(y)) = 2x495 + 2y >= 2x495 + 2y = s(+(p(x495),y)) p(+(x495,s(y))) = 2x495 + 2y >= 2x495 + 2y = p(s(+(x495,y))) s(+(p(x495),y)) = 2x495 + 2y >= 2x495 + 2y = s(p(+(x495,y))) +(p(x497),p(y)) = 2x497 + 2y >= 2x497 + 2y = p(+(x497,p(y))) +(p(x497),p(y)) = 2x497 + 2y >= 2x497 + 2y = p(+(p(x497),y)) p(+(x497,p(y))) = 2x497 + 2y >= 2x497 + 2y = p(p(+(x497,y))) p(+(p(x497),y)) = 2x497 + 2y >= 2x497 + 2y = p(p(+(x497,y))) +(p(x499),y) = 2x499 + 2y >= 2x499 + 2y = p(+(x499,y)) +(p(x499),y) = 2x499 + 2y >= 2x499 + 2y = +(y,p(x499)) p(+(x499,y)) = 2x499 + 2y >= 2x499 + 2y = p(+(y,x499)) +(y,p(x499)) = 2x499 + 2y >= 2x499 + 2y = p(+(y,x499)) -(+(p(x501),y)) = 2x501 + 2y >= 2x501 + 2y = -(p(+(x501,y))) -(+(p(x501),y)) = 2x501 + 2y >= 2x501 + 2y = +(-(p(x501)),-(y)) -(p(+(x501,y))) = 2x501 + 2y >= 2x501 + 2y = s(-(+(x501,y))) s(-(+(x501,y))) = 2x501 + 2y >= 2x501 + 2y = s(+(-(x501),-(y))) +(-(p(x501)),-(y)) = 2x501 + 2y >= 2x501 + 2y = +(s(-(x501)),-(y)) +(s(-(x501)),-(y)) = 2x501 + 2y >= 2x501 + 2y = s(+(-(x501),-(y))) +(x,s(p(x503))) = 2x + 2x503 >= 2x + 2x503 = s(+(x,p(x503))) s(+(x,p(x503))) = 2x + 2x503 >= 2x + 2x503 = s(p(+(x,x503))) +(s(p(x504)),y) = 2x504 + 2y >= 2x504 + 2y = s(+(p(x504),y)) s(+(p(x504),y)) = 2x504 + 2y >= 2x504 + 2y = s(p(+(x504,y))) -(s(p(x506))) = x506 >= x506 = p(-(p(x506))) p(-(p(x506))) = x506 >= x506 = p(s(-(x506))) +(x,p(s(x507))) = 2x + 2x507 >= 2x + 2x507 = p(+(x,s(x507))) p(+(x,s(x507))) = 2x + 2x507 >= 2x + 2x507 = p(s(+(x,x507))) +(p(s(x508)),y) = 2x508 + 2y >= 2x508 + 2y = p(+(s(x508),y)) p(+(s(x508),y)) = 2x508 + 2y >= 2x508 + 2y = p(s(+(x508,y))) -(p(s(x510))) = x510 >= x510 = s(-(s(x510))) s(-(s(x510))) = x510 >= x510 = s(p(-(x510))) +(x,0()) = 2x + 4 >= 2x + 4 = +(0(),x) +(x,0()) = 2x + 4 >= x = x +(0(),x) = 2x + 4 >= x = x +(x,s(y)) = 2x + 2y >= 2x + 2y = +(s(y),x) +(x,s(y)) = 2x + 2y >= 2x + 2y = s(+(x,y)) +(s(y),x) = 2x + 2y >= 2x + 2y = s(+(y,x)) s(+(x,y)) = 2x + 2y >= 2x + 2y = s(+(y,x)) +(x,p(y)) = 2x + 2y >= 2x + 2y = +(p(y),x) +(x,p(y)) = 2x + 2y >= 2x + 2y = p(+(x,y)) +(p(y),x) = 2x + 2y >= 2x + 2y = p(+(y,x)) p(+(x,y)) = 2x + 2y >= 2x + 2y = p(+(y,x)) +(0(),y) = 2y + 4 >= 2y + 4 = +(y,0()) +(0(),y) = 2y + 4 >= y = y +(y,0()) = 2y + 4 >= y = y +(s(x),y) = 2x + 2y >= 2x + 2y = +(y,s(x)) +(s(x),y) = 2x + 2y >= 2x + 2y = s(+(x,y)) +(y,s(x)) = 2x + 2y >= 2x + 2y = s(+(y,x)) s(+(x,y)) = 2x + 2y >= 2x + 2y = s(+(y,x)) +(p(x),y) = 2x + 2y >= 2x + 2y = +(y,p(x)) +(p(x),y) = 2x + 2y >= 2x + 2y = p(+(x,y)) +(y,p(x)) = 2x + 2y >= 2x + 2y = p(+(y,x)) p(+(x,y)) = 2x + 2y >= 2x + 2y = p(+(y,x)) -(+(x,y)) = 2x + 2y >= 2x + 2y = -(+(y,x)) -(+(x,y)) = 2x + 2y >= 2x + 2y = +(-(x),-(y)) -(+(y,x)) = 2x + 2y >= 2x + 2y = +(-(y),-(x)) +(-(x),-(y)) = 2x + 2y >= 2x + 2y = +(-(y),-(x)) -(0()) = 2 >= 2 = 0() -(s(x)) = x >= x = p(-(x)) -(p(x)) = x >= x = s(-(x)) +(x,y) = 2x + 2y >= 2x + 2y = +(y,x) problem: strict: +(s(x),0()) -> s(+(x,0())) +(p(x),0()) -> p(+(x,0())) +(x,0()) -> +(0(),x) -(+(x,0())) -> +(-(x),-(0())) +(-(x),-(0())) -> +(-(x),0()) +(0(),s(x459)) -> s(+(0(),x459)) +(s(x),s(x461)) -> s(+(s(x),x461)) +(s(x),s(x461)) -> s(+(x,s(x461))) s(+(s(x),x461)) -> s(s(+(x,x461))) s(+(x,s(x461))) -> s(s(+(x,x461))) +(p(x),s(x463)) -> s(+(p(x),x463)) +(p(x),s(x463)) -> p(+(x,s(x463))) s(+(p(x),x463)) -> s(p(+(x,x463))) p(+(x,s(x463))) -> p(s(+(x,x463))) +(x,s(x465)) -> s(+(x,x465)) +(x,s(x465)) -> +(s(x465),x) s(+(x,x465)) -> s(+(x465,x)) +(s(x465),x) -> s(+(x465,x)) -(+(x,s(x467))) -> -(s(+(x,x467))) -(+(x,s(x467))) -> +(-(x),-(s(x467))) -(s(+(x,x467))) -> p(-(+(x,x467))) p(-(+(x,x467))) -> p(+(-(x),-(x467))) +(-(x),-(s(x467))) -> +(-(x),p(-(x467))) +(-(x),p(-(x467))) -> p(+(-(x),-(x467))) +(0(),p(x469)) -> p(+(0(),x469)) +(s(x),p(x471)) -> p(+(s(x),x471)) +(s(x),p(x471)) -> s(+(x,p(x471))) p(+(s(x),x471)) -> p(s(+(x,x471))) s(+(x,p(x471))) -> s(p(+(x,x471))) +(p(x),p(x473)) -> p(+(p(x),x473)) +(p(x),p(x473)) -> p(+(x,p(x473))) p(+(p(x),x473)) -> p(p(+(x,x473))) p(+(x,p(x473))) -> p(p(+(x,x473))) +(x,p(x475)) -> p(+(x,x475)) +(x,p(x475)) -> +(p(x475),x) p(+(x,x475)) -> p(+(x475,x)) +(p(x475),x) -> p(+(x475,x)) -(+(x,p(x477))) -> -(p(+(x,x477))) -(+(x,p(x477))) -> +(-(x),-(p(x477))) -(p(+(x,x477))) -> s(-(+(x,x477))) s(-(+(x,x477))) -> s(+(-(x),-(x477))) +(-(x),-(p(x477))) -> +(-(x),s(-(x477))) +(-(x),s(-(x477))) -> s(+(-(x),-(x477))) +(0(),s(y)) -> s(+(0(),y)) +(0(),p(y)) -> p(+(0(),y)) +(0(),y) -> +(y,0()) -(+(0(),y)) -> +(-(0()),-(y)) +(-(0()),-(y)) -> +(0(),-(y)) +(s(x483),0()) -> s(+(x483,0())) +(s(x485),s(y)) -> s(+(x485,s(y))) +(s(x485),s(y)) -> s(+(s(x485),y)) s(+(x485,s(y))) -> s(s(+(x485,y))) s(+(s(x485),y)) -> s(s(+(x485,y))) +(s(x487),p(y)) -> s(+(x487,p(y))) +(s(x487),p(y)) -> p(+(s(x487),y)) s(+(x487,p(y))) -> s(p(+(x487,y))) p(+(s(x487),y)) -> p(s(+(x487,y))) +(s(x489),y) -> s(+(x489,y)) +(s(x489),y) -> +(y,s(x489)) s(+(x489,y)) -> s(+(y,x489)) +(y,s(x489)) -> s(+(y,x489)) -(+(s(x491),y)) -> -(s(+(x491,y))) -(+(s(x491),y)) -> +(-(s(x491)),-(y)) -(s(+(x491,y))) -> p(-(+(x491,y))) p(-(+(x491,y))) -> p(+(-(x491),-(y))) +(-(s(x491)),-(y)) -> +(p(-(x491)),-(y)) +(p(-(x491)),-(y)) -> p(+(-(x491),-(y))) +(p(x493),0()) -> p(+(x493,0())) +(p(x495),s(y)) -> p(+(x495,s(y))) +(p(x495),s(y)) -> s(+(p(x495),y)) p(+(x495,s(y))) -> p(s(+(x495,y))) s(+(p(x495),y)) -> s(p(+(x495,y))) +(p(x497),p(y)) -> p(+(x497,p(y))) +(p(x497),p(y)) -> p(+(p(x497),y)) p(+(x497,p(y))) -> p(p(+(x497,y))) p(+(p(x497),y)) -> p(p(+(x497,y))) +(p(x499),y) -> p(+(x499,y)) +(p(x499),y) -> +(y,p(x499)) p(+(x499,y)) -> p(+(y,x499)) +(y,p(x499)) -> p(+(y,x499)) -(+(p(x501),y)) -> -(p(+(x501,y))) -(+(p(x501),y)) -> +(-(p(x501)),-(y)) -(p(+(x501,y))) -> s(-(+(x501,y))) s(-(+(x501,y))) -> s(+(-(x501),-(y))) +(-(p(x501)),-(y)) -> +(s(-(x501)),-(y)) +(s(-(x501)),-(y)) -> s(+(-(x501),-(y))) +(x,s(p(x503))) -> s(+(x,p(x503))) s(+(x,p(x503))) -> s(p(+(x,x503))) +(s(p(x504)),y) -> s(+(p(x504),y)) s(+(p(x504),y)) -> s(p(+(x504,y))) -(s(p(x506))) -> p(-(p(x506))) p(-(p(x506))) -> p(s(-(x506))) +(x,p(s(x507))) -> p(+(x,s(x507))) p(+(x,s(x507))) -> p(s(+(x,x507))) +(p(s(x508)),y) -> p(+(s(x508),y)) p(+(s(x508),y)) -> p(s(+(x508,y))) -(p(s(x510))) -> s(-(s(x510))) s(-(s(x510))) -> s(p(-(x510))) +(x,0()) -> +(0(),x) +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) +(x,p(y)) -> +(p(y),x) +(x,p(y)) -> p(+(x,y)) +(p(y),x) -> p(+(y,x)) p(+(x,y)) -> p(+(y,x)) +(0(),y) -> +(y,0()) +(s(x),y) -> +(y,s(x)) +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) +(p(x),y) -> +(y,p(x)) +(p(x),y) -> p(+(x,y)) +(y,p(x)) -> p(+(y,x)) p(+(x,y)) -> p(+(y,x)) -(+(x,y)) -> -(+(y,x)) -(+(x,y)) -> +(-(x),-(y)) -(+(y,x)) -> +(-(y),-(x)) +(-(x),-(y)) -> +(-(y),-(x)) weak: +(x,s(y)) -> s(+(x,y)) +(x,p(y)) -> p(+(x,y)) +(s(x),y) -> s(+(x,y)) +(p(x),y) -> p(+(x,y)) -(0()) -> 0() -(s(x)) -> p(-(x)) -(p(x)) -> s(-(x)) +(x,y) -> +(y,x) -(+(x,y)) -> +(-(x),-(y)) Matrix Interpretation Processor: dim=1 interpretation: [-](x0) = 2x0, [p](x0) = x0, [s](x0) = x0, [+](x0, x1) = 4x0 + 4x1, [0] = 1 orientation: +(s(x),0()) = 4x + 4 >= 4x + 4 = s(+(x,0())) +(p(x),0()) = 4x + 4 >= 4x + 4 = p(+(x,0())) +(x,0()) = 4x + 4 >= 4x + 4 = +(0(),x) -(+(x,0())) = 8x + 8 >= 8x + 8 = +(-(x),-(0())) +(-(x),-(0())) = 8x + 8 >= 8x + 4 = +(-(x),0()) +(0(),s(x459)) = 4x459 + 4 >= 4x459 + 4 = s(+(0(),x459)) +(s(x),s(x461)) = 4x + 4x461 >= 4x + 4x461 = s(+(s(x),x461)) +(s(x),s(x461)) = 4x + 4x461 >= 4x + 4x461 = s(+(x,s(x461))) s(+(s(x),x461)) = 4x + 4x461 >= 4x + 4x461 = s(s(+(x,x461))) s(+(x,s(x461))) = 4x + 4x461 >= 4x + 4x461 = s(s(+(x,x461))) +(p(x),s(x463)) = 4x + 4x463 >= 4x + 4x463 = s(+(p(x),x463)) +(p(x),s(x463)) = 4x + 4x463 >= 4x + 4x463 = p(+(x,s(x463))) s(+(p(x),x463)) = 4x + 4x463 >= 4x + 4x463 = s(p(+(x,x463))) p(+(x,s(x463))) = 4x + 4x463 >= 4x + 4x463 = p(s(+(x,x463))) +(x,s(x465)) = 4x + 4x465 >= 4x + 4x465 = s(+(x,x465)) +(x,s(x465)) = 4x + 4x465 >= 4x + 4x465 = +(s(x465),x) s(+(x,x465)) = 4x + 4x465 >= 4x + 4x465 = s(+(x465,x)) +(s(x465),x) = 4x + 4x465 >= 4x + 4x465 = s(+(x465,x)) -(+(x,s(x467))) = 8x + 8x467 >= 8x + 8x467 = -(s(+(x,x467))) -(+(x,s(x467))) = 8x + 8x467 >= 8x + 8x467 = +(-(x),-(s(x467))) -(s(+(x,x467))) = 8x + 8x467 >= 8x + 8x467 = p(-(+(x,x467))) p(-(+(x,x467))) = 8x + 8x467 >= 8x + 8x467 = p(+(-(x),-(x467))) +(-(x),-(s(x467))) = 8x + 8x467 >= 8x + 8x467 = +(-(x),p(-(x467))) +(-(x),p(-(x467))) = 8x + 8x467 >= 8x + 8x467 = p(+(-(x),-(x467))) +(0(),p(x469)) = 4x469 + 4 >= 4x469 + 4 = p(+(0(),x469)) +(s(x),p(x471)) = 4x + 4x471 >= 4x + 4x471 = p(+(s(x),x471)) +(s(x),p(x471)) = 4x + 4x471 >= 4x + 4x471 = s(+(x,p(x471))) p(+(s(x),x471)) = 4x + 4x471 >= 4x + 4x471 = p(s(+(x,x471))) s(+(x,p(x471))) = 4x + 4x471 >= 4x + 4x471 = s(p(+(x,x471))) +(p(x),p(x473)) = 4x + 4x473 >= 4x + 4x473 = p(+(p(x),x473)) +(p(x),p(x473)) = 4x + 4x473 >= 4x + 4x473 = p(+(x,p(x473))) p(+(p(x),x473)) = 4x + 4x473 >= 4x + 4x473 = p(p(+(x,x473))) p(+(x,p(x473))) = 4x + 4x473 >= 4x + 4x473 = p(p(+(x,x473))) +(x,p(x475)) = 4x + 4x475 >= 4x + 4x475 = p(+(x,x475)) +(x,p(x475)) = 4x + 4x475 >= 4x + 4x475 = +(p(x475),x) p(+(x,x475)) = 4x + 4x475 >= 4x + 4x475 = p(+(x475,x)) +(p(x475),x) = 4x + 4x475 >= 4x + 4x475 = p(+(x475,x)) -(+(x,p(x477))) = 8x + 8x477 >= 8x + 8x477 = -(p(+(x,x477))) -(+(x,p(x477))) = 8x + 8x477 >= 8x + 8x477 = +(-(x),-(p(x477))) -(p(+(x,x477))) = 8x + 8x477 >= 8x + 8x477 = s(-(+(x,x477))) s(-(+(x,x477))) = 8x + 8x477 >= 8x + 8x477 = s(+(-(x),-(x477))) +(-(x),-(p(x477))) = 8x + 8x477 >= 8x + 8x477 = +(-(x),s(-(x477))) +(-(x),s(-(x477))) = 8x + 8x477 >= 8x + 8x477 = s(+(-(x),-(x477))) +(0(),s(y)) = 4y + 4 >= 4y + 4 = s(+(0(),y)) +(0(),p(y)) = 4y + 4 >= 4y + 4 = p(+(0(),y)) +(0(),y) = 4y + 4 >= 4y + 4 = +(y,0()) -(+(0(),y)) = 8y + 8 >= 8y + 8 = +(-(0()),-(y)) +(-(0()),-(y)) = 8y + 8 >= 8y + 4 = +(0(),-(y)) +(s(x483),0()) = 4x483 + 4 >= 4x483 + 4 = s(+(x483,0())) +(s(x485),s(y)) = 4x485 + 4y >= 4x485 + 4y = s(+(x485,s(y))) +(s(x485),s(y)) = 4x485 + 4y >= 4x485 + 4y = s(+(s(x485),y)) s(+(x485,s(y))) = 4x485 + 4y >= 4x485 + 4y = s(s(+(x485,y))) s(+(s(x485),y)) = 4x485 + 4y >= 4x485 + 4y = s(s(+(x485,y))) +(s(x487),p(y)) = 4x487 + 4y >= 4x487 + 4y = s(+(x487,p(y))) +(s(x487),p(y)) = 4x487 + 4y >= 4x487 + 4y = p(+(s(x487),y)) s(+(x487,p(y))) = 4x487 + 4y >= 4x487 + 4y = s(p(+(x487,y))) p(+(s(x487),y)) = 4x487 + 4y >= 4x487 + 4y = p(s(+(x487,y))) +(s(x489),y) = 4x489 + 4y >= 4x489 + 4y = s(+(x489,y)) +(s(x489),y) = 4x489 + 4y >= 4x489 + 4y = +(y,s(x489)) s(+(x489,y)) = 4x489 + 4y >= 4x489 + 4y = s(+(y,x489)) +(y,s(x489)) = 4x489 + 4y >= 4x489 + 4y = s(+(y,x489)) -(+(s(x491),y)) = 8x491 + 8y >= 8x491 + 8y = -(s(+(x491,y))) -(+(s(x491),y)) = 8x491 + 8y >= 8x491 + 8y = +(-(s(x491)),-(y)) -(s(+(x491,y))) = 8x491 + 8y >= 8x491 + 8y = p(-(+(x491,y))) p(-(+(x491,y))) = 8x491 + 8y >= 8x491 + 8y = p(+(-(x491),-(y))) +(-(s(x491)),-(y)) = 8x491 + 8y >= 8x491 + 8y = +(p(-(x491)),-(y)) +(p(-(x491)),-(y)) = 8x491 + 8y >= 8x491 + 8y = p(+(-(x491),-(y))) +(p(x493),0()) = 4x493 + 4 >= 4x493 + 4 = p(+(x493,0())) +(p(x495),s(y)) = 4x495 + 4y >= 4x495 + 4y = p(+(x495,s(y))) +(p(x495),s(y)) = 4x495 + 4y >= 4x495 + 4y = s(+(p(x495),y)) p(+(x495,s(y))) = 4x495 + 4y >= 4x495 + 4y = p(s(+(x495,y))) s(+(p(x495),y)) = 4x495 + 4y >= 4x495 + 4y = s(p(+(x495,y))) +(p(x497),p(y)) = 4x497 + 4y >= 4x497 + 4y = p(+(x497,p(y))) +(p(x497),p(y)) = 4x497 + 4y >= 4x497 + 4y = p(+(p(x497),y)) p(+(x497,p(y))) = 4x497 + 4y >= 4x497 + 4y = p(p(+(x497,y))) p(+(p(x497),y)) = 4x497 + 4y >= 4x497 + 4y = p(p(+(x497,y))) +(p(x499),y) = 4x499 + 4y >= 4x499 + 4y = p(+(x499,y)) +(p(x499),y) = 4x499 + 4y >= 4x499 + 4y = +(y,p(x499)) p(+(x499,y)) = 4x499 + 4y >= 4x499 + 4y = p(+(y,x499)) +(y,p(x499)) = 4x499 + 4y >= 4x499 + 4y = p(+(y,x499)) -(+(p(x501),y)) = 8x501 + 8y >= 8x501 + 8y = -(p(+(x501,y))) -(+(p(x501),y)) = 8x501 + 8y >= 8x501 + 8y = +(-(p(x501)),-(y)) -(p(+(x501,y))) = 8x501 + 8y >= 8x501 + 8y = s(-(+(x501,y))) s(-(+(x501,y))) = 8x501 + 8y >= 8x501 + 8y = s(+(-(x501),-(y))) +(-(p(x501)),-(y)) = 8x501 + 8y >= 8x501 + 8y = +(s(-(x501)),-(y)) +(s(-(x501)),-(y)) = 8x501 + 8y >= 8x501 + 8y = s(+(-(x501),-(y))) +(x,s(p(x503))) = 4x + 4x503 >= 4x + 4x503 = s(+(x,p(x503))) s(+(x,p(x503))) = 4x + 4x503 >= 4x + 4x503 = s(p(+(x,x503))) +(s(p(x504)),y) = 4x504 + 4y >= 4x504 + 4y = s(+(p(x504),y)) s(+(p(x504),y)) = 4x504 + 4y >= 4x504 + 4y = s(p(+(x504,y))) -(s(p(x506))) = 2x506 >= 2x506 = p(-(p(x506))) p(-(p(x506))) = 2x506 >= 2x506 = p(s(-(x506))) +(x,p(s(x507))) = 4x + 4x507 >= 4x + 4x507 = p(+(x,s(x507))) p(+(x,s(x507))) = 4x + 4x507 >= 4x + 4x507 = p(s(+(x,x507))) +(p(s(x508)),y) = 4x508 + 4y >= 4x508 + 4y = p(+(s(x508),y)) p(+(s(x508),y)) = 4x508 + 4y >= 4x508 + 4y = p(s(+(x508,y))) -(p(s(x510))) = 2x510 >= 2x510 = s(-(s(x510))) s(-(s(x510))) = 2x510 >= 2x510 = s(p(-(x510))) +(x,0()) = 4x + 4 >= 4x + 4 = +(0(),x) +(x,s(y)) = 4x + 4y >= 4x + 4y = +(s(y),x) +(x,s(y)) = 4x + 4y >= 4x + 4y = s(+(x,y)) +(s(y),x) = 4x + 4y >= 4x + 4y = s(+(y,x)) s(+(x,y)) = 4x + 4y >= 4x + 4y = s(+(y,x)) +(x,p(y)) = 4x + 4y >= 4x + 4y = +(p(y),x) +(x,p(y)) = 4x + 4y >= 4x + 4y = p(+(x,y)) +(p(y),x) = 4x + 4y >= 4x + 4y = p(+(y,x)) p(+(x,y)) = 4x + 4y >= 4x + 4y = p(+(y,x)) +(0(),y) = 4y + 4 >= 4y + 4 = +(y,0()) +(s(x),y) = 4x + 4y >= 4x + 4y = +(y,s(x)) +(s(x),y) = 4x + 4y >= 4x + 4y = s(+(x,y)) +(y,s(x)) = 4x + 4y >= 4x + 4y = s(+(y,x)) s(+(x,y)) = 4x + 4y >= 4x + 4y = s(+(y,x)) +(p(x),y) = 4x + 4y >= 4x + 4y = +(y,p(x)) +(p(x),y) = 4x + 4y >= 4x + 4y = p(+(x,y)) +(y,p(x)) = 4x + 4y >= 4x + 4y = p(+(y,x)) p(+(x,y)) = 4x + 4y >= 4x + 4y = p(+(y,x)) -(+(x,y)) = 8x + 8y >= 8x + 8y = -(+(y,x)) -(+(x,y)) = 8x + 8y >= 8x + 8y = +(-(x),-(y)) -(+(y,x)) = 8x + 8y >= 8x + 8y = +(-(y),-(x)) +(-(x),-(y)) = 8x + 8y >= 8x + 8y = +(-(y),-(x)) -(0()) = 2 >= 1 = 0() -(s(x)) = 2x >= 2x = p(-(x)) -(p(x)) = 2x >= 2x = s(-(x)) +(x,y) = 4x + 4y >= 4x + 4y = +(y,x) problem: strict: +(s(x),0()) -> s(+(x,0())) +(p(x),0()) -> p(+(x,0())) +(x,0()) -> +(0(),x) -(+(x,0())) -> +(-(x),-(0())) +(0(),s(x459)) -> s(+(0(),x459)) +(s(x),s(x461)) -> s(+(s(x),x461)) +(s(x),s(x461)) -> s(+(x,s(x461))) s(+(s(x),x461)) -> s(s(+(x,x461))) s(+(x,s(x461))) -> s(s(+(x,x461))) +(p(x),s(x463)) -> s(+(p(x),x463)) +(p(x),s(x463)) -> p(+(x,s(x463))) s(+(p(x),x463)) -> s(p(+(x,x463))) p(+(x,s(x463))) -> p(s(+(x,x463))) +(x,s(x465)) -> s(+(x,x465)) +(x,s(x465)) -> +(s(x465),x) s(+(x,x465)) -> s(+(x465,x)) +(s(x465),x) -> s(+(x465,x)) -(+(x,s(x467))) -> -(s(+(x,x467))) -(+(x,s(x467))) -> +(-(x),-(s(x467))) -(s(+(x,x467))) -> p(-(+(x,x467))) p(-(+(x,x467))) -> p(+(-(x),-(x467))) +(-(x),-(s(x467))) -> +(-(x),p(-(x467))) +(-(x),p(-(x467))) -> p(+(-(x),-(x467))) +(0(),p(x469)) -> p(+(0(),x469)) +(s(x),p(x471)) -> p(+(s(x),x471)) +(s(x),p(x471)) -> s(+(x,p(x471))) p(+(s(x),x471)) -> p(s(+(x,x471))) s(+(x,p(x471))) -> s(p(+(x,x471))) +(p(x),p(x473)) -> p(+(p(x),x473)) +(p(x),p(x473)) -> p(+(x,p(x473))) p(+(p(x),x473)) -> p(p(+(x,x473))) p(+(x,p(x473))) -> p(p(+(x,x473))) +(x,p(x475)) -> p(+(x,x475)) +(x,p(x475)) -> +(p(x475),x) p(+(x,x475)) -> p(+(x475,x)) +(p(x475),x) -> p(+(x475,x)) -(+(x,p(x477))) -> -(p(+(x,x477))) -(+(x,p(x477))) -> +(-(x),-(p(x477))) -(p(+(x,x477))) -> s(-(+(x,x477))) s(-(+(x,x477))) -> s(+(-(x),-(x477))) +(-(x),-(p(x477))) -> +(-(x),s(-(x477))) +(-(x),s(-(x477))) -> s(+(-(x),-(x477))) +(0(),s(y)) -> s(+(0(),y)) +(0(),p(y)) -> p(+(0(),y)) +(0(),y) -> +(y,0()) -(+(0(),y)) -> +(-(0()),-(y)) +(s(x483),0()) -> s(+(x483,0())) +(s(x485),s(y)) -> s(+(x485,s(y))) +(s(x485),s(y)) -> s(+(s(x485),y)) s(+(x485,s(y))) -> s(s(+(x485,y))) s(+(s(x485),y)) -> s(s(+(x485,y))) +(s(x487),p(y)) -> s(+(x487,p(y))) +(s(x487),p(y)) -> p(+(s(x487),y)) s(+(x487,p(y))) -> s(p(+(x487,y))) p(+(s(x487),y)) -> p(s(+(x487,y))) +(s(x489),y) -> s(+(x489,y)) +(s(x489),y) -> +(y,s(x489)) s(+(x489,y)) -> s(+(y,x489)) +(y,s(x489)) -> s(+(y,x489)) -(+(s(x491),y)) -> -(s(+(x491,y))) -(+(s(x491),y)) -> +(-(s(x491)),-(y)) -(s(+(x491,y))) -> p(-(+(x491,y))) p(-(+(x491,y))) -> p(+(-(x491),-(y))) +(-(s(x491)),-(y)) -> +(p(-(x491)),-(y)) +(p(-(x491)),-(y)) -> p(+(-(x491),-(y))) +(p(x493),0()) -> p(+(x493,0())) +(p(x495),s(y)) -> p(+(x495,s(y))) +(p(x495),s(y)) -> s(+(p(x495),y)) p(+(x495,s(y))) -> p(s(+(x495,y))) s(+(p(x495),y)) -> s(p(+(x495,y))) +(p(x497),p(y)) -> p(+(x497,p(y))) +(p(x497),p(y)) -> p(+(p(x497),y)) p(+(x497,p(y))) -> p(p(+(x497,y))) p(+(p(x497),y)) -> p(p(+(x497,y))) +(p(x499),y) -> p(+(x499,y)) +(p(x499),y) -> +(y,p(x499)) p(+(x499,y)) -> p(+(y,x499)) +(y,p(x499)) -> p(+(y,x499)) -(+(p(x501),y)) -> -(p(+(x501,y))) -(+(p(x501),y)) -> +(-(p(x501)),-(y)) -(p(+(x501,y))) -> s(-(+(x501,y))) s(-(+(x501,y))) -> s(+(-(x501),-(y))) +(-(p(x501)),-(y)) -> +(s(-(x501)),-(y)) +(s(-(x501)),-(y)) -> s(+(-(x501),-(y))) +(x,s(p(x503))) -> s(+(x,p(x503))) s(+(x,p(x503))) -> s(p(+(x,x503))) +(s(p(x504)),y) -> s(+(p(x504),y)) s(+(p(x504),y)) -> s(p(+(x504,y))) -(s(p(x506))) -> p(-(p(x506))) p(-(p(x506))) -> p(s(-(x506))) +(x,p(s(x507))) -> p(+(x,s(x507))) p(+(x,s(x507))) -> p(s(+(x,x507))) +(p(s(x508)),y) -> p(+(s(x508),y)) p(+(s(x508),y)) -> p(s(+(x508,y))) -(p(s(x510))) -> s(-(s(x510))) s(-(s(x510))) -> s(p(-(x510))) +(x,0()) -> +(0(),x) +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) +(x,p(y)) -> +(p(y),x) +(x,p(y)) -> p(+(x,y)) +(p(y),x) -> p(+(y,x)) p(+(x,y)) -> p(+(y,x)) +(0(),y) -> +(y,0()) +(s(x),y) -> +(y,s(x)) +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) +(p(x),y) -> +(y,p(x)) +(p(x),y) -> p(+(x,y)) +(y,p(x)) -> p(+(y,x)) p(+(x,y)) -> p(+(y,x)) -(+(x,y)) -> -(+(y,x)) -(+(x,y)) -> +(-(x),-(y)) -(+(y,x)) -> +(-(y),-(x)) +(-(x),-(y)) -> +(-(y),-(x)) weak: +(x,s(y)) -> s(+(x,y)) +(x,p(y)) -> p(+(x,y)) +(s(x),y) -> s(+(x,y)) +(p(x),y) -> p(+(x,y)) -(s(x)) -> p(-(x)) -(p(x)) -> s(-(x)) +(x,y) -> +(y,x) -(+(x,y)) -> +(-(x),-(y)) Matrix Interpretation Processor: dim=1 interpretation: [-](x0) = 4x0, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [+](x0, x1) = x0 + x1, [0] = 0 orientation: +(s(x),0()) = x + 1 >= x + 1 = s(+(x,0())) +(p(x),0()) = x + 1 >= x + 1 = p(+(x,0())) +(x,0()) = x >= x = +(0(),x) -(+(x,0())) = 4x >= 4x = +(-(x),-(0())) +(0(),s(x459)) = x459 + 1 >= x459 + 1 = s(+(0(),x459)) +(s(x),s(x461)) = x + x461 + 2 >= x + x461 + 2 = s(+(s(x),x461)) +(s(x),s(x461)) = x + x461 + 2 >= x + x461 + 2 = s(+(x,s(x461))) s(+(s(x),x461)) = x + x461 + 2 >= x + x461 + 2 = s(s(+(x,x461))) s(+(x,s(x461))) = x + x461 + 2 >= x + x461 + 2 = s(s(+(x,x461))) +(p(x),s(x463)) = x + x463 + 2 >= x + x463 + 2 = s(+(p(x),x463)) +(p(x),s(x463)) = x + x463 + 2 >= x + x463 + 2 = p(+(x,s(x463))) s(+(p(x),x463)) = x + x463 + 2 >= x + x463 + 2 = s(p(+(x,x463))) p(+(x,s(x463))) = x + x463 + 2 >= x + x463 + 2 = p(s(+(x,x463))) +(x,s(x465)) = x + x465 + 1 >= x + x465 + 1 = s(+(x,x465)) +(x,s(x465)) = x + x465 + 1 >= x + x465 + 1 = +(s(x465),x) s(+(x,x465)) = x + x465 + 1 >= x + x465 + 1 = s(+(x465,x)) +(s(x465),x) = x + x465 + 1 >= x + x465 + 1 = s(+(x465,x)) -(+(x,s(x467))) = 4x + 4x467 + 4 >= 4x + 4x467 + 4 = -(s(+(x,x467))) -(+(x,s(x467))) = 4x + 4x467 + 4 >= 4x + 4x467 + 4 = +(-(x),-(s(x467))) -(s(+(x,x467))) = 4x + 4x467 + 4 >= 4x + 4x467 + 1 = p(-(+(x,x467))) p(-(+(x,x467))) = 4x + 4x467 + 1 >= 4x + 4x467 + 1 = p(+(-(x),-(x467))) +(-(x),-(s(x467))) = 4x + 4x467 + 4 >= 4x + 4x467 + 1 = +(-(x),p(-(x467))) +(-(x),p(-(x467))) = 4x + 4x467 + 1 >= 4x + 4x467 + 1 = p(+(-(x),-(x467))) +(0(),p(x469)) = x469 + 1 >= x469 + 1 = p(+(0(),x469)) +(s(x),p(x471)) = x + x471 + 2 >= x + x471 + 2 = p(+(s(x),x471)) +(s(x),p(x471)) = x + x471 + 2 >= x + x471 + 2 = s(+(x,p(x471))) p(+(s(x),x471)) = x + x471 + 2 >= x + x471 + 2 = p(s(+(x,x471))) s(+(x,p(x471))) = x + x471 + 2 >= x + x471 + 2 = s(p(+(x,x471))) +(p(x),p(x473)) = x + x473 + 2 >= x + x473 + 2 = p(+(p(x),x473)) +(p(x),p(x473)) = x + x473 + 2 >= x + x473 + 2 = p(+(x,p(x473))) p(+(p(x),x473)) = x + x473 + 2 >= x + x473 + 2 = p(p(+(x,x473))) p(+(x,p(x473))) = x + x473 + 2 >= x + x473 + 2 = p(p(+(x,x473))) +(x,p(x475)) = x + x475 + 1 >= x + x475 + 1 = p(+(x,x475)) +(x,p(x475)) = x + x475 + 1 >= x + x475 + 1 = +(p(x475),x) p(+(x,x475)) = x + x475 + 1 >= x + x475 + 1 = p(+(x475,x)) +(p(x475),x) = x + x475 + 1 >= x + x475 + 1 = p(+(x475,x)) -(+(x,p(x477))) = 4x + 4x477 + 4 >= 4x + 4x477 + 4 = -(p(+(x,x477))) -(+(x,p(x477))) = 4x + 4x477 + 4 >= 4x + 4x477 + 4 = +(-(x),-(p(x477))) -(p(+(x,x477))) = 4x + 4x477 + 4 >= 4x + 4x477 + 1 = s(-(+(x,x477))) s(-(+(x,x477))) = 4x + 4x477 + 1 >= 4x + 4x477 + 1 = s(+(-(x),-(x477))) +(-(x),-(p(x477))) = 4x + 4x477 + 4 >= 4x + 4x477 + 1 = +(-(x),s(-(x477))) +(-(x),s(-(x477))) = 4x + 4x477 + 1 >= 4x + 4x477 + 1 = s(+(-(x),-(x477))) +(0(),s(y)) = y + 1 >= y + 1 = s(+(0(),y)) +(0(),p(y)) = y + 1 >= y + 1 = p(+(0(),y)) +(0(),y) = y >= y = +(y,0()) -(+(0(),y)) = 4y >= 4y = +(-(0()),-(y)) +(s(x483),0()) = x483 + 1 >= x483 + 1 = s(+(x483,0())) +(s(x485),s(y)) = x485 + y + 2 >= x485 + y + 2 = s(+(x485,s(y))) +(s(x485),s(y)) = x485 + y + 2 >= x485 + y + 2 = s(+(s(x485),y)) s(+(x485,s(y))) = x485 + y + 2 >= x485 + y + 2 = s(s(+(x485,y))) s(+(s(x485),y)) = x485 + y + 2 >= x485 + y + 2 = s(s(+(x485,y))) +(s(x487),p(y)) = x487 + y + 2 >= x487 + y + 2 = s(+(x487,p(y))) +(s(x487),p(y)) = x487 + y + 2 >= x487 + y + 2 = p(+(s(x487),y)) s(+(x487,p(y))) = x487 + y + 2 >= x487 + y + 2 = s(p(+(x487,y))) p(+(s(x487),y)) = x487 + y + 2 >= x487 + y + 2 = p(s(+(x487,y))) +(s(x489),y) = x489 + y + 1 >= x489 + y + 1 = s(+(x489,y)) +(s(x489),y) = x489 + y + 1 >= x489 + y + 1 = +(y,s(x489)) s(+(x489,y)) = x489 + y + 1 >= x489 + y + 1 = s(+(y,x489)) +(y,s(x489)) = x489 + y + 1 >= x489 + y + 1 = s(+(y,x489)) -(+(s(x491),y)) = 4x491 + 4y + 4 >= 4x491 + 4y + 4 = -(s(+(x491,y))) -(+(s(x491),y)) = 4x491 + 4y + 4 >= 4x491 + 4y + 4 = +(-(s(x491)),-(y)) -(s(+(x491,y))) = 4x491 + 4y + 4 >= 4x491 + 4y + 1 = p(-(+(x491,y))) p(-(+(x491,y))) = 4x491 + 4y + 1 >= 4x491 + 4y + 1 = p(+(-(x491),-(y))) +(-(s(x491)),-(y)) = 4x491 + 4y + 4 >= 4x491 + 4y + 1 = +(p(-(x491)),-(y)) +(p(-(x491)),-(y)) = 4x491 + 4y + 1 >= 4x491 + 4y + 1 = p(+(-(x491),-(y))) +(p(x493),0()) = x493 + 1 >= x493 + 1 = p(+(x493,0())) +(p(x495),s(y)) = x495 + y + 2 >= x495 + y + 2 = p(+(x495,s(y))) +(p(x495),s(y)) = x495 + y + 2 >= x495 + y + 2 = s(+(p(x495),y)) p(+(x495,s(y))) = x495 + y + 2 >= x495 + y + 2 = p(s(+(x495,y))) s(+(p(x495),y)) = x495 + y + 2 >= x495 + y + 2 = s(p(+(x495,y))) +(p(x497),p(y)) = x497 + y + 2 >= x497 + y + 2 = p(+(x497,p(y))) +(p(x497),p(y)) = x497 + y + 2 >= x497 + y + 2 = p(+(p(x497),y)) p(+(x497,p(y))) = x497 + y + 2 >= x497 + y + 2 = p(p(+(x497,y))) p(+(p(x497),y)) = x497 + y + 2 >= x497 + y + 2 = p(p(+(x497,y))) +(p(x499),y) = x499 + y + 1 >= x499 + y + 1 = p(+(x499,y)) +(p(x499),y) = x499 + y + 1 >= x499 + y + 1 = +(y,p(x499)) p(+(x499,y)) = x499 + y + 1 >= x499 + y + 1 = p(+(y,x499)) +(y,p(x499)) = x499 + y + 1 >= x499 + y + 1 = p(+(y,x499)) -(+(p(x501),y)) = 4x501 + 4y + 4 >= 4x501 + 4y + 4 = -(p(+(x501,y))) -(+(p(x501),y)) = 4x501 + 4y + 4 >= 4x501 + 4y + 4 = +(-(p(x501)),-(y)) -(p(+(x501,y))) = 4x501 + 4y + 4 >= 4x501 + 4y + 1 = s(-(+(x501,y))) s(-(+(x501,y))) = 4x501 + 4y + 1 >= 4x501 + 4y + 1 = s(+(-(x501),-(y))) +(-(p(x501)),-(y)) = 4x501 + 4y + 4 >= 4x501 + 4y + 1 = +(s(-(x501)),-(y)) +(s(-(x501)),-(y)) = 4x501 + 4y + 1 >= 4x501 + 4y + 1 = s(+(-(x501),-(y))) +(x,s(p(x503))) = x + x503 + 2 >= x + x503 + 2 = s(+(x,p(x503))) s(+(x,p(x503))) = x + x503 + 2 >= x + x503 + 2 = s(p(+(x,x503))) +(s(p(x504)),y) = x504 + y + 2 >= x504 + y + 2 = s(+(p(x504),y)) s(+(p(x504),y)) = x504 + y + 2 >= x504 + y + 2 = s(p(+(x504,y))) -(s(p(x506))) = 4x506 + 8 >= 4x506 + 5 = p(-(p(x506))) p(-(p(x506))) = 4x506 + 5 >= 4x506 + 2 = p(s(-(x506))) +(x,p(s(x507))) = x + x507 + 2 >= x + x507 + 2 = p(+(x,s(x507))) p(+(x,s(x507))) = x + x507 + 2 >= x + x507 + 2 = p(s(+(x,x507))) +(p(s(x508)),y) = x508 + y + 2 >= x508 + y + 2 = p(+(s(x508),y)) p(+(s(x508),y)) = x508 + y + 2 >= x508 + y + 2 = p(s(+(x508,y))) -(p(s(x510))) = 4x510 + 8 >= 4x510 + 5 = s(-(s(x510))) s(-(s(x510))) = 4x510 + 5 >= 4x510 + 2 = s(p(-(x510))) +(x,0()) = x >= x = +(0(),x) +(x,s(y)) = x + y + 1 >= x + y + 1 = +(s(y),x) +(x,s(y)) = x + y + 1 >= x + y + 1 = s(+(x,y)) +(s(y),x) = x + y + 1 >= x + y + 1 = s(+(y,x)) s(+(x,y)) = x + y + 1 >= x + y + 1 = s(+(y,x)) +(x,p(y)) = x + y + 1 >= x + y + 1 = +(p(y),x) +(x,p(y)) = x + y + 1 >= x + y + 1 = p(+(x,y)) +(p(y),x) = x + y + 1 >= x + y + 1 = p(+(y,x)) p(+(x,y)) = x + y + 1 >= x + y + 1 = p(+(y,x)) +(0(),y) = y >= y = +(y,0()) +(s(x),y) = x + y + 1 >= x + y + 1 = +(y,s(x)) +(s(x),y) = x + y + 1 >= x + y + 1 = s(+(x,y)) +(y,s(x)) = x + y + 1 >= x + y + 1 = s(+(y,x)) s(+(x,y)) = x + y + 1 >= x + y + 1 = s(+(y,x)) +(p(x),y) = x + y + 1 >= x + y + 1 = +(y,p(x)) +(p(x),y) = x + y + 1 >= x + y + 1 = p(+(x,y)) +(y,p(x)) = x + y + 1 >= x + y + 1 = p(+(y,x)) p(+(x,y)) = x + y + 1 >= x + y + 1 = p(+(y,x)) -(+(x,y)) = 4x + 4y >= 4x + 4y = -(+(y,x)) -(+(x,y)) = 4x + 4y >= 4x + 4y = +(-(x),-(y)) -(+(y,x)) = 4x + 4y >= 4x + 4y = +(-(y),-(x)) +(-(x),-(y)) = 4x + 4y >= 4x + 4y = +(-(y),-(x)) -(s(x)) = 4x + 4 >= 4x + 1 = p(-(x)) -(p(x)) = 4x + 4 >= 4x + 1 = s(-(x)) +(x,y) = x + y >= x + y = +(y,x) problem: strict: +(s(x),0()) -> s(+(x,0())) +(p(x),0()) -> p(+(x,0())) +(x,0()) -> +(0(),x) -(+(x,0())) -> +(-(x),-(0())) +(0(),s(x459)) -> s(+(0(),x459)) +(s(x),s(x461)) -> s(+(s(x),x461)) +(s(x),s(x461)) -> s(+(x,s(x461))) s(+(s(x),x461)) -> s(s(+(x,x461))) s(+(x,s(x461))) -> s(s(+(x,x461))) +(p(x),s(x463)) -> s(+(p(x),x463)) +(p(x),s(x463)) -> p(+(x,s(x463))) s(+(p(x),x463)) -> s(p(+(x,x463))) p(+(x,s(x463))) -> p(s(+(x,x463))) +(x,s(x465)) -> s(+(x,x465)) +(x,s(x465)) -> +(s(x465),x) s(+(x,x465)) -> s(+(x465,x)) +(s(x465),x) -> s(+(x465,x)) -(+(x,s(x467))) -> -(s(+(x,x467))) -(+(x,s(x467))) -> +(-(x),-(s(x467))) p(-(+(x,x467))) -> p(+(-(x),-(x467))) +(-(x),p(-(x467))) -> p(+(-(x),-(x467))) +(0(),p(x469)) -> p(+(0(),x469)) +(s(x),p(x471)) -> p(+(s(x),x471)) +(s(x),p(x471)) -> s(+(x,p(x471))) p(+(s(x),x471)) -> p(s(+(x,x471))) s(+(x,p(x471))) -> s(p(+(x,x471))) +(p(x),p(x473)) -> p(+(p(x),x473)) +(p(x),p(x473)) -> p(+(x,p(x473))) p(+(p(x),x473)) -> p(p(+(x,x473))) p(+(x,p(x473))) -> p(p(+(x,x473))) +(x,p(x475)) -> p(+(x,x475)) +(x,p(x475)) -> +(p(x475),x) p(+(x,x475)) -> p(+(x475,x)) +(p(x475),x) -> p(+(x475,x)) -(+(x,p(x477))) -> -(p(+(x,x477))) -(+(x,p(x477))) -> +(-(x),-(p(x477))) s(-(+(x,x477))) -> s(+(-(x),-(x477))) +(-(x),s(-(x477))) -> s(+(-(x),-(x477))) +(0(),s(y)) -> s(+(0(),y)) +(0(),p(y)) -> p(+(0(),y)) +(0(),y) -> +(y,0()) -(+(0(),y)) -> +(-(0()),-(y)) +(s(x483),0()) -> s(+(x483,0())) +(s(x485),s(y)) -> s(+(x485,s(y))) +(s(x485),s(y)) -> s(+(s(x485),y)) s(+(x485,s(y))) -> s(s(+(x485,y))) s(+(s(x485),y)) -> s(s(+(x485,y))) +(s(x487),p(y)) -> s(+(x487,p(y))) +(s(x487),p(y)) -> p(+(s(x487),y)) s(+(x487,p(y))) -> s(p(+(x487,y))) p(+(s(x487),y)) -> p(s(+(x487,y))) +(s(x489),y) -> s(+(x489,y)) +(s(x489),y) -> +(y,s(x489)) s(+(x489,y)) -> s(+(y,x489)) +(y,s(x489)) -> s(+(y,x489)) -(+(s(x491),y)) -> -(s(+(x491,y))) -(+(s(x491),y)) -> +(-(s(x491)),-(y)) p(-(+(x491,y))) -> p(+(-(x491),-(y))) +(p(-(x491)),-(y)) -> p(+(-(x491),-(y))) +(p(x493),0()) -> p(+(x493,0())) +(p(x495),s(y)) -> p(+(x495,s(y))) +(p(x495),s(y)) -> s(+(p(x495),y)) p(+(x495,s(y))) -> p(s(+(x495,y))) s(+(p(x495),y)) -> s(p(+(x495,y))) +(p(x497),p(y)) -> p(+(x497,p(y))) +(p(x497),p(y)) -> p(+(p(x497),y)) p(+(x497,p(y))) -> p(p(+(x497,y))) p(+(p(x497),y)) -> p(p(+(x497,y))) +(p(x499),y) -> p(+(x499,y)) +(p(x499),y) -> +(y,p(x499)) p(+(x499,y)) -> p(+(y,x499)) +(y,p(x499)) -> p(+(y,x499)) -(+(p(x501),y)) -> -(p(+(x501,y))) -(+(p(x501),y)) -> +(-(p(x501)),-(y)) s(-(+(x501,y))) -> s(+(-(x501),-(y))) +(s(-(x501)),-(y)) -> s(+(-(x501),-(y))) +(x,s(p(x503))) -> s(+(x,p(x503))) s(+(x,p(x503))) -> s(p(+(x,x503))) +(s(p(x504)),y) -> s(+(p(x504),y)) s(+(p(x504),y)) -> s(p(+(x504,y))) +(x,p(s(x507))) -> p(+(x,s(x507))) p(+(x,s(x507))) -> p(s(+(x,x507))) +(p(s(x508)),y) -> p(+(s(x508),y)) p(+(s(x508),y)) -> p(s(+(x508,y))) +(x,0()) -> +(0(),x) +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) +(x,p(y)) -> +(p(y),x) +(x,p(y)) -> p(+(x,y)) +(p(y),x) -> p(+(y,x)) p(+(x,y)) -> p(+(y,x)) +(0(),y) -> +(y,0()) +(s(x),y) -> +(y,s(x)) +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) +(p(x),y) -> +(y,p(x)) +(p(x),y) -> p(+(x,y)) +(y,p(x)) -> p(+(y,x)) p(+(x,y)) -> p(+(y,x)) -(+(x,y)) -> -(+(y,x)) -(+(x,y)) -> +(-(x),-(y)) -(+(y,x)) -> +(-(y),-(x)) +(-(x),-(y)) -> +(-(y),-(x)) weak: +(x,s(y)) -> s(+(x,y)) +(x,p(y)) -> p(+(x,y)) +(s(x),y) -> s(+(x,y)) +(p(x),y) -> p(+(x,y)) +(x,y) -> +(y,x) -(+(x,y)) -> +(-(x),-(y)) Matrix Interpretation Processor: dim=1 interpretation: [-](x0) = x0, [p](x0) = x0, [s](x0) = x0 + 1, [+](x0, x1) = 2x0 + 2x1 + 2, [0] = 1 orientation: +(s(x),0()) = 2x + 6 >= 2x + 5 = s(+(x,0())) +(p(x),0()) = 2x + 4 >= 2x + 4 = p(+(x,0())) +(x,0()) = 2x + 4 >= 2x + 4 = +(0(),x) -(+(x,0())) = 2x + 4 >= 2x + 4 = +(-(x),-(0())) +(0(),s(x459)) = 2x459 + 6 >= 2x459 + 5 = s(+(0(),x459)) +(s(x),s(x461)) = 2x + 2x461 + 6 >= 2x + 2x461 + 5 = s(+(s(x),x461)) +(s(x),s(x461)) = 2x + 2x461 + 6 >= 2x + 2x461 + 5 = s(+(x,s(x461))) s(+(s(x),x461)) = 2x + 2x461 + 5 >= 2x + 2x461 + 4 = s(s(+(x,x461))) s(+(x,s(x461))) = 2x + 2x461 + 5 >= 2x + 2x461 + 4 = s(s(+(x,x461))) +(p(x),s(x463)) = 2x + 2x463 + 4 >= 2x + 2x463 + 3 = s(+(p(x),x463)) +(p(x),s(x463)) = 2x + 2x463 + 4 >= 2x + 2x463 + 4 = p(+(x,s(x463))) s(+(p(x),x463)) = 2x + 2x463 + 3 >= 2x + 2x463 + 3 = s(p(+(x,x463))) p(+(x,s(x463))) = 2x + 2x463 + 4 >= 2x + 2x463 + 3 = p(s(+(x,x463))) +(x,s(x465)) = 2x + 2x465 + 4 >= 2x + 2x465 + 3 = s(+(x,x465)) +(x,s(x465)) = 2x + 2x465 + 4 >= 2x + 2x465 + 4 = +(s(x465),x) s(+(x,x465)) = 2x + 2x465 + 3 >= 2x + 2x465 + 3 = s(+(x465,x)) +(s(x465),x) = 2x + 2x465 + 4 >= 2x + 2x465 + 3 = s(+(x465,x)) -(+(x,s(x467))) = 2x + 2x467 + 4 >= 2x + 2x467 + 3 = -(s(+(x,x467))) -(+(x,s(x467))) = 2x + 2x467 + 4 >= 2x + 2x467 + 4 = +(-(x),-(s(x467))) p(-(+(x,x467))) = 2x + 2x467 + 2 >= 2x + 2x467 + 2 = p(+(-(x),-(x467))) +(-(x),p(-(x467))) = 2x + 2x467 + 2 >= 2x + 2x467 + 2 = p(+(-(x),-(x467))) +(0(),p(x469)) = 2x469 + 4 >= 2x469 + 4 = p(+(0(),x469)) +(s(x),p(x471)) = 2x + 2x471 + 4 >= 2x + 2x471 + 4 = p(+(s(x),x471)) +(s(x),p(x471)) = 2x + 2x471 + 4 >= 2x + 2x471 + 3 = s(+(x,p(x471))) p(+(s(x),x471)) = 2x + 2x471 + 4 >= 2x + 2x471 + 3 = p(s(+(x,x471))) s(+(x,p(x471))) = 2x + 2x471 + 3 >= 2x + 2x471 + 3 = s(p(+(x,x471))) +(p(x),p(x473)) = 2x + 2x473 + 2 >= 2x + 2x473 + 2 = p(+(p(x),x473)) +(p(x),p(x473)) = 2x + 2x473 + 2 >= 2x + 2x473 + 2 = p(+(x,p(x473))) p(+(p(x),x473)) = 2x + 2x473 + 2 >= 2x + 2x473 + 2 = p(p(+(x,x473))) p(+(x,p(x473))) = 2x + 2x473 + 2 >= 2x + 2x473 + 2 = p(p(+(x,x473))) +(x,p(x475)) = 2x + 2x475 + 2 >= 2x + 2x475 + 2 = p(+(x,x475)) +(x,p(x475)) = 2x + 2x475 + 2 >= 2x + 2x475 + 2 = +(p(x475),x) p(+(x,x475)) = 2x + 2x475 + 2 >= 2x + 2x475 + 2 = p(+(x475,x)) +(p(x475),x) = 2x + 2x475 + 2 >= 2x + 2x475 + 2 = p(+(x475,x)) -(+(x,p(x477))) = 2x + 2x477 + 2 >= 2x + 2x477 + 2 = -(p(+(x,x477))) -(+(x,p(x477))) = 2x + 2x477 + 2 >= 2x + 2x477 + 2 = +(-(x),-(p(x477))) s(-(+(x,x477))) = 2x + 2x477 + 3 >= 2x + 2x477 + 3 = s(+(-(x),-(x477))) +(-(x),s(-(x477))) = 2x + 2x477 + 4 >= 2x + 2x477 + 3 = s(+(-(x),-(x477))) +(0(),s(y)) = 2y + 6 >= 2y + 5 = s(+(0(),y)) +(0(),p(y)) = 2y + 4 >= 2y + 4 = p(+(0(),y)) +(0(),y) = 2y + 4 >= 2y + 4 = +(y,0()) -(+(0(),y)) = 2y + 4 >= 2y + 4 = +(-(0()),-(y)) +(s(x483),0()) = 2x483 + 6 >= 2x483 + 5 = s(+(x483,0())) +(s(x485),s(y)) = 2x485 + 2y + 6 >= 2x485 + 2y + 5 = s(+(x485,s(y))) +(s(x485),s(y)) = 2x485 + 2y + 6 >= 2x485 + 2y + 5 = s(+(s(x485),y)) s(+(x485,s(y))) = 2x485 + 2y + 5 >= 2x485 + 2y + 4 = s(s(+(x485,y))) s(+(s(x485),y)) = 2x485 + 2y + 5 >= 2x485 + 2y + 4 = s(s(+(x485,y))) +(s(x487),p(y)) = 2x487 + 2y + 4 >= 2x487 + 2y + 3 = s(+(x487,p(y))) +(s(x487),p(y)) = 2x487 + 2y + 4 >= 2x487 + 2y + 4 = p(+(s(x487),y)) s(+(x487,p(y))) = 2x487 + 2y + 3 >= 2x487 + 2y + 3 = s(p(+(x487,y))) p(+(s(x487),y)) = 2x487 + 2y + 4 >= 2x487 + 2y + 3 = p(s(+(x487,y))) +(s(x489),y) = 2x489 + 2y + 4 >= 2x489 + 2y + 3 = s(+(x489,y)) +(s(x489),y) = 2x489 + 2y + 4 >= 2x489 + 2y + 4 = +(y,s(x489)) s(+(x489,y)) = 2x489 + 2y + 3 >= 2x489 + 2y + 3 = s(+(y,x489)) +(y,s(x489)) = 2x489 + 2y + 4 >= 2x489 + 2y + 3 = s(+(y,x489)) -(+(s(x491),y)) = 2x491 + 2y + 4 >= 2x491 + 2y + 3 = -(s(+(x491,y))) -(+(s(x491),y)) = 2x491 + 2y + 4 >= 2x491 + 2y + 4 = +(-(s(x491)),-(y)) p(-(+(x491,y))) = 2x491 + 2y + 2 >= 2x491 + 2y + 2 = p(+(-(x491),-(y))) +(p(-(x491)),-(y)) = 2x491 + 2y + 2 >= 2x491 + 2y + 2 = p(+(-(x491),-(y))) +(p(x493),0()) = 2x493 + 4 >= 2x493 + 4 = p(+(x493,0())) +(p(x495),s(y)) = 2x495 + 2y + 4 >= 2x495 + 2y + 4 = p(+(x495,s(y))) +(p(x495),s(y)) = 2x495 + 2y + 4 >= 2x495 + 2y + 3 = s(+(p(x495),y)) p(+(x495,s(y))) = 2x495 + 2y + 4 >= 2x495 + 2y + 3 = p(s(+(x495,y))) s(+(p(x495),y)) = 2x495 + 2y + 3 >= 2x495 + 2y + 3 = s(p(+(x495,y))) +(p(x497),p(y)) = 2x497 + 2y + 2 >= 2x497 + 2y + 2 = p(+(x497,p(y))) +(p(x497),p(y)) = 2x497 + 2y + 2 >= 2x497 + 2y + 2 = p(+(p(x497),y)) p(+(x497,p(y))) = 2x497 + 2y + 2 >= 2x497 + 2y + 2 = p(p(+(x497,y))) p(+(p(x497),y)) = 2x497 + 2y + 2 >= 2x497 + 2y + 2 = p(p(+(x497,y))) +(p(x499),y) = 2x499 + 2y + 2 >= 2x499 + 2y + 2 = p(+(x499,y)) +(p(x499),y) = 2x499 + 2y + 2 >= 2x499 + 2y + 2 = +(y,p(x499)) p(+(x499,y)) = 2x499 + 2y + 2 >= 2x499 + 2y + 2 = p(+(y,x499)) +(y,p(x499)) = 2x499 + 2y + 2 >= 2x499 + 2y + 2 = p(+(y,x499)) -(+(p(x501),y)) = 2x501 + 2y + 2 >= 2x501 + 2y + 2 = -(p(+(x501,y))) -(+(p(x501),y)) = 2x501 + 2y + 2 >= 2x501 + 2y + 2 = +(-(p(x501)),-(y)) s(-(+(x501,y))) = 2x501 + 2y + 3 >= 2x501 + 2y + 3 = s(+(-(x501),-(y))) +(s(-(x501)),-(y)) = 2x501 + 2y + 4 >= 2x501 + 2y + 3 = s(+(-(x501),-(y))) +(x,s(p(x503))) = 2x + 2x503 + 4 >= 2x + 2x503 + 3 = s(+(x,p(x503))) s(+(x,p(x503))) = 2x + 2x503 + 3 >= 2x + 2x503 + 3 = s(p(+(x,x503))) +(s(p(x504)),y) = 2x504 + 2y + 4 >= 2x504 + 2y + 3 = s(+(p(x504),y)) s(+(p(x504),y)) = 2x504 + 2y + 3 >= 2x504 + 2y + 3 = s(p(+(x504,y))) +(x,p(s(x507))) = 2x + 2x507 + 4 >= 2x + 2x507 + 4 = p(+(x,s(x507))) p(+(x,s(x507))) = 2x + 2x507 + 4 >= 2x + 2x507 + 3 = p(s(+(x,x507))) +(p(s(x508)),y) = 2x508 + 2y + 4 >= 2x508 + 2y + 4 = p(+(s(x508),y)) p(+(s(x508),y)) = 2x508 + 2y + 4 >= 2x508 + 2y + 3 = p(s(+(x508,y))) +(x,0()) = 2x + 4 >= 2x + 4 = +(0(),x) +(x,s(y)) = 2x + 2y + 4 >= 2x + 2y + 4 = +(s(y),x) +(x,s(y)) = 2x + 2y + 4 >= 2x + 2y + 3 = s(+(x,y)) +(s(y),x) = 2x + 2y + 4 >= 2x + 2y + 3 = s(+(y,x)) s(+(x,y)) = 2x + 2y + 3 >= 2x + 2y + 3 = s(+(y,x)) +(x,p(y)) = 2x + 2y + 2 >= 2x + 2y + 2 = +(p(y),x) +(x,p(y)) = 2x + 2y + 2 >= 2x + 2y + 2 = p(+(x,y)) +(p(y),x) = 2x + 2y + 2 >= 2x + 2y + 2 = p(+(y,x)) p(+(x,y)) = 2x + 2y + 2 >= 2x + 2y + 2 = p(+(y,x)) +(0(),y) = 2y + 4 >= 2y + 4 = +(y,0()) +(s(x),y) = 2x + 2y + 4 >= 2x + 2y + 4 = +(y,s(x)) +(s(x),y) = 2x + 2y + 4 >= 2x + 2y + 3 = s(+(x,y)) +(y,s(x)) = 2x + 2y + 4 >= 2x + 2y + 3 = s(+(y,x)) s(+(x,y)) = 2x + 2y + 3 >= 2x + 2y + 3 = s(+(y,x)) +(p(x),y) = 2x + 2y + 2 >= 2x + 2y + 2 = +(y,p(x)) +(p(x),y) = 2x + 2y + 2 >= 2x + 2y + 2 = p(+(x,y)) +(y,p(x)) = 2x + 2y + 2 >= 2x + 2y + 2 = p(+(y,x)) p(+(x,y)) = 2x + 2y + 2 >= 2x + 2y + 2 = p(+(y,x)) -(+(x,y)) = 2x + 2y + 2 >= 2x + 2y + 2 = -(+(y,x)) -(+(x,y)) = 2x + 2y + 2 >= 2x + 2y + 2 = +(-(x),-(y)) -(+(y,x)) = 2x + 2y + 2 >= 2x + 2y + 2 = +(-(y),-(x)) +(-(x),-(y)) = 2x + 2y + 2 >= 2x + 2y + 2 = +(-(y),-(x)) +(x,y) = 2x + 2y + 2 >= 2x + 2y + 2 = +(y,x) problem: strict: +(p(x),0()) -> p(+(x,0())) +(x,0()) -> +(0(),x) -(+(x,0())) -> +(-(x),-(0())) +(p(x),s(x463)) -> p(+(x,s(x463))) s(+(p(x),x463)) -> s(p(+(x,x463))) +(x,s(x465)) -> +(s(x465),x) s(+(x,x465)) -> s(+(x465,x)) -(+(x,s(x467))) -> +(-(x),-(s(x467))) p(-(+(x,x467))) -> p(+(-(x),-(x467))) +(-(x),p(-(x467))) -> p(+(-(x),-(x467))) +(0(),p(x469)) -> p(+(0(),x469)) +(s(x),p(x471)) -> p(+(s(x),x471)) s(+(x,p(x471))) -> s(p(+(x,x471))) +(p(x),p(x473)) -> p(+(p(x),x473)) +(p(x),p(x473)) -> p(+(x,p(x473))) p(+(p(x),x473)) -> p(p(+(x,x473))) p(+(x,p(x473))) -> p(p(+(x,x473))) +(x,p(x475)) -> p(+(x,x475)) +(x,p(x475)) -> +(p(x475),x) p(+(x,x475)) -> p(+(x475,x)) +(p(x475),x) -> p(+(x475,x)) -(+(x,p(x477))) -> -(p(+(x,x477))) -(+(x,p(x477))) -> +(-(x),-(p(x477))) s(-(+(x,x477))) -> s(+(-(x),-(x477))) +(0(),p(y)) -> p(+(0(),y)) +(0(),y) -> +(y,0()) -(+(0(),y)) -> +(-(0()),-(y)) +(s(x487),p(y)) -> p(+(s(x487),y)) s(+(x487,p(y))) -> s(p(+(x487,y))) +(s(x489),y) -> +(y,s(x489)) s(+(x489,y)) -> s(+(y,x489)) -(+(s(x491),y)) -> +(-(s(x491)),-(y)) p(-(+(x491,y))) -> p(+(-(x491),-(y))) +(p(-(x491)),-(y)) -> p(+(-(x491),-(y))) +(p(x493),0()) -> p(+(x493,0())) +(p(x495),s(y)) -> p(+(x495,s(y))) s(+(p(x495),y)) -> s(p(+(x495,y))) +(p(x497),p(y)) -> p(+(x497,p(y))) +(p(x497),p(y)) -> p(+(p(x497),y)) p(+(x497,p(y))) -> p(p(+(x497,y))) p(+(p(x497),y)) -> p(p(+(x497,y))) +(p(x499),y) -> p(+(x499,y)) +(p(x499),y) -> +(y,p(x499)) p(+(x499,y)) -> p(+(y,x499)) +(y,p(x499)) -> p(+(y,x499)) -(+(p(x501),y)) -> -(p(+(x501,y))) -(+(p(x501),y)) -> +(-(p(x501)),-(y)) s(-(+(x501,y))) -> s(+(-(x501),-(y))) s(+(x,p(x503))) -> s(p(+(x,x503))) s(+(p(x504),y)) -> s(p(+(x504,y))) +(x,p(s(x507))) -> p(+(x,s(x507))) +(p(s(x508)),y) -> p(+(s(x508),y)) +(x,0()) -> +(0(),x) +(x,s(y)) -> +(s(y),x) s(+(x,y)) -> s(+(y,x)) +(x,p(y)) -> +(p(y),x) +(x,p(y)) -> p(+(x,y)) +(p(y),x) -> p(+(y,x)) p(+(x,y)) -> p(+(y,x)) +(0(),y) -> +(y,0()) +(s(x),y) -> +(y,s(x)) s(+(x,y)) -> s(+(y,x)) +(p(x),y) -> +(y,p(x)) +(p(x),y) -> p(+(x,y)) +(y,p(x)) -> p(+(y,x)) p(+(x,y)) -> p(+(y,x)) -(+(x,y)) -> -(+(y,x)) -(+(x,y)) -> +(-(x),-(y)) -(+(y,x)) -> +(-(y),-(x)) +(-(x),-(y)) -> +(-(y),-(x)) weak: +(x,p(y)) -> p(+(x,y)) +(p(x),y) -> p(+(x,y)) +(x,y) -> +(y,x) -(+(x,y)) -> +(-(x),-(y)) Matrix Interpretation Processor: dim=1 interpretation: [-](x0) = 2x0, [p](x0) = x0, [s](x0) = x0, [+](x0, x1) = x0 + x1 + 4, [0] = 0 orientation: +(p(x),0()) = x + 4 >= x + 4 = p(+(x,0())) +(x,0()) = x + 4 >= x + 4 = +(0(),x) -(+(x,0())) = 2x + 8 >= 2x + 4 = +(-(x),-(0())) +(p(x),s(x463)) = x + x463 + 4 >= x + x463 + 4 = p(+(x,s(x463))) s(+(p(x),x463)) = x + x463 + 4 >= x + x463 + 4 = s(p(+(x,x463))) +(x,s(x465)) = x + x465 + 4 >= x + x465 + 4 = +(s(x465),x) s(+(x,x465)) = x + x465 + 4 >= x + x465 + 4 = s(+(x465,x)) -(+(x,s(x467))) = 2x + 2x467 + 8 >= 2x + 2x467 + 4 = +(-(x),-(s(x467))) p(-(+(x,x467))) = 2x + 2x467 + 8 >= 2x + 2x467 + 4 = p(+(-(x),-(x467))) +(-(x),p(-(x467))) = 2x + 2x467 + 4 >= 2x + 2x467 + 4 = p(+(-(x),-(x467))) +(0(),p(x469)) = x469 + 4 >= x469 + 4 = p(+(0(),x469)) +(s(x),p(x471)) = x + x471 + 4 >= x + x471 + 4 = p(+(s(x),x471)) s(+(x,p(x471))) = x + x471 + 4 >= x + x471 + 4 = s(p(+(x,x471))) +(p(x),p(x473)) = x + x473 + 4 >= x + x473 + 4 = p(+(p(x),x473)) +(p(x),p(x473)) = x + x473 + 4 >= x + x473 + 4 = p(+(x,p(x473))) p(+(p(x),x473)) = x + x473 + 4 >= x + x473 + 4 = p(p(+(x,x473))) p(+(x,p(x473))) = x + x473 + 4 >= x + x473 + 4 = p(p(+(x,x473))) +(x,p(x475)) = x + x475 + 4 >= x + x475 + 4 = p(+(x,x475)) +(x,p(x475)) = x + x475 + 4 >= x + x475 + 4 = +(p(x475),x) p(+(x,x475)) = x + x475 + 4 >= x + x475 + 4 = p(+(x475,x)) +(p(x475),x) = x + x475 + 4 >= x + x475 + 4 = p(+(x475,x)) -(+(x,p(x477))) = 2x + 2x477 + 8 >= 2x + 2x477 + 8 = -(p(+(x,x477))) -(+(x,p(x477))) = 2x + 2x477 + 8 >= 2x + 2x477 + 4 = +(-(x),-(p(x477))) s(-(+(x,x477))) = 2x + 2x477 + 8 >= 2x + 2x477 + 4 = s(+(-(x),-(x477))) +(0(),p(y)) = y + 4 >= y + 4 = p(+(0(),y)) +(0(),y) = y + 4 >= y + 4 = +(y,0()) -(+(0(),y)) = 2y + 8 >= 2y + 4 = +(-(0()),-(y)) +(s(x487),p(y)) = x487 + y + 4 >= x487 + y + 4 = p(+(s(x487),y)) s(+(x487,p(y))) = x487 + y + 4 >= x487 + y + 4 = s(p(+(x487,y))) +(s(x489),y) = x489 + y + 4 >= x489 + y + 4 = +(y,s(x489)) s(+(x489,y)) = x489 + y + 4 >= x489 + y + 4 = s(+(y,x489)) -(+(s(x491),y)) = 2x491 + 2y + 8 >= 2x491 + 2y + 4 = +(-(s(x491)),-(y)) p(-(+(x491,y))) = 2x491 + 2y + 8 >= 2x491 + 2y + 4 = p(+(-(x491),-(y))) +(p(-(x491)),-(y)) = 2x491 + 2y + 4 >= 2x491 + 2y + 4 = p(+(-(x491),-(y))) +(p(x493),0()) = x493 + 4 >= x493 + 4 = p(+(x493,0())) +(p(x495),s(y)) = x495 + y + 4 >= x495 + y + 4 = p(+(x495,s(y))) s(+(p(x495),y)) = x495 + y + 4 >= x495 + y + 4 = s(p(+(x495,y))) +(p(x497),p(y)) = x497 + y + 4 >= x497 + y + 4 = p(+(x497,p(y))) +(p(x497),p(y)) = x497 + y + 4 >= x497 + y + 4 = p(+(p(x497),y)) p(+(x497,p(y))) = x497 + y + 4 >= x497 + y + 4 = p(p(+(x497,y))) p(+(p(x497),y)) = x497 + y + 4 >= x497 + y + 4 = p(p(+(x497,y))) +(p(x499),y) = x499 + y + 4 >= x499 + y + 4 = p(+(x499,y)) +(p(x499),y) = x499 + y + 4 >= x499 + y + 4 = +(y,p(x499)) p(+(x499,y)) = x499 + y + 4 >= x499 + y + 4 = p(+(y,x499)) +(y,p(x499)) = x499 + y + 4 >= x499 + y + 4 = p(+(y,x499)) -(+(p(x501),y)) = 2x501 + 2y + 8 >= 2x501 + 2y + 8 = -(p(+(x501,y))) -(+(p(x501),y)) = 2x501 + 2y + 8 >= 2x501 + 2y + 4 = +(-(p(x501)),-(y)) s(-(+(x501,y))) = 2x501 + 2y + 8 >= 2x501 + 2y + 4 = s(+(-(x501),-(y))) s(+(x,p(x503))) = x + x503 + 4 >= x + x503 + 4 = s(p(+(x,x503))) s(+(p(x504),y)) = x504 + y + 4 >= x504 + y + 4 = s(p(+(x504,y))) +(x,p(s(x507))) = x + x507 + 4 >= x + x507 + 4 = p(+(x,s(x507))) +(p(s(x508)),y) = x508 + y + 4 >= x508 + y + 4 = p(+(s(x508),y)) +(x,0()) = x + 4 >= x + 4 = +(0(),x) +(x,s(y)) = x + y + 4 >= x + y + 4 = +(s(y),x) s(+(x,y)) = x + y + 4 >= x + y + 4 = s(+(y,x)) +(x,p(y)) = x + y + 4 >= x + y + 4 = +(p(y),x) +(x,p(y)) = x + y + 4 >= x + y + 4 = p(+(x,y)) +(p(y),x) = x + y + 4 >= x + y + 4 = p(+(y,x)) p(+(x,y)) = x + y + 4 >= x + y + 4 = p(+(y,x)) +(0(),y) = y + 4 >= y + 4 = +(y,0()) +(s(x),y) = x + y + 4 >= x + y + 4 = +(y,s(x)) s(+(x,y)) = x + y + 4 >= x + y + 4 = s(+(y,x)) +(p(x),y) = x + y + 4 >= x + y + 4 = +(y,p(x)) +(p(x),y) = x + y + 4 >= x + y + 4 = p(+(x,y)) +(y,p(x)) = x + y + 4 >= x + y + 4 = p(+(y,x)) p(+(x,y)) = x + y + 4 >= x + y + 4 = p(+(y,x)) -(+(x,y)) = 2x + 2y + 8 >= 2x + 2y + 8 = -(+(y,x)) -(+(x,y)) = 2x + 2y + 8 >= 2x + 2y + 4 = +(-(x),-(y)) -(+(y,x)) = 2x + 2y + 8 >= 2x + 2y + 4 = +(-(y),-(x)) +(-(x),-(y)) = 2x + 2y + 4 >= 2x + 2y + 4 = +(-(y),-(x)) +(x,y) = x + y + 4 >= x + y + 4 = +(y,x) problem: strict: +(p(x),0()) -> p(+(x,0())) +(x,0()) -> +(0(),x) +(p(x),s(x463)) -> p(+(x,s(x463))) s(+(p(x),x463)) -> s(p(+(x,x463))) +(x,s(x465)) -> +(s(x465),x) s(+(x,x465)) -> s(+(x465,x)) +(-(x),p(-(x467))) -> p(+(-(x),-(x467))) +(0(),p(x469)) -> p(+(0(),x469)) +(s(x),p(x471)) -> p(+(s(x),x471)) s(+(x,p(x471))) -> s(p(+(x,x471))) +(p(x),p(x473)) -> p(+(p(x),x473)) +(p(x),p(x473)) -> p(+(x,p(x473))) p(+(p(x),x473)) -> p(p(+(x,x473))) p(+(x,p(x473))) -> p(p(+(x,x473))) +(x,p(x475)) -> p(+(x,x475)) +(x,p(x475)) -> +(p(x475),x) p(+(x,x475)) -> p(+(x475,x)) +(p(x475),x) -> p(+(x475,x)) -(+(x,p(x477))) -> -(p(+(x,x477))) +(0(),p(y)) -> p(+(0(),y)) +(0(),y) -> +(y,0()) +(s(x487),p(y)) -> p(+(s(x487),y)) s(+(x487,p(y))) -> s(p(+(x487,y))) +(s(x489),y) -> +(y,s(x489)) s(+(x489,y)) -> s(+(y,x489)) +(p(-(x491)),-(y)) -> p(+(-(x491),-(y))) +(p(x493),0()) -> p(+(x493,0())) +(p(x495),s(y)) -> p(+(x495,s(y))) s(+(p(x495),y)) -> s(p(+(x495,y))) +(p(x497),p(y)) -> p(+(x497,p(y))) +(p(x497),p(y)) -> p(+(p(x497),y)) p(+(x497,p(y))) -> p(p(+(x497,y))) p(+(p(x497),y)) -> p(p(+(x497,y))) +(p(x499),y) -> p(+(x499,y)) +(p(x499),y) -> +(y,p(x499)) p(+(x499,y)) -> p(+(y,x499)) +(y,p(x499)) -> p(+(y,x499)) -(+(p(x501),y)) -> -(p(+(x501,y))) s(+(x,p(x503))) -> s(p(+(x,x503))) s(+(p(x504),y)) -> s(p(+(x504,y))) +(x,p(s(x507))) -> p(+(x,s(x507))) +(p(s(x508)),y) -> p(+(s(x508),y)) +(x,0()) -> +(0(),x) +(x,s(y)) -> +(s(y),x) s(+(x,y)) -> s(+(y,x)) +(x,p(y)) -> +(p(y),x) +(x,p(y)) -> p(+(x,y)) +(p(y),x) -> p(+(y,x)) p(+(x,y)) -> p(+(y,x)) +(0(),y) -> +(y,0()) +(s(x),y) -> +(y,s(x)) s(+(x,y)) -> s(+(y,x)) +(p(x),y) -> +(y,p(x)) +(p(x),y) -> p(+(x,y)) +(y,p(x)) -> p(+(y,x)) p(+(x,y)) -> p(+(y,x)) -(+(x,y)) -> -(+(y,x)) +(-(x),-(y)) -> +(-(y),-(x)) weak: +(x,p(y)) -> p(+(x,y)) +(p(x),y) -> p(+(x,y)) +(x,y) -> +(y,x) Matrix Interpretation Processor: dim=1 interpretation: [-](x0) = 2x0, [p](x0) = x0 + 2, [s](x0) = x0, [+](x0, x1) = 2x0 + 2x1, [0] = 2 orientation: +(p(x),0()) = 2x + 8 >= 2x + 6 = p(+(x,0())) +(x,0()) = 2x + 4 >= 2x + 4 = +(0(),x) +(p(x),s(x463)) = 2x + 2x463 + 4 >= 2x + 2x463 + 2 = p(+(x,s(x463))) s(+(p(x),x463)) = 2x + 2x463 + 4 >= 2x + 2x463 + 2 = s(p(+(x,x463))) +(x,s(x465)) = 2x + 2x465 >= 2x + 2x465 = +(s(x465),x) s(+(x,x465)) = 2x + 2x465 >= 2x + 2x465 = s(+(x465,x)) +(-(x),p(-(x467))) = 4x + 4x467 + 4 >= 4x + 4x467 + 2 = p(+(-(x),-(x467))) +(0(),p(x469)) = 2x469 + 8 >= 2x469 + 6 = p(+(0(),x469)) +(s(x),p(x471)) = 2x + 2x471 + 4 >= 2x + 2x471 + 2 = p(+(s(x),x471)) s(+(x,p(x471))) = 2x + 2x471 + 4 >= 2x + 2x471 + 2 = s(p(+(x,x471))) +(p(x),p(x473)) = 2x + 2x473 + 8 >= 2x + 2x473 + 6 = p(+(p(x),x473)) +(p(x),p(x473)) = 2x + 2x473 + 8 >= 2x + 2x473 + 6 = p(+(x,p(x473))) p(+(p(x),x473)) = 2x + 2x473 + 6 >= 2x + 2x473 + 4 = p(p(+(x,x473))) p(+(x,p(x473))) = 2x + 2x473 + 6 >= 2x + 2x473 + 4 = p(p(+(x,x473))) +(x,p(x475)) = 2x + 2x475 + 4 >= 2x + 2x475 + 2 = p(+(x,x475)) +(x,p(x475)) = 2x + 2x475 + 4 >= 2x + 2x475 + 4 = +(p(x475),x) p(+(x,x475)) = 2x + 2x475 + 2 >= 2x + 2x475 + 2 = p(+(x475,x)) +(p(x475),x) = 2x + 2x475 + 4 >= 2x + 2x475 + 2 = p(+(x475,x)) -(+(x,p(x477))) = 4x + 4x477 + 8 >= 4x + 4x477 + 4 = -(p(+(x,x477))) +(0(),p(y)) = 2y + 8 >= 2y + 6 = p(+(0(),y)) +(0(),y) = 2y + 4 >= 2y + 4 = +(y,0()) +(s(x487),p(y)) = 2x487 + 2y + 4 >= 2x487 + 2y + 2 = p(+(s(x487),y)) s(+(x487,p(y))) = 2x487 + 2y + 4 >= 2x487 + 2y + 2 = s(p(+(x487,y))) +(s(x489),y) = 2x489 + 2y >= 2x489 + 2y = +(y,s(x489)) s(+(x489,y)) = 2x489 + 2y >= 2x489 + 2y = s(+(y,x489)) +(p(-(x491)),-(y)) = 4x491 + 4y + 4 >= 4x491 + 4y + 2 = p(+(-(x491),-(y))) +(p(x493),0()) = 2x493 + 8 >= 2x493 + 6 = p(+(x493,0())) +(p(x495),s(y)) = 2x495 + 2y + 4 >= 2x495 + 2y + 2 = p(+(x495,s(y))) s(+(p(x495),y)) = 2x495 + 2y + 4 >= 2x495 + 2y + 2 = s(p(+(x495,y))) +(p(x497),p(y)) = 2x497 + 2y + 8 >= 2x497 + 2y + 6 = p(+(x497,p(y))) +(p(x497),p(y)) = 2x497 + 2y + 8 >= 2x497 + 2y + 6 = p(+(p(x497),y)) p(+(x497,p(y))) = 2x497 + 2y + 6 >= 2x497 + 2y + 4 = p(p(+(x497,y))) p(+(p(x497),y)) = 2x497 + 2y + 6 >= 2x497 + 2y + 4 = p(p(+(x497,y))) +(p(x499),y) = 2x499 + 2y + 4 >= 2x499 + 2y + 2 = p(+(x499,y)) +(p(x499),y) = 2x499 + 2y + 4 >= 2x499 + 2y + 4 = +(y,p(x499)) p(+(x499,y)) = 2x499 + 2y + 2 >= 2x499 + 2y + 2 = p(+(y,x499)) +(y,p(x499)) = 2x499 + 2y + 4 >= 2x499 + 2y + 2 = p(+(y,x499)) -(+(p(x501),y)) = 4x501 + 4y + 8 >= 4x501 + 4y + 4 = -(p(+(x501,y))) s(+(x,p(x503))) = 2x + 2x503 + 4 >= 2x + 2x503 + 2 = s(p(+(x,x503))) s(+(p(x504),y)) = 2x504 + 2y + 4 >= 2x504 + 2y + 2 = s(p(+(x504,y))) +(x,p(s(x507))) = 2x + 2x507 + 4 >= 2x + 2x507 + 2 = p(+(x,s(x507))) +(p(s(x508)),y) = 2x508 + 2y + 4 >= 2x508 + 2y + 2 = p(+(s(x508),y)) +(x,0()) = 2x + 4 >= 2x + 4 = +(0(),x) +(x,s(y)) = 2x + 2y >= 2x + 2y = +(s(y),x) s(+(x,y)) = 2x + 2y >= 2x + 2y = s(+(y,x)) +(x,p(y)) = 2x + 2y + 4 >= 2x + 2y + 4 = +(p(y),x) +(x,p(y)) = 2x + 2y + 4 >= 2x + 2y + 2 = p(+(x,y)) +(p(y),x) = 2x + 2y + 4 >= 2x + 2y + 2 = p(+(y,x)) p(+(x,y)) = 2x + 2y + 2 >= 2x + 2y + 2 = p(+(y,x)) +(0(),y) = 2y + 4 >= 2y + 4 = +(y,0()) +(s(x),y) = 2x + 2y >= 2x + 2y = +(y,s(x)) s(+(x,y)) = 2x + 2y >= 2x + 2y = s(+(y,x)) +(p(x),y) = 2x + 2y + 4 >= 2x + 2y + 4 = +(y,p(x)) +(p(x),y) = 2x + 2y + 4 >= 2x + 2y + 2 = p(+(x,y)) +(y,p(x)) = 2x + 2y + 4 >= 2x + 2y + 2 = p(+(y,x)) p(+(x,y)) = 2x + 2y + 2 >= 2x + 2y + 2 = p(+(y,x)) -(+(x,y)) = 4x + 4y >= 4x + 4y = -(+(y,x)) +(-(x),-(y)) = 4x + 4y >= 4x + 4y = +(-(y),-(x)) +(x,y) = 2x + 2y >= 2x + 2y = +(y,x) problem: strict: +(x,0()) -> +(0(),x) +(x,s(x465)) -> +(s(x465),x) s(+(x,x465)) -> s(+(x465,x)) +(x,p(x475)) -> +(p(x475),x) p(+(x,x475)) -> p(+(x475,x)) +(0(),y) -> +(y,0()) +(s(x489),y) -> +(y,s(x489)) s(+(x489,y)) -> s(+(y,x489)) +(p(x499),y) -> +(y,p(x499)) p(+(x499,y)) -> p(+(y,x499)) +(x,0()) -> +(0(),x) +(x,s(y)) -> +(s(y),x) s(+(x,y)) -> s(+(y,x)) +(x,p(y)) -> +(p(y),x) p(+(x,y)) -> p(+(y,x)) +(0(),y) -> +(y,0()) +(s(x),y) -> +(y,s(x)) s(+(x,y)) -> s(+(y,x)) +(p(x),y) -> +(y,p(x)) p(+(x,y)) -> p(+(y,x)) -(+(x,y)) -> -(+(y,x)) +(-(x),-(y)) -> +(-(y),-(x)) weak: +(x,y) -> +(y,x) Shift Processor (ldh) lab=left (force): strict: weak: Decreasing Processor: The following diagrams are decreasing: peak: 0() <-0|[1,0,0]- +(0(),0()) -3|[1,0,0]-> 0() joins: peak: s(x) <-0|[1,0,0]- +(s(x),0()) -4|[1,0,0]-> s(+(x,0())) joins: s(+(x,0())) -0|0[0,0,0]-> s(x) peak: p(x) <-0|[1,0,0]- +(p(x),0()) -5|[1,0,0]-> p(+(x,0())) joins: p(+(x,0())) -0|0[0,0,0]-> p(x) peak: x <-0|[1,0,0]- +(x,0()) -11|[1,0,0]-> +(0(),x) joins: +(0(),x) -3|[1,0,0]-> x peak: -(x) <-0|0[1,0,0]- -(+(x,0())) -12|[1,0,0]-> +(-(x),-(0())) joins: +(-(x),-(0())) -8|1[0,2,1]-> +(-(x),0()) -0|[0,0,0]-> -(x) peak: s(+(0(),x459)) <-1|[1,0,0]- +(0(),s(x459)) -3|[1,0,0]-> s(x459) joins: s(+(0(),x459)) -3|0[0,0,0]-> s(x459) peak: s(+(s(x),x461)) <-1|[1,0,0]- +(s(x),s(x461)) -4|[1,0,0]-> s(+(x,s(x461))) joins: s(+(s(x),x461)) -4|0[0,0,0]-> s(s(+(x,x461))) s(+(x,s(x461))) -1|0[0,0,0]-> s(s(+(x,x461))) peak: s(+(p(x),x463)) <-1|[1,0,0]- +(p(x),s(x463)) -5|[1,0,0]-> p(+(x,s(x463))) joins: s(+(p(x),x463)) -5|0[0,0,0]-> s(p(+(x,x463))) -6|[0,0,0]-> +(x,x463) p(+(x,s(x463))) -1|0[0,0,0]-> p(s(+(x,x463))) -7|[0,0,0]-> +(x,x463) peak: s(+(x,x465)) <-1|[1,0,0]- +(x,s(x465)) -11|[1,0,0]-> +(s(x465),x) joins: s(+(x,x465)) -11|0[0,0,0]-> s(+(x465,x)) +(s(x465),x) -4|[1,0,0]-> s(+(x465,x)) peak: -(s(+(x,x467))) <-1|0[1,0,0]- -(+(x,s(x467))) -12|[1,0,0]-> +(-(x),-(s(x467))) joins: -(s(+(x,x467))) -9|[0,0,0]-> p(-(+(x,x467))) -12|0[0,0,0]-> p(+(-(x),-(x467))) +(-(x),-(s(x467))) -9|1[0,2,1]-> +(-(x),p(-(x467))) -2|[0,0,0]-> p(+(-(x),-(x467))) peak: p(+(0(),x469)) <-2|[1,0,0]- +(0(),p(x469)) -3|[1,0,0]-> p(x469) joins: p(+(0(),x469)) -3|0[0,0,0]-> p(x469) peak: p(+(s(x),x471)) <-2|[1,0,0]- +(s(x),p(x471)) -4|[1,0,0]-> s(+(x,p(x471))) joins: p(+(s(x),x471)) -4|0[0,0,0]-> p(s(+(x,x471))) -7|[0,0,0]-> +(x,x471) s(+(x,p(x471))) -2|0[0,0,0]-> s(p(+(x,x471))) -6|[0,0,0]-> +(x,x471) peak: p(+(p(x),x473)) <-2|[1,0,0]- +(p(x),p(x473)) -5|[1,0,0]-> p(+(x,p(x473))) joins: p(+(p(x),x473)) -5|0[0,0,0]-> p(p(+(x,x473))) p(+(x,p(x473))) -2|0[0,0,0]-> p(p(+(x,x473))) peak: p(+(x,x475)) <-2|[1,0,0]- +(x,p(x475)) -11|[1,0,0]-> +(p(x475),x) joins: p(+(x,x475)) -11|0[0,0,0]-> p(+(x475,x)) +(p(x475),x) -5|[1,0,0]-> p(+(x475,x)) peak: -(p(+(x,x477))) <-2|0[1,0,0]- -(+(x,p(x477))) -12|[1,0,0]-> +(-(x),-(p(x477))) joins: -(p(+(x,x477))) -10|[0,0,0]-> s(-(+(x,x477))) -12|0[0,0,0]-> s(+(-(x),-(x477))) +(-(x),-(p(x477))) -10|1[0,2,1]-> +(-(x),s(-(x477))) -1|[0,0,0]-> s(+(-(x),-(x477))) peak: 0() <-3|[1,0,0]- +(0(),0()) -0|[1,0,0]-> 0() joins: peak: s(y) <-3|[1,0,0]- +(0(),s(y)) -1|[1,0,0]-> s(+(0(),y)) joins: s(+(0(),y)) -3|0[0,0,0]-> s(y) peak: p(y) <-3|[1,0,0]- +(0(),p(y)) -2|[1,0,0]-> p(+(0(),y)) joins: p(+(0(),y)) -3|0[0,0,0]-> p(y) peak: y <-3|[1,0,0]- +(0(),y) -11|[1,0,0]-> +(y,0()) joins: +(y,0()) -0|[1,0,0]-> y peak: -(y) <-3|0[1,0,0]- -(+(0(),y)) -12|[1,0,0]-> +(-(0()),-(y)) joins: +(-(0()),-(y)) -8|0[0,2,1]-> +(0(),-(y)) -3|[0,0,0]-> -(y) peak: s(+(x483,0())) <-4|[1,0,0]- +(s(x483),0()) -0|[1,0,0]-> s(x483) joins: s(+(x483,0())) -0|0[0,0,0]-> s(x483) peak: s(+(x485,s(y))) <-4|[1,0,0]- +(s(x485),s(y)) -1|[1,0,0]-> s(+(s(x485),y)) joins: s(+(x485,s(y))) -1|0[0,0,0]-> s(s(+(x485,y))) s(+(s(x485),y)) -4|0[0,0,0]-> s(s(+(x485,y))) peak: s(+(x487,p(y))) <-4|[1,0,0]- +(s(x487),p(y)) -2|[1,0,0]-> p(+(s(x487),y)) joins: s(+(x487,p(y))) -2|0[0,0,0]-> s(p(+(x487,y))) -6|[0,0,0]-> +(x487,y) p(+(s(x487),y)) -4|0[0,0,0]-> p(s(+(x487,y))) -7|[0,0,0]-> +(x487,y) peak: s(+(x489,y)) <-4|[1,0,0]- +(s(x489),y) -11|[1,0,0]-> +(y,s(x489)) joins: s(+(x489,y)) -11|0[0,0,0]-> s(+(y,x489)) +(y,s(x489)) -1|[1,0,0]-> s(+(y,x489)) peak: -(s(+(x491,y))) <-4|0[1,0,0]- -(+(s(x491),y)) -12|[1,0,0]-> +(-(s(x491)),-(y)) joins: -(s(+(x491,y))) -9|[0,0,0]-> p(-(+(x491,y))) -12|0[0,0,0]-> p(+(-(x491),-(y))) +(-(s(x491)),-(y)) -9|0[0,2,1]-> +(p(-(x491)),-(y)) -5|[0,0,0]-> p(+(-(x491),-(y))) peak: p(+(x493,0())) <-5|[1,0,0]- +(p(x493),0()) -0|[1,0,0]-> p(x493) joins: p(+(x493,0())) -0|0[0,0,0]-> p(x493) peak: p(+(x495,s(y))) <-5|[1,0,0]- +(p(x495),s(y)) -1|[1,0,0]-> s(+(p(x495),y)) joins: p(+(x495,s(y))) -1|0[0,0,0]-> p(s(+(x495,y))) -7|[0,0,0]-> +(x495,y) s(+(p(x495),y)) -5|0[0,0,0]-> s(p(+(x495,y))) -6|[0,0,0]-> +(x495,y) peak: p(+(x497,p(y))) <-5|[1,0,0]- +(p(x497),p(y)) -2|[1,0,0]-> p(+(p(x497),y)) joins: p(+(x497,p(y))) -2|0[0,0,0]-> p(p(+(x497,y))) p(+(p(x497),y)) -5|0[0,0,0]-> p(p(+(x497,y))) peak: p(+(x499,y)) <-5|[1,0,0]- +(p(x499),y) -11|[1,0,0]-> +(y,p(x499)) joins: p(+(x499,y)) -11|0[0,0,0]-> p(+(y,x499)) +(y,p(x499)) -2|[1,0,0]-> p(+(y,x499)) peak: -(p(+(x501,y))) <-5|0[1,0,0]- -(+(p(x501),y)) -12|[1,0,0]-> +(-(p(x501)),-(y)) joins: -(p(+(x501,y))) -10|[0,0,0]-> s(-(+(x501,y))) -12|0[0,0,0]-> s(+(-(x501),-(y))) +(-(p(x501)),-(y)) -10|0[0,2,1]-> +(s(-(x501)),-(y)) -4|[0,0,0]-> s(+(-(x501),-(y))) peak: +(x,x503) <-6|1[1,2,1]- +(x,s(p(x503))) -1|[1,0,0]-> s(+(x,p(x503))) joins: s(+(x,p(x503))) -2|0[0,0,0]-> s(p(+(x,x503))) -6|[0,0,0]-> +(x,x503) peak: +(x504,y) <-6|0[1,2,1]- +(s(p(x504)),y) -4|[1,0,0]-> s(+(p(x504),y)) joins: s(+(p(x504),y)) -5|0[0,0,0]-> s(p(+(x504,y))) -6|[0,0,0]-> +(x504,y) peak: p(x505) <-6|0[1,0,0]- p(s(p(x505))) -7|[1,0,0]-> p(x505) joins: peak: -(x506) <-6|0[1,0,0]- -(s(p(x506))) -9|[1,0,0]-> p(-(p(x506))) joins: p(-(p(x506))) -10|0[0,0,0]-> p(s(-(x506))) -7|[0,0,0]-> -(x506) peak: +(x,x507) <-7|1[1,2,1]- +(x,p(s(x507))) -2|[1,0,0]-> p(+(x,s(x507))) joins: p(+(x,s(x507))) -1|0[0,0,0]-> p(s(+(x,x507))) -7|[0,0,0]-> +(x,x507) peak: +(x508,y) <-7|0[1,2,1]- +(p(s(x508)),y) -5|[1,0,0]-> p(+(s(x508),y)) joins: p(+(s(x508),y)) -4|0[0,0,0]-> p(s(+(x508,y))) -7|[0,0,0]-> +(x508,y) peak: s(x509) <-7|0[1,0,0]- s(p(s(x509))) -6|[1,0,0]-> s(x509) joins: peak: -(x510) <-7|0[1,0,0]- -(p(s(x510))) -10|[1,0,0]-> s(-(s(x510))) joins: s(-(s(x510))) -9|0[0,0,0]-> s(p(-(x510))) -6|[0,0,0]-> -(x510) peak: +(0(),x) <-11|[1,0,0]- +(x,0()) -0|[1,0,0]-> x joins: +(0(),x) -3|[1,0,0]-> x peak: +(s(y),x) <-11|[1,0,0]- +(x,s(y)) -1|[1,0,0]-> s(+(x,y)) joins: +(s(y),x) -4|[1,0,0]-> s(+(y,x)) s(+(x,y)) -11|0[0,0,0]-> s(+(y,x)) peak: +(p(y),x) <-11|[1,0,0]- +(x,p(y)) -2|[1,0,0]-> p(+(x,y)) joins: +(p(y),x) -5|[1,0,0]-> p(+(y,x)) p(+(x,y)) -11|0[0,0,0]-> p(+(y,x)) peak: +(y,0()) <-11|[1,0,0]- +(0(),y) -3|[1,0,0]-> y joins: +(y,0()) -0|[1,0,0]-> y peak: +(y,s(x)) <-11|[1,0,0]- +(s(x),y) -4|[1,0,0]-> s(+(x,y)) joins: +(y,s(x)) -1|[1,0,0]-> s(+(y,x)) s(+(x,y)) -11|0[0,0,0]-> s(+(y,x)) peak: +(y,p(x)) <-11|[1,0,0]- +(p(x),y) -5|[1,0,0]-> p(+(x,y)) joins: +(y,p(x)) -2|[1,0,0]-> p(+(y,x)) p(+(x,y)) -11|0[0,0,0]-> p(+(y,x)) peak: -(+(y,x)) <-11|0[1,0,0]- -(+(x,y)) -12|[1,0,0]-> +(-(x),-(y)) joins: -(+(y,x)) -12|[1,0,0]-> +(-(y),-(x)) +(-(x),-(y)) -11|[0,0,0]-> +(-(y),-(x)) Qed