Initial specification of big

BIG/.project

+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>BIG</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+		<buildCommand>
+			<name>org.rodinp.core.rodinbuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>org.rodinp.core.rodinnature</nature>
+	</natures>
+</projectDescription>

BIG/BIG_c1.bcc

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.scContextFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd;de.prob.symbolic.ctxBase">
+    <org.eventb.core.scAxiom name="'" org.eventb.core.label="axm1;" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-IUKsXEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scAxiom name="(" org.eventb.core.label="axm2;" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYKsXEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scAxiom name=")" org.eventb.core.label="axm3;" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYasXEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scConstant name="source_smart_contract" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.constant#_NmUHEKmBEe6I4bA9GxwhqQ" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+    <org.eventb.core.scCarrierSet name="CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_B7Fx4KmIEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+    <org.eventb.core.scConstant name="gateway" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.constant#_t3pvIKo_Ee6I4bA9GxwhqQ" org.eventb.core.type="GATEWAYS"/>
+    <org.eventb.core.scCarrierSet name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_lsmHUKpBEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+    <org.eventb.core.scCarrierSet name="GATEWAYS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_bUpUwKmAEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(GATEWAYS)"/>
+    <org.eventb.core.scConstant name="target_smart_contract" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.constant#_kx61gapGEe6I4bA9GxwhqQ" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+    <org.eventb.core.scCarrierSet name="TRANSACTIONS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_OLUJEKsXEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
+    <org.eventb.core.scCarrierSet name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_ISeO4KmBEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+</org.eventb.core.scContextFile>

BIG/BIG_c1.bpo

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.poFile org.eventb.core.poStamp="33">
+    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="33">
+        <org.eventb.core.poIdentifier name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+        <org.eventb.core.poIdentifier name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
+        <org.eventb.core.poIdentifier name="TRANSACTIONS" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+        <org.eventb.core.poIdentifier name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.poIdentifier name="gateway" org.eventb.core.type="GATEWAYS"/>
+        <org.eventb.core.poIdentifier name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/BIG/BIG_c1.bpo|org.eventb.core.poFile#BIG_c1|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="33">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-IUKsXEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYKsXEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYasXEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.poPredicateSet>
+</org.eventb.core.poFile>

BIG/BIG_c1.bpr

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.prFile version="1">
+    <org.eventb.core.prProof name="axm5;/WD" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p0" org.eventb.core.prSets="GATEWAYS">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="hyp" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p0"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="finite(GATEWAYS)"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.hyp"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="axm6;/WD" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p0" org.eventb.core.prSets="BLOCKCHAINS">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="hyp" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p0"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="finite(BLOCKCHAINS)"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.hyp"/>
+    </org.eventb.core.prProof>
+</org.eventb.core.prFile>

BIG/BIG_c1.bps

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.psFile/>

BIG/BIG_c1.buc

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd;de.prob.symbolic.ctxBase" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_lFfl26sXEe6I4bA9GxwhqQ" org.eventb.texttools.text_lastmodified="1704382825645" org.eventb.texttools.text_representation="context BIG_c1&#10;&#10;sets GATEWAYS TRANSACTIONS CROSS_CHAIN_SMART_CONTRACTS CROSS_CHAIN_EVENTS&#10;CROSS_CHAIN_TRANSACTIONS&#10;&#10;constants source_smart_contract target_smart_contract gateway&#10;&#10;axioms&#10;&#9;@axm1: source_smart_contract ∈ CROSS_CHAIN_SMART_CONTRACTS&#10;&#9;@axm2: target_smart_contract ∈ CROSS_CHAIN_SMART_CONTRACTS&#10;&#9;@axm3: gateway ∈ GATEWAYS&#10;&#10;end&#10;" version="3">
+    <org.eventb.core.axiom name="_j4-IUKsXEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="axm1;" org.eventb.core.predicate="source_smart_contract ∈ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.emf.persistence.emf_id="_lFfl2KsXEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.axiom name="_j4-vYKsXEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="axm2;" org.eventb.core.predicate="target_smart_contract ∈ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.emf.persistence.emf_id="_lFfl2asXEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.axiom name="_j4-vYasXEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="axm3;" org.eventb.core.predicate="gateway ∈ GATEWAYS" org.eventb.emf.persistence.emf_id="_lFfl2qsXEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.constant name="_NmUHEKmBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="source_smart_contract" org.eventb.emf.persistence.emf_id="_lFfl1asXEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.constant name="_kx61gapGEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="target_smart_contract" org.eventb.emf.persistence.emf_id="_lFfl1qsXEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.constant name="_t3pvIKo_Ee6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="gateway" org.eventb.emf.persistence.emf_id="_lFfl16sXEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.carrierSet name="_bUpUwKmAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="GATEWAYS" org.eventb.emf.persistence.emf_id="_lFfl0KsXEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.carrierSet name="_OLUJEKsXEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="TRANSACTIONS" org.eventb.emf.persistence.emf_id="_lFfl0asXEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.carrierSet name="_ISeO4KmBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.emf.persistence.emf_id="_lFfl0qsXEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.carrierSet name="_B7Fx4KmIEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="CROSS_CHAIN_EVENTS" org.eventb.emf.persistence.emf_id="_lFfl06sXEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.carrierSet name="_lsmHUKpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="CROSS_CHAIN_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_lFfl1KsXEe6I4bA9GxwhqQ"/>
+</org.eventb.core.contextFile>

