Documentation

SE.Transformation.Reference.Composition

Composition Reference #

Canonical known composition rules for transformation operators.

The lookup is intentionally partial. none means that this theory does not currently specify a canonical composition relation for the ordered pair. It does not mean that the pair is invalid or semantically unknown.

Composition is directional: (left, right) and (right, left) are distinct queries.

source
def SE.Transformation.composition? :
OperatorCode → OperatorCode → Option CompositionRelation

Return the canonical composition relation for an ordered operator pair when one is specified by this theory.

Equations
Instances For
    source
    @[simp]
    theorem SE.Transformation.authorizeThenAttest :
    composition? OperatorCode.AZ OperatorCode.AT = some CompositionRelation.composable

    Authorization followed by attestation is a canonical composable pair.

    source
    @[simp]
    theorem SE.Transformation.bindThenUnbind :
    composition? OperatorCode.BD OperatorCode.UB = some CompositionRelation.inverseLike

    Binding followed by unbinding is a canonical inverse-like sequence.

    source
    @[simp]
    theorem SE.Transformation.splitThenMerge :
    composition? OperatorCode.SP OperatorCode.MG = some CompositionRelation.inverseLike

    Splitting followed by merging is a canonical inverse-like sequence.

    source
    theorem SE.Transformation.composition_defined_iff (left right : OperatorCode) :
    (∃ (relation : CompositionRelation), composition? left right = some relation) ↔ left = OperatorCode.AZ ∧ right = OperatorCode.AT ∨ left = OperatorCode.BD ∧ right = OperatorCode.UB ∨ left = OperatorCode.SP ∧ right = OperatorCode.MG

    A composition relation is specified exactly for the three canonical ordered pairs currently declared by this theory.