| Back: | ⟨a, b | aaa=bb, babab=b⟩ |
|---|
Completion settings:
Axiom: aaa=bb.
Flip LHS and RHS.
Defines rule #4.
Referenced by [3], [4], [5], [7], [8], [9].
Axiom: babab=b.
Defines rule #5.
Overlap of [1] bb=aaa with [1] bb=aaa:
Critical pair: baaa=aaab.
Flip LHS and RHS.
Defines rule #3.
Referenced by [4], [6], [7], [9].
Overlap of [1] bb=aaa with [2] babab=b:
Critical pair: bb=aaaabab.
Reduce LHS:
| [1] | (bb) |
| ⇒ aaa |
Reduce RHS:
| [3] | a(aaab)ab |
| [3] | ⇒ aba(aaab) |
| ⇒ ababaaa |
Flip LHS and RHS.
Referenced by [9].
Overlap of [2] babab=b with [1] bb=aaa:
Critical pair: babaaaa=bb.
Reduce RHS:
| [1] | (bb) |
| ⇒ aaa |
Overlap of [5] babaaaa=aaa with [3] aaab=baaa:
Critical pair: babaabaaa=aaaab.
Reduce RHS:
| [3] | a(aaab) |
| ⇒ abaaa |
Referenced by [8].
Overlap of [5] babaaaa=aaa with [3] aaab=baaa:
Critical pair: babaaabaaa=aaaaab.
Reduce LHS:
| [3] | bab(aaab)aaa |
| [1] | ⇒ ba(bb)aaaaaa |
| ⇒ baaaaaaaaaa |
Reduce RHS:
| [3] | aa(aaab) |
| ⇒ aabaaa |
Flip LHS and RHS.
Referenced by [8].
Simplify [6] babaabaaa=abaaa.
Reduce LHS:
| [7] | bab(aabaaa) |
| [1] | ⇒ ba(bb)aaaaaaaaaa |
| ⇒ baaaaaaaaaaaaaa |
Flip LHS and RHS.
Defines rule #2.
Referenced by [9].
Overlap of [8] abaaa=baaaaaaaaaaaaaa with [3] aaab=baaa:
Critical pair: ababaaa=baaaaaaaaaaaaaaab.
Reduce LHS:
| [4] | (ababaaa) |
| ⇒ aaa |
Reduce RHS:
| [3] | baaaaaaaaaaaa(aaab) |
| [3] | ⇒ baaaaaaaaa(aaab)aaa |
| [3] | ⇒ baaaaaa(aaab)aaaaaa |
| [3] | ⇒ baaa(aaab)aaaaaaaaa |
| [3] | ⇒ b(aaab)aaaaaaaaaaaa |
| [1] | ⇒ (bb)aaaaaaaaaaaaaaa |
| ⇒ aaaaaaaaaaaaaaaaaa |
Flip LHS and RHS.
Defines rule #1.