BIG/BIG_m1.bcm

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
+    <org.eventb.core.scSeesContext name="'" org.eventb.core.scTarget="/BIG/BIG_c1.bcc" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.seesContext#_sUpukKl_Ee6I4bA9GxwhqQ"/>
+    <org.eventb.core.scInternalContext name="BIG_c1">
+        <org.eventb.core.scAxiom name="'" org.eventb.core.label="axm1;" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-IUKsXEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scAxiom name="(" org.eventb.core.label="axm2;" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYKsXEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scAxiom name=")" org.eventb.core.label="axm3;" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYasXEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scConstant name="source_smart_contract" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.constant#_NmUHEKmBEe6I4bA9GxwhqQ" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.scCarrierSet name="CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_B7Fx4KmIEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+        <org.eventb.core.scConstant name="gateway" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.constant#_t3pvIKo_Ee6I4bA9GxwhqQ" org.eventb.core.type="GATEWAYS"/>
+        <org.eventb.core.scCarrierSet name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_lsmHUKpBEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.scCarrierSet name="GATEWAYS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_bUpUwKmAEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(GATEWAYS)"/>
+        <org.eventb.core.scConstant name="target_smart_contract" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.constant#_kx61gapGEe6I4bA9GxwhqQ" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.scCarrierSet name="TRANSACTIONS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_OLUJEKsXEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
+        <org.eventb.core.scCarrierSet name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_ISeO4KmBEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+    </org.eventb.core.scInternalContext>
+    <org.eventb.core.scInvariant name="BIG_c2" org.eventb.core.label="inv1;" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_o6juoKviEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="BIG_c3" org.eventb.core.label="inv2;" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↠ CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="BIG_c4" org.eventb.core.label="inv3;" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_Q6dKkKpAEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="BIG_c5" org.eventb.core.label="inv4;" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_c7TQ0KpBEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="BIG_c6" org.eventb.core.label="inv6;" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_G1eDUKpbEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scVariable name="triggered_events" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.variable#_YvZFkamHEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+    <org.eventb.core.scVariable name="received_cross_chain_transactions" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.variable#_H2zkgKpbEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
+    <org.eventb.core.scVariable name="subscriptions" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.variable#_I9HgkapAEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
+    <org.eventb.core.scVariable name="gateway_pending_transactions" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.variable#_8T2BAKpBEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+    <org.eventb.core.scVariable name="received_transactions" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.variable#_SAycYamDEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
+    <org.eventb.core.scEvent name="received_cross_chain_transactiont" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'">
+        <org.eventb.core.scAction name="'" org.eventb.core.assignment="received_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)" org.eventb.core.label="act1;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'|org.eventb.core.action#_SAxOQKmDEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.scAction name="(" org.eventb.core.assignment="triggered_events ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)" org.eventb.core.label="act2;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'|org.eventb.core.action#_TlWCkamHEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.scAction name=")" org.eventb.core.assignment="subscriptions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)" org.eventb.core.label="act3;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'|org.eventb.core.action#_mv5M0KpAEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.scAction name="*" org.eventb.core.assignment="gateway_pending_transactions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)" org.eventb.core.label="act4;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'|org.eventb.core.action#_8Ty9sKpBEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.scAction name="+" org.eventb.core.assignment="received_cross_chain_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)" org.eventb.core.label="act6;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'|org.eventb.core.action#_J6KjYKpbEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.scEvent>
+    <org.eventb.core.scEvent name="received_cross_chain_transactionu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_I9G5gKpAEe6I4bA9GxwhqQ">
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="gateway ↦ source_smart_contract∉subscriptions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_I9G5gKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_SAx1UKmDEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scAction name="(" org.eventb.core.assignment="subscriptions ≔ subscriptions∪{gateway ↦ source_smart_contract}" org.eventb.core.label="act1;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_I9G5gKpAEe6I4bA9GxwhqQ|org.eventb.core.action#_a_IQYKmDEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.scEvent>
+    <org.eventb.core.scEvent name="received_cross_chain_transactionv" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="SUBMIT_CROSS_CHAIN_TRANSACTION" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ">
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="transaction∈TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ|org.eventb.core.guard#_TlWCkqmHEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd3;" org.eventb.core.predicate="transaction∉received_transactions[{source_smart_contract}]" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ|org.eventb.core.guard#_HCtL8KmIEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scParameter name="transaction" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ|org.eventb.core.parameter#_SAx1UqmDEe6I4bA9GxwhqQ" org.eventb.core.type="TRANSACTIONS"/>
+        <org.eventb.core.scAction name="transactioo" org.eventb.core.assignment="received_transactions ≔ received_transactions∪{source_smart_contract ↦ transaction}" org.eventb.core.label="act1;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ|org.eventb.core.action#_AeyzAKmIEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.scEvent>
+    <org.eventb.core.scEvent name="received_cross_chain_transactionw" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ">
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ transaction∈received_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ|org.eventb.core.guard#_iUmtQKpAEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2;" org.eventb.core.predicate="cross_chain_event∉triggered_events[{source_smart_contract}]" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ|org.eventb.core.guard#_1SOwwKmDEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scParameter name="cross_chain_event" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ|org.eventb.core.parameter#_AezaEamIEe6I4bA9GxwhqQ" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+        <org.eventb.core.scParameter name="transaction" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ|org.eventb.core.parameter#_TlWCk6mHEe6I4bA9GxwhqQ" org.eventb.core.type="TRANSACTIONS"/>
+        <org.eventb.core.scAction name="cross_chain_evenu" org.eventb.core.assignment="triggered_events ≔ triggered_events∪{source_smart_contract ↦ cross_chain_event}" org.eventb.core.label="act1;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ|org.eventb.core.action#_I9G5gapAEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.scAction name="cross_chain_evenv" org.eventb.core.assignment="received_transactions ≔ received_transactions ∖ {source_smart_contract ↦ transaction}" org.eventb.core.label="act2;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ|org.eventb.core.action#_gaDEIKmHEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.scEvent>
+    <org.eventb.core.scEvent name="received_cross_chain_transactionx" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="LISTEN_SMART_CONTRACT_EVENT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ">
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ cross_chain_event∈triggered_events" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_DMOGsKpFEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2;" org.eventb.core.predicate="gateway ↦ source_smart_contract∈subscriptions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_AezaEKmIEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_x51DwKpCEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scParameter name="cross_chain_event" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.parameter#_8VKsIqpAEe6I4bA9GxwhqQ" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+        <org.eventb.core.scParameter name="cross_chain_transaction" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.parameter#_8T1Z8qpBEe6I4bA9GxwhqQ" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
+        <org.eventb.core.scAction name="cross_chain_transactioo" org.eventb.core.assignment="gateway_pending_transactions ≔ gateway_pending_transactions∪{gateway ↦ cross_chain_transaction}" org.eventb.core.label="act1;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.action#_8T0y4KpBEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.scAction name="cross_chain_transactiop" org.eventb.core.assignment="triggered_events ≔ triggered_events ∖ {source_smart_contract ↦ cross_chain_event}" org.eventb.core.label="act2;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.action#_NAy78KpBEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.scEvent>
+    <org.eventb.core.scEvent name="received_cross_chain_transactiony" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_0sEN8KpaEe6I4bA9GxwhqQ">
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∈gateway_pending_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_0sEN8KpaEe6I4bA9GxwhqQ|org.eventb.core.guard#_tUzFcKpaEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scParameter name="cross_chain_transaction" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_0sEN8KpaEe6I4bA9GxwhqQ|org.eventb.core.parameter#_tUzFcapaEe6I4bA9GxwhqQ" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
+        <org.eventb.core.scAction name="cross_chain_transactioo" org.eventb.core.assignment="received_cross_chain_transactions ≔ received_cross_chain_transactions∪{target_smart_contract ↦ cross_chain_transaction}" org.eventb.core.label="act1;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_0sEN8KpaEe6I4bA9GxwhqQ|org.eventb.core.action#_G1dcQKpbEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.scAction name="cross_chain_transactiop" org.eventb.core.assignment="gateway_pending_transactions ≔ gateway_pending_transactions ∖ {gateway ↦ cross_chain_transaction}" org.eventb.core.label="act2;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_0sEN8KpaEe6I4bA9GxwhqQ|org.eventb.core.action#_G1dcQapbEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.scEvent>
+</org.eventb.core.scMachineFile>

BIG/BIG_m1.bpo_tmp

+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.poFile/>
\ No newline at end of file

BIG/BIG_m1.bps

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.psFile>
+    <org.eventb.core.psStatus name="INITIALISATION/inv11;/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="115" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBMIT_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="115" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="PROCESS_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="115" org.eventb.core.psManual="false"/>
+</org.eventb.core.psFile>

BIG/BIG_m1.bum

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_oyeJzKviEe6I4bA9GxwhqQ" org.eventb.texttools.text_lastmodified="1704470038332" org.eventb.texttools.text_representation="machine BIG_m1 sees BIG_c1&#10;&#10;variables received_transactions triggered_events subscriptions gateway_pending_transactions received_cross_chain_transactions&#10;&#10;invariants&#10;&#9;@inv1: received_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS // Every transaction is submitted to a smart contract&#10;&#9;@inv2: triggered_events ∈ CROSS_CHAIN_SMART_CONTRACTS ↠ CROSS_CHAIN_EVENTS // Every event is triggered by a smart contract&#10;&#9;@inv3: subscriptions ∈ GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS&#10;&#9;@inv4: gateway_pending_transactions ∈ GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS&#10;&#9;@inv6: received_cross_chain_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS&#10;&#10;events&#10;  event INITIALISATION&#10;  &#9;then&#10;  &#9;&#9;@act1: received_transactions ≔ ∅&#10;   &#9;&#9;@act2: triggered_events ≔ ∅&#10;   &#9;&#9;@act3: subscriptions ≔ ∅&#10;   &#9;&#9;@act4: gateway_pending_transactions ≔ ∅&#10;   &#9;&#9;@act6: received_cross_chain_transactions ≔ ∅&#10;  end&#10;&#10;  event SUBSCRIBE_SMART_CONTRACT_EVENTS&#10;  &#9;where&#10;  &#9;&#9;@grd1: gateway ↦ source_smart_contract ∉ subscriptions // The gateway is not already subscribed to the smart contract events&#10;  &#9;then&#10;&#9;&#9;@act1: subscriptions ≔ subscriptions  ∪ {gateway ↦ source_smart_contract} // The gateway is subscribed to listen to the smart contract events&#10;  end&#10;&#10;  event SUBMIT_CROSS_CHAIN_TRANSACTION&#10;&#9;any transaction&#10;&#9;where&#10;&#9;&#9;@grd1: transaction ∈ TRANSACTIONS&#10;&#9;&#9;@grd3: transaction ∉ received_transactions[{source_smart_contract}]&#10;&#9;then&#10;&#9;&#9;@act1: received_transactions ≔ received_transactions ∪ {source_smart_contract ↦ transaction}&#10;  end&#10;&#10;  event PROCESS_CROSS_CHAIN_TRANSACTION&#10;  &#9;any transaction cross_chain_event&#10;  &#9;where&#10;  &#9;&#9;@grd1: source_smart_contract ↦ transaction ∈ received_transactions // The smart contract has a pending transaction to process&#10;  &#9;&#9;@grd2: cross_chain_event ∉ triggered_events[{source_smart_contract}] // The smart contract will allways trigger a new event&#10;  &#9;then&#10;  &#9;&#9;@act1: triggered_events ≔  triggered_events ∪ {source_smart_contract ↦ cross_chain_event} // The smart contract triggers a new event related to the transaction processing&#10;  &#9;&#9;@act2: received_transactions ≔ received_transactions ∖ {source_smart_contract ↦ transaction} // The smart contract processed the transaction&#10;  end&#10;&#10;  event LISTEN_SMART_CONTRACT_EVENT&#10;  &#9;any cross_chain_event cross_chain_transaction&#10;  &#9;where&#10;  &#9;&#9;@grd1: source_smart_contract ↦ cross_chain_event ∈ triggered_events // The smart contract has triggered an event&#10;  &#9;&#9;@grd2: gateway ↦ source_smart_contract ∈ subscriptions // Exist a subscription to the smart contract events&#10;  &#9;&#9;@grd3: gateway ↦ cross_chain_transaction ∉ gateway_pending_transactions // The event was not already listened&#10;  &#9;then&#10;&#9;&#9;@act1: gateway_pending_transactions ≔ gateway_pending_transactions ∪ {gateway ↦ cross_chain_transaction} // The event is added to the cross-chain transactions to be processed by the gateway&#10;  &#9;&#9;@act2: triggered_events ≔ triggered_events ∖ {source_smart_contract ↦ cross_chain_event} // The event is listened and processed&#10;  end&#10;&#10;  event GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION&#10;  &#9;any cross_chain_transaction&#10;  &#9;when&#10;  &#9;&#9;@grd1: gateway ↦ cross_chain_transaction ∈ gateway_pending_transactions // There is one pending cross-chain transaction to process&#10;  &#9;then&#10;  &#9;&#9;@act1: received_cross_chain_transactions ≔ received_cross_chain_transactions ∪ {target_smart_contract ↦ cross_chain_transaction}&#10;  &#9;&#9;@act2: gateway_pending_transactions ≔  gateway_pending_transactions ∖ {gateway ↦ cross_chain_transaction}&#10;  end&#10;&#10;end&#10;" version="5">
+    <org.eventb.core.seesContext name="_sUpukKl_Ee6I4bA9GxwhqQ" org.eventb.core.target="BIG_c1"/>
+    <org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION" org.eventb.emf.persistence.emf_id="_oyeJr6viEe6I4bA9GxwhqQ">
+        <org.eventb.core.action name="_SAxOQKmDEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_oyeJqqviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.action name="_TlWCkamHEe6I4bA9GxwhqQ" org.eventb.core.assignment="triggered_events ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_oyeJq6viEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.action name="_mv5M0KpAEe6I4bA9GxwhqQ" org.eventb.core.assignment="subscriptions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act3;" org.eventb.emf.persistence.emf_id="_oyeJrKviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.action name="_8Ty9sKpBEe6I4bA9GxwhqQ" org.eventb.core.assignment="gateway_pending_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act4;" org.eventb.emf.persistence.emf_id="_oyeJraviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.action name="_J6KjYKpbEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_cross_chain_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act6;" org.eventb.emf.persistence.emf_id="_oyeJrqviEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_I9G5gKpAEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS" org.eventb.emf.persistence.emf_id="_oyeJsqviEe6I4bA9GxwhqQ">
+        <org.eventb.core.action name="_a_IQYKmDEe6I4bA9GxwhqQ" org.eventb.core.assignment="subscriptions ≔ subscriptions  ∪ {gateway ↦ source_smart_contract}" org.eventb.core.comment="The gateway is subscribed to listen to the smart contract events" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_oyeJsaviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_SAx1UKmDEe6I4bA9GxwhqQ" org.eventb.core.comment="The gateway is not already subscribed to the smart contract events" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="gateway ↦ source_smart_contract ∉ subscriptions" org.eventb.emf.persistence.emf_id="_oyeJsKviEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_58YTEKmAEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_oyeJt6viEe6I4bA9GxwhqQ">
+        <org.eventb.core.action name="_AeyzAKmIEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_transactions ≔ received_transactions ∪ {source_smart_contract ↦ transaction}" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_oyeJtqviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_TlWCkqmHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="transaction ∈ TRANSACTIONS" org.eventb.emf.persistence.emf_id="_oyeJtKviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_HCtL8KmIEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="grd3;" org.eventb.core.predicate="transaction ∉ received_transactions[{source_smart_contract}]" org.eventb.emf.persistence.emf_id="_oyeJtaviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.parameter name="_SAx1UqmDEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="transaction" org.eventb.emf.persistence.emf_id="_oyeJs6viEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_TlWCkKmHEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_oyeJvqviEe6I4bA9GxwhqQ">
+        <org.eventb.core.action name="_I9G5gapAEe6I4bA9GxwhqQ" org.eventb.core.assignment="triggered_events ≔  triggered_events ∪ {source_smart_contract ↦ cross_chain_event}" org.eventb.core.comment="The smart contract triggers a new event related to the transaction processing" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_oyeJvKviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.action name="_gaDEIKmHEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_transactions ≔ received_transactions ∖ {source_smart_contract ↦ transaction}" org.eventb.core.comment="The smart contract processed the transaction" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_oyeJvaviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_iUmtQKpAEe6I4bA9GxwhqQ" org.eventb.core.comment="The smart contract has a pending transaction to process" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ transaction ∈ received_transactions" org.eventb.emf.persistence.emf_id="_oyeJuqviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_1SOwwKmDEe6I4bA9GxwhqQ" org.eventb.core.comment="The smart contract will allways trigger a new event" org.eventb.core.generated="false" org.eventb.core.label="grd2;" org.eventb.core.predicate="cross_chain_event ∉ triggered_events[{source_smart_contract}]" org.eventb.emf.persistence.emf_id="_oyeJu6viEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.parameter name="_TlWCk6mHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="transaction" org.eventb.emf.persistence.emf_id="_oyeJuKviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.parameter name="_AezaEamIEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_event" org.eventb.emf.persistence.emf_id="_oyeJuaviEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_8VKFEKpAEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_SMART_CONTRACT_EVENT" org.eventb.emf.persistence.emf_id="_oyeJxqviEe6I4bA9GxwhqQ">
+        <org.eventb.core.action name="_8T0y4KpBEe6I4bA9GxwhqQ" org.eventb.core.assignment="gateway_pending_transactions ≔ gateway_pending_transactions ∪ {gateway ↦ cross_chain_transaction}" org.eventb.core.comment="The event is added to the cross-chain transactions to be processed by the gateway" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_oyeJxKviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.action name="_NAy78KpBEe6I4bA9GxwhqQ" org.eventb.core.assignment="triggered_events ≔ triggered_events ∖ {source_smart_contract ↦ cross_chain_event}" org.eventb.core.comment="The event is listened and processed" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_oyeJxaviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_DMOGsKpFEe6I4bA9GxwhqQ" org.eventb.core.comment="The smart contract has triggered an event" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ cross_chain_event ∈ triggered_events" org.eventb.emf.persistence.emf_id="_oyeJwaviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_AezaEKmIEe6I4bA9GxwhqQ" org.eventb.core.comment="Exist a subscription to the smart contract events" org.eventb.core.generated="false" org.eventb.core.label="grd2;" org.eventb.core.predicate="gateway ↦ source_smart_contract ∈ subscriptions" org.eventb.emf.persistence.emf_id="_oyeJwqviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_x51DwKpCEe6I4bA9GxwhqQ" org.eventb.core.comment="The event was not already listened" org.eventb.core.generated="false" org.eventb.core.label="grd3;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction ∉ gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_oyeJw6viEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.parameter name="_8VKsIqpAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_event" org.eventb.emf.persistence.emf_id="_oyeJv6viEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.parameter name="_8T1Z8qpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_transaction" org.eventb.emf.persistence.emf_id="_oyeJwKviEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_0sEN8KpaEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_oyeJy6viEe6I4bA9GxwhqQ">
+        <org.eventb.core.action name="_G1dcQKpbEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_cross_chain_transactions ≔ received_cross_chain_transactions ∪ {target_smart_contract ↦ cross_chain_transaction}" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_oyeJyaviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.action name="_G1dcQapbEe6I4bA9GxwhqQ" org.eventb.core.assignment="gateway_pending_transactions ≔  gateway_pending_transactions ∖ {gateway ↦ cross_chain_transaction}" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_oyeJyqviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_tUzFcKpaEe6I4bA9GxwhqQ" org.eventb.core.comment="There is one pending cross-chain transaction to process" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction ∈ gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_oyeJyKviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.parameter name="_tUzFcapaEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_transaction" org.eventb.emf.persistence.emf_id="_oyeJx6viEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.event>
+    <org.eventb.core.invariant name="_o6juoKviEe6I4bA9GxwhqQ" org.eventb.core.comment="Every transaction is submitted to a smart contract" org.eventb.core.generated="false" org.eventb.core.label="inv1;" org.eventb.core.predicate="received_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.emf.persistence.emf_id="_oyeJpaviEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.invariant name="_d6dcQKmHEe6I4bA9GxwhqQ" org.eventb.core.comment="Every event is triggered by a smart contract" org.eventb.core.generated="false" org.eventb.core.label="inv2;" org.eventb.core.predicate="triggered_events ∈ CROSS_CHAIN_SMART_CONTRACTS ↠ CROSS_CHAIN_EVENTS" org.eventb.emf.persistence.emf_id="_oyeJpqviEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.invariant name="_Q6dKkKpAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="inv3;" org.eventb.core.predicate="subscriptions ∈ GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.emf.persistence.emf_id="_oyeJp6viEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.invariant name="_c7TQ0KpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="inv4;" org.eventb.core.predicate="gateway_pending_transactions ∈ GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_oyeJqKviEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.invariant name="_G1eDUKpbEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="inv6;" org.eventb.core.predicate="received_cross_chain_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_oyeJqaviEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.variable name="_SAycYamDEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_oyeJoKviEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.variable name="_YvZFkamHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_oyeJoaviEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.variable name="_I9HgkapAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_oyeJoqviEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.variable name="_8T2BAKpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_oyeJo6viEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.variable name="_H2zkgKpbEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="received_cross_chain_transactions" org.eventb.emf.persistence.emf_id="_oyeJpKviEe6I4bA9GxwhqQ"/>
+</org.eventb.core.machineFile>

BIG/Ethereum_Fabric_m2.bpr

+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.prFile version="1"/>
\ No newline at end of file

BIG/Fabric_Ethereum_c2.bcc

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.scContextFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd;de.prob.symbolic.ctxBase">
+    <org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/BIG/BIG_c1.bcc|org.eventb.core.scContextFile#BIG_c1" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.extendsContext#'"/>
+    <org.eventb.core.scInternalContext name="BIG_c1">
+        <org.eventb.core.scAxiom name="'" org.eventb.core.label="axm1;" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-IUKsXEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scAxiom name="(" org.eventb.core.label="axm2;" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYKsXEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scAxiom name=")" org.eventb.core.label="axm3;" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYasXEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scConstant name="source_smart_contract" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.constant#_NmUHEKmBEe6I4bA9GxwhqQ" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.scCarrierSet name="CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_B7Fx4KmIEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+        <org.eventb.core.scConstant name="gateway" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.constant#_t3pvIKo_Ee6I4bA9GxwhqQ" org.eventb.core.type="GATEWAYS"/>
+        <org.eventb.core.scCarrierSet name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_lsmHUKpBEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.scCarrierSet name="GATEWAYS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_bUpUwKmAEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(GATEWAYS)"/>
+        <org.eventb.core.scConstant name="target_smart_contract" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.constant#_kx61gapGEe6I4bA9GxwhqQ" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.scCarrierSet name="TRANSACTIONS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_OLUJEKsXEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
+        <org.eventb.core.scCarrierSet name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_ISeO4KmBEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+    </org.eventb.core.scInternalContext>
+    <org.eventb.core.scCarrierSet name="ACCOUNTS" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.carrierSet#_u7_J0qsXEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(ACCOUNTS)"/>
+</org.eventb.core.scContextFile>

BIG/Fabric_Ethereum_c2.bpo

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.poFile org.eventb.core.poStamp="9">
+    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="9">
+        <org.eventb.core.poIdentifier name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+        <org.eventb.core.poIdentifier name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
+        <org.eventb.core.poIdentifier name="TRANSACTIONS" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+        <org.eventb.core.poIdentifier name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.poIdentifier name="gateway" org.eventb.core.type="GATEWAYS"/>
+        <org.eventb.core.poIdentifier name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTT" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-IUKsXEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTU" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYKsXEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTV" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYasXEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poIdentifier name="ACCOUNTS" org.eventb.core.type="ℙ(ACCOUNTS)"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_c2.bpo|org.eventb.core.poFile#Fabric_Ethereum_c2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="9"/>
+</org.eventb.core.poFile>

BIG/Fabric_Ethereum_c2.bpr

+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.prFile version="1"/>
\ No newline at end of file

BIG/Fabric_Ethereum_c2.bps

+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.psFile/>
\ No newline at end of file

BIG/Fabric_Ethereum_c2.buc

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd;de.prob.symbolic.ctxBase" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_1wfRkasZEe6I4bA9GxwhqQ" org.eventb.texttools.text_lastmodified="1704383796522" org.eventb.texttools.text_representation="context Fabric_Ethereum_c2 extends BIG_c1&#10;&#10;sets ACCOUNTS&#10;&#10;end&#10;" version="3">
+    <org.eventb.core.extendsContext name="'" org.eventb.core.target="BIG_c1"/>
+    <org.eventb.core.carrierSet name="_u7_J0qsXEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="ACCOUNTS" org.eventb.emf.persistence.emf_id="_1wfRkKsZEe6I4bA9GxwhqQ"/>
+</org.eventb.core.contextFile>

BIG/Fabric_Ethereum_m2.bpo

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.poFile org.eventb.core.poStamp="13">
+    <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="10">
+        <org.eventb.core.poIdentifier name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+        <org.eventb.core.poIdentifier name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
+        <org.eventb.core.poIdentifier name="TRANSACTIONS" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+        <org.eventb.core.poIdentifier name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.poIdentifier name="gateway" org.eventb.core.type="GATEWAYS"/>
+        <org.eventb.core.poIdentifier name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTT" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-IUKsXEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTU" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYKsXEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTV" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYasXEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poIdentifier name="ACCOUNTS" org.eventb.core.type="ℙ(ACCOUNTS)"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="13">
+        <org.eventb.core.poIdentifier name="balances" org.eventb.core.type="ℙ(ACCOUNTS×ℤ)"/>
+        <org.eventb.core.poIdentifier name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+        <org.eventb.core.poIdentifier name="received_cross_chain_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
+        <org.eventb.core.poIdentifier name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
+        <org.eventb.core.poPredicate name="received_cross_chain_transactiont" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="received_cross_chain_transactionu" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="received_cross_chain_transactionv" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_Q6dKkKpAEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="received_cross_chain_transactionw" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_c7TQ0KpBEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="received_cross_chain_transactionx" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_G1eDUKpbEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poSequent name="INITIALISATION/inv1;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="11">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiont"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="balances'∈ACCOUNTS ↔ ℕ1" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_sn-N4KsZEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqR"/>
+        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_sn-N4KsZEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poSequent#INITIALISATION\/inv1;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiont" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="11">
+        <org.eventb.core.poIdentifier name="triggered_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+        <org.eventb.core.poIdentifier name="gateway_pending_transactions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="balances'" org.eventb.core.type="ℙ(ACCOUNTS×ℤ)"/>
+        <org.eventb.core.poIdentifier name="received_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="subscriptions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
+        <org.eventb.core.poIdentifier name="received_cross_chain_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactiont" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiont" org.eventb.core.poStamp="11"/>
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionu" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="13">
+        <org.eventb.core.poIdentifier name="subscriptions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionu" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionu" org.eventb.core.poStamp="13">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="gateway ↦ source_smart_contract∉subscriptions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_I9G5gKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_SAx1UKmDEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="13">
+        <org.eventb.core.poIdentifier name="transaction" org.eventb.core.type="TRANSACTIONS"/>
+        <org.eventb.core.poIdentifier name="received_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionv" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.poStamp="13">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="transaction∈TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ|org.eventb.core.guard#_TlWCkqmHEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="transaction∉received_transactions[{source_smart_contract}]" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ|org.eventb.core.guard#_HCtL8KmIEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="13">
+        <org.eventb.core.poIdentifier name="triggered_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+        <org.eventb.core.poIdentifier name="transaction" org.eventb.core.type="TRANSACTIONS"/>
+        <org.eventb.core.poIdentifier name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+        <org.eventb.core.poIdentifier name="received_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionw" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.poStamp="13">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="source_smart_contract ↦ transaction∈received_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ|org.eventb.core.guard#_iUmtQKpAEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="cross_chain_event∉triggered_events[{source_smart_contract}]" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ|org.eventb.core.guard#_1SOwwKmDEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="13">
+        <org.eventb.core.poIdentifier name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
+        <org.eventb.core.poIdentifier name="triggered_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+        <org.eventb.core.poIdentifier name="gateway_pending_transactions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionx" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.poStamp="13">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="source_smart_contract ↦ cross_chain_event∈triggered_events" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_DMOGsKpFEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="gateway ↦ source_smart_contract∈subscriptions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_AezaEKmIEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_x51DwKpCEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="13">
+        <org.eventb.core.poIdentifier name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
+        <org.eventb.core.poIdentifier name="gateway_pending_transactions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="received_cross_chain_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactiony" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.poStamp="13">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∈gateway_pending_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_0sEN8KpaEe6I4bA9GxwhqQ|org.eventb.core.guard#_tUzFcKpaEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="13">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="balances∈ACCOUNTS ↔ ℕ1" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_sn-N4KsZEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.poPredicateSet>
+</org.eventb.core.poFile>