(ignored inputs)COMMENT doi:10.1016/j.jsc.2004.02.003 [116] p. 890 ( R_+ union R_int ) submitted by: Aart Middeldorp
Rewrite Rules:
   [ 0(sharp) -> sharp,
     +(?x,sharp) -> ?x,
     +(0(?x),0(?y)) -> 0(+(?x,?y)),
     +(0(?x),1(?y)) -> 1(+(?x,?y)),
     +(1(?x),1(?y)) -> j(+(?x,+(?y,1(sharp)))),
     +(0(?x),j(?y)) -> j(+(?x,?y)),
     +(j(?x),1(?y)) -> 0(+(?x,?y)),
     +(j(?x),j(?y)) -> 1(+(?x,+(?y,j(sharp)))),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [ +(sharp,0(?y_1)) = 0(+(sharp,?y_1)),
     +(0(?x_1),sharp) = 0(+(?x_1,sharp)),
     +(sharp,1(?y_2)) = 1(+(sharp,?y_2)),
     +(sharp,j(?y_4)) = j(+(sharp,?y_4)),
     +(?x_7,?x) = +(+(?x_7,?x),sharp),
     +(?x_7,0(+(?x_1,?y_1))) = +(+(?x_7,0(?x_1)),0(?y_1)),
     +(?x_7,1(+(?x_2,?y_2))) = +(+(?x_7,0(?x_2)),1(?y_2)),
     +(?x_7,j(+(?x_3,+(?y_3,1(sharp))))) = +(+(?x_7,1(?x_3)),1(?y_3)),
     +(?x_7,j(+(?x_4,?y_4))) = +(+(?x_7,0(?x_4)),j(?y_4)),
     +(?x_7,0(+(?x_5,?y_5))) = +(+(?x_7,j(?x_5)),1(?y_5)),
     +(?x_7,1(+(?x_6,+(?y_6,j(sharp))))) = +(+(?x_7,j(?x_6)),j(?y_6)),
     +(?x_7,+(?x_8,+(?y_8,?z_8))) = +(+(?x_7,+(?x_8,?y_8)),?z_8),
     +(?x_7,+(?y_9,?x_9)) = +(+(?x_7,?x_9),?y_9),
     +(?x,?z_8) = +(?x,+(sharp,?z_8)),
     +(0(+(?x_1,?y_1)),?z_8) = +(0(?x_1),+(0(?y_1),?z_8)),
     +(1(+(?x_2,?y_2)),?z_8) = +(0(?x_2),+(1(?y_2),?z_8)),
     +(j(+(?x_3,+(?y_3,1(sharp)))),?z_8) = +(1(?x_3),+(1(?y_3),?z_8)),
     +(j(+(?x_4,?y_4)),?z_8) = +(0(?x_4),+(j(?y_4),?z_8)),
     +(0(+(?x_5,?y_5)),?z_8) = +(j(?x_5),+(1(?y_5),?z_8)),
     +(1(+(?x_6,+(?y_6,j(sharp)))),?z_8) = +(j(?x_6),+(j(?y_6),?z_8)),
     +(+(+(?x_7,?y_7),?z_7),?z_8) = +(?x_7,+(+(?y_7,?z_7),?z_8)),
     +(+(?y_9,?x_9),?z_8) = +(?x_9,+(?y_9,?z_8)),
     +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
Outer CPs:
   [ +(?x_8,?y_8) = +(?x_8,+(?y_8,sharp)),
     ?x = +(sharp,?x),
     0(+(?x_1,?y_1)) = +(0(?y_1),0(?x_1)),
     1(+(?x_2,?y_2)) = +(1(?y_2),0(?x_2)),
     j(+(?x_3,+(?y_3,1(sharp)))) = +(1(?y_3),1(?x_3)),
     j(+(?x_4,?y_4)) = +(j(?y_4),0(?x_4)),
     0(+(?x_5,?y_5)) = +(1(?y_5),j(?x_5)),
     1(+(?x_6,+(?y_6,j(sharp)))) = +(j(?y_6),j(?x_6)),
     +(+(+(?x_8,?y_8),?y_7),?z_7) = +(?x_8,+(?y_8,+(?y_7,?z_7))),
     +(+(?x_7,?y_7),?z_7) = +(+(?y_7,?z_7),?x_7),
     +(?x_8,+(?y_8,?z_8)) = +(?z_8,+(?x_8,?y_8)) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ 0(+(sharp,?y_1)) = +(sharp,0(?y_1)),
     0(+(?x_1,sharp)) = +(0(?x_1),sharp),
     1(+(sharp,?y_2)) = +(sharp,1(?y_2)),
     j(+(sharp,?y_4)) = +(sharp,j(?y_4)),
     +(?x_8,+(?y_8,sharp)) = +(?x_8,?y_8),
     +(sharp,?x) = ?x,
     +(+(?x_8,?x),sharp) = +(?x_8,?x),
     +(?x,+(sharp,?z_9)) = +(?x,?z_9),
     +(sharp,sharp) = 0(+(sharp,sharp)),
     +(0(?y),sharp) = 0(+(sharp,?y)),
     +(sharp,0(?x)) = 0(+(?x,sharp)),
     +(0(?y),0(?x)) = 0(+(?x,?y)),
     +(sharp,0(?y)) = 0(+(sharp,?y)),
     +(0(?x),sharp) = 0(+(?x,sharp)),
     +(+(?x_8,sharp),sharp) = +(?x_8,0(+(sharp,sharp))),
     +(sharp,+(sharp,?z_9)) = +(0(+(sharp,sharp)),?z_9),
     +(+(?x_8,sharp),0(?y)) = +(?x_8,0(+(sharp,?y))),
     +(+(?x_8,0(?x)),sharp) = +(?x_8,0(+(?x,sharp))),
     +(sharp,+(0(?y),?z_9)) = +(0(+(sharp,?y)),?z_9),
     +(0(?x),+(sharp,?z_9)) = +(0(+(?x,sharp)),?z_9),
     +(+(?x_8,0(?x)),0(?y)) = +(?x_8,0(+(?x,?y))),
     +(0(?x),+(0(?y),?z_9)) = +(0(+(?x,?y)),?z_9),
     +(1(?y),sharp) = 1(+(sharp,?y)),
     +(1(?y),0(?x)) = 1(+(?x,?y)),
     +(sharp,1(?y)) = 1(+(sharp,?y)),
     +(+(?x_8,sharp),1(?y)) = +(?x_8,1(+(sharp,?y))),
     +(sharp,+(1(?y),?z_9)) = +(1(+(sharp,?y)),?z_9),
     +(+(?x_8,0(?x)),1(?y)) = +(?x_8,1(+(?x,?y))),
     +(0(?x),+(1(?y),?z_9)) = +(1(+(?x,?y)),?z_9),
     +(1(?y),1(?x)) = j(+(?x,+(?y,1(sharp)))),
     +(+(?x_8,1(?x)),1(?y)) = +(?x_8,j(+(?x,+(?y,1(sharp))))),
     +(1(?x),+(1(?y),?z_9)) = +(j(+(?x,+(?y,1(sharp)))),?z_9),
     +(j(?y),sharp) = j(+(sharp,?y)),
     +(j(?y),0(?x)) = j(+(?x,?y)),
     +(sharp,j(?y)) = j(+(sharp,?y)),
     +(+(?x_8,sharp),j(?y)) = +(?x_8,j(+(sharp,?y))),
     +(sharp,+(j(?y),?z_9)) = +(j(+(sharp,?y)),?z_9),
     +(+(?x_8,0(?x)),j(?y)) = +(?x_8,j(+(?x,?y))),
     +(0(?x),+(j(?y),?z_9)) = +(j(+(?x,?y)),?z_9),
     +(1(?y),j(?x)) = 0(+(?x,?y)),
     +(+(?x_8,j(?x)),1(?y)) = +(?x_8,0(+(?x,?y))),
     +(j(?x),+(1(?y),?z_9)) = +(0(+(?x,?y)),?z_9),
     +(j(?y),j(?x)) = 1(+(?x,+(?y,j(sharp)))),
     +(+(?x_8,j(?x)),j(?y)) = +(?x_8,1(+(?x,+(?y,j(sharp))))),
     +(j(?x),+(j(?y),?z_9)) = +(1(+(?x,+(?y,j(sharp)))),?z_9),
     +(?x_8,+(?y_8,+(+(?y,?y_9),?z_9))) = +(+(+(?x_8,?y_8),?y),+(?y_9,?z_9)),
     +(?x_8,+(?y_8,?y)) = +(+(+(?x_8,?y_8),?y),sharp),
     +(?x_8,+(?y_8,0(+(?x_11,?y_11)))) = +(+(+(?x_8,?y_8),0(?x_11)),0(?y_11)),
     +(?x_8,+(?y_8,1(+(?x_12,?y_12)))) = +(+(+(?x_8,?y_8),0(?x_12)),1(?y_12)),
     +(?x_8,+(?y_8,j(+(?x_13,+(?y_13,1(sharp)))))) = +(+(+(?x_8,?y_8),1(?x_13)),1(?y_13)),
     +(?x_8,+(?y_8,j(+(?x_14,?y_14)))) = +(+(+(?x_8,?y_8),0(?x_14)),j(?y_14)),
     +(?x_8,+(?y_8,0(+(?x_15,?y_15)))) = +(+(+(?x_8,?y_8),j(?x_15)),1(?y_15)),
     +(?x_8,+(?y_8,1(+(?x_16,+(?y_16,j(sharp)))))) = +(+(+(?x_8,?y_8),j(?x_16)),j(?y_16)),
     +(?x_8,+(?y_8,+(?x_17,+(?y_17,?z)))) = +(+(+(?x_8,?y_8),+(?x_17,?y_17)),?z),
     +(?x_8,+(?y_8,+(?z,?y))) = +(+(+(?x_8,?y_8),?y),?z),
     +(+(+(?y,?y_1),?z_1),?x) = +(+(?x,?y),+(?y_1,?z_1)),
     +(?y,?x) = +(+(?x,?y),sharp),
     +(0(+(?x_3,?y_3)),?x) = +(+(?x,0(?x_3)),0(?y_3)),
     +(1(+(?x_4,?y_4)),?x) = +(+(?x,0(?x_4)),1(?y_4)),
     +(j(+(?x_5,+(?y_5,1(sharp)))),?x) = +(+(?x,1(?x_5)),1(?y_5)),
     +(j(+(?x_6,?y_6)),?x) = +(+(?x,0(?x_6)),j(?y_6)),
     +(0(+(?x_7,?y_7)),?x) = +(+(?x,j(?x_7)),1(?y_7)),
     +(1(+(?x_8,+(?y_8,j(sharp)))),?x) = +(+(?x,j(?x_8)),j(?y_8)),
     +(+(?x_9,+(?y_9,?z)),?x) = +(+(?x,+(?x_9,?y_9)),?z),
     +(+(?z,?y),?x) = +(+(?x,?y),?z),
     +(?x_8,+(?y_8,+(?y,?z))) = +(+(+(?x_8,?y_8),?y),?z),
     +(+(?y,?z),?x) = +(+(?x,?y),?z),
     +(?x,+(+(?y,?y_1),?z_1)) = +(+(?x,?y),+(?y_1,?z_1)),
     +(?x,?y) = +(+(?x,?y),sharp),
     +(?x,0(+(?x_3,?y_3))) = +(+(?x,0(?x_3)),0(?y_3)),
     +(?x,1(+(?x_4,?y_4))) = +(+(?x,0(?x_4)),1(?y_4)),
     +(?x,j(+(?x_5,+(?y_5,1(sharp))))) = +(+(?x,1(?x_5)),1(?y_5)),
     +(?x,j(+(?x_6,?y_6))) = +(+(?x,0(?x_6)),j(?y_6)),
     +(?x,0(+(?x_7,?y_7))) = +(+(?x,j(?x_7)),1(?y_7)),
     +(?x,1(+(?x_8,+(?y_8,j(sharp))))) = +(+(?x,j(?x_8)),j(?y_8)),
     +(?x,+(?x_9,+(?y_9,?z))) = +(+(?x,+(?x_9,?y_9)),?z),
     +(?x,+(?z,?y)) = +(+(?x,?y),?z),
     +(+(?x_1,?x),+(+(?y,?y_2),?z_2)) = +(?x_1,+(+(?x,?y),+(?y_2,?z_2))),
     +(+(?x_1,?x),?y) = +(?x_1,+(+(?x,?y),sharp)),
     +(+(?x_1,?x),0(+(?x_4,?y_4))) = +(?x_1,+(+(?x,0(?x_4)),0(?y_4))),
     +(+(?x_1,?x),1(+(?x_5,?y_5))) = +(?x_1,+(+(?x,0(?x_5)),1(?y_5))),
     +(+(?x_1,?x),j(+(?x_6,+(?y_6,1(sharp))))) = +(?x_1,+(+(?x,1(?x_6)),1(?y_6))),
     +(+(?x_1,?x),j(+(?x_7,?y_7))) = +(?x_1,+(+(?x,0(?x_7)),j(?y_7))),
     +(+(?x_1,?x),0(+(?x_8,?y_8))) = +(?x_1,+(+(?x,j(?x_8)),1(?y_8))),
     +(+(?x_1,?x),1(+(?x_9,+(?y_9,j(sharp))))) = +(?x_1,+(+(?x,j(?x_9)),j(?y_9))),
     +(+(?x_1,?x),+(?x_10,+(?y_10,?z))) = +(?x_1,+(+(?x,+(?x_10,?y_10)),?z)),
     +(+(?x_1,?x),+(?z,?y)) = +(?x_1,+(+(?x,?y),?z)),
     +(?x,+(+(+(?y,?y_10),?z_10),?z_9)) = +(+(+(?x,?y),+(?y_10,?z_10)),?z_9),
     +(?x,+(?y,?z_9)) = +(+(+(?x,?y),sharp),?z_9),
     +(?x,+(0(+(?x_12,?y_12)),?z_9)) = +(+(+(?x,0(?x_12)),0(?y_12)),?z_9),
     +(?x,+(1(+(?x_13,?y_13)),?z_9)) = +(+(+(?x,0(?x_13)),1(?y_13)),?z_9),
     +(?x,+(j(+(?x_14,+(?y_14,1(sharp)))),?z_9)) = +(+(+(?x,1(?x_14)),1(?y_14)),?z_9),
     +(?x,+(j(+(?x_15,?y_15)),?z_9)) = +(+(+(?x,0(?x_15)),j(?y_15)),?z_9),
     +(?x,+(0(+(?x_16,?y_16)),?z_9)) = +(+(+(?x,j(?x_16)),1(?y_16)),?z_9),
     +(?x,+(1(+(?x_17,+(?y_17,j(sharp)))),?z_9)) = +(+(+(?x,j(?x_17)),j(?y_17)),?z_9),
     +(?x,+(+(?x_18,+(?y_18,?z)),?z_9)) = +(+(+(?x,+(?x_18,?y_18)),?z),?z_9),
     +(?x,+(+(?z,?y),?z_9)) = +(+(+(?x,?y),?z),?z_9),
     +(+(?x_1,?x),+(?y,?z)) = +(?x_1,+(+(?x,?y),?z)),
     +(?x,+(+(?y,?z),?z_9)) = +(+(+(?x,?y),?z),?z_9),
     +(?x_1,+(?y_1,?y)) = +(+(?x_1,?y_1),+(?y,sharp)),
     ?x = +(?x,+(sharp,sharp)),
     0(+(?x_3,?y_3)) = +(0(?x_3),+(0(?y_3),sharp)),
     1(+(?x_4,?y_4)) = +(0(?x_4),+(1(?y_4),sharp)),
     j(+(?x_5,+(?y_5,1(sharp)))) = +(1(?x_5),+(1(?y_5),sharp)),
     j(+(?x_6,?y_6)) = +(0(?x_6),+(j(?y_6),sharp)),
     0(+(?x_7,?y_7)) = +(j(?x_7),+(1(?y_7),sharp)),
     1(+(?x_8,+(?y_8,j(sharp)))) = +(j(?x_8),+(j(?y_8),sharp)),
     +(?y,?x) = +(?x,+(?y,sharp)),
     +(+(+(?x_9,+(?y_9,?y)),?y_8),?z_8) = +(+(?x_9,?y_9),+(?y,+(?y_8,?z_8))),
     +(+(?x,?y_8),?z_8) = +(?x,+(sharp,+(?y_8,?z_8))),
     +(+(0(+(?x_11,?y_11)),?y_8),?z_8) = +(0(?x_11),+(0(?y_11),+(?y_8,?z_8))),
     +(+(1(+(?x_12,?y_12)),?y_8),?z_8) = +(0(?x_12),+(1(?y_12),+(?y_8,?z_8))),
     +(+(j(+(?x_13,+(?y_13,1(sharp)))),?y_8),?z_8) = +(1(?x_13),+(1(?y_13),+(?y_8,?z_8))),
     +(+(j(+(?x_14,?y_14)),?y_8),?z_8) = +(0(?x_14),+(j(?y_14),+(?y_8,?z_8))),
     +(+(0(+(?x_15,?y_15)),?y_8),?z_8) = +(j(?x_15),+(1(?y_15),+(?y_8,?z_8))),
     +(+(1(+(?x_16,+(?y_16,j(sharp)))),?y_8),?z_8) = +(j(?x_16),+(j(?y_16),+(?y_8,?z_8))),
     +(+(+(+(?x,?y_17),?z_17),?y_8),?z_8) = +(?x,+(+(?y_17,?z_17),+(?y_8,?z_8))),
     +(+(+(?y,?x),?y_8),?z_8) = +(?x,+(?y,+(?y_8,?z_8))),
     +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?z,?x) = +(?x,+(sharp,?z)),
     +(?z,0(+(?x_3,?y_3))) = +(0(?x_3),+(0(?y_3),?z)),
     +(?z,1(+(?x_4,?y_4))) = +(0(?x_4),+(1(?y_4),?z)),
     +(?z,j(+(?x_5,+(?y_5,1(sharp))))) = +(1(?x_5),+(1(?y_5),?z)),
     +(?z,j(+(?x_6,?y_6))) = +(0(?x_6),+(j(?y_6),?z)),
     +(?z,0(+(?x_7,?y_7))) = +(j(?x_7),+(1(?y_7),?z)),
     +(?z,1(+(?x_8,+(?y_8,j(sharp))))) = +(j(?x_8),+(j(?y_8),?z)),
     +(?z,+(+(?x,?y_9),?z_9)) = +(?x,+(+(?y_9,?z_9),?z)),
     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?x,+(?y,sharp)),
     +(+(+(?x,?y),?y_8),?z_8) = +(?x,+(?y,+(?y_8,?z_8))),
     +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?x,?z) = +(?x,+(sharp,?z)),
     +(0(+(?x_3,?y_3)),?z) = +(0(?x_3),+(0(?y_3),?z)),
     +(1(+(?x_4,?y_4)),?z) = +(0(?x_4),+(1(?y_4),?z)),
     +(j(+(?x_5,+(?y_5,1(sharp)))),?z) = +(1(?x_5),+(1(?y_5),?z)),
     +(j(+(?x_6,?y_6)),?z) = +(0(?x_6),+(j(?y_6),?z)),
     +(0(+(?x_7,?y_7)),?z) = +(j(?x_7),+(1(?y_7),?z)),
     +(1(+(?x_8,+(?y_8,j(sharp)))),?z) = +(j(?x_8),+(j(?y_8),?z)),
     +(+(+(?x,?y_9),?z_9),?z) = +(?x,+(+(?y_9,?z_9),?z)),
     +(+(?y,?x),?z) = +(?x,+(?y,?z)),
     +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1),
     +(?x,+(?z,?z_1)) = +(+(?x,+(sharp,?z)),?z_1),
     +(0(+(?x_4,?y_4)),+(?z,?z_1)) = +(+(0(?x_4),+(0(?y_4),?z)),?z_1),
     +(1(+(?x_5,?y_5)),+(?z,?z_1)) = +(+(0(?x_5),+(1(?y_5),?z)),?z_1),
     +(j(+(?x_6,+(?y_6,1(sharp)))),+(?z,?z_1)) = +(+(1(?x_6),+(1(?y_6),?z)),?z_1),
     +(j(+(?x_7,?y_7)),+(?z,?z_1)) = +(+(0(?x_7),+(j(?y_7),?z)),?z_1),
     +(0(+(?x_8,?y_8)),+(?z,?z_1)) = +(+(j(?x_8),+(1(?y_8),?z)),?z_1),
     +(1(+(?x_9,+(?y_9,j(sharp)))),+(?z,?z_1)) = +(+(j(?x_9),+(j(?y_9),?z)),?z_1),
     +(+(+(?x,?y_10),?z_10),+(?z,?z_1)) = +(+(?x,+(+(?y_10,?z_10),?z)),?z_1),
     +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(+(?x_9,+(?x_10,+(?y_10,?y))),?z) = +(?x_9,+(+(?x_10,?y_10),+(?y,?z))),
     +(+(?x_9,?x),?z) = +(?x_9,+(?x,+(sharp,?z))),
     +(+(?x_9,0(+(?x_12,?y_12))),?z) = +(?x_9,+(0(?x_12),+(0(?y_12),?z))),
     +(+(?x_9,1(+(?x_13,?y_13))),?z) = +(?x_9,+(0(?x_13),+(1(?y_13),?z))),
     +(+(?x_9,j(+(?x_14,+(?y_14,1(sharp))))),?z) = +(?x_9,+(1(?x_14),+(1(?y_14),?z))),
     +(+(?x_9,j(+(?x_15,?y_15))),?z) = +(?x_9,+(0(?x_15),+(j(?y_15),?z))),
     +(+(?x_9,0(+(?x_16,?y_16))),?z) = +(?x_9,+(j(?x_16),+(1(?y_16),?z))),
     +(+(?x_9,1(+(?x_17,+(?y_17,j(sharp))))),?z) = +(?x_9,+(j(?x_17),+(j(?y_17),?z))),
     +(+(?x_9,+(+(?x,?y_18),?z_18)),?z) = +(?x_9,+(?x,+(+(?y_18,?z_18),?z))),
     +(+(?x_9,+(?y,?x)),?z) = +(?x_9,+(?x,+(?y,?z))),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(+(?x_9,+(?x,?y)),?z) = +(?x_9,+(?x,+(?y,?z))),
     ?x = +(sharp,?x),
     0(+(?x_2,?y_2)) = +(0(?y_2),0(?x_2)),
     1(+(?x_3,?y_3)) = +(1(?y_3),0(?x_3)),
     j(+(?x_4,+(?y_4,1(sharp)))) = +(1(?y_4),1(?x_4)),
     j(+(?x_5,?y_5)) = +(j(?y_5),0(?x_5)),
     0(+(?x_6,?y_6)) = +(1(?y_6),j(?x_6)),
     1(+(?x_7,+(?y_7,j(sharp)))) = +(j(?y_7),j(?x_7)),
     +(+(?x,?y_8),?z_8) = +(+(?y_8,?z_8),?x),
     +(?x_9,+(?y_9,?y)) = +(?y,+(?x_9,?y_9)),
     +(+(?x_9,?x),?y) = +(?x_9,+(?y,?x)),
     +(?x,+(?y,?z_10)) = +(+(?y,?x),?z_10) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <+(sharp,0(?y_1)), 0(+(sharp,?y_1))> by Rules <0, 2> preceded by [(+,1)]
 joinable by a reduction of rules <[([],10),([],1)], [([(0,1)],10),([(0,1)],1)]>
