Problem: a1() -> b1() a1() -> c1() b1() -> b2() c1() -> c2() a2() -> b2() a2() -> c2() b2() -> b3() c2() -> c3() a3() -> b3() a3() -> c3() b3() -> b4() c3() -> c4() a4() -> b4() a4() -> c4() b4() -> b5() c4() -> c5() a5() -> b5() a5() -> c5() b5() -> b6() c5() -> c6() a6() -> b6() a6() -> c6() b6() -> b7() c6() -> c7() a7() -> b7() a7() -> c7() b7() -> b8() c7() -> c8() a8() -> b8() a8() -> c8() b8() -> b9() c8() -> c9() a9() -> b9() a9() -> c9() b9() -> b10() c9() -> c10() a10() -> b11() b10() -> b11() c10() -> b11() Proof: sorted: (order) 0:a1() -> b1() a1() -> c1() b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() 1:a2() -> b2() a2() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() 2:a3() -> b3() a3() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() 3:a4() -> b4() a4() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() 4:a5() -> b5() a5() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() 5:a6() -> b6() a6() -> c6() b6() -> b7() c6() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() 6:a7() -> b7() a7() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() 7:a8() -> b8() a8() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() 8:a9() -> b9() a9() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() 9:a10() -> b11() ----- sorts [0>1, 0>2, 1>5, 2>4, 3>4, 3>5, 4>7, 5>8, 6>7, 6>8, 7>10, 8>11, 9>10, 9>11, 10>13, 11>14, 12>13, 12>14, 13>16, 14>17, 15>16, 15>17, 16>19, 17>20, 18>19, 18>20, 19>22, 20>23, 21>22, 21>23, 22>25, 23>26, 24>25, 24>26, 25>28, 26>27, 27>30, 28>30, 29>30] sort attachment (non-strict) a1 : 0 b1 : 1 c1 : 2 b2 : 5 c2 : 4 a2 : 3 b3 : 8 c3 : 7 a3 : 6 b4 : 11 c4 : 10 a4 : 9 b5 : 14 c5 : 13 a5 : 12 b6 : 17 c6 : 16 a6 : 15 b7 : 20 c7 : 19 a7 : 18 b8 : 23 c8 : 22 a8 : 21 b9 : 26 c9 : 25 a9 : 24 b10 : 27 c10 : 28 a10 : 29 b11 : 30 ----- 0:a1() -> b1() a1() -> c1() b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() Uncurry Processor: a1() -> b1() a1() -> c1() b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() Ground Confluence Processor: confluent by decision procedure. 1:a2() -> b2() a2() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() Uncurry Processor: a2() -> b2() a2() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() Ground Confluence Processor: confluent by decision procedure. 2:a3() -> b3() a3() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() Church Rosser Transformation Processor (critical pair closing system, Thm 2.11): b3() -> b4() b4() -> b5() b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c3() -> c4() c4() -> c5() c5() -> c6() c6() -> c7() c7() -> c8() c8() -> c9() c9() -> c10() c10() -> b11() critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [c10] = 0, [b10] = 0, [c9] = 1, [b9] = 0, [c8] = 2, [b8] = 0, [c7] = 2, [b7] = 0, [c6] = 2, [b6] = 0, [c5] = 3, [b5] = 0, [c4] = 4, [b4] = 0, [c3] = 4, [b3] = 0 orientation: b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c3() = 4 >= 4 = c4() c4() = 4 >= 3 = c5() c5() = 3 >= 2 = c6() c6() = 2 >= 2 = c7() c7() = 2 >= 2 = c8() c8() = 2 >= 1 = c9() c9() = 1 >= 0 = c10() c10() = 0 >= 0 = b11() problem: b3() -> b4() b4() -> b5() b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c3() -> c4() c6() -> c7() c7() -> c8() c10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [c10] = 1, [b10] = 0, [b9] = 0, [c8] = 0, [b8] = 0, [c7] = 0, [b7] = 0, [c6] = 0, [b6] = 0, [b5] = 0, [c4] = 0, [b4] = 0, [c3] = 0, [b3] = 0 orientation: b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c3() = 0 >= 0 = c4() c6() = 0 >= 0 = c7() c7() = 0 >= 0 = c8() c10() = 1 >= 0 = b11() problem: b3() -> b4() b4() -> b5() b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c3() -> c4() c6() -> c7() c7() -> c8() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 0, [c8] = 0, [b8] = 0, [c7] = 4, [b7] = 0, [c6] = 4, [b6] = 0, [b5] = 0, [c4] = 0, [b4] = 0, [c3] = 0, [b3] = 0 orientation: b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c3() = 0 >= 0 = c4() c6() = 4 >= 4 = c7() c7() = 4 >= 0 = c8() problem: b3() -> b4() b4() -> b5() b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c3() -> c4() c6() -> c7() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 0, [b8] = 0, [c7] = 0, [b7] = 0, [c6] = 1, [b6] = 0, [b5] = 0, [c4] = 0, [b4] = 0, [c3] = 0, [b3] = 0 orientation: b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c3() = 0 >= 0 = c4() c6() = 1 >= 0 = c7() problem: b3() -> b4() b4() -> b5() b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c3() -> c4() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 0, [b8] = 0, [b7] = 0, [b6] = 0, [b5] = 0, [c4] = 0, [b4] = 0, [c3] = 1, [b3] = 0 orientation: b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c3() = 1 >= 0 = c4() problem: b3() -> b4() b4() -> b5() b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 1, [b8] = 2, [b7] = 2, [b6] = 2, [b5] = 2, [b4] = 4, [b3] = 4 orientation: b3() = 4 >= 4 = b4() b4() = 4 >= 2 = b5() b5() = 2 >= 2 = b6() b6() = 2 >= 2 = b7() b7() = 2 >= 2 = b8() b8() = 2 >= 1 = b9() b9() = 1 >= 0 = b10() b10() = 0 >= 0 = b11() problem: b3() -> b4() b5() -> b6() b6() -> b7() b7() -> b8() b10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 1, [b8] = 0, [b7] = 0, [b6] = 0, [b5] = 0, [b4] = 0, [b3] = 0 orientation: b3() = 0 >= 0 = b4() b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b10() = 1 >= 0 = b11() problem: b3() -> b4() b5() -> b6() b6() -> b7() b7() -> b8() Matrix Interpretation Processor: dim=1 interpretation: [b8] = 0, [b7] = 0, [b6] = 4, [b5] = 4, [b4] = 0, [b3] = 0 orientation: b3() = 0 >= 0 = b4() b5() = 4 >= 4 = b6() b6() = 4 >= 0 = b7() b7() = 0 >= 0 = b8() problem: b3() -> b4() b5() -> b6() b7() -> b8() Matrix Interpretation Processor: dim=1 interpretation: [b8] = 0, [b7] = 1, [b6] = 0, [b5] = 0, [b4] = 0, [b3] = 0 orientation: b3() = 0 >= 0 = b4() b5() = 0 >= 0 = b6() b7() = 1 >= 0 = b8() problem: b3() -> b4() b5() -> b6() Matrix Interpretation Processor: dim=1 interpretation: [b6] = 0, [b5] = 1, [b4] = 0, [b3] = 0 orientation: b3() = 0 >= 0 = b4() b5() = 1 >= 0 = b6() problem: b3() -> b4() Matrix Interpretation Processor: dim=1 interpretation: [b4] = 0, [b3] = 1 orientation: b3() = 1 >= 0 = b4() problem: Qed 3:a4() -> b4() a4() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() Church Rosser Transformation Processor (critical pair closing system, Thm 2.11): b4() -> b5() b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c4() -> c5() c5() -> c6() c6() -> c7() c7() -> c8() c8() -> c9() c9() -> c10() c10() -> b11() critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [c10] = 1, [b10] = 0, [c9] = 4, [b9] = 0, [c8] = 4, [b8] = 0, [c7] = 4, [b7] = 0, [c6] = 4, [b6] = 0, [c5] = 4, [b5] = 0, [c4] = 4, [b4] = 0 orientation: b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c4() = 4 >= 4 = c5() c5() = 4 >= 4 = c6() c6() = 4 >= 4 = c7() c7() = 4 >= 4 = c8() c8() = 4 >= 4 = c9() c9() = 4 >= 1 = c10() c10() = 1 >= 0 = b11() problem: b4() -> b5() b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c4() -> c5() c5() -> c6() c6() -> c7() c7() -> c8() c8() -> c9() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [c9] = 0, [b9] = 0, [c8] = 0, [b8] = 0, [c7] = 0, [b7] = 0, [c6] = 4, [b6] = 0, [c5] = 4, [b5] = 0, [c4] = 4, [b4] = 0 orientation: b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c4() = 4 >= 4 = c5() c5() = 4 >= 4 = c6() c6() = 4 >= 0 = c7() c7() = 0 >= 0 = c8() c8() = 0 >= 0 = c9() problem: b4() -> b5() b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c4() -> c5() c5() -> c6() c7() -> c8() c8() -> c9() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [c9] = 0, [b9] = 0, [c8] = 4, [b8] = 0, [c7] = 4, [b7] = 0, [c6] = 0, [b6] = 0, [c5] = 0, [b5] = 0, [c4] = 0, [b4] = 0 orientation: b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c4() = 0 >= 0 = c5() c5() = 0 >= 0 = c6() c7() = 4 >= 4 = c8() c8() = 4 >= 0 = c9() problem: b4() -> b5() b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c4() -> c5() c5() -> c6() c7() -> c8() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 0, [c8] = 0, [b8] = 0, [c7] = 1, [b7] = 0, [c6] = 0, [b6] = 0, [c5] = 0, [b5] = 0, [c4] = 0, [b4] = 0 orientation: b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c4() = 0 >= 0 = c5() c5() = 0 >= 0 = c6() c7() = 1 >= 0 = c8() problem: b4() -> b5() b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c4() -> c5() c5() -> c6() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 0, [b8] = 0, [b7] = 0, [c6] = 0, [b6] = 0, [c5] = 4, [b5] = 0, [c4] = 4, [b4] = 0 orientation: b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c4() = 4 >= 4 = c5() c5() = 4 >= 0 = c6() problem: b4() -> b5() b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c4() -> c5() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 0, [b8] = 0, [b7] = 0, [b6] = 0, [c5] = 0, [b5] = 0, [c4] = 1, [b4] = 0 orientation: b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c4() = 1 >= 0 = c5() problem: b4() -> b5() b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 1, [b8] = 2, [b7] = 2, [b6] = 4, [b5] = 4, [b4] = 4 orientation: b4() = 4 >= 4 = b5() b5() = 4 >= 4 = b6() b6() = 4 >= 2 = b7() b7() = 2 >= 2 = b8() b8() = 2 >= 1 = b9() b9() = 1 >= 0 = b10() b10() = 0 >= 0 = b11() problem: b4() -> b5() b5() -> b6() b7() -> b8() b10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 1, [b8] = 0, [b7] = 0, [b6] = 0, [b5] = 0, [b4] = 0 orientation: b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() b7() = 0 >= 0 = b8() b10() = 1 >= 0 = b11() problem: b4() -> b5() b5() -> b6() b7() -> b8() Matrix Interpretation Processor: dim=1 interpretation: [b8] = 0, [b7] = 1, [b6] = 0, [b5] = 0, [b4] = 0 orientation: b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() b7() = 1 >= 0 = b8() problem: b4() -> b5() b5() -> b6() Matrix Interpretation Processor: dim=1 interpretation: [b6] = 0, [b5] = 4, [b4] = 4 orientation: b4() = 4 >= 4 = b5() b5() = 4 >= 0 = b6() problem: b4() -> b5() Matrix Interpretation Processor: dim=1 interpretation: [b5] = 0, [b4] = 1 orientation: b4() = 1 >= 0 = b5() problem: Qed 4:a5() -> b5() a5() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() Church Rosser Transformation Processor (critical pair closing system, Thm 2.11): b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c5() -> c6() c6() -> c7() c7() -> c8() c8() -> c9() c9() -> c10() c10() -> b11() critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [c10] = 0, [b10] = 0, [c9] = 0, [b9] = 0, [c8] = 1, [b8] = 0, [c7] = 4, [b7] = 0, [c6] = 4, [b6] = 0, [c5] = 4, [b5] = 0 orientation: b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c5() = 4 >= 4 = c6() c6() = 4 >= 4 = c7() c7() = 4 >= 1 = c8() c8() = 1 >= 0 = c9() c9() = 0 >= 0 = c10() c10() = 0 >= 0 = b11() problem: b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c5() -> c6() c6() -> c7() c9() -> c10() c10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [c10] = 4, [b10] = 0, [c9] = 4, [b9] = 0, [b8] = 0, [c7] = 0, [b7] = 0, [c6] = 0, [b6] = 0, [c5] = 0, [b5] = 0 orientation: b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c5() = 0 >= 0 = c6() c6() = 0 >= 0 = c7() c9() = 4 >= 4 = c10() c10() = 4 >= 0 = b11() problem: b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c5() -> c6() c6() -> c7() c9() -> c10() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [c10] = 0, [b10] = 0, [c9] = 1, [b9] = 0, [b8] = 0, [c7] = 0, [b7] = 0, [c6] = 0, [b6] = 0, [c5] = 0, [b5] = 0 orientation: b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c5() = 0 >= 0 = c6() c6() = 0 >= 0 = c7() c9() = 1 >= 0 = c10() problem: b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c5() -> c6() c6() -> c7() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 0, [b8] = 0, [c7] = 0, [b7] = 0, [c6] = 4, [b6] = 0, [c5] = 4, [b5] = 0 orientation: b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c5() = 4 >= 4 = c6() c6() = 4 >= 0 = c7() problem: b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c5() -> c6() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 0, [b8] = 0, [b7] = 0, [c6] = 0, [b6] = 0, [c5] = 1, [b5] = 0 orientation: b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c5() = 1 >= 0 = c6() problem: b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 4, [b8] = 4, [b7] = 4, [b6] = 4, [b5] = 4 orientation: b5() = 4 >= 4 = b6() b6() = 4 >= 4 = b7() b7() = 4 >= 4 = b8() b8() = 4 >= 4 = b9() b9() = 4 >= 0 = b10() b10() = 0 >= 0 = b11() problem: b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() b10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 1, [b9] = 0, [b8] = 0, [b7] = 0, [b6] = 0, [b5] = 0 orientation: b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b10() = 1 >= 0 = b11() problem: b5() -> b6() b6() -> b7() b7() -> b8() b8() -> b9() Matrix Interpretation Processor: dim=1 interpretation: [b9] = 0, [b8] = 0, [b7] = 4, [b6] = 4, [b5] = 4 orientation: b5() = 4 >= 4 = b6() b6() = 4 >= 4 = b7() b7() = 4 >= 0 = b8() b8() = 0 >= 0 = b9() problem: b5() -> b6() b6() -> b7() b8() -> b9() Matrix Interpretation Processor: dim=1 interpretation: [b9] = 0, [b8] = 1, [b7] = 0, [b6] = 0, [b5] = 0 orientation: b5() = 0 >= 0 = b6() b6() = 0 >= 0 = b7() b8() = 1 >= 0 = b9() problem: b5() -> b6() b6() -> b7() Matrix Interpretation Processor: dim=1 interpretation: [b7] = 0, [b6] = 4, [b5] = 4 orientation: b5() = 4 >= 4 = b6() b6() = 4 >= 0 = b7() problem: b5() -> b6() Matrix Interpretation Processor: dim=1 interpretation: [b6] = 0, [b5] = 1 orientation: b5() = 1 >= 0 = b6() problem: Qed 5:a6() -> b6() a6() -> c6() b6() -> b7() c6() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() Church Rosser Transformation Processor (critical pair closing system, Thm 2.11): b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c6() -> c7() c7() -> c8() c8() -> c9() c9() -> c10() c10() -> b11() critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [c10] = 0, [b10] = 0, [c9] = 0, [b9] = 0, [c8] = 0, [b8] = 0, [c7] = 4, [b7] = 0, [c6] = 4, [b6] = 0 orientation: b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c6() = 4 >= 4 = c7() c7() = 4 >= 0 = c8() c8() = 0 >= 0 = c9() c9() = 0 >= 0 = c10() c10() = 0 >= 0 = b11() problem: b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c6() -> c7() c8() -> c9() c9() -> c10() c10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [c10] = 0, [b10] = 0, [c9] = 4, [b9] = 0, [c8] = 4, [b8] = 0, [c7] = 0, [b7] = 0, [c6] = 0, [b6] = 0 orientation: b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c6() = 0 >= 0 = c7() c8() = 4 >= 4 = c9() c9() = 4 >= 0 = c10() c10() = 0 >= 0 = b11() problem: b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c6() -> c7() c8() -> c9() c10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [c10] = 1, [b10] = 0, [c9] = 0, [b9] = 0, [c8] = 0, [b8] = 0, [c7] = 0, [b7] = 0, [c6] = 0, [b6] = 0 orientation: b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c6() = 0 >= 0 = c7() c8() = 0 >= 0 = c9() c10() = 1 >= 0 = b11() problem: b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c6() -> c7() c8() -> c9() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [c9] = 0, [b9] = 0, [c8] = 1, [b8] = 0, [c7] = 0, [b7] = 0, [c6] = 0, [b6] = 0 orientation: b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c6() = 0 >= 0 = c7() c8() = 1 >= 0 = c9() problem: b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c6() -> c7() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 0, [b8] = 0, [c7] = 0, [b7] = 0, [c6] = 1, [b6] = 0 orientation: b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c6() = 1 >= 0 = c7() problem: b6() -> b7() b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 0, [b8] = 4, [b7] = 4, [b6] = 4 orientation: b6() = 4 >= 4 = b7() b7() = 4 >= 4 = b8() b8() = 4 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() problem: b6() -> b7() b7() -> b8() b9() -> b10() b10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 4, [b9] = 4, [b8] = 0, [b7] = 0, [b6] = 0 orientation: b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b9() = 4 >= 4 = b10() b10() = 4 >= 0 = b11() problem: b6() -> b7() b7() -> b8() b9() -> b10() Matrix Interpretation Processor: dim=1 interpretation: [b10] = 0, [b9] = 1, [b8] = 0, [b7] = 0, [b6] = 0 orientation: b6() = 0 >= 0 = b7() b7() = 0 >= 0 = b8() b9() = 1 >= 0 = b10() problem: b6() -> b7() b7() -> b8() Matrix Interpretation Processor: dim=1 interpretation: [b8] = 0, [b7] = 4, [b6] = 4 orientation: b6() = 4 >= 4 = b7() b7() = 4 >= 0 = b8() problem: b6() -> b7() Matrix Interpretation Processor: dim=1 interpretation: [b7] = 0, [b6] = 1 orientation: b6() = 1 >= 0 = b7() problem: Qed 6:a7() -> b7() a7() -> c7() b7() -> b8() c7() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() Church Rosser Transformation Processor (critical pair closing system, Thm 2.11): b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c7() -> c8() c8() -> c9() c9() -> c10() c10() -> b11() critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [c10] = 0, [b10] = 0, [c9] = 1, [b9] = 0, [c8] = 4, [b8] = 0, [c7] = 4, [b7] = 0 orientation: b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c7() = 4 >= 4 = c8() c8() = 4 >= 1 = c9() c9() = 1 >= 0 = c10() c10() = 0 >= 0 = b11() problem: b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c7() -> c8() c10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [c10] = 1, [b10] = 0, [b9] = 0, [c8] = 0, [b8] = 0, [c7] = 0, [b7] = 0 orientation: b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c7() = 0 >= 0 = c8() c10() = 1 >= 0 = b11() problem: b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() c7() -> c8() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 0, [c8] = 0, [b8] = 0, [c7] = 1, [b7] = 0 orientation: b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c7() = 1 >= 0 = c8() problem: b7() -> b8() b8() -> b9() b9() -> b10() b10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 4, [b8] = 4, [b7] = 4 orientation: b7() = 4 >= 4 = b8() b8() = 4 >= 4 = b9() b9() = 4 >= 0 = b10() b10() = 0 >= 0 = b11() problem: b7() -> b8() b8() -> b9() b10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 1, [b9] = 0, [b8] = 0, [b7] = 0 orientation: b7() = 0 >= 0 = b8() b8() = 0 >= 0 = b9() b10() = 1 >= 0 = b11() problem: b7() -> b8() b8() -> b9() Matrix Interpretation Processor: dim=1 interpretation: [b9] = 0, [b8] = 4, [b7] = 4 orientation: b7() = 4 >= 4 = b8() b8() = 4 >= 0 = b9() problem: b7() -> b8() Matrix Interpretation Processor: dim=1 interpretation: [b8] = 0, [b7] = 1 orientation: b7() = 1 >= 0 = b8() problem: Qed 7:a8() -> b8() a8() -> c8() b8() -> b9() c8() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() Church Rosser Transformation Processor (critical pair closing system, Thm 2.11): b8() -> b9() b9() -> b10() b10() -> b11() c8() -> c9() c9() -> c10() c10() -> b11() critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [c10] = 0, [b10] = 0, [c9] = 4, [b9] = 0, [c8] = 4, [b8] = 0 orientation: b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c8() = 4 >= 4 = c9() c9() = 4 >= 0 = c10() c10() = 0 >= 0 = b11() problem: b8() -> b9() b9() -> b10() b10() -> b11() c8() -> c9() c10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [c10] = 1, [b10] = 0, [c9] = 0, [b9] = 0, [c8] = 0, [b8] = 0 orientation: b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c8() = 0 >= 0 = c9() c10() = 1 >= 0 = b11() problem: b8() -> b9() b9() -> b10() b10() -> b11() c8() -> c9() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [c9] = 0, [b9] = 0, [c8] = 1, [b8] = 0 orientation: b8() = 0 >= 0 = b9() b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c8() = 1 >= 0 = c9() problem: b8() -> b9() b9() -> b10() b10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 0, [b9] = 4, [b8] = 4 orientation: b8() = 4 >= 4 = b9() b9() = 4 >= 0 = b10() b10() = 0 >= 0 = b11() problem: b8() -> b9() b10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 1, [b9] = 0, [b8] = 0 orientation: b8() = 0 >= 0 = b9() b10() = 1 >= 0 = b11() problem: b8() -> b9() Matrix Interpretation Processor: dim=1 interpretation: [b9] = 0, [b8] = 1 orientation: b8() = 1 >= 0 = b9() problem: Qed 8:a9() -> b9() a9() -> c9() b9() -> b10() c9() -> c10() b10() -> b11() c10() -> b11() Church Rosser Transformation Processor (critical pair closing system, Thm 2.11): b9() -> b10() b10() -> b11() c9() -> c10() c10() -> b11() critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [c10] = 4, [b10] = 0, [c9] = 4, [b9] = 0 orientation: b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c9() = 4 >= 4 = c10() c10() = 4 >= 0 = b11() problem: b9() -> b10() b10() -> b11() c9() -> c10() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [c10] = 0, [b10] = 0, [c9] = 1, [b9] = 0 orientation: b9() = 0 >= 0 = b10() b10() = 0 >= 0 = b11() c9() = 1 >= 0 = c10() problem: b9() -> b10() b10() -> b11() Matrix Interpretation Processor: dim=1 interpretation: [b11] = 0, [b10] = 4, [b9] = 4 orientation: b9() = 4 >= 4 = b10() b10() = 4 >= 0 = b11() problem: b9() -> b10() Matrix Interpretation Processor: dim=1 interpretation: [b10] = 0, [b9] = 1 orientation: b9() = 1 >= 0 = b10() problem: Qed 9:a10() -> b11() Church Rosser Transformation Processor (critical pair closing system, Thm 2.11): critical peaks: joinable Qed