This MR is a follow up on the renamings performed (implicitly) as part of !215 (merged). This MR makes the following changes:
-
auth_both_frac_valid
andauth_both_valid
are now of the same shape asauth_both_frac_validN
andauth_both_validN
. That is, both are now biimplications. - The left-to-right direction of
auth_both_frac_valid
andauth_both_valid
only holds in case the camera is discrete. The right-to-left versions for non-discrete cameras are suffixed_2
, the convention that we use throughout the development. - Change the direction of lemmas like
auth_frag_valid
andauth_auth_valid
so that it's consistent with the other lemmas. I.e. make sure that the ◯ and ● are always on the LHS of the biimplication.