Critical Pair <+(0(?x_1),sharp), 0(+(?x_1,sharp))> by Rules <0, 2> preceded by [(+,2)]
 joinable by a reduction of rules <[([],1)], [([(0,1)],1)]>
Critical Pair <+(sharp,1(?y_2)), 1(+(sharp,?y_2))> by Rules <0, 3> preceded by [(+,1)]
 joinable by a reduction of rules <[([],10),([],1)], [([(1,1)],10),([(1,1)],1)]>
Critical Pair <+(sharp,j(?y_4)), j(+(sharp,?y_4))> by Rules <0, 5> preceded by [(+,1)]
 joinable by a reduction of rules <[([],10),([],1)], [([(j,1)],10),([(j,1)],1)]>
Critical Pair <+(?x_7,?x), +(+(?x_7,?x),sharp)> by Rules <1, 8> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([],1)]>
Critical Pair <+(?x_7,0(+(?x_1,?y_1))), +(+(?x_7,0(?x_1)),0(?y_1))> by Rules <2, 8> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([],9),([(+,2)],2)]>
Critical Pair <+(?x_7,1(+(?x_2,?y_2))), +(+(?x_7,0(?x_2)),1(?y_2))> by Rules <3, 8> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([],9),([(+,2)],3)]>
Critical Pair <+(?x_7,j(+(?x_3,+(?y_3,1(sharp))))), +(+(?x_7,1(?x_3)),1(?y_3))> by Rules <4, 8> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([],9),([(+,2)],4)]>
Critical Pair <+(?x_7,j(+(?x_4,?y_4))), +(+(?x_7,0(?x_4)),j(?y_4))> by Rules <5, 8> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([],9),([(+,2)],5)]>
Critical Pair <+(?x_7,0(+(?x_5,?y_5))), +(+(?x_7,j(?x_5)),1(?y_5))> by Rules <6, 8> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([],9),([(+,2)],6)]>
Critical Pair <+(?x_7,1(+(?x_6,+(?y_6,j(sharp))))), +(+(?x_7,j(?x_6)),j(?y_6))> by Rules <7, 8> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([],9),([(+,2)],7)]>
Critical Pair <+(?x_7,+(?x_8,+(?y_8,?z_8))), +(+(?x_7,+(?x_8,?y_8)),?z_8)> by Rules <9, 8> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],8)], [([],9)]>
Critical Pair <+(?x_7,+(?y_9,?x_9)), +(+(?x_7,?x_9),?y_9)> by Rules <10, 8> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],10)], [([],9)]>
Critical Pair <+(?x,?z_8), +(?x,+(sharp,?z_8))> by Rules <1, 9> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([(+,2)],10),([(+,2)],1)]>
 joinable by a reduction of rules <[], [([],8),([(+,1)],1)]>
