<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.prFile version="1">
    <org.eventb.core.prProof name="INITIALISATION/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="INITIALISATION/inv16/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway ↦ source_smart_contract∉subscriptions">
            <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="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
            <org.eventb.core.prIdent name="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬gateway ↦ source_smart_contract∈subscriptions">
            <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="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
            <org.eventb.core.prIdent name="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="INITIATE_CC_TX_IN_ETHEREUM/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p5" 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="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="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="INITIATE_CC_TX_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p5" 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="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="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="TRIGGER_CC_TX_EVENT_IN_ETHEREUM/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p5" 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="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" 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="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="TRIGGER_CC_TX_EVENT_IN_ETHEREUM/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p5" 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="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" 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="1∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="TRIGGER_CC_TX_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p5" 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="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" 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="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="LISTEN_CC_TX_EVENT_IN_ETHEREUM/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_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="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
            <org.eventb.core.prIdent name="gateway" 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="p5" org.eventb.core.predicate="¬gateway ↦ cross_chain_transaction∈gateway_pending_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="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
            <org.eventb.core.prIdent name="gateway" 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="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="LISTEN_CC_TX_EVENT_IN_ETHEREUM/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_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="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
            <org.eventb.core.prIdent name="gateway" 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="p5" org.eventb.core.predicate="¬gateway ↦ cross_chain_transaction∈gateway_pending_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="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
            <org.eventb.core.prIdent name="gateway" 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="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="LISTEN_CC_TX_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_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="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
            <org.eventb.core.prIdent name="gateway" 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="p5" org.eventb.core.predicate="¬gateway ↦ cross_chain_transaction∈gateway_pending_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="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
            <org.eventb.core.prIdent name="gateway" 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="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="SUBMIT_CC_TX_TO_FABRIC/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="SUBMIT_CC_TX_TO_FABRIC/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="CREATE_GATEWAY_USER/inv16/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway_user∉authenticated_users">
            <org.eventb.core.prIdent name="USERS" org.eventb.core.type="ℙ(USERS)"/>
            <org.eventb.core.prIdent name="authenticated_users" org.eventb.core.type="ℙ(USERS)"/>
            <org.eventb.core.prIdent name="gateway_user" org.eventb.core.type="USERS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬gateway_user∈authenticated_users">
            <org.eventb.core.prIdent name="USERS" org.eventb.core.type="ℙ(USERS)"/>
            <org.eventb.core.prIdent name="authenticated_users" org.eventb.core.type="ℙ(USERS)"/>
            <org.eventb.core.prIdent name="gateway_user" org.eventb.core.type="USERS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="INITIALISATION/inv17/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="GRANT_PERMISSION/inv17/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬user ↦ permission∈grants">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="USERS" org.eventb.core.type="ℙ(USERS)"/>
            <org.eventb.core.prIdent name="grants" org.eventb.core.type="ℙ(USERS×PERMISSIONS)"/>
            <org.eventb.core.prIdent name="permission" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="user" org.eventb.core.type="USERS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="user ↦ permission∉grants">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="USERS" org.eventb.core.type="ℙ(USERS)"/>
            <org.eventb.core.prIdent name="grants" org.eventb.core.type="ℙ(USERS×PERMISSIONS)"/>
            <org.eventb.core.prIdent name="permission" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="user" org.eventb.core.type="USERS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="EMIT_CC_TX_EVENT_IN_ETHEREUM/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="cross_chain_event∉emitted_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="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
            <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="p5" org.eventb.core.predicate="¬cross_chain_event∈emitted_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="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
            <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="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="EMIT_CC_TX_EVENT_IN_ETHEREUM/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="cross_chain_event∉emitted_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="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
            <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="p5" org.eventb.core.predicate="¬cross_chain_event∈emitted_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="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
            <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="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="EMIT_CC_TX_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="cross_chain_event∉emitted_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="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
            <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="p5" org.eventb.core.predicate="¬cross_chain_event∈emitted_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="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
            <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="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="EMIT_EVENT_IN_ETHEREUM/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="emitted_event∉emitted_events[{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="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <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="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬emitted_event∈emitted_events[{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="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <org.eventb.core.prIdent name="source_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.partitionRewrites"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="EMIT_EVENT_IN_ETHEREUM/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="emitted_event∉emitted_events[{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="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <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="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬emitted_event∈emitted_events[{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="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <org.eventb.core.prIdent name="source_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.partitionRewrites"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="EMIT_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="emitted_event∉emitted_events[{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="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <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="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬emitted_event∈emitted_events[{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="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <org.eventb.core.prIdent name="source_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.partitionRewrites"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="LISTEN_EVENT_IN_ETHEREUM/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway ↦ pending_event∉gateway_pending_events">
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_events" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬gateway ↦ pending_event∈gateway_pending_events">
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_events" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="LISTEN_EVENT_IN_ETHEREUM/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway ↦ pending_event∉gateway_pending_events">
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_events" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬gateway ↦ pending_event∈gateway_pending_events">
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_events" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="LISTEN_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway ↦ pending_event∉gateway_pending_events">
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_events" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬gateway ↦ pending_event∈gateway_pending_events">
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_events" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="SUBMIT_TX_TO_FABRIC/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="SUBMIT_TX_TO_FABRIC/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" 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="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps=""/>
                    </org.eventb.core.prAnte>
                </org.eventb.core.prRule>
            </org.eventb.core.prAnte>
            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
</org.eventb.core.prFile>