defdata bit $($oneof $01))$

defdata bv $($listof bit$))$

defdata bv$5($list bit bit bit bit bit$))$

Note that bv$5$ is a subtype of bv: every element of bv$5$ is also an

element of bv$.$ This is how you state this fact. Think of the form

below as a kind of property involving data definitions.

defdata$-$subtype bv$5$ bv$)$

We define lobv$5,$ a list of bv$5\text{'}$s$.$ Something of this type is a

message.

defdata lobv$5($listof bv$5))$

We also define a list of bv$\text{'}$s$.$

defdata lobv $($listof bv$))$

Notice that lobv$5$ is a subtype of lobv.

defdata$-$subtype lobv$5$ lobv$)$

Question $1$

Use CHECK to check that is of type lobv$5.$

Us;; Question $1$

;; Use CHECK to check that $*$SECRET$-$MESSAGE$*$ is of type lobv$5.$

;; Use PROPERTY to check that $*$SECRET$-$MESSAGE$*$ is of type lobv$5.$

;;

;; Notice that PROPERTY is more general than CHECK and CHECK$=,$ as we can always

;; turn a CHECK or CHECK$=$ form into a PROPERTY form, eg given the form

;; $($CHECK exp$1)$

;; an equivalent PROPERTY form is:

;; $($PROPERTY $()$ exp$1)$

;; Given the form

;; $($CHECK$=$ exp$1$ exp$2)$

;; an equivalent PROPERTY form is:

;; $($PROPERTY $()(==$ exp$1$ exp$2))$

$($check XXX$)$

"Property $1"$

$($property $()$

XXX$)$