title: It is possible to compute the Kauffman bracket using Z3py?
body: <p>I am trying to compute the Kauffman bracket of the trefoil knot using Z3py.  Until now I have the following code:</p>
  
  <pre><code>a, b, c, d, e, f, A, B = Ints('a b c d e f A B')
  
  delta = Function('delta', IntSort(), IntSort(), IntSort())
  def X(a,b,c,d):
      return A*delta(a,d)*delta(b,c)+B*delta(a,b)*delta(c,d)
  Trefoil = X(a,d,b,e)*X(e,b,f,c)*X(c,f,d,a)  
  print simplify(simplify(Trefoil, som= True),mul_to_power=True)
  </code></pre>
  
  <p>with this code I am obtaining the following output:</p>
  
  <pre><code>A**3·
  delta(a, e)·
  delta(b, f)·
  delta(c, a)·
  delta(d, b)·
  delta(e, c)·
  delta(f, d) +
  A**2·
  B·
  delta(a, d)·
  delta(b, e)·
  delta(b, f)·
  delta(c, a)·
  delta(e, c)·
  delta(f, d) +
  A**2·
  B·
  delta(a, e)·
  delta(c, a)·
  delta(d, b)·
  delta(e, b)·
  delta(f, c)·
  delta(f, d) +
  A·
  B**2·
  delta(a, d)·
  delta(b, e)·
  delta(c, a)·
  delta(e, b)·
  delta(f, c)·
  delta(f, d) +
  A**2·
  B·
  delta(a, e)·
  delta(b, f)·
  delta(c, f)·
  delta(d, a)·
  delta(d, b)·
  delta(e, c) +
  A·
  B**2·
  delta(a, d)·
  delta(b, e)·
  delta(b, f)·
  delta(c, f)·
  delta(d, a)·
  delta(e, c) +
  A·
  B**2·
  delta(a, e)·
  delta(c, f)·
  delta(d, a)·
  delta(d, b)·
  delta(e, b)·
  delta(f, c) +
  B**3·
  delta(a, d)·
  delta(b, e)·
  delta(c, f)·
  delta(d, a)·
  delta(e, b)·
  delta(f, c)
  </code></pre>
  
  <p>Now I need to apply the rule:</p>
  
  <pre><code>delta(a,b)*delta(b,c) = delta(a,c)
  </code></pre>
  
  <p>and to simplify the output using such rule.  Please, could you tell me how to do it.  Many thanks.</p>