title: Accumulation of union of sets
body: <p>I have two classes <code>A</code> and <code>B</code> and a relation with extra data of class <code>R</code> on them.</p>
  <p>So, <code>A</code> and <code>B</code> are related to each other via <code>R</code>.</p>
  <pre><code>sig A {}
  sig B {}
  
  sig R {
      a : A,
      b : B,
      data : Bool
  }
  </code></pre>
  <p>here, Bool is defined as:</p>
  <pre><code>sig Bool {}
  sig True, False extends Bool {}
  </code></pre>
  <p>Now, I extend <code>A</code> like this:</p>
  <pre><code>sig A{
      allb : some B
  }
  </code></pre>
  <p>Which contains all instances of <code>B</code> for which there is a relation between this <code>A</code> and that <code>B</code> and where the data is of type <code>True</code>.</p>
  <p>I want to express the following logical statement as an Alloy fact:</p>
  <p><a href="https://i.stack.imgur.com/MC2WI.png" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/MC2WI.png" alt="Formal version of text above" /></a><br />
  <sub>(source: <a href="http://dropproxy.com/f/3B" rel="nofollow noreferrer">dropproxy.com</a>)</sub></p>
  <p>I assume here that <code>True == 1</code> and <code>False != 1</code> and that the sets <code>A</code> and <code>R</code> contain all instances of <code>A</code> and <code>R</code> respectively.</p>
  <p>What I've tried so far is to define a <code>fun trueR(a : A)</code> which should return all <code>R</code>'s for which <code>R.a = a and r.data = True</code> and a <code>fact allbIsRTrue</code> which states that for each <code>A</code> <code>allb</code> should be the sum of the <code>R.b</code>'s returned by <code>trueR</code>.</p>
  <p>However, here is where I get stuck, I can't find the right construct to sum over sets in the reference and tries with <code>sum</code> have resulted in syntax errors.</p>
  <p>How would I specify my formal constraint as an Alloy fact?</p>