|
|
|
@ -0,0 +1,775 @@
@@ -0,0 +1,775 @@
|
|
|
|
|
<?xml version="1.0" encoding="UTF-8" standalone="no"?> |
|
|
|
|
<org.eventb.core.poFile org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poIdentifier name="Model" org.eventb.core.type="โ(Model)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="Property" org.eventb.core.type="โ(Property)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="Inst" org.eventb.core.type="Model"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="Mdl" org.eventb.core.type="Model"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="Pat" org.eventb.core.type="Model"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="Pattern" org.eventb.core.type="โ(Model)"/> |
|
|
|
|
<org.eventb.core.poPredicate name="Propertz" org.eventb.core.predicate="PatternโModel" org.eventb.core.source="/pseim/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.axiom#_h20wcfqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="Propert{" org.eventb.core.predicate="MdlโModel โ Pattern" org.eventb.core.source="/pseim/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.axiom#_h20wcvqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="Propert|" org.eventb.core.predicate="PatโPattern" org.eventb.core.source="/pseim/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.axiom#_h20wc_qkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="Propert}" org.eventb.core.predicate="InstโModel โ Pattern" org.eventb.core.source="/pseim/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.axiom#_fxjdEQKnEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poPredicate name="Propert~" org.eventb.core.predicate="Instโ Mdl" org.eventb.core.source="/pseim/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.axiom#_DGgrYAUMEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="Component" org.eventb.core.type="โ(Component)"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poIdentifier name="c_index" org.eventb.core.type="โ(Componentรโค)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="c_multiplicity" org.eventb.core.type="โ(Componentรโค)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="components" org.eventb.core.type="โ(ModelรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="container" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="inst2pat_c" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="to_clone_c" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="to_unfold_c" org.eventb.core.type="โ(Component)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="to_unfold_c_in" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poSequent name="irrefl/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="containerโฉ(id โฆ โ(ComponentรComponent))=(โ
โฆ โ(ComponentรComponent))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNI_qkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNI_qkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_unfold_in/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_unfold_cโฉdom(to_unfold_c_in)=(โ
โฆ โ(Component))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_nieoAAMxEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_nieoAAMxEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_clone/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo."/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_unfold_cโฉran(to_clone_c)=(โ
โฆ โ(Component))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0AMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0AMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo."/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="to_clone_c_mult/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Invariant" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo1"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="โcโฆComponentยทcโdom(inst2pat_c)โcโdom(c_index)โงc_indexโComponent โธ โคโงinst2pat_cโComponent โธ Componentโงinst2pat_c(c)โdom(c_multiplicity)โงc_multiplicityโComponent โธ โค" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_V6rHAAM1Eei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_V6rHAAM1Eei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo1"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="VWD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of variant" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="โcโฆComponentยทcโto_unfold_cโชran(to_clone_c)โ{scโฆโ(Component)ยทcโscโงcontainerโผ[sc]โsc โฃ sc}โ (โ
โฆ โ(โ(Component)))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.variant#_yRrOsAK6EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.variant#_yRrOsAK6EeiAPf1wPUl3Gw"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="FIN" org.eventb.core.accurate="true" org.eventb.core.poDesc="Finiteness of variant" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="finite(โcโฆComponentยทcโto_unfold_cโชran(to_clone_c) โฃ {c} ร inter({scโฆโ(Component)ยทcโscโงcontainerโผ[sc]โsc โฃ sc}))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.variant#_yRrOsAK6EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.variant#_yRrOsAK6EeiAPf1wPUl3Gw"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/comp_finite/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="โmโฆModelยทfinite(({Inst} โฉค components)[{m}])" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_cQf0ZPqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_cQf0ZPqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/comp_finite\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD1"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/comp_not_shared/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="({Inst} โฉค components)โผโComponent โธ Model" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_ip9Q0PqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_ip9Q0PqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/comp_not_shared\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD2"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/c_mult/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="c_multiplicity๎(c_mult_others๎{pcโฆComponentยทpcโdom(inst_components) โฃ pc โฆ card(inst_components[{pc}])})โ({Inst} โฉค components)[Pattern] โ โ" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_GMp30PqWEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_GMp30PqWEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/c_mult\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD3"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/cont_ty/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="components[{Inst}] โฉค containerโran({Inst} โฉค components) โธ ran({Inst} โฉค components)" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8fqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8fqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/cont_ty\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD4"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/cont_ctr/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{Inst} โฉค components;(components[{Inst}] โฉค container);({Inst} โฉค components)โผโ(id โฆ โ(ModelรModel))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8vqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8vqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/cont_ctr\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD5"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/acycl/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="โfโฆโ(ComponentรComponent)ยทfโComponent โ Componentโงcomponents[{Inst}] โฉค containerโfโงf;fโfโง(id โฆ โ(ComponentรComponent))โฉf=(โ
โฆ โ(ComponentรComponent))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_oXBHAPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_oXBHAPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/acycl\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD6"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/to_unfold_c_in/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(โ
โฆ โ(ComponentรComponent))โ({Inst} โฉค components)[{Pat}] โ ({Inst} โฉค components)[{Inst}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNJPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNJPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/to_unfold_c_in\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD8"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/to_clone_c/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(โ
โฆ โ(ComponentรComponent))โ({Inst} โฉค components)[{Inst}] โธ ({Inst} โฉค components)[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dq0MPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dq0MPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/to_clone_c\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD9"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/to_unfold_c/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="components[{Pat}] โ dom(container)โ({Inst} โฉค components)[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEQA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEQA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/to_unfold_c\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD10"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/inst2pat_c_ty/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(โ
โฆ โ(ComponentรComponent))โ({Inst} โฉค components)[{Inst}] โ ({Inst} โฉค components)[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEgA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEgA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/inst2pat_c_ty\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD11"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/inst2pat_clone/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(โ
โฆ โ(ComponentรComponent))โ(โ
โฆ โ(ComponentรComponent))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_Hwdz4AKtEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_Hwdz4AKtEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/inst2pat_clone\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD12"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/inst2pat_unfold_in/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(โ
โฆ โ(ComponentรComponent));(โ
โฆ โ(ComponentรComponent))โcomponents[{Inst}] โฉค container" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_xudpYQK5EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_xudpYQK5EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/inst2pat_unfold_in\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD13"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/pat2inst_unfold/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(components[{Pat}] โ dom(container))โฉran(โ
โฆ โ(ComponentรComponent))=(โ
โฆ โ(Component))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_fxu54ALAEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_fxu54ALAEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/pat2inst_unfold\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD14"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/unfold_root/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(components[{Pat}] โ dom(container))โฉdom(components[{Inst}] โฉค container)=(โ
โฆ โ(Component))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoAMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoAMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/unfold_root\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD15"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/unfold_in/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="dom(โ
โฆ โ(ComponentรComponent))โdom(components[{Inst}] โฉค container)" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoQMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoQMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/unfold_in\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD16"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/inst2pat_cont/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(โ
โฆ โ(ComponentรComponent));(components[{Inst}] โฉค container)=components[{Inst}] โฉค container;(โ
โฆ โ(ComponentรComponent))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0QMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0QMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/inst2pat_cont\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo1|org.eventb.core.poPredicate#PRD19"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/c_index_ty/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(โ
โฆ โ(Componentรโค))โdom(โ
โฆ โ(ComponentรComponent)) โ โ" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0gMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0gMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/c_index_ty\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo1|org.eventb.core.poPredicate#PRD20"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/to_clone_c_mult/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="โcโฆComponentยทcโdom(โ
โฆ โ(ComponentรComponent))โ(โ
โฆ โ(Componentรโค))(c)โ1 โฅ (c_multiplicity๎(c_mult_others๎{pcโฆComponentยทpcโdom(inst_components) โฃ pc โฆ card(inst_components[{pc}])}))((โ
โฆ โ(ComponentรComponent))(c))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_V6rHAAM1Eei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_V6rHAAM1Eei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#instanciate_pattern\/to_clone_c_mult\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD21"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="instanciate_pattern/c_mult/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of action" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="โpcโฆComponentยทpcโdom(inst_components)โfinite(inst_components[{pc}])" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.action#_O1UjhfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.action#_O1UjhfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ip"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poPredicateSet name="EVTIDENTto_unfold_c_ip" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poIdentifier name="to_clone_c'" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="to_unfold_c'" org.eventb.core.type="โ(Component)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="inst_components" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="container'" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="c_index'" org.eventb.core.type="โ(Componentรโค)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="c_multiplicity'" org.eventb.core.type="โ(Componentรโค)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="components'" org.eventb.core.type="โ(ModelรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="to_unfold_c_in'" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="c_mult_others" org.eventb.core.type="โ(Componentรโค)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="inst2pat_c'" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poPredicateSet name="EVTALLHYPto_unfold_c_ip" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTIDENTto_unfold_c_ip" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="inst_componentsโcomponents[{Pat}] โ components[{Mdl}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.guard#_O1UjgvqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="inst_componentsโผโcomponents[{Mdl}] โธ components[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.guard#_O1Ujg_qmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="c_mult_othersโcomponents[{Pat}] โ dom(inst_components) โ โ" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.guard#_O1UjhPqmEeectLZKwQfI0A"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/new_c_ty/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTHYPto_unfold_c_iq'"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cโdom(c_multiplicity)โงc_multiplicityโComponent โธ โค" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.guard#_O1WYsvqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.guard#_O1WYsvqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTHYPto_unfold_c_iq'"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/comp_finite/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="โmโฆModelยทfinite((componentsโช({Inst} ร ran(new_c)))[{m}])" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_cQf0ZPqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_cQf0ZPqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/comp_finite\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD1"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/comp_not_shared/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(componentsโช({Inst} ร ran(new_c)))โผโComponent โธ Model" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_ip9Q0PqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_ip9Q0PqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/comp_not_shared\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD2"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/c_mult/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="c_multiplicityโ(componentsโช({Inst} ร ran(new_c)))[Pattern] โ โ" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_GMp30PqWEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_GMp30PqWEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/c_mult\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD3"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/cont_ty/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="containerโran(componentsโช({Inst} ร ran(new_c))) โธ ran(componentsโช({Inst} ร ran(new_c)))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8fqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8fqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/cont_ty\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD4"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/cont_ctr/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(componentsโช({Inst} ร ran(new_c)));container;(componentsโช({Inst} ร ran(new_c)))โผโ(id โฆ โ(ModelรModel))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8vqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8vqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/cont_ctr\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD5"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/to_unfold_c_in/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_unfold_c_inโ(componentsโช({Inst} ร ran(new_c)))[{Pat}] โ (componentsโช({Inst} ร ran(new_c)))[{Inst}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNJPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNJPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/to_unfold_c_in\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD8"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/to_clone_c/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_clone_cโช(ran(new_c) ร {c})โ(componentsโช({Inst} ร ran(new_c)))[{Inst}] โธ (componentsโช({Inst} ร ran(new_c)))[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dq0MPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dq0MPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/to_clone_c\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD9"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/to_unfold_c/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_unfold_c โ {c}โ(componentsโช({Inst} ร ran(new_c)))[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEQA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEQA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/to_unfold_c\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD10"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/inst2pat_c_ty/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="inst2pat_cโช(ran(new_c) ร {c})โ(componentsโช({Inst} ร ran(new_c)))[{Inst}] โ (componentsโช({Inst} ร ran(new_c)))[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEgA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEgA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/inst2pat_c_ty\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD11"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/inst2pat_clone/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_clone_cโช(ran(new_c) ร {c})โinst2pat_cโช(ran(new_c) ร {c})" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_Hwdz4AKtEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_Hwdz4AKtEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/inst2pat_clone\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD12"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/inst2pat_unfold_in/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_unfold_c_in;(inst2pat_cโช(ran(new_c) ร {c}))โcontainer" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_xudpYQK5EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_xudpYQK5EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/inst2pat_unfold_in\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD13"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/pat2inst_unfold/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(to_unfold_c โ {c})โฉran(inst2pat_cโช(ran(new_c) ร {c}))=(โ
โฆ โ(Component))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_fxu54ALAEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_fxu54ALAEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/pat2inst_unfold\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD14"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/unfold_root/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(to_unfold_c โ {c})โฉdom(container)=(โ
โฆ โ(Component))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoAMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoAMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/unfold_root\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD15"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/inst2pat_cont/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(inst2pat_cโช(ran(new_c) ร {c}));container=container;(inst2pat_cโช(ran(new_c) ร {c}))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0QMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0QMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/inst2pat_cont\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo1|org.eventb.core.poPredicate#PRD19"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/c_index_ty/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="c_indexโชnew_cโผโdom(inst2pat_cโช(ran(new_c) ร {c})) โ โ" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0gMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0gMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/c_index_ty\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo1|org.eventb.core.poPredicate#PRD20"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/to_clone_c_mult/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="โc0โฆComponentยทc0โdom(inst2pat_cโช(ran(new_c) ร {c}))โ(c_indexโชnew_cโผ)(c0)โ1 โฅ c_multiplicity((inst2pat_cโช(ran(new_c) ร {c}))(c0))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_V6rHAAM1Eei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_V6rHAAM1Eei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/to_clone_c_mult\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD21"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_root_c/VAR" org.eventb.core.accurate="true" org.eventb.core.poDesc="Variant of event" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_iq"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(โc0โฆComponentยทc0โ(to_unfold_c โ {c})โชran(to_clone_cโช(ran(new_c) ร {c})) โฃ {c0} ร inter({scโฆโ(Component)ยทc0โscโงcontainerโผ[sc]โsc โฃ sc}))โ(โcโฆComponentยทcโto_unfold_cโชran(to_clone_c) โฃ {c} ร inter({scโฆโ(Component)ยทcโscโงcontainerโผ[sc]โsc โฃ sc}))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.variant#_yRrOsAK6EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.variant#_yRrOsAK6EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_root_c\/VAR|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poPredicateSet name="EVTIDENTto_unfold_c_iq" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poIdentifier name="to_clone_c'" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="to_unfold_c'" org.eventb.core.type="โ(Component)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="c_index'" org.eventb.core.type="โ(Componentรโค)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="c" org.eventb.core.type="Component"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="components'" org.eventb.core.type="โ(ModelรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="new_c" org.eventb.core.type="โ(โครComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="inst2pat_c'" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poPredicateSet name="EVTHYPto_unfold_c_iq'" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTIDENTto_unfold_c_iq" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="cโto_unfold_c" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.guard#_O1WYsfqmEeectLZKwQfI0A"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poPredicateSet name="EVTALLHYPto_unfold_c_iq" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTHYPto_unfold_c_iq'" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="new_cโ1 โฅ c_multiplicity(c) โฃ Component โ ran(components)" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.guard#_O1WYsvqmEeectLZKwQfI0A"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poSequent name="clone_c/to_unfold_c_in/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ir"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_unfold_c_inโช(containerโผ[{to_clone_c(c)}] ร {c})โcomponents[{Pat}] โ components[{Inst}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNJPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNJPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#clone_c\/to_unfold_c_in\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD8"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="clone_c/to_clone_c/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ir"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{c} โฉค to_clone_cโcomponents[{Inst}] โธ components[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dq0MPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dq0MPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#clone_c\/to_clone_c\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD9"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="clone_c/inst2pat_clone/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ir"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{c} โฉค to_clone_cโinst2pat_c" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_Hwdz4AKtEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_Hwdz4AKtEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#clone_c\/inst2pat_clone\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD12"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="clone_c/inst2pat_unfold_in/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ir"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(to_unfold_c_inโช(containerโผ[{to_clone_c(c)}] ร {c}));inst2pat_cโcontainer" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_xudpYQK5EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_xudpYQK5EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#clone_c\/inst2pat_unfold_in\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD13"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="clone_c/unfold_in/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ir"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="dom(to_unfold_c_inโช(containerโผ[{to_clone_c(c)}] ร {c}))โdom(container)" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoQMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoQMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#clone_c\/unfold_in\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD16"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="clone_c/to_unfold_c_in/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of action" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ir"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cโdom(to_clone_c)โงto_clone_cโComponent โธ Component" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.action#_O1YN4fqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.action#_O1YN4fqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ir"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="clone_c/VAR" org.eventb.core.accurate="true" org.eventb.core.poDesc="Variant of event" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_ir"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(โc0โฆComponentยทc0โto_unfold_cโชran({c} โฉค to_clone_c) โฃ {c0} ร inter({scโฆโ(Component)ยทc0โscโงcontainerโผ[sc]โsc โฃ sc}))โ(โcโฆComponentยทcโto_unfold_cโชran(to_clone_c) โฃ {c} ร inter({scโฆโ(Component)ยทcโscโงcontainerโผ[sc]โsc โฃ sc}))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.variant#_yRrOsAK6EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.variant#_yRrOsAK6EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#clone_c\/VAR|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poPredicateSet name="EVTIDENTto_unfold_c_ir" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poIdentifier name="to_clone_c'" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="c" org.eventb.core.type="Component"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="to_unfold_c_in'" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poPredicateSet name="EVTALLHYPto_unfold_c_ir" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTIDENTto_unfold_c_ir" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="cโdom(to_clone_c)" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.guard#_O1WYs_qmEeectLZKwQfI0A"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/new_c_ty/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTHYPto_unfold_c_is'"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cโdom(c_multiplicity)โงc_multiplicityโComponent โธ โค" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_O1WYtfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_O1WYtfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTHYPto_unfold_c_is'"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/comp_finite/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="โmโฆModelยทfinite((componentsโช({Inst} ร ran(new_c)))[{m}])" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_cQf0ZPqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_cQf0ZPqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/comp_finite\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD1"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/comp_not_shared/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(componentsโช({Inst} ร ran(new_c)))โผโComponent โธ Model" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_ip9Q0PqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_ip9Q0PqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/comp_not_shared\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD2"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/c_mult/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="c_multiplicityโ(componentsโช({Inst} ร ran(new_c)))[Pattern] โ โ" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_GMp30PqWEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_GMp30PqWEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/c_mult\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD3"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/cont_ty/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="containerโช(ran(new_c) ร {dest})โran(componentsโช({Inst} ร ran(new_c))) โธ ran(componentsโช({Inst} ร ran(new_c)))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8fqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8fqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/cont_ty\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD4"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/cont_ctr/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(componentsโช({Inst} ร ran(new_c)));(containerโช(ran(new_c) ร {dest}));(componentsโช({Inst} ร ran(new_c)))โผโ(id โฆ โ(ModelรModel))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8vqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8vqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/cont_ctr\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD5"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/acycl/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="โfโฆโ(ComponentรComponent)ยทfโComponent โ Componentโงcontainerโช(ran(new_c) ร {dest})โfโงf;fโfโง(id โฆ โ(ComponentรComponent))โฉf=(โ
โฆ โ(ComponentรComponent))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_oXBHAPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_oXBHAPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/acycl\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD6"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/to_unfold_c_in/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_unfold_c_in โ {c โฆ dest}โ(componentsโช({Inst} ร ran(new_c)))[{Pat}] โ (componentsโช({Inst} ร ran(new_c)))[{Inst}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNJPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNJPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/to_unfold_c_in\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD8"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/to_clone_c/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_clone_cโช(ran(new_c) ร {c})โ(componentsโช({Inst} ร ran(new_c)))[{Inst}] โธ (componentsโช({Inst} ร ran(new_c)))[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dq0MPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dq0MPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/to_clone_c\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD9"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/to_unfold_c/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_unfold_cโ(componentsโช({Inst} ร ran(new_c)))[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEQA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEQA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/to_unfold_c\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD10"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/inst2pat_c_ty/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="inst2pat_cโช(ran(new_c) ร {c})โ(componentsโช({Inst} ร ran(new_c)))[{Inst}] โ (componentsโช({Inst} ร ran(new_c)))[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEgA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEgA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/inst2pat_c_ty\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD11"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/inst2pat_clone/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_clone_cโช(ran(new_c) ร {c})โinst2pat_cโช(ran(new_c) ร {c})" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_Hwdz4AKtEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_Hwdz4AKtEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/inst2pat_clone\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD12"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/inst2pat_unfold_in/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(to_unfold_c_in โ {c โฆ dest});(inst2pat_cโช(ran(new_c) ร {c}))โcontainerโช(ran(new_c) ร {dest})" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_xudpYQK5EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_xudpYQK5EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/inst2pat_unfold_in\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD13"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/pat2inst_unfold/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_unfold_cโฉran(inst2pat_cโช(ran(new_c) ร {c}))=(โ
โฆ โ(Component))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_fxu54ALAEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_fxu54ALAEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/pat2inst_unfold\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD14"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/unfold_root/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_unfold_cโฉdom(containerโช(ran(new_c) ร {dest}))=(โ
โฆ โ(Component))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoAMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoAMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/unfold_root\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD15"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/unfold_in/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="dom(to_unfold_c_in โ {c โฆ dest})โdom(containerโช(ran(new_c) ร {dest}))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoQMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoQMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/unfold_in\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD16"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/inst2pat_cont/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(inst2pat_cโช(ran(new_c) ร {c}));(containerโช(ran(new_c) ร {dest}))=(containerโช(ran(new_c) ร {dest}));(inst2pat_cโช(ran(new_c) ร {c}))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0QMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0QMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/inst2pat_cont\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo1|org.eventb.core.poPredicate#PRD19"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/c_index_ty/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="c_indexโชnew_cโผโdom(inst2pat_cโช(ran(new_c) ร {c})) โ โ" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0gMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0gMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/c_index_ty\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo1|org.eventb.core.poPredicate#PRD20"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/to_clone_c_mult/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="โc0โฆComponentยทc0โdom(inst2pat_cโช(ran(new_c) ร {c}))โ(c_indexโชnew_cโผ)(c0)โ1 โฅ c_multiplicity((inst2pat_cโช(ran(new_c) ร {c}))(c0))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_V6rHAAM1Eei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_V6rHAAM1Eei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/to_clone_c_mult\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD21"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="unfold_node_c/VAR" org.eventb.core.accurate="true" org.eventb.core.poDesc="Variant of event" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_is"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(โc0โฆComponentยทc0โto_unfold_cโชran(to_clone_cโช(ran(new_c) ร {c})) โฃ {c0} ร inter({scโฆโ(Component)ยทc0โscโง(containerโช(ran(new_c) ร {dest}))โผ[sc]โsc โฃ sc}))โ(โcโฆComponentยทcโto_unfold_cโชran(to_clone_c) โฃ {c} ร inter({scโฆโ(Component)ยทcโscโงcontainerโผ[sc]โsc โฃ sc}))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.variant#_yRrOsAK6EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.variant#_yRrOsAK6EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#unfold_node_c\/VAR|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poPredicateSet name="EVTIDENTto_unfold_c_is" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poIdentifier name="to_clone_c'" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="container'" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="c_index'" org.eventb.core.type="โ(Componentรโค)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="c" org.eventb.core.type="Component"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="components'" org.eventb.core.type="โ(ModelรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="dest" org.eventb.core.type="Component"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="new_c" org.eventb.core.type="โ(โครComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="to_unfold_c_in'" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="inst2pat_c'" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poPredicateSet name="EVTHYPto_unfold_c_is'" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTIDENTto_unfold_c_is" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="c โฆ destโto_unfold_c_in" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_O1WYtPqmEeectLZKwQfI0A"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poPredicateSet name="EVTALLHYPto_unfold_c_is" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTHYPto_unfold_c_is'" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="new_cโ1 โฅ c_multiplicity(c) โฃ Component โ ran(components)" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_O1WYtfqmEeectLZKwQfI0A"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poSequent name="apply_pattern/comp_finite/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_it"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="โmโฆModelยทfinite((componentsโช({Mdl} ร ran(new_components)))[{m}])" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_cQf0ZPqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_cQf0ZPqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#apply_pattern\/comp_finite\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD1"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="apply_pattern/comp_not_shared/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_it"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(componentsโช({Mdl} ร ran(new_components)))โผโComponent โธ Model" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_ip9Q0PqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_ip9Q0PqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#apply_pattern\/comp_not_shared\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD2"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="apply_pattern/c_mult/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_it"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="c_multiplicityโ(componentsโช({Mdl} ร ran(new_components)))[Pattern] โ โ" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_GMp30PqWEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_GMp30PqWEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#apply_pattern\/c_mult\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD3"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="apply_pattern/cont_ty/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_it"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="containerโช((inst_componentsโชnew_components)โผ;container;(inst_componentsโชnew_components))โran(componentsโช({Mdl} ร ran(new_components))) โธ ran(componentsโช({Mdl} ร ran(new_components)))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8fqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8fqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#apply_pattern\/cont_ty\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD4"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="apply_pattern/cont_ctr/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_it"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(componentsโช({Mdl} ร ran(new_components)));(containerโช((inst_componentsโชnew_components)โผ;container;(inst_componentsโชnew_components)));(componentsโช({Mdl} ร ran(new_components)))โผโ(id โฆ โ(ModelรModel))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8vqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8vqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#apply_pattern\/cont_ctr\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD5"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="apply_pattern/acycl/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_it"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="โfโฆโ(ComponentรComponent)ยทfโComponent โ Componentโงcontainerโช((inst_componentsโชnew_components)โผ;container;(inst_componentsโชnew_components))โfโงf;fโfโง(id โฆ โ(ComponentรComponent))โฉf=(โ
โฆ โ(ComponentรComponent))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_oXBHAPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_oXBHAPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#apply_pattern\/acycl\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{|org.eventb.core.poPredicate#PRD6"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="apply_pattern/to_unfold_c_in/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_it"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_unfold_c_inโ(componentsโช({Mdl} ร ran(new_components)))[{Pat}] โ (componentsโช({Mdl} ร ran(new_components)))[{Inst}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNJPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNJPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#apply_pattern\/to_unfold_c_in\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD8"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="apply_pattern/to_clone_c/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_it"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_clone_cโ(componentsโช({Mdl} ร ran(new_components)))[{Inst}] โธ (componentsโช({Mdl} ร ran(new_components)))[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dq0MPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dq0MPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#apply_pattern\/to_clone_c\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD9"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="apply_pattern/to_unfold_c/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_it"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_unfold_cโ(componentsโช({Mdl} ร ran(new_components)))[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEQA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEQA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#apply_pattern\/to_unfold_c\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD10"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="apply_pattern/inst2pat_c_ty/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_it"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="inst2pat_cโ(componentsโช({Mdl} ร ran(new_components)))[{Inst}] โ (componentsโช({Mdl} ร ran(new_components)))[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEgA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEgA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#apply_pattern\/inst2pat_c_ty\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD11"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="apply_pattern/inst2pat_unfold_in/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_it"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_unfold_c_in;inst2pat_cโcontainerโช((inst_componentsโชnew_components)โผ;container;(inst_componentsโชnew_components))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_xudpYQK5EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_xudpYQK5EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#apply_pattern\/inst2pat_unfold_in\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD13"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="apply_pattern/unfold_root/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_it"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_unfold_cโฉdom(containerโช((inst_componentsโชnew_components)โผ;container;(inst_componentsโชnew_components)))=(โ
โฆ โ(Component))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoAMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoAMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#apply_pattern\/unfold_root\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD15"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="apply_pattern/unfold_in/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_it"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="dom(to_unfold_c_in)โdom(containerโช((inst_componentsโชnew_components)โผ;container;(inst_componentsโชnew_components)))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoQMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoQMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#apply_pattern\/unfold_in\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-|org.eventb.core.poPredicate#PRD16"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poSequent name="apply_pattern/inst2pat_cont/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTALLHYPto_unfold_c_it"/> |
|
|
|
|
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="inst2pat_c;(containerโช((inst_componentsโชnew_components)โผ;container;(inst_componentsโชnew_components)))=(containerโช((inst_componentsโชnew_components)โผ;container;(inst_componentsโชnew_components)));inst2pat_c" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0QMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0QMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poSequent#apply_pattern\/inst2pat_cont\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> |
|
|
|
|
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo1|org.eventb.core.poPredicate#PRD19"/> |
|
|
|
|
</org.eventb.core.poSequent> |
|
|
|
|
<org.eventb.core.poPredicateSet name="EVTIDENTto_unfold_c_it" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poIdentifier name="inst_components" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="container'" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="components'" org.eventb.core.type="โ(ModelรComponent)"/> |
|
|
|
|
<org.eventb.core.poIdentifier name="new_components" org.eventb.core.type="โ(ComponentรComponent)"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poPredicateSet name="EVTALLHYPto_unfold_c_it" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#EVTIDENTto_unfold_c_it" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="inst_componentsโcomponents[{Inst}] โค components[{Mdl}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A|org.eventb.core.guard#_O1WYtvqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="new_componentsโcomponents[{Inst}] โ dom(inst_components) โฃ Component โ ran(components)" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A|org.eventb.core.guard#_O1W_wvqmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="dom(inst_components) โ container;inst_componentsโinst_components;container" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A|org.eventb.core.guard#_O1W_w_qmEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="container[dom(inst_components)]โdom(inst_components)" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1Xm2PqmEeectLZKwQfI0A|org.eventb.core.guard#_O1Xm0vqmEeectLZKwQfI0A"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poPredicateSet name="HYPcComponen{" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="componentsโModel โ Component" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_cQf0Y_qUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="โmโฆModelยทfinite(components[{m}])" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_cQf0ZPqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="componentsโผโComponent โธ Model" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_ip9Q0PqUEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="c_multiplicityโcomponents[Pattern] โ โ" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_GMp30PqWEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="containerโran(components) โธ ran(components)" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8fqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="components;container;componentsโผโ(id โฆ โ(ModelรModel))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8vqgEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="โfโฆโ(ComponentรComponent)ยทfโComponent โ Componentโงcontainerโfโงf;fโfโง(id โฆ โ(ComponentรComponent))โฉf=(โ
โฆ โ(ComponentรComponent))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_oXBHAPqkEeectLZKwQfI0A"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poPredicateSet name="HYPcComponeo-" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponen{" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD7" org.eventb.core.predicate="containerโฉ(id โฆ โ(ComponentรComponent))=(โ
โฆ โ(ComponentรComponent))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNI_qkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD8" org.eventb.core.predicate="to_unfold_c_inโcomponents[{Pat}] โ components[{Inst}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNJPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD9" org.eventb.core.predicate="to_clone_cโcomponents[{Inst}] โธ components[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dq0MPqkEeectLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD10" org.eventb.core.predicate="to_unfold_cโcomponents[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEQA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD11" org.eventb.core.predicate="inst2pat_cโcomponents[{Inst}] โ components[{Pat}]" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEgA1EeictLZKwQfI0A"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD12" org.eventb.core.predicate="to_clone_cโinst2pat_c" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_Hwdz4AKtEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD13" org.eventb.core.predicate="to_unfold_c_in;inst2pat_cโcontainer" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_xudpYQK5EeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD14" org.eventb.core.predicate="to_unfold_cโฉran(inst2pat_c)=(โ
โฆ โ(Component))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_fxu54ALAEeiAPf1wPUl3Gw"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD15" org.eventb.core.predicate="to_unfold_cโฉdom(container)=(โ
โฆ โ(Component))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoAMwEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD16" org.eventb.core.predicate="dom(to_unfold_c_in)โdom(container)" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoQMwEei9ocE08JsPSw"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poPredicateSet name="HYPcComponeo." org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo-" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD17" org.eventb.core.predicate="to_unfold_cโฉdom(to_unfold_c_in)=(โ
โฆ โ(Component))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_nieoAAMxEei9ocE08JsPSw"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poPredicateSet name="HYPcComponeo1" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo." org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD18" org.eventb.core.predicate="to_unfold_cโฉran(to_clone_c)=(โ
โฆ โ(Component))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0AMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD19" org.eventb.core.predicate="inst2pat_c;container=container;inst2pat_c" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0QMzEei9ocE08JsPSw"/> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD20" org.eventb.core.predicate="c_indexโdom(inst2pat_c) โ โ" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0gMzEei9ocE08JsPSw"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/pseim/mComponent.bpo|org.eventb.core.poFile#mComponent|org.eventb.core.poPredicateSet#HYPcComponeo1" org.eventb.core.poStamp="0"> |
|
|
|
|
<org.eventb.core.poPredicate name="PRD21" org.eventb.core.predicate="โcโฆComponentยทcโdom(inst2pat_c)โc_index(c)โ1 โฅ c_multiplicity(inst2pat_c(c))" org.eventb.core.source="/pseim/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_V6rHAAM1Eei9ocE08JsPSw"/> |
|
|
|
|
</org.eventb.core.poPredicateSet> |
|
|
|
|
</org.eventb.core.poFile> |