| Back: | ⟨a, b | aaaabaababa=1⟩ |
|---|
Completion settings:
Axiom: aaaabaababa=1.
Referenced by [3].
Axiom: aba=c.
Referenced by [3], [4], [5], [6], [13], [14], [22].
Overlap of [1] aaaabaababa=1 with [2] aba=c:
Critical pair: aaacababa=1.
Reduce LHS:
| [2] | aaac(aba)ba |
| ⇒ aaaccba |
Referenced by [5], [6], [7], [9], [10], [12].
Overlap of [2] aba=c with [2] aba=c:
Critical pair: abc=cba.
Referenced by [15].
Overlap of [2] aba=c with [3] aaaccba=1:
Critical pair: ab=caaccba.
Flip LHS and RHS.
Referenced by [8].
Overlap of [3] aaaccba=1 with [2] aba=c:
Critical pair: aaaccbc=ba.
Referenced by [10], [13], [19].
Overlap of [3] aaaccba=1 with [3] aaaccba=1:
Critical pair: aaaccb=aaccba.
Flip LHS and RHS.
Simplify [5] caaccba=ab.
Reduce LHS:
| [7] | c(aaccba) |
| ⇒ caaaccb |
Overlap of [7] aaccba=aaaccb with [7] aaccba=aaaccb:
Critical pair: aaccbaaaccb=aaaccbaccba.
Reduce LHS:
| [7] | (aaccba)aaccb |
| [3] | ⇒ (aaaccba)accb |
| ⇒ accb |
Reduce RHS:
| [3] | (aaaccba)ccba |
| ⇒ ccba |
Flip LHS and RHS.
Referenced by [10], [17], [18].
Overlap of [6] aaaccbc=ba with [9] ccba=accb:
Critical pair: aaaccbaccb=bacba.
Reduce LHS:
| [3] | (aaaccba)ccb |
| ⇒ ccb |
Flip LHS and RHS.
Referenced by [11].
Overlap of [10] bacba=ccb with [10] bacba=ccb:
Critical pair: bacccb=ccbcba.
Flip LHS and RHS.
Overlap of [3] aaaccba=1 with [7] aaccba=aaaccb:
Critical pair: aaaaccb=1.
Referenced by [14], [16], [17], [21].
Overlap of [6] aaaccbc=ba with [11] ccbcba=bacccb:
Critical pair: aaabacccb=baba.
Reduce LHS:
| [2] | aa(aba)cccb |
| ⇒ aaccccb |
Reduce RHS:
| [2] | b(aba) |
| ⇒ bc |
Flip LHS and RHS.
Defines rule #6.
Overlap of [12] aaaaccb=1 with [11] ccbcba=bacccb:
Critical pair: aaaabacccb=cba.
Reduce LHS:
| [2] | aaa(aba)cccb |
| ⇒ aaaccccb |
Flip LHS and RHS.
Overlap of [8] caaaccb=ab with [13] bc=aaccccb:
Critical pair: caaaccaaccccb=abc.
Reduce RHS:
| [4] | (abc) |
| [14] | ⇒ (cba) |
| ⇒ aaaccccb |
Overlap of [12] aaaaccb=1 with [14] cba=aaaccccb:
Critical pair: aaaacaaaccccb=a.
Referenced by [17].
Overlap of [9] ccba=accb with [16] aaaacaaaccccb=a:
Critical pair: ccba=accbaaacaaaccccb.
Reduce LHS:
| [9] | (ccba) |
| ⇒ accb |
Reduce RHS:
| [9] | a(ccba)aacaaaccccb |
| [9] | ⇒ aa(ccba)acaaaccccb |
| [9] | ⇒ aaa(ccba)caaaccccb |
| [12] | ⇒ (aaaaccb)caaaccccb |
| ⇒ caaaccccb |
Flip LHS and RHS.
Referenced by [18], [20], [21].
Overlap of [17] caaaccccb=accb with [9] ccba=accb:
Critical pair: caaaccaccb=accba.
Reduce RHS:
| [9] | a(ccba) |
| ⇒ aaccb |
Referenced by [20].
Overlap of [6] aaaccbc=ba with [13] bc=aaccccb:
Critical pair: aaaccaaccccb=ba.
Flip LHS and RHS.
Defines rule #5.
Overlap of [18] caaaccaccb=aaccb with [19] ba=aaaccaaccccb:
Critical pair: caaaccaccaaaccaaccccb=aaccba.
Reduce LHS:
| [15] | caaaccac(caaaccaaccccb) |
| [17] | ⇒ caaacca(caaaccccb) |
| ⇒ caaaccaaccb |
Reduce RHS:
| [19] | aacc(ba) |
| [15] | ⇒ aac(caaaccaaccccb) |
| [17] | ⇒ aa(caaaccccb) |
| ⇒ aaaccb |
Referenced by [21].
Overlap of [20] caaaccaaccb=aaaccb with [19] ba=aaaccaaccccb:
Critical pair: caaaccaaccaaaccaaccccb=aaaccba.
Reduce LHS:
| [15] | caaaccaac(caaaccaaccccb) |
| [17] | ⇒ caaaccaa(caaaccccb) |
| [8] | ⇒ caaac(caaaccb) |
| ⇒ caaacab |
Reduce RHS:
| [19] | aaacc(ba) |
| [15] | ⇒ aaac(caaaccaaccccb) |
| [17] | ⇒ aaa(caaaccccb) |
| [12] | ⇒ (aaaaccb) |
| ⇒ 1 |
Defines rule #4.
Overlap of [21] caaacab=1 with [2] aba=c:
Critical pair: caaacc=a.
Defines rule #2.
Overlap of [22] caaacc=a with [21] caaacab=1:
Critical pair: caaac=aaaacab.
Flip LHS and RHS.
Defines rule #3.
Overlap of [22] caaacc=a with [22] caaacc=a:
Critical pair: caaaca=aaaacc.
Flip LHS and RHS.
Defines rule #1.