m2_motor_context.buc

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.core.generated="false" org.eventb.texttools.text_lastmodified="1590749091316" org.eventb.texttools.text_representation="context m2_motor_context extends m1_shafts_context&#10;&#10;sets MOTOR_STATE&#10;&#10;constants ON OFF&#10;&#10;axioms&#10;@motor_finite finite(MOTOR_STATE)&#10;@motor partition(MOTOR_STATE, {ON}, {OFF}) //REQ 6&#10;end&#10;" version="3">
<org.eventb.core.extendsContext name="_LAqS8J-XEeq6js3PozKjqQ" org.eventb.core.target="m1_shafts_context"/>
<org.eventb.core.carrierSet name="__eDggJ-YEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="MOTOR_STATE"/>
<org.eventb.core.constant name="__eEHkJ-YEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="ON"/>
<org.eventb.core.constant name="__eEHkZ-YEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="OFF"/>
<org.eventb.core.axiom name="_brXfUKFQEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="motor_finite" org.eventb.core.predicate="finite(MOTOR_STATE)"/>
<org.eventb.core.axiom name="_brXfUaFQEeq6js3PozKjqQ" org.eventb.core.comment="REQ 6" org.eventb.core.generated="false" org.eventb.core.label="motor" org.eventb.core.predicate="partition(MOTOR_STATE, {ON}, {OFF})"/>
</org.eventb.core.contextFile>