Skip to content
  • Robbert Krebbers's avatar
    The unbounded fractional authoritative camera. · 1d67a47f
    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) → ●?{p} a ~~> ●?{p + q} (a ⋅ b) ⋅ ◯?{q} b
    
    - At the cost of that, we no longer have the `◯?{1} a` is an exclusive
      fragmental element (cf. `frac_auth_frag_validN_op_1_l`).
    1d67a47f