290 Formalization

6 Functions