Pattern-Instanciation-On-System-Engineering-Model/Event-B/pseim/mComponent.bum

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd;de.prob.units.mchBase;org.eventb.codegen.ui.cgConfig" org.eventb.texttools.text_lastmodified="1576654863977" org.eventb.texttools.text_representation="machine mComponent sees cComponent&#10;&#10;variables components container containers c_multiplicity c_index to_unfold_c to_unfold_c_in inst2pat_c M P c_indexes&#10;&#10;invariants&#10;  @comp components ∈ Model ↔ Component&#10;  @comp_finite ∀m·finite(components[{m}])&#10;  @comp_not_shared components∼ ∈ Component ⇸ Model&#10;  @c_mult c_multiplicity ∈ components[{Pat}] → ℕ&#10;  @cont_ty container ∈ ran(components) ⇸ ran(components)&#10;  @cl_ty containers∈ran(components) ↔ ran(components)&#10;  @cl_fin ∀c·finite(containers∼[{c}])&#10;  @cl_cont container ⊆ containers&#10;  @cl_trans containers;containers ⊆ containers&#10;  @cl_left containers ⊆ container;(containers∪id)&#10;  @cl_irrefl containers ∩ id = ∅&#10;  @cl_comp components;containers;components∼ ⊆ id&#10;  theorem @cl_compr components;containers∼;components∼ ⊆ id&#10;  theorem @cont_ctr components;container;components∼ ⊆ id&#10;  theorem @cont_fin ∀c·finite(container∼[{c}])&#10;  theorem @irrefl container ∩ id = ∅&#10;  theorem @cont_mono ∀s,c· s↦c∈container ⇒ containers∼[{s}] ⊂ containers∼[{c}]&#10;&#10;  @to_unfold_c_in to_unfold_c_in ∈ components[{Pat}] ↔ components[{Inst}]&#10;  @to_unfold_c to_unfold_c ⊆ components[{Pat}]&#10;  @inst2pat_c_ty inst2pat_c ∈ components[{Inst}] → components[{Pat}]&#10;  @inst2pat_unfold_in to_unfold_c_in;inst2pat_c ⊆ container&#10;  @pat2inst_unfold to_unfold_c ∩ ran(inst2pat_c) = ∅&#10;  @unfold_root to_unfold_c ∩ dom(container) = ∅&#10;  @unfold_in dom(to_unfold_c_in) ⊆ dom(container)&#10;  @unfold_mul ∀c·c∈to_unfold_c ⇒ c_multiplicity(c) &gt; 0&#10;  @unfold_in_mul ∀c·c∈dom(to_unfold_c_in) ⇒ c_multiplicity(c) &gt; 0&#10;  @unfold_in_i2p ran(to_unfold_c_in) ⊆ dom(inst2pat_c)&#10;  @unfold_cont (inst2pat_c;to_unfold_c_in) ∩ container =∅&#10;  theorem @unfold_unfold_in to_unfold_c ∩ dom(to_unfold_c_in) = ∅&#10;  theorem @unfold_fin ∀c·finite(to_unfold_c_in[{c}])&#10;  @inst2pat_cont inst2pat_c;container = container;inst2pat_c&#10;  @c_index_ty c_index ∈ dom(inst2pat_c) → ℕ&#10;  @to_clone_c_mult ∀c· c∈dom(inst2pat_c) ⇒ c_index(c) ∈ 1‥c_multiplicity(inst2pat_c(c))&#10;  theorem @M_fin finite(ran(c_multiplicity))&#10;  @P P = components[{Pat}]&#10;  @Pnz P ≠ ∅&#10;  @M M = max(ran(c_multiplicity))&#10;  theorem @P_fin finite(P)&#10;  @c_indexes_ty c_indexes ∈ dom(inst2pat_c) ↣ (P ⇸ 1‥M)&#10;  @c_indexes_dom ∀i·i∈dom(inst2pat_c) ⇒ dom(c_indexes(i)) = (containers∪id)[{inst2pat_c(i)}]&#10;  @c_indexes_val ∀i·i∈dom(inst2pat_c) ⇒ c_indexes(i) = inst2pat_c∼;(((containers∪id)[{i}]) ◁ c_index)&#10;  @i2p_dom ∀i·i∈dom(inst2pat_c) ⇒ containers[{i}] ⊆ dom(inst2pat_c)&#10;  @unfold_index_ext ∀c,m· c ∈ to_unfold_c ∧ m∈ran(c_indexes) ⇒ c∉dom(m)&#10;  @unfold_in_index_ext ∀c,i,m· c↦i ∈ to_unfold_c_in ∧ c_indexes(i)⊆m ∧ m ∈ ran(c_indexes) ⇒ c∉dom(m)&#10;  theorem @unfold_index ∀c,k· c ∈ to_unfold_c ∧ k∈1‥M ⇒&#10;                        {c ↦ k} ∉ ran(c_indexes)&#10;  theorem @unfold_in_index ∀c,i,k· c↦i ∈ to_unfold_c_in ∧ k∈1‥M ⇒&#10;                           (c_indexes(i)  {c↦k}) ∉ ran(c_indexes)&#10;&#10;variant (P⇸1‥M)∖c_indexes[dom(inst2pat_c)]&#10;&#10;events&#10;  event instanciate_pattern&#10;    any inst_components c_mult_others c_mult&#10;    where&#10;      @ic inst_components ∈ components[{Pat}] ↔ components[{Mdl}]&#10;      @icr inst_components∼ ∈ components[{Mdl}] ⇸ components[{Pat}]&#10;      @cm c_mult_others ∈ components[{Pat}] ∖ dom(inst_components) → ℕ&#10;      @cmult c_mult = (c_mult_others  {pc· pc ∈ dom(inst_components) ∣ pc ↦ card(inst_components[{pc}])})&#10;    then&#10;      @c_mult c_multiplicity ≔ c_mult&#10;      @to_unfold_c to_unfold_c ≔ (components[{Pat}] ∖ dom(container))∖ c_mult∼[{0}]&#10;      @to_unfold_c_in to_unfold_c_in ≔ ∅&#10;      @components_inst components ≔ {Inst} ⩤ components&#10;      @container_inst container ≔ components[{Inst}] ⩤ container&#10;      @containers_inst containers ≔ components[{Inst}] ⩤ containers&#10;      @c_index c_index ≔ ∅&#10;      @c_indexes c_indexes ≔ ∅&#10;      @pat2inst_c inst2pat_c ≔ ∅&#10;      @M M ≔ max(ran(c_mult))&#10;  end&#10;&#10;  convergent event unfold_root_c&#10;    any c new_c&#10;    where&#10;      @c_ty c ∈ to_unfold_c&#10;      @new_c_ty new_c ∈ 1‥c_multiplicity(c) ↣ Component ∖ ran(components)&#10;      theorem @new_c_fin finite(ran(new_c))&#10;      theorem @new_c_card card(ran(new_c)) = c_multiplicity(c)&#10;    then&#10;      @new_c_model components ≔ components ∪ ({Inst}×ran(new_c))&#10;      @to_unfold_c_in to_unfold_c_in ≔ to_unfold_c_in ∪&#10;                      ((container∼[{c}] ∖ c_multiplicity∼[{0}]) × ran(new_c))&#10;      @c_index c_index ≔ c_index ∪ new_c∼&#10;      @to_unfold_c to_unfold_c ≔ to_unfold_c ∖ {c}&#10;      @pat2inst_c inst2pat_c ≔ inst2pat_c ∪ (ran(new_c) × {c})&#10;      @c_indexes c_indexes ≔ c_indexes ∪ {i·i∈ran(new_c) ∣ i↦{c↦new_c∼(i)}}&#10;  end&#10;&#10;  convergent event unfold_node_c // réplication des éléments composants // A voir: duplication du contenu de C&#10;    any c dest new_c&#10;    where&#10;      @c_ty c ↦ dest ∈ to_unfold_c_in&#10;      @new_c_ty new_c ∈ 1‥c_multiplicity(c) ↣ Component ∖ ran(components)&#10;      theorem @new_c_fin finite(ran(new_c))&#10;      theorem @new_c_card card(ran(new_c)) = c_multiplicity(c)&#10;    then&#10;      @new_c_model components ≔ components ∪ ({Inst}×ran(new_c))&#10;      @new_c_container container ≔ container ∪ (ran(new_c)×{dest})&#10;      @c_index c_index ≔ c_index ∪ new_c∼&#10;      @to_unfold_c_in to_unfold_c_in ≔ (to_unfold_c_in ∖ {c ↦ dest}) ∪&#10;                      ((container∼[{c}] ∖ c_multiplicity∼[{0}]) × ran(new_c))&#10;      @pat2inst_c inst2pat_c ≔ inst2pat_c ∪ (ran(new_c) × {c})&#10;      @cont containers ≔ containers ∪ (ran(new_c) × {dest}) ∪ (ran(new_c) × containers[{dest}])&#10;      @c_indexes c_indexes ≔ c_indexes ∪ {i·i∈ran(new_c) ∣ i↦(c_indexes(dest)  {c↦new_c∼(i)})}&#10;  end&#10;&#10;  event apply_pattern // transformation du modèle&#10;    any inst_components // instance mapping&#10;        new_components&#10;    where&#10;      @ic inst_components ∈ components[{Inst}] ⤔ components[{Mdl}]&#10;      @nc new_components ∈ components[{Inst}] ∖ dom(inst_components) ↣ Component ∖ ran(components)&#10;      @acycl_inst_components dom(inst_components) ◁ container;inst_components ⊆ inst_components;container&#10;      @acycl_container container[dom(inst_components)] ⊆ dom(inst_components)&#10;      theorem @inst_containers_dom containers[dom(inst_components)] ⊆ dom(inst_components)&#10;      theorem @inst_containers dom(inst_components) ◁ containers;inst_components ⊆ inst_components;containers&#10;      theorem @new_cont ran(new_components) ∩ ran(container) = ∅&#10;      theorem @new_conts ran(new_components) ∩ ran(containers) = ∅&#10;    then&#10;      @m components ≔ components ∪ ({Mdl}×ran(new_components))&#10;      @f container ≔ container ∪ (new_components∼;container;(inst_components ∪ new_components))&#10;      @c containers ≔ containers ∪ (new_components∼;containers;(new_components ∪ inst_components);(containers ∪ id))&#10;  end&#10;end&#10;" version="5">
<org.eventb.core.seesContext name="_cQf0YPqUEeectLZKwQfI0A" org.eventb.core.target="cComponent"/>
<org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="instanciate_pattern">
<org.eventb.core.parameter name="_O1UjgPqmEeectLZKwQfI0A" org.eventb.core.identifier="inst_components"/>
<org.eventb.core.guard name="_O1UjgvqmEeectLZKwQfI0A" org.eventb.core.label="ic" org.eventb.core.predicate="inst_components ∈ components[{Pat}] ↔ components[{Mdl}]"/>
<org.eventb.core.guard name="_O1Ujg_qmEeectLZKwQfI0A" org.eventb.core.label="icr" org.eventb.core.predicate="inst_components∼ ∈ components[{Mdl}] ⇸ components[{Pat}]"/>
<org.eventb.core.guard name="_O1UjhPqmEeectLZKwQfI0A" org.eventb.core.label="cm" org.eventb.core.predicate="c_mult_others ∈ components[{Pat}] ∖ dom(inst_components) → ℕ"/>
<org.eventb.core.action name="_O1UjhfqmEeectLZKwQfI0A" org.eventb.core.assignment="c_multiplicity ≔ c_mult" org.eventb.core.label="c_mult"/>
<org.eventb.core.parameter name="_O1UjgfqmEeectLZKwQfI0A" org.eventb.core.identifier="c_mult_others"/>
<org.eventb.core.action name="_O1WYt_qmEeectLZKwQfI0A" org.eventb.core.assignment="to_unfold_c ≔ (components[{Pat}] ∖ dom(container))∖ c_mult∼[{0}]" org.eventb.core.label="to_unfold_c"/>
<org.eventb.core.action name="_O1WYuPqmEeectLZKwQfI0A" org.eventb.core.assignment="to_unfold_c_in ≔ ∅" org.eventb.core.label="to_unfold_c_in"/>
<org.eventb.core.action name="_O1W_xPqmEeectLZKwQfI0A" org.eventb.core.assignment="components ≔ {Inst} ⩤ components" org.eventb.core.label="components_inst"/>
<org.eventb.core.action name="_O1W_xfqmEeectLZKwQfI0A" org.eventb.core.assignment="container ≔ components[{Inst}] ⩤ container" org.eventb.core.label="container_inst"/>
<org.eventb.core.action name="_O1W_xvqmEeectLZKwQfI0A" org.eventb.core.assignment="containers ≔ components[{Inst}] ⩤ containers" org.eventb.core.label="containers_inst"/>
<org.eventb.core.action name="_O1W_x_qmEeectLZKwQfI0A" org.eventb.core.assignment="c_index ≔ ∅" org.eventb.core.label="c_index"/>
<org.eventb.core.parameter name="_O1VxofqmEeectLZKwQfI0A" org.eventb.core.identifier="c_mult"/>
<org.eventb.core.guard name="_O1WYsfqmEeectLZKwQfI0A" org.eventb.core.label="cmult" org.eventb.core.predicate="c_mult = (c_mult_others  {pc· pc ∈ dom(inst_components) ∣ pc ↦ card(inst_components[{pc}])})"/>
<org.eventb.core.action name="_O1W_yPqmEeectLZKwQfI0A" org.eventb.core.assignment="c_indexes ≔ ∅" org.eventb.core.label="c_indexes"/>
<org.eventb.core.action name="_O1Xm1PqmEeectLZKwQfI0A" org.eventb.core.assignment="inst2pat_c ≔ ∅" org.eventb.core.label="pat2inst_c"/>
<org.eventb.core.action name="_O1Xm1fqmEeectLZKwQfI0A" org.eventb.core.assignment="M ≔ max(ran(c_mult))" org.eventb.core.label="M"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_cQf0YfqUEeectLZKwQfI0A" org.eventb.core.identifier="components"/>
<org.eventb.core.variable name="_cQf0YvqUEeectLZKwQfI0A" org.eventb.core.identifier="container"/>
<org.eventb.core.invariant name="_cQf0Y_qUEeectLZKwQfI0A" org.eventb.core.label="comp" org.eventb.core.predicate="components ∈ Model ↔ Component"/>
<org.eventb.core.invariant name="_cQf0ZPqUEeectLZKwQfI0A" org.eventb.core.label="comp_finite" org.eventb.core.predicate="∀m·finite(components[{m}])"/>
<org.eventb.core.invariant name="_ip9Q0PqUEeectLZKwQfI0A" org.eventb.core.label="comp_not_shared" org.eventb.core.predicate="components∼ ∈ Component ⇸ Model"/>
<org.eventb.core.invariant name="_GMp30PqWEeectLZKwQfI0A" org.eventb.core.label="c_mult" org.eventb.core.predicate="c_multiplicity ∈ components[{Pat}] → ℕ"/>
<org.eventb.core.variable name="_gmDo8PqgEeectLZKwQfI0A" org.eventb.core.identifier="containers"/>
<org.eventb.core.invariant name="_gmDo8fqgEeectLZKwQfI0A" org.eventb.core.label="cont_ty" org.eventb.core.predicate="container ∈ ran(components) ⇸ ran(components)"/>
<org.eventb.core.invariant name="_gmDo8vqgEeectLZKwQfI0A" org.eventb.core.label="cl_ty" org.eventb.core.predicate="containers∈ran(components) ↔ ran(components)"/>
<org.eventb.core.invariant name="_oXBHAPqkEeectLZKwQfI0A" org.eventb.core.label="cl_fin" org.eventb.core.predicate="∀c·finite(containers∼[{c}])"/>
<org.eventb.core.variable name="_1dqNIPqkEeectLZKwQfI0A" org.eventb.core.identifier="c_multiplicity"/>
<org.eventb.core.variable name="_1dqNIfqkEeectLZKwQfI0A" org.eventb.core.identifier="c_index"/>
<org.eventb.core.variable name="_1dqNIvqkEeectLZKwQfI0A" org.eventb.core.identifier="to_unfold_c"/>
<org.eventb.core.invariant name="_1dqNI_qkEeectLZKwQfI0A" org.eventb.core.label="cl_cont" org.eventb.core.predicate="container ⊆ containers"/>
<org.eventb.core.invariant name="_1dqNJPqkEeectLZKwQfI0A" org.eventb.core.label="cl_trans" org.eventb.core.predicate="containers;containers ⊆ containers"/>
<org.eventb.core.invariant name="_1dq0MPqkEeectLZKwQfI0A" org.eventb.core.label="cl_left" org.eventb.core.predicate="containers ⊆ container;(containers∪id)"/>
<org.eventb.core.event name="_O1VxoPqmEeectLZKwQfI0A" org.eventb.core.convergence="1" org.eventb.core.extended="false" org.eventb.core.label="unfold_root_c">
<org.eventb.core.guard name="_O1WYsvqmEeectLZKwQfI0A" org.eventb.core.label="c_ty" org.eventb.core.predicate="c ∈ to_unfold_c"/>
<org.eventb.core.parameter name="_O1WYsPqmEeectLZKwQfI0A" org.eventb.core.identifier="c"/>
<org.eventb.core.action name="_O1Xm1vqmEeectLZKwQfI0A" org.eventb.core.assignment="components ≔ components ∪ ({Inst}×ran(new_c))" org.eventb.core.label="new_c_model"/>
<org.eventb.core.action name="_O1Xm1_qmEeectLZKwQfI0A" org.eventb.core.assignment="to_unfold_c_in ≔ to_unfold_c_in ∪&#10;                      ((container∼[{c}] ∖ c_multiplicity∼[{0}]) × ran(new_c))" org.eventb.core.label="to_unfold_c_in"/>
<org.eventb.core.guard name="_O1WYs_qmEeectLZKwQfI0A" org.eventb.core.label="new_c_ty" org.eventb.core.predicate="new_c ∈ 1‥c_multiplicity(c) ↣ Component ∖ ran(components)"/>
<org.eventb.core.guard name="_O1WYtPqmEeectLZKwQfI0A" org.eventb.core.label="new_c_fin" org.eventb.core.predicate="finite(ran(new_c))" org.eventb.core.theorem="true"/>
<org.eventb.core.parameter name="_O1W_wPqmEeectLZKwQfI0A" org.eventb.core.identifier="new_c"/>
<org.eventb.core.guard name="_O1WYtfqmEeectLZKwQfI0A" org.eventb.core.label="new_c_card" org.eventb.core.predicate="card(ran(new_c)) = c_multiplicity(c)" org.eventb.core.theorem="true"/>
<org.eventb.core.action name="_O1YN4PqmEeectLZKwQfI0A" org.eventb.core.assignment="c_index ≔ c_index ∪ new_c∼" org.eventb.core.label="c_index"/>
<org.eventb.core.action name="_O1YN4fqmEeectLZKwQfI0A" org.eventb.core.assignment="to_unfold_c ≔ to_unfold_c ∖ {c}" org.eventb.core.label="to_unfold_c"/>
<org.eventb.core.action name="_O1YN4vqmEeectLZKwQfI0A" org.eventb.core.assignment="inst2pat_c ≔ inst2pat_c ∪ (ran(new_c) × {c})" org.eventb.core.label="pat2inst_c"/>
<org.eventb.core.action name="_lyJKIPreEeerIsS6OyYQ4w" org.eventb.core.assignment="c_indexes ≔ c_indexes ∪ {i·i∈ran(new_c) ∣ i↦{c↦new_c∼(i)}}" org.eventb.core.label="c_indexes"/>
</org.eventb.core.event>
<org.eventb.core.event name="_O1WYufqmEeectLZKwQfI0A" org.eventb.core.comment="réplication des éléments composants // A voir: duplication du contenu de C" org.eventb.core.convergence="1" org.eventb.core.extended="false" org.eventb.core.label="unfold_node_c">
<org.eventb.core.parameter name="_O1W_wfqmEeectLZKwQfI0A" org.eventb.core.identifier="c"/>
<org.eventb.core.guard name="_O1WYtvqmEeectLZKwQfI0A" org.eventb.core.label="c_ty" org.eventb.core.predicate="c ↦ dest ∈ to_unfold_c_in"/>
<org.eventb.core.parameter name="_O1Xm0PqmEeectLZKwQfI0A" org.eventb.core.identifier="dest"/>
<org.eventb.core.parameter name="_O1Xm0fqmEeectLZKwQfI0A" org.eventb.core.identifier="new_c"/>
<org.eventb.core.guard name="_O1W_wvqmEeectLZKwQfI0A" org.eventb.core.label="new_c_ty" org.eventb.core.predicate="new_c ∈ 1‥c_multiplicity(c) ↣ Component ∖ ran(components)"/>
<org.eventb.core.guard name="_O1W_w_qmEeectLZKwQfI0A" org.eventb.core.label="new_c_fin" org.eventb.core.predicate="finite(ran(new_c))" org.eventb.core.theorem="true"/>
<org.eventb.core.guard name="_O1Xm0vqmEeectLZKwQfI0A" org.eventb.core.label="new_c_card" org.eventb.core.predicate="card(ran(new_c)) = c_multiplicity(c)" org.eventb.core.theorem="true"/>
<org.eventb.core.action name="_rQ0PgftxEeectLZKwQfI0A" org.eventb.core.assignment="components ≔ components ∪ ({Inst}×ran(new_c))" org.eventb.core.label="new_c_model"/>
<org.eventb.core.action name="_xQWRoP01EeeINffjS36taQ" org.eventb.core.assignment="container ≔ container ∪ (ran(new_c)×{dest})" org.eventb.core.label="new_c_container"/>
<org.eventb.core.action name="_254qkAA2EeictLZKwQfI0A" org.eventb.core.assignment="c_index ≔ c_index ∪ new_c∼" org.eventb.core.label="c_index"/>
<org.eventb.core.action name="_ptpcYAxlEeqU6uo9ksjEPA" org.eventb.core.assignment="to_unfold_c_in ≔ (to_unfold_c_in ∖ {c ↦ dest}) ∪&#10;                      ((container∼[{c}] ∖ c_multiplicity∼[{0}]) × ran(new_c))" org.eventb.core.label="to_unfold_c_in"/>
<org.eventb.core.action name="_ptpcYQxlEeqU6uo9ksjEPA" org.eventb.core.assignment="inst2pat_c ≔ inst2pat_c ∪ (ran(new_c) × {c})" org.eventb.core.label="pat2inst_c"/>
<org.eventb.core.action name="_ptpcYgxlEeqU6uo9ksjEPA" org.eventb.core.assignment="containers ≔ containers ∪ (ran(new_c) × {dest}) ∪ (ran(new_c) × containers[{dest}])" org.eventb.core.label="cont"/>
<org.eventb.core.action name="__Rz3sAyBEeqU6uo9ksjEPA" org.eventb.core.assignment="c_indexes ≔ c_indexes ∪ {i·i∈ran(new_c) ∣ i↦(c_indexes(dest)  {c↦new_c∼(i)})}" org.eventb.core.label="c_indexes"/>
</org.eventb.core.event>
<org.eventb.core.event name="_O1W_yfqmEeectLZKwQfI0A" org.eventb.core.comment="transformation du modèle" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="apply_pattern">
<org.eventb.core.parameter name="_rQ0PgPtxEeectLZKwQfI0A" org.eventb.core.comment="instance mapping" org.eventb.core.identifier="inst_components"/>
<org.eventb.core.guard name="_AkqiQAhGEeqU6uo9ksjEPA" org.eventb.core.label="ic" org.eventb.core.predicate="inst_components ∈ components[{Inst}] ⤔ components[{Mdl}]"/>
<org.eventb.core.parameter name="_h4VmkAKrEeiAPf1wPUl3Gw" org.eventb.core.identifier="new_components"/>
<org.eventb.core.guard name="_AkqiQQhGEeqU6uo9ksjEPA" org.eventb.core.label="nc" org.eventb.core.predicate="new_components ∈ components[{Inst}] ∖ dom(inst_components) ↣ Component ∖ ran(components)"/>
<org.eventb.core.guard name="_AkqiQghGEeqU6uo9ksjEPA" org.eventb.core.label="acycl_inst_components" org.eventb.core.predicate="dom(inst_components) ◁ container;inst_components ⊆ inst_components;container"/>
<org.eventb.core.guard name="_AkqiQwhGEeqU6uo9ksjEPA" org.eventb.core.label="acycl_container" org.eventb.core.predicate="container[dom(inst_components)] ⊆ dom(inst_components)"/>
<org.eventb.core.action name="_nECSUA3EEeqU6uo9ksjEPA" org.eventb.core.assignment="components ≔ components ∪ ({Mdl}×ran(new_components))" org.eventb.core.label="m"/>
<org.eventb.core.action name="_nECSUQ3EEeqU6uo9ksjEPA" org.eventb.core.assignment="container ≔ container ∪ (new_components∼;container;(inst_components ∪ new_components))" org.eventb.core.label="f"/>
<org.eventb.core.action name="_suvPACASEeq7BuY4D8yZpw" org.eventb.core.assignment="containers ≔ containers ∪ (new_components∼;containers;(new_components ∪ inst_components);(containers ∪ id))" org.eventb.core.label="c"/>
<org.eventb.core.guard name="_PCNOECCpEeq7BuY4D8yZpw" org.eventb.core.label="inst_containers_dom" org.eventb.core.predicate="containers[dom(inst_components)] ⊆ dom(inst_components)" org.eventb.core.theorem="true"/>
<org.eventb.core.guard name="_PCN1ICCpEeq7BuY4D8yZpw" org.eventb.core.label="inst_containers" org.eventb.core.predicate="dom(inst_components) ◁ containers;inst_components ⊆ inst_components;containers" org.eventb.core.theorem="true"/>
<org.eventb.core.guard name="_vq9m8CC_Eeq7BuY4D8yZpw" org.eventb.core.label="new_cont" org.eventb.core.predicate="ran(new_components) ∩ ran(container) = ∅" org.eventb.core.theorem="true"/>
<org.eventb.core.guard name="_vq9m8SC_Eeq7BuY4D8yZpw" org.eventb.core.label="new_conts" org.eventb.core.predicate="ran(new_components) ∩ ran(containers) = ∅" org.eventb.core.theorem="true"/>
</org.eventb.core.event>
<org.eventb.core.invariant name="_l7KVEQA1EeictLZKwQfI0A" org.eventb.core.label="cl_irrefl" org.eventb.core.predicate="containers ∩ id = ∅"/>
<org.eventb.core.invariant name="_l7KVEgA1EeictLZKwQfI0A" org.eventb.core.label="cl_comp" org.eventb.core.predicate="components;containers;components∼ ⊆ id"/>
<org.eventb.core.variable name="_9phD8AKqEeiAPf1wPUl3Gw" org.eventb.core.identifier="to_unfold_c_in"/>
<org.eventb.core.invariant name="_Hwdz4AKtEeiAPf1wPUl3Gw" org.eventb.core.label="cl_compr" org.eventb.core.predicate="components;containers∼;components∼ ⊆ id" org.eventb.core.theorem="true"/>
<org.eventb.core.variable name="_xudpYAK5EeiAPf1wPUl3Gw" org.eventb.core.identifier="inst2pat_c"/>
<org.eventb.core.invariant name="_xudpYQK5EeiAPf1wPUl3Gw" org.eventb.core.label="cont_ctr" org.eventb.core.predicate="components;container;components∼ ⊆ id" org.eventb.core.theorem="true"/>
<org.eventb.core.invariant name="_fxu54ALAEeiAPf1wPUl3Gw" org.eventb.core.label="cont_fin" org.eventb.core.predicate="∀c·finite(container∼[{c}])" org.eventb.core.theorem="true"/>
<org.eventb.core.invariant name="_PaxdoAMwEei9ocE08JsPSw" org.eventb.core.label="irrefl" org.eventb.core.predicate="container ∩ id = ∅" org.eventb.core.theorem="true"/>
<org.eventb.core.invariant name="_nieoAAMxEei9ocE08JsPSw" org.eventb.core.label="cont_mono" org.eventb.core.predicate="∀s,c· s↦c∈container ⇒ containers∼[{s}] ⊂ containers∼[{c}]" org.eventb.core.theorem="true"/>
<org.eventb.core.invariant name="_gxZD0AMzEei9ocE08JsPSw" org.eventb.core.label="to_unfold_c_in" org.eventb.core.predicate="to_unfold_c_in ∈ components[{Pat}] ↔ components[{Inst}]"/>
<org.eventb.core.invariant name="_gxZD0QMzEei9ocE08JsPSw" org.eventb.core.label="to_unfold_c" org.eventb.core.predicate="to_unfold_c ⊆ components[{Pat}]"/>
<org.eventb.core.invariant name="_gxZD0gMzEei9ocE08JsPSw" org.eventb.core.label="inst2pat_c_ty" org.eventb.core.predicate="inst2pat_c ∈ components[{Inst}] → components[{Pat}]"/>
<org.eventb.core.invariant name="_V6rHAAM1Eei9ocE08JsPSw" org.eventb.core.label="inst2pat_unfold_in" org.eventb.core.predicate="to_unfold_c_in;inst2pat_c ⊆ container"/>
<org.eventb.core.variant name="_gEhCEQhLEeqU6uo9ksjEPA" org.eventb.core.expression="(P⇸1‥M)∖c_indexes[dom(inst2pat_c)]"/>
<org.eventb.core.invariant name="_4gspwAkfEeqU6uo9ksjEPA" org.eventb.core.label="pat2inst_unfold" org.eventb.core.predicate="to_unfold_c ∩ ran(inst2pat_c) = ∅"/>
<org.eventb.core.invariant name="_ClMccAk_EeqU6uo9ksjEPA" org.eventb.core.label="unfold_root" org.eventb.core.predicate="to_unfold_c ∩ dom(container) = ∅"/>
<org.eventb.core.invariant name="_6Bzq0AlZEeqU6uo9ksjEPA" org.eventb.core.label="unfold_in" org.eventb.core.predicate="dom(to_unfold_c_in) ⊆ dom(container)"/>
<org.eventb.core.invariant name="_-v2gwAl5EeqU6uo9ksjEPA" org.eventb.core.label="unfold_mul" org.eventb.core.predicate="∀c·c∈to_unfold_c ⇒ c_multiplicity(c) &gt; 0"/>
<org.eventb.core.invariant name="_Ar4dsAl8EeqU6uo9ksjEPA" org.eventb.core.label="unfold_in_mul" org.eventb.core.predicate="∀c·c∈dom(to_unfold_c_in) ⇒ c_multiplicity(c) &gt; 0"/>
<org.eventb.core.invariant name="_byYtUAxjEeqU6uo9ksjEPA" org.eventb.core.label="unfold_in_i2p" org.eventb.core.predicate="ran(to_unfold_c_in) ⊆ dom(inst2pat_c)"/>
<org.eventb.core.invariant name="_ptqDcQxlEeqU6uo9ksjEPA" org.eventb.core.label="unfold_cont" org.eventb.core.predicate="(inst2pat_c;to_unfold_c_in) ∩ container =∅"/>
<org.eventb.core.invariant name="_ptqDcgxlEeqU6uo9ksjEPA" org.eventb.core.label="unfold_unfold_in" org.eventb.core.predicate="to_unfold_c ∩ dom(to_unfold_c_in) = ∅" org.eventb.core.theorem="true"/>
<org.eventb.core.invariant name="_MM724AxtEeqU6uo9ksjEPA" org.eventb.core.label="unfold_fin" org.eventb.core.predicate="∀c·finite(to_unfold_c_in[{c}])" org.eventb.core.theorem="true"/>
<org.eventb.core.invariant name="_MM724QxtEeqU6uo9ksjEPA" org.eventb.core.label="inst2pat_cont" org.eventb.core.predicate="inst2pat_c;container = container;inst2pat_c"/>
<org.eventb.core.variable name="__R1F0AyBEeqU6uo9ksjEPA" org.eventb.core.identifier="M"/>
<org.eventb.core.invariant name="__R1F0QyBEeqU6uo9ksjEPA" org.eventb.core.label="c_index_ty" org.eventb.core.predicate="c_index ∈ dom(inst2pat_c) → ℕ"/>
<org.eventb.core.variable name="_nEDgcA3EEeqU6uo9ksjEPA" org.eventb.core.identifier="P"/>
<org.eventb.core.variable name="_nEDgcQ3EEeqU6uo9ksjEPA" org.eventb.core.identifier="c_indexes"/>
<org.eventb.core.invariant name="_nEDgcg3EEeqU6uo9ksjEPA" org.eventb.core.label="to_clone_c_mult" org.eventb.core.predicate="∀c· c∈dom(inst2pat_c) ⇒ c_index(c) ∈ 1‥c_multiplicity(inst2pat_c(c))"/>
<org.eventb.core.invariant name="_nEDgcw3EEeqU6uo9ksjEPA" org.eventb.core.label="M_fin" org.eventb.core.predicate="finite(ran(c_multiplicity))" org.eventb.core.theorem="true"/>
<org.eventb.core.invariant name="_nEDgdA3EEeqU6uo9ksjEPA" org.eventb.core.label="P" org.eventb.core.predicate="P = components[{Pat}]"/>
<org.eventb.core.invariant name="_nEDgdQ3EEeqU6uo9ksjEPA" org.eventb.core.label="Pnz" org.eventb.core.predicate="P ≠ ∅"/>
<org.eventb.core.invariant name="_3N038Q6WEeqU6uo9ksjEPA" org.eventb.core.label="M" org.eventb.core.predicate="M = max(ran(c_multiplicity))"/>
<org.eventb.core.invariant name="_rcyHQA6gEeqU6uo9ksjEPA" org.eventb.core.label="P_fin" org.eventb.core.predicate="finite(P)" org.eventb.core.theorem="true"/>
<org.eventb.core.invariant name="_rcyHQQ6gEeqU6uo9ksjEPA" org.eventb.core.label="c_indexes_ty" org.eventb.core.predicate="c_indexes ∈ dom(inst2pat_c) ↣ (P ⇸ 1‥M)"/>
<org.eventb.core.invariant name="_2SMx0Q7FEeqU6uo9ksjEPA" org.eventb.core.label="c_indexes_dom" org.eventb.core.predicate="∀i·i∈dom(inst2pat_c) ⇒ dom(c_indexes(i)) = (containers∪id)[{inst2pat_c(i)}]"/>
<org.eventb.core.invariant name="_2SMx0g7FEeqU6uo9ksjEPA" org.eventb.core.label="c_indexes_val" org.eventb.core.predicate="∀i·i∈dom(inst2pat_c) ⇒ c_indexes(i) = inst2pat_c∼;(((containers∪id)[{i}]) ◁ c_index)"/>
<org.eventb.core.invariant name="_2SMx0w7FEeqU6uo9ksjEPA" org.eventb.core.label="i2p_dom" org.eventb.core.predicate="∀i·i∈dom(inst2pat_c) ⇒ containers[{i}] ⊆ dom(inst2pat_c)"/>
<org.eventb.core.invariant name="_2SMx1A7FEeqU6uo9ksjEPA" org.eventb.core.label="unfold_index_ext" org.eventb.core.predicate="∀c,m· c ∈ to_unfold_c ∧ m∈ran(c_indexes) ⇒ c∉dom(m)"/>
<org.eventb.core.invariant name="_iR6UgA7fEeqU6uo9ksjEPA" org.eventb.core.label="unfold_in_index_ext" org.eventb.core.predicate="∀c,i,m· c↦i ∈ to_unfold_c_in ∧ c_indexes(i)⊆m ∧ m ∈ ran(c_indexes) ⇒ c∉dom(m)"/>
<org.eventb.core.invariant name="_BSFPUBEBEeqU6uo9ksjEPA" org.eventb.core.label="unfold_index" org.eventb.core.predicate="∀c,k· c ∈ to_unfold_c ∧ k∈1‥M ⇒&#10;                        {c ↦ k} ∉ ran(c_indexes)" org.eventb.core.theorem="true"/>
<org.eventb.core.invariant name="_vsdVYCC3Eeq7BuY4D8yZpw" org.eventb.core.label="unfold_in_index" org.eventb.core.predicate="∀c,i,k· c↦i ∈ to_unfold_c_in ∧ k∈1‥M ⇒&#10;                           (c_indexes(i)  {c↦k}) ∉ ran(c_indexes)" org.eventb.core.theorem="true"/>
</org.eventb.core.machineFile>