Critical Pair <+(0(+(?x_1,?y_1)),?z_8), +(0(?x_1),+(0(?y_1),?z_8))> by Rules <2, 9> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],8),([(+,1)],2)]>
Critical Pair <+(1(+(?x_2,?y_2)),?z_8), +(0(?x_2),+(1(?y_2),?z_8))> by Rules <3, 9> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],8),([(+,1)],3)]>
Critical Pair <+(j(+(?x_3,+(?y_3,1(sharp)))),?z_8), +(1(?x_3),+(1(?y_3),?z_8))> by Rules <4, 9> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],8),([(+,1)],4)]>
Critical Pair <+(j(+(?x_4,?y_4)),?z_8), +(0(?x_4),+(j(?y_4),?z_8))> by Rules <5, 9> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],8),([(+,1)],5)]>
Critical Pair <+(0(+(?x_5,?y_5)),?z_8), +(j(?x_5),+(1(?y_5),?z_8))> by Rules <6, 9> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],8),([(+,1)],6)]>
Critical Pair <+(1(+(?x_6,+(?y_6,j(sharp)))),?z_8), +(j(?x_6),+(j(?y_6),?z_8))> by Rules <7, 9> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],8),([(+,1)],7)]>
Critical Pair <+(+(+(?x_7,?y_7),?z_7),?z_8), +(?x_7,+(+(?y_7,?z_7),?z_8))> by Rules <8, 9> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],9)], [([],8)]>
Critical Pair <+(+(?y_9,?x_9),?z_8), +(?x_9,+(?y_9,?z_8))> by Rules <10, 9> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],10)], [([],8)]>
Critical Pair <+(?x_1,+(+(?x,?y),?z)), +(+(?x_1,?x),+(?y,?z))> by Rules <8, 8> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],9)], [([],9)]>
Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <9, 9> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],8)], [([],8)]>
Critical Pair <+(?x_8,+(?y_8,sharp)), +(?x_8,?y_8)> by Rules <9, 1> preceded by []
 joinable by a reduction of rules <[([(+,2)],1)], []>
