Structural System Composition

Defines System.compose, which joins two systems via bridge connectors, and proves that composition preserves WellFormed.

def VerifiedMBSE.Core.System.compose (s1 s2 : System) (bridge : List Connector) : System

Compose two systems via bridge connectors.

Equations

• s1.compose s2 bridge = { parts := s1.parts ++ s2.parts, connectors := s1.connectors ++ s2.connectors ++ bridge }

theorem VerifiedMBSE.Core.System.compose_parts (s1 s2 : System) (bridge : List Connector) : (s1.compose s2 bridge).parts = s1.parts ++ s2.parts

parts after compose is the concatenation.

theorem VerifiedMBSE.Core.System.compose_connectors (s1 s2 : System) (bridge : List Connector) : (s1.compose s2 bridge).connectors = s1.connectors ++ s2.connectors ++ bridge

connectors after compose is the concatenation.

theorem VerifiedMBSE.Core.System.compose_WellFormed (s1 s2 : System) (bridge : List Connector) (hw1 : s1.WellFormed) (hw2 : s2.WellFormed) (hbridge : ∀ (c : Connector), c ∈ bridge → c.source.part ∈ s1.parts ++ s2.parts ∧ c.target.part ∈ s1.parts ++ s2.parts) : (s1.compose s2 bridge).WellFormed

compose preserves WellFormed: if both systems are WellFormed and bridges reference composed parts, the result is also WellFormed.