diff --git a/BIG/.project b/BIG/.project
new file mode 100644
index 0000000000000000000000000000000000000000..4d519899e14c6d7257e90cb48cf243dc5b475121
--- /dev/null
+++ b/BIG/.project
@@ -0,0 +1,17 @@
+<?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>
diff --git a/BIG/BIG_c1.bcc b/BIG/BIG_c1.bcc
new file mode 100644
index 0000000000000000000000000000000000000000..dc6dab94daa2be93e8c8eaebdb7ee9c05318c2ac
--- /dev/null
+++ b/BIG/BIG_c1.bcc
@@ -0,0 +1,14 @@
+<?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>
diff --git a/BIG/BIG_c1.bpo b/BIG/BIG_c1.bpo
new file mode 100644
index 0000000000000000000000000000000000000000..d3839e43dc13cbf18fb439603ba38f47330e1493
--- /dev/null
+++ b/BIG/BIG_c1.bpo
@@ -0,0 +1,18 @@
+<?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>
diff --git a/BIG/BIG_c1.bpr b/BIG/BIG_c1.bpr
new file mode 100644
index 0000000000000000000000000000000000000000..62b97ca7f30c74059f65a6cb53569c8a0769595e
--- /dev/null
+++ b/BIG/BIG_c1.bpr
@@ -0,0 +1,15 @@
+<?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>
diff --git a/BIG/BIG_c1.bps b/BIG/BIG_c1.bps
new file mode 100644
index 0000000000000000000000000000000000000000..f8ccc4bc6729e01b426a4e64400dbcafe7e5df15
--- /dev/null
+++ b/BIG/BIG_c1.bps
@@ -0,0 +1,2 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.psFile/>
diff --git a/BIG/BIG_c1.buc b/BIG/BIG_c1.buc
new file mode 100644
index 0000000000000000000000000000000000000000..2d1b905d6c3c1bcb7f5a8982550a730ab5a1792c
--- /dev/null
+++ b/BIG/BIG_c1.buc
@@ -0,0 +1,14 @@
+<?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>
diff --git a/BIG/BIG_m1.bcm b/BIG/BIG_m1.bcm
new file mode 100644
index 0000000000000000000000000000000000000000..5f9333c6b9aa355707d50ed876d29c7fc85cdfab
--- /dev/null
+++ b/BIG/BIG_m1.bcm
@@ -0,0 +1,67 @@
+<?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>
diff --git a/BIG/BIG_m1.bpo b/BIG/BIG_m1.bpo
new file mode 100644
index 0000000000000000000000000000000000000000..f5f29051b24e2a07cbe2ac944ea77137b1206942
--- /dev/null
+++ b/BIG/BIG_m1.bpo
@@ -0,0 +1,120 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.poFile org.eventb.core.poStamp="116">
+    <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="113">
+        <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.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="116">
+        <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="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.poPredicateSet>
+    <org.eventb.core.poSequent name="INITIALISATION/inv11;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="116">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiont"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#INITIALISATION\/inv11;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="INITIALISATION/inv2;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="116">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiont"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#INITIALISATION\/inv2;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiont" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="116">
+        <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="received_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×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_transactiont" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiont" org.eventb.core.poStamp="116"/>
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionu" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="116"/>
+    <org.eventb.core.poSequent name="SUBMIT_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="116">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionv"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="received_transactions∪{source_smart_contract ↦ transaction}∈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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#SUBMIT_CROSS_CHAIN_TRANSACTION\/inv11;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="116">
+        <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/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.poStamp="116">
+        <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.poSequent name="PROCESS_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="116">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionw"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="received_transactions ∖ {source_smart_contract ↦ transaction}∈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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#PROCESS_CROSS_CHAIN_TRANSACTION\/inv11;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="PROCESS_CROSS_CHAIN_TRANSACTION/inv2;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="116">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionw"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="triggered_events∪{source_smart_contract ↦ cross_chain_event}∈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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#PROCESS_CROSS_CHAIN_TRANSACTION\/inv2;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="116">
+        <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/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.poStamp="116">
+        <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.poSequent name="LISTEN_SMART_CONTRACT_EVENT/inv2;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="116">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionx"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="triggered_events ∖ {source_smart_contract ↦ cross_chain_event}∈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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#LISTEN_SMART_CONTRACT_EVENT\/inv2;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="116">
+        <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/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.poStamp="116">
+        <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 ↦ 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/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="116">
+        <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/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.poStamp="116">
+        <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/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="116">
+        <org.eventb.core.poPredicate name="PRD0" 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="PRD1" 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="PRD2" 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="PRD3" 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.poFile>
diff --git a/BIG/BIG_m1.bpo_tmp b/BIG/BIG_m1.bpo_tmp
new file mode 100644
index 0000000000000000000000000000000000000000..1daa70d8814e39ef405b0dcd5b6599163524d97c
--- /dev/null
+++ b/BIG/BIG_m1.bpo_tmp
@@ -0,0 +1,2 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.poFile/>
\ No newline at end of file
diff --git a/BIG/BIG_m1.bpr b/BIG/BIG_m1.bpr
new file mode 100644
index 0000000000000000000000000000000000000000..19b33785d3ff78bf93674813735c58457679f8d6
--- /dev/null
+++ b/BIG/BIG_m1.bpr
@@ -0,0 +1,262 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.prFile version="1">
+    <org.eventb.core.prProof name="INITIALISATION/inv1;/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="" org.eventb.core.prSets="CROSS_CHAIN_SMART_CONTRACTS,TRANSACTIONS">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
+                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="(∅ ⦂ ℙ(ℙ(ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS))))⊆{CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS}"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="card(GATEWAYS)=1">
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="∃x⦂GATEWAYS·GATEWAYS={x}">
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="SUBMIT_CROSS_CHAIN_TRANSACTION/inv1;/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p0" org.eventb.core.prSets="CROSS_CHAIN_SMART_CONTRACTS,TRANSACTIONS">
+        <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.prIdent name="received_transactions" org.eventb.core.type="ℙ(ℙ(CROSS_CHAIN_SMART_CONTRACTS)×ℙ(TRANSACTIONS))"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="received_transactions⊆{CROSS_CHAIN_SMART_CONTRACTS ↦ TRANSACTIONS}"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.hyp"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="inv7;/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,CROSS_CHAIN_SMART_CONTRACTS">
+        <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.prIdent name="blockchain_smart_contracts" org.eventb.core.type="ℙ(BLOCKCHAINS×CROSS_CHAIN_SMART_CONTRACTS)"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="finite(blockchain_smart_contracts)"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.hyp"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="INITIALISATION/inv6;/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="" org.eventb.core.prSets="BLOCKCHAINS,CROSS_CHAIN_SMART_CONTRACTS">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
+                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="source_blockchain" org.eventb.core.type="BLOCKCHAINS"/>
+        <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.prIdent name="target_blockchain" org.eventb.core.type="BLOCKCHAINS"/>
+        <org.eventb.core.prIdent name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="finite({source_blockchain ↦ source_smart_contract}∪{target_blockchain ↦ target_smart_contract})"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="card(GATEWAYS)=1">
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="∃x⦂GATEWAYS·GATEWAYS={x}">
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="INITIALISATION/inv7;/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="" org.eventb.core.prSets="BLOCKCHAINS,CROSS_CHAIN_SMART_CONTRACTS">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
+                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+                    <org.eventb.core.prAnte name="'">
+                        <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p5"/>
+                        <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p6"/>
+                        <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p7"/>
+                        <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p8"/>
+                        <org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p9"/>
+                    </org.eventb.core.prAnte>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="source_blockchain" org.eventb.core.type="BLOCKCHAINS"/>
+        <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.prIdent name="target_blockchain" org.eventb.core.type="BLOCKCHAINS"/>
+        <org.eventb.core.prIdent name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="finite({source_blockchain ↦ source_smart_contract}∪{target_blockchain ↦ target_smart_contract})"/>
+        <org.eventb.core.prPred name="p9" org.eventb.core.predicate="gateway∈GATEWAYS">
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="card(GATEWAYS)=1">
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="source_blockchain∈BLOCKCHAINS"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="1+1 − card({source_blockchain ↦ source_smart_contract}∩{target_blockchain ↦ target_smart_contract})=2"/>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="target_blockchain∈BLOCKCHAINS"/>
+        <org.eventb.core.prPred name="p8" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="card({source_blockchain ↦ source_smart_contract}∪{target_blockchain ↦ target_smart_contract})=2"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="∃x⦂GATEWAYS·GATEWAYS={x}">
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="INITIALISATION/inv11;/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p0"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p2"/>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="gateway∈GATEWAYS">
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="SUBMIT_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p0" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p1"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+                    <org.eventb.core.prAnte name="'">
+                        <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p2"/>
+                        <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
+                        <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p4"/>
+                        <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p5"/>
+                        <org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p6"/>
+                        <org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p7"/>
+                        <org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p8"/>
+                        <org.eventb.core.prHypAction name="HIDE7" org.eventb.core.prHyps="p9"/>
+                    </org.eventb.core.prAnte>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="¬transaction∈received_transactions[{source_smart_contract}]">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="TRANSACTIONS" org.eventb.core.type="â„™(TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+            <org.eventb.core.prIdent name="transaction" org.eventb.core.type="TRANSACTIONS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway∈GATEWAYS">
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="â„™(CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="transaction∉received_transactions[{source_smart_contract}]">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="TRANSACTIONS" org.eventb.core.type="â„™(TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+            <org.eventb.core.prIdent name="transaction" org.eventb.core.type="TRANSACTIONS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p9" org.eventb.core.predicate="transaction∈TRANSACTIONS">
+            <org.eventb.core.prIdent name="TRANSACTIONS" org.eventb.core.type="â„™(TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="transaction" org.eventb.core.type="TRANSACTIONS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="â„™(CROSS_CHAIN_TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p8" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="â„™(CROSS_CHAIN_TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="received_cross_chain_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="PROCESS_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p0" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p1"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+                    <org.eventb.core.prAnte name="'">
+                        <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p2"/>
+                        <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
+                        <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p4"/>
+                        <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p5"/>
+                        <org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p6"/>
+                        <org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p7"/>
+                        <org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p8"/>
+                    </org.eventb.core.prAnte>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway∈GATEWAYS">
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="â„™(CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="¬cross_chain_event∈triggered_events[{source_smart_contract}]">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="â„™(CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+            <org.eventb.core.prIdent name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="cross_chain_event∉triggered_events[{source_smart_contract}]">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="â„™(CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+            <org.eventb.core.prIdent name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="â„™(CROSS_CHAIN_TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p8" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="â„™(CROSS_CHAIN_TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="received_cross_chain_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+    </org.eventb.core.prProof>
+</org.eventb.core.prFile>
diff --git a/BIG/BIG_m1.bps b/BIG/BIG_m1.bps
new file mode 100644
index 0000000000000000000000000000000000000000..e8ba065565fd53002e0748f6def4ac5fa8e84e6a
--- /dev/null
+++ b/BIG/BIG_m1.bps
@@ -0,0 +1,6 @@
+<?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>
diff --git a/BIG/BIG_m1.bum b/BIG/BIG_m1.bum
new file mode 100644
index 0000000000000000000000000000000000000000..f2c3f6d0ee954353bd25e3a60f1b33cb1da1b9b8
--- /dev/null
+++ b/BIG/BIG_m1.bum
@@ -0,0 +1,54 @@
+<?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>
diff --git a/BIG/Ethereum_Fabric_m2.bpr b/BIG/Ethereum_Fabric_m2.bpr
new file mode 100644
index 0000000000000000000000000000000000000000..d13ec2a20267852024def0758a1effc175861a98
--- /dev/null
+++ b/BIG/Ethereum_Fabric_m2.bpr
@@ -0,0 +1,2 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.prFile version="1"/>
\ No newline at end of file
diff --git a/BIG/Fabric_Ethereum_c2.bcc b/BIG/Fabric_Ethereum_c2.bcc
new file mode 100644
index 0000000000000000000000000000000000000000..753604b94311311dd7e3853d33d2ea7adf2c674b
--- /dev/null
+++ b/BIG/Fabric_Ethereum_c2.bcc
@@ -0,0 +1,18 @@
+<?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>
diff --git a/BIG/Fabric_Ethereum_c2.bpo b/BIG/Fabric_Ethereum_c2.bpo
new file mode 100644
index 0000000000000000000000000000000000000000..86a693c28d20591b275c7fd72d0c9489efcca74a
--- /dev/null
+++ b/BIG/Fabric_Ethereum_c2.bpo
@@ -0,0 +1,18 @@
+<?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>
diff --git a/BIG/Fabric_Ethereum_c2.bpr b/BIG/Fabric_Ethereum_c2.bpr
new file mode 100644
index 0000000000000000000000000000000000000000..d13ec2a20267852024def0758a1effc175861a98
--- /dev/null
+++ b/BIG/Fabric_Ethereum_c2.bpr
@@ -0,0 +1,2 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.prFile version="1"/>
\ No newline at end of file
diff --git a/BIG/Fabric_Ethereum_c2.bps b/BIG/Fabric_Ethereum_c2.bps
new file mode 100644
index 0000000000000000000000000000000000000000..ced513e210f482c3c7cafb26e5e709e8b27ac922
--- /dev/null
+++ b/BIG/Fabric_Ethereum_c2.bps
@@ -0,0 +1,2 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.psFile/>
\ No newline at end of file
diff --git a/BIG/Fabric_Ethereum_c2.buc b/BIG/Fabric_Ethereum_c2.buc
new file mode 100644
index 0000000000000000000000000000000000000000..a153e18a949a1d20e718e7ce837d0b675f15d85e
--- /dev/null
+++ b/BIG/Fabric_Ethereum_c2.buc
@@ -0,0 +1,5 @@
+<?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>
diff --git a/BIG/Fabric_Ethereum_m2.bcm b/BIG/Fabric_Ethereum_m2.bcm
new file mode 100644
index 0000000000000000000000000000000000000000..7895852a5ee31a14d3ea92cf69c12b4e9bd49e55
--- /dev/null
+++ b/BIG/Fabric_Ethereum_m2.bcm
@@ -0,0 +1,81 @@
+<?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.scRefinesMachine name="'" org.eventb.core.scTarget="/BIG/BIG_m1.bcm" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.refinesMachine#'"/>
+    <org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/BIG/Fabric_Ethereum_c2.bcc" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.seesContext#_wnFu0KsZEe6I4bA9GxwhqQ"/>
+    <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.scInternalContext name="Fabric_Ethereum_c2">
+        <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.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.scInternalContext>
+    <org.eventb.core.scInvariant name="BIG_c2" org.eventb.core.label="inv11;" 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.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.scInvariant name="Fabric_Ethereum_c3" org.eventb.core.label="inv1;" 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.theorem="false"/>
+    <org.eventb.core.scVariable name="balances" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.variable#_DPQj0KsaEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(ACCOUNTS×ℤ)"/>
+    <org.eventb.core.scVariable name="triggered_events" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|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="true" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|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="true" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|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="true" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.variable#_8T2BAKpBEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+    <org.eventb.core.scVariable name="received_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|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="false" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" 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.scRefinesEvent name="'" org.eventb.core.scTarget="/BIG/BIG_m1.bcm|org.eventb.core.scMachineFile#BIG_m1|org.eventb.core.scEvent#received_cross_chain_transactiont" 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.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.scAction name="," org.eventb.core.assignment="balances :∣ ⊤" org.eventb.core.label="GEN" 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.scEvent>
+    <org.eventb.core.scEvent name="received_cross_chain_transactionu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqS">
+        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/BIG/BIG_m1.bcm|org.eventb.core.scMachineFile#BIG_m1|org.eventb.core.scEvent#received_cross_chain_transactionu" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqS|org.eventb.core.refinesEvent#'"/>
+        <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="true" org.eventb.core.label="SUBMIT_CROSS_CHAIN_TRANSACTION" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqT">
+        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/BIG/BIG_m1.bcm|org.eventb.core.scMachineFile#BIG_m1|org.eventb.core.scEvent#received_cross_chain_transactionv" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqT|org.eventb.core.refinesEvent#'"/>
+        <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.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.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.scEvent>
+    <org.eventb.core.scEvent name="received_cross_chain_transactionw" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqU">
+        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/BIG/BIG_m1.bcm|org.eventb.core.scMachineFile#BIG_m1|org.eventb.core.scEvent#received_cross_chain_transactionw" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqU|org.eventb.core.refinesEvent#'"/>
+        <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.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.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.scEvent>
+    <org.eventb.core.scEvent name="received_cross_chain_transactionx" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="LISTEN_SMART_CONTRACT_EVENT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqV">
+        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/BIG/BIG_m1.bcm|org.eventb.core.scMachineFile#BIG_m1|org.eventb.core.scEvent#received_cross_chain_transactionx" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqV|org.eventb.core.refinesEvent#'"/>
+        <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.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.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.scEvent>
+    <org.eventb.core.scEvent name="received_cross_chain_transactiony" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqW">
+        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/BIG/BIG_m1.bcm|org.eventb.core.scMachineFile#BIG_m1|org.eventb.core.scEvent#received_cross_chain_transactiony" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqW|org.eventb.core.refinesEvent#'"/>
+        <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.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.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.scEvent>
+</org.eventb.core.scMachineFile>
diff --git a/BIG/Fabric_Ethereum_m2.bpo b/BIG/Fabric_Ethereum_m2.bpo
new file mode 100644
index 0000000000000000000000000000000000000000..c6cc1e4d895633f94fa16637a3a477b66afd6ad4
--- /dev/null
+++ b/BIG/Fabric_Ethereum_m2.bpo
@@ -0,0 +1,94 @@
+<?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>
diff --git a/BIG/Fabric_Ethereum_m2.bpr b/BIG/Fabric_Ethereum_m2.bpr
new file mode 100644
index 0000000000000000000000000000000000000000..33fc5c29e9f4a30bc19efe3d345ff2fbde06ddb4
--- /dev/null
+++ b/BIG/Fabric_Ethereum_m2.bpr
@@ -0,0 +1,26 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.prFile version="1">
+    <org.eventb.core.prProof name="INITIALISATION/inv1;/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p0"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p2"/>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="gateway∈GATEWAYS">
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="â„™(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+    </org.eventb.core.prProof>
+</org.eventb.core.prFile>
diff --git a/BIG/Fabric_Ethereum_m2.bps b/BIG/Fabric_Ethereum_m2.bps
new file mode 100644
index 0000000000000000000000000000000000000000..90cd9acf661cb6b2573898ddd7ffc5a46aa0b485
--- /dev/null
+++ b/BIG/Fabric_Ethereum_m2.bps
@@ -0,0 +1,4 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.psFile>
+    <org.eventb.core.psStatus name="INITIALISATION/inv1;/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+</org.eventb.core.psFile>
diff --git a/BIG/Fabric_Ethereum_m2.bum b/BIG/Fabric_Ethereum_m2.bum
new file mode 100644
index 0000000000000000000000000000000000000000..4edd2bad99f8ca767539106dfc472b7774884ed1
--- /dev/null
+++ b/BIG/Fabric_Ethereum_m2.bum
@@ -0,0 +1,28 @@
+<?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="_MkFlQ6saEe6I4bA9GxwhqQ" org.eventb.texttools.text_lastmodified="1704383949573" org.eventb.texttools.text_representation="machine Fabric_Ethereum_m2 refines BIG_m1  sees Fabric_Ethereum_c2&#10;&#10;variables received_transactions triggered_events subscriptions gateway_pending_transactions&#10;received_cross_chain_transactions balances&#10;&#10;invariants&#10;&#9;@inv1: balances ∈ ACCOUNTS ↔ ℕ1&#10;&#10;events&#10;  event INITIALISATION extends INITIALISATION&#10;  end&#10;&#10;  event SUBSCRIBE_SMART_CONTRACT_EVENTS extends SUBSCRIBE_SMART_CONTRACT_EVENTS&#10;  end&#10;&#10;  event SUBMIT_CROSS_CHAIN_TRANSACTION extends SUBMIT_CROSS_CHAIN_TRANSACTION&#10;  end&#10;&#10;  event PROCESS_CROSS_CHAIN_TRANSACTION extends PROCESS_CROSS_CHAIN_TRANSACTION&#10;  end&#10;&#10;  event LISTEN_SMART_CONTRACT_EVENT extends LISTEN_SMART_CONTRACT_EVENT&#10;  end&#10;&#10;  event GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION extends GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION&#10;  end&#10;end&#10;" version="5">
+    <org.eventb.core.refinesMachine name="'" org.eventb.core.target="BIG_m1"/>
+    <org.eventb.core.seesContext name="_wnFu0KsZEe6I4bA9GxwhqQ" org.eventb.core.target="Fabric_Ethereum_c2"/>
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqR" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION" org.eventb.emf.persistence.emf_id="_MkFlN6saEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqS" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS" org.eventb.emf.persistence.emf_id="_MkFlOasaEe6I4bA9GxwhqQ">
+        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqT" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_MkFlO6saEe6I4bA9GxwhqQ">
+        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBMIT_CROSS_CHAIN_TRANSACTION"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqU" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_MkFlPasaEe6I4bA9GxwhqQ">
+        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="PROCESS_CROSS_CHAIN_TRANSACTION"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqV" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_SMART_CONTRACT_EVENT" org.eventb.emf.persistence.emf_id="_MkFlP6saEe6I4bA9GxwhqQ">
+        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="LISTEN_SMART_CONTRACT_EVENT"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqW" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_MkFlQasaEe6I4bA9GxwhqQ">
+        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION"/>
+    </org.eventb.core.event>
+    <org.eventb.core.invariant name="_sn-N4KsZEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="inv1;" org.eventb.core.predicate="balances ∈ ACCOUNTS ↔ ℕ1" org.eventb.emf.persistence.emf_id="_MkFlNqsaEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.variable name="_SAycYamDEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_MkFlMKsaEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.variable name="_YvZFkamHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_MkFlMasaEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.variable name="_I9HgkapAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_MkFlMqsaEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.variable name="_8T2BAKpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_MkFlM6saEe6I4bA9GxwhqQ"/>
+    <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="_MkFlNKsaEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.variable name="_DPQj0KsaEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="balances" org.eventb.emf.persistence.emf_id="_MkFlNasaEe6I4bA9GxwhqQ"/>
+</org.eventb.core.machineFile>