1. 11 Jun, 2019 2 commits
    • Robbert Krebbers's avatar
      The unbounded fractional authoritative camera. · 151dda05
      Robbert Krebbers authored
      The unbounded fractional authoritative camera is a version of the fractional
      authoritative camera that can be used with fractions `> 1`.
      
      Most of the reasoning principles for this version of the fractional
      authoritative cameras are the same as for the original version. There are two
      difference:
      
      - We get the additional rule that can be used to allocate a "surplus", i.e.
        if we have the authoritative element we can always increase its fraction
        and allocate a new fragment.
      
            ✓ (a ⋅ b) → ●U{p} a ~~> ●U{p + q} (a ⋅ b) ⋅ ◯U{q} b
      
      - At the cost of that, we no longer have the `◯U{1} a` is an exclusive
        fragmental element (cf. `frac_auth_frag_validN_op_1_l`).
      151dda05
    • Robbert Krebbers's avatar
      8ebe1485
  2. 10 Jun, 2019 9 commits
  3. 09 Jun, 2019 6 commits
  4. 07 Jun, 2019 2 commits
  5. 06 Jun, 2019 7 commits
  6. 05 Jun, 2019 12 commits
  7. 04 Jun, 2019 2 commits