bunched.prelude.sets

• Preimage of a FinMap
• set_map_2

bunched.prelude.lists

bunched.algebra.notation

• Turnstiles
• BI connectives
• Update modalities
• Big Ops

bunched.algebra.interface

• Axioms for a general BI (logic of bunched implications)

bunched.algebra.derived_laws

bunched.algebra.bi

bunched.algebra.from_monoid

bunched.algebra.from_closure

• Algebra carrier
  • Additional operations
• Properties of the closure operator and closed sets
• Closure strength and the BI operations
  • BI laws
• Other properties

bunched.syntax

• Formulas and bunches
  • Bunched contexts with a hole
  • Bunch equivalence
• Properties

bunched.terms

• Bunched terms
  • Term linearization
  • Term "folding"
  • Structural rules
• Properties
  • fmap properties
  • interpretation properties
  • linearization properties
  • term folding properties

bunched.analytic_completion

bunched.bunch_decomp

• Alternative representation of decomposition of bunches
• Properties of bunched contexts

bunched.seqcalc

• Sequent calculus
• Properties
• Interpretation

bunched.interp

• Interpretation of BI intro the associated algebras

bunched.seqcalc_height

• • Alternative formulation of bunch equivalences
• SEQUENT CALCULUS
• Inversion lemmas

bunched.cutelim

• Parameters to the proof: a list of simple structural extensions
• Construction of the 'universal' cf-provability algebra
  • Principal closed sets
• Baisc properties of C
• We show that cl is strong
• Interpretation in C and Okada's lemma
  • Simple structural rules in C
• Cut admissibility

bunched.seqcalc_s4

• Syntax and sequence calculus for BI□
  • Formulas and bunches
  • Bunch equivalence
  • Sequent calculus itself
  • Alternative representation of decomposition of bunches
• Properties

bunched.interp_s4

• Interpretation of the sequent calculus in an arbitrary BI.

bunched.seqcalc_height_s4

• • Alternative formulation of bunch equivalences
• SEQUENT CALCULUS
• Inversion lemmas

bunched.cutelim_s4