Problem: -(+(x,y)) -> +(-(x),-(y)) +(x,y) -> +(y,x) +(+(x,y),z) -> +(x,+(y,z)) Proof: Commute Transformation Processor: -(+(x,y)) -> +(-(x),-(y)) +(x,y) -> +(y,x) +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) Church Rosser Transformation Processor (dup): strict: weak: -(+(x,y)) -> +(-(x),-(y)) +(x,y) -> +(y,x) +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) critical peaks: 15 -(+(y,x)) <-1|0[]- -(+(x,y)) -0|[]-> +(-(x),-(y)) +(z,+(x,y)) <-1|[]- +(+(x,y),z) -2|[]-> +(x,+(y,z)) +(+(y,x),z) <-1|0[]- +(+(x,y),z) -2|[]-> +(x,+(y,z)) +(+(y,z),x) <-1|[]- +(x,+(y,z)) -3|[]-> +(+(x,y),z) +(x,+(z,y)) <-1|1[]- +(x,+(y,z)) -3|[]-> +(+(x,y),z) -(+(x83,+(x84,y))) <-2|0[]- -(+(+(x83,x84),y)) -0|[]-> +(-(+(x83,x84)),-(y)) +(x86,+(x87,y)) <-2|[]- +(+(x86,x87),y) -1|[]-> +(y,+(x86,x87)) +(+(x89,+(x90,y)),z) <-2|0[]- +(+(+(x89,x90),y),z) -2|[]-> +(+(x89,x90),+(y,z)) +(x92,+(x93,+(y,z))) <-2|[]- +(+(x92,x93),+(y,z)) -3|[]-> +(+(+(x92,x93),y),z) +(x,+(x95,+(x96,z))) <-2|1[]- +(x,+(+(x95,x96),z)) -3|[]-> +(+(x,+(x95,x96)),z) -(+(+(x,x99),x100)) <-3|0[]- -(+(x,+(x99,x100))) -0|[]-> +(-(x),-(+(x99,x100))) +(+(x,x102),x103) <-3|[]- +(x,+(x102,x103)) -1|[]-> +(+(x102,x103),x) +(+(+(x,y),x105),x106) <-3|[]- +(+(x,y),+(x105,x106)) -2|[]-> +(x,+(y,+(x105,x106))) +(+(+(x,x108),x109),z) <-3|0[]- +(+(x,+(x108,x109)),z) -2|[]-> +(x,+(+(x108,x109),z)) +(x,+(+(y,x111),x112)) <-3|1[]- +(x,+(y,+(x111,x112))) -3|[]-> +(+(x,y),+(x111,x112)) Polynomial Interpretation Processor: dimension: 1 interpretation: [-](x0) = 3x0 + 1, [+](x0, x1) = x0 + x1 + 1 orientation: -(+(x,y)) = 3x + 3y + 4 >= 3x + 3y + 3 = +(-(x),-(y)) +(x,y) = x + y + 1 >= x + y + 1 = +(y,x) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) problem: strict: weak: +(x,y) -> +(y,x) +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) Shift Processor (no label): strict: weak: Shift Processor lab=left (dd): strict: -(+(x,y)) -> -(+(y,x)) -(+(x,y)) -> +(-(x),-(y)) -(+(y,x)) -> +(-(y),-(x)) +(-(x),-(y)) -> +(-(y),-(x)) +(+(x,y),z) -> +(z,+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) +(z,+(x,y)) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(x,y),z) +(+(x,y),z) -> +(+(y,x),z) +(+(x,y),z) -> +(x,+(y,z)) +(+(y,x),z) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(y,z),x) +(x,+(y,z)) -> +(+(x,y),z) +(+(y,z),x) -> +(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(x,+(z,y)) +(x,+(y,z)) -> +(+(x,y),z) +(x,+(z,y)) -> +(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) -(+(+(x83,x84),y)) -> -(+(x83,+(x84,y))) -(+(+(x83,x84),y)) -> +(-(+(x83,x84)),-(y)) -(+(x83,+(x84,y))) -> +(-(x83),-(+(x84,y))) +(-(x83),-(+(x84,y))) -> +(-(x83),+(-(x84),-(y))) +(-(+(x83,x84)),-(y)) -> +(+(-(x83),-(x84)),-(y)) +(+(-(x83),-(x84)),-(y)) -> +(-(x83),+(-(x84),-(y))) -(+(x83,+(x84,y))) -> -(+(+(x83,x84),y)) -(+(+(x83,x84),y)) -> +(-(+(x83,x84)),-(y)) +(+(x86,x87),y) -> +(x86,+(x87,y)) +(+(x86,x87),y) -> +(y,+(x86,x87)) +(x86,+(x87,y)) -> +(+(x86,x87),y) +(y,+(x86,x87)) -> +(+(x86,x87),y) +(+(+(x89,x90),y),z) -> +(+(x89,+(x90,y)),z) +(+(+(x89,x90),y),z) -> +(+(x89,x90),+(y,z)) +(+(x89,+(x90,y)),z) -> +(+(+(x89,x90),y),z) +(+(x89,x90),+(y,z)) -> +(+(+(x89,x90),y),z) +(+(x92,x93),+(y,z)) -> +(x92,+(x93,+(y,z))) +(+(x92,x93),+(y,z)) -> +(+(+(x92,x93),y),z) +(x92,+(x93,+(y,z))) -> +(+(x92,x93),+(y,z)) +(+(+(x92,x93),y),z) -> +(+(x92,x93),+(y,z)) +(x,+(+(x95,x96),z)) -> +(x,+(x95,+(x96,z))) +(x,+(+(x95,x96),z)) -> +(+(x,+(x95,x96)),z) +(x,+(x95,+(x96,z))) -> +(x,+(+(x95,x96),z)) +(+(x,+(x95,x96)),z) -> +(x,+(+(x95,x96),z)) -(+(x,+(x99,x100))) -> -(+(+(x,x99),x100)) -(+(x,+(x99,x100))) -> +(-(x),-(+(x99,x100))) -(+(+(x,x99),x100)) -> +(-(+(x,x99)),-(x100)) +(-(+(x,x99)),-(x100)) -> +(+(-(x),-(x99)),-(x100)) +(-(x),-(+(x99,x100))) -> +(-(x),+(-(x99),-(x100))) +(-(x),+(-(x99),-(x100))) -> +(+(-(x),-(x99)),-(x100)) -(+(+(x,x99),x100)) -> -(+(x,+(x99,x100))) -(+(x,+(x99,x100))) -> +(-(x),-(+(x99,x100))) +(x,+(x102,x103)) -> +(+(x,x102),x103) +(x,+(x102,x103)) -> +(+(x102,x103),x) +(+(x,x102),x103) -> +(x,+(x102,x103)) +(+(x102,x103),x) -> +(x,+(x102,x103)) +(+(x,y),+(x105,x106)) -> +(+(+(x,y),x105),x106) +(+(x,y),+(x105,x106)) -> +(x,+(y,+(x105,x106))) +(+(+(x,y),x105),x106) -> +(+(x,y),+(x105,x106)) +(x,+(y,+(x105,x106))) -> +(+(x,y),+(x105,x106)) +(+(x,+(x108,x109)),z) -> +(+(+(x,x108),x109),z) +(+(x,+(x108,x109)),z) -> +(x,+(+(x108,x109),z)) +(+(+(x,x108),x109),z) -> +(+(x,+(x108,x109)),z) +(x,+(+(x108,x109),z)) -> +(+(x,+(x108,x109)),z) +(x,+(y,+(x111,x112))) -> +(x,+(+(y,x111),x112)) +(x,+(y,+(x111,x112))) -> +(+(x,y),+(x111,x112)) +(x,+(+(y,x111),x112)) -> +(x,+(y,+(x111,x112))) +(+(x,y),+(x111,x112)) -> +(x,+(y,+(x111,x112))) weak: -(+(x,y)) -> +(-(x),-(y)) +(x,y) -> +(y,x) +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) Polynomial Interpretation Processor: dimension: 1 interpretation: [-](x0) = 2x0 + 2, [+](x0, x1) = x0 + x1 + 3 orientation: -(+(x,y)) = 2x + 2y + 8 >= 2x + 2y + 8 = -(+(y,x)) -(+(x,y)) = 2x + 2y + 8 >= 2x + 2y + 7 = +(-(x),-(y)) -(+(y,x)) = 2x + 2y + 8 >= 2x + 2y + 7 = +(-(y),-(x)) +(-(x),-(y)) = 2x + 2y + 7 >= 2x + 2y + 7 = +(-(y),-(x)) +(+(x,y),z) = x + y + z + 6 >= x + y + z + 6 = +(z,+(x,y)) +(+(x,y),z) = x + y + z + 6 >= x + y + z + 6 = +(x,+(y,z)) +(z,+(x,y)) = x + y + z + 6 >= x + y + z + 6 = +(+(x,y),z) +(x,+(y,z)) = x + y + z + 6 >= x + y + z + 6 = +(+(x,y),z) +(+(x,y),z) = x + y + z + 6 >= x + y + z + 6 = +(+(y,x),z) +(+(x,y),z) = x + y + z + 6 >= x + y + z + 6 = +(x,+(y,z)) +(+(y,x),z) = x + y + z + 6 >= x + y + z + 6 = +(+(x,y),z) +(x,+(y,z)) = x + y + z + 6 >= x + y + z + 6 = +(+(x,y),z) +(x,+(y,z)) = x + y + z + 6 >= x + y + z + 6 = +(+(y,z),x) +(x,+(y,z)) = x + y + z + 6 >= x + y + z + 6 = +(+(x,y),z) +(+(y,z),x) = x + y + z + 6 >= x + y + z + 6 = +(x,+(y,z)) +(+(x,y),z) = x + y + z + 6 >= x + y + z + 6 = +(x,+(y,z)) +(x,+(y,z)) = x + y + z + 6 >= x + y + z + 6 = +(x,+(z,y)) +(x,+(y,z)) = x + y + z + 6 >= x + y + z + 6 = +(+(x,y),z) +(x,+(z,y)) = x + y + z + 6 >= x + y + z + 6 = +(x,+(y,z)) +(+(x,y),z) = x + y + z + 6 >= x + y + z + 6 = +(x,+(y,z)) -(+(+(x83,x84),y)) = 2x83 + 2x84 + 2y + 14 >= 2x83 + 2x84 + 2y + 14 = -(+(x83,+(x84,y))) -(+(+(x83,x84),y)) = 2x83 + 2x84 + 2y + 14 >= 2x83 + 2x84 + 2y + 13 = +(-(+(x83,x84)),-(y)) -(+(x83,+(x84,y))) = 2x83 + 2x84 + 2y + 14 >= 2x83 + 2x84 + 2y + 13 = +(-(x83),-(+(x84,y))) +(-(x83),-(+(x84,y))) = 2x83 + 2x84 + 2y + 13 >= 2x83 + 2x84 + 2y + 12 = +(-(x83),+(-(x84),-(y))) +(-(+(x83,x84)),-(y)) = 2x83 + 2x84 + 2y + 13 >= 2x83 + 2x84 + 2y + 12 = +(+(-(x83),-(x84)),-(y)) +(+(-(x83),-(x84)),-(y)) = 2x83 + 2x84 + 2y + 12 >= 2x83 + 2x84 + 2y + 12 = +(-(x83),+(-(x84),-(y))) -(+(x83,+(x84,y))) = 2x83 + 2x84 + 2y + 14 >= 2x83 + 2x84 + 2y + 14 = -(+(+(x83,x84),y)) -(+(+(x83,x84),y)) = 2x83 + 2x84 + 2y + 14 >= 2x83 + 2x84 + 2y + 13 = +(-(+(x83,x84)),-(y)) +(+(x86,x87),y) = x86 + x87 + y + 6 >= x86 + x87 + y + 6 = +(x86,+(x87,y)) +(+(x86,x87),y) = x86 + x87 + y + 6 >= x86 + x87 + y + 6 = +(y,+(x86,x87)) +(x86,+(x87,y)) = x86 + x87 + y + 6 >= x86 + x87 + y + 6 = +(+(x86,x87),y) +(y,+(x86,x87)) = x86 + x87 + y + 6 >= x86 + x87 + y + 6 = +(+(x86,x87),y) +(+(+(x89,x90),y),z) = x89 + x90 + y + z + 9 >= x89 + x90 + y + z + 9 = +(+(x89,+(x90,y)),z) +(+(+(x89,x90),y),z) = x89 + x90 + y + z + 9 >= x89 + x90 + y + z + 9 = +(+(x89,x90),+(y,z)) +(+(x89,+(x90,y)),z) = x89 + x90 + y + z + 9 >= x89 + x90 + y + z + 9 = +(+(+(x89,x90),y),z) +(+(x89,x90),+(y,z)) = x89 + x90 + y + z + 9 >= x89 + x90 + y + z + 9 = +(+(+(x89,x90),y),z) +(+(x92,x93),+(y,z)) = x92 + x93 + y + z + 9 >= x92 + x93 + y + z + 9 = +(x92,+(x93,+(y,z))) +(+(x92,x93),+(y,z)) = x92 + x93 + y + z + 9 >= x92 + x93 + y + z + 9 = +(+(+(x92,x93),y),z) +(x92,+(x93,+(y,z))) = x92 + x93 + y + z + 9 >= x92 + x93 + y + z + 9 = +(+(x92,x93),+(y,z)) +(+(+(x92,x93),y),z) = x92 + x93 + y + z + 9 >= x92 + x93 + y + z + 9 = +(+(x92,x93),+(y,z)) +(x,+(+(x95,x96),z)) = x + x95 + x96 + z + 9 >= x + x95 + x96 + z + 9 = +(x,+(x95,+(x96,z))) +(x,+(+(x95,x96),z)) = x + x95 + x96 + z + 9 >= x + x95 + x96 + z + 9 = +(+(x,+(x95,x96)),z) +(x,+(x95,+(x96,z))) = x + x95 + x96 + z + 9 >= x + x95 + x96 + z + 9 = +(x,+(+(x95,x96),z)) +(+(x,+(x95,x96)),z) = x + x95 + x96 + z + 9 >= x + x95 + x96 + z + 9 = +(x,+(+(x95,x96),z)) -(+(x,+(x99,x100))) = 2x + 2x100 + 2x99 + 14 >= 2x + 2x100 + 2x99 + 14 = -(+(+(x,x99),x100)) -(+(x,+(x99,x100))) = 2x + 2x100 + 2x99 + 14 >= 2x + 2x100 + 2x99 + 13 = +(-(x),-(+(x99,x100))) -(+(+(x,x99),x100)) = 2x + 2x100 + 2x99 + 14 >= 2x + 2x100 + 2x99 + 13 = +(-(+(x,x99)),-(x100)) +(-(+(x,x99)),-(x100)) = 2x + 2x100 + 2x99 + 13 >= 2x + 2x100 + 2x99 + 12 = +(+(-(x),-(x99)),-(x100)) +(-(x),-(+(x99,x100))) = 2x + 2x100 + 2x99 + 13 >= 2x + 2x100 + 2x99 + 12 = +(-(x),+(-(x99),-(x100))) +(-(x),+(-(x99),-(x100))) = 2x + 2x100 + 2x99 + 12 >= 2x + 2x100 + 2x99 + 12 = +(+(-(x),-(x99)),-(x100)) -(+(+(x,x99),x100)) = 2x + 2x100 + 2x99 + 14 >= 2x + 2x100 + 2x99 + 14 = -(+(x,+(x99,x100))) -(+(x,+(x99,x100))) = 2x + 2x100 + 2x99 + 14 >= 2x + 2x100 + 2x99 + 13 = +(-(x),-(+(x99,x100))) +(x,+(x102,x103)) = x + x102 + x103 + 6 >= x + x102 + x103 + 6 = +(+(x,x102),x103) +(x,+(x102,x103)) = x + x102 + x103 + 6 >= x + x102 + x103 + 6 = +(+(x102,x103),x) +(+(x,x102),x103) = x + x102 + x103 + 6 >= x + x102 + x103 + 6 = +(x,+(x102,x103)) +(+(x102,x103),x) = x + x102 + x103 + 6 >= x + x102 + x103 + 6 = +(x,+(x102,x103)) +(+(x,y),+(x105,x106)) = x + x105 + x106 + y + 9 >= x + x105 + x106 + y + 9 = +(+(+(x,y),x105),x106) +(+(x,y),+(x105,x106)) = x + x105 + x106 + y + 9 >= x + x105 + x106 + y + 9 = +(x,+(y,+(x105,x106))) +(+(+(x,y),x105),x106) = x + x105 + x106 + y + 9 >= x + x105 + x106 + y + 9 = +(+(x,y),+(x105,x106)) +(x,+(y,+(x105,x106))) = x + x105 + x106 + y + 9 >= x + x105 + x106 + y + 9 = +(+(x,y),+(x105,x106)) +(+(x,+(x108,x109)),z) = x + x108 + x109 + z + 9 >= x + x108 + x109 + z + 9 = +(+(+(x,x108),x109),z) +(+(x,+(x108,x109)),z) = x + x108 + x109 + z + 9 >= x + x108 + x109 + z + 9 = +(x,+(+(x108,x109),z)) +(+(+(x,x108),x109),z) = x + x108 + x109 + z + 9 >= x + x108 + x109 + z + 9 = +(+(x,+(x108,x109)),z) +(x,+(+(x108,x109),z)) = x + x108 + x109 + z + 9 >= x + x108 + x109 + z + 9 = +(+(x,+(x108,x109)),z) +(x,+(y,+(x111,x112))) = x + x111 + x112 + y + 9 >= x + x111 + x112 + y + 9 = +(x,+(+(y,x111),x112)) +(x,+(y,+(x111,x112))) = x + x111 + x112 + y + 9 >= x + x111 + x112 + y + 9 = +(+(x,y),+(x111,x112)) +(x,+(+(y,x111),x112)) = x + x111 + x112 + y + 9 >= x + x111 + x112 + y + 9 = +(x,+(y,+(x111,x112))) +(+(x,y),+(x111,x112)) = x + x111 + x112 + y + 9 >= x + x111 + x112 + y + 9 = +(x,+(y,+(x111,x112))) +(x,y) = x + y + 3 >= x + y + 3 = +(y,x) problem: strict: -(+(x,y)) -> -(+(y,x)) +(-(x),-(y)) -> +(-(y),-(x)) +(+(x,y),z) -> +(z,+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) +(z,+(x,y)) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(x,y),z) +(+(x,y),z) -> +(+(y,x),z) +(+(x,y),z) -> +(x,+(y,z)) +(+(y,x),z) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(y,z),x) +(x,+(y,z)) -> +(+(x,y),z) +(+(y,z),x) -> +(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(x,+(z,y)) +(x,+(y,z)) -> +(+(x,y),z) +(x,+(z,y)) -> +(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) -(+(+(x83,x84),y)) -> -(+(x83,+(x84,y))) +(+(-(x83),-(x84)),-(y)) -> +(-(x83),+(-(x84),-(y))) -(+(x83,+(x84,y))) -> -(+(+(x83,x84),y)) +(+(x86,x87),y) -> +(x86,+(x87,y)) +(+(x86,x87),y) -> +(y,+(x86,x87)) +(x86,+(x87,y)) -> +(+(x86,x87),y) +(y,+(x86,x87)) -> +(+(x86,x87),y) +(+(+(x89,x90),y),z) -> +(+(x89,+(x90,y)),z) +(+(+(x89,x90),y),z) -> +(+(x89,x90),+(y,z)) +(+(x89,+(x90,y)),z) -> +(+(+(x89,x90),y),z) +(+(x89,x90),+(y,z)) -> +(+(+(x89,x90),y),z) +(+(x92,x93),+(y,z)) -> +(x92,+(x93,+(y,z))) +(+(x92,x93),+(y,z)) -> +(+(+(x92,x93),y),z) +(x92,+(x93,+(y,z))) -> +(+(x92,x93),+(y,z)) +(+(+(x92,x93),y),z) -> +(+(x92,x93),+(y,z)) +(x,+(+(x95,x96),z)) -> +(x,+(x95,+(x96,z))) +(x,+(+(x95,x96),z)) -> +(+(x,+(x95,x96)),z) +(x,+(x95,+(x96,z))) -> +(x,+(+(x95,x96),z)) +(+(x,+(x95,x96)),z) -> +(x,+(+(x95,x96),z)) -(+(x,+(x99,x100))) -> -(+(+(x,x99),x100)) +(-(x),+(-(x99),-(x100))) -> +(+(-(x),-(x99)),-(x100)) -(+(+(x,x99),x100)) -> -(+(x,+(x99,x100))) +(x,+(x102,x103)) -> +(+(x,x102),x103) +(x,+(x102,x103)) -> +(+(x102,x103),x) +(+(x,x102),x103) -> +(x,+(x102,x103)) +(+(x102,x103),x) -> +(x,+(x102,x103)) +(+(x,y),+(x105,x106)) -> +(+(+(x,y),x105),x106) +(+(x,y),+(x105,x106)) -> +(x,+(y,+(x105,x106))) +(+(+(x,y),x105),x106) -> +(+(x,y),+(x105,x106)) +(x,+(y,+(x105,x106))) -> +(+(x,y),+(x105,x106)) +(+(x,+(x108,x109)),z) -> +(+(+(x,x108),x109),z) +(+(x,+(x108,x109)),z) -> +(x,+(+(x108,x109),z)) +(+(+(x,x108),x109),z) -> +(+(x,+(x108,x109)),z) +(x,+(+(x108,x109),z)) -> +(+(x,+(x108,x109)),z) +(x,+(y,+(x111,x112))) -> +(x,+(+(y,x111),x112)) +(x,+(y,+(x111,x112))) -> +(+(x,y),+(x111,x112)) +(x,+(+(y,x111),x112)) -> +(x,+(y,+(x111,x112))) +(+(x,y),+(x111,x112)) -> +(x,+(y,+(x111,x112))) weak: +(x,y) -> +(y,x) +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) Shift Processor (ldh) lab=left (force): strict: weak: Decreasing Processor: The following diagrams are decreasing: peak: -(+(y,x)) <-1|0[1]- -(+(x,y)) -0|[1]-> +(-(x),-(y)) joins: -(+(y,x)) -0|[1]-> +(-(y),-(x)) +(-(x),-(y)) -1|[0]-> +(-(y),-(x)) peak: +(z,+(x,y)) <-1|[1]- +(+(x,y),z) -2|[1]-> +(x,+(y,z)) joins: +(z,+(x,y)) -1|[1]-> +(+(x,y),z) +(x,+(y,z)) -3|[1]-> +(+(x,y),z) peak: +(+(y,x),z) <-1|0[1]- +(+(x,y),z) -2|[1]-> +(x,+(y,z)) joins: +(+(y,x),z) -1|0[1]-> +(+(x,y),z) +(x,+(y,z)) -3|[1]-> +(+(x,y),z) peak: +(+(y,z),x) <-1|[1]- +(x,+(y,z)) -3|[1]-> +(+(x,y),z) joins: +(+(y,z),x) -1|[1]-> +(x,+(y,z)) +(+(x,y),z) -2|[1]-> +(x,+(y,z)) peak: +(x,+(z,y)) <-1|1[1]- +(x,+(y,z)) -3|[1]-> +(+(x,y),z) joins: +(x,+(z,y)) -1|1[1]-> +(x,+(y,z)) +(+(x,y),z) -2|[1]-> +(x,+(y,z)) peak: -(+(x83,+(x84,y))) <-2|0[1]- -(+(+(x83,x84),y)) -0|[1]-> +(-(+(x83,x84)),-(y)) joins: -(+(x83,+(x84,y))) -0|[1]-> +(-(x83),-(+(x84,y))) -0|1[0]-> +(-(x83),+(-(x84),-(y))) +(-(+(x83,x84)),-(y)) -0|0[0]-> +(+(-(x83),-(x84)),-(y)) -2| [0]-> +(-(x83),+(-(x84),-(y))) peak: +(x86,+(x87,y)) <-2|[1]- +(+(x86,x87),y) -1|[1]-> +(y,+(x86,x87)) joins: +(x86,+(x87,y)) -3|[1]-> +(+(x86,x87),y) +(y,+(x86,x87)) -1|[1]-> +(+(x86,x87),y) peak: +(+(x89,+(x90,y)),z) <-2|0[1]- +(+(+(x89,x90),y),z) -2|[1]-> +(+(x89,x90),+(y,z)) joins: +(+(x89,+(x90,y)),z) -3|0[1]-> +(+(+(x89,x90),y),z) +(+(x89,x90),+(y,z)) -3|[1]-> +(+(+(x89,x90),y),z) peak: +(x92,+(x93,+(y,z))) <-2|[1]- +(+(x92,x93),+(y,z)) -3|[1]-> +(+(+(x92,x93),y),z) joins: +(x92,+(x93,+(y,z))) -3|[1]-> +(+(x92,x93),+(y,z)) +(+(+(x92,x93),y),z) -2|[1]-> +(+(x92,x93),+(y,z)) peak: +(x,+(x95,+(x96,z))) <-2|1[1]- +(x,+(+(x95,x96),z)) -3|[1]-> +(+(x,+(x95,x96)),z) joins: +(x,+(x95,+(x96,z))) -3|1[1]-> +(x,+(+(x95,x96),z)) +(+(x,+(x95,x96)),z) -2|[1]-> +(x,+(+(x95,x96),z)) peak: -(+(+(x,x99),x100)) <-3|0[1]- -(+(x,+(x99,x100))) -0|[1]-> +(-(x),-(+(x99,x100))) joins: -(+(+(x,x99),x100)) -0|[1]-> +(-(+(x,x99)),-(x100)) -0|0[0]-> +(+(-(x),-(x99)),-(x100)) +(-(x),-(+(x99,x100))) -0|1[0]-> +(-(x),+(-(x99),-(x100))) -3| [0]-> +(+(-(x),-(x99)),-(x100)) peak: +(+(x,x102),x103) <-3|[1]- +(x,+(x102,x103)) -1|[1]-> +(+(x102,x103),x) joins: +(+(x,x102),x103) -2|[1]-> +(x,+(x102,x103)) +(+(x102,x103),x) -1|[1]-> +(x,+(x102,x103)) peak: +(+(+(x,y),x105),x106) <-3|[1]- +(+(x,y),+(x105,x106)) -2|[1]-> +(x,+(y,+(x105,x106))) joins: +(+(+(x,y),x105),x106) -2|[1]-> +(+(x,y),+(x105,x106)) +(x,+(y,+(x105,x106))) -3|[1]-> +(+(x,y),+(x105,x106)) peak: +(+(+(x,x108),x109),z) <-3|0[1]- +(+(x,+(x108,x109)),z) -2|[1]-> +(x,+(+(x108,x109),z)) joins: +(+(+(x,x108),x109),z) -2|0[1]-> +(+(x,+(x108,x109)),z) +(x,+(+(x108,x109),z)) -3|[1]-> +(+(x,+(x108,x109)),z) peak: +(x,+(+(y,x111),x112)) <-3|1[1]- +(x,+(y,+(x111,x112))) -3|[1]-> +(+(x,y),+(x111,x112)) joins: +(x,+(+(y,x111),x112)) -2|1[1]-> +(x,+(y,+(x111,x112))) +(+(x,y),+(x111,x112)) -2|[1]-> +(x,+(y,+(x111,x112))) Qed