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() -> b6() b5() -> b6() c5() -> b6() Proof: sorted: (order-sorted) 0:a1() -> b1() a1() -> c1() b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() 1:a2() -> b2() a2() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() 2:a3() -> b3() a3() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() 3:a4() -> b4() a4() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() 4:a5() -> b6() ----- 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>12, 12>15, 13>15, 14>15] 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 : 12 c5 : 13 a5 : 14 b6 : 15 ----- 0:a1() -> b1() a1() -> c1() b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() Church Rosser Transformation Processor: b1() -> b2() b2() -> b3() b3() -> b4() b4() -> b5() b5() -> b6() c1() -> c2() c2() -> c3() c3() -> c4() c4() -> c5() c5() -> b6() critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [c2] = 4, [b6] = 0, [b1] = 0, [b2] = 0, [c4] = 0, [c3] = 0, [b5] = 0, [b4] = 0, [c5] = 0, [b3] = 0, [c1] = 4 orientation: b1() = 0 >= 0 = b2() b2() = 0 >= 0 = b3() b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() c1() = 4 >= 4 = c2() c2() = 4 >= 0 = c3() c3() = 0 >= 0 = c4() c4() = 0 >= 0 = c5() c5() = 0 >= 0 = b6() problem: b1() -> b2() b2() -> b3() b3() -> b4() b4() -> b5() b5() -> b6() c1() -> c2() c3() -> c4() c4() -> c5() c5() -> b6() Matrix Interpretation Processor: dim=1 interpretation: [c2] = 0, [b6] = 0, [b1] = 0, [b2] = 0, [c4] = 4, [c3] = 4, [b5] = 0, [b4] = 0, [c5] = 0, [b3] = 0, [c1] = 0 orientation: b1() = 0 >= 0 = b2() b2() = 0 >= 0 = b3() b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() c1() = 0 >= 0 = c2() c3() = 4 >= 4 = c4() c4() = 4 >= 0 = c5() c5() = 0 >= 0 = b6() problem: b1() -> b2() b2() -> b3() b3() -> b4() b4() -> b5() b5() -> b6() c1() -> c2() c3() -> c4() c5() -> b6() Matrix Interpretation Processor: dim=1 interpretation: [c2] = 0, [b6] = 0, [b1] = 0, [b2] = 0, [c4] = 0, [c3] = 0, [b5] = 0, [b4] = 0, [c5] = 1, [b3] = 0, [c1] = 0 orientation: b1() = 0 >= 0 = b2() b2() = 0 >= 0 = b3() b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() c1() = 0 >= 0 = c2() c3() = 0 >= 0 = c4() c5() = 1 >= 0 = b6() problem: b1() -> b2() b2() -> b3() b3() -> b4() b4() -> b5() b5() -> b6() c1() -> c2() c3() -> c4() Matrix Interpretation Processor: dim=1 interpretation: [c2] = 0, [b6] = 0, [b1] = 0, [b2] = 0, [c4] = 0, [c3] = 1, [b5] = 0, [b4] = 0, [b3] = 0, [c1] = 0 orientation: b1() = 0 >= 0 = b2() b2() = 0 >= 0 = b3() b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() c1() = 0 >= 0 = c2() c3() = 1 >= 0 = c4() problem: b1() -> b2() b2() -> b3() b3() -> b4() b4() -> b5() b5() -> b6() c1() -> c2() Matrix Interpretation Processor: dim=1 interpretation: [c2] = 0, [b6] = 0, [b1] = 0, [b2] = 0, [b5] = 0, [b4] = 0, [b3] = 0, [c1] = 1 orientation: b1() = 0 >= 0 = b2() b2() = 0 >= 0 = b3() b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() c1() = 1 >= 0 = c2() problem: b1() -> b2() b2() -> b3() b3() -> b4() b4() -> b5() b5() -> b6() Matrix Interpretation Processor: dim=1 interpretation: [b6] = 0, [b1] = 4, [b2] = 4, [b5] = 0, [b4] = 0, [b3] = 4 orientation: b1() = 4 >= 4 = b2() b2() = 4 >= 4 = b3() b3() = 4 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() problem: b1() -> b2() b2() -> b3() b4() -> b5() b5() -> b6() Matrix Interpretation Processor: dim=1 interpretation: [b6] = 0, [b1] = 0, [b2] = 0, [b5] = 4, [b4] = 4, [b3] = 0 orientation: b1() = 0 >= 0 = b2() b2() = 0 >= 0 = b3() b4() = 4 >= 4 = b5() b5() = 4 >= 0 = b6() problem: b1() -> b2() b2() -> b3() b4() -> b5() Matrix Interpretation Processor: dim=1 interpretation: [b1] = 0, [b2] = 0, [b5] = 0, [b4] = 1, [b3] = 0 orientation: b1() = 0 >= 0 = b2() b2() = 0 >= 0 = b3() b4() = 1 >= 0 = b5() problem: b1() -> b2() b2() -> b3() Matrix Interpretation Processor: dim=1 interpretation: [b1] = 4, [b2] = 4, [b3] = 0 orientation: b1() = 4 >= 4 = b2() b2() = 4 >= 0 = b3() problem: b1() -> b2() Matrix Interpretation Processor: dim=1 interpretation: [b1] = 1, [b2] = 0 orientation: b1() = 1 >= 0 = b2() problem: Qed 1:a2() -> b2() a2() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() Church Rosser Transformation Processor: b2() -> b3() b3() -> b4() b4() -> b5() b5() -> b6() c2() -> c3() c3() -> c4() c4() -> c5() c5() -> b6() critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [c2] = 4, [b6] = 0, [b2] = 0, [c4] = 1, [c3] = 4, [b5] = 0, [b4] = 0, [c5] = 0, [b3] = 0 orientation: b2() = 0 >= 0 = b3() b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() c2() = 4 >= 4 = c3() c3() = 4 >= 1 = c4() c4() = 1 >= 0 = c5() c5() = 0 >= 0 = b6() problem: b2() -> b3() b3() -> b4() b4() -> b5() b5() -> b6() c2() -> c3() c5() -> b6() Matrix Interpretation Processor: dim=1 interpretation: [c2] = 0, [b6] = 0, [b2] = 0, [c3] = 0, [b5] = 0, [b4] = 0, [c5] = 1, [b3] = 0 orientation: b2() = 0 >= 0 = b3() b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() c2() = 0 >= 0 = c3() c5() = 1 >= 0 = b6() problem: b2() -> b3() b3() -> b4() b4() -> b5() b5() -> b6() c2() -> c3() Matrix Interpretation Processor: dim=1 interpretation: [c2] = 1, [b6] = 0, [b2] = 0, [c3] = 0, [b5] = 0, [b4] = 0, [b3] = 0 orientation: b2() = 0 >= 0 = b3() b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() c2() = 1 >= 0 = c3() problem: b2() -> b3() b3() -> b4() b4() -> b5() b5() -> b6() Matrix Interpretation Processor: dim=1 interpretation: [b6] = 0, [b2] = 4, [b5] = 0, [b4] = 4, [b3] = 4 orientation: b2() = 4 >= 4 = b3() b3() = 4 >= 4 = b4() b4() = 4 >= 0 = b5() b5() = 0 >= 0 = b6() problem: b2() -> b3() b3() -> b4() b5() -> b6() Matrix Interpretation Processor: dim=1 interpretation: [b6] = 0, [b2] = 0, [b5] = 1, [b4] = 0, [b3] = 0 orientation: b2() = 0 >= 0 = b3() b3() = 0 >= 0 = b4() b5() = 1 >= 0 = b6() problem: b2() -> b3() b3() -> b4() Matrix Interpretation Processor: dim=1 interpretation: [b2] = 4, [b4] = 0, [b3] = 4 orientation: b2() = 4 >= 4 = b3() b3() = 4 >= 0 = b4() problem: b2() -> b3() Matrix Interpretation Processor: dim=1 interpretation: [b2] = 1, [b3] = 0 orientation: b2() = 1 >= 0 = b3() problem: Qed 2:a3() -> b3() a3() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() Church Rosser Transformation Processor: b3() -> b4() b4() -> b5() b5() -> b6() c3() -> c4() c4() -> c5() c5() -> b6() critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [b6] = 0, [c4] = 4, [c3] = 4, [b5] = 0, [b4] = 0, [c5] = 0, [b3] = 0 orientation: b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() c3() = 4 >= 4 = c4() c4() = 4 >= 0 = c5() c5() = 0 >= 0 = b6() problem: b3() -> b4() b4() -> b5() b5() -> b6() c3() -> c4() c5() -> b6() Matrix Interpretation Processor: dim=1 interpretation: [b6] = 0, [c4] = 0, [c3] = 0, [b5] = 0, [b4] = 0, [c5] = 1, [b3] = 0 orientation: b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() c3() = 0 >= 0 = c4() c5() = 1 >= 0 = b6() problem: b3() -> b4() b4() -> b5() b5() -> b6() c3() -> c4() Matrix Interpretation Processor: dim=1 interpretation: [b6] = 0, [c4] = 0, [c3] = 1, [b5] = 0, [b4] = 0, [b3] = 0 orientation: b3() = 0 >= 0 = b4() b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() c3() = 1 >= 0 = c4() problem: b3() -> b4() b4() -> b5() b5() -> b6() Matrix Interpretation Processor: dim=1 interpretation: [b6] = 0, [b5] = 0, [b4] = 4, [b3] = 4 orientation: b3() = 4 >= 4 = b4() b4() = 4 >= 0 = b5() b5() = 0 >= 0 = b6() 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() -> b6() Church Rosser Transformation Processor (critical pair closing system, Thm 2.11): b4() -> b5() b5() -> b6() c4() -> c5() c5() -> b6() critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [b6] = 0, [c4] = 4, [b5] = 0, [b4] = 0, [c5] = 4 orientation: b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() c4() = 4 >= 4 = c5() c5() = 4 >= 0 = b6() problem: b4() -> b5() b5() -> b6() c4() -> c5() Matrix Interpretation Processor: dim=1 interpretation: [b6] = 0, [c4] = 1, [b5] = 0, [b4] = 0, [c5] = 0 orientation: b4() = 0 >= 0 = b5() b5() = 0 >= 0 = b6() c4() = 1 >= 0 = c5() 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() -> b6() Church Rosser Transformation Processor: critical peaks: joinable Qed