1		generated(1426692580234,'Wed Mar 18 16:29:40 CET 2015').
2		project_name('Pacemaker_1_Modify_Hyt_15March2011').
3		machine_name('M0_AOO').
4		disprover_po('INITIALISATION/inv6/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'last_sp\''),integer_set(none)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none)),member(none,identifier(none,'Pace_Int\''),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,'OFF'),identifier(none,'last_sp\''),identifier(none,'ON'),identifier(none,'Pace_Int_flag\''),identifier(none,'Pace_Int\''),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))],[member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))],true).
5		disprover_po('INITIALISATION/inv2/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'last_sp\''),integer_set(none)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none)),member(none,identifier(none,'Pace_Int\''),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,'OFF'),identifier(none,'last_sp\''),identifier(none,'ON'),identifier(none,'Pace_Int_flag\''),identifier(none,'Pace_Int\''),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),member(none,integer(none,1),natural_set(none)),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))],[],true).
6		disprover_po('INITIALISATION/inv3/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'last_sp\''),integer_set(none)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none)),member(none,identifier(none,'Pace_Int\''),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,'OFF'),identifier(none,'last_sp\''),identifier(none,'ON'),identifier(none,'Pace_Int_flag\''),identifier(none,'Pace_Int\''),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),less_equal(none,integer(none,1),identifier(none,'LRL_Time_Int')),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))],[],true).
7		disprover_po('INITIALISATION/inv4/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'last_sp\''),integer_set(none)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none)),member(none,identifier(none,'Pace_Int\''),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'last_sp\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,'OFF'),identifier(none,'last_sp\''),identifier(none,'ON'),identifier(none,'Pace_Int_flag\''),identifier(none,'Pace_Int\''),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),member(none,identifier(none,'last_sp\''),natural_set(none)),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'last_sp\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))],[member(none,identifier(none,'last_sp\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))],true).
8		disprover_po('INITIALISATION/inv7/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'last_sp\''),integer_set(none)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none)),member(none,identifier(none,'Pace_Int\''),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'last_sp\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,'OFF'),identifier(none,'last_sp\''),identifier(none,'ON'),identifier(none,'Pace_Int_flag\''),identifier(none,'Pace_Int\''),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),conjunct(none,greater_equal(none,identifier(none,'last_sp\''),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,'last_sp\''),identifier(none,'LRL_Time_Int'))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'last_sp\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))],[member(none,identifier(none,'last_sp\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))],true).
9		disprover_po('INITIALISATION/inv8/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'last_sp\''),integer_set(none)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none)),member(none,identifier(none,'Pace_Int\''),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,'OFF'),identifier(none,'last_sp\''),identifier(none,'ON'),identifier(none,'Pace_Int_flag\''),identifier(none,'Pace_Int\''),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag\''),boolean_false(none)),less(none,integer(none,1),identifier(none,'Pace_Int\''))),equal(none,identifier(none,'OFF'),identifier(none,'OFF'))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none))],[member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none))],true).
10		disprover_po('INITIALISATION/thm1/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'last_sp\''),integer_set(none)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none)),member(none,identifier(none,'Pace_Int\''),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,'OFF'),identifier(none,'last_sp\''),identifier(none,'ON'),identifier(none,'Pace_Int_flag\''),identifier(none,'Pace_Int\''),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag\''),boolean_false(none)),equal(none,identifier(none,'OFF'),identifier(none,'ON'))),equal(none,integer(none,1),identifier(none,'Pace_Int\''))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none))],[member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none))],true).
11		disprover_po('INITIALISATION/act3/FIS',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'last_sp\''),integer_set(none)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none)),member(none,identifier(none,'Pace_Int\''),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,'OFF'),identifier(none,'last_sp\''),identifier(none,'ON'),identifier(none,'Pace_Int_flag\''),identifier(none,'Pace_Int\''),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),not_equal(none,interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))],[],true).
12		disprover_po('INITIALISATION/act4/FIS',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'last_sp\''),integer_set(none)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none)),member(none,identifier(none,'Pace_Int\''),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,'OFF'),identifier(none,'last_sp\''),identifier(none,'ON'),identifier(none,'Pace_Int_flag\''),identifier(none,'Pace_Int\''),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),not_equal(none,interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))],[],true).
13		disprover_po('INITIALISATION/act5/FIS',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'last_sp\''),integer_set(none)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,'Pace_Int_flag\''),bool_set(none)),member(none,identifier(none,'Pace_Int\''),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,'OFF'),identifier(none,'last_sp\''),identifier(none,'ON'),identifier(none,'Pace_Int_flag\''),identifier(none,'Pace_Int\''),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),not_equal(none,bool_set(none),typeof(none,empty_set(none),pow_subset(none,bool_set(none)))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))],[],true).
14		disprover_po('Pace_ON/inv4/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'last_sp\''),integer_set(none)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF')),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'last_sp\''),identifier(none,'ON'),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),member(none,identifier(none,sp),natural_set(none)),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF')),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))],[member(none,identifier(none,last_sp),natural_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF')),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))],true).
15		disprover_po('Pace_ON/inv7/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'last_sp\''),integer_set(none)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF')),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'last_sp\''),identifier(none,'ON'),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),conjunct(none,greater_equal(none,identifier(none,sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int'))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF')),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))],[conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF')),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))],true).
16		disprover_po('Pace_ON/inv8/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'last_sp\''),integer_set(none)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF')),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'last_sp\''),identifier(none,'ON'),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'ON'),identifier(none,'OFF'))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF')),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))],[implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF')),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))],true).
17		disprover_po('Pace_ON/thm1/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'last_sp\''),integer_set(none)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF')),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'last_sp\''),identifier(none,'ON'),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'ON'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF')),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))],[implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF')),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))],true).
18		disprover_po('Pace_OFF/inv2/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'ON'),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),member(none,integer(none,1),natural_set(none)),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))],[member(none,identifier(none,sp),natural_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))],true).
19		disprover_po('Pace_OFF/inv3/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'ON'),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),less_equal(none,integer(none,1),identifier(none,'LRL_Time_Int')),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))],[less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))],true).
20		disprover_po('Pace_OFF/inv8/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'ON'),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,integer(none,1),identifier(none,'Pace_Int'))),equal(none,identifier(none,'OFF'),identifier(none,'OFF'))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))],[implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))],true).
21		disprover_po('Pace_OFF/thm1/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'Pacemaker_Actuator\''),identifier(none,status)),member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))]),constants(none,[identifier(none,'Pacemaker_Actuator\''),identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'ON'),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'OFF'),identifier(none,'ON'))),equal(none,integer(none,1),identifier(none,'Pace_Int'))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))],[implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))],true).
22		disprover_po('tic/inv2/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))]),constants(none,[identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'ON'),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),member(none,add(none,identifier(none,sp),integer(none,1)),natural_set(none)),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))],[member(none,identifier(none,sp),natural_set(none)),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))],true).
23		disprover_po('tic/inv3/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))]),constants(none,[identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'ON'),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),less_equal(none,add(none,identifier(none,sp),integer(none,1)),identifier(none,'LRL_Time_Int')),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))],[less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))],true).
24		disprover_po('tic/inv8/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))]),constants(none,[identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'ON'),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,add(none,identifier(none,sp),integer(none,1)),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))],[implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))],true).
25		disprover_po('tic/thm1/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))]),constants(none,[identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'ON'),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,add(none,identifier(none,sp),integer(none,1)),identifier(none,'Pace_Int'))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))],[implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))],true).
26		disprover_po('tic/VAR',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))]),constants(none,[identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'ON'),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),less(none,minus(none,identifier(none,'Pace_Int'),add(none,identifier(none,sp),integer(none,1))),minus(none,identifier(none,'Pace_Int'),identifier(none,sp))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))],[conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))],true).
27		disprover_po('tic/NAT',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'sp\''),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))]),constants(none,[identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'ON'),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'sp\''),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),member(none,minus(none,identifier(none,'Pace_Int'),identifier(none,sp)),natural_set(none)),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))],[conjunct(none,greater(none,identifier(none,sp),integer(none,0)),less(none,identifier(none,sp),identifier(none,'Pace_Int')))],true).
28		disprover_po('Change_Pace_Int/inv6/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,'Pace_Int\''),integer_set(none)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pace_Int_flag'),boolean_true(none)),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))]),constants(none,[identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'ON'),identifier(none,'Pace_Int\''),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pace_Int_flag'),boolean_true(none)),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))],[member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),equal(none,identifier(none,'Pace_Int_flag'),boolean_true(none)),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))],true).
29		disprover_po('Change_Pace_Int/inv8/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,'Pace_Int\''),integer_set(none)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pace_Int_flag'),boolean_true(none)),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))]),constants(none,[identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'ON'),identifier(none,'Pace_Int\''),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int\''))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pace_Int_flag'),boolean_true(none)),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))],[implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),equal(none,identifier(none,'Pace_Int_flag'),boolean_true(none)),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))],true).
30		disprover_po('Change_Pace_Int/thm1/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,'Pace_Int\''),integer_set(none)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pace_Int_flag'),boolean_true(none)),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))]),constants(none,[identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'ON'),identifier(none,'Pace_Int\''),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int\''))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pace_Int_flag'),boolean_true(none)),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))],[implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pace_Int_flag'),boolean_true(none)),member(none,identifier(none,'Pace_Int\''),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')))],true).
31		disprover_po('Change_Pace_Int/act1/FIS',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'LRL'),integer_set(none)),member(none,identifier(none,sp),integer_set(none)),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'OFF'),identifier(none,status)),member(none,identifier(none,'ON'),identifier(none,status)),member(none,identifier(none,'Pace_Int\''),integer_set(none)),member(none,identifier(none,last_sp),integer_set(none)),member(none,identifier(none,'Pace_Int'),integer_set(none)),member(none,identifier(none,'URL_Time_Int'),integer_set(none)),member(none,identifier(none,'URL'),integer_set(none)),member(none,identifier(none,'LRL_Time_Int'),integer_set(none)),equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pace_Int_flag'),boolean_true(none))]),constants(none,[identifier(none,'LRL'),identifier(none,sp),identifier(none,'Pace_Int_flag'),identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'),identifier(none,'ON'),identifier(none,'Pace_Int\''),identifier(none,last_sp),identifier(none,'Pace_Int'),identifier(none,'URL_Time_Int'),identifier(none,'URL'),identifier(none,'LRL_Time_Int')]),sets(none,[deferred_set(none,status)])]),not_equal(none,interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),[equal(none,identifier(none,status),set_extension(none,[identifier(none,'ON'),identifier(none,'OFF')])),not_equal(none,identifier(none,'ON'),identifier(none,'OFF')),member(none,identifier(none,'LRL'),interval(none,integer(none,30),integer(none,175))),member(none,identifier(none,'URL'),interval(none,integer(none,50),integer(none,175))),conjunct(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'URL_Time_Int'),div(none,integer(none,60000),identifier(none,'URL')))),implication(none,member(none,identifier(none,'URL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'URL'),integer(none,0))),conjunct(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),equal(none,identifier(none,'LRL_Time_Int'),div(none,integer(none,60000),identifier(none,'LRL')))),implication(none,member(none,identifier(none,'LRL_Time_Int'),natural1_set(none)),not_equal(none,identifier(none,'LRL'),integer(none,0))),less(none,identifier(none,'LRL'),identifier(none,'URL')),less(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int')),member(none,identifier(none,'Pacemaker_Actuator'),identifier(none,status)),member(none,identifier(none,'Pace_Int'),interval(none,identifier(none,'URL_Time_Int'),identifier(none,'LRL_Time_Int'))),member(none,identifier(none,sp),natural_set(none)),less_equal(none,identifier(none,sp),identifier(none,'LRL_Time_Int')),member(none,identifier(none,last_sp),natural_set(none)),conjunct(none,greater_equal(none,identifier(none,last_sp),identifier(none,'URL_Time_Int')),less_equal(none,identifier(none,last_sp),identifier(none,'LRL_Time_Int'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),less(none,identifier(none,sp),identifier(none,'Pace_Int'))),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'OFF'))),implication(none,conjunct(none,equal(none,identifier(none,'Pace_Int_flag'),boolean_false(none)),equal(none,identifier(none,'Pacemaker_Actuator'),identifier(none,'ON'))),equal(none,identifier(none,sp),identifier(none,'Pace_Int'))),member(none,identifier(none,'Pace_Int_flag'),bool_set(none)),equal(none,identifier(none,'Pace_Int_flag'),boolean_true(none))],[equal(none,identifier(none,'Pace_Int_flag'),boolean_true(none))],true).
32