Conformance

SE.Persistence.Conformance

Finite regression guards for the Persistence public surface.

The statements below can fail when the vocabulary is edited:

• the reference list of classification values is duplicate-free and complete;
• ign, prs and brk are pairwise distinct;
• the coarse matrix agrees with the pattern at applicable transformations and sends inapplicable ones to ign;
• lifting along the Transformation taxonomy commutes with the coarse matrix.

Mathematical theorems about the relations are not restated here.

theorem SE.Persistence.referenceClassificationValues_nodup : referenceClassificationValues.Nodup

referenceClassificationValues has no duplicates.

theorem SE.Persistence.referenceClassificationValues_complete (v : ClassificationValue) : v ∈ referenceClassificationValues

Every classification value occurs in referenceClassificationValues.

theorem SE.Persistence.referenceClassificationValues_length : referenceClassificationValues.length = 3

There are exactly three classification values.

theorem SE.Persistence.prs_ne_brk : ClassificationValue.prs ≠ ClassificationValue.brk

Preserving and breaking are different values.

theorem SE.Persistence.ign_ne_prs : ClassificationValue.ign ≠ ClassificationValue.prs

Ignoring and preserving are different values.

theorem SE.Persistence.ign_ne_brk : ClassificationValue.ign ≠ ClassificationValue.brk

Ignoring and breaking are different values.

theorem SE.Persistence.liftFamily_coarse_all (c : Classification Transformation.TransformationFamily) (op : Transformation.OperatorCode) : c.liftFamily.coarse op = c.coarse (Transformation.operatorFamily op)

Lifting along families commutes with the coarse matrix, operator by operator.

theorem SE.Persistence.liftKind_coarse_all (c : Classification Transformation.TransformationKind) (op : Transformation.OperatorCode) : c.liftKind.coarse op = c.coarse (Transformation.operatorKind op)

Lifting along kinds commutes with the coarse matrix, operator by operator.