This repository contains the theory files for the paper `Contextuality in distributed systems'
Notable proofs include - The proof that maximal covers are closed under antichain meet and join, located in Topological_Spaces.thy (max_cover_closed_meet && max_cover_closed_join)
The proof of theorem 2 (that Chaos forms a tuple system) can be found at the bottom of Information_Algebras.thy
Example 1 is formalised in Example.thy
Proofs currently build in release candidate 2 for Isabelle 2022, other versions untested.