# Theory Message_Bus

    (*  File:       Message_Bus.thy
        Copyright   2026  Ludwig-Maximilians-Universität (LMU) München
    *)
    ✐‹creator "Michael Kirsten, Ludwig-Maximilians-Universität München"›
    ✐‹contributor "Terru Stübinger, Karlsruhe Institute of Technology (KIT)"›
    section ‹Model Three: Message Bus›

    theory Message_Bus
      imports "Featherweight_OCL.UML_Main"
    begin

    text ‹
      Featherweight OCL can only reason about one meta-model at a time.
      So in the following, we will have one model containing classes Car1 and Car2,
      but pretend they are separate.

      Note: This should correspond to Figure 5 from the paper.
    ›

    subsection ‹Types›

    datatype 𝒯⇩C⇩a⇩r⇩1 = mk⇩C⇩a⇩r⇩1 (car1⇩o⇩i⇩d: oid) (car1⇩m⇩b: "oid option")
    datatype 𝒯⇩C⇩a⇩r⇩2 = mk⇩C⇩a⇩r⇩2 (car2⇩o⇩i⇩d: oid) (car2⇩m⇩b: "oid option")
    datatype 𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 = mk⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 (mb1⇩o⇩i⇩d: oid)
                            (mb1⇩p⇩r⇩o⇩t: "string option")
    datatype 𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 = mk⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 (mb2⇩o⇩i⇩d: oid)
    datatype 𝒯⇩E⇩C⇩U⇩2 = mk⇩E⇩C⇩U⇩2 (ecu2⇩o⇩i⇩d: oid) (ecu2⇩p⇩r⇩o⇩t: "string option")

    datatype 𝔄 =
      in⇩C⇩a⇩r⇩1 𝒯⇩C⇩a⇩r⇩1 | in⇩C⇩a⇩r⇩2 𝒯⇩C⇩a⇩r⇩2 | in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 |
        in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 | in⇩E⇩C⇩U⇩2 𝒯⇩E⇩C⇩U⇩2

    type_synonym Boolean         = "𝔄 Boolean"
    type_synonym Integer         = "𝔄 Integer"
    type_synonym String          = "𝔄 String"
    type_synonym Void            = "𝔄 Void"
    type_synonym Car1            = "(𝔄, 𝒯⇩C⇩a⇩r⇩1 option option) val"
    type_synonym Car2            = "(𝔄, 𝒯⇩C⇩a⇩r⇩2 option option) val"
    type_synonym MessageBus1     = "(𝔄, 𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 option option) val"
    type_synonym MessageBus2     = "(𝔄, 𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 option option) val"
    type_synonym ECU2            = "(𝔄, 𝒯⇩E⇩C⇩U⇩2 option option) val"
    type_synonym Set_Integer     = "(𝔄, int option option) Set"
    type_synonym Set_String      = "(𝔄, string option option) Set"
    type_synonym Set_Car1        = "(𝔄, 𝒯⇩C⇩a⇩r⇩1 option option) Set"
    type_synonym Set_Car2        = "(𝔄, 𝒯⇩C⇩a⇩r⇩2 option option) Set"
    type_synonym Set_MessageBus1 = "(𝔄, 𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 option option) Set"
    type_synonym Set_MessageBus2 = "(𝔄, 𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 option option) Set"
    type_synonym Set_ECU2        = "(𝔄, 𝒯⇩E⇩C⇩U⇩2 option option) Set"

    subsubsection ‹Some Machinery›

    instantiation 𝒯⇩C⇩a⇩r⇩1 :: object
    begin
    definition oid_of_𝒯⇩C⇩a⇩r⇩1[code_unfold]: "oid_of ≡ car1⇩o⇩i⇩d"
      instance ..
    end
    instantiation 𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 :: object
    begin
    definition oid_of_𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1[code_unfold]: "oid_of ≡ mb1⇩o⇩i⇩d"
      instance ..
    end
    instantiation 𝒯⇩C⇩a⇩r⇩2 :: object
    begin
      definition oid_of_𝒯⇩C⇩a⇩r⇩2[code_unfold]: "oid_of ≡ car2⇩o⇩i⇩d"
      instance ..
    end
    instantiation 𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 :: object
    begin
    definition oid_of_𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2[code_unfold]: "oid_of ≡ mb2⇩o⇩i⇩d"
      instance ..
    end
    instantiation 𝒯⇩E⇩C⇩U⇩2 :: object
    begin
      definition oid_of_𝒯⇩E⇩C⇩U⇩2[code_unfold]: "oid_of ≡ ecu2⇩o⇩i⇩d"
      instance ..
    end

    instantiation 𝔄 :: object
    begin
      definition oid⇩𝔄[code_unfold]:
        "oid_of x ≡
            (case x of
              in⇩C⇩a⇩r⇩1 car⇩1 ⇒ car1⇩o⇩i⇩d car⇩1 |
              in⇩C⇩a⇩r⇩2 car⇩2 ⇒ car2⇩o⇩i⇩d car⇩2 |
              in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 mb⇩1 ⇒ mb1⇩o⇩i⇩d mb⇩1 |
              in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 mb⇩2 ⇒ mb2⇩o⇩i⇩d mb⇩2 |
              in⇩E⇩C⇩U⇩2 ecu2 ⇒ ecu2⇩o⇩i⇩d ecu2)"
      instance ..
    end

    lemma singleton_set_size:
      fixes
        τ :: "𝔄 st" and
        a :: "'a"
      shows "Set{λ (_ :: 𝔄 st). ⌊⌊a⌋⌋}->size⇩S⇩e⇩t() τ = 𝟭 τ"
    proof -
      let ?set = "⌈⌈Rep_Set⇩b⇩a⇩s⇩e (Set{λ (_ :: 𝔄 st). ⌊⌊a⌋⌋} τ)⌉⌉"
      have
        "?set = {⌊⌊a⌋⌋}" and
        "card ?set = 1"
        by (simp_all add: OclIncluding_rep_set mtSet_rep_set)
      thus ?thesis
        unfolding UML_Set.OclSize_def OclInt1_def
        by simp
    qed

    subsection ‹Instantiation of Strict Equality›

    overloading StrictRefEq ≡ "StrictRefEq :: [Car1, Car1] ⇒ Boolean"
    begin
      definition StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[code_unfold]:
        "(x::Car1) ≐ y ≡ StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y"
    end
    overloading StrictRefEq ≡ "StrictRefEq :: [MessageBus1, MessageBus1] ⇒ Boolean"
    begin
      definition StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1[code_unfold]:
        "(x::MessageBus1) ≐ y ≡ StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y"
    end
    overloading StrictRefEq ≡ "StrictRefEq :: [Car2, Car2] ⇒ Boolean"
    begin
      definition StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩2[code_unfold]:
        "(x::Car2) ≐ y ≡ StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y"
    end
    overloading StrictRefEq ≡ "StrictRefEq :: [MessageBus2, MessageBus2] ⇒ Boolean"
    begin
      definition StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2[code_unfold]:
        "(x::MessageBus2) ≐ y ≡ StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y"
    end
    overloading StrictRefEq ≡ "StrictRefEq :: [ECU2, ECU2] ⇒ Boolean"
    begin
      definition StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩E⇩C⇩U⇩2[code_unfold]:
        "(x::ECU2) ≐ y ≡ StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y"
    end

    lemmas cps23 =
        cp_StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t[of "x::Car1" "y::Car1" "τ::𝔄 st",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[symmetric]]
        cp_intro(9)      [of "C::Car1 ⇒ Car1" "D::Car1 ⇒ Car1",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[symmetric] ]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_def     [of "x::Car1" "y::Car1", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_defargs [of _ "x::Car1" "y::Car1", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict1 [of "x::Car1", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict2 [of "x::Car1", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[symmetric]]
        cp_StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t[of "x::Car1" "y::Car1" "τ::𝔄 st",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1[symmetric]]
        cp_StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t[of "x::MessageBus1" "y::MessageBus1" "τ::𝔄 st",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1[symmetric]]
        cp_intro(9)      [of "C::MessageBus1 ⇒ MessageBus1"
                            "D::MessageBus1 ⇒ MessageBus1",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1[symmetric] ]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_def     [of "x::MessageBus1" "y::MessageBus1",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_defargs [of _ "x::MessageBus1" "y::MessageBus1",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict1 [of "x::MessageBus1", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict2 [of "x::MessageBus1", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1[symmetric]]
        cp_StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t[of "x::MessageBus1" "y::MessageBus1" "τ::𝔄 st",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1[symmetric]]
        cp_intro(9)      [of "C::Car2 ⇒ Car2" "D::Car2 ⇒ Car2",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩2[symmetric] ]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_def     [of "x::Car2" "y::Car2", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩2[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_defargs [of _ "x::Car2" "y::Car2", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩2[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict1 [of "x::Car2", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩2[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict2 [of "x::Car2", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩2[symmetric]]
        cp_StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t[of "x::MessageBus2" "y::MessageBus2" "τ::𝔄 st",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2[symmetric]]
        cp_intro(9)      [of "C::MessageBus2 ⇒ MessageBus2"
                            "D::MessageBus2 ⇒ MessageBus2",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2[symmetric] ]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_def     [of "x::MessageBus2" "y::MessageBus2",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_defargs [of _ "x::MessageBus2" "y::MessageBus2",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict1 [of "x::MessageBus2", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict2 [of "x::MessageBus2", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2[symmetric]]
        cp_StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t[of "x::MessageBus2" "y::MessageBus2" "τ::𝔄 st",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2[symmetric]]
        cp_StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t[of "x::ECU2" "y::ECU2" "τ::𝔄 st",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩E⇩C⇩U⇩2[symmetric]]
        cp_intro(9)      [of "C::ECU2 ⇒ ECU2" "D::ECU2 ⇒ ECU2",
                        simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩E⇩C⇩U⇩2[symmetric] ]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_def     [of "x::ECU2" "y::ECU2", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩E⇩C⇩U⇩2[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_defargs [of _ "x::ECU2" "y::ECU2", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩E⇩C⇩U⇩2[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict1 [of "x::ECU2", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩E⇩C⇩U⇩2[symmetric]]
        StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_strict2 [of "x::ECU2", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩E⇩C⇩U⇩2[symmetric]]
        cp_StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t
                      [of "x::ECU2" "y::ECU2" "τ::𝔄 st", simplified StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩E⇩C⇩U⇩2[symmetric]]
      for x y τ C D

    subsection ‹OCL Usage: OclAsType›

    consts OclAsType⇩C⇩a⇩r⇩1       :: "'α ⇒ Car1" ("(_) .oclAsType'(Car1')")
    consts OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 :: "'α ⇒ MessageBus1" ("(_) .oclAsType'(MessageBus1')")
    consts OclAsType⇩C⇩a⇩r⇩2       :: "'α ⇒ Car2" ("(_) .oclAsType'(Car2')")
    consts OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 :: "'α ⇒ MessageBus2" ("(_) .oclAsType'(MessageBus2')")
    consts OclAsType⇩E⇩C⇩U⇩2      :: "'α ⇒ ECU2" ("(_) .oclAsType'(ECU2')")

    definition OclAsType⇩C⇩a⇩r⇩1_𝔄 :: "𝔄 ⇒ ⟨𝒯⇩C⇩a⇩r⇩1⟩⇩⊥" where
      "OclAsType⇩C⇩a⇩r⇩1_𝔄 ≡
        (λ u::𝔄. ⌊case u of in⇩C⇩a⇩r⇩1 (v::𝒯⇩C⇩a⇩r⇩1) ⇒ v⌋)"
    definition OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_𝔄 :: "𝔄 ⇒ ⟨𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1⟩⇩⊥" where
      "OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_𝔄 ≡
        (λ u::𝔄. ⌊case u of in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 (v::𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1) ⇒ v⌋)"
    definition OclAsType⇩C⇩a⇩r⇩2_𝔄 :: "𝔄 ⇒ ⟨𝒯⇩C⇩a⇩r⇩2⟩⇩⊥" where
      "OclAsType⇩C⇩a⇩r⇩2_𝔄 ≡
        (λ u::𝔄. ⌊case u of in⇩C⇩a⇩r⇩2 (v::𝒯⇩C⇩a⇩r⇩2) ⇒ v⌋)"
    definition OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_𝔄 :: "𝔄 ⇒ ⟨𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2⟩⇩⊥" where
      "OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_𝔄 ≡
        (λ u::𝔄. ⌊case u of in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 (v::𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2) ⇒ v⌋)"
    definition OclAsType⇩E⇩C⇩U⇩2_𝔄 :: "𝔄 ⇒ ⟨𝒯⇩E⇩C⇩U⇩2⟩⇩⊥" where
      "OclAsType⇩E⇩C⇩U⇩2_𝔄 ≡
        (λ u::𝔄. ⌊case u of in⇩E⇩C⇩U⇩2 (v::𝒯⇩E⇩C⇩U⇩2) ⇒ v⌋)"

    lemmas [simp] =
      OclAsType⇩C⇩a⇩r⇩1_𝔄_def
      OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_𝔄_def
      OclAsType⇩C⇩a⇩r⇩2_𝔄_def
      OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_𝔄_def
      OclAsType⇩E⇩C⇩U⇩2_𝔄_def

    lemma OclAsType⇩C⇩a⇩r⇩1_𝔄_some:
      fixes x :: "𝔄"
      shows "OclAsType⇩C⇩a⇩r⇩1_𝔄 x ≠ None"
      by simp
    lemma OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_𝔄_some:
      fixes x :: "𝔄"
      shows "OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_𝔄 x ≠ None"
      by simp
    lemma OclAsType⇩C⇩a⇩r⇩2_𝔄_some:
      fixes x :: "𝔄"
      shows "OclAsType⇩C⇩a⇩r⇩2_𝔄 x ≠ None"
      by simp
    lemma OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_𝔄_some:
      fixes x :: "𝔄"
      shows "OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_𝔄 x ≠ None"
      by simp
    lemma OclAsType⇩E⇩C⇩U⇩2_𝔄_some:
      fixes x :: "𝔄"
      shows "OclAsType⇩E⇩C⇩U⇩2_𝔄 x ≠ None"
      by simp

    overloading OclAsType⇩C⇩a⇩r⇩1 ≡ "OclAsType⇩C⇩a⇩r⇩1 :: Car1 ⇒ Car1"
    begin
      definition OclAsType⇩C⇩a⇩r⇩1_Car1[code_unfold]:
        "(X::Car1) .oclAsType(Car1) ≡ X"
    end
    overloading OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 ≡ "OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 ::
                                        MessageBus1 ⇒ MessageBus1"
    begin
      definition OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1[code_unfold]:
        "(X::MessageBus1) .oclAsType(MessageBus1) ≡ X"
    end
    overloading OclAsType⇩C⇩a⇩r⇩2 ≡ "OclAsType⇩C⇩a⇩r⇩2 :: Car2 ⇒ Car2"
    begin
      definition OclAsType⇩C⇩a⇩r⇩2_Car2[code_unfold]:
        "(X::Car2) .oclAsType(Car2) ≡ X"
    end
    overloading OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 ≡ "OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 ::
                                        MessageBus2 ⇒ MessageBus2"
    begin
      definition OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2[code_unfold]:
        "(X::MessageBus2) .oclAsType(MessageBus2) ≡ X"
    end
    overloading OclAsType⇩E⇩C⇩U⇩2 ≡ "OclAsType⇩E⇩C⇩U⇩2 :: ECU2 ⇒ ECU2"
    begin
      definition OclAsType⇩E⇩C⇩U⇩2_ECU2[code_unfold]:
        "(X::ECU2) .oclAsType(ECU2) ≡ X"
    end

    lemmas [simp] =
      OclAsType⇩C⇩a⇩r⇩1_Car1 OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1
      OclAsType⇩C⇩a⇩r⇩2_Car2 OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2
      OclAsType⇩E⇩C⇩U⇩2_ECU2

    lemma OclAsType⇩C⇩a⇩r⇩1_Car1_strict: "(invalid::Car1) .oclAsType(Car1) = invalid"
      by simp
    lemma OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1_strict:
      "(invalid::MessageBus1) .oclAsType(MessageBus1) = invalid"
      by simp
    lemma OclAsType⇩C⇩a⇩r⇩2_Car2_strict: "(invalid::Car2) .oclAsType(Car2) = invalid"
      by simp
    lemma OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2_strict:
      "(invalid::MessageBus2) .oclAsType(MessageBus2) = invalid"
      by simp
    lemma OclAsType⇩E⇩C⇩U⇩2_ECU2_strict: "(invalid::ECU2) .oclAsType(ECU2) = invalid"
      by simp

    lemma OclAsType⇩C⇩a⇩r⇩1_Car1_nullstrict: "(null::Car1) .oclAsType(Car1) = null"
      by simp
    lemma OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1_nullstrict:
      "(null::MessageBus1) .oclAsType(MessageBus1) = null"
      by simp
    lemma OclAsType⇩C⇩a⇩r⇩2_Car2_nullstrict: "(null::Car2) .oclAsType(Car2) = null"
      by simp
    lemma OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2_nullstrict:
      "(null::MessageBus2) .oclAsType(MessageBus2) = null"
      by simp
    lemma OclAsType⇩E⇩C⇩U⇩2_ECU2_nullstrict: "(null::ECU2) .oclAsType(ECU2) = null"
      by simp

    subsection ‹OCL Usage: OclIsTypeOf›

    consts OclIsTypeOf⇩C⇩a⇩r⇩1      :: "'α ⇒ Boolean" ("(_).oclIsTypeOf'(Car1')")
    consts OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 :: "'α ⇒ Boolean" ("(_).oclIsTypeOf'(MessageBus1')")
    consts OclIsTypeOf⇩C⇩a⇩r⇩2      :: "'α ⇒ Boolean" ("(_).oclIsTypeOf'(Car2')")
    consts OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 :: "'α ⇒ Boolean" ("(_).oclIsTypeOf'(MessageBus2')")
    consts OclIsTypeOf⇩E⇩C⇩U⇩2      :: "'α ⇒ Boolean" ("(_).oclIsTypeOf'(ECU2')")

    overloading OclIsTypeOf⇩C⇩a⇩r⇩1 ≡ "OclIsTypeOf⇩C⇩a⇩r⇩1 :: Car1 ⇒ Boolean"
    begin
      definition OclIsTypeOf⇩C⇩a⇩r⇩1_Car1[code_unfold]:
          "(X::Car1) .oclIsTypeOf(Car1) ≡ (λ τ :: (𝔄 st).
                  case X τ of
                    ⊥ ⇒ invalid τ |
                    _ ⇒ true τ)"
    end
    overloading OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 ≡ "OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 :: MessageBus1 ⇒ Boolean"
    begin
      definition OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1[code_unfold]:
          "(X::MessageBus1) .oclIsTypeOf(MessageBus1) ≡ (λ τ :: (𝔄 st).
                case X τ of
                  ⊥ ⇒ invalid τ |
                  _ ⇒ true τ)"
    end
    overloading OclIsTypeOf⇩C⇩a⇩r⇩2 ≡ "OclIsTypeOf⇩C⇩a⇩r⇩2 :: Car2 ⇒ Boolean"
    begin
      definition OclIsTypeOf⇩C⇩a⇩r⇩2_Car2[code_unfold]:
          "(X::Car2) .oclIsTypeOf(Car2) ≡ (λ τ :: (𝔄 st).
                  case X τ of
                    ⊥ ⇒ invalid τ |
                    _ ⇒ true τ)"
    end
    overloading OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 ≡ "OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 :: MessageBus2 ⇒ Boolean"
    begin
      definition OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2[code_unfold]:
          "(X::MessageBus2) .oclIsTypeOf(MessageBus2) ≡ (λ τ :: (𝔄 st).
                case X τ of
                  ⊥ ⇒ invalid τ |
                  _ ⇒ true τ)"
    end
    overloading OclIsTypeOf⇩E⇩C⇩U⇩2 ≡ "OclIsTypeOf⇩E⇩C⇩U⇩2 :: ECU2 ⇒ Boolean"
    begin
      definition OclIsTypeOf⇩E⇩C⇩U⇩2_ECU2[code_unfold]:
          "(X::ECU2) .oclIsTypeOf(ECU2) ≡ (λ τ :: (𝔄 st).
                case X τ of
                  ⊥ ⇒ invalid τ |
                  _ ⇒ true τ)"
    end

    lemma OclIsTypeOf⇩C⇩a⇩r⇩1_Car1':
      fixes X :: "Car1"
      shows "X .oclIsTypeOf(Car1) = (λ τ :: (𝔄 st).
                if τ ⊨ υ X
                then case X τ of
                        ⊥ ⇒ invalid τ |
                        _ ⇒ true τ
                else invalid τ)"
      unfolding OclIsTypeOf⇩C⇩a⇩r⇩1_Car1 foundation18' bot_option_def
      by (rule ext, simp)
    lemma OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1':
      fixes X :: "MessageBus1"
      shows "X .oclIsTypeOf(MessageBus1) = (λ τ :: (𝔄 st).
                if τ ⊨ υ X
                then case X τ of
                        ⊥ ⇒ invalid τ |
                        _ ⇒ true τ
                else invalid τ)"
      unfolding OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1 foundation18' bot_option_def
      by (rule ext, simp)

    lemma OclIsTypeOf⇩C⇩a⇩r⇩2_Car2':
      fixes X :: "Car2"
      shows "X .oclIsTypeOf(Car2) = (λ τ :: (𝔄 st).
                if τ ⊨ υ X
                then case X τ of
                        ⊥ ⇒ invalid τ |
                        _ ⇒ true τ
                else invalid τ)"
      unfolding OclIsTypeOf⇩C⇩a⇩r⇩2_Car2 foundation18' bot_option_def
      by (rule ext, simp)
    lemma OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2':
      fixes X :: "MessageBus2"
      shows "X .oclIsTypeOf(MessageBus2) = (λ τ :: (𝔄 st).
                if τ ⊨ υ X
                then case X τ of
                        ⊥ ⇒ invalid τ |
                        _ ⇒ true τ
                else invalid τ)"
      unfolding OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2 foundation18' bot_option_def
      by (rule ext, simp)

    lemma OclIsTypeOf⇩E⇩C⇩U⇩2_ECU2':
      fixes X :: "ECU2"
      shows "(X .oclIsTypeOf(ECU2)) = (λ τ :: (𝔄 st).
                if (τ ⊨ υ X)
                then case X τ of
                        ⊥ ⇒ invalid τ |
                        _ ⇒ true τ
                else invalid τ)"
      unfolding OclIsTypeOf⇩E⇩C⇩U⇩2_ECU2 foundation18' bot_option_def
      by (rule ext, simp)

    interpretation OclIsTypeOf⇩C⇩a⇩r⇩1_Car1:
        profile_mono_schemeV
        "OclIsTypeOf⇩C⇩a⇩r⇩1::Car1 ⇒ Boolean"
        "λ _::(⟨⟨𝒯⇩C⇩a⇩r⇩1⟩⇩⊥⟩⇩⊥). ⌊⌊True⌋⌋"
    proof (unfold_locales, unfold OclIsTypeOf⇩C⇩a⇩r⇩1_Car1' OclValid_def true_def,
            simp add: atomize_eq, rule ext)
      fix
        x :: "Car1" and
        τ :: "𝔄 st"
      show "(if (υ x) τ = ⌊⌊True⌋⌋ then case x τ of
              ⊥ ⇒ invalid τ |
              ⌊a::(⟨𝒯⇩C⇩a⇩r⇩1⟩⇩⊥)⌋ ⇒ ⌊⌊True⌋⌋ else invalid τ) =
                                  (if (υ x) τ = ⌊⌊True⌋⌋ then ⌊⌊True⌋⌋ else invalid τ)"
        by (auto split: option.split,
            metis OclValid_def bot_option_def foundation18' true_def)
    qed

    interpretation OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1:
        profile_mono_schemeV
        "OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1::MessageBus1 ⇒ Boolean"
        "λ _::(⟨⟨𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1⟩⇩⊥⟩⇩⊥). ⌊⌊True⌋⌋"
    proof (unfold_locales, unfold OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1'
                            OclValid_def true_def,
            simp add: atomize_eq, rule ext)
      fix
        x :: "MessageBus1" and
        τ :: "𝔄 st"
      show "(if (υ x) τ = ⌊⌊True⌋⌋ then case x τ of
              ⊥ ⇒ invalid τ |
              ⌊a::(⟨𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1⟩⇩⊥)⌋ ⇒ ⌊⌊True⌋⌋ else invalid τ) =
                                        (if (υ x) τ = ⌊⌊True⌋⌋ then ⌊⌊True⌋⌋ else invalid τ)"
        by (auto split: option.split,
            metis OclValid_def bot_option_def foundation18' true_def)
    qed

    interpretation OclIsTypeOf⇩C⇩a⇩r⇩2_Car2:
        profile_mono_schemeV
        "OclIsTypeOf⇩C⇩a⇩r⇩2::Car2 ⇒ Boolean"
        "λ _::(⟨⟨𝒯⇩C⇩a⇩r⇩2⟩⇩⊥⟩⇩⊥). ⌊⌊True⌋⌋"
    proof (unfold_locales, unfold OclIsTypeOf⇩C⇩a⇩r⇩2_Car2' OclValid_def true_def false_def,
            simp add: atomize_eq, rule ext)
      fix
        x :: "Car2" and
        τ :: "𝔄 st"
      show "(if (υ x) τ = ⌊⌊True⌋⌋ then case x τ of
              ⊥ ⇒ invalid τ |
              ⌊a::(⟨𝒯⇩C⇩a⇩r⇩2⟩⇩⊥)⌋ ⇒ ⌊⌊True⌋⌋ else invalid τ) =
                                  (if (υ x) τ = ⌊⌊True⌋⌋ then ⌊⌊True⌋⌋ else invalid τ)"
        by (auto split: option.split,
            metis OclValid_def bot_option_def foundation18' true_def)
    qed

    interpretation OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2:
        profile_mono_schemeV
        "OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2::MessageBus2 ⇒ Boolean"
        "λ _::(⟨⟨𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2⟩⇩⊥⟩⇩⊥). ⌊⌊True⌋⌋"
    proof (unfold_locales, unfold OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2'
                              OclValid_def true_def false_def,
            simp add: atomize_eq, rule ext)
      fix
        x :: "MessageBus2" and
        τ :: "𝔄 st"
      show "(if (υ x) τ = ⌊⌊True⌋⌋ then case x τ of
              ⊥ ⇒ invalid τ |
              ⌊a::(⟨𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2⟩⇩⊥)⌋ ⇒ ⌊⌊True⌋⌋ else invalid τ) =
                                        (if (υ x) τ = ⌊⌊True⌋⌋ then ⌊⌊True⌋⌋ else invalid τ)"
        by (auto split: option.split,
            metis OclValid_def bot_option_def foundation18' true_def)
    qed

    interpretation OclIsTypeOf⇩E⇩C⇩U⇩2_ECU2:
        profile_mono_schemeV
        "OclIsTypeOf⇩E⇩C⇩U⇩2::ECU2 ⇒ Boolean"
        "λ _::(⟨⟨𝒯⇩E⇩C⇩U⇩2⟩⇩⊥⟩⇩⊥). ⌊⌊True⌋⌋"
    proof (unfold_locales, unfold OclIsTypeOf⇩E⇩C⇩U⇩2_ECU2' OclValid_def true_def false_def,
            simp add: atomize_eq, rule ext)
      fix
        x :: "ECU2" and
        τ :: "𝔄 st"
      show "(if (υ x) τ = ⌊⌊True⌋⌋ then case x τ of
              ⊥ ⇒ invalid τ |
              ⌊a::(⟨𝒯⇩E⇩C⇩U⇩2⟩⇩⊥)⌋ ⇒ ⌊⌊True⌋⌋ else invalid τ) =
                                  (if (υ x) τ = ⌊⌊True⌋⌋ then ⌊⌊True⌋⌋ else invalid τ)"
        by (auto split: option.split,
            metis OclValid_def bot_option_def foundation18' true_def)
    qed

    lemma cp_OclIsTypeOf⇩C⇩a⇩r⇩1_Car1_Car1:
      fixes P :: "Car1 ⇒ Car1"
      shows "cp P ⟹ cp(λ X::Car1. ((P X) .oclIsTypeOf(Car1)))"
      using OclIsTypeOf⇩C⇩a⇩r⇩1_Car1.cp
      by simp
    lemma cp_OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1_MessageBus1:
      fixes P :: "MessageBus1 ⇒ MessageBus1"
      shows "cp P ⟹ cp(λ X::MessageBus1. ((P X) .oclIsTypeOf(MessageBus1)))"
      using OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1.cp
      by simp

    lemma cp_OclIsTypeOf⇩C⇩a⇩r⇩2_Car2_Car2:
      fixes P :: "Car2 ⇒ Car2"
      shows "cp P ⟹ cp(λ X::Car2. ((P X) .oclIsTypeOf(Car2)))"
      using OclIsTypeOf⇩C⇩a⇩r⇩2_Car2.cp
      by simp
    lemma cp_OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2_MessageBus2:
      fixes P :: "MessageBus2 ⇒ MessageBus2"
      shows "cp P ⟹ cp(λ X::MessageBus2. ((P X) .oclIsTypeOf(MessageBus2)))"
      using OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2.cp
      by simp

    lemma cp_OclIsTypeOf⇩E⇩C⇩U⇩2_ECU2_ECU2:
      fixes P :: "ECU2 ⇒ ECU2"
      shows "cp P ⟹ cp(λ X::ECU2. ((P X) .oclIsTypeOf(ECU2)))"
      using OclIsTypeOf⇩E⇩C⇩U⇩2_ECU2.cp
      by simp

    lemmas [simp] =
      cp_OclIsTypeOf⇩C⇩a⇩r⇩1_Car1_Car1 cp_OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1_MessageBus1
      cp_OclIsTypeOf⇩C⇩a⇩r⇩2_Car2_Car2 cp_OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2_MessageBus2
      cp_OclIsTypeOf⇩E⇩C⇩U⇩2_ECU2_ECU2

    lemma OclIsTypeOf⇩C⇩a⇩r⇩1_Car1_strict1[simp]:
      "(invalid::Car1) .oclIsTypeOf(Car1) = invalid"
      by (rule OclIsTypeOf⇩C⇩a⇩r⇩1_Car1.strict)
    lemma OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1_strict1[simp]:
      "(invalid::MessageBus1) .oclIsTypeOf(MessageBus1) = invalid"
      by (rule OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1.strict)

    lemma OclIsTypeOf⇩C⇩a⇩r⇩2_Car2_strict1[simp]:
      "(invalid::Car2) .oclIsTypeOf(Car2) = invalid"
      by (rule OclIsTypeOf⇩C⇩a⇩r⇩2_Car2.strict)
    lemma OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2_strict1[simp]:
      "(invalid::MessageBus2) .oclIsTypeOf(MessageBus2) = invalid"
      by (rule OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2.strict)

    lemma OclIsTypeOf⇩E⇩C⇩U⇩2_ECU2_strict1[simp]:
      "(invalid::ECU2) .oclIsTypeOf(ECU2) = invalid"
      by (rule OclIsTypeOf⇩E⇩C⇩U⇩2_ECU2.strict)

    lemma OclIsTypeOf⇩C⇩a⇩r⇩1_Car1_strict2[simp]:
      "(null::Car1) .oclIsTypeOf(Car1) = true"
      unfolding OclIsTypeOf⇩C⇩a⇩r⇩1_Car1 null_fun_def null_option_def
      by simp
    lemma OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1_strict2[simp]:
      "(null::MessageBus1) .oclIsTypeOf(MessageBus1) = true"
      unfolding OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1 null_fun_def null_option_def
      by simp

    lemma OclIsTypeOf⇩C⇩a⇩r⇩2_Car2_strict2[simp]:
      "(null::Car2) .oclIsTypeOf(Car2) = true"
      unfolding OclIsTypeOf⇩C⇩a⇩r⇩2_Car2 null_fun_def null_option_def
      by simp
    lemma OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2_strict2[simp]:
      "(null::MessageBus2) .oclIsTypeOf(MessageBus2) = true"
      unfolding OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2 null_fun_def null_option_def
      by simp

    lemma OclIsTypeOf⇩E⇩C⇩U⇩2_ECU2_strict2[simp]:
      "(null::ECU2) .oclIsTypeOf(ECU2) = true"
      unfolding OclIsTypeOf⇩E⇩C⇩U⇩2_ECU2 null_fun_def null_option_def
      by simp

    subsection ‹OCL Usage: OclIsKindOf›

    text ‹A couple of general heap accessors›

    definition pre⇩s⇩t⇩a⇩t⇩e :: "'𝔄 × '𝔅 ⇒ '𝔄" where
      "pre⇩s⇩t⇩a⇩t⇩e ≡ fst"

    definition post⇩s⇩t⇩a⇩t⇩e :: "'𝔄 × '𝔅 ⇒ '𝔅" where
      "post⇩s⇩t⇩a⇩t⇩e ≡ snd"

    definition reconst⇩𝒯⇩_⇩b⇩a⇩s⇩e :: "('τ ⇒ 𝔄 st ⇒ ⟨⟨'τ⟩⇩⊥⟩⇩⊥) ⇒ 'τ ⇒ 𝔄 st ⇒ ⟨⟨'τ⟩⇩⊥⟩⇩⊥" where
      "reconst⇩𝒯⇩_⇩b⇩a⇩s⇩e ≡ (λ (convert :: 'τ ⇒ 𝔄 st ⇒ ⟨⟨'τ⟩⇩⊥⟩⇩⊥) (τ::'τ). convert τ)"

    definition list⇩f⇩l⇩a⇩t⇩t⇩e⇩n :: "oid list list ⇒ oid list" where
      "list⇩f⇩l⇩a⇩t⇩t⇩e⇩n ≡ (λ ls⇩1 :: oid list list.
          foldl (λ oids⇩1 :: _ list.
            (λ ls⇩2 :: _ list. foldl (λ oids⇩2 :: _ list. (λ l :: _. Cons l oids⇩2)) oids⇩1 (rev ls⇩2)))
              Nil (rev ls⇩1))"

    definition switch⇩2_1 :: "'α list ⇒ 'α × 'α" where
      "switch⇩2_1 = (λ [x, y]    ⇒ (x, y))"
    definition switch⇩2_2 :: "'α list ⇒ 'α × 'α" where
      "switch⇩2_2 = (λ [x, y]    ⇒ (y, x))"
    definition switch⇩3_1 :: "'α list ⇒ 'α × 'α" where
      "switch⇩3_1 = (λ [x, y, z] ⇒ (x, y))"
    definition switch⇩3_2 :: "'α list ⇒ 'α × 'α" where
      "switch⇩3_2 = (λ [x, y, z] ⇒ (x, z))"
    definition switch⇩3_3 :: "'α list ⇒ 'α × 'α" where
      "switch⇩3_3 = (λ [x, y, z] ⇒ (y, x))"
    definition switch⇩3_4 :: "'α list ⇒ 'α × 'α" where
      "switch⇩3_4 = (λ [x, y, z] ⇒ (y, z))"
    definition switch⇩3_5 :: "'α list ⇒ 'α × 'α" where
      "switch⇩3_5 = (λ [x, y ,z] ⇒ (z, x))"
    definition switch⇩3_6 :: "'α list ⇒ 'α × 'α" where
      "switch⇩3_6 = (λ [x, y, z] ⇒ (z, y))"

    subsubsection ‹OclIsKindOf›

    consts OclIsKindOf⇩C⇩a⇩r⇩1       :: "'α ⇒ Boolean" ("(_).oclIsKindOf'(Car1')")
    consts OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 :: "'α ⇒ Boolean" ("(_).oclIsKindOf'(MessageBus1')")
    consts OclIsKindOf⇩C⇩a⇩r⇩2       :: "'α ⇒ Boolean" ("(_).oclIsKindOf'(Car2')")
    consts OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 :: "'α ⇒ Boolean" ("(_).oclIsKindOf'(MessageBus2')")
    consts OclIsKindOf⇩E⇩C⇩U⇩2      :: "'α ⇒ Boolean" ("(_).oclIsKindOf'(ECU2')")

    overloading OclIsKindOf⇩C⇩a⇩r⇩1 ≡ "OclIsKindOf⇩C⇩a⇩r⇩1 :: Car1 ⇒ Boolean"
    begin
      definition OclIsKindOf⇩C⇩a⇩r⇩1_Car1[code_unfold]:
          "(X::Car1) .oclIsKindOf(Car1) ≡ (λ τ :: (𝔄 st).
                case X τ of
                  ⊥ ⇒ invalid τ |
                  _ ⇒ true τ)"
    end
    overloading OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 ≡ "OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 :: MessageBus1 ⇒ Boolean"
    begin
      definition OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1[code_unfold]:
          "(X::MessageBus1) .oclIsKindOf(MessageBus1) ≡ (λ τ :: (𝔄 st).
                case X τ of
                  ⊥ ⇒ invalid τ |
                  _ ⇒ true τ)"
    end
    overloading OclIsKindOf⇩C⇩a⇩r⇩2 ≡ "OclIsKindOf⇩C⇩a⇩r⇩2 :: Car2 ⇒ Boolean"
    begin
      definition OclIsKindOf⇩C⇩a⇩r⇩2_Car2[code_unfold]:
          "(X::Car2) .oclIsKindOf(Car2) ≡ (λ τ :: (𝔄 st).
                case X τ of
                  ⊥ ⇒ invalid τ |
                  _ ⇒ true τ)"
    end
    overloading OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 ≡ "OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 ::
                                            MessageBus2 ⇒ Boolean"
    begin
      definition OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2[code_unfold]:
          "(X::MessageBus2) .oclIsKindOf(MessageBus2) ≡ (λ τ :: (𝔄 st).
                case X τ of
                  ⊥ ⇒ invalid τ |
                  _ ⇒ true τ)"
    end
    overloading OclIsKindOf⇩E⇩C⇩U⇩2 ≡ "OclIsKindOf⇩E⇩C⇩U⇩2 :: ECU2 ⇒ Boolean"
    begin
      definition OclIsKindOf⇩E⇩C⇩U⇩2_ECU2[code_unfold]:
          "(X::ECU2) .oclIsKindOf(ECU2) ≡ (λ τ :: (𝔄 st).
                case X τ of
                  ⊥ ⇒ invalid τ |
                  _ ⇒ true τ)"
    end

    lemma cp_OclIsKindOf⇩C⇩a⇩r⇩1_Car1_Car1:
      fixes P :: "Car1 ⇒ Car1"
      shows "cp P ⟹ cp(λ X::Car1. ((P X) .oclIsKindOf(Car1)))"
      unfolding OclIsKindOf⇩C⇩a⇩r⇩1_Car1
      by (rule cpI1, safe)
    lemma cp_OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1_MessageBus1:
      fixes P :: "MessageBus1 ⇒ MessageBus1"
      shows "cp P ⟹ cp(λ X::MessageBus1. ((P X) .oclIsKindOf(MessageBus1)))"
      unfolding OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1
      by (rule cpI1, safe)
    lemma cp_OclIsKindOf⇩C⇩a⇩r⇩2_Car2_Car2:
      fixes P :: "Car2 ⇒ Car2"
      shows "cp P ⟹ cp(λ X::Car2. ((P X) .oclIsKindOf(Car2)))"
      unfolding OclIsKindOf⇩C⇩a⇩r⇩2_Car2
      by (rule cpI1, safe)
    lemma cp_OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2_MessageBus2:
      fixes P :: "MessageBus2 ⇒ MessageBus2"
      shows "cp P ⟹ cp(λ X::MessageBus2. ((P X) .oclIsKindOf(MessageBus2)))"
      unfolding OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2
      by (rule cpI1, safe)
    lemma cp_OclIsKindOf⇩E⇩C⇩U⇩2_ECU2_ECU2:
      fixes P :: "ECU2 ⇒ ECU2"
      shows "cp P ⟹ cp(λ X::ECU2. ((P X) .oclIsKindOf(ECU2)))"
      unfolding OclIsKindOf⇩E⇩C⇩U⇩2_ECU2
      by (rule cpI1, safe)

    lemmas [simp] =
      cp_OclIsKindOf⇩C⇩a⇩r⇩1_Car1_Car1 cp_OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1_MessageBus1
      cp_OclIsKindOf⇩C⇩a⇩r⇩2_Car2_Car2 cp_OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2_MessageBus2
      cp_OclIsKindOf⇩E⇩C⇩U⇩2_ECU2_ECU2

    lemma OclIsKindOf⇩C⇩a⇩r⇩1_Car1_strict1[simp]:
      "(invalid::Car1) .oclIsKindOf(Car1) = invalid"
      unfolding invalid_def bot_option_def OclIsKindOf⇩C⇩a⇩r⇩1_Car1
      by simp
    lemma OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1_strict1[simp]: "(invalid::MessageBus1)
                                                            .oclIsKindOf(MessageBus1) = invalid"
      unfolding invalid_def bot_option_def OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1
      by simp
    lemma OclIsKindOf⇩C⇩a⇩r⇩2_Car2_strict1[simp]:
      "(invalid::Car2) .oclIsKindOf(Car2) = invalid"
      unfolding invalid_def bot_option_def OclIsKindOf⇩C⇩a⇩r⇩2_Car2
      by simp
    lemma OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2_strict1[simp]:
      "(invalid::MessageBus2) .oclIsKindOf(MessageBus2) = invalid"
      unfolding invalid_def bot_option_def OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2
      by simp
    lemma OclIsKindOf⇩E⇩C⇩U⇩2_ECU2_strict1[simp]:
      "(invalid::ECU2) .oclIsKindOf(ECU2) = invalid"
      unfolding invalid_def bot_option_def OclIsKindOf⇩E⇩C⇩U⇩2_ECU2
      by simp

    lemma OclIsKindOf⇩C⇩a⇩r⇩1_Car1_strict2[simp]:
      "(null::Car1) .oclIsKindOf(Car1) = true"
      unfolding null_fun_def null_option_def OclIsKindOf⇩C⇩a⇩r⇩1_Car1
      by simp
    lemma OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1_strict2[simp]:
      "(null::MessageBus1) .oclIsKindOf(MessageBus1) = true"
      unfolding null_fun_def null_option_def OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1
      by simp
    lemma OclIsKindOf⇩C⇩a⇩r⇩2_Car2_strict2[simp]:
      "(null::Car2) .oclIsKindOf(Car2) = true"
      unfolding null_fun_def null_option_def OclIsKindOf⇩C⇩a⇩r⇩2_Car2
      by simp
    lemma OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2_strict2[simp]:
      "(null::MessageBus2) .oclIsKindOf(MessageBus2) = true"
      unfolding null_fun_def null_option_def OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2
      by simp
    lemma OclIsKindOf⇩E⇩C⇩U⇩2_ECU2_strict2[simp]:
      "(null::ECU2) .oclIsKindOf(ECU2) = true"
      unfolding null_fun_def null_option_def OclIsKindOf⇩E⇩C⇩U⇩2_ECU2
      by simp

    subsection ‹OCL Usage: OclAllInstances›

    definition Car1        :: "𝔄 ⇒ ⟨𝒯⇩C⇩a⇩r⇩1⟩⇩⊥"       where "Car1 ≡ OclAsType⇩C⇩a⇩r⇩1_𝔄"
    definition Car2        :: "𝔄 ⇒ ⟨𝒯⇩C⇩a⇩r⇩2⟩⇩⊥"       where "Car2 ≡ OclAsType⇩C⇩a⇩r⇩2_𝔄"
    definition MessageBus1 :: "𝔄 ⇒ ⟨𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1⟩⇩⊥" where "MessageBus1 ≡ OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_𝔄"
    definition MessageBus2 :: "𝔄 ⇒ ⟨𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2⟩⇩⊥" where "MessageBus2 ≡ OclAsType⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_𝔄"
    definition ECU2        :: "𝔄 ⇒ ⟨𝒯⇩E⇩C⇩U⇩2⟩⇩⊥"       where "ECU2 ≡ OclAsType⇩E⇩C⇩U⇩2_𝔄"

    lemmas [simp] =
      Car1_def MessageBus1_def
      Car2_def MessageBus2_def
      ECU2_def

    lemma OclAllInstances_generic⇩C⇩a⇩r⇩1_exec:
      fixes pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "OclAllInstances_generic pre_post Car1 =
              (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` Car1 ` ran (heap (pre_post τ))⌋⌋)"
    proof -
      let ?S1 = "λ τ :: 𝔄 st. Car1 ` ran (heap (pre_post τ))"
      let ?S2 = "λ τ :: 𝔄 st. ?S1 τ - {None}"
      have B: "⋀ τ :: 𝔄 st. ?S2 τ ⊆ ?S1 τ"
        by safe
      have "⋀ τ :: 𝔄 st. ?S1 τ ⊆ ?S2 τ"
        by force
      thus ?thesis
        by(insert equalityI [OF B], simp)
    qed
    lemma OclAllInstances_generic⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_exec:
      fixes pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "OclAllInstances_generic pre_post MessageBus1 =
              (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` MessageBus1 ` ran (heap (pre_post τ))⌋⌋)"
    proof -
      let ?S1 = "λ τ :: 𝔄 st. MessageBus1 ` ran (heap (pre_post τ))"
      let ?S2 = "λ τ :: 𝔄 st. ?S1 τ - {None}"
      have B: "⋀ τ :: 𝔄 st. ?S2 τ ⊆ ?S1 τ"
        by safe
      have "⋀ τ :: 𝔄 st. ?S1 τ ⊆ ?S2 τ"
        by force
      thus ?thesis
        by(insert equalityI [OF B], simp)
    qed

    lemma OclAllInstances_generic⇩C⇩a⇩r⇩2_exec:
      fixes pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "OclAllInstances_generic pre_post Car2 =
              (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` Car2 ` ran (heap (pre_post τ))⌋⌋)"
    proof -
      let ?S1 = "λ τ :: 𝔄 st. Car2 ` ran (heap (pre_post τ))"
      let ?S2 = "λ τ :: 𝔄 st. ?S1 τ - {None}"
      have B: "⋀ τ :: 𝔄 st. ?S2 τ ⊆ ?S1 τ"
        by safe
      have "⋀ τ :: 𝔄 st. ?S1 τ ⊆ ?S2 τ"
        by force
      thus ?thesis
        by(insert equalityI [OF B], simp)
    qed
    lemma OclAllInstances_generic⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_exec:
      fixes pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "OclAllInstances_generic pre_post MessageBus2 =
              (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` MessageBus2 ` ran (heap (pre_post τ))⌋⌋)"
    proof -
      let ?S1 = "λ τ :: 𝔄 st. MessageBus2 ` ran (heap (pre_post τ))"
      let ?S2 = "λ τ :: 𝔄 st. ?S1 τ - {None}"
      have B: "⋀ τ :: 𝔄 st. ?S2 τ ⊆ ?S1 τ"
        by safe
      have "⋀ τ :: 𝔄 st. ?S1 τ ⊆ ?S2 τ"
        by force
      thus ?thesis
        by(insert equalityI [OF B], simp)
    qed

    lemma OclAllInstances_generic⇩E⇩C⇩U⇩2_exec:
      fixes pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "OclAllInstances_generic pre_post ECU2 =
              (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` ECU2 ` ran (heap (pre_post τ))⌋⌋)"
    proof -
      let ?S1 = "λ τ :: 𝔄 st. ECU2 ` ran (heap (pre_post τ))"
      let ?S2 = "λ τ :: 𝔄 st. ?S1 τ - {None}"
      have B: "⋀ τ :: 𝔄 st. ?S2 τ ⊆ ?S1 τ"
        by safe
      have "⋀ τ :: 𝔄 st. ?S1 τ ⊆ ?S2 τ"
        by force
      thus ?thesis
        by(insert equalityI [OF B], simp)
    qed

    lemma OclAllInstances_at_post⇩C⇩a⇩r⇩1_exec: "Car1 .allInstances() =
            (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` Car1 ` ran (heap (post⇩s⇩t⇩a⇩t⇩e τ))⌋⌋)"
      unfolding OclAllInstances_at_post_def post⇩s⇩t⇩a⇩t⇩e_def
      by(rule OclAllInstances_generic⇩C⇩a⇩r⇩1_exec)
    lemma OclAllInstances_at_post⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_exec: "MessageBus1 .allInstances() =
            (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` MessageBus1 ` ran (heap (post⇩s⇩t⇩a⇩t⇩e τ))⌋⌋)"
      unfolding OclAllInstances_at_post_def post⇩s⇩t⇩a⇩t⇩e_def
      by(rule OclAllInstances_generic⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_exec)
    lemma OclAllInstances_at_post⇩C⇩a⇩r⇩2_exec: "Car2 .allInstances() =
            (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` Car2 ` ran (heap (post⇩s⇩t⇩a⇩t⇩e τ))⌋⌋)"
      unfolding OclAllInstances_at_post_def post⇩s⇩t⇩a⇩t⇩e_def
      by(rule OclAllInstances_generic⇩C⇩a⇩r⇩2_exec)
    lemma OclAllInstances_at_post⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_exec: "MessageBus2 .allInstances() =
            (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` MessageBus2 ` ran (heap (post⇩s⇩t⇩a⇩t⇩e τ))⌋⌋)"
      unfolding OclAllInstances_at_post_def post⇩s⇩t⇩a⇩t⇩e_def
      by(rule OclAllInstances_generic⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_exec)
    lemma OclAllInstances_at_post⇩E⇩C⇩U⇩2_exec: "ECU2 .allInstances() =
            (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` ECU2 ` ran (heap (post⇩s⇩t⇩a⇩t⇩e τ))⌋⌋)"
      unfolding OclAllInstances_at_post_def post⇩s⇩t⇩a⇩t⇩e_def
      by(rule OclAllInstances_generic⇩E⇩C⇩U⇩2_exec)

    lemma OclAllInstances_at_pre⇩C⇩a⇩r⇩1_exec: "Car1 .allInstances@pre() =
            (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` Car1 ` ran (heap (pre⇩s⇩t⇩a⇩t⇩e τ))⌋⌋)"
      unfolding OclAllInstances_at_pre_def pre⇩s⇩t⇩a⇩t⇩e_def
      by(rule OclAllInstances_generic⇩C⇩a⇩r⇩1_exec)
    lemma OclAllInstances_at_pre⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_exec:
      "MessageBus1 .allInstances@pre() =
            (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` MessageBus1 ` ran (heap (pre⇩s⇩t⇩a⇩t⇩e τ))⌋⌋)"
      unfolding OclAllInstances_at_pre_def pre⇩s⇩t⇩a⇩t⇩e_def
      by(rule OclAllInstances_generic⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_exec)
    lemma OclAllInstances_at_pre⇩C⇩a⇩r⇩2_exec: "Car2 .allInstances@pre() =
            (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` Car2 ` ran (heap (pre⇩s⇩t⇩a⇩t⇩e τ))⌋⌋)"
      unfolding OclAllInstances_at_pre_def pre⇩s⇩t⇩a⇩t⇩e_def
      by(rule OclAllInstances_generic⇩C⇩a⇩r⇩2_exec)
    lemma OclAllInstances_at_pre⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_exec:
      "MessageBus2 .allInstances@pre() =
            (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` MessageBus2 ` ran (heap (pre⇩s⇩t⇩a⇩t⇩e τ))⌋⌋)"
      unfolding OclAllInstances_at_pre_def pre⇩s⇩t⇩a⇩t⇩e_def
      by(rule OclAllInstances_generic⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_exec)
    lemma OclAllInstances_at_pre⇩E⇩C⇩U⇩2_exec: "ECU2 .allInstances@pre() =
            (λ τ :: 𝔄 st. Abs_Set⇩b⇩a⇩s⇩e ⌊⌊Some ` ECU2 ` ran (heap (pre⇩s⇩t⇩a⇩t⇩e τ))⌋⌋)"
      unfolding OclAllInstances_at_pre_def pre⇩s⇩t⇩a⇩t⇩e_def
      by(rule OclAllInstances_generic⇩E⇩C⇩U⇩2_exec)

    lemma Car1_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩11:
      fixes pre_post :: "𝔄 st ⇒ 𝔄 state"
      assumes [simp]: "⋀ x :: 𝔄 state. pre_post (x, x) = x"
      shows "∃ τ :: 𝔄 st.
                (τ ⊨ ((OclAllInstances_generic pre_post Car1)
                          ->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car1))))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclAllInstances_generic_def
      apply(rule_tac x = τ⇩0 in exI)
      unfolding τ⇩0_def OclValid_def
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      by simp_all

    lemma MessageBus1_allInstances_generic_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩11:
      fixes pre_post :: "𝔄 st ⇒ 𝔄 state"
      assumes [simp]: "⋀ x :: 𝔄 state. pre_post (x, x) = x"
      shows "∃ τ :: 𝔄 st.
                (τ ⊨ ((OclAllInstances_generic pre_post MessageBus1)
                        ->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(MessageBus1))))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclAllInstances_generic_def
      apply(rule_tac x = τ⇩0 in exI)
      unfolding τ⇩0_def OclValid_def
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      by simp_all

    lemma Car2_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩21:
      fixes pre_post :: "𝔄 st ⇒ 𝔄 state"
      assumes [simp]: "⋀ x :: 𝔄 state. pre_post (x, x) = x"
      shows "∃ τ :: 𝔄 st.
                (τ ⊨ ((OclAllInstances_generic pre_post Car2)
                        ->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car2))))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclAllInstances_generic_def
      apply(rule_tac x = τ⇩0 in exI)
      unfolding τ⇩0_def OclValid_def
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      by simp_all

    lemma MessageBus2_allInstances_generic_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩21:
      fixes pre_post :: "𝔄 st ⇒ 𝔄 state"
      assumes [simp]: "⋀ x :: 𝔄 state. pre_post (x, x) = x"
      shows "∃ τ :: 𝔄 st.
                (τ ⊨ ((OclAllInstances_generic pre_post MessageBus2)
                        ->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(MessageBus2))))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclAllInstances_generic_def
      apply(rule_tac x = τ⇩0 in exI)
      unfolding τ⇩0_def OclValid_def
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      by simp_all

    lemma ECU2_allInstances_generic_oclIsTypeOf⇩E⇩C⇩U⇩21:
      fixes pre_post :: "𝔄 st ⇒ 𝔄 state"
      assumes [simp]: "⋀x::𝔄 state. pre_post (x, x) = x"
      shows "∃ τ. (τ ⊨ ((OclAllInstances_generic pre_post ECU2)
                          ->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(ECU2))))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclAllInstances_generic_def
      apply(rule_tac x = τ⇩0 in exI)
      unfolding τ⇩0_def OclValid_def
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      by simp_all

    lemma Car1_allInstances_at_post_oclIsTypeOf⇩C⇩a⇩r⇩11:
      "∃ τ :: 𝔄 st. (τ ⊨ (Car1 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car1))))"
      unfolding OclAllInstances_at_post_def
      by(rule Car1_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩11, simp)
    lemma MessageBus1_allInstances_at_post_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩11:
      "∃ τ :: 𝔄 st. (τ ⊨ (MessageBus1 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(MessageBus1))))"
      unfolding OclAllInstances_at_post_def
      by(rule MessageBus1_allInstances_generic_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩11, simp)
    lemma Car2_allInstances_at_post_oclIsTypeOf⇩C⇩a⇩r⇩21:
      "∃ τ :: 𝔄 st. (τ ⊨ (Car2 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car2))))"
      unfolding OclAllInstances_at_post_def
      by(rule Car2_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩21, simp)
    lemma MessageBus2_allInstances_at_post_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩21:
      "∃ τ :: 𝔄 st. (τ ⊨ (MessageBus2 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(MessageBus2))))"
      unfolding OclAllInstances_at_post_def
      by(rule MessageBus2_allInstances_generic_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩21, simp)
    lemma ECU2_allInstances_at_post_oclIsTypeOf⇩E⇩C⇩U⇩21:
      "∃ τ :: 𝔄 st. (τ ⊨ (ECU2 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(ECU2))))"
      unfolding OclAllInstances_at_post_def
      by(rule ECU2_allInstances_generic_oclIsTypeOf⇩E⇩C⇩U⇩21, simp)

    lemma Car1_allInstances_at_pre_oclIsTypeOf⇩C⇩a⇩r⇩11:
      "∃ τ :: 𝔄 st. (τ ⊨ (Car1 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car1))))"
      unfolding OclAllInstances_at_pre_def
      by(rule Car1_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩11, simp)
    lemma MessageBus1_allInstances_at_pre_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩11:
      "∃ τ :: 𝔄 st. (τ ⊨ (MessageBus1 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(MessageBus1))))"
      unfolding OclAllInstances_at_pre_def
      by(rule MessageBus1_allInstances_generic_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩11, simp)
    lemma Car2_allInstances_at_pre_oclIsTypeOf⇩C⇩a⇩r⇩21:
      "∃ τ :: 𝔄 st. (τ ⊨ (Car2 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car2))))"
      unfolding OclAllInstances_at_pre_def
      by(rule Car2_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩21, simp)
    lemma MessageBus2_allInstances_at_pre_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩21:
      "∃ τ :: 𝔄 st. (τ ⊨ (MessageBus2 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(MessageBus2))))"
      unfolding OclAllInstances_at_pre_def
      by(rule MessageBus2_allInstances_generic_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩21, simp)
    lemma ECU_allInstances_at_pre_oclIsTypeOf⇩E⇩C⇩U⇩21:
      "∃ τ :: 𝔄 st. (τ ⊨ (ECU2 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(ECU2))))"
      unfolding OclAllInstances_at_pre_def
      by(rule ECU2_allInstances_generic_oclIsTypeOf⇩E⇩C⇩U⇩21, simp)

    lemma Car1_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩1:
      fixes
        τ :: "𝔄 st" and
        pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "τ ⊨ ((OclAllInstances_generic pre_post Car1)->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car1)))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclAllInstances_generic_def OclValid_def OclIsTypeOf⇩C⇩a⇩r⇩1_Car1
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      by (simp add: bot_option_def, simp)
    lemma MessageBus1_allInstances_generic_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1:
      fixes
        τ :: "𝔄 st" and
        pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "τ ⊨ ((OclAllInstances_generic pre_post MessageBus1)
                    ->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(MessageBus1)))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclAllInstances_generic_def OclValid_def OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      by (simp add: bot_option_def, simp)
    lemma Car2_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩2:
      fixes
        τ :: "𝔄 st" and
        pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "τ ⊨ ((OclAllInstances_generic pre_post Car2)->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car2)))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclAllInstances_generic_def OclValid_def OclIsTypeOf⇩C⇩a⇩r⇩2_Car2
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      by (simp add: bot_option_def, simp)
    lemma MessageBus2_allInstances_generic_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2:
      fixes
        τ :: "𝔄 st" and
        pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "τ ⊨ ((OclAllInstances_generic pre_post MessageBus2)
                    ->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(MessageBus2)))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclAllInstances_generic_def OclValid_def OclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      by (simp add: bot_option_def, simp)
    lemma ECU2_allInstances_generic_oclIsTypeOf⇩E⇩C⇩U⇩2:
      fixes
        τ :: "𝔄 st" and
        pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "τ ⊨ ((OclAllInstances_generic pre_post ECU2)->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(ECU2)))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclAllInstances_generic_def OclValid_def OclIsTypeOf⇩E⇩C⇩U⇩2_ECU2
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      by (simp add: bot_option_def, simp)

    lemma Car1_allInstances_at_post_oclIsTypeOf⇩C⇩a⇩r⇩1:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car1 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car1)))"
      unfolding OclAllInstances_at_post_def
      by(rule Car1_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩1)
    lemma MessageBus1_allInstances_at_post_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (MessageBus1 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(MessageBus1)))"
      unfolding OclAllInstances_at_post_def
      by(rule MessageBus1_allInstances_generic_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1)
    lemma Car2_allInstances_at_post_oclIsTypeOf⇩C⇩a⇩r⇩2:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car2 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car2)))"
      unfolding OclAllInstances_at_post_def
      by(rule Car2_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩2)
    lemma MessageBus2_allInstances_at_post_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (MessageBus2 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(MessageBus2)))"
      unfolding OclAllInstances_at_post_def
      by(rule MessageBus2_allInstances_generic_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2)
    lemma ECU2_allInstances_at_post_oclIsTypeOf⇩E⇩C⇩U⇩2:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (ECU2 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(ECU2)))"
      unfolding OclAllInstances_at_post_def
      by(rule ECU2_allInstances_generic_oclIsTypeOf⇩E⇩C⇩U⇩2)

    lemma Car1_allInstances_at_pre_oclIsTypeOf⇩C⇩a⇩r⇩1:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car1 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car1)))"
      unfolding OclAllInstances_at_pre_def
      by(rule Car1_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩1)
    lemma MessageBus1_allInstances_at_pre_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (MessageBus1 .allInstances@pre()->forAll⇩S⇩e⇩t(X|X .oclIsTypeOf(MessageBus1)))"
      unfolding OclAllInstances_at_pre_def
      by(rule MessageBus1_allInstances_generic_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1)
    lemma Car2_allInstances_at_pre_oclIsTypeOf⇩C⇩a⇩r⇩2:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car2 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(Car2)))"
      unfolding OclAllInstances_at_pre_def
      by(rule Car2_allInstances_generic_oclIsTypeOf⇩C⇩a⇩r⇩2)
    lemma MessageBus2_allInstances_at_pre_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (MessageBus2 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(MessageBus2)))"
      unfolding OclAllInstances_at_pre_def
      by(rule MessageBus2_allInstances_generic_oclIsTypeOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2)
    lemma ECU2_allInstances_at_pre_oclIsTypeOf⇩E⇩C⇩U⇩2:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (ECU2 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsTypeOf(ECU2)))"
      unfolding OclAllInstances_at_pre_def
      by(rule ECU2_allInstances_generic_oclIsTypeOf⇩E⇩C⇩U⇩2)

    lemma Car1_allInstances_generic_oclIsKindOf⇩C⇩a⇩r⇩1:
      fixes
        τ :: "𝔄 st" and
        pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "τ ⊨ ((OclAllInstances_generic pre_post Car1)->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(Car1)))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclValid_def OclAllInstances_generic_def OclIsKindOf⇩C⇩a⇩r⇩1_Car1
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      unfolding bot_option_def
      by simp_all
    lemma MessageBus1_allInstances_generic_oclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1:
      fixes
        τ :: "𝔄 st" and
        pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "τ ⊨ ((OclAllInstances_generic pre_post MessageBus1)
                    ->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(MessageBus1)))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclValid_def OclAllInstances_generic_def OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1_MessageBus1
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      unfolding bot_option_def
      by simp_all
    lemma Car2_allInstances_generic_oclIsKindOf⇩C⇩a⇩r⇩2:
      fixes
        τ :: "𝔄 st" and
        pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "τ ⊨ ((OclAllInstances_generic pre_post Car2)->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(Car2)))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclValid_def OclAllInstances_generic_def OclIsKindOf⇩C⇩a⇩r⇩2_Car2
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      unfolding bot_option_def
      by simp_all
    lemma MessageBus2_allInstances_generic_oclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2:
      fixes
        τ :: "𝔄 st" and
        pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "τ ⊨ ((OclAllInstances_generic pre_post MessageBus2)
                    ->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(MessageBus2)))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclValid_def OclAllInstances_generic_def OclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2_MessageBus2
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      unfolding bot_option_def
      by simp_all
    lemma ECU2_allInstances_generic_oclIsKindOf⇩E⇩C⇩U⇩2:
      fixes
        τ :: "𝔄 st" and
        pre_post :: "𝔄 st ⇒ 𝔄 state"
      shows "τ ⊨ ((OclAllInstances_generic pre_post ECU2)->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(ECU2)))"
      unfolding OclAllInstances_generic_defined[simplified OclValid_def] UML_Set.OclForall_def
      unfolding OclValid_def OclAllInstances_generic_def OclIsKindOf⇩E⇩C⇩U⇩2_ECU2
      apply(subst (1 2 3) Abs_Set⇩b⇩a⇩s⇩e_inverse)
      unfolding bot_option_def
      by simp_all

    lemma Car1_allInstances_at_post_oclIsKindOf⇩C⇩a⇩r⇩1:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car1 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(Car1)))"
      unfolding OclAllInstances_at_post_def
      by(rule Car1_allInstances_generic_oclIsKindOf⇩C⇩a⇩r⇩1)
    lemma MessageBus1_allInstances_at_post_oclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1:
      fixes     τ :: "𝔄 st"
      shows "τ ⊨ (MessageBus1 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(MessageBus1)))"
      unfolding OclAllInstances_at_post_def
      by(rule MessageBus1_allInstances_generic_oclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1)
    lemma Car2_allInstances_at_post_oclIsKindOf⇩C⇩a⇩r⇩2:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car2 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(Car2)))"
      unfolding OclAllInstances_at_post_def
      by(rule Car2_allInstances_generic_oclIsKindOf⇩C⇩a⇩r⇩2)
    lemma MessageBus2_allInstances_at_post_oclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (MessageBus2 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(MessageBus2)))"
      unfolding OclAllInstances_at_post_def
      by(rule MessageBus2_allInstances_generic_oclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2)
    lemma ECU2_allInstances_at_post_oclIsKindOf⇩E⇩C⇩U⇩2:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (ECU2 .allInstances()->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(ECU2)))"
      unfolding OclAllInstances_at_post_def
      by(rule ECU2_allInstances_generic_oclIsKindOf⇩E⇩C⇩U⇩2)

    lemma Car1_allInstances_at_pre_oclIsKindOf⇩C⇩a⇩r⇩1:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car1 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(Car1)))"
      unfolding OclAllInstances_at_pre_def
      by(rule Car1_allInstances_generic_oclIsKindOf⇩C⇩a⇩r⇩1)
    lemma MessageBus1_allInstances_at_pre_oclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (MessageBus1 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(MessageBus1)))"
      unfolding OclAllInstances_at_pre_def
      by(rule MessageBus1_allInstances_generic_oclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1)
    lemma Car2_allInstances_at_pre_oclIsKindOf⇩C⇩a⇩r⇩2:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (Car2 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(Car2)))"
      unfolding OclAllInstances_at_pre_def
      by(rule Car2_allInstances_generic_oclIsKindOf⇩C⇩a⇩r⇩2)
    lemma MessageBus2_allInstances_at_pre_oclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (MessageBus2 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(MessageBus2)))"
      unfolding OclAllInstances_at_pre_def
      by(rule MessageBus2_allInstances_generic_oclIsKindOf⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2)
    lemma ECU2_allInstances_at_pre_oclIsKindOf⇩E⇩C⇩U⇩2:
      fixes τ :: "𝔄 st"
      shows "τ ⊨ (ECU2 .allInstances@pre()->forAll⇩S⇩e⇩t(X | X .oclIsKindOf(ECU2)))"
      unfolding OclAllInstances_at_pre_def
      by(rule ECU2_allInstances_generic_oclIsKindOf⇩E⇩C⇩U⇩2)

    subsection ‹OCL Usage: The Accessors›

    text ‹Now we also define accessors›

    definition oid⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 :: oid where
      "oid⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 ≡ 20"
    definition oid⇩C⇩a⇩r⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 :: oid where
      "oid⇩C⇩a⇩r⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 ≡ 30"
    definition oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰 :: oid where
      "oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰 ≡ 21"

    definition eval_extract :: "(𝔄, ('α::object) option option) val ⇒
                                  (oid ⇒ (𝔄, 'β::null) val) ⇒
                                  (𝔄, 'β) val" where
      "eval_extract X f ≡ (λ τ :: 𝔄 st.
          case (X :: 𝔄 st ⇒ ⟨⟨'α⟩⇩⊥⟩⇩⊥) τ of
            ⊥      ⇒ invalid τ |  ― ‹exception propagation›
            ⌊⊥⌋    ⇒ invalid τ |  ― ‹dereferencing null pointer›
            ⌊⌊obj⌋⌋ ⇒ f (oid_of obj) τ)"

    definition deref_assocs :: "(𝔄 st ⇒ 𝔄 state) ⇒
                                    (oid list list ⇒ oid list × oid list) ⇒
                                    oid ⇒ (oid list ⇒ (𝔄, 'α::null) val) ⇒
                                    oid ⇒ (𝔄, 'α) val" where
      "deref_assocs pre⇩p⇩o⇩s⇩t to⇩f⇩r⇩o⇩m assoc⇩o⇩i⇩d f oid ≡ (λ τ :: 𝔄 st.
          case (assocs (pre⇩p⇩o⇩s⇩t τ)) assoc⇩o⇩i⇩d of
            ⌊S::oid list list list⌋ ⇒
              f (list⇩f⇩l⇩a⇩t⇩t⇩e⇩n (map (post⇩s⇩t⇩a⇩t⇩e ∘ to⇩f⇩r⇩o⇩m)
                (filter (λ p :: (oid list list).
                    List.member (pre⇩s⇩t⇩a⇩t⇩e (to⇩f⇩r⇩o⇩m p)) oid) S))) τ |
            _ ⇒ invalid τ)"

    definition deref_oid⇩C⇩a⇩r⇩1 :: "(𝔄 st ⇒ 𝔄 state) ⇒
                                  (𝒯⇩C⇩a⇩r⇩1 ⇒ (𝔄, 'α::null) val) ⇒
                                  oid ⇒ (𝔄, 'α) val" where
      "deref_oid⇩C⇩a⇩r⇩1 fst⇩s⇩n⇩d f oid ≡ (λ τ :: (𝔄 st).
          case (heap (fst⇩s⇩n⇩d τ)) oid of
            ⌊in⇩C⇩a⇩r⇩1 obj⌋ ⇒ f obj τ |
            _           ⇒ invalid τ)"
    definition deref_oid⇩C⇩a⇩r⇩2 :: "(𝔄 st ⇒ 𝔄 state) ⇒
                                  (𝒯⇩C⇩a⇩r⇩2 ⇒ (𝔄, 'α::null) val) ⇒
                                  oid ⇒ (𝔄, 'α) val" where
      "deref_oid⇩C⇩a⇩r⇩2 fst⇩s⇩n⇩d f oid ≡ (λ τ :: (𝔄 st).
          case (heap (fst⇩s⇩n⇩d τ)) oid of
            ⌊ in⇩C⇩a⇩r⇩2 obj ⌋ ⇒ f obj τ |
            _             ⇒ invalid τ)"

    definition deref_oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 :: "(𝔄 st ⇒ 𝔄 state) ⇒
                                        (𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 ⇒ (𝔄, 'α::null) val) ⇒
                                        oid ⇒ (𝔄, 'α::null) val" where
      "deref_oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 fst⇩s⇩n⇩d f oid ≡ (λ τ :: (𝔄 st).
          case (heap (fst⇩s⇩n⇩d τ)) oid of
            ⌊in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 obj⌋ ⇒ f obj τ |
            _           ⇒ invalid τ)"
    definition deref_oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 :: "(𝔄 st ⇒ 𝔄 state) ⇒
                                        (𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 ⇒ (𝔄, 'α::null) val) ⇒
                                        oid ⇒ (𝔄, 'α::null) val" where
      "deref_oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 fst⇩s⇩n⇩d f oid ≡ (λ τ :: (𝔄 st).
          case (heap (fst⇩s⇩n⇩d τ)) oid of
            ⌊ in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 obj ⌋ ⇒ f obj τ |
            _             ⇒ invalid τ)"

    definition deref_oid⇩E⇩C⇩U⇩2 :: "(𝔄 st ⇒ 𝔄 state) ⇒
                                  (𝒯⇩E⇩C⇩U⇩2 ⇒ (𝔄, 'α::null) val) ⇒
                                  oid ⇒ (𝔄, 'α::null) val" where
      "deref_oid⇩E⇩C⇩U⇩2 fst⇩s⇩n⇩d f oid ≡ (λ τ :: (𝔄 st).
          case (heap (fst⇩s⇩n⇩d τ)) oid of
            ⌊in⇩E⇩C⇩U⇩2 obj⌋ ⇒ f obj τ |
            _           ⇒ invalid τ)"

    definition select⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 :: "(('α ⇒ 'β ⇒ ⟨⟨'α⟩⇩⊥⟩⇩⊥) ⇒
                                              'a ⇒ 'b st ⇒ 'c::null) ⇒
                                            'a list ⇒ 'b st ⇒ 'c" where
      "select⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 f ≡ select_object mtSet UML_Set.OclIncluding UML_Set.OclANY
                                    (f (λ (x::'α) (_::'β). ⌊⌊x⌋⌋))"
    definition select⇩C⇩a⇩r⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 :: "(('α ⇒ 'β ⇒ ⟨⟨'α⟩⇩⊥⟩⇩⊥) ⇒
                                              'a ⇒ 'b st ⇒ 'c::null) ⇒
                                            'a list ⇒ 'b st ⇒ 'c" where
      "select⇩C⇩a⇩r⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 f ≡ select_object mtSet UML_Set.OclIncluding UML_Set.OclANY
                                    (f (λ (x::'α) (_::'β). ⌊⌊x⌋⌋))"
    definition select⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰 :: "(('α ⇒ 'β ⇒ ⟨⟨'α⟩⇩⊥⟩⇩⊥) ⇒
                                          'a ⇒ 'b st ⇒ 'c::null) ⇒
                                        'a list ⇒ 'b st ⇒ Set('c)" where
      "select⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰 f ≡ select_object⇩S⇩e⇩t (f (λ (x::'α) (_::'β). ⌊⌊x⌋⌋))"

    definition select⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯 :: "(('α ⇒ 'β ⇒ ⟨⟨'α⟩⇩⊥⟩⇩⊥) ⇒
                                            string ⇒ 'a::null) ⇒
                                          𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 ⇒ 'a" where
      "select⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯 f ≡ (λ X::𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1.
          case X of
            (mk⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 (_::oid) ⊥)   ⇒ null |
            (mk⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 (_::oid) ⌊prot::string⌋) ⇒ f (λ (x::'α) (_::'β). ⌊⌊x⌋⌋) prot)"
    definition select⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯 :: "(('α ⇒ 'β ⇒ ⟨⟨'α⟩⇩⊥⟩⇩⊥) ⇒ string ⇒ 'a::null) ⇒
                                      𝒯⇩E⇩C⇩U⇩2 ⇒ 'a" where
      "select⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯 f ≡ (λ X::𝒯⇩E⇩C⇩U⇩2.
          case X of
            (mk⇩E⇩C⇩U⇩2 (_::oid) ⊥)   ⇒ null |
            (mk⇩E⇩C⇩U⇩2 (_::oid) ⌊prot::string⌋) ⇒ f (λ (x::'α) (_::'β). ⌊⌊x⌋⌋) prot)"

    definition deref_assocs⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 :: "(𝔄 st ⇒ 𝔄 state) ⇒
                                                (oid list ⇒ 𝔄 st ⇒ 'a::null) ⇒
                                                𝒯⇩C⇩a⇩r⇩1 ⇒ 𝔄 st ⇒ 'a" where
      "deref_assocs⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 fst⇩s⇩n⇩d f ≡ (λ mk⇩C⇩a⇩r⇩1 (oid::oid) (_::⟨nat⟩⇩⊥) ⇒
          deref_assocs fst⇩s⇩n⇩d switch⇩2_1 oid⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 f oid)"
    definition deref_assocs⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮⇩2 :: "(𝔄 st ⇒ 𝔄 state) ⇒
                                                (oid list ⇒ 𝔄 st ⇒ 'a::null) ⇒
                                                𝒯⇩C⇩a⇩r⇩2 ⇒ 𝔄 st ⇒ 'a" where
      "deref_assocs⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮⇩2 fst⇩s⇩n⇩d f ≡ (λ mk⇩C⇩a⇩r⇩2 (oid::oid) (_::⟨nat⟩⇩⊥) ⇒
          deref_assocs fst⇩s⇩n⇩d switch⇩2_1 oid⇩C⇩a⇩r⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 f oid)"
    definition deref_assocs⇩2ℰ𝒞𝒰 :: "(𝔄 st ⇒ 𝔄 state) ⇒ (oid list ⇒ 𝔄 st ⇒ 'a::null) ⇒
                                        𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 ⇒ 𝔄 st ⇒ 'a" where
      "deref_assocs⇩2ℰ𝒞𝒰 fst⇩s⇩n⇩d f ≡ (λ mk⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 oid ⇒
          deref_assocs fst⇩s⇩n⇩d switch⇩2_2 oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰 f oid)"

    definition dot⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 :: "Car1 ⇒ MessageBus1"
                  ("(1(_).messagebus⇩C⇩a⇩r⇩1)" 50) where
      "(X).messagebus⇩C⇩a⇩r⇩1 ≡ eval_extract X
                        (deref_oid⇩C⇩a⇩r⇩1 post⇩s⇩t⇩a⇩t⇩e
                          (deref_assocs⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 post⇩s⇩t⇩a⇩t⇩e
                            (select⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 (deref_oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 post⇩s⇩t⇩a⇩t⇩e))))"
    definition dot⇩C⇩a⇩r⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 :: "Car2 ⇒ MessageBus2"
                  ("(1(_).messagebus⇩C⇩a⇩r⇩2)" 50) where
      "(X).messagebus⇩C⇩a⇩r⇩2 ≡ eval_extract X
                        (deref_oid⇩C⇩a⇩r⇩2 post⇩s⇩t⇩a⇩t⇩e
                          (deref_assocs⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮⇩2 post⇩s⇩t⇩a⇩t⇩e
                            (select⇩C⇩a⇩r⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 (deref_oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 post⇩s⇩t⇩a⇩t⇩e))))"
    definition dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰 :: "MessageBus2 ⇒ Set_ECU2"
                  ("(1(_).ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2)" 50) where
      "(X).ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 ≡ eval_extract X
                        (deref_oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 post⇩s⇩t⇩a⇩t⇩e
                          (deref_assocs⇩2ℰ𝒞𝒰 post⇩s⇩t⇩a⇩t⇩e
                            (select⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰 (deref_oid⇩E⇩C⇩U⇩2 post⇩s⇩t⇩a⇩t⇩e))))"

    definition dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯 :: "MessageBus1 ⇒ String"
                  ("(1(_).prot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1)" 50) where
      "(X).prot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 ≡ eval_extract X
                            (deref_oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 post⇩s⇩t⇩a⇩t⇩e
                              (select⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯 reconst⇩𝒯⇩_⇩b⇩a⇩s⇩e))"

    definition dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯 :: "ECU2 ⇒ String"  ("(1(_).prot⇩E⇩C⇩U⇩2)" 50) where
      "(X).prot⇩E⇩C⇩U⇩2 ≡ eval_extract X
                            (deref_oid⇩E⇩C⇩U⇩2 post⇩s⇩t⇩a⇩t⇩e
                              (select⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯 reconst⇩𝒯⇩_⇩b⇩a⇩s⇩e))"
    (*
    definition dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯⇩S⇩e⇩t :: "Set_ECU2 ⇒ Set_String"
                  ("(1(_).prot⇩E⇩C⇩U⇩2⇩-⇩S⇩e⇩t)" 50) where
      "(X).prot⇩E⇩C⇩U⇩2⇩-⇩S⇩e⇩t = OclSetMapVals dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯 X"
    *)
    definition dot⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮_at_pre :: "Car1 ⇒ MessageBus1"
                  ("(1(_).messagebus⇩C⇩a⇩r⇩1@pre)" 50) where
      "(X).messagebus⇩C⇩a⇩r⇩1@pre ≡ eval_extract X
                        (deref_oid⇩C⇩a⇩r⇩1 pre⇩s⇩t⇩a⇩t⇩e
                          (deref_assocs⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 pre⇩s⇩t⇩a⇩t⇩e
                            (select⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 (deref_oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 pre⇩s⇩t⇩a⇩t⇩e))))"
    definition dot⇩C⇩a⇩r⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮_at_pre :: "Car2 ⇒ MessageBus2"
                  ("(1(_).messagebus⇩C⇩a⇩r⇩2@pre)" 50) where
      "(X).messagebus⇩C⇩a⇩r⇩2@pre ≡ eval_extract X
                        (deref_oid⇩C⇩a⇩r⇩2 pre⇩s⇩t⇩a⇩t⇩e
                          (deref_assocs⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮⇩2 pre⇩s⇩t⇩a⇩t⇩e
                            (select⇩C⇩a⇩r⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 (deref_oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 pre⇩s⇩t⇩a⇩t⇩e))))"

    definition dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰_at_pre :: "MessageBus2 ⇒ Set_ECU2"
                  ("(1(_).ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2@pre)" 50) where
      "(X).ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2@pre ≡ eval_extract X
                                (deref_oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 pre⇩s⇩t⇩a⇩t⇩e
                                  (deref_assocs⇩2ℰ𝒞𝒰 pre⇩s⇩t⇩a⇩t⇩e
                                    (select⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰 (deref_oid⇩E⇩C⇩U⇩2 pre⇩s⇩t⇩a⇩t⇩e))))"

    definition dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯_at_pre :: "MessageBus1 ⇒ String"
                                              ("(1(_).prot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1@pre)" 50) where
      "(X).prot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1@pre ≡ eval_extract X
                            (deref_oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 pre⇩s⇩t⇩a⇩t⇩e
                              (select⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯 reconst⇩𝒯⇩_⇩b⇩a⇩s⇩e))"
    definition dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯_at_pre :: "ECU2 ⇒ String" ("(1(_).prot⇩E⇩C⇩U⇩2@pre)" 50) where
      "(X).prot⇩E⇩C⇩U⇩2@pre ≡ eval_extract X
                            (deref_oid⇩E⇩C⇩U⇩2 pre⇩s⇩t⇩a⇩t⇩e
                              (select⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯 reconst⇩𝒯⇩_⇩b⇩a⇩s⇩e))"

    lemmas dot_accessor =
      dot⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮_def dot⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮_at_pre_def
      dot⇩C⇩a⇩r⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮_def dot⇩C⇩a⇩r⇩2ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮_at_pre_def
      dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰_def dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰_at_pre_def
      dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯_def dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯_at_pre_def
      dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯_def dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯_at_pre_def

    lemmas [simp] = eval_extract_def

    lemma cp_dot⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮:
      fixes
        X :: "Car1" and
        τ :: "𝔄 st"
      shows "((X).messagebus⇩C⇩a⇩r⇩1) τ = ((λ _. X τ).messagebus⇩C⇩a⇩r⇩1) τ"
      by (simp add: dot_accessor)
    lemma cp_dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰:
      fixes
        X :: "MessageBus2" and
        τ :: "𝔄 st"
      shows "((X).ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2) τ = ((λ _. X τ).ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2) τ"
      by (simp add: dot_accessor)
    lemma cp_dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯:
      fixes
        X :: "MessageBus1" and
        τ :: "𝔄 st"
      shows "((X).prot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1) τ = ((λ (_::𝔄 st). X τ).prot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1) τ"
      by (simp add: dot_accessor)
    lemma cp_dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯:
      fixes
        X :: "ECU2" and
        τ :: "𝔄 st"
      shows "((X).prot⇩E⇩C⇩U⇩2) τ = ((λ (_::𝔄 st). X τ).prot⇩E⇩C⇩U⇩2) τ"
      by (simp add: dot_accessor)

    lemma cp_dot⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮_at_pre:
      fixes
        X :: "Car1" and
        τ :: "𝔄 st"
      shows "((X).messagebus⇩C⇩a⇩r⇩1@pre) τ = ((λ _. X τ).messagebus⇩C⇩a⇩r⇩1@pre) τ"
      by (simp add: dot_accessor)
    lemma cp_dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰_at_pre:
      fixes
        X :: "MessageBus2" and
        τ :: "𝔄 st"
      shows "((X).ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2@pre) τ = ((λ _. X τ).ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2@pre) τ"
      by (simp add: dot_accessor)
    lemma cp_dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯_at_pre:
      fixes
        X :: "MessageBus1" and
        τ :: "𝔄 st"
      shows "((X).prot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1@pre) τ = ((λ (_::𝔄 st). X τ).prot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1@pre) τ"
      by (simp add: dot_accessor)
    lemma cp_dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯_at_pre:
      fixes
        X :: "ECU2" and
        τ :: "𝔄 st"
      shows "((X).prot⇩E⇩C⇩U⇩2@pre) τ = ((λ (_::𝔄 st). X τ).prot⇩E⇩C⇩U⇩2@pre) τ"
      by (simp add: dot_accessor)

    lemmas cp_dot⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮_I [simp, intro!]=
      cp_dot⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮[THEN allI [THEN allI],
                of "λ (X::Car1) (_::𝔄 st). X"
                    "λ (_::Car1) (τ::𝔄 st). τ", THEN cpI1]
    lemmas cp_dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰_I [simp, intro!]=
      cp_dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰[THEN allI [THEN allI],
                of "λ (X::MessageBus2) (_::𝔄 st). X"
                    "λ (_::MessageBus2) (τ::𝔄 st). τ", THEN cpI1]
    lemmas cp_dot⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮_at_pre_I [simp, intro!]=
      cp_dot⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮_at_pre[THEN allI [THEN allI],
                of "λ (X::Car1) (_::𝔄 st). X"
                    "λ (_::Car1) (τ::𝔄 st). τ", THEN cpI1]
    lemmas cp_dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰_at_pre_I [simp, intro!]=
      cp_dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰_at_pre[THEN allI [THEN allI],
                of "λ (X::MessageBus2) (_::𝔄 st). X"
                    "λ (_::MessageBus2) (τ::𝔄 st). τ", THEN cpI1]
    lemmas cp_dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯_I [simp, intro!]=
      cp_dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯[THEN allI [THEN allI],
                of "λ (X::MessageBus1) (_::𝔄 st). X"
                    "λ (_::MessageBus1) (τ::𝔄 st). τ", THEN cpI1]
    lemmas cp_dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯_I [simp, intro!]=
      cp_dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯[THEN allI [THEN allI],
                of "λ (X::ECU2) (_::𝔄 st). X"
                    "λ (_::ECU2) (τ::𝔄 st). τ", THEN cpI1]
    lemmas cp_dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯_at_pre_I [simp, intro!]=
      cp_dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯_at_pre[THEN allI [THEN allI],
                of "λ (X::MessageBus1) (_::𝔄 st). X"
                    "λ (_::MessageBus1) (τ::𝔄 st). τ", THEN cpI1]
    lemmas cp_dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯_at_pre_I [simp, intro!]=
      cp_dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯_at_pre[THEN allI [THEN allI],
                of "λ (X::ECU2) (_::𝔄 st). X"
                    "λ (_::ECU2) (τ::𝔄 st). τ", THEN cpI1]

    lemma dot⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮_nullstrict [simp]:
      "(null).messagebus⇩C⇩a⇩r⇩1 = invalid"
      unfolding dot_accessor null_fun_def null_option_def bot_option_def
      by (rule ext, simp)
    lemma dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰_nullstrict [simp]:
      "(null).ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 = invalid"
      unfolding dot_accessor null_fun_def null_option_def bot_option_def
      by (rule ext, simp)
    lemma dot⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮_at_pre_nullstrict [simp]:
      "(null).messagebus⇩C⇩a⇩r⇩1@pre = invalid"
      unfolding dot_accessor null_fun_def null_option_def bot_option_def
      by (rule ext, simp)
    lemma dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰_at_pre_nullstrict [simp]:
      "(null).ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2@pre = invalid"
      unfolding dot_accessor null_fun_def null_option_def bot_option_def
      by (rule ext, simp)
    lemma dot⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮_strict [simp]:
      "(invalid).messagebus⇩C⇩a⇩r⇩1 = invalid"
      by (rule ext, simp add: dot_accessor bot_option_def invalid_def)
    lemma dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰_strict [simp]:
      "(invalid).ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 = invalid"
      by (rule ext, simp add: dot_accessor bot_option_def invalid_def)
    lemma dot⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮_at_pre_strict [simp]:
      "(invalid).messagebus⇩C⇩a⇩r⇩1@pre = invalid"
      by (rule ext, simp add: dot_accessor bot_option_def invalid_def)
    lemma dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰_at_pre_strict [simp]:
      "(invalid).ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2@pre = invalid"
      by (rule ext, simp add: dot_accessor bot_option_def invalid_def)

    lemma dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯_nullstrict [simp]:
      "(null).prot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 = invalid"
      unfolding dot_accessor null_fun_def null_option_def bot_option_def
      by (rule ext, simp)
    lemma dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯_nullstrict [simp]:
      "(null).prot⇩E⇩C⇩U⇩2 = invalid"
      unfolding dot_accessor null_fun_def null_option_def bot_option_def
      by (rule ext, simp)
    lemma dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯_at_pre_nullstrict [simp]:
      "(null).prot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1@pre = invalid"
      unfolding dot_accessor null_fun_def null_option_def bot_option_def
      by (rule ext, simp)
    lemma dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯_at_pre_nullstrict [simp]:
      "(null).prot⇩E⇩C⇩U⇩2@pre = invalid"
      unfolding dot_accessor null_fun_def null_option_def bot_option_def
      by (rule ext, simp)
    lemma dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯_strict [simp]:
      "(invalid).prot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 = invalid"
      by (rule ext, simp add: dot_accessor bot_option_def invalid_def)
    lemma dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯_strict [simp]:
      "(invalid).prot⇩E⇩C⇩U⇩2 = invalid"
      by (rule ext, simp add: dot_accessor bot_option_def invalid_def)
    lemma dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1𝒫ℛ𝒪𝒯_at_pre_strict [simp]:
      "(invalid).prot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1@pre = invalid"
      by (rule ext, simp add: dot_accessor bot_option_def invalid_def)
    lemma dot⇩E⇩C⇩U⇩2𝒫ℛ𝒪𝒯_at_pre_strict [simp]:
      "(invalid).prot⇩E⇩C⇩U⇩2@pre = invalid"
      by (rule ext, simp add: dot_accessor bot_option_def invalid_def)

    lemma dot⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮_def_mono:
      fixes
        X :: "Car1" and
        τ :: "𝔄 st"
      shows "τ ⊨ δ(X .messagebus⇩C⇩a⇩r⇩1) ⟹ τ ⊨ δ(X)"
      apply(case_tac "τ ⊨ (X ≜ invalid)")
      apply(insert StrongEq_L_subst2[where
              P = "(λ x::Car1. (δ (x .messagebus⇩C⇩a⇩r⇩1)))" and
              τ = "τ" and x = "X" and y = "invalid"])
      apply(simp, case_tac "τ ⊨ (X ≜ null)")
      apply(insert StrongEq_L_subst2[where
              P = "(λ x::Car1. (δ (x .messagebus⇩C⇩a⇩r⇩1)))" and
              τ = "τ" and x = "X" and y = "null"])
      by(simp, simp add: defined_split)

    lemma dot⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰_def_mono:
      fixes
        X :: "MessageBus2" and
        τ :: "𝔄 st"
      shows "τ ⊨ δ(X .ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2) ⟹ τ ⊨ δ(X)"
      apply(case_tac "τ ⊨ (X ≜ invalid)")
      apply(insert StrongEq_L_subst2[where
              P = "(λ x::MessageBus2. (δ (x .ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2)))" and
              τ = "τ" and x = "X" and y = "invalid"])
      apply(simp, case_tac "τ ⊨ (X ≜ null)")
      apply(insert StrongEq_L_subst2[where
              P = "(λ x::MessageBus2. (δ (x .ecu⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2)))" and
              τ = "τ" and x = "X" and y = "null"])
      by(simp, simp add: defined_split)

    subsection ‹An Example Heap›

    text ‹We can give an example state with some concrete car1s and car2s:›

    definition oid⇩0 :: "'a::zero"    where "oid⇩0 ≡ 0"
    definition oid⇩1 :: "'a::numeral" where "oid⇩1 ≡ 1"
    definition oid⇩2 :: "'a::numeral" where "oid⇩2 ≡ 2"
    definition oid⇩3 :: "'a::numeral" where "oid⇩3 ≡ 3"
    definition oid⇩4 :: "'a::numeral" where "oid⇩4 ≡ 4"
    definition oid⇩M⇩0:: "'a::numeral" where "oid⇩M⇩0 ≡ 5"
    definition oid⇩M⇩1:: "'a::numeral" where "oid⇩M⇩1 ≡ 6"
    definition oid⇩M⇩2:: "'a::numeral" where "oid⇩M⇩2 ≡ 7"
    definition oid⇩M⇩3:: "'a::numeral" where "oid⇩M⇩3 ≡ 8"
    definition oid⇩M⇩4:: "'a::numeral" where "oid⇩M⇩4 ≡ 9"
    definition oid⇩E⇩0:: "'a::numeral" where "oid⇩E⇩0 ≡ 10"
    definition oid⇩E⇩1:: "'a::numeral" where "oid⇩E⇩1 ≡ 11"
    definition oid⇩E⇩2:: "'a::numeral" where "oid⇩E⇩2 ≡ 12"

    definition oids :: "'a::{zero,numeral} list" where
      "oids ≡ [oid⇩0, oid⇩1, oid⇩2, oid⇩3, oid⇩4,
                oid⇩M⇩0, oid⇩M⇩1, oid⇩M⇩2, oid⇩M⇩3, oid⇩M⇩4,
                oid⇩E⇩0, oid⇩E⇩1, oid⇩E⇩2]"

    definition str⇩0 :: "string" where "str⇩0 ≡ ''a''"
    definition str⇩1 :: "string" where "str⇩1 ≡ ''b''"
    definition str⇩2 :: "string" where "str⇩2 ≡ ''c''"
    definition str⇩3 :: "string" where "str⇩3 ≡ ''d''"

    definition prots :: "string list" where
      "prots ≡ [str⇩0, str⇩1, str⇩2, str⇩3]"

    definition car1⇩1 :: "𝒯⇩C⇩a⇩r⇩1" where "car1⇩1 ≡ mk⇩C⇩a⇩r⇩1 oid⇩0 ⌊oid⇩M⇩0⌋"
    definition car1⇩2 :: "𝒯⇩C⇩a⇩r⇩1" where "car1⇩2 ≡ mk⇩C⇩a⇩r⇩1 oid⇩1 ⌊oid⇩M⇩1⌋"
    definition car2⇩1 :: "𝒯⇩C⇩a⇩r⇩2" where "car2⇩1 ≡ mk⇩C⇩a⇩r⇩2 oid⇩2 ⌊oid⇩M⇩2⌋"
    definition car2⇩2 :: "𝒯⇩C⇩a⇩r⇩2" where "car2⇩2 ≡ mk⇩C⇩a⇩r⇩2 oid⇩3 ⌊oid⇩M⇩3⌋"

    definition cars⇩m⇩a⇩n :: "𝒯⇩C⇩a⇩r⇩1 list" where
      "cars⇩m⇩a⇩n ≡ [car1⇩1, car1⇩2]"
    definition cars⇩s⇩u⇩p :: "𝒯⇩C⇩a⇩r⇩2 list" where
      "cars⇩s⇩u⇩p ≡ [car2⇩1, car2⇩2]"

    definition mb1⇩1 :: "𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1" where "mb1⇩1 ≡ mk⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 oid⇩M⇩0 ⌊str⇩0⌋"
    definition mb1⇩2 :: "𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1" where "mb1⇩2 ≡ mk⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 oid⇩M⇩1 ⌊str⇩1⌋"
    definition mb2⇩1 :: "𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2" where "mb2⇩1 ≡ mk⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 oid⇩M⇩2"
    definition mb2⇩2 :: "𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2" where "mb2⇩2 ≡ mk⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 oid⇩M⇩3"

    definition mbs⇩m⇩a⇩n :: "𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 list" where
      "mbs⇩m⇩a⇩n ≡ [mb1⇩1, mb1⇩2]"
    definition mbs⇩s⇩u⇩p :: "𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 list" where
      "mbs⇩s⇩u⇩p ≡ [mb2⇩1, mb2⇩2]"

    definition ecu2⇩1 :: "𝒯⇩E⇩C⇩U⇩2" where "ecu2⇩1 ≡ mk⇩E⇩C⇩U⇩2 oid⇩E⇩0 ⌊str⇩2⌋"
    definition ecu2⇩2 :: "𝒯⇩E⇩C⇩U⇩2" where "ecu2⇩2 ≡ mk⇩E⇩C⇩U⇩2 oid⇩E⇩1 ⌊str⇩3⌋"

    definition ecus⇩s⇩u⇩p :: "𝒯⇩E⇩C⇩U⇩2 list" where
      "ecus⇩s⇩u⇩p ≡ [ecu2⇩1, ecu2⇩2]"

    definition σ :: "𝔄 state" where
      "σ ≡ ⦇heap = Map.empty(
                oid⇩0 ↦ in⇩C⇩a⇩r⇩1 car1⇩1, oid⇩1 ↦ in⇩C⇩a⇩r⇩1 car1⇩2,
                oid⇩2 ↦ in⇩C⇩a⇩r⇩2 car2⇩1, oid⇩3 ↦ in⇩C⇩a⇩r⇩2 car2⇩2,
                oid⇩M⇩0 ↦ in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 mb1⇩1, oid⇩M⇩1 ↦ in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 mb1⇩2,
                oid⇩M⇩2 ↦ in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 mb2⇩1, oid⇩M⇩3 ↦ in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 mb2⇩2,
                oid⇩E⇩0 ↦ in⇩E⇩C⇩U⇩2 ecu2⇩1, oid⇩E⇩1 ↦ in⇩E⇩C⇩U⇩2 ecu2⇩2),
             assocs = Map.empty(
                oid⇩C⇩a⇩r⇩1ℳℰ𝒮𝒮𝒜𝒢ℰℬ𝒰𝒮 ↦ [[[oid⇩0],[oid⇩M⇩0]],[[oid⇩1],[oid⇩M⇩1]]],
                oid⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2ℰ𝒞𝒰 ↦ [[[oid⇩M⇩2],[oid⇩E⇩0]],[[oid⇩M⇩3],[oid⇩E⇩1]]])⦈"

    abbreviation "τ ≡ (σ, σ)"

    definition σ⇩0 :: "𝔄 state" where
      "σ⇩0 ≡ ⦇heap = Map.empty, assocs = Map.empty⦈"

    text ‹
      There is already an equivalent definition of ‹τ⇩0 ≡ (σ⇩0, σ⇩0)› in
      \<^theory>‹Featherweight_OCL.UML_State›.
    ›
    lemma τ⇩0_equiv: "τ⇩0 ≡ (σ⇩0, σ⇩0)"
      unfolding σ⇩0_def τ⇩0_def
      by argo

    lemma refl⇩0_τ_wff: "WFF τ⇩0"
      by(auto simp: WFF_def τ⇩0_equiv τ⇩0_def)
    lemma refl_τ_wff: "WFF τ"
      by(auto simp: WFF_def σ_def
                oid⇩0_def oid⇩1_def oid⇩2_def oid⇩3_def
                oid⇩M⇩0_def oid⇩M⇩1_def oid⇩M⇩2_def oid⇩M⇩3_def
                oid⇩E⇩0_def oid⇩E⇩1_def oid⇩𝔄
                car1⇩1_def car1⇩2_def car2⇩1_def car2⇩2_def
                mb1⇩1_def mb1⇩2_def mb2⇩1_def mb2⇩2_def
                ecu2⇩1_def ecu2⇩2_def)
    lemma basic_τ_wff: "WFF (σ⇩0, σ)"
      by(auto simp: WFF_def σ⇩0_def σ_def
                oid⇩0_def oid⇩1_def oid⇩2_def oid⇩3_def
                oid⇩M⇩0_def oid⇩M⇩1_def oid⇩M⇩2_def oid⇩M⇩3_def
                oid⇩E⇩0_def oid⇩E⇩1_def oid⇩𝔄
                oid_of_𝒯⇩C⇩a⇩r⇩1 oid_of_𝒯⇩C⇩a⇩r⇩2
                oid_of_𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 oid_of_𝒯⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 oid_of_𝒯⇩E⇩C⇩U⇩2
                car1⇩1_def car1⇩2_def car2⇩1_def car2⇩2_def
                mb1⇩1_def mb1⇩2_def mb2⇩1_def mb2⇩2_def
                ecu2⇩1_def ecu2⇩2_def)

    lemma[simp, code_unfold]: "dom (heap σ) =
        {oid⇩0, oid⇩1, oid⇩2, oid⇩3, oid⇩M⇩0, oid⇩M⇩1, oid⇩M⇩2, oid⇩M⇩3, oid⇩E⇩0, oid⇩E⇩1}"
      unfolding σ_def
      by auto
    lemma[simp, code_unfold]: "dom (heap σ⇩0) = {}"
      unfolding σ⇩0_def
      by auto

    lemma[code_unfold]: "ran (heap σ) = {
      in⇩C⇩a⇩r⇩1 car1⇩1, in⇩C⇩a⇩r⇩1 car1⇩2, in⇩C⇩a⇩r⇩2 car2⇩1, in⇩C⇩a⇩r⇩2 car2⇩2,
      in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 mb1⇩1, in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1 mb1⇩2,
      in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 mb2⇩1, in⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2 mb2⇩2,
      in⇩E⇩C⇩U⇩2 ecu2⇩1, in⇩E⇩C⇩U⇩2 ecu2⇩2}"
      unfolding σ_def oid⇩0_def oid⇩1_def oid⇩2_def oid⇩3_def oid⇩E⇩0_def oid⇩E⇩1_def
                oid⇩M⇩0_def oid⇩M⇩1_def oid⇩M⇩2_def oid⇩M⇩3_def
      by (simp add: insert_commute)

    lemma[code_unfold]: "ran (heap σ⇩0) = {}"
      unfolding σ⇩0_def
      by simp

    text ‹Abbreviations for Some Constant OCL Values›

    definition x⇩c⇩a⇩r⇩1⇩_⇩1 :: "Car1" where
      "x⇩c⇩a⇩r⇩1⇩_⇩1 ≡ λ _. ⌊⌊car1⇩1⌋⌋"
    definition x⇩c⇩a⇩r⇩2⇩_⇩1 :: "Car2" where
      "x⇩c⇩a⇩r⇩2⇩_⇩1 ≡ λ _. ⌊⌊car2⇩1⌋⌋"
    definition x⇩c⇩a⇩r⇩1⇩_⇩2 :: "Car1" where
      "x⇩c⇩a⇩r⇩1⇩_⇩2 ≡ λ _. ⌊⌊car1⇩2⌋⌋"
    definition x⇩c⇩a⇩r⇩2⇩_⇩2 :: "Car2" where
      "x⇩c⇩a⇩r⇩2⇩_⇩2 ≡ λ _. ⌊⌊car2⇩2⌋⌋"

    lemmas[simp] = x⇩c⇩a⇩r⇩1⇩_⇩1_def x⇩c⇩a⇩r⇩2⇩_⇩1_def x⇩c⇩a⇩r⇩1⇩_⇩2_def x⇩c⇩a⇩r⇩2⇩_⇩2_def

    lemma[code_unfold]: "((x::Car1) ≐ y) = StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y"
      by(simp only: StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩1)
    lemma[code_unfold]: "((x::Car2) ≐ y) = StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y"
      by(simp only: StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩C⇩a⇩r⇩2)

    definition x⇩m⇩b⇩1⇩_⇩1 :: "MessageBus1" where
      "x⇩m⇩b⇩1⇩_⇩1 ≡ λ _. ⌊⌊mb1⇩1⌋⌋"
    definition x⇩m⇩b⇩2⇩_⇩1 :: "MessageBus2" where
      "x⇩m⇩b⇩2⇩_⇩1 ≡ λ _. ⌊⌊mb2⇩1⌋⌋"
    definition x⇩m⇩b⇩1⇩_⇩2 :: "MessageBus1" where
      "x⇩m⇩b⇩1⇩_⇩2 ≡ λ _. ⌊⌊mb1⇩2⌋⌋"
    definition x⇩m⇩b⇩2⇩_⇩2 :: "MessageBus2" where
      "x⇩m⇩b⇩2⇩_⇩2 ≡ λ _. ⌊⌊mb2⇩2⌋⌋"

    lemmas[simp] = x⇩m⇩b⇩1⇩_⇩1_def x⇩m⇩b⇩2⇩_⇩1_def x⇩m⇩b⇩1⇩_⇩2_def x⇩m⇩b⇩2⇩_⇩2_def

    lemma[code_unfold]: "((x::MessageBus1) ≐ y) = StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y"
      by(simp only: StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩1)
    lemma[code_unfold]: "((x::MessageBus2) ≐ y) = StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t x y"
      by(simp only: StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t⇩_⇩M⇩e⇩s⇩s⇩a⇩g⇩e⇩B⇩u⇩s⇩2)

    end