Counterexample to the theorem:

A lens range has trivial intersection with its complement.

(It even shows: there is a lens range that is its own complement)

def GaudisCrypt.CounterExamples.flipRange : DetermFootprint Bool

Counterexample: {id, Bool.not} is a valid DetermFootprint Bool that is its own complement, disproving DetermFootprint.compl_is_compl for general DetermFootprints.

Equations

• One or more equations did not get rendered due to their size.

theorem GaudisCrypt.CounterExamples.flipRange_compl_eq_self : flipRangeᶜ = flipRange