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) 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 [1>2, 1>3, 2>6, 3>5, 4>5, 4>6, 5>8, 6>9, 7>8, 7>9, 8>11, 9>12, 10>11, 10>12, 11>14, 12>13, 13>16, 14>16, 15>16] sort attachment (non-strict) a1 : 1 b1 : 2 c1 : 3 b2 : 6 c2 : 5 a2 : 4 b3 : 9 c3 : 8 a3 : 7 b4 : 12 c4 : 11 a4 : 10 b5 : 13 c5 : 14 a5 : 15 b6 : 16 ----- 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 (kb): a1() -> b1() a1() -> c1() b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() critical peaks: joinable Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [0] [c5] = [0] [0], [0] [b5] = [0] [0], [0] [c4] = [0] [0], [0] [b4] = [0] [0], [0] [c3] = [0] [0], [0] [b3] = [0] [0], [0] [c2] = [0] [0], [0] [b2] = [0] [0], [0] [c1] = [0] [0], [0] [b1] = [0] [0], [1] [a1] = [0] [0] orientation: [1] [0] a1() = [0] >= [0] = b1() [0] [0] [1] [0] a1() = [0] >= [0] = c1() [0] [0] [0] [0] b1() = [0] >= [0] = b2() [0] [0] [0] [0] c1() = [0] >= [0] = c2() [0] [0] [0] [0] b2() = [0] >= [0] = b3() [0] [0] [0] [0] c2() = [0] >= [0] = c3() [0] [0] [0] [0] b3() = [0] >= [0] = b4() [0] [0] [0] [0] c3() = [0] >= [0] = c4() [0] [0] [0] [0] b4() = [0] >= [0] = b5() [0] [0] [0] [0] c4() = [0] >= [0] = c5() [0] [0] [0] [0] b5() = [0] >= [0] = b6() [0] [0] [0] [0] c5() = [0] >= [0] = b6() [0] [0] problem: b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [0] [c5] = [0] [0], [0] [b5] = [0] [0], [0] [c4] = [0] [0], [0] [b4] = [0] [0], [0] [c3] = [0] [0], [0] [b3] = [0] [0], [0] [c2] = [0] [0], [0] [b2] = [0] [0], [1] [c1] = [0] [0], [1] [b1] = [0] [0] orientation: [1] [0] b1() = [0] >= [0] = b2() [0] [0] [1] [0] c1() = [0] >= [0] = c2() [0] [0] [0] [0] b2() = [0] >= [0] = b3() [0] [0] [0] [0] c2() = [0] >= [0] = c3() [0] [0] [0] [0] b3() = [0] >= [0] = b4() [0] [0] [0] [0] c3() = [0] >= [0] = c4() [0] [0] [0] [0] b4() = [0] >= [0] = b5() [0] [0] [0] [0] c4() = [0] >= [0] = c5() [0] [0] [0] [0] b5() = [0] >= [0] = b6() [0] [0] [0] [0] c5() = [0] >= [0] = b6() [0] [0] problem: b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [0] [c5] = [0] [0], [0] [b5] = [0] [0], [0] [c4] = [0] [0], [0] [b4] = [0] [0], [0] [c3] = [0] [0], [0] [b3] = [0] [0], [1] [c2] = [0] [0], [1] [b2] = [0] [0] orientation: [1] [0] b2() = [0] >= [0] = b3() [0] [0] [1] [0] c2() = [0] >= [0] = c3() [0] [0] [0] [0] b3() = [0] >= [0] = b4() [0] [0] [0] [0] c3() = [0] >= [0] = c4() [0] [0] [0] [0] b4() = [0] >= [0] = b5() [0] [0] [0] [0] c4() = [0] >= [0] = c5() [0] [0] [0] [0] b5() = [0] >= [0] = b6() [0] [0] [0] [0] c5() = [0] >= [0] = b6() [0] [0] problem: b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [0] [c5] = [0] [0], [0] [b5] = [0] [0], [0] [c4] = [0] [0], [0] [b4] = [0] [0], [1] [c3] = [0] [0], [1] [b3] = [0] [0] orientation: [1] [0] b3() = [0] >= [0] = b4() [0] [0] [1] [0] c3() = [0] >= [0] = c4() [0] [0] [0] [0] b4() = [0] >= [0] = b5() [0] [0] [0] [0] c4() = [0] >= [0] = c5() [0] [0] [0] [0] b5() = [0] >= [0] = b6() [0] [0] [0] [0] c5() = [0] >= [0] = b6() [0] [0] problem: b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [0] [c5] = [0] [0], [0] [b5] = [0] [0], [1] [c4] = [0] [0], [1] [b4] = [0] [0] orientation: [1] [0] b4() = [0] >= [0] = b5() [0] [0] [1] [0] c4() = [0] >= [0] = c5() [0] [0] [0] [0] b5() = [0] >= [0] = b6() [0] [0] [0] [0] c5() = [0] >= [0] = b6() [0] [0] problem: b5() -> b6() c5() -> b6() Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [1] [c5] = [0] [0], [1] [b5] = [0] [0] orientation: [1] [0] b5() = [0] >= [0] = b6() [0] [0] [1] [0] c5() = [0] >= [0] = b6() [0] [0] 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 (kb): a2() -> b2() a2() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() critical peaks: joinable Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [0] [c5] = [0] [0], [0] [b5] = [0] [0], [0] [c4] = [0] [0], [0] [b4] = [0] [0], [0] [c3] = [0] [0], [0] [b3] = [0] [0], [1] [a2] = [0] [0], [0] [c2] = [0] [0], [0] [b2] = [0] [0] orientation: [1] [0] a2() = [0] >= [0] = b2() [0] [0] [1] [0] a2() = [0] >= [0] = c2() [0] [0] [0] [0] b2() = [0] >= [0] = b3() [0] [0] [0] [0] c2() = [0] >= [0] = c3() [0] [0] [0] [0] b3() = [0] >= [0] = b4() [0] [0] [0] [0] c3() = [0] >= [0] = c4() [0] [0] [0] [0] b4() = [0] >= [0] = b5() [0] [0] [0] [0] c4() = [0] >= [0] = c5() [0] [0] [0] [0] b5() = [0] >= [0] = b6() [0] [0] [0] [0] c5() = [0] >= [0] = b6() [0] [0] problem: b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [0] [c5] = [0] [0], [0] [b5] = [0] [0], [0] [c4] = [0] [0], [0] [b4] = [0] [0], [0] [c3] = [0] [0], [0] [b3] = [0] [0], [1] [c2] = [0] [0], [1] [b2] = [0] [0] orientation: [1] [0] b2() = [0] >= [0] = b3() [0] [0] [1] [0] c2() = [0] >= [0] = c3() [0] [0] [0] [0] b3() = [0] >= [0] = b4() [0] [0] [0] [0] c3() = [0] >= [0] = c4() [0] [0] [0] [0] b4() = [0] >= [0] = b5() [0] [0] [0] [0] c4() = [0] >= [0] = c5() [0] [0] [0] [0] b5() = [0] >= [0] = b6() [0] [0] [0] [0] c5() = [0] >= [0] = b6() [0] [0] problem: b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [0] [c5] = [0] [0], [0] [b5] = [0] [0], [0] [c4] = [0] [0], [0] [b4] = [0] [0], [1] [c3] = [0] [0], [1] [b3] = [0] [0] orientation: [1] [0] b3() = [0] >= [0] = b4() [0] [0] [1] [0] c3() = [0] >= [0] = c4() [0] [0] [0] [0] b4() = [0] >= [0] = b5() [0] [0] [0] [0] c4() = [0] >= [0] = c5() [0] [0] [0] [0] b5() = [0] >= [0] = b6() [0] [0] [0] [0] c5() = [0] >= [0] = b6() [0] [0] problem: b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [0] [c5] = [0] [0], [0] [b5] = [0] [0], [1] [c4] = [0] [0], [1] [b4] = [0] [0] orientation: [1] [0] b4() = [0] >= [0] = b5() [0] [0] [1] [0] c4() = [0] >= [0] = c5() [0] [0] [0] [0] b5() = [0] >= [0] = b6() [0] [0] [0] [0] c5() = [0] >= [0] = b6() [0] [0] problem: b5() -> b6() c5() -> b6() Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [1] [c5] = [0] [0], [1] [b5] = [0] [0] orientation: [1] [0] b5() = [0] >= [0] = b6() [0] [0] [1] [0] c5() = [0] >= [0] = b6() [0] [0] problem: Qed 2:a3() -> b3() a3() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() Church Rosser Transformation Processor (kb): a3() -> b3() a3() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() critical peaks: joinable Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [0] [c5] = [0] [0], [0] [b5] = [0] [0], [0] [c4] = [0] [0], [0] [b4] = [0] [0], [1] [a3] = [0] [0], [0] [c3] = [0] [0], [0] [b3] = [0] [0] orientation: [1] [0] a3() = [0] >= [0] = b3() [0] [0] [1] [0] a3() = [0] >= [0] = c3() [0] [0] [0] [0] b3() = [0] >= [0] = b4() [0] [0] [0] [0] c3() = [0] >= [0] = c4() [0] [0] [0] [0] b4() = [0] >= [0] = b5() [0] [0] [0] [0] c4() = [0] >= [0] = c5() [0] [0] [0] [0] b5() = [0] >= [0] = b6() [0] [0] [0] [0] c5() = [0] >= [0] = b6() [0] [0] problem: b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [0] [c5] = [0] [0], [0] [b5] = [0] [0], [0] [c4] = [0] [0], [0] [b4] = [0] [0], [1] [c3] = [0] [0], [1] [b3] = [0] [0] orientation: [1] [0] b3() = [0] >= [0] = b4() [0] [0] [1] [0] c3() = [0] >= [0] = c4() [0] [0] [0] [0] b4() = [0] >= [0] = b5() [0] [0] [0] [0] c4() = [0] >= [0] = c5() [0] [0] [0] [0] b5() = [0] >= [0] = b6() [0] [0] [0] [0] c5() = [0] >= [0] = b6() [0] [0] problem: b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [0] [c5] = [0] [0], [0] [b5] = [0] [0], [1] [c4] = [0] [0], [1] [b4] = [0] [0] orientation: [1] [0] b4() = [0] >= [0] = b5() [0] [0] [1] [0] c4() = [0] >= [0] = c5() [0] [0] [0] [0] b5() = [0] >= [0] = b6() [0] [0] [0] [0] c5() = [0] >= [0] = b6() [0] [0] problem: b5() -> b6() c5() -> b6() Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [1] [c5] = [0] [0], [1] [b5] = [0] [0] orientation: [1] [0] b5() = [0] >= [0] = b6() [0] [0] [1] [0] c5() = [0] >= [0] = b6() [0] [0] problem: Qed 3:a4() -> b4() a4() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() Church Rosser Transformation Processor (kb): a4() -> b4() a4() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() critical peaks: joinable Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [0] [c5] = [0] [0], [0] [b5] = [0] [0], [1] [a4] = [0] [0], [0] [c4] = [0] [0], [0] [b4] = [0] [0] orientation: [1] [0] a4() = [0] >= [0] = b4() [0] [0] [1] [0] a4() = [0] >= [0] = c4() [0] [0] [0] [0] b4() = [0] >= [0] = b5() [0] [0] [0] [0] c4() = [0] >= [0] = c5() [0] [0] [0] [0] b5() = [0] >= [0] = b6() [0] [0] [0] [0] c5() = [0] >= [0] = b6() [0] [0] problem: b4() -> b5() c4() -> c5() b5() -> b6() c5() -> b6() Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [0] [c5] = [0] [0], [0] [b5] = [0] [0], [1] [c4] = [0] [0], [1] [b4] = [0] [0] orientation: [1] [0] b4() = [0] >= [0] = b5() [0] [0] [1] [0] c4() = [0] >= [0] = c5() [0] [0] [0] [0] b5() = [0] >= [0] = b6() [0] [0] [0] [0] c5() = [0] >= [0] = b6() [0] [0] problem: b5() -> b6() c5() -> b6() Matrix Interpretation Processor: dim=3 interpretation: [0] [b6] = [0] [0], [1] [c5] = [0] [0], [1] [b5] = [0] [0] orientation: [1] [0] b5() = [0] >= [0] = b6() [0] [0] [1] [0] c5() = [0] >= [0] = b6() [0] [0] problem: Qed 4:a5() -> b6() Church Rosser Transformation Processor: strict: weak: critical peaks: 0 Qed