Critical Pair <+(sharp,?x_9), ?x_9> by Rules <10, 1> preceded by []
 joinable by a reduction of rules <[([],10),([],1)], []>
Critical Pair <+(0(?y_1),0(?x_1)), 0(+(?x_1,?y_1))> by Rules <10, 2> preceded by []
 joinable by a reduction of rules <[([],2)], [([(0,1)],10)]>
Critical Pair <+(1(?y_2),0(?x_2)), 1(+(?x_2,?y_2))> by Rules <10, 3> preceded by []
 joinable by a reduction of rules <[([],10),([],3)], []>
Critical Pair <+(1(?y_3),1(?x_3)), j(+(?x_3,+(?y_3,1(sharp))))> by Rules <10, 4> preceded by []
 joinable by a reduction of rules <[([],10),([],4)], []>
 joinable by a reduction of rules <[([],4),([(j,1),(+,2)],10)], [([(j,1)],10),([(j,1)],9)]>
 joinable by a reduction of rules <[([],4),([(j,1)],10)], [([(j,1),(+,2)],10),([(j,1)],8)]>
 joinable by a reduction of rules <[([],4),([(j,1)],8)], [([(j,1)],8),([(j,1),(+,1)],10)]>
Critical Pair <+(j(?y_4),0(?x_4)), j(+(?x_4,?y_4))> by Rules <10, 5> preceded by []
 joinable by a reduction of rules <[([],10),([],5)], []>
