| Back: | ⟨a, b | abb=aaa, baa=ab⟩ |
|---|
Completion settings:
Axiom: abb=aaa.
Referenced by [3].
Axiom: baa=ab.
Flip LHS and RHS.
Defines rule #2.
Overlap of [1] abb=aaa with [2] ab=baa:
Critical pair: baab=aaa.
Reduce LHS:
| [2] | ba(ab) |
| [2] | ⇒ b(ab)aa |
| ⇒ bbaaaa |
Referenced by [4], [5], [6], [7], [10].
Overlap of [2] ab=baa with [3] bbaaaa=aaa:
Critical pair: aaaa=baabaaaa.
Reduce RHS:
| [2] | ba(ab)aaaa |
| [2] | ⇒ b(ab)aaaaaa |
| [3] | ⇒ (bbaaaa)aaaa |
| ⇒ aaaaaaa |
Flip LHS and RHS.
Overlap of [3] bbaaaa=aaa with [2] ab=baa:
Critical pair: bbaaabaa=aaab.
Reduce LHS:
| [2] | bbaa(ab)aa |
| [2] | ⇒ bba(ab)aaaa |
| [2] | ⇒ bb(ab)aaaaaa |
| [3] | ⇒ b(bbaaaa)aaaa |
| [4] | ⇒ b(aaaaaaa) |
| ⇒ baaaa |
Reduce RHS:
| [2] | aa(ab) |
| [2] | ⇒ a(ab)aa |
| [2] | ⇒ (ab)aaaa |
| ⇒ baaaaaa |
Flip LHS and RHS.
Referenced by [8].
Overlap of [3] bbaaaa=aaa with [4] aaaaaaa=aaaa:
Critical pair: bbaaaa=aaaaaa.
Reduce LHS:
| [3] | (bbaaaa) |
| ⇒ aaa |
Flip LHS and RHS.
Overlap of [3] bbaaaa=aaa with [6] aaaaaa=aaa:
Critical pair: bbaaa=aaaaa.
Referenced by [9], [10], [11].
Simplify [5] baaaaaa=baaaa.
Reduce LHS:
| [6] | b(aaaaaa) |
| ⇒ baaa |
Flip LHS and RHS.
Referenced by [9].
Overlap of [7] bbaaa=aaaaa with [8] baaaa=baaa:
Critical pair: bbaaa=aaaaaa.
Reduce LHS:
| [7] | (bbaaa) |
| ⇒ aaaaa |
Reduce RHS:
| [6] | (aaaaaa) |
| ⇒ aaa |
Referenced by [10].
Overlap of [3] bbaaaa=aaa with [9] aaaaa=aaa:
Critical pair: bbaaa=aaaa.
Reduce LHS:
| [7] | (bbaaa) |
| [9] | ⇒ (aaaaa) |
| ⇒ aaa |
Flip LHS and RHS.
Defines rule #1.
Referenced by [11].
Simplify [7] bbaaa=aaaaa.
Reduce RHS:
| [10] | (aaaa)a |
| [10] | ⇒ (aaaa) |
| ⇒ aaa |
Defines rule #3.