| Back: | ⟨a, b | aaaabbabba=1⟩ |
|---|
Completion settings:
Axiom: aaaabbabba=1.
Referenced by [4].
Axiom: aaaa=c.
Defines rule #5.
Referenced by [4], [5], [6], [8], [9], [13], [17], [20], [27], [31].
Axiom: abb=d.
Overlap of [1] aaaabbabba=1 with [2] aaaa=c:
Critical pair: cbbabba=1.
Reduce LHS:
| [3] | cbb(abb)a |
| ⇒ cbbda |
Referenced by [7].
Overlap of [2] aaaa=c with [2] aaaa=c:
Critical pair: ac=ca.
Defines rule #2.
Referenced by [19], [28], [29].
Overlap of [2] aaaa=c with [3] abb=d:
Critical pair: aaad=cbb.
Flip LHS and RHS.
Referenced by [7].
Simplify [4] cbbda=1.
Reduce LHS:
| [6] | (cbb)da |
| ⇒ aaadda |
Referenced by [8], [9], [10], [11], [12], [13], [14].
Overlap of [2] aaaa=c with [7] aaadda=1:
Critical pair: a=cdda.
Flip LHS and RHS.
Overlap of [2] aaaa=c with [7] aaadda=1:
Critical pair: aa=cadda.
Flip LHS and RHS.
Referenced by [13].
Overlap of [7] aaadda=1 with [3] abb=d:
Critical pair: aaaddd=bb.
Flip LHS and RHS.
Referenced by [15].
Overlap of [7] aaadda=1 with [7] aaadda=1:
Critical pair: aaadd=aadda.
Referenced by [12], [14], [15].
Overlap of [8] cdda=a with [7] aaadda=1:
Critical pair: cdd=aaadda.
Reduce RHS:
| [11] | (aaadd)a |
| ⇒ aaddaa |
Flip LHS and RHS.
Overlap of [9] cadda=aa with [7] aaadda=1:
Critical pair: cadd=aaaadda.
Reduce RHS:
| [2] | (aaaa)dda |
| [8] | ⇒ (cdda) |
| ⇒ a |
Referenced by [23].
Overlap of [7] aaadda=1 with [11] aaadd=aadda:
Critical pair: aaddaa=1.
Reduce LHS:
| [12] | (aaddaa) |
| ⇒ cdd |
Defines rule #3.
Referenced by [16], [21], [22], [26], [28], [30], [32].
Simplify [10] bb=aaaddd.
Reduce RHS:
| [11] | (aaadd)d |
| ⇒ aaddad |
Referenced by [24].
Simplify [12] aaddaa=cdd.
Reduce RHS:
| [14] | (cdd) |
| ⇒ 1 |
Overlap of [16] aaddaa=1 with [2] aaaa=c:
Critical pair: aaddc=aa.
Referenced by [19].
Overlap of [16] aaddaa=1 with [16] aaddaa=1:
Critical pair: aadd=ddaa.
Referenced by [19].
Simplify [17] aaddc=aa.
Reduce LHS:
| [18] | (aadd)c |
| [5] | ⇒ dda(ac) |
| [5] | ⇒ dd(ac)a |
| ⇒ ddcaa |
Referenced by [20].
Overlap of [19] ddcaa=aa with [2] aaaa=c:
Critical pair: ddcc=aaaa.
Reduce RHS:
| [2] | (aaaa) |
| ⇒ c |
Referenced by [21].
Overlap of [20] ddcc=c with [14] cdd=1:
Critical pair: ddc=cdd.
Reduce RHS:
| [14] | (cdd) |
| ⇒ 1 |
Referenced by [22], [23], [27].
Overlap of [14] cdd=1 with [21] ddc=1:
Critical pair: cd=dc.
Flip LHS and RHS.
Defines rule #1.
Overlap of [21] ddc=1 with [13] cadd=a:
Critical pair: dda=add.
Flip LHS and RHS.
Defines rule #4.
Referenced by [24], [27], [30], [32].
Simplify [15] bb=aaddad.
Reduce RHS:
| [23] | a(add)ad |
| [23] | ⇒ (add)aad |
| ⇒ ddaaad |
Defines rule #8.
Referenced by [25].
Overlap of [24] bb=ddaaad with [24] bb=ddaaad:
Critical pair: bddaaad=ddaaadb.
Flip LHS and RHS.
Overlap of [14] cdd=1 with [25] ddaaadb=bddaaad:
Critical pair: cbddaaad=aaadb.
Flip LHS and RHS.
Defines rule #7.
Overlap of [23] add=dda with [25] ddaaadb=bddaaad:
Critical pair: abddaaad=ddaaaadb.
Reduce RHS:
| [2] | dd(aaaa)db |
| [21] | ⇒ (ddc)db |
| ⇒ db |
Referenced by [28].
Overlap of [27] abddaaad=db with [22] dc=cd:
Critical pair: abddaaacd=dbc.
Reduce LHS:
| [5] | abddaa(ac)d |
| [5] | ⇒ abdda(ac)ad |
| [5] | ⇒ abdd(ac)aad |
| [22] | ⇒ abd(dc)aaad |
| [22] | ⇒ ab(dc)daaad |
| [14] | ⇒ ab(cdd)aaad |
| ⇒ abaaad |
Referenced by [29].
Overlap of [28] abaaad=dbc with [22] dc=cd:
Critical pair: abaaacd=dbcc.
Reduce LHS:
| [5] | abaa(ac)d |
| [5] | ⇒ aba(ac)ad |
| [5] | ⇒ ab(ac)aad |
| ⇒ abcaaad |
Referenced by [30].
Overlap of [29] abcaaad=dbcc with [23] add=dda:
Critical pair: abcaadda=dbccd.
Reduce LHS:
| [23] | abca(add)a |
| [23] | ⇒ abc(add)aa |
| [14] | ⇒ ab(cdd)aaa |
| ⇒ abaaa |
Referenced by [31].
Overlap of [30] abaaa=dbccd with [2] aaaa=c:
Critical pair: abc=dbccda.
Referenced by [32].
Overlap of [31] abc=dbccda with [14] cdd=1:
Critical pair: ab=dbccdadd.
Reduce RHS:
| [23] | dbccd(add) |
| [14] | ⇒ dbc(cdd)da |
| ⇒ dbcda |
Defines rule #6.