Shows that the following theorem is wrong:

• Given two lenses, there exists a smallest lens containing both (no_least_lens)

def GaudisCrypt.CounterExamples.example_lens_1 : Lens bit (bit × bit × bit)

Equations

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

def GaudisCrypt.CounterExamples.example_lens_2 : Lens bit (bit × bit × bit)

Equations

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

def GaudisCrypt.CounterExamples.upper_bound_1 : Lens (bit × bit) (bit × bit × bit)

Equations

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

def GaudisCrypt.CounterExamples.upper_bound_2 : Lens (bit × bit) (bit × bit × bit)

Equations

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

theorem GaudisCrypt.CounterExamples.ub11 : LensIn.mk' upper_bound_1 ≥ LensIn.mk' example_lens_1

theorem GaudisCrypt.CounterExamples.ub12 : LensIn.mk' upper_bound_1 ≥ LensIn.mk' example_lens_2

theorem GaudisCrypt.CounterExamples.ub21 : LensIn.mk' upper_bound_2 ≥ LensIn.mk' example_lens_1

theorem GaudisCrypt.CounterExamples.ub22 : LensIn.mk' upper_bound_2 ≥ LensIn.mk' example_lens_2

theorem GaudisCrypt.CounterExamples.no_least_lens : ¬∃ (l : LensIn (bit × bit × bit)), IsLUB {LensIn.mk' example_lens_1, LensIn.mk' example_lens_2} l