Union of LTSs

Note: there is a nontrivial balance between ergonomics and generality here. These definitions might change in the future.

def Cslib.LTS.union {State : Type u} {Label : Type v} (lts1 lts2 : LTS State Label) : LTS State Label

The union of two LTSs defined on the same types.

Equations

• lts1.union lts2 = { Tr := lts1.Tr ⊔ lts2.Tr }

def Cslib.LTS.unionSubtype {State : Type u} {Label : Type v} {S1 : State → Prop} {L1 : Label → Prop} {S2 : State → Prop} {L2 : Label → Prop} [DecidablePred S1] [DecidablePred L1] [DecidablePred S2] [DecidablePred L2] (lts1 : LTS (Subtype S1) (Subtype L1)) (lts2 : LTS (Subtype S2) (Subtype L2)) : LTS State Label

The union of two LTSs that have common supertypes for states and labels.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.LTS.inl {State : Type u} {Label : Type v} {State' : Type u_1} (lts : LTS State Label) : LTS { x : State ⊕ State' // x.isLeft = true } { _label : Label // True }

Lifting of an LTS State Label to LTS (State ⊕ State') Label.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.LTS.inr {State : Type u} {Label : Type v} {State' : Type u_1} (lts : LTS State Label) : LTS { x : State' ⊕ State // x.isRight = true } { _label : Label // True }

Lifting of an LTS State Label to LTS (State' ⊕ State) Label.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.LTS.unionSum {Label : Type v} {State1 : Type u_1} {State2 : Type u_2} (lts1 : LTS State1 Label) (lts2 : LTS State2 Label) : LTS (State1 ⊕ State2) Label

Union of two LTSs with the same Label type. The result combines the original respective state types State1 and State2 into (State1 ⊕ State2).

Equations

• lts1.unionSum lts2 = lts1.inl.unionSubtype lts2.inr