| Back: | ⟨a, b | aaaababaaa=a⟩ |
|---|
Completion settings:
Axiom: aaaababaaa=a.
Referenced by [3].
Axiom: aba=c.
Defines rule #1.
Referenced by [3], [4], [5], [6], [10], [16], [17], [21], [27].
Overlap of [1] aaaababaaa=a with [2] aba=c:
Critical pair: aaacbaaa=a.
Referenced by [5], [6], [7], [8], [12], [14], [18].
Overlap of [2] aba=c with [2] aba=c:
Critical pair: abc=cba.
Defines rule #2.
Overlap of [2] aba=c with [3] aaacbaaa=a:
Critical pair: aba=caacbaaa.
Reduce LHS:
| [2] | (aba) |
| ⇒ c |
Flip LHS and RHS.
Referenced by [9].
Overlap of [3] aaacbaaa=a with [2] aba=c:
Critical pair: aaacbaac=aba.
Reduce RHS:
| [2] | (aba) |
| ⇒ c |
Referenced by [11].
Overlap of [3] aaacbaaa=a with [3] aaacbaaa=a:
Critical pair: aaacba=acbaaa.
Flip LHS and RHS.
Referenced by [8], [9], [13], [14], [15].
Overlap of [3] aaacbaaa=a with [3] aaacbaaa=a:
Critical pair: aaacbaa=aacbaaa.
Reduce RHS:
| [7] | a(acbaaa) |
| ⇒ aaaacba |
Referenced by [11], [13], [14], [15], [18].
Simplify [5] caacbaaa=c.
Reduce LHS:
| [7] | ca(acbaaa) |
| ⇒ caaaacba |
Referenced by [10].
Overlap of [9] caaaacba=c with [2] aba=c:
Critical pair: caaaacbc=cba.
Referenced by [26].
Simplify [6] aaacbaac=c.
Reduce LHS:
| [8] | (aaacbaa)c |
| ⇒ aaaacbac |
Referenced by [12], [13], [14], [15], [19].
Overlap of [3] aaacbaaa=a with [11] aaaacbac=c:
Critical pair: aaacbc=aacbac.
Flip LHS and RHS.
Referenced by [19].
Overlap of [11] aaaacbac=c with [7] acbaaa=aaacba:
Critical pair: aaaacbaaacba=cbaaa.
Reduce LHS:
| [8] | a(aaacbaa)acba |
| [8] | ⇒ aa(aaacbaa)cba |
| [11] | ⇒ aa(aaaacbac)ba |
| ⇒ aacba |
Flip LHS and RHS.
Overlap of [7] acbaaa=aaacba with [3] aaacbaaa=a:
Critical pair: acbaa=aaacbaacbaaa.
Reduce RHS:
| [8] | (aaacbaa)cbaaa |
| [11] | ⇒ (aaaacbac)baaa |
| [13] | ⇒ (cbaaa) |
| ⇒ aacba |
Overlap of [7] acbaaa=aaacba with [11] aaaacbac=c:
Critical pair: acbc=aaacbaacbac.
Reduce RHS:
| [8] | (aaacbaa)cbac |
| [11] | ⇒ (aaaacbac)bac |
| ⇒ cbac |
Flip LHS and RHS.
Defines rule #5.
Overlap of [4] abc=cba with [15] cbac=acbc:
Critical pair: abacbc=cbabac.
Reduce LHS:
| [2] | (aba)cbc |
| ⇒ ccbc |
Reduce RHS:
| [2] | cb(aba)c |
| ⇒ cbcc |
Flip LHS and RHS.
Defines rule #6.
Overlap of [2] aba=c with [14] acbaa=aacba:
Critical pair: abaacba=ccbaa.
Reduce LHS:
| [2] | (aba)acba |
| ⇒ cacba |
Flip LHS and RHS.
Referenced by [23].
Overlap of [3] aaacbaaa=a with [8] aaacbaa=aaaacba:
Critical pair: aaaacbaa=a.
Reduce LHS:
| [8] | a(aaacbaa) |
| ⇒ aaaaacba |
Overlap of [11] aaaacbac=c with [12] aacbac=aaacbc:
Critical pair: aaaaacbc=c.
Referenced by [22].
Overlap of [13] cbaaa=aacba with [18] aaaaacba=a:
Critical pair: cbaa=aacbaaaacba.
Reduce RHS:
| [14] | a(acbaa)aacba |
| [14] | ⇒ aa(acbaa)acba |
| [14] | ⇒ aaa(acbaa)cba |
| [18] | ⇒ (aaaaacba)cba |
| ⇒ acba |
Defines rule #3.
Referenced by [21], [24], [25], [27].
Overlap of [4] abc=cba with [20] cbaa=acba:
Critical pair: abacba=cbabaa.
Reduce LHS:
| [2] | (aba)cba |
| ⇒ ccba |
Reduce RHS:
| [2] | cb(aba)a |
| ⇒ cbca |
Flip LHS and RHS.
Defines rule #4.
Referenced by [22].
Overlap of [19] aaaaacbc=c with [21] cbca=ccba:
Critical pair: aaaaaccba=ca.
Referenced by [23].
Overlap of [22] aaaaaccba=ca with [17] ccbaa=cacba:
Critical pair: aaaaacacba=caa.
Referenced by [24].
Overlap of [23] aaaaacacba=caa with [20] cbaa=acba:
Critical pair: aaaaacaacba=caaa.
Referenced by [25].
Overlap of [24] aaaaacaacba=caaa with [20] cbaa=acba:
Critical pair: aaaaacaaacba=caaaa.
Overlap of [25] aaaaacaaacba=caaaa with [15] cbac=acbc:
Critical pair: aaaaacaaaacbc=caaaac.
Reduce LHS:
| [10] | aaaaa(caaaacbc) |
| [18] | ⇒ (aaaaacba) |
| ⇒ a |
Flip LHS and RHS.
Defines rule #8.
Referenced by [27].
Overlap of [25] aaaaacaaacba=caaaa with [20] cbaa=acba:
Critical pair: aaaaacaaaacba=caaaaa.
Reduce LHS:
| [26] | aaaaa(caaaac)ba |
| [2] | ⇒ aaaaa(aba) |
| ⇒ aaaaac |
Defines rule #7.