| Back: | ⟨a, b, c | aab=cc, baa=1⟩ |
|---|
Completion settings:
Axiom: aab=cc.
Flip LHS and RHS.
Defines rule #16.
Axiom: baa=1.
Defines rule #1.
Referenced by [4], [8], [9], [10], [15], [17], [18], [20], [21], [22], [26].
Axiom: aca=d.
Referenced by [4], [5], [10], [12].
Overlap of [2] baa=1 with [3] aca=d:
Critical pair: bad=ca.
Flip LHS and RHS.
Defines rule #7.
Referenced by [5], [6], [7], [11], [12], [17], [18], [23], [25].
Overlap of [4] ca=bad with [3] aca=d:
Critical pair: cd=badca.
Reduce RHS:
| [4] | bad(ca) |
| ⇒ badbad |
Defines rule #13.
Overlap of [1] cc=aab with [1] cc=aab:
Critical pair: caab=aabc.
Reduce LHS:
| [4] | (ca)ab |
| ⇒ badab |
Flip LHS and RHS.
Overlap of [1] cc=aab with [4] ca=bad:
Critical pair: cbad=aaba.
Defines rule #15.
Referenced by [10], [17], [18].
Overlap of [2] baa=1 with [6] aabc=badab:
Critical pair: bbadab=bc.
Flip LHS and RHS.
Referenced by [9], [10], [11], [26].
Overlap of [2] baa=1 with [6] aabc=badab:
Critical pair: babadab=abc.
Reduce RHS:
| [8] | a(bc) |
| ⇒ abbadab |
Referenced by [13].
Overlap of [3] aca=d with [6] aabc=badab:
Critical pair: acbadab=dabc.
Reduce LHS:
| [7] | a(cbad)ab |
| [2] | ⇒ aaa(baa)b |
| ⇒ aaab |
Reduce RHS:
| [8] | da(bc) |
| ⇒ dabbadab |
Flip LHS and RHS.
Referenced by [14].
Overlap of [8] bc=bbadab with [4] ca=bad:
Critical pair: bbad=bbadaba.
Flip LHS and RHS.
Referenced by [19].
Overlap of [3] aca=d with [4] ca=bad:
Critical pair: abad=d.
Defines rule #4.
Referenced by [13], [16], [24], [29], [30].
Overlap of [9] babadab=abbadab with [12] abad=d:
Critical pair: bdab=abbadab.
Flip LHS and RHS.
Overlap of [10] dabbadab=aaab with [13] abbadab=bdab:
Critical pair: dbdab=aaab.
Overlap of [14] dbdab=aaab with [2] baa=1:
Critical pair: dbda=aaabaa.
Reduce RHS:
| [2] | aaa(baa) |
| ⇒ aaa |
Defines rule #9.
Overlap of [14] dbdab=aaab with [12] abad=d:
Critical pair: dbdd=aaabad.
Reduce RHS:
| [12] | aa(abad) |
| ⇒ aad |
Defines rule #17.
Referenced by [18].
Overlap of [7] cbad=aaba with [15] dbda=aaa:
Critical pair: cbaaaa=aababda.
Reduce LHS:
| [2] | c(baa)aa |
| [4] | ⇒ (ca)a |
| ⇒ bada |
Flip LHS and RHS.
Referenced by [27].
Overlap of [7] cbad=aaba with [16] dbdd=aad:
Critical pair: cbaaad=aababdd.
Reduce LHS:
| [2] | c(baa)ad |
| [4] | ⇒ (ca)d |
| ⇒ badd |
Flip LHS and RHS.
Referenced by [28].
Overlap of [13] abbadab=bdab with [11] bbadaba=bbad:
Critical pair: abbad=bdaba.
Overlap of [2] baa=1 with [19] abbad=bdaba:
Critical pair: babdaba=bbad.
Flip LHS and RHS.
Defines rule #5.
Referenced by [26].
Overlap of [19] abbad=bdaba with [15] dbda=aaa:
Critical pair: abbaaaa=bdababda.
Reduce LHS:
| [2] | ab(baa)aa |
| [2] | ⇒ a(baa) |
| ⇒ a |
Flip LHS and RHS.
Referenced by [22].
Overlap of [21] bdababda=a with [21] bdababda=a:
Critical pair: bdabaa=ababda.
Reduce LHS:
| [2] | bda(baa) |
| ⇒ bda |
Flip LHS and RHS.
Defines rule #6.
Referenced by [23], [24], [27].
Overlap of [4] ca=bad with [22] ababda=bda:
Critical pair: cbda=badbabda.
Defines rule #14.
Overlap of [22] ababda=bda with [12] abad=d:
Critical pair: ababdd=bdabad.
Reduce RHS:
| [12] | bd(abad) |
| ⇒ bdd |
Defines rule #12.
Overlap of [4] ca=bad with [24] ababdd=bdd:
Critical pair: cbdd=badbabdd.
Defines rule #18.
Simplify [8] bc=bbadab.
Reduce RHS:
| [20] | (bbad)ab |
| [2] | ⇒ babda(baa)b |
| ⇒ babdab |
Defines rule #8.
Overlap of [17] aababda=bada with [22] ababda=bda:
Critical pair: abda=bada.
Flip LHS and RHS.
Defines rule #2.
Referenced by [29].
Overlap of [18] aababdd=badd with [24] ababdd=bdd:
Critical pair: abdd=badd.
Flip LHS and RHS.
Defines rule #10.
Overlap of [12] abad=d with [27] bada=abda:
Critical pair: aabda=da.
Defines rule #3.
Referenced by [30].
Overlap of [29] aabda=da with [12] abad=d:
Critical pair: aabdd=dabad.
Reduce RHS:
| [12] | d(abad) |
| ⇒ dd |
Defines rule #11.