Invariants

SE.Transformation.Invariants

Finite regression guards for the transformation taxonomy.

operatorFamily and familyKind are total functions, so "every operator has exactly one family" holds by construction and is not restated here. The statements below can fail when the taxonomy is edited:

• the reference lists are duplicate-free and complete;
• no family and no kind is empty;
• the derived queries operatorsInFamily, operatorsInKind and familiesInKind agree with their membership specifications.

theorem SE.Transformation.referenceOperators_nodup : referenceOperators.Nodup

referenceOperators has no duplicates.

theorem SE.Transformation.referenceFamilies_nodup : referenceFamilies.Nodup

referenceFamilies has no duplicates.

theorem SE.Transformation.referenceKinds_nodup : referenceKinds.Nodup

referenceKinds has no duplicates.

theorem SE.Transformation.referenceOperators_complete (op : OperatorCode) : op ∈ referenceOperators

Every operator code occurs in referenceOperators.

theorem SE.Transformation.referenceFamilies_complete (f : TransformationFamily) : f ∈ referenceFamilies

Every transformation family occurs in referenceFamilies.

theorem SE.Transformation.referenceKinds_complete (k : TransformationKind) : k ∈ referenceKinds

Every transformation kind occurs in referenceKinds.

theorem SE.Transformation.mem_operatorsInFamily_iff {op : OperatorCode} {f : TransformationFamily} : op ∈ operatorsInFamily f ↔ operatorFamily op = f

Membership in operatorsInFamily is exactly family membership.

theorem SE.Transformation.mem_operatorsInKind_iff {op : OperatorCode} {k : TransformationKind} : op ∈ operatorsInKind k ↔ operatorKind op = k

Membership in operatorsInKind is exactly kind membership.

theorem SE.Transformation.mem_familiesInKind_iff {f : TransformationFamily} {k : TransformationKind} : f ∈ familiesInKind k ↔ familyKind f = k

Membership in familiesInKind is exactly the familyKind assignment.

theorem SE.Transformation.operatorsInFamily_ne_nil (f : TransformationFamily) : operatorsInFamily f ≠ []

Every family has at least one operator.

theorem SE.Transformation.familiesInKind_ne_nil (k : TransformationKind) : familiesInKind k ≠ []

Every kind has at least one family.

theorem SE.Transformation.operatorsInKind_ne_nil (k : TransformationKind) : operatorsInKind k ≠ []

Every kind has at least one operator.