MOISE
/
Pattern-Instanciation-On-System-Engineering-Model
mirror of http://172.16.200.102/MOISE/Pattern-Instanciation-On-System-Engineering-Model.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
This project is a demonstrator of pattern instanciation on system engineering model (pseim), made by the MOISE project. It contains the metamodel of the pseim, graphical and textual editors, formal verification models (event-B) and examples.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
12 Commits
1 Branch
0 Tags
3.4 MiB
Tree: 72e69c8c5d
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '72e69c8c5d'
${ noResults }
Pattern-Instanciation-On-Sy.../Event-B/pseim/pattern_safety.bpr

1015 lines
91 KiB
Raw Normal View History Unescape

Update Event-B models and proofs
5 years ago
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.prFile version="1">
<org.eventb.core.prProof name="f_acycl/WD" org.eventb.core.confidence="1000" org.eventb.core.prFresh="m" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16,p17,p18,p19" org.eventb.core.prSets="Component,Link,Model,Port">
<org.eventb.core.lang name="L"/>
<org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(Port,IPort,OPort))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p8" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p20,p21"/>
<org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p20,p21"/>
<org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(Link,Transpose,Identity,Shift,First,Rotate))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p2" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p22,p23,p24,p25,p26,p27,p28,p29,p30,p31,p32"/>
<org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p22,p23,p24,p25,p26,p27,p28,p29,p30,p31,p32"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p38">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p33"/>
<org.eventb.core.prHypAction name="REWRITE1" org.eventb.core.prHidden="p3" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p34,p35,p36"/>
<org.eventb.core.prHypAction name="REWRITE2" org.eventb.core.prHidden="p14" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p37"/>
<org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p39"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p40"/>
<org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p41"/>
<org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p42"/>
<org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p43"/>
<org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p44"/>
<org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p45"/>
<org.eventb.core.prRule name="r3" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p38" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p46">
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∀ goal (frees m)" org.eventb.core.prGoal="p46" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p47">
<org.eventb.core.prIdent name="m" org.eventb.core.type="Model"/>
<org.eventb.core.prRule name="r5" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.prHyps="p7">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p10" org.eventb.core.prInfHyps="p48"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p10"/>
<org.eventb.core.prRule name="r5" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with toy_container=∅" org.eventb.core.prHyps="p11">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p49"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p48" org.eventb.core.prInfHyps="p50"/>
<org.eventb.core.prHypAction name="DESELECT2" org.eventb.core.prHyps="p1,p48"/>
<org.eventb.core.prRule name="r5" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with container_var={safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ ∅}" org.eventb.core.prGoal="p47" org.eventb.core.prHyps="p50">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p51">
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p51" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p52">
<org.eventb.core.prRule name="r6" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p52" org.eventb.core.prHyps="p17,p13,p19,p9,p7,p1,p11,p18,p6,p12,p15,p5,p10,p16,p20,p21,p22,p23,p24,p25,p26,p27,p28,p29,p30,p31,p32,p33,p34,p35,p36,p37,p48,p49,p50">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="(" org.eventb.core.prGoal="p53">
<org.eventb.core.prRule name="r5" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.prHyps="p7">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p10" org.eventb.core.prInfHyps="p48"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p10"/>
<org.eventb.core.prRule name="r5" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with toy_container=∅" org.eventb.core.prHyps="p11">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p49"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p48" org.eventb.core.prInfHyps="p50"/>
<org.eventb.core.prHypAction name="DESELECT2" org.eventb.core.prHyps="p1,p48"/>
<org.eventb.core.prRule name="r5" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with container_var={safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ ∅}" org.eventb.core.prGoal="p53" org.eventb.core.prHyps="p50">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p54">
<org.eventb.core.prRule name="r6" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p54" org.eventb.core.prHyps="p17,p13,p19,p9,p7,p1,p11,p18,p6,p12,p15,p5,p10,p16,p20,p21,p22,p23,p24,p25,p26,p27,p28,p29,p30,p31,p32,p33,p34,p35,p36,p37,p48,p49,p50">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="First" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.prIdent name="IPort" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.prIdent name="Identity" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.prIdent name="Inst" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="LKind" org.eventb.core.type="ℙ(ℙ(Link))"/>
<org.eventb.core.prIdent name="Mdl" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="OPort" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.prIdent name="Pat" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="Pattern" org.eventb.core.type="ℙ(Model)"/>
<org.eventb.core.prIdent name="Rotate" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.prIdent name="Shift" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.prIdent name="Transpose" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.prIdent name="ballot_box" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="components_var" org.eventb.core.type="ℙ(Model×ℙ(Component))"/>
<org.eventb.core.prIdent name="container_var" org.eventb.core.type="ℙ(Model×ℙ(Component×Component))"/>
<org.eventb.core.prIdent name="f_container_var" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="replicator" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="safety_comp" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="safety_container" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="safety_model" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="toy_app" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="toy_container" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="toy_inp_1" org.eventb.core.type="Port"/>
<org.eventb.core.prIdent name="toy_inp_2" org.eventb.core.type="Port"/>
<org.eventb.core.prIdent name="toy_model" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="toy_output" org.eventb.core.type="Port"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="toy_container∈Component ⇸ Component"/>
<org.eventb.core.prPred name="p39" org.eventb.core.predicate="Pattern⊆Model"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="partition(Link,Transpose,Identity,Shift,First,Rotate)"/>
<org.eventb.core.prPred name="p26" org.eventb.core.predicate="Transpose∩Rotate=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p53" org.eventb.core.predicate="container_var∈Model ⇸ ℙ(Component × Component)"/>
<org.eventb.core.prPred name="p48" org.eventb.core.predicate="container_var={safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ toy_container}"/>
<org.eventb.core.prPred name="p51" org.eventb.core.predicate="m∈dom({safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ (∅ ⦂ ℙ(Component×Component))})">
<org.eventb.core.prIdent name="m" org.eventb.core.type="Model"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p45" org.eventb.core.predicate="toy_app∈Component"/>
<org.eventb.core.prPred name="p38" org.eventb.core.predicate="(∀m⦂Model·m∈dom(container_var))∧container_var∈Model ⇸ ℙ(Component × Component)"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="Pat∈Pattern"/>
<org.eventb.core.prPred name="p27" org.eventb.core.predicate="Identity∩Shift=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="∀m⦂Model·m∈dom(container_var)∧container_var∈Model ⇸ ℙ(Component × Component)"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="f_container_var={replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="Model={safety_model,toy_model}"/>
<org.eventb.core.prPred name="p52" org.eventb.core.predicate="m∈{safety_model,toy_model}">
<org.eventb.core.prIdent name="m" org.eventb.core.type="Model"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p46" org.eventb.core.predicate="∀m⦂Model·m∈dom(container_var)"/>
<org.eventb.core.prPred name="p42" org.eventb.core.predicate="safety_comp∈Component"/>
<org.eventb.core.prPred name="p36" org.eventb.core.predicate="¬ballot_box=safety_comp"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="toy_container=(∅ ⦂ ℙ(Component×Component))"/>
<org.eventb.core.prPred name="p23" org.eventb.core.predicate="Transpose∩Identity=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p22" org.eventb.core.predicate="Link=Transpose∪Identity∪Shift∪First∪Rotate"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="safety_model≠toy_model"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="Port=IPort∪OPort"/>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="IPort∩OPort=(∅ ⦂ ℙ(Port))"/>
<org.eventb.core.prPred name="p54" org.eventb.core.predicate="{safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ (∅ ⦂ ℙ(Component×Component))}∈Model ⇸ ℙ(Component × Component)"/>
<org.eventb.core.prPred name="p43" org.eventb.core.predicate="safety_model∈Model"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="Mdl∈Model ∖ Pattern"/>
<org.eventb.core.prPred name="p29" org.eventb.core.predicate="Identity∩Rotate=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p35" org.eventb.core.predicate="¬replicator=safety_comp"/>
<org.eventb.core.prPred name="p33" org.eventb.core.predicate="¬Inst=Mdl"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="components_var={safety_model ↦ {replicator,ballot_box,safety_comp},toy_model ↦ {toy_app}}"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p37" org.eventb.core.predicate="¬safety_model=toy_model"/>
<org.eventb.core.prPred name="p50" org.eventb.core.predicate="container_var={safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ (∅ ⦂ ℙ(Component×Component))}"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="container_var={safety_model ↦ safety_container,toy_model ↦ toy_container}"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="toy_inp_2∈IPort"/>
<org.eventb.core.prPred name="p49" org.eventb.core.predicate="(∅ ⦂ ℙ(Component×Component))∈Component ⇸ Component"/>
<org.eventb.core.prPred name="p32" org.eventb.core.predicate="First∩Rotate=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p28" org.eventb.core.predicate="Identity∩First=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p44" org.eventb.core.predicate="toy_model∈Model"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="replicator≠ballot_box∧replicator≠safety_comp∧ballot_box≠safety_comp"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="Inst≠Mdl"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="toy_inp_1∈IPort"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="partition(Port,IPort,OPort)"/>
<org.eventb.core.prPred name="p30" org.eventb.core.predicate="Shift∩First=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p40" org.eventb.core.predicate="replicator∈Component"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="LKind={Transpose,Identity,Shift,First,Rotate}"/>
<org.eventb.core.prPred name="p24" org.eventb.core.predicate="Transpose∩Shift=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p41" org.eventb.core.predicate="ballot_box∈Component"/>
<org.eventb.core.prPred name="p47" org.eventb.core.predicate="m∈dom(container_var)">
<org.eventb.core.prIdent name="m" org.eventb.core.type="Model"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p34" org.eventb.core.predicate="¬replicator=ballot_box"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="toy_output∈OPort"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="Inst∈Model ∖ Pattern"/>
<org.eventb.core.prPred name="p31" org.eventb.core.predicate="Shift∩Rotate=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p25" org.eventb.core.predicate="Transpose∩First=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
<org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
<org.eventb.core.prReas name="r6" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalML:1"/>
<org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
<org.eventb.core.prReas name="r3" org.eventb.core.prRID="org.eventb.core.seqprover.conj:0"/>
<org.eventb.core.prReas name="r4" org.eventb.core.prRID="org.eventb.core.seqprover.allI"/>
<org.eventb.core.prReas name="r5" org.eventb.core.prRID="org.eventb.core.seqprover.eq:1"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="f_acycl/THM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16,p17,p18,p19,p20,p21,p22" org.eventb.core.prSets="Component,Model,Port">
<org.eventb.core.lang name="L"/>
<org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="sl/ds" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="SELECT0" org.eventb.core.prHyps="p9,p21,p3,p16"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="CVC3" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16,p17,p18,p19,p20,p21,p22">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="R1000"/>
<org.eventb.core.prString name=".config_id" org.eventb.core.prSValue="CVC3"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="IPort" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.prIdent name="Mdl" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="OPort" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.prIdent name="Pat" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="Pattern" org.eventb.core.type="ℙ(Model)"/>
<org.eventb.core.prIdent name="ballot_box" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="components_var" org.eventb.core.type="ℙ(Model×ℙ(Component))"/>
<org.eventb.core.prIdent name="container_var" org.eventb.core.type="ℙ(Model×ℙ(Component×Component))"/>
<org.eventb.core.prIdent name="f_container_var" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="replicator" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="safety_comp" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="safety_container" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="safety_model" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="toy_app" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="toy_container" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="toy_inp_1" org.eventb.core.type="Port"/>
<org.eventb.core.prIdent name="toy_inp_2" org.eventb.core.type="Port"/>
<org.eventb.core.prIdent name="toy_model" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="toy_output" org.eventb.core.type="Port"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="toy_container∈Component ⇸ Component"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="toy_model∈Model"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="Pattern⊆Model"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="safety_comp∈Component"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="∀m⦂Model·container_var(m)⊆f_container_var∧f_container_var;f_container_var⊆f_container_var∧(id ⦂ ℙ(Component×Component))∩f_container_var=(∅ ⦂ ℙ(Component×Component))"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="replicator≠ballot_box∧replicator≠safety_comp∧ballot_box≠safety_comp"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="toy_inp_1∈IPort"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="components_var={safety_model ↦ {replicator,ballot_box,safety_comp},toy_model ↦ {toy_app}}"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(Port,IPort,OPort)"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="replicator∈Component"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="toy_app∈Component"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="toy_container=(∅ ⦂ ℙ(Component×Component))"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="container_var={safety_model ↦ safety_container,toy_model ↦ toy_container}"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="toy_inp_2∈IPort"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="ballot_box∈Component"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="Pat∈Pattern"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="safety_model≠toy_model"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="safety_model∈Model"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="toy_output∈OPort"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="f_container_var={replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="Mdl∈Model ∖ Pattern"/>
<org.eventb.core.prPred name="p22" org.eventb.core.predicate="Model={safety_model,toy_model}"/>
<org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.smt.core.externalSMT"/>
<org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.mngHyp"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="c_multiplicity_assign&#10;/WD" org.eventb.core.confidence="1000" org.eventb.core.prFresh="pc" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16,p17,p18,p19,p20,p21,p22,p23" org.eventb.core.prSets="Component,Link,Model,Port">
<org.eventb.core.lang name="L"/>
<org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(Port,IPort,OPort))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p9" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p24,p25"/>
<org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p24,p25"/>
<org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(Link,Transpose,Identity,Shift,First,Rotate))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p3" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p26,p27,p28,p29,p30,p31,p32,p33,p34,p35,p36"/>
<org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p26,p27,p28,p29,p30,p31,p32,p33,p34,p35,p36"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p5" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p37"/>
<org.eventb.core.prHypAction name="REWRITE1" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p38,p39,p40"/>
<org.eventb.core.prHypAction name="REWRITE2" org.eventb.core.prHidden="p17" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p41"/>
<org.eventb.core.prHypAction name="REWRITE3" org.eventb.core.prHidden="p2" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p42,p43,p44"/>
<org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p45"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p46"/>
<org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p47"/>
<org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p48"/>
<org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p49"/>
<org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p50"/>
<org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p51"/>
<org.eventb.core.prRule name="r3" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p52">
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.prHyps="p8">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p11" org.eventb.core.prInfHyps="p53"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p11"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with toy_container=∅" org.eventb.core.prHyps="p12">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p54"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p53" org.eventb.core.prInfHyps="p55"/>
<org.eventb.core.prHypAction name="DESELECT2" org.eventb.core.prHyps="p1,p53"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with f_container_var={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.prHyps="p19">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p42" org.eventb.core.prInfHyps="p56"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p43" org.eventb.core.prInfHyps="p57"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p44" org.eventb.core.prInfHyps="p58"/>
<org.eventb.core.prHypAction name="DESELECT3" org.eventb.core.prHyps="p42,p43,p44"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with c_multiplicity_var={safety_model ↦ {safety_comp ↦ 1,replicator ↦ 3,ballot_box ↦ 1}}" org.eventb.core.prGoal="p52" org.eventb.core.prHyps="p15">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p59">
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p59" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p60">
<org.eventb.core.prRule name="r5" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p60" org.eventb.core.prHyps=""/>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="(" org.eventb.core.prGoal="p61">
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.prHyps="p8">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p11" org.eventb.core.prInfHyps="p53"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p11"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with toy_container=∅" org.eventb.core.prHyps="p12">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p54"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p53" org.eventb.core.prInfHyps="p55"/>
<org.eventb.core.prHypAction name="DESELECT2" org.eventb.core.prHyps="p1,p53"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with f_container_var={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.prHyps="p19">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p42" org.eventb.core.prInfHyps="p56"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p43" org.eventb.core.prInfHyps="p57"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p44" org.eventb.core.prInfHyps="p58"/>
<org.eventb.core.prHypAction name="DESELECT3" org.eventb.core.prHyps="p42,p43,p44"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with c_multiplicity_var={safety_model ↦ {safety_comp ↦ 1,replicator ↦ 3,ballot_box ↦ 1}}" org.eventb.core.prGoal="p61" org.eventb.core.prHyps="p15">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p62">
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with container_var={safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ ∅}" org.eventb.core.prHyps="p55">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p56" org.eventb.core.prInfHyps="p63"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p56"/>
<org.eventb.core.prRule name="r6" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p62" org.eventb.core.prHyps="p20,p14,p23,p10,p8,p1,p12,p22,p7,p13,p18,p6,p11,p19,p21,p16,p15,p24,p25,p26,p27,p28,p29,p30,p31,p32,p33,p34,p35,p36,p37,p38,p39,p40,p41,p42,p43,p44,p53,p54,p55,p56,p57,p58,p63">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name=")" org.eventb.core.prGoal="p64">
<org.eventb.core.prRule name="r7" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∀ goal (frees pc)" org.eventb.core.prGoal="p64" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p65">
<org.eventb.core.prIdent name="pc" org.eventb.core.type="Component"/>
<org.eventb.core.prRule name="r8" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⇒ goal" org.eventb.core.prGoal="p65" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p67" org.eventb.core.prHyps="p66">
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.prHyps="p8">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p11" org.eventb.core.prInfHyps="p53"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p11"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with toy_container=∅" org.eventb.core.prHyps="p12">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p54"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p53" org.eventb.core.prInfHyps="p55"/>
<org.eventb.core.prHypAction name="DESELECT2" org.eventb.core.prHyps="p1,p53"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with f_container_var={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.prHyps="p19">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p42" org.eventb.core.prInfHyps="p56"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p43" org.eventb.core.prInfHyps="p57"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p44" org.eventb.core.prInfHyps="p58"/>
<org.eventb.core.prHypAction name="DESELECT3" org.eventb.core.prHyps="p42,p43,p44"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with inst_components_par={safety_comp ↦ toy_app}" org.eventb.core.prGoal="p67" org.eventb.core.prHyps="p21">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p69">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p66" org.eventb.core.prInfHyps="p68"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p66"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p68" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p70"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with container_var={safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ ∅}" org.eventb.core.prHyps="p55">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p56" org.eventb.core.prInfHyps="p63"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p56"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with pc=safety_comp" org.eventb.core.prGoal="p69" org.eventb.core.prHyps="p70">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p71">
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p71" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p60">
<org.eventb.core.prRule name="r5" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p60" org.eventb.core.prHyps=""/>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="First" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.prIdent name="IPort" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.prIdent name="Identity" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.prIdent name="Inst" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="LKind" org.eventb.core.type="ℙ(ℙ(Link))"/>
<org.eventb.core.prIdent name="Mdl" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="OPort" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.prIdent name="Pat" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="Pattern" org.eventb.core.type="ℙ(Model)"/>
<org.eventb.core.prIdent name="Rotate" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.prIdent name="Shift" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.prIdent name="Transpose" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.prIdent name="ballot_box" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="c_mult_others_par" org.eventb.core.type="ℙ(Component×ℤ)"/>
<org.eventb.core.prIdent name="c_multiplicity_var" org.eventb.core.type="ℙ(Model×ℙ(Component×ℤ))"/>
<org.eventb.core.prIdent name="components_var" org.eventb.core.type="ℙ(Model×ℙ(Component))"/>
<org.eventb.core.prIdent name="container_var" org.eventb.core.type="ℙ(Model×ℙ(Component×Component))"/>
<org.eventb.core.prIdent name="f_container_var" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="inst_components_par" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="replicator" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="safety_comp" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="safety_container" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="safety_model" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="toy_app" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="toy_container" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="toy_inp_1" org.eventb.core.type="Port"/>
<org.eventb.core.prIdent name="toy_inp_2" org.eventb.core.type="Port"/>
<org.eventb.core.prIdent name="toy_model" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="toy_output" org.eventb.core.type="Port"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="toy_container∈Component ⇸ Component"/>
<org.eventb.core.prPred name="p45" org.eventb.core.predicate="Pattern⊆Model"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(Link,Transpose,Identity,Shift,First,Rotate)"/>
<org.eventb.core.prPred name="p30" org.eventb.core.predicate="Transpose∩Rotate=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p68" org.eventb.core.predicate="pc∈dom({safety_comp ↦ toy_app})">
<org.eventb.core.prIdent name="pc" org.eventb.core.type="Component"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p53" org.eventb.core.predicate="container_var={safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ toy_container}"/>
<org.eventb.core.prPred name="p51" org.eventb.core.predicate="toy_app∈Component"/>
<org.eventb.core.prPred name="p64" org.eventb.core.predicate="∀pc⦂Component·pc∈dom(inst_components_par)⇒finite(inst_components_par[{pc}])"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="Pat∈Pattern"/>
<org.eventb.core.prPred name="p65" org.eventb.core.predicate="pc∈dom(inst_components_par)⇒finite(inst_components_par[{pc}])">
<org.eventb.core.prIdent name="pc" org.eventb.core.type="Component"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p67" org.eventb.core.predicate="finite(inst_components_par[{pc}])">
<org.eventb.core.prIdent name="pc" org.eventb.core.type="Component"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p31" org.eventb.core.predicate="Identity∩Shift=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p70" org.eventb.core.predicate="pc=safety_comp">
<org.eventb.core.prIdent name="pc" org.eventb.core.type="Component"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="f_container_var={replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p22" org.eventb.core.predicate="Model={safety_model,toy_model}"/>
<org.eventb.core.prPred name="p43" org.eventb.core.predicate="f_container_var;f_container_var⊆f_container_var"/>
<org.eventb.core.prPred name="p48" org.eventb.core.predicate="safety_comp∈Component"/>
<org.eventb.core.prPred name="p40" org.eventb.core.predicate="¬ballot_box=safety_comp"/>
<org.eventb.core.prPred name="p61" org.eventb.core.predicate="c_multiplicity_var∈Model ⇸ ℙ(Component × ℤ)"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="toy_container=(∅ ⦂ ℙ(Component×Component))"/>
<org.eventb.core.prPred name="p27" org.eventb.core.predicate="Transpose∩Identity=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p26" org.eventb.core.predicate="Link=Transpose∪Identity∪Shift∪First∪Rotate"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="c_mult_others_par={replicator ↦ 3,ballot_box ↦ 1}"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="safety_model≠toy_model"/>
<org.eventb.core.prPred name="p24" org.eventb.core.predicate="Port=IPort∪OPort"/>
<org.eventb.core.prPred name="p25" org.eventb.core.predicate="IPort∩OPort=(∅ ⦂ ℙ(Port))"/>
<org.eventb.core.prPred name="p49" org.eventb.core.predicate="safety_model∈Model"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="Mdl∈Model ∖ Pattern"/>
<org.eventb.core.prPred name="p33" org.eventb.core.predicate="Identity∩Rotate=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p39" org.eventb.core.predicate="¬replicator=safety_comp"/>
<org.eventb.core.prPred name="p37" org.eventb.core.predicate="¬Inst=Mdl"/>
<org.eventb.core.prPred name="p58" org.eventb.core.predicate="(id ⦂ ℙ(Component×Component))∩{replicator ↦ safety_comp,ballot_box ↦ safety_comp}=(∅ ⦂ ℙ(Component×Component))"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="∀m⦂Model·container_var(m)⊆f_container_var∧f_container_var;f_container_var⊆f_container_var∧(id ⦂ ℙ(Component×Component))∩f_container_var=(∅ ⦂ ℙ(Component×Component))"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="components_var={safety_model ↦ {replicator,ballot_box,safety_comp},toy_model ↦ {toy_app}}"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p41" org.eventb.core.predicate="¬safety_model=toy_model"/>
<org.eventb.core.prPred name="p55" org.eventb.core.predicate="container_var={safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ (∅ ⦂ ℙ(Component×Component))}"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="container_var={safety_model ↦ safety_container,toy_model ↦ toy_container}"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="toy_inp_2∈IPort"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="c_multiplicity_var={safety_model ↦ {safety_comp ↦ 1,replicator ↦ 3,ballot_box ↦ 1}}"/>
<org.eventb.core.prPred name="p54" org.eventb.core.predicate="(∅ ⦂ ℙ(Component×Component))∈Component ⇸ Component"/>
<org.eventb.core.prPred name="p62" org.eventb.core.predicate="{safety_model ↦ {safety_comp ↦ 1,replicator ↦ 3,ballot_box ↦ 1}}∈Model ⇸ ℙ(Component × ℤ)"/>
<org.eventb.core.prPred name="p36" org.eventb.core.predicate="First∩Rotate=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p32" org.eventb.core.predicate="Identity∩First=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p52" org.eventb.core.predicate="safety_model∈dom(c_multiplicity_var)"/>
<org.eventb.core.prPred name="p66" org.eventb.core.predicate="pc∈dom(inst_components_par)">
<org.eventb.core.prIdent name="pc" org.eventb.core.type="Component"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p50" org.eventb.core.predicate="toy_model∈Model"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="safety_model∈dom(c_multiplicity_var)∧c_multiplicity_var∈Model ⇸ ℙ(Component × ℤ)∧(∀pc⦂Component·pc∈dom(inst_components_par)⇒finite(inst_components_par[{pc}]))"/>
<org.eventb.core.prPred name="p42" org.eventb.core.predicate="∀m⦂Model·container_var(m)⊆f_container_var"/>
<org.eventb.core.prPred name="p60" org.eventb.core.predicate="⊤"/>
<org.eventb.core.prPred name="p63" org.eventb.core.predicate="∀m⦂Model·{safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ (∅ ⦂ ℙ(Component×Component))}(m)⊆{replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="replicator≠ballot_box∧replicator≠safety_comp∧ballot_box≠safety_comp"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="Inst≠Mdl"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="toy_inp_1∈IPort"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(Port,IPort,OPort)"/>
<org.eventb.core.prPred name="p34" org.eventb.core.predicate="Shift∩First=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p46" org.eventb.core.predicate="replicator∈Component"/>
<org.eventb.core.prPred name="p57" org.eventb.core.predicate="{replicator ↦ safety_comp,ballot_box ↦ safety_comp};{replicator ↦ safety_comp,ballot_box ↦ safety_comp}⊆{replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="LKind={Transpose,Identity,Shift,First,Rotate}"/>
<org.eventb.core.prPred name="p71" org.eventb.core.predicate="finite({safety_comp ↦ toy_app}[{safety_comp}])"/>
<org.eventb.core.prPred name="p28" org.eventb.core.predicate="Transpose∩Shift=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p47" org.eventb.core.predicate="ballot_box∈Component"/>
<org.eventb.core.prPred name="p38" org.eventb.core.predicate="¬replicator=ballot_box"/>
<org.eventb.core.prPred name="p56" org.eventb.core.predicate="∀m⦂Model·container_var(m)⊆{replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="toy_output∈OPort"/>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="inst_components_par={safety_comp ↦ toy_app}"/>
<org.eventb.core.prPred name="p59" org.eventb.core.predicate="safety_model∈dom({safety_model ↦ {safety_comp ↦ 1,replicator ↦ 3,ballot_box ↦ 1}})"/>
<org.eventb.core.prPred name="p44" org.eventb.core.predicate="(id ⦂ ℙ(Component×Component))∩f_container_var=(∅ ⦂ ℙ(Component×Component))"/>
<org.eventb.core.prPred name="p23" org.eventb.core.predicate="Inst∈Model ∖ Pattern"/>
<org.eventb.core.prPred name="p35" org.eventb.core.predicate="Shift∩Rotate=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p69" org.eventb.core.predicate="finite({safety_comp ↦ toy_app}[{pc}])">
<org.eventb.core.prIdent name="pc" org.eventb.core.type="Component"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p29" org.eventb.core.predicate="Transpose∩First=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
<org.eventb.core.prReas name="r8" org.eventb.core.prRID="org.eventb.core.seqprover.impI"/>
<org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
<org.eventb.core.prReas name="r6" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalML:1"/>
<org.eventb.core.prReas name="r5" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
<org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
<org.eventb.core.prReas name="r3" org.eventb.core.prRID="org.eventb.core.seqprover.conj:0"/>
<org.eventb.core.prReas name="r4" org.eventb.core.prRID="org.eventb.core.seqprover.eq:1"/>
<org.eventb.core.prReas name="r7" org.eventb.core.prRID="org.eventb.core.seqprover.allI"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="c_multiplicity_assign&#10;/THM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prHyps="p0,p1,p2,p3,p4,p5,p6" org.eventb.core.prSets="Component,Model">
<org.eventb.core.lang name="L"/>
<org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="sl/ds" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="SELECT0" org.eventb.core.prHyps="p7,p4,p0,p5,p2,p8,p9,p10,p11"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Z3" org.eventb.core.prHyps="p0,p1,p2,p3,p4,p5,p6">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="R1000"/>
<org.eventb.core.prString name=".config_id" org.eventb.core.prSValue="Z3"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="Inst" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="Mdl" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="Pat" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="Pattern" org.eventb.core.type="ℙ(Model)"/>
<org.eventb.core.prIdent name="ballot_box" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="replicator" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="safety_comp" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="safety_container" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="safety_model" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="toy_model" org.eventb.core.type="Model"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="Pat∈Pattern"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="Pattern⊆Model"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="replicator≠ballot_box∧replicator≠safety_comp∧ballot_box≠safety_comp"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="Inst≠Mdl"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="c_multiplicity_var∈Model ⇸ ℙ(Component × ℤ)">
<org.eventb.core.prIdent name="c_multiplicity_var" org.eventb.core.type="ℙ(Model×ℙ(Component×ℤ))"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="partition(Port,IPort,OPort)">
<org.eventb.core.prIdent name="IPort" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.prIdent name="OPort" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.prIdent name="Port" org.eventb.core.type="ℙ(Port)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="Mdl∈Model ∖ Pattern"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="Inst∈Model ∖ Pattern"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="Model={safety_model,toy_model}"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="∀pc⦂Component·pc∈dom(inst_components_par)⇒finite(inst_components_par[{pc}])">
<org.eventb.core.prIdent name="inst_components_par" org.eventb.core.type="ℙ(Component×Component)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="safety_model∈dom(c_multiplicity_var)">
<org.eventb.core.prIdent name="c_multiplicity_var" org.eventb.core.type="ℙ(Model×ℙ(Component×ℤ))"/>
</org.eventb.core.prPred>
<org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.mngHyp"/>
<org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.smt.core.externalSMT"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="to_unfold_c_var&#10;/WD" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16,p17,p18,p19,p20,p21,p22,p23,p24,p25,p26,p27,p28" org.eventb.core.prSets="Component,Link,Model,Port">
<org.eventb.core.lang name="L"/>
<org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(Port,IPort,OPort))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p19" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p29,p30"/>
<org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p29,p30"/>
<org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(Link,Transpose,Identity,Shift,First,Rotate))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p31,p32,p33,p34,p35,p36,p37,p38,p39,p40,p41"/>
<org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p31,p32,p33,p34,p35,p36,p37,p38,p39,p40,p41"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p16" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p42"/>
<org.eventb.core.prHypAction name="REWRITE1" org.eventb.core.prHidden="p15" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p43,p44,p45"/>
<org.eventb.core.prHypAction name="REWRITE2" org.eventb.core.prHidden="p24" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p46"/>
<org.eventb.core.prHypAction name="REWRITE3" org.eventb.core.prHidden="p3" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p47,p48,p49"/>
<org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p50"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p51"/>
<org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p52"/>
<org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p53"/>
<org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p54"/>
<org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p55"/>
<org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p56"/>
<org.eventb.core.prRule name="r3" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p57">
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.prHyps="p6">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p8" org.eventb.core.prInfHyps="p58"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p8"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with toy_container=∅" org.eventb.core.prHyps="p22">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p59"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p58" org.eventb.core.prInfHyps="p60"/>
<org.eventb.core.prHypAction name="DESELECT2" org.eventb.core.prHyps="p1,p58"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with components_var={safety_model ↦ {replicator,ballot_box,safety_comp},toy_model ↦ {toy_app}}" org.eventb.core.prGoal="p57" org.eventb.core.prHyps="p5">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p61">
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p61" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p62">
<org.eventb.core.prRule name="r5" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p62" org.eventb.core.prHyps=""/>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="(" org.eventb.core.prGoal="p63">
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.prHyps="p6">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p8" org.eventb.core.prInfHyps="p58"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p8"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with toy_container=∅" org.eventb.core.prHyps="p22">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p59"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p58" org.eventb.core.prInfHyps="p60"/>
<org.eventb.core.prHypAction name="DESELECT2" org.eventb.core.prHyps="p1,p58"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with components_var={safety_model ↦ {replicator,ballot_box,safety_comp},toy_model ↦ {toy_app}}" org.eventb.core.prGoal="p63" org.eventb.core.prHyps="p5">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p64">
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with f_container_var={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.prHyps="p12">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p47" org.eventb.core.prInfHyps="p65"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p48" org.eventb.core.prInfHyps="p66"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p49" org.eventb.core.prInfHyps="p67"/>
<org.eventb.core.prHypAction name="DESELECT3" org.eventb.core.prHyps="p47,p48,p49"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with inst_components_par={safety_comp ↦ toy_app}" org.eventb.core.prHyps="p27">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p2" org.eventb.core.prInfHyps="p68"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p2"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p68" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p69"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with c_mult_others_par={replicator ↦ 3,ballot_box ↦ 1}" org.eventb.core.prHyps="p23">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p69" org.eventb.core.prInfHyps="p70"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p69"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with c_multiplicity_var={safety_model ↦ {safety_comp ↦ 1,replicator ↦ 3,ballot_box ↦ 1}}" org.eventb.core.prHyps="p11">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p70" org.eventb.core.prInfHyps="p71"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p70"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p71" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p72"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with container_var={safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ ∅}" org.eventb.core.prHyps="p60">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p65" org.eventb.core.prInfHyps="p73"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p65"/>
<org.eventb.core.prRule name="r6" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p64" org.eventb.core.prHyps="p26,p10,p28,p20,p6,p1,p22,p13,p18,p9,p25,p5,p8,p12,p27,p23,p11,p2,p14,p17,p7,p21,p29,p30,p31,p32,p33,p34,p35,p36,p37,p38,p39,p40,p41,p42,p43,p44,p45,p46,p47,p48,p49,p58,p59,p60,p65,p66,p67,p69,p70,p72,p73">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name=")" org.eventb.core.prGoal="p74">
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.prHyps="p6">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p8" org.eventb.core.prInfHyps="p58"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p8"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with toy_container=∅" org.eventb.core.prHyps="p22">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p59"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p58" org.eventb.core.prInfHyps="p60"/>
<org.eventb.core.prHypAction name="DESELECT2" org.eventb.core.prHyps="p1,p58"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with f_container_var={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.prHyps="p12">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p47" org.eventb.core.prInfHyps="p65"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p48" org.eventb.core.prInfHyps="p66"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p49" org.eventb.core.prInfHyps="p67"/>
<org.eventb.core.prHypAction name="DESELECT3" org.eventb.core.prHyps="p47,p48,p49"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with inst_components_par={safety_comp ↦ toy_app}" org.eventb.core.prHyps="p27">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p2" org.eventb.core.prInfHyps="p68"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p2"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p68" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p69"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with c_mult_others_par={replicator ↦ 3,ballot_box ↦ 1}" org.eventb.core.prHyps="p23">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p69" org.eventb.core.prInfHyps="p70"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p69"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with c_multiplicity_var={safety_model ↦ {safety_comp ↦ 1,replicator ↦ 3,ballot_box ↦ 1}}" org.eventb.core.prHyps="p11">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p70" org.eventb.core.prInfHyps="p71"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p70"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p71" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p72"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with container_var={safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ ∅}" org.eventb.core.prGoal="p74" org.eventb.core.prHyps="p60">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p75">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p65" org.eventb.core.prInfHyps="p73"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p65"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p75" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p62">
<org.eventb.core.prRule name="r5" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p62" org.eventb.core.prHyps=""/>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="*" org.eventb.core.prGoal="p76">
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.prHyps="p6">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p8" org.eventb.core.prInfHyps="p58"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p8"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with toy_container=∅" org.eventb.core.prHyps="p22">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p59"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p58" org.eventb.core.prInfHyps="p60"/>
<org.eventb.core.prHypAction name="DESELECT2" org.eventb.core.prHyps="p1,p58"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with f_container_var={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.prHyps="p12">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p47" org.eventb.core.prInfHyps="p65"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p48" org.eventb.core.prInfHyps="p66"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p49" org.eventb.core.prInfHyps="p67"/>
<org.eventb.core.prHypAction name="DESELECT3" org.eventb.core.prHyps="p47,p48,p49"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with inst_components_par={safety_comp ↦ toy_app}" org.eventb.core.prHyps="p27">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p2" org.eventb.core.prInfHyps="p68"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p2"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p68" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p69"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with c_mult_others_par={replicator ↦ 3,ballot_box ↦ 1}" org.eventb.core.prHyps="p23">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p69" org.eventb.core.prInfHyps="p70"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p69"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with c_multiplicity_var={safety_model ↦ {safety_comp ↦ 1,replicator ↦ 3,ballot_box ↦ 1}}" org.eventb.core.prHyps="p11">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p70" org.eventb.core.prInfHyps="p71"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p70"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p71" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p72"/>
<org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with container_var={safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ ∅}" org.eventb.core.prGoal="p76" org.eventb.core.prHyps="p60">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p77">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p65" org.eventb.core.prInfHyps="p73"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p65"/>
<org.eventb.core.prRule name="r6" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p77" org.eventb.core.prHyps="p26,p10,p28,p20,p6,p1,p22,p13,p18,p9,p25,p5,p8,p12,p27,p23,p11,p2,p14,p17,p7,p21,p29,p30,p31,p32,p33,p34,p35,p36,p37,p38,p39,p40,p41,p42,p43,p44,p45,p46,p47,p48,p49,p58,p59,p60,p65,p66,p67,p69,p70,p72,p73">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="First" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.prIdent name="IPort" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.prIdent name="Identity" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.prIdent name="Inst" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="LKind" org.eventb.core.type="ℙ(ℙ(Link))"/>
<org.eventb.core.prIdent name="Mdl" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="OPort" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.prIdent name="Pat" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="Pattern" org.eventb.core.type="ℙ(Model)"/>
<org.eventb.core.prIdent name="Rotate" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.prIdent name="Shift" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.prIdent name="Transpose" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.prIdent name="ballot_box" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="c_mult_others_par" org.eventb.core.type="ℙ(Component×ℤ)"/>
<org.eventb.core.prIdent name="c_multiplicity_var" org.eventb.core.type="ℙ(Model×ℙ(Component×ℤ))"/>
<org.eventb.core.prIdent name="components_var" org.eventb.core.type="ℙ(Model×ℙ(Component))"/>
<org.eventb.core.prIdent name="container_var" org.eventb.core.type="ℙ(Model×ℙ(Component×Component))"/>
<org.eventb.core.prIdent name="f_container_var" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="inst_components_par" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="replicator" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="safety_comp" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="safety_container" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="safety_model" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="to_unfold_c_var" org.eventb.core.type="ℙ(Component)"/>
<org.eventb.core.prIdent name="toy_app" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="toy_container" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="toy_inp_1" org.eventb.core.type="Port"/>
<org.eventb.core.prIdent name="toy_inp_2" org.eventb.core.type="Port"/>
<org.eventb.core.prIdent name="toy_model" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="toy_output" org.eventb.core.type="Port"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="toy_container∈Component ⇸ Component"/>
<org.eventb.core.prPred name="p50" org.eventb.core.predicate="Pattern⊆Model"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="partition(Link,Transpose,Identity,Shift,First,Rotate)"/>
<org.eventb.core.prPred name="p35" org.eventb.core.predicate="Transpose∩Rotate=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p76" org.eventb.core.predicate="container_var∈Model ⇸ ℙ(Component × Component)"/>
<org.eventb.core.prPred name="p58" org.eventb.core.predicate="container_var={safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ toy_container}"/>
<org.eventb.core.prPred name="p56" org.eventb.core.predicate="toy_app∈Component"/>
<org.eventb.core.prPred name="p74" org.eventb.core.predicate="safety_model∈dom(container_var)"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="∀pc⦂Component·pc∈dom(inst_components_par)⇒finite(inst_components_par[{pc}])"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="Pat∈Pattern"/>
<org.eventb.core.prPred name="p36" org.eventb.core.predicate="Identity∩Shift=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p70" org.eventb.core.predicate="c_multiplicity_var(safety_model)={replicator ↦ 3,ballot_box ↦ 1}{pc⦂Component·pc=safety_comp ∣ pc ↦ card({safety_comp ↦ toy_app}[{pc}])}"/>
<org.eventb.core.prPred name="p72" org.eventb.core.predicate="{safety_comp ↦ 1,replicator ↦ 3,ballot_box ↦ 1}={replicator ↦ 3,ballot_box ↦ 1}{pc⦂Component·pc=safety_comp ∣ pc ↦ card({safety_comp ↦ toy_app}[{pc}])}"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="f_container_var={replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p71" org.eventb.core.predicate="{safety_model ↦ {safety_comp ↦ 1,replicator ↦ 3,ballot_box ↦ 1}}(safety_model)={replicator ↦ 3,ballot_box ↦ 1}{pc⦂Component·pc=safety_comp ∣ pc ↦ card({safety_comp ↦ toy_app}[{pc}])}"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="Model={safety_model,toy_model}"/>
<org.eventb.core.prPred name="p48" org.eventb.core.predicate="f_container_var;f_container_var⊆f_container_var"/>
<org.eventb.core.prPred name="p53" org.eventb.core.predicate="safety_comp∈Component"/>
<org.eventb.core.prPred name="p45" org.eventb.core.predicate="¬ballot_box=safety_comp"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="c_multiplicity_var∈Model ⇸ ℙ(Component × ℤ)"/>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="to_unfold_c_var={safety_comp}"/>
<org.eventb.core.prPred name="p22" org.eventb.core.predicate="toy_container=(∅ ⦂ ℙ(Component×Component))"/>
<org.eventb.core.prPred name="p32" org.eventb.core.predicate="Transpose∩Identity=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p31" org.eventb.core.predicate="Link=Transpose∪Identity∪Shift∪First∪Rotate"/>
<org.eventb.core.prPred name="p23" org.eventb.core.predicate="c_mult_others_par={replicator ↦ 3,ballot_box ↦ 1}"/>
<org.eventb.core.prPred name="p24" org.eventb.core.predicate="safety_model≠toy_model"/>
<org.eventb.core.prPred name="p29" org.eventb.core.predicate="Port=IPort∪OPort"/>
<org.eventb.core.prPred name="p30" org.eventb.core.predicate="IPort∩OPort=(∅ ⦂ ℙ(Port))"/>
<org.eventb.core.prPred name="p77" org.eventb.core.predicate="{safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ (∅ ⦂ ℙ(Component×Component))}∈Model ⇸ ℙ(Component × Component)"/>
<org.eventb.core.prPred name="p54" org.eventb.core.predicate="safety_model∈Model"/>
<org.eventb.core.prPred name="p26" org.eventb.core.predicate="Mdl∈Model ∖ Pattern"/>
<org.eventb.core.prPred name="p38" org.eventb.core.predicate="Identity∩Rotate=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p44" org.eventb.core.predicate="¬replicator=safety_comp"/>
<org.eventb.core.prPred name="p42" org.eventb.core.predicate="¬Inst=Mdl"/>
<org.eventb.core.prPred name="p67" org.eventb.core.predicate="(id ⦂ ℙ(Component×Component))∩{replicator ↦ safety_comp,ballot_box ↦ safety_comp}=(∅ ⦂ ℙ(Component×Component))"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="c_multiplicity_var(safety_model)=c_mult_others_par{pc⦂Component·pc∈dom(inst_components_par) ∣ pc ↦ card(inst_components_par[{pc}])}"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="∀m⦂Model·container_var(m)⊆f_container_var∧f_container_var;f_container_var⊆f_container_var∧(id ⦂ ℙ(Component×Component))∩f_container_var=(∅ ⦂ ℙ(Component×Component))"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="components_var={safety_model ↦ {replicator,ballot_box,safety_comp},toy_model ↦ {toy_app}}"/>
<org.eventb.core.prPred name="p63" org.eventb.core.predicate="components_var∈Model ⇸ ℙ(Component)"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p46" org.eventb.core.predicate="¬safety_model=toy_model"/>
<org.eventb.core.prPred name="p60" org.eventb.core.predicate="container_var={safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ (∅ ⦂ ℙ(Component×Component))}"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="container_var={safety_model ↦ safety_container,toy_model ↦ toy_container}"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="toy_inp_2∈IPort"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="safety_model∈dom(components_var)∧components_var∈Model ⇸ ℙ(Component)∧safety_model∈dom(container_var)∧container_var∈Model ⇸ ℙ(Component × Component)"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="c_multiplicity_var={safety_model ↦ {safety_comp ↦ 1,replicator ↦ 3,ballot_box ↦ 1}}"/>
<org.eventb.core.prPred name="p61" org.eventb.core.predicate="safety_model∈dom({safety_model ↦ {replicator,ballot_box,safety_comp},toy_model ↦ {toy_app}})"/>
<org.eventb.core.prPred name="p59" org.eventb.core.predicate="(∅ ⦂ ℙ(Component×Component))∈Component ⇸ Component"/>
<org.eventb.core.prPred name="p64" org.eventb.core.predicate="{safety_model ↦ {replicator,ballot_box,safety_comp},toy_model ↦ {toy_app}}∈Model ⇸ ℙ(Component)"/>
<org.eventb.core.prPred name="p68" org.eventb.core.predicate="c_multiplicity_var(safety_model)=c_mult_others_par{pc⦂Component·pc∈dom({safety_comp ↦ toy_app}) ∣ pc ↦ card({safety_comp ↦ toy_app}[{pc}])}"/>
<org.eventb.core.prPred name="p41" org.eventb.core.predicate="First∩Rotate=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p37" org.eventb.core.predicate="Identity∩First=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p75" org.eventb.core.predicate="safety_model∈dom({safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ (∅ ⦂ ℙ(Component×Component))})"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="safety_model∈dom(c_multiplicity_var)"/>
<org.eventb.core.prPred name="p55" org.eventb.core.predicate="toy_model∈Model"/>
<org.eventb.core.prPred name="p47" org.eventb.core.predicate="∀m⦂Model·container_var(m)⊆f_container_var"/>
<org.eventb.core.prPred name="p62" org.eventb.core.predicate="⊤"/>
<org.eventb.core.prPred name="p73" org.eventb.core.predicate="∀m⦂Model·{safety_model ↦ {replicator ↦ safety_comp,ballot_box ↦ safety_comp},toy_model ↦ (∅ ⦂ ℙ(Component×Component))}(m)⊆{replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="replicator≠ballot_box∧replicator≠safety_comp∧ballot_box≠safety_comp"/>
<org.eventb.core.prPred name="p57" org.eventb.core.predicate="safety_model∈dom(components_var)"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="Inst≠Mdl"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="toy_inp_1∈IPort"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="partition(Port,IPort,OPort)"/>
<org.eventb.core.prPred name="p39" org.eventb.core.predicate="Shift∩First=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p51" org.eventb.core.predicate="replicator∈Component"/>
<org.eventb.core.prPred name="p66" org.eventb.core.predicate="{replicator ↦ safety_comp,ballot_box ↦ safety_comp};{replicator ↦ safety_comp,ballot_box ↦ safety_comp}⊆{replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="LKind={Transpose,Identity,Shift,First,Rotate}"/>
<org.eventb.core.prPred name="p33" org.eventb.core.predicate="Transpose∩Shift=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p52" org.eventb.core.predicate="ballot_box∈Component"/>
<org.eventb.core.prPred name="p43" org.eventb.core.predicate="¬replicator=ballot_box"/>
<org.eventb.core.prPred name="p65" org.eventb.core.predicate="∀m⦂Model·container_var(m)⊆{replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p25" org.eventb.core.predicate="toy_output∈OPort"/>
<org.eventb.core.prPred name="p27" org.eventb.core.predicate="inst_components_par={safety_comp ↦ toy_app}"/>
<org.eventb.core.prPred name="p49" org.eventb.core.predicate="(id ⦂ ℙ(Component×Component))∩f_container_var=(∅ ⦂ ℙ(Component×Component))"/>
<org.eventb.core.prPred name="p28" org.eventb.core.predicate="Inst∈Model ∖ Pattern"/>
<org.eventb.core.prPred name="p40" org.eventb.core.predicate="Shift∩Rotate=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prPred name="p69" org.eventb.core.predicate="c_multiplicity_var(safety_model)=c_mult_others_par{pc⦂Component·pc=safety_comp ∣ pc ↦ card({safety_comp ↦ toy_app}[{pc}])}"/>
<org.eventb.core.prPred name="p34" org.eventb.core.predicate="Transpose∩First=(∅ ⦂ ℙ(Link))"/>
<org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
<org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
<org.eventb.core.prReas name="r6" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalML:1"/>
<org.eventb.core.prReas name="r5" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
<org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
<org.eventb.core.prReas name="r3" org.eventb.core.prRID="org.eventb.core.seqprover.conj:0"/>
<org.eventb.core.prReas name="r4" org.eventb.core.prRID="org.eventb.core.seqprover.eq:1"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="to_unfold_c_var&#10;/THM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16,p17,p18,p19,p20,p21,p22,p23,p24,p25,p26,p27,p28,p29,p30,p31,p32,p33,p34,p35,p36,p37" org.eventb.core.prSets="Component,Model,Port">
<org.eventb.core.lang name="L"/>
<org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="sl/ds" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="SELECT0" org.eventb.core.prHyps="p3,p36,p14,p37,p23,p26,p18,p25,p11,p22,p6,p10,p7"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="CVC3" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p27,p30,p20,p21,p8,p1,p29,p33,p19,p32,p17,p9,p24,p13,p34,p5,p12,p16,p4,p35,p31,p15,p2,p28,p3,p36,p14,p37,p23,p26,p18,p25,p11,p22,p6,p10,p7">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="R1000"/>
<org.eventb.core.prString name=".config_id" org.eventb.core.prSValue="CVC3"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="IPort" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.prIdent name="Inst" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="Mdl" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="OPort" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.prIdent name="Pat" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="Pattern" org.eventb.core.type="ℙ(Model)"/>
<org.eventb.core.prIdent name="ballot_box" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="c_mult_others_par" org.eventb.core.type="ℙ(Component×ℤ)"/>
<org.eventb.core.prIdent name="c_multiplicity_var" org.eventb.core.type="ℙ(Model×ℙ(Component×ℤ))"/>
<org.eventb.core.prIdent name="components_var" org.eventb.core.type="ℙ(Model×ℙ(Component))"/>
<org.eventb.core.prIdent name="container_var" org.eventb.core.type="ℙ(Model×ℙ(Component×Component))"/>
<org.eventb.core.prIdent name="f_container_var" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="inst_components_par" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="replicator" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="safety_comp" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="safety_container" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="safety_model" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="to_unfold_c_var" org.eventb.core.type="ℙ(Component)"/>
<org.eventb.core.prIdent name="toy_app" org.eventb.core.type="Component"/>
<org.eventb.core.prIdent name="toy_container" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.prIdent name="toy_inp_1" org.eventb.core.type="Port"/>
<org.eventb.core.prIdent name="toy_inp_2" org.eventb.core.type="Port"/>
<org.eventb.core.prIdent name="toy_model" org.eventb.core.type="Model"/>
<org.eventb.core.prIdent name="toy_output" org.eventb.core.type="Port"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="toy_container∈Component ⇸ Component"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="c_multiplicity_var(safety_model)=c_mult_others_par{pc⦂Component·pc∈dom(inst_components_par) ∣ pc ↦ card(inst_components_par[{pc}])}"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="Pattern⊆Model"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="∀m⦂Model·container_var(m)⊆f_container_var∧f_container_var;f_container_var⊆f_container_var∧(id ⦂ ℙ(Component×Component))∩f_container_var=(∅ ⦂ ℙ(Component×Component))"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="components_var={safety_model ↦ {replicator,ballot_box,safety_comp},toy_model ↦ {toy_app}}"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="components_var∈Model ⇸ ℙ(Component)"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="container_var∈Model ⇸ ℙ(Component × Component)"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="toy_app∈Component"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="safety_model∈dom(container_var)"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="∀pc⦂Component·pc∈dom(inst_components_par)⇒finite(inst_components_par[{pc}])"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="container_var={safety_model ↦ safety_container,toy_model ↦ toy_container}"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="toy_inp_2∈IPort"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="Pat∈Pattern"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="c_multiplicity_var={safety_model ↦ {safety_comp ↦ 1,replicator ↦ 3,ballot_box ↦ 1}}"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="f_container_var={replicator ↦ safety_comp,ballot_box ↦ safety_comp}"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="Model={safety_model,toy_model}"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="safety_model∈dom(c_multiplicity_var)"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="toy_model∈Model"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="safety_comp∈Component"/>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="replicator≠ballot_box∧replicator≠safety_comp∧ballot_box≠safety_comp"/>
<org.eventb.core.prPred name="p22" org.eventb.core.predicate="safety_model∈dom(components_var)"/>
<org.eventb.core.prPred name="p23" org.eventb.core.predicate="Inst≠Mdl"/>
<org.eventb.core.prPred name="p24" org.eventb.core.predicate="toy_inp_1∈IPort"/>
<org.eventb.core.prPred name="p25" org.eventb.core.predicate="c_multiplicity_var∈Model ⇸ ℙ(Component × ℤ)"/>
<org.eventb.core.prPred name="p26" org.eventb.core.predicate="partition(Port,IPort,OPort)"/>
<org.eventb.core.prPred name="p27" org.eventb.core.predicate="replicator∈Component"/>
<org.eventb.core.prPred name="p28" org.eventb.core.predicate="to_unfold_c_var={safety_comp}"/>
<org.eventb.core.prPred name="p29" org.eventb.core.predicate="toy_container=(∅ ⦂ ℙ(Component×Component))"/>
<org.eventb.core.prPred name="p30" org.eventb.core.predicate="ballot_box∈Component"/>
<org.eventb.core.prPred name="p31" org.eventb.core.predicate="c_mult_others_par={replicator ↦ 3,ballot_box ↦ 1}"/>
<org.eventb.core.prPred name="p32" org.eventb.core.predicate="safety_model≠toy_model"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="to_unfold_c_var=components_var(safety_model) ∖ dom(container_var(safety_model))"/>
<org.eventb.core.prPred name="p33" org.eventb.core.predicate="safety_model∈Model"/>
<org.eventb.core.prPred name="p34" org.eventb.core.predicate="toy_output∈OPort"/>
<org.eventb.core.prPred name="p35" org.eventb.core.predicate="inst_components_par={safety_comp ↦ toy_app}"/>
<org.eventb.core.prPred name="p36" org.eventb.core.predicate="Mdl∈Model ∖ Pattern"/>
<org.eventb.core.prPred name="p37" org.eventb.core.predicate="Inst∈Model ∖ Pattern"/>
<org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.mngHyp"/>
<org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.smt.core.externalSMT"/>
</org.eventb.core.prProof>
</org.eventb.core.prFile>