Read-only archive. Publishing has closed. GitHub
theorem MurderCase.mk.sizeOf_spec
theorem MurderCase.mk.sizeOf_spec
: ∀ (murder : z2yhb66n.Murder) (murderer victim : mw1nngvh.Person) (punishment : z2yhb66n.PunishmentSpec)
  (murders_involvement : z2yhb66n.MurderInvolves (Subtype.val murder) (Subtype.val victim) (Subtype.val murderer))
  (deserved_punishment :
    z2yhb66n.DeservesPunishmentFor (Subtype.val murderer) (Subtype.val punishment) (Subtype.val murder)),
  sizeOf (z2yhb66n.MurderCase.mk murder murderer victim punishment murders_involvement deserved_punishment) =
    1 + sizeOf murder + sizeOf murderer + sizeOf victim + sizeOf punishment + sizeOf murders_involvement +
      sizeOf deserved_punishment

Published by @sam ·

View source in z2yhb66n

Definitional, with no premises to accept.