• 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
Name
Last commit
Last update
benchmark Loading commit data...
docs Loading commit data...
tests Loading commit data...
theories Loading commit data...
.gitattributes Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
.gitmodules Loading commit data...
CHANGELOG.md Loading commit data...
CONTRIBUTING.md Loading commit data...
Editor.md Loading commit data...
LICENSE Loading commit data...
LICENSE-CODE Loading commit data...
LICENSE-DOCS Loading commit data...
Makefile Loading commit data...
Makefile.coq.local Loading commit data...
Naming.md Loading commit data...
ProofMode.md Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
descr Loading commit data...
opam Loading commit data...