1		package(load_event_b_project([event_b_model(none,drone_0,[sees(none,[basis_ctx,drone_0_ctx]),refines(none,basis),variables(none,[identifier(none,'START'),identifier(none,'OFF'),identifier(none,'SHUTDOWN'),identifier(none,'SCXML_iq'),identifier(none,'SCXML_eq'),identifier(none,'SCXML_dt'),identifier(none,'SCXML_uc'),identifier(none,'OPERATIONAL')]),invariant(none,[member(rodinpos(drone_0,typeof_OFF,'_4QE8QOYfEemvmYCWQGpCPA'),identifier(none,'OFF'),bool_set(none)),member(rodinpos(drone_0,typeof_START,'_4QE8QeYfEemvmYCWQGpCPA'),identifier(none,'START'),bool_set(none)),member(rodinpos(drone_0,typeof_OPERATIONAL,'_4QFjUOYfEemvmYCWQGpCPA'),identifier(none,'OPERATIONAL'),bool_set(none)),member(rodinpos(drone_0,typeof_SHUTDOWN,'_4QFjUeYfEemvmYCWQGpCPA'),identifier(none,'SHUTDOWN'),bool_set(none)),partition(rodinpos(drone_0,distinct_states_in_drone_sm,'_4QGKYOYfEemvmYCWQGpCPA'),set_extension(none,[boolean_true(none)]),[intersection(none,set_extension(none,[identifier(none,'OFF')]),set_extension(none,[boolean_true(none)])),intersection(none,set_extension(none,[identifier(none,'START')]),set_extension(none,[boolean_true(none)])),intersection(none,set_extension(none,[identifier(none,'OPERATIONAL')]),set_extension(none,[boolean_true(none)])),intersection(none,set_extension(none,[identifier(none,'SHUTDOWN')]),set_extension(none,[boolean_true(none)]))])]),theorems(none,[]),events(none,[event(rodinpos(drone_0,'INITIALISATION','_4Kre4OYfEemvmYCWQGpCPA'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(drone_0,init_SCXML_iq,'_4KB-oOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_iq')],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))]),assign(rodinpos(drone_0,init_SCXML_eq,'_4KB-oeYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_eq')],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))]),assign(rodinpos(drone_0,'SCXML_setNotComplete','_4KClsOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_uc')],[boolean_false(none)]),assign(rodinpos(drone_0,init_SCXML_dt,'_4KClseYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_dt')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))]),assign(rodinpos(drone_0,init_OFF,'_4P59IOYfEemvmYCWQGpCPA'),[identifier(none,'OFF')],[boolean_true(none)]),assign(rodinpos(drone_0,init_START,'_4P59IeYfEemvmYCWQGpCPA'),[identifier(none,'START')],[boolean_false(none)]),assign(rodinpos(drone_0,init_OPERATIONAL,'_4P6kMOYfEemvmYCWQGpCPA'),[identifier(none,'OPERATIONAL')],[boolean_false(none)]),assign(rodinpos(drone_0,init_SHUTDOWN,'_4P6kMeYfEemvmYCWQGpCPA'),[identifier(none,'SHUTDOWN')],[boolean_false(none)])],[]),event(rodinpos(drone_0,'SCXML_futureRaiseExternalTrigger','_4Kre4eYfEemvmYCWQGpCPA'),'SCXML_futureRaiseExternalTrigger',anticipated(none),['SCXML_futureRaiseExternalTrigger'],[identifier(rodinpos(drone_0,[],'_4KDz0OYfEemvmYCWQGpCPA'),'SCXML_raisedTrigger')],[member(rodinpos(drone_0,typeof_SCXML_raisedTriggers,'_4KDz0eYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTrigger'),identifier(none,'SCXML_FutureExternalTrigger')),member(rodinpos(drone_0,typeof_SCXML_raisedTriggers0,'_4KsF8eYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTrigger'),identifier(none,'SCXML_FutureExternalTrigger0'))],[],[assign(rodinpos(drone_0,'SCXML_raiseExternalTriggers','_4KEa4OYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_eq')],[function(none,identifier(none,'Seq_append'),[couple(none,[identifier(none,'SCXML_eq'),identifier(none,'SCXML_raisedTrigger')])])])],[]),event(rodinpos(drone_0,'SCXML_dequeueInternalTrigger','_4KstAOYfEemvmYCWQGpCPA'),'SCXML_dequeueInternalTrigger',anticipated(none),['SCXML_dequeueInternalTrigger'],[],[not_equal(rodinpos(drone_0,grd1,'_4KHeMOYfEemvmYCWQGpCPB'),identifier(none,'SCXML_iq'),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))),equal(rodinpos(drone_0,'SCXML_hasNoDequeuedTriggers','_4KFpAeYfEemvmYCWQGpCPA'),identifier(none,'SCXML_dt'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))),equal(rodinpos(drone_0,'SCXML_isComplete','_4KGQEOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_true(none))],[equal(rodinpos(drone_0,'PO','_4KHeMOYfEemvmYCWQGpCPC'),function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_iq')]),union(none,set_extension(none,[function(none,identifier(none,'Seq_head'),[identifier(none,'SCXML_iq')])]),function(none,identifier(none,'Seq_content'),[function(none,identifier(none,'Seq_tail'),[identifier(none,'SCXML_iq')])])))],[assign(rodinpos(drone_0,'SCXML_storeDequeuedTrigger','_4KGQEeYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_dt')],[set_extension(none,[function(none,identifier(none,'Seq_head'),[identifier(none,'SCXML_iq')])])]),assign(rodinpos(drone_0,'SCXML_consumeDequeuedTrigger','_4KG3IOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_iq')],[function(none,identifier(none,'Seq_tail'),[identifier(none,'SCXML_iq')])]),assign(rodinpos(drone_0,'SCXML_setNotComplete','_4KHeMOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_uc')],[boolean_false(none)])],[]),event(rodinpos(drone_0,'SCXML_dequeueExternalTrigger','_4KstAuYfEemvmYCWQGpCPA'),'SCXML_dequeueExternalTrigger',anticipated(none),['SCXML_dequeueExternalTrigger'],[],[not_equal(rodinpos(drone_0,grd1,grd1),identifier(none,'SCXML_eq'),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))),equal(rodinpos(drone_0,'SCXML_hasNoDequeuedTriggers','_4KLIkOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_dt'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))),equal(rodinpos(drone_0,'SCXML_isComplete','_4KLvoOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_true(none)),equal(rodinpos(drone_0,'SCXML_internalQEmpty','_4KMWsOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_iq'),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))))],[],[assign(rodinpos(drone_0,'SCXML_storeDequeuedTrigger','_4KM9wOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_dt')],[set_extension(none,[function(none,identifier(none,'Seq_head'),[identifier(none,'SCXML_eq')])])]),assign(rodinpos(drone_0,'SCXML_consumeDequeuedTrigger','_4KNk0OYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_eq')],[function(none,identifier(none,'Seq_tail'),[identifier(none,'SCXML_eq')])]),assign(rodinpos(drone_0,'SCXML_setNotComplete','_4KOL4OYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_uc')],[boolean_false(none)])],[]),event(rodinpos(drone_0,'SCXML_futureTriggeredTransitionSet','_4KtUEeYfEemvmYCWQGpCPA'),'SCXML_futureTriggeredTransitionSet',anticipated(none),['SCXML_futureTriggeredTransitionSet'],[identifier(rodinpos(drone_0,[],'_4KOy8OYfEemvmYCWQGpCPA'),'SCXML_trigger'),identifier(rodinpos(drone_0,[],'_4KPaAOYfEemvmYCWQGpCPA'),'SCXML_raisedTriggers')],[member(rodinpos(drone_0,typeof_SCXML_trigger,'_4KPaAeYfEemvmYCWQGpCPA'),identifier(none,'SCXML_trigger'),identifier(none,'SCXML_dt')),equal(rodinpos(drone_0,'SCXML_isNotComplete','_4KQBEOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_false(none)),member(rodinpos(drone_0,typeof_SCXML_raisedTriggers,'_4KQoIOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTriggers'),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_FutureInternalTrigger')])),not_member(rodinpos(drone_0,'SCXML_triggersInThisRefinement_0','_4Kt7IOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_trigger'),set_extension(none,[identifier(none,toTakeoff),identifier(none,off),identifier(none,on)]))],[equal(rodinpos(drone_0,'PO','_4KRPMeYfEemvmYCWQGpCPB'),function(none,identifier(none,'Seq_content'),[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])]),union(none,function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_iq')]),function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_raisedTriggers')])))],[assign(rodinpos(drone_0,'SCXML_clearDequeuedTriggers','_4KRPMOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_dt')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))]),assign(rodinpos(drone_0,'SCXML_raiseInternalTriggers','_4KRPMeYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_iq')],[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])])],[]),event(rodinpos(drone_0,'SCXML_noTriggeredTransitionsEnabled','_4Kt7IeYfEemvmYCWQGpCPA'),'SCXML_noTriggeredTransitionsEnabled',anticipated(none),['SCXML_noTriggeredTransitionsEnabled'],[],[equal(rodinpos(drone_0,'SCXML_isNotComplete','_4KTEYOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_false(none)),not_equal(rodinpos(drone_0,'SCXML_hasDequeuedTriggers','_4KTrcOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_dt'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER'))))],[],[assign(rodinpos(drone_0,'SCXML_clearDequeuedTriggers','_4KTrceYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_dt')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))])],[]),event(rodinpos(drone_0,'SCXML_futureUntriggeredTransitionSet','_4KuiMeYfEemvmYCWQGpCPA'),'SCXML_futureUntriggeredTransitionSet',anticipated(none),['SCXML_futureUntriggeredTransitionSet'],[identifier(rodinpos(drone_0,[],'_4KUSgeYfEemvmYCWQGpCPA'),'SCXML_raisedTriggers')],[equal(rodinpos(drone_0,'SCXML_isNotComplete','_4KU5kOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_false(none)),equal(rodinpos(drone_0,'SCXML_hasNoDequeuedTriggers','_4KU5keYfEemvmYCWQGpCPA'),identifier(none,'SCXML_dt'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))),member(rodinpos(drone_0,typeof_SCXML_raisedTriggers,'_4KVgoOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTriggers'),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_FutureInternalTrigger')]))],[equal(rodinpos(drone_0,'PO','_4KVgoeYfEemvmYCWQGpCPB'),function(none,identifier(none,'Seq_content'),[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])]),union(none,function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_iq')]),function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_raisedTriggers')])))],[assign(rodinpos(drone_0,'SCXML_raiseInternalTriggers','_4KVgoeYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_iq')],[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])])],[]),event(rodinpos(drone_0,'SCXML_NoUntriggeredTransitions','_4KvJQOYfEemvmYCWQGpCPA'),'SCXML_NoUntriggeredTransitions',anticipated(none),['SCXML_NoUntriggeredTransitions'],[],[equal(rodinpos(drone_0,'SCXML_isNotComplete','_4KWHsOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_false(none)),equal(rodinpos(drone_0,'SCXML_hasNoDequeuedTriggers','_4KWuwOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_dt'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER'))))],[],[assign(rodinpos(drone_0,'SCXML_setComplete','_4KWuweYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_uc')],[boolean_true(none)])],[]),event(rodinpos(drone_0,'ExternalTriggerEvent_toTakeoff','_4KvJQuYfEemvmYCWQGpCPA'),'ExternalTriggerEvent_toTakeoff',anticipated(none),['SCXML_futureRaiseExternalTrigger'],[identifier(rodinpos(drone_0,[],'_4KDz0OYfEemvmYCWQGpCPA'),'SCXML_raisedTrigger')],[member(rodinpos(drone_0,typeof_SCXML_raisedTriggers,'_4KDz0eYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTrigger'),identifier(none,'SCXML_FutureExternalTrigger')),equal(rodinpos(drone_0,raisedExternalTrigger,'_4KvwUeYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTrigger'),identifier(none,toTakeoff))],[],[assign(rodinpos(drone_0,'SCXML_raiseExternalTriggers','_4KEa4OYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_eq')],[function(none,identifier(none,'Seq_append'),[couple(none,[identifier(none,'SCXML_eq'),identifier(none,'SCXML_raisedTrigger')])])])],[]),event(rodinpos(drone_0,'ExternalTriggerEvent_off','_4KvwUuYfEemvmYCWQGpCPA'),'ExternalTriggerEvent_off',anticipated(none),['SCXML_futureRaiseExternalTrigger'],[identifier(rodinpos(drone_0,[],'_4KDz0OYfEemvmYCWQGpCPA'),'SCXML_raisedTrigger')],[member(rodinpos(drone_0,typeof_SCXML_raisedTriggers,'_4KDz0eYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTrigger'),identifier(none,'SCXML_FutureExternalTrigger')),equal(rodinpos(drone_0,raisedExternalTrigger,'_4KwXYeYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTrigger'),identifier(none,off))],[],[assign(rodinpos(drone_0,'SCXML_raiseExternalTriggers','_4KEa4OYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_eq')],[function(none,identifier(none,'Seq_append'),[couple(none,[identifier(none,'SCXML_eq'),identifier(none,'SCXML_raisedTrigger')])])])],[]),event(rodinpos(drone_0,'ExternalTriggerEvent_on','_4Kw-cOYfEemvmYCWQGpCPA'),'ExternalTriggerEvent_on',anticipated(none),['SCXML_futureRaiseExternalTrigger'],[identifier(rodinpos(drone_0,[],'_4KDz0OYfEemvmYCWQGpCPA'),'SCXML_raisedTrigger')],[member(rodinpos(drone_0,typeof_SCXML_raisedTriggers,'_4KDz0eYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTrigger'),identifier(none,'SCXML_FutureExternalTrigger')),equal(rodinpos(drone_0,raisedExternalTrigger,'_4Kw-cuYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTrigger'),identifier(none,on))],[],[assign(rodinpos(drone_0,'SCXML_raiseExternalTriggers','_4KEa4OYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_eq')],[function(none,identifier(none,'Seq_append'),[couple(none,[identifier(none,'SCXML_eq'),identifier(none,'SCXML_raisedTrigger')])])])],[]),event(rodinpos(drone_0,toTakeoff__OPERATIONAL_OPERATIONAL,'_4KxlgOYfEemvmYCWQGpCPA'),toTakeoff__OPERATIONAL_OPERATIONAL,anticipated(none),['SCXML_futureTriggeredTransitionSet'],[identifier(rodinpos(drone_0,[],'_4KOy8OYfEemvmYCWQGpCPA'),'SCXML_trigger'),identifier(rodinpos(drone_0,[],'_4KPaAOYfEemvmYCWQGpCPA'),'SCXML_raisedTriggers')],[member(rodinpos(drone_0,typeof_SCXML_trigger,'_4KPaAeYfEemvmYCWQGpCPA'),identifier(none,'SCXML_trigger'),identifier(none,'SCXML_dt')),equal(rodinpos(drone_0,'SCXML_isNotComplete','_4KQBEOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_false(none)),member(rodinpos(drone_0,typeof_SCXML_raisedTriggers,'_4KQoIOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTriggers'),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_FutureInternalTrigger')])),equal(rodinpos(drone_0,isin_OPERATIONAL,'_4QADwOYfEemvmYCWQGpCPA'),identifier(none,'OPERATIONAL'),boolean_true(none)),equal(rodinpos(drone_0,'SCXML_trigger','_4KyMkOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_trigger'),identifier(none,toTakeoff))],[equal(rodinpos(drone_0,'PO','_4KRPMeYfEemvmYCWQGpCPB'),function(none,identifier(none,'Seq_content'),[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])]),union(none,function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_iq')]),function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_raisedTriggers')])))],[assign(rodinpos(drone_0,'SCXML_clearDequeuedTriggers','_4KRPMOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_dt')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))]),assign(rodinpos(drone_0,'SCXML_raiseInternalTriggers','_4KRPMeYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_iq')],[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])])],[]),event(rodinpos(drone_0,'SHUTDOWN_OFF','_4KyzoOYfEemvmYCWQGpCPA'),'SHUTDOWN_OFF',anticipated(none),['SCXML_futureUntriggeredTransitionSet'],[identifier(rodinpos(drone_0,[],'_4KUSgeYfEemvmYCWQGpCPA'),'SCXML_raisedTriggers')],[equal(rodinpos(drone_0,'SCXML_isNotComplete','_4KU5kOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_false(none)),equal(rodinpos(drone_0,'SCXML_hasNoDequeuedTriggers','_4KU5keYfEemvmYCWQGpCPA'),identifier(none,'SCXML_dt'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))),member(rodinpos(drone_0,typeof_SCXML_raisedTriggers,'_4KVgoOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTriggers'),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_FutureInternalTrigger')])),equal(rodinpos(drone_0,isin_SHUTDOWN,'_4QAq0OYfEemvmYCWQGpCPA'),identifier(none,'SHUTDOWN'),boolean_true(none))],[equal(rodinpos(drone_0,'PO','_4KVgoeYfEemvmYCWQGpCPB'),function(none,identifier(none,'Seq_content'),[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])]),union(none,function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_iq')]),function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_raisedTriggers')])))],[assign(rodinpos(drone_0,'SCXML_raiseInternalTriggers','_4KVgoeYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_iq')],[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])]),assign(rodinpos(drone_0,leave_SHUTDOWN,'_4QBR4OYfEemvmYCWQGpCPA'),[identifier(none,'SHUTDOWN')],[boolean_false(none)]),assign(rodinpos(drone_0,enter_OFF,'_4QBR4eYfEemvmYCWQGpCPA'),[identifier(none,'OFF')],[boolean_true(none)])],[]),event(rodinpos(drone_0,toTakeoff__START_OPERATIONAL,'_4KyzouYfEemvmYCWQGpCPA'),toTakeoff__START_OPERATIONAL,anticipated(none),['SCXML_futureTriggeredTransitionSet'],[identifier(rodinpos(drone_0,[],'_4KOy8OYfEemvmYCWQGpCPA'),'SCXML_trigger'),identifier(rodinpos(drone_0,[],'_4KPaAOYfEemvmYCWQGpCPA'),'SCXML_raisedTriggers')],[member(rodinpos(drone_0,typeof_SCXML_trigger,'_4KPaAeYfEemvmYCWQGpCPA'),identifier(none,'SCXML_trigger'),identifier(none,'SCXML_dt')),equal(rodinpos(drone_0,'SCXML_isNotComplete','_4KQBEOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_false(none)),member(rodinpos(drone_0,typeof_SCXML_raisedTriggers,'_4KQoIOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTriggers'),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_FutureInternalTrigger')])),equal(rodinpos(drone_0,isin_START,'_4QB48OYfEemvmYCWQGpCPA'),identifier(none,'START'),boolean_true(none)),equal(rodinpos(drone_0,'SCXML_trigger','_4K0BwOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_trigger'),identifier(none,toTakeoff))],[equal(rodinpos(drone_0,'PO','_4KRPMeYfEemvmYCWQGpCPB'),function(none,identifier(none,'Seq_content'),[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])]),union(none,function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_iq')]),function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_raisedTriggers')])))],[assign(rodinpos(drone_0,'SCXML_clearDequeuedTriggers','_4KRPMOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_dt')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))]),assign(rodinpos(drone_0,'SCXML_raiseInternalTriggers','_4KRPMeYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_iq')],[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])]),assign(rodinpos(drone_0,leave_START,'_4QB48eYfEemvmYCWQGpCPA'),[identifier(none,'START')],[boolean_false(none)]),assign(rodinpos(drone_0,enter_OPERATIONAL,'_4QCgAOYfEemvmYCWQGpCPA'),[identifier(none,'OPERATIONAL')],[boolean_true(none)])],[]),event(rodinpos(drone_0,off__OPERATIONAL_SHUTDOWN,'_4K0o0OYfEemvmYCWQGpCPA'),off__OPERATIONAL_SHUTDOWN,anticipated(none),['SCXML_futureTriggeredTransitionSet'],[identifier(rodinpos(drone_0,[],'_4KOy8OYfEemvmYCWQGpCPA'),'SCXML_trigger'),identifier(rodinpos(drone_0,[],'_4KPaAOYfEemvmYCWQGpCPA'),'SCXML_raisedTriggers')],[member(rodinpos(drone_0,typeof_SCXML_trigger,'_4KPaAeYfEemvmYCWQGpCPA'),identifier(none,'SCXML_trigger'),identifier(none,'SCXML_dt')),equal(rodinpos(drone_0,'SCXML_isNotComplete','_4KQBEOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_false(none)),member(rodinpos(drone_0,typeof_SCXML_raisedTriggers,'_4KQoIOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTriggers'),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_FutureInternalTrigger')])),equal(rodinpos(drone_0,isin_OPERATIONAL,'_4QDHEOYfEemvmYCWQGpCPA'),identifier(none,'OPERATIONAL'),boolean_true(none)),equal(rodinpos(drone_0,'SCXML_trigger','_4K2eAOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_trigger'),identifier(none,off))],[equal(rodinpos(drone_0,'PO','_4KRPMeYfEemvmYCWQGpCPB'),function(none,identifier(none,'Seq_content'),[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])]),union(none,function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_iq')]),function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_raisedTriggers')])))],[assign(rodinpos(drone_0,'SCXML_clearDequeuedTriggers','_4KRPMOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_dt')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))]),assign(rodinpos(drone_0,'SCXML_raiseInternalTriggers','_4KRPMeYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_iq')],[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])]),assign(rodinpos(drone_0,leave_OPERATIONAL,'_4QDuIOYfEemvmYCWQGpCPA'),[identifier(none,'OPERATIONAL')],[boolean_false(none)]),assign(rodinpos(drone_0,enter_SHUTDOWN,'_4QDuIeYfEemvmYCWQGpCPA'),[identifier(none,'SHUTDOWN')],[boolean_true(none)])],[]),event(rodinpos(drone_0,on__OFF_START,'_4K2eAeYfEemvmYCWQGpCPA'),on__OFF_START,anticipated(none),['SCXML_futureTriggeredTransitionSet'],[identifier(rodinpos(drone_0,[],'_4KOy8OYfEemvmYCWQGpCPA'),'SCXML_trigger'),identifier(rodinpos(drone_0,[],'_4KPaAOYfEemvmYCWQGpCPA'),'SCXML_raisedTriggers')],[member(rodinpos(drone_0,typeof_SCXML_trigger,'_4KPaAeYfEemvmYCWQGpCPA'),identifier(none,'SCXML_trigger'),identifier(none,'SCXML_dt')),equal(rodinpos(drone_0,'SCXML_isNotComplete','_4KQBEOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_false(none)),member(rodinpos(drone_0,typeof_SCXML_raisedTriggers,'_4KQoIOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTriggers'),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_FutureInternalTrigger')])),equal(rodinpos(drone_0,isin_OFF,'_4QEVMOYfEemvmYCWQGpCPA'),identifier(none,'OFF'),boolean_true(none)),equal(rodinpos(drone_0,'SCXML_trigger','_4K3FEeYfEemvmYCWQGpCPA'),identifier(none,'SCXML_trigger'),identifier(none,on))],[equal(rodinpos(drone_0,'PO','_4KRPMeYfEemvmYCWQGpCPB'),function(none,identifier(none,'Seq_content'),[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])]),union(none,function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_iq')]),function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_raisedTriggers')])))],[assign(rodinpos(drone_0,'SCXML_clearDequeuedTriggers','_4KRPMOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_dt')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))]),assign(rodinpos(drone_0,'SCXML_raiseInternalTriggers','_4KRPMeYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_iq')],[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])]),assign(rodinpos(drone_0,leave_OFF,'_4QEVMeYfEemvmYCWQGpCPA'),[identifier(none,'OFF')],[boolean_false(none)]),assign(rodinpos(drone_0,enter_START,'_4QEVMuYfEemvmYCWQGpCPA'),[identifier(none,'START')],[boolean_true(none)])],[])])]),event_b_model(none,basis,[sees(none,[basis_ctx]),variables(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_eq'),identifier(none,'SCXML_dt'),identifier(none,'SCXML_uc')]),invariant(none,[member(rodinpos(basis,typeof_SCXML_iq,'_4J-7UeYfEemvmYCWQGpCPA'),identifier(none,'SCXML_iq'),identifier(none,'InternalQueueType')),member(rodinpos(basis,typeof_SCXML_eq,'_4J_iYOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_eq'),identifier(none,'ExternalQueueType')),member(rodinpos(basis,typeof_SCXML_uc,'_4KAJcOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),bool_set(none)),subset(rodinpos(basis,typeof_SCXML_dt,'_4KAwgOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_dt'),identifier(none,'SCXML_TRIGGER')),implication(rodinpos(basis,oneDequeuedTrigger,'_4KAwgeYfEemvmYCWQGpCPA'),not_equal(none,identifier(none,'SCXML_dt'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))),exists(none,[identifier(none,t)],conjunct(none,member(none,identifier(none,t),identifier(none,'SCXML_TRIGGER')),equal(none,identifier(none,'SCXML_dt'),set_extension(none,[identifier(none,t)])))))]),theorems(none,[equal(rodinpos(basis,disjointQueues,'_4J_iYeYfEemvmYCWQGpCPA'),intersection(none,function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_iq')]),function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_eq')])),typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER'))))]),events(none,[event(rodinpos(basis,'INITIALISATION','_4KBXkOYfEemvmYCWQGpCPA'),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(basis,init_SCXML_iq,'_4KB-oOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_iq')],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))]),assign(rodinpos(basis,init_SCXML_eq,'_4KB-oeYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_eq')],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))]),assign(rodinpos(basis,'SCXML_setNotComplete','_4KClsOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_uc')],[boolean_false(none)]),assign(rodinpos(basis,init_SCXML_dt,'_4KClseYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_dt')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))])],[]),event(rodinpos(basis,'SCXML_futureRaiseExternalTrigger','_4KDMwOYfEemvmYCWQGpCPA'),'SCXML_futureRaiseExternalTrigger',anticipated(none),[],[identifier(rodinpos(basis,[],'_4KDz0OYfEemvmYCWQGpCPA'),'SCXML_raisedTrigger')],[member(rodinpos(basis,typeof_SCXML_raisedTriggers,'_4KDz0eYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTrigger'),identifier(none,'SCXML_FutureExternalTrigger'))],[],[assign(rodinpos(basis,'SCXML_raiseExternalTriggers','_4KEa4OYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_eq')],[function(none,identifier(none,'Seq_append'),[couple(none,[identifier(none,'SCXML_eq'),identifier(none,'SCXML_raisedTrigger')])])])],[]),event(rodinpos(basis,'SCXML_dequeueInternalTrigger','_4KEa4eYfEemvmYCWQGpCPA'),'SCXML_dequeueInternalTrigger',anticipated(none),[],[],[not_equal(rodinpos(basis,grd1,'_4KHeMOYfEemvmYCWQGpCPB'),identifier(none,'SCXML_iq'),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))),equal(rodinpos(basis,'SCXML_hasNoDequeuedTriggers','_4KFpAeYfEemvmYCWQGpCPA'),identifier(none,'SCXML_dt'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))),equal(rodinpos(basis,'SCXML_isComplete','_4KGQEOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_true(none))],[equal(rodinpos(basis,'PO','_4KHeMOYfEemvmYCWQGpCPC'),function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_iq')]),union(none,set_extension(none,[function(none,identifier(none,'Seq_head'),[identifier(none,'SCXML_iq')])]),function(none,identifier(none,'Seq_content'),[function(none,identifier(none,'Seq_tail'),[identifier(none,'SCXML_iq')])])))],[assign(rodinpos(basis,'SCXML_storeDequeuedTrigger','_4KGQEeYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_dt')],[set_extension(none,[function(none,identifier(none,'Seq_head'),[identifier(none,'SCXML_iq')])])]),assign(rodinpos(basis,'SCXML_consumeDequeuedTrigger','_4KG3IOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_iq')],[function(none,identifier(none,'Seq_tail'),[identifier(none,'SCXML_iq')])]),assign(rodinpos(basis,'SCXML_setNotComplete','_4KHeMOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_uc')],[boolean_false(none)])],[]),event(rodinpos(basis,'SCXML_dequeueExternalTrigger','_4KHeMeYfEemvmYCWQGpCPA'),'SCXML_dequeueExternalTrigger',anticipated(none),[],[],[not_equal(rodinpos(basis,grd1,grd1),identifier(none,'SCXML_eq'),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))),equal(rodinpos(basis,'SCXML_hasNoDequeuedTriggers','_4KLIkOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_dt'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))),equal(rodinpos(basis,'SCXML_isComplete','_4KLvoOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_true(none)),equal(rodinpos(basis,'SCXML_internalQEmpty','_4KMWsOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_iq'),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))))],[],[assign(rodinpos(basis,'SCXML_storeDequeuedTrigger','_4KM9wOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_dt')],[set_extension(none,[function(none,identifier(none,'Seq_head'),[identifier(none,'SCXML_eq')])])]),assign(rodinpos(basis,'SCXML_consumeDequeuedTrigger','_4KNk0OYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_eq')],[function(none,identifier(none,'Seq_tail'),[identifier(none,'SCXML_eq')])]),assign(rodinpos(basis,'SCXML_setNotComplete','_4KOL4OYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_uc')],[boolean_false(none)])],[]),event(rodinpos(basis,'SCXML_futureTriggeredTransitionSet','_4KOL4eYfEemvmYCWQGpCPA'),'SCXML_futureTriggeredTransitionSet',anticipated(none),[],[identifier(rodinpos(basis,[],'_4KOy8OYfEemvmYCWQGpCPA'),'SCXML_trigger'),identifier(rodinpos(basis,[],'_4KPaAOYfEemvmYCWQGpCPA'),'SCXML_raisedTriggers')],[member(rodinpos(basis,typeof_SCXML_trigger,'_4KPaAeYfEemvmYCWQGpCPA'),identifier(none,'SCXML_trigger'),identifier(none,'SCXML_dt')),equal(rodinpos(basis,'SCXML_isNotComplete','_4KQBEOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_false(none)),member(rodinpos(basis,typeof_SCXML_raisedTriggers,'_4KQoIOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTriggers'),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_FutureInternalTrigger')]))],[equal(rodinpos(basis,'PO','_4KRPMeYfEemvmYCWQGpCPB'),function(none,identifier(none,'Seq_content'),[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])]),union(none,function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_iq')]),function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_raisedTriggers')])))],[assign(rodinpos(basis,'SCXML_clearDequeuedTriggers','_4KRPMOYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_dt')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))]),assign(rodinpos(basis,'SCXML_raiseInternalTriggers','_4KRPMeYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_iq')],[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])])],[]),event(rodinpos(basis,'SCXML_noTriggeredTransitionsEnabled','_4KSdUOYfEemvmYCWQGpCPA'),'SCXML_noTriggeredTransitionsEnabled',anticipated(none),[],[],[equal(rodinpos(basis,'SCXML_isNotComplete','_4KTEYOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_false(none)),not_equal(rodinpos(basis,'SCXML_hasDequeuedTriggers','_4KTrcOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_dt'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER'))))],[],[assign(rodinpos(basis,'SCXML_clearDequeuedTriggers','_4KTrceYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_dt')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))])],[]),event(rodinpos(basis,'SCXML_futureUntriggeredTransitionSet','_4KUSgOYfEemvmYCWQGpCPA'),'SCXML_futureUntriggeredTransitionSet',anticipated(none),[],[identifier(rodinpos(basis,[],'_4KUSgeYfEemvmYCWQGpCPA'),'SCXML_raisedTriggers')],[equal(rodinpos(basis,'SCXML_isNotComplete','_4KU5kOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_false(none)),equal(rodinpos(basis,'SCXML_hasNoDequeuedTriggers','_4KU5keYfEemvmYCWQGpCPA'),identifier(none,'SCXML_dt'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER')))),member(rodinpos(basis,typeof_SCXML_raisedTriggers,'_4KVgoOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_raisedTriggers'),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_FutureInternalTrigger')]))],[equal(rodinpos(basis,'PO','_4KVgoeYfEemvmYCWQGpCPB'),function(none,identifier(none,'Seq_content'),[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])]),union(none,function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_iq')]),function(none,identifier(none,'Seq_content'),[identifier(none,'SCXML_raisedTriggers')])))],[assign(rodinpos(basis,'SCXML_raiseInternalTriggers','_4KVgoeYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_iq')],[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,'SCXML_iq'),identifier(none,'SCXML_raisedTriggers')])])])],[]),event(rodinpos(basis,'SCXML_NoUntriggeredTransitions','_4KVgouYfEemvmYCWQGpCPA'),'SCXML_NoUntriggeredTransitions',anticipated(none),[],[],[equal(rodinpos(basis,'SCXML_isNotComplete','_4KWHsOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_uc'),boolean_false(none)),equal(rodinpos(basis,'SCXML_hasNoDequeuedTriggers','_4KWuwOYfEemvmYCWQGpCPA'),identifier(none,'SCXML_dt'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'SCXML_TRIGGER'))))],[],[assign(rodinpos(basis,'SCXML_setComplete','_4KWuweYfEemvmYCWQGpCPA'),[identifier(none,'SCXML_uc')],[boolean_true(none)])],[])])])],[event_b_context(none,basis_ctx,[extends(none,[]),constants(none,[identifier(none,'SCXML_FutureInternalTrigger'),identifier(none,'ExternalQueueType'),identifier(none,'Seq_append'),identifier(none,'Seq_length'),identifier(none,'Seq_head'),identifier(none,'Seq_tail'),identifier(none,'SCXML_FutureExternalTrigger'),identifier(none,'Seq'),identifier(none,'InternalQueueType'),identifier(none,'Seq_content'),identifier(none,'Seq_concat')]),abstract_constants(none,[]),axioms(none,[partition(rodinpos(basis_ctx,axm1,'_4Jz8MeYfEemvmYCWQGpCPA'),identifier(none,'SCXML_TRIGGER'),[identifier(none,'SCXML_FutureInternalTrigger'),identifier(none,'SCXML_FutureExternalTrigger')]),finite(rodinpos(basis_ctx,'finite triggers','_5ZrCoCBBEeuhho5A2-LUQA'),identifier(none,'SCXML_TRIGGER')),equal(rodinpos(basis_ctx,'Seq-def','_WoFtyC5dEeuetqa88bjbPg'),identifier(none,'Seq'),event_b_comprehension_set(none,[identifier(none,'T')],couple(none,[identifier(none,'T'),event_b_comprehension_set(none,[identifier(none,n),identifier(none,s)],identifier(none,s),conjunct(none,member(none,identifier(none,n),integer_set(none)),conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,n),natural_set(none)),member(none,identifier(none,s),total_function(none,interval(none,integer(none,0),minus(none,identifier(none,n),integer(none,1))),identifier(none,'T')))))))]),conjunct(none,member(none,identifier(none,'T'),pow_subset(none,identifier(none,'SCXML_TRIGGER'))),subset(none,identifier(none,'T'),identifier(none,'SCXML_TRIGGER'))))),equal(rodinpos(basis_ctx,'Seq_length-def','_WoHi8S5dEeuetqa88bjbPg'),identifier(none,'Seq_length'),event_b_comprehension_set(none,[identifier(none,s)],couple(none,[identifier(none,s),card(none,identifier(none,s))]),conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')]))))),equal(rodinpos(basis_ctx,'Seq_append-def','_WoHi9C5dEeuetqa88bjbPg'),identifier(none,'Seq_append'),event_b_comprehension_set(none,[identifier(none,s),identifier(none,t)],couple(none,[couple(none,[identifier(none,s),identifier(none,t)]),event_b_comprehension_set(none,[identifier(none,i),identifier(none,v)],couple(none,[identifier(none,i),identifier(none,v)]),conjunct(none,member(none,identifier(none,i),integer_set(none)),conjunct(none,member(none,identifier(none,v),identifier(none,'SCXML_TRIGGER')),conjunct(none,member(none,identifier(none,i),interval(none,integer(none,0),function(none,identifier(none,'Seq_length'),[identifier(none,s)]))),conjunct(none,implication(none,less(none,identifier(none,i),function(none,identifier(none,'Seq_length'),[identifier(none,s)])),equal(none,identifier(none,v),function(none,identifier(none,s),[identifier(none,i)]))),implication(none,equal(none,identifier(none,i),function(none,identifier(none,'Seq_length'),[identifier(none,s)])),equal(none,identifier(none,v),identifier(none,t))))))))]),conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,t),identifier(none,'SCXML_TRIGGER')),conjunct(none,member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')])),member(none,identifier(none,t),identifier(none,'SCXML_TRIGGER'))))))),equal(rodinpos(basis_ctx,'Seq_concat-def','_WoIKAC5dEeuetqa88bjbPg'),identifier(none,'Seq_concat'),event_b_comprehension_set(none,[identifier(none,s1),identifier(none,s2)],couple(none,[couple(none,[identifier(none,s1),identifier(none,s2)]),event_b_comprehension_set(none,[identifier(none,i),identifier(none,v)],couple(none,[identifier(none,i),identifier(none,v)]),conjunct(none,member(none,identifier(none,i),integer_set(none)),conjunct(none,member(none,identifier(none,v),identifier(none,'SCXML_TRIGGER')),conjunct(none,member(none,identifier(none,i),interval(none,integer(none,0),minus(none,add(none,function(none,identifier(none,'Seq_length'),[identifier(none,s1)]),function(none,identifier(none,'Seq_length'),[identifier(none,s2)])),integer(none,1)))),conjunct(none,implication(none,less(none,identifier(none,i),function(none,identifier(none,'Seq_length'),[identifier(none,s1)])),equal(none,identifier(none,v),function(none,identifier(none,s1),[identifier(none,i)]))),implication(none,greater_equal(none,identifier(none,i),function(none,identifier(none,'Seq_length'),[identifier(none,s1)])),equal(none,identifier(none,v),function(none,identifier(none,s2),[minus(none,identifier(none,i),function(none,identifier(none,'Seq_length'),[identifier(none,s1)]))]))))))))]),conjunct(none,member(none,identifier(none,s1),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,s2),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,s1),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')])),member(none,identifier(none,s2),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')]))))))),equal(rodinpos(basis_ctx,'Seq_head-def','_WoIKAi5dEeuetqa88bjbPg'),identifier(none,'Seq_head'),event_b_comprehension_set(none,[identifier(none,s)],couple(none,[identifier(none,s),function(none,identifier(none,s),[integer(none,0)])]),conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')])),not_equal(none,identifier(none,s),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))))))),equal(rodinpos(basis_ctx,'Seq_tail-def','_WoIKBC5dEeuetqa88bjbPg'),identifier(none,'Seq_tail'),event_b_comprehension_set(none,[identifier(none,s)],couple(none,[identifier(none,s),event_b_comprehension_set(none,[identifier(none,i),identifier(none,v)],couple(none,[identifier(none,i),identifier(none,v)]),conjunct(none,member(none,identifier(none,i),integer_set(none)),conjunct(none,member(none,identifier(none,v),identifier(none,'SCXML_TRIGGER')),conjunct(none,member(none,identifier(none,i),interval(none,integer(none,0),minus(none,function(none,identifier(none,'Seq_length'),[identifier(none,s)]),integer(none,2)))),equal(none,identifier(none,v),function(none,identifier(none,s),[add(none,identifier(none,i),integer(none,1))]))))))]),conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')])),not_equal(none,identifier(none,s),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))))))),equal(rodinpos(basis_ctx,'Seq_content-def','_WoIxES5dEeuetqa88bjbPj'),identifier(none,'Seq_content'),event_b_comprehension_set(none,[identifier(none,s)],couple(none,[identifier(none,s),range(none,identifier(none,s))]),conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')]))))),equal(rodinpos(basis_ctx,intQ,'_WoIxEC5dEeuetqa88bjbPg'),identifier(none,'InternalQueueType'),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_FutureInternalTrigger')])),equal(rodinpos(basis_ctx,extQ,'_WoIxES5dEeuetqa88bjbPg'),identifier(none,'ExternalQueueType'),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_FutureExternalTrigger')]))]),theorems(none,[member(rodinpos(basis_ctx,'Seq-type','_WoGU0C5dEeuetqa88bjbPg'),identifier(none,'Seq'),total_function(none,pow_subset(none,identifier(none,'SCXML_TRIGGER')),pow_subset(none,partial_function(none,natural_set(none),identifier(none,'SCXML_TRIGGER'))))),forall(rodinpos(basis_ctx,'Seq-finite','_WoHi8C5dEeuetqa88bjbPg'),[identifier(none,s)],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')]))),finite(none,identifier(none,s)))),member(rodinpos(basis_ctx,'Seq_length-type','_WoHi8i5dEeuetqa88bjbPg'),identifier(none,'Seq_length'),total_function(none,function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')]),natural_set(none))),forall(rodinpos(basis_ctx,'Seq_length-card','_WoHi8y5dEeuetqa88bjbPg'),[identifier(none,n),identifier(none,s)],implication(none,conjunct(none,member(none,identifier(none,n),integer_set(none)),conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,n),natural_set(none)),member(none,identifier(none,s),total_function(none,interval(none,integer(none,0),minus(none,identifier(none,n),integer(none,1))),identifier(none,'SCXML_TRIGGER')))))),equal(none,card(none,identifier(none,s)),identifier(none,n)))),member(rodinpos(basis_ctx,'Seq_append-type','_WoHi9S5dEeuetqa88bjbPg'),identifier(none,'Seq_append'),total_function(none,cartesian_product(none,function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')]),identifier(none,'SCXML_TRIGGER')),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')]))),member(rodinpos(basis_ctx,'Seq_concat-type','_WoIKAS5dEeuetqa88bjbPg'),identifier(none,'Seq_concat'),total_function(none,cartesian_product(none,function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')]),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')])),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')]))),member(rodinpos(basis_ctx,'Seq_head-type','_WoIKAy5dEeuetqa88bjbPg'),identifier(none,'Seq_head'),total_function(none,set_subtraction(none,function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')]),set_extension(none,[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))])),identifier(none,'SCXML_TRIGGER'))),member(rodinpos(basis_ctx,'Seq_tail-type','_WoIKBS5dEeuetqa88bjbPg'),identifier(none,'Seq_tail'),total_function(none,set_subtraction(none,function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')]),set_extension(none,[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))])),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')]))),member(rodinpos(basis_ctx,'Seq_content-type','_WoIxES5dEeuetqa88bjbPk'),identifier(none,'Seq_content'),total_function(none,function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')]),pow_subset(none,identifier(none,'SCXML_TRIGGER')))),forall(rodinpos(basis_ctx,th_headUtail,'_0xNO0C9MEeuA7oboPvUhLA'),[identifier(none,s)],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')])),not_equal(none,identifier(none,s),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))))),equal(none,range(none,identifier(none,s)),union(none,set_extension(none,[function(none,identifier(none,'Seq_head'),[identifier(none,s)])]),range(none,function(none,identifier(none,'Seq_tail'),[identifier(none,s)])))))),forall(rodinpos(basis_ctx,th_concat,'_WoIxES5dEeuetqa88bjbPi'),[identifier(none,s1),identifier(none,s2)],implication(none,conjunct(none,member(none,identifier(none,s1),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,s2),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,s1),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')])),member(none,identifier(none,s2),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')]))))),equal(none,range(none,function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,s1),identifier(none,s2)])])),union(none,range(none,identifier(none,s1)),range(none,identifier(none,s2)))))),subset(rodinpos(basis_ctx,axm2,'_WoIxES5dEeuetqa88bjbPh'),identifier(none,'InternalQueueType'),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')])),forall(rodinpos(basis_ctx,th_headContent,'_WoIxES5dEeuetqa88bjbPm'),[identifier(none,s),identifier(none,'T')],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,'T'),pow_subset(none,identifier(none,'SCXML_TRIGGER'))),conjunct(none,subset(none,identifier(none,'T'),identifier(none,'SCXML_TRIGGER')),conjunct(none,member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'T')])),not_equal(none,identifier(none,s),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))))))),member(none,function(none,identifier(none,'Seq_head'),[identifier(none,s)]),identifier(none,'T')))),forall(rodinpos(basis_ctx,th_lengthTail,'_WoIxES5dEeuetqa88bjbPn'),[identifier(none,s)],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')])),not_equal(none,identifier(none,s),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))))),equal(none,function(none,identifier(none,'Seq_length'),[function(none,identifier(none,'Seq_tail'),[identifier(none,s)])]),minus(none,function(none,identifier(none,'Seq_length'),[identifier(none,s)]),integer(none,1))))),forall(rodinpos(basis_ctx,th_contentAppend,'_WoIxES5dEeuetqa88bjbPo'),[identifier(none,s),identifier(none,e)],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,e),identifier(none,'SCXML_TRIGGER')),conjunct(none,member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'SCXML_TRIGGER')])),member(none,identifier(none,e),identifier(none,'SCXML_TRIGGER'))))),subset(none,function(none,identifier(none,'Seq_content'),[identifier(none,s)]),function(none,identifier(none,'Seq_content'),[function(none,identifier(none,'Seq_append'),[couple(none,[identifier(none,s),identifier(none,e)])])])))),forall(rodinpos(basis_ctx,th_appendType,'_WoIxES5dEeuetqa88bjbPp'),[identifier(none,s),identifier(none,'T'),identifier(none,t)],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,'T'),pow_subset(none,identifier(none,'SCXML_TRIGGER'))),conjunct(none,member(none,identifier(none,t),identifier(none,'SCXML_TRIGGER')),conjunct(none,member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'T')])),member(none,identifier(none,t),identifier(none,'T')))))),member(none,function(none,identifier(none,'Seq_append'),[couple(none,[identifier(none,s),identifier(none,t)])]),function(none,identifier(none,'Seq'),[identifier(none,'T')])))),forall(rodinpos(basis_ctx,th_TailType,'_WoIxES5dEeuetqa88bjbPq'),[identifier(none,s),identifier(none,'T')],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,'T'),pow_subset(none,identifier(none,'SCXML_TRIGGER'))),conjunct(none,member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'T')])),not_equal(none,identifier(none,s),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))))))),member(none,function(none,identifier(none,'Seq_tail'),[identifier(none,s)]),function(none,identifier(none,'Seq'),[identifier(none,'T')])))),forall(rodinpos(basis_ctx,th_concatType,'_WoIxES5dEeuetqa88bjbPr'),[identifier(none,s1),identifier(none,s2),identifier(none,'T')],implication(none,conjunct(none,member(none,identifier(none,s1),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,s2),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,'T'),pow_subset(none,identifier(none,'SCXML_TRIGGER'))),conjunct(none,member(none,identifier(none,s1),function(none,identifier(none,'Seq'),[identifier(none,'T')])),member(none,identifier(none,s2),function(none,identifier(none,'Seq'),[identifier(none,'T')])))))),member(none,function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,s1),identifier(none,s2)])]),function(none,identifier(none,'Seq'),[identifier(none,'T')])))),forall(rodinpos(basis_ctx,thm_contentConcat,'_WoIxES5dEeuetqa88bjbPs'),[identifier(none,s1),identifier(none,s2),identifier(none,'T')],implication(none,conjunct(none,member(none,identifier(none,s1),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,s2),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,'T'),pow_subset(none,identifier(none,'SCXML_TRIGGER'))),conjunct(none,member(none,identifier(none,s1),function(none,identifier(none,'Seq'),[identifier(none,'T')])),member(none,identifier(none,s2),function(none,identifier(none,'Seq'),[identifier(none,'T')])))))),equal(none,function(none,identifier(none,'Seq_content'),[function(none,identifier(none,'Seq_concat'),[couple(none,[identifier(none,s1),identifier(none,s2)])])]),union(none,function(none,identifier(none,'Seq_content'),[identifier(none,s1)]),function(none,identifier(none,'Seq_content'),[identifier(none,s2)]))))),forall(rodinpos(basis_ctx,th_tailValue,'_WoIxES5dEeuetqa88bjbPt'),[identifier(none,s),identifier(none,i)],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,i),integer_set(none)),conjunct(none,exists(none,[identifier(none,'T')],conjunct(none,member(none,identifier(none,'T'),pow_subset(none,identifier(none,'SCXML_TRIGGER'))),member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'T')])))),conjunct(none,not_equal(none,identifier(none,s),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER'))))),member(none,identifier(none,i),domain(none,function(none,identifier(none,'Seq_tail'),[identifier(none,s)]))))))),equal(none,function(none,identifier(none,s),[add(none,identifier(none,i),integer(none,1))]),function(none,function(none,identifier(none,'Seq_tail'),[identifier(none,s)]),[identifier(none,i)])))),forall(rodinpos(basis_ctx,th_appendDomain,'_WoIxES5dEeuetqa88bjbPu'),[identifier(none,s),identifier(none,t)],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,t),identifier(none,'SCXML_TRIGGER')),exists(none,[identifier(none,'T')],conjunct(none,member(none,identifier(none,'T'),pow_subset(none,identifier(none,'SCXML_TRIGGER'))),member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'T')])))))),subset(none,domain(none,identifier(none,s)),domain(none,function(none,identifier(none,'Seq_append'),[couple(none,[identifier(none,s),identifier(none,t)])]))))),forall(rodinpos(basis_ctx,th_appendValue,'_WoIxES5dEeuetqa88bjbPv'),[identifier(none,s),identifier(none,t),identifier(none,i)],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,t),identifier(none,'SCXML_TRIGGER')),conjunct(none,member(none,identifier(none,i),integer_set(none)),conjunct(none,exists(none,[identifier(none,'T')],conjunct(none,member(none,identifier(none,'T'),pow_subset(none,identifier(none,'SCXML_TRIGGER'))),member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'T')])))),member(none,identifier(none,i),domain(none,identifier(none,s))))))),equal(none,function(none,identifier(none,s),[identifier(none,i)]),function(none,function(none,identifier(none,'Seq_append'),[couple(none,[identifier(none,s),identifier(none,t)])]),[identifier(none,i)])))),forall(rodinpos(basis_ctx,th_appendNewValue,'_WoIxES5dEeuetqa88bjbPw'),[identifier(none,s),identifier(none,t)],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'SCXML_TRIGGER')))),conjunct(none,member(none,identifier(none,t),identifier(none,'SCXML_TRIGGER')),exists(none,[identifier(none,'T')],conjunct(none,member(none,identifier(none,'T'),pow_subset(none,identifier(none,'SCXML_TRIGGER'))),member(none,identifier(none,s),function(none,identifier(none,'Seq'),[identifier(none,'T')])))))),equal(none,function(none,function(none,identifier(none,'Seq_append'),[couple(none,[identifier(none,s),identifier(none,t)])]),[function(none,identifier(none,'Seq_length'),[identifier(none,s)])]),identifier(none,t))))]),sets(none,[deferred_set(none,'SCXML_TRIGGER')])]),event_b_context(none,drone_0_ctx,[extends(none,[basis_ctx]),constants(none,[identifier(none,toTakeoff),identifier(none,'SCXML_FutureExternalTrigger0'),identifier(none,off),identifier(none,'SCXML_FutureInternalTrigger0'),identifier(none,on)]),abstract_constants(none,[]),axioms(none,[partition(rodinpos(drone_0_ctx,typeof_SCXML_FutureExternalTrigger0,'_4K9LseYfEemvmYCWQGpCPA'),identifier(none,'SCXML_FutureExternalTrigger'),[identifier(none,'SCXML_FutureExternalTrigger0'),set_extension(none,[identifier(none,toTakeoff)]),set_extension(none,[identifier(none,off)]),set_extension(none,[identifier(none,on)])]),equal(rodinpos(drone_0_ctx,typeof_SCXML_FutureInternalTrigger0,'_4K9LsuYfEemvmYCWQGpCPA'),identifier(none,'SCXML_FutureInternalTrigger0'),identifier(none,'SCXML_FutureInternalTrigger'))]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po(basis_ctx,'Theorem',[axiom('Seq-type')],true),po(basis_ctx,'Well-definedness of Theorem',[axiom('Seq-finite')],true),po(basis_ctx,'Theorem',[axiom('Seq-finite')],true),po(basis_ctx,'Well-definedness of Axiom',[axiom('Seq_length-def')],true),po(basis_ctx,'Well-definedness of Theorem',[axiom('Seq_length-type')],true),po(basis_ctx,'Theorem',[axiom('Seq_length-type')],true),po(basis_ctx,'Well-definedness of Theorem',[axiom('Seq_length-card')],true),po(basis_ctx,'Theorem',[axiom('Seq_length-card')],true),po(basis_ctx,'Well-definedness of Axiom',[axiom('Seq_append-def')],true),po(basis_ctx,'Well-definedness of Theorem',[axiom('Seq_append-type')],true),po(basis_ctx,'Theorem',[axiom('Seq_append-type')],true),po(basis_ctx,'Well-definedness of Axiom',[axiom('Seq_concat-def')],true),po(basis_ctx,'Well-definedness of Theorem',[axiom('Seq_concat-type')],true),po(basis_ctx,'Theorem',[axiom('Seq_concat-type')],true),po(basis_ctx,'Well-definedness of Axiom',[axiom('Seq_head-def')],true),po(basis_ctx,'Well-definedness of Theorem',[axiom('Seq_head-type')],true),po(basis_ctx,'Theorem',[axiom('Seq_head-type')],true),po(basis_ctx,'Well-definedness of Axiom',[axiom('Seq_tail-def')],true),po(basis_ctx,'Well-definedness of Theorem',[axiom('Seq_tail-type')],true),po(basis_ctx,'Theorem',[axiom('Seq_tail-type')],true),po(basis_ctx,'Well-definedness of Axiom',[axiom('Seq_content-def')],true),po(basis_ctx,'Well-definedness of Theorem',[axiom('Seq_content-type')],true),po(basis_ctx,'Theorem',[axiom('Seq_content-type')],true),po(basis_ctx,'Well-definedness of Theorem',[axiom(th_headUtail)],true),po(basis_ctx,'Theorem',[axiom(th_headUtail)],true),po(basis_ctx,'Well-definedness of Theorem',[axiom(th_concat)],true),po(basis_ctx,'Theorem',[axiom(th_concat)],true),po(basis_ctx,'Well-definedness of Axiom',[axiom(intQ)],true),po(basis_ctx,'Well-definedness of Axiom',[axiom(extQ)],true),po(basis_ctx,'Well-definedness of Theorem',[axiom(axm2)],true),po(basis_ctx,'Theorem',[axiom(axm2)],true),po(basis_ctx,'Well-definedness of Theorem',[axiom(th_headContent)],true),po(basis_ctx,'Theorem',[axiom(th_headContent)],true),po(basis_ctx,'Well-definedness of Theorem',[axiom(th_lengthTail)],true),po(basis_ctx,'Theorem',[axiom(th_lengthTail)],true),po(basis_ctx,'Well-definedness of Theorem',[axiom(th_contentAppend)],true),po(basis_ctx,'Theorem',[axiom(th_contentAppend)],true),po(basis_ctx,'Well-definedness of Theorem',[axiom(th_appendType)],true),po(basis_ctx,'Theorem',[axiom(th_appendType)],true),po(basis_ctx,'Well-definedness of Theorem',[axiom(th_TailType)],true),po(basis_ctx,'Theorem',[axiom(th_TailType)],true),po(basis_ctx,'Well-definedness of Theorem',[axiom(th_concatType)],true),po(basis_ctx,'Theorem',[axiom(th_concatType)],true),po(basis_ctx,'Well-definedness of Theorem',[axiom(thm_contentConcat)],true),po(basis_ctx,'Theorem',[axiom(thm_contentConcat)],true),po(basis_ctx,'Well-definedness of Theorem',[axiom(th_tailValue)],true),po(basis_ctx,'Theorem',[axiom(th_tailValue)],true),po(basis_ctx,'Well-definedness of Theorem',[axiom(th_appendDomain)],true),po(basis_ctx,'Theorem',[axiom(th_appendDomain)],true),po(basis_ctx,'Well-definedness of Theorem',[axiom(th_appendValue)],true),po(basis_ctx,'Theorem',[axiom(th_appendValue)],true),po(basis_ctx,'Well-definedness of Theorem',[axiom(th_appendNewValue)],true),po(basis_ctx,'Theorem',[axiom(th_appendNewValue)],true),po(drone_0,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(distinct_states_in_drone_sm)],true),po(drone_0,'Invariant preservation',[event('SCXML_futureUntriggeredTransitionSet'),event('SHUTDOWN_OFF'),invariant(distinct_states_in_drone_sm)],true),po(drone_0,'Invariant preservation',[event('SCXML_futureTriggeredTransitionSet'),event(toTakeoff__START_OPERATIONAL),invariant(distinct_states_in_drone_sm)],true),po(drone_0,'Invariant preservation',[event('SCXML_futureTriggeredTransitionSet'),event(off__OPERATIONAL_SHUTDOWN),invariant(distinct_states_in_drone_sm)],true),po(drone_0,'Invariant preservation',[event('SCXML_futureTriggeredTransitionSet'),event(on__OFF_START),invariant(distinct_states_in_drone_sm)],true),po(basis,'Well-definedness of Theorem',[invariant(disjointQueues)],true),po(basis,'Theorem',[invariant(disjointQueues)],true),po(basis,'Invariant establishment',[event('INITIALISATION'),invariant(typeof_SCXML_iq)],true),po(basis,'Invariant establishment',[event('INITIALISATION'),invariant(typeof_SCXML_eq)],true),po(basis,'Invariant establishment',[event('INITIALISATION'),invariant(oneDequeuedTrigger)],true),po(basis,'Invariant preservation',[event('SCXML_futureRaiseExternalTrigger'),invariant(typeof_SCXML_eq)],true),po(basis,'Well-definedness of action',[action('SCXML_raiseExternalTriggers')],true),po(basis,'Well-definedness of Theorem',[guard('PO'),event('SCXML_dequeueInternalTrigger')],true),po(basis,'Theorem',[guard('PO'),event('SCXML_dequeueInternalTrigger')],true),po(basis,'Invariant preservation',[event('SCXML_dequeueInternalTrigger'),invariant(typeof_SCXML_iq)],true),po(basis,'Invariant preservation',[event('SCXML_dequeueInternalTrigger'),invariant(oneDequeuedTrigger)],true),po(basis,'Well-definedness of action',[action('SCXML_storeDequeuedTrigger')],true),po(basis,'Well-definedness of action',[action('SCXML_consumeDequeuedTrigger')],true),po(basis,'Invariant preservation',[event('SCXML_dequeueExternalTrigger'),invariant(typeof_SCXML_eq)],true),po(basis,'Invariant preservation',[event('SCXML_dequeueExternalTrigger'),invariant(oneDequeuedTrigger)],true),po(basis,'Well-definedness of action',[action('SCXML_storeDequeuedTrigger')],true),po(basis,'Well-definedness of action',[action('SCXML_consumeDequeuedTrigger')],true),po(basis,'Well-definedness of Guard',[guard(typeof_SCXML_raisedTriggers),event('SCXML_futureTriggeredTransitionSet')],true),po(basis,'Well-definedness of Theorem',[guard('PO'),event('SCXML_futureTriggeredTransitionSet')],true),po(basis,'Theorem',[guard('PO'),event('SCXML_futureTriggeredTransitionSet')],true),po(basis,'Invariant preservation',[event('SCXML_futureTriggeredTransitionSet'),invariant(typeof_SCXML_iq)],true),po(basis,'Invariant preservation',[event('SCXML_futureTriggeredTransitionSet'),invariant(oneDequeuedTrigger)],true),po(basis,'Well-definedness of action',[action('SCXML_raiseInternalTriggers')],true),po(basis,'Invariant preservation',[event('SCXML_noTriggeredTransitionsEnabled'),invariant(oneDequeuedTrigger)],true),po(basis,'Well-definedness of Guard',[guard(typeof_SCXML_raisedTriggers),event('SCXML_futureUntriggeredTransitionSet')],true),po(basis,'Well-definedness of Theorem',[guard('PO'),event('SCXML_futureUntriggeredTransitionSet')],true),po(basis,'Theorem',[guard('PO'),event('SCXML_futureUntriggeredTransitionSet')],true),po(basis,'Invariant preservation',[event('SCXML_futureUntriggeredTransitionSet'),invariant(typeof_SCXML_iq)],true),po(basis,'Well-definedness of action',[action('SCXML_raiseInternalTriggers')],true)],_Error)).
2