		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Concatenation-wfp

A concatenation is well-formed iff it is not empty and all its repetitions are well-formed.

Signature
(concatenation-wfp concatenation) → yes/no
Arguments: concatenation — Guard (concatenationp concatenation).
Returns: yes/no — Type (booleanp yes/no).

This non-emptiness condition is required by the rule concatenation in [RFC:4]. The well-formedness condition on the repetitions is structural.

Function: concatenation-wfp

(defun concatenation-wfp (concatenation)
  (declare (xargs :guard (concatenationp concatenation)))
  (and (consp concatenation)
       (repetition-list-wfp concatenation)))