Critical Pair <+(1(?y_5),j(?x_5)), 0(+(?x_5,?y_5))> by Rules <10, 6> preceded by []
 joinable by a reduction of rules <[([],10),([],6)], []>
Critical Pair <+(j(?y_6),j(?x_6)), 1(+(?x_6,+(?y_6,j(sharp))))> by Rules <10, 7> preceded by []
 joinable by a reduction of rules <[([],10),([],7)], []>
 joinable by a reduction of rules <[([],7),([(1,1),(+,2)],10)], [([(1,1)],10),([(1,1)],9)]>
 joinable by a reduction of rules <[([],7),([(1,1)],10)], [([(1,1),(+,2)],10),([(1,1)],8)]>
 joinable by a reduction of rules <[([],7),([(1,1)],8)], [([(1,1)],8),([(1,1),(+,1)],10)]>
Critical Pair <+(?x_8,+(?y_8,+(?y_7,?z_7))), +(+(+(?x_8,?y_8),?y_7),?z_7)> by Rules <9, 8> preceded by []
 joinable by a reduction of rules <[([],8)], [([],9)]>
Critical Pair <+(+(?y_7,?z_7),?x_9), +(+(?x_9,?y_7),?z_7)> by Rules <10, 8> preceded by []
 joinable by a reduction of rules <[([],10)], [([],9)]>
Critical Pair <+(?y_9,+(?x_8,?y_8)), +(?x_8,+(?y_8,?y_9))> by Rules <10, 9> preceded by []
 joinable by a reduction of rules <[([],10)], [([],8)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 14 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
unknown Non-Confluence
Check relative termination:
   [ 0(sharp) -> sharp,
     +(?x,sharp) -> ?x,
     +(0(?x),0(?y)) -> 0(+(?x,?y)),
     +(0(?x),1(?y)) -> 1(+(?x,?y)),
     +(1(?x),1(?y)) -> j(+(?x,+(?y,1(sharp)))),
     +(0(?x),j(?y)) -> j(+(?x,?y)),
     +(j(?x),1(?y)) -> 0(+(?x,?y)),
     +(j(?x),j(?y)) -> 1(+(?x,+(?y,j(sharp)))) ]
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]