CCTx_Ethereum_Fabric_Animation_m3.bpr

            <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.prFile>