{
  "transitionList": [
    {
      "name": "start_xtl_system",
      "destState": {
        "xtl_state": "state(sequent([],conjunct(member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),member($(rover),domain($(radiation)))),success(1)),[rawsets([deferred_set(none,orientations),deferred_set(none,fieldTypes)]),des_hyps([conjunct(less_equal(10,$('B')),member($('B'),'NATURAL1')),conjunct(less_equal(10,$('L')),member($('L'),'NATURAL1')),equal($(field),cartesian_product(interval(1,$('B')),interval(1,$('L')))),member($(baseStation),$(field)),partition($(orientations),[set_extension([$('N')]),set_extension([$('O')]),set_extension([$('S')]),set_extension([$('W')])]),member($(initialOrientation),$(orientations)),member($('Offset'),total_function($(orientations),cartesian_product(interval(unary_minus(1),1),interval(unary_minus(1),1)))),equal($('Offset'),set_extension([couple($('N'),couple(0,1)),couple($('O'),couple(1,0)),couple($('S'),couple(0,unary_minus(1))),couple($('W'),couple(unary_minus(1),0))])),equal($(frontPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(add(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),equal($(rearPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(minus(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))),minus(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),member($(newOrientation),total_function($(orientations),$(orientations))),equal($(newOrientation),set_extension([couple($('W'),$('N')),couple($('N'),$('O')),couple($('O'),$('S')),couple($('S'),$('W'))])),subset($(obstacles),$(field)),not_member($(baseStation),$(obstacles)),conjunct(less_equal($(betaMax),multiplication($('B'),2)),member($(betaMax),'NATURAL1')),conjunct(less(0,$(epsilonK)),less_equal($(epsilonK),div($('B'),5))),implication(less_equal(1,$(epsilonK)),not_equal(5,0)),member($(visibilityRange),total_function(cartesian_product($(field),$(orientations)),pow_subset(cartesian_product('INTEGER','INTEGER')))),equal($(visibilityRange),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),union(event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(add($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(1,0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),minus($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,unary_minus(1))),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),add($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,1)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field)))),event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(minus($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(unary_minus(1),0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field)))))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(conjunct(conjunct(forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))))),member($(radiation),total_function($(field),'NATURAL')),member($(alphaMax),'NATURAL1'),conjunct(less($(alphaInt),$(alphaMax)),member($(alphaInt),'NATURAL')),less_equal(function($(radiation),$(baseStation)),$(alphaMax)),member($(baseStation),domain($(radiation))),member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),conjunct(less(0,$(epsilonS)),less_equal($(epsilonS),div($('B'),5))),implication(less_equal(1,$(epsilonS)),not_equal(5,0)),member($(sensorRange),total_function($(field),pow_subset($(field)))),equal($(sensorRange),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(conjunct(less(unary_minus(add($(epsilonS),1)),minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')))),less(unary_minus(add($(epsilonS),1)),minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),less(minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),less(minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),member(couple($(x),$(y)),$(field))))),member($('Pos'),$(field)))),member($(findInterestingFields),total_function($(field),pow_subset($(field)))),equal($(findInterestingFields),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(less($(alphaInt),function($(radiation),couple($(x),$(y)))),less(function($(radiation),couple($(x),$(y))),$(alphaMax))),member(couple($(x),$(y)),$(field))),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))))),member($('Pos'),$(field)))),forall([$('Pos')],member($('Pos'),$(field)),forall([$(x),$(y)],truth,conjunct(conjunct(implication(conjunct(member(couple($(x),$(y)),$(field)),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))),conjunct(member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),member(couple($(x),$(y)),domain($(radiation))))),member($('Pos'),domain($(sensorRange)))),member($(sensorRange),partial_function(cartesian_product('INTEGER','INTEGER'),pow_subset(cartesian_product('INTEGER','INTEGER'))))))),subset(set_extension([$(rover)]),$(field)),member($(orientation),$(orientations)),conjunct(less_equal($(battery),$(betaMax)),member($(battery),'NATURAL')),conjunct(less($(betaMin),$(betaMax)),member($(betaMin),'NATURAL')),less_equal(1,$(battery)),subset($(freeFields),$(field)),subset($(occupiedFields),$(field)),member($(baseStation),$(freeFields)),equal(intersection($(obstacles),$(freeFields)),empty_set),subset($(occupiedFields),$(obstacles)),member($(rover),$(freeFields))])])."
      }
    },
    {
      "name": "reselect_hyp",
      "params": {
        "para1": "member($(radiation),total_function($(field),'NATURAL'))"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(radiation),total_function($(field),'NATURAL'))],conjunct(member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),member($(rover),domain($(radiation)))),success(1)),[ids_types([b(identifier(orientations),set(global(orientations)),[])]),rawsets([deferred_set(none,orientations),deferred_set(none,fieldTypes)]),des_hyps([conjunct(less_equal(10,$('B')),member($('B'),'NATURAL1')),conjunct(less_equal(10,$('L')),member($('L'),'NATURAL1')),equal($(field),cartesian_product(interval(1,$('B')),interval(1,$('L')))),member($(baseStation),$(field)),partition($(orientations),[set_extension([$('N')]),set_extension([$('O')]),set_extension([$('S')]),set_extension([$('W')])]),member($(initialOrientation),$(orientations)),member($('Offset'),total_function($(orientations),cartesian_product(interval(unary_minus(1),1),interval(unary_minus(1),1)))),equal($('Offset'),set_extension([couple($('N'),couple(0,1)),couple($('O'),couple(1,0)),couple($('S'),couple(0,unary_minus(1))),couple($('W'),couple(unary_minus(1),0))])),equal($(frontPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(add(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),equal($(rearPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(minus(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))),minus(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),member($(newOrientation),total_function($(orientations),$(orientations))),equal($(newOrientation),set_extension([couple($('W'),$('N')),couple($('N'),$('O')),couple($('O'),$('S')),couple($('S'),$('W'))])),subset($(obstacles),$(field)),not_member($(baseStation),$(obstacles)),conjunct(less_equal($(betaMax),multiplication($('B'),2)),member($(betaMax),'NATURAL1')),conjunct(less(0,$(epsilonK)),less_equal($(epsilonK),div($('B'),5))),implication(less_equal(1,$(epsilonK)),not_equal(5,0)),member($(visibilityRange),total_function(cartesian_product($(field),$(orientations)),pow_subset(cartesian_product('INTEGER','INTEGER')))),equal($(visibilityRange),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),union(event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(add($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(1,0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),minus($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,unary_minus(1))),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),add($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,1)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field)))),event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(minus($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(unary_minus(1),0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field)))))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(conjunct(conjunct(forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))))),member($(alphaMax),'NATURAL1'),conjunct(less($(alphaInt),$(alphaMax)),member($(alphaInt),'NATURAL')),less_equal(function($(radiation),$(baseStation)),$(alphaMax)),member($(baseStation),domain($(radiation))),member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),conjunct(less(0,$(epsilonS)),less_equal($(epsilonS),div($('B'),5))),implication(less_equal(1,$(epsilonS)),not_equal(5,0)),member($(sensorRange),total_function($(field),pow_subset($(field)))),equal($(sensorRange),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(conjunct(less(unary_minus(add($(epsilonS),1)),minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')))),less(unary_minus(add($(epsilonS),1)),minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),less(minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),less(minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),member(couple($(x),$(y)),$(field))))),member($('Pos'),$(field)))),member($(findInterestingFields),total_function($(field),pow_subset($(field)))),equal($(findInterestingFields),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(less($(alphaInt),function($(radiation),couple($(x),$(y)))),less(function($(radiation),couple($(x),$(y))),$(alphaMax))),member(couple($(x),$(y)),$(field))),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))))),member($('Pos'),$(field)))),forall([$('Pos')],member($('Pos'),$(field)),forall([$(x),$(y)],truth,conjunct(conjunct(implication(conjunct(member(couple($(x),$(y)),$(field)),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))),conjunct(member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),member(couple($(x),$(y)),domain($(radiation))))),member($('Pos'),domain($(sensorRange)))),member($(sensorRange),partial_function(cartesian_product('INTEGER','INTEGER'),pow_subset(cartesian_product('INTEGER','INTEGER'))))))),subset(set_extension([$(rover)]),$(field)),member($(orientation),$(orientations)),conjunct(less_equal($(battery),$(betaMax)),member($(battery),'NATURAL')),conjunct(less($(betaMin),$(betaMax)),member($(betaMin),'NATURAL')),less_equal(1,$(battery)),subset($(freeFields),$(field)),subset($(occupiedFields),$(field)),member($(baseStation),$(freeFields)),equal(intersection($(obstacles),$(freeFields)),empty_set),subset($(occupiedFields),$(obstacles)),member($(rover),$(freeFields))])])."
      }
    },
    {
      "name": "reselect_hyp",
      "params": {
        "para1": "subset(set_extension([$(rover)]),$(field))"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(radiation),total_function($(field),'NATURAL')),subset(set_extension([$(rover)]),$(field))],conjunct(member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),member($(rover),domain($(radiation)))),success(1)),[ids_types([b(identifier(field),any,[]),b(identifier(orientations),set(global(orientations)),[]),b(identifier(radiation),any,[])]),rawsets([deferred_set(none,orientations),deferred_set(none,fieldTypes)]),des_hyps([conjunct(less_equal(10,$('B')),member($('B'),'NATURAL1')),conjunct(less_equal(10,$('L')),member($('L'),'NATURAL1')),equal($(field),cartesian_product(interval(1,$('B')),interval(1,$('L')))),member($(baseStation),$(field)),partition($(orientations),[set_extension([$('N')]),set_extension([$('O')]),set_extension([$('S')]),set_extension([$('W')])]),member($(initialOrientation),$(orientations)),member($('Offset'),total_function($(orientations),cartesian_product(interval(unary_minus(1),1),interval(unary_minus(1),1)))),equal($('Offset'),set_extension([couple($('N'),couple(0,1)),couple($('O'),couple(1,0)),couple($('S'),couple(0,unary_minus(1))),couple($('W'),couple(unary_minus(1),0))])),equal($(frontPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(add(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),equal($(rearPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(minus(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))),minus(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),member($(newOrientation),total_function($(orientations),$(orientations))),equal($(newOrientation),set_extension([couple($('W'),$('N')),couple($('N'),$('O')),couple($('O'),$('S')),couple($('S'),$('W'))])),subset($(obstacles),$(field)),not_member($(baseStation),$(obstacles)),conjunct(less_equal($(betaMax),multiplication($('B'),2)),member($(betaMax),'NATURAL1')),conjunct(less(0,$(epsilonK)),less_equal($(epsilonK),div($('B'),5))),implication(less_equal(1,$(epsilonK)),not_equal(5,0)),member($(visibilityRange),total_function(cartesian_product($(field),$(orientations)),pow_subset(cartesian_product('INTEGER','INTEGER')))),equal($(visibilityRange),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),union(event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(add($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(1,0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),minus($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,unary_minus(1))),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),add($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,1)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field)))),event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(minus($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(unary_minus(1),0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field)))))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(conjunct(conjunct(forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))))),member($(alphaMax),'NATURAL1'),conjunct(less($(alphaInt),$(alphaMax)),member($(alphaInt),'NATURAL')),less_equal(function($(radiation),$(baseStation)),$(alphaMax)),member($(baseStation),domain($(radiation))),member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),conjunct(less(0,$(epsilonS)),less_equal($(epsilonS),div($('B'),5))),implication(less_equal(1,$(epsilonS)),not_equal(5,0)),member($(sensorRange),total_function($(field),pow_subset($(field)))),equal($(sensorRange),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(conjunct(less(unary_minus(add($(epsilonS),1)),minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')))),less(unary_minus(add($(epsilonS),1)),minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),less(minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),less(minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),member(couple($(x),$(y)),$(field))))),member($('Pos'),$(field)))),member($(findInterestingFields),total_function($(field),pow_subset($(field)))),equal($(findInterestingFields),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(less($(alphaInt),function($(radiation),couple($(x),$(y)))),less(function($(radiation),couple($(x),$(y))),$(alphaMax))),member(couple($(x),$(y)),$(field))),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))))),member($('Pos'),$(field)))),forall([$('Pos')],member($('Pos'),$(field)),forall([$(x),$(y)],truth,conjunct(conjunct(implication(conjunct(member(couple($(x),$(y)),$(field)),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))),conjunct(member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),member(couple($(x),$(y)),domain($(radiation))))),member($('Pos'),domain($(sensorRange)))),member($(sensorRange),partial_function(cartesian_product('INTEGER','INTEGER'),pow_subset(cartesian_product('INTEGER','INTEGER'))))))),member($(orientation),$(orientations)),conjunct(less_equal($(battery),$(betaMax)),member($(battery),'NATURAL')),conjunct(less($(betaMin),$(betaMax)),member($(betaMin),'NATURAL')),less_equal(1,$(battery)),subset($(freeFields),$(field)),subset($(occupiedFields),$(field)),member($(baseStation),$(freeFields)),equal(intersection($(obstacles),$(freeFields)),empty_set),subset($(occupiedFields),$(obstacles)),member($(rover),$(freeFields))])])."
      }
    },
    {
      "name": "reselect_hyp",
      "params": {
        "para1": "member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER'))"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(radiation),total_function($(field),'NATURAL')),subset(set_extension([$(rover)]),$(field)),member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER'))],conjunct(member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),member($(rover),domain($(radiation)))),success(1)),[ids_types([b(identifier(field),any,[]),b(identifier(orientations),set(global(orientations)),[]),b(identifier(radiation),any,[]),b(identifier(rover),any,[])]),rawsets([deferred_set(none,orientations),deferred_set(none,fieldTypes)]),des_hyps([conjunct(less_equal(10,$('B')),member($('B'),'NATURAL1')),conjunct(less_equal(10,$('L')),member($('L'),'NATURAL1')),equal($(field),cartesian_product(interval(1,$('B')),interval(1,$('L')))),member($(baseStation),$(field)),partition($(orientations),[set_extension([$('N')]),set_extension([$('O')]),set_extension([$('S')]),set_extension([$('W')])]),member($(initialOrientation),$(orientations)),member($('Offset'),total_function($(orientations),cartesian_product(interval(unary_minus(1),1),interval(unary_minus(1),1)))),equal($('Offset'),set_extension([couple($('N'),couple(0,1)),couple($('O'),couple(1,0)),couple($('S'),couple(0,unary_minus(1))),couple($('W'),couple(unary_minus(1),0))])),equal($(frontPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(add(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),equal($(rearPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(minus(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))),minus(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),member($(newOrientation),total_function($(orientations),$(orientations))),equal($(newOrientation),set_extension([couple($('W'),$('N')),couple($('N'),$('O')),couple($('O'),$('S')),couple($('S'),$('W'))])),subset($(obstacles),$(field)),not_member($(baseStation),$(obstacles)),conjunct(less_equal($(betaMax),multiplication($('B'),2)),member($(betaMax),'NATURAL1')),conjunct(less(0,$(epsilonK)),less_equal($(epsilonK),div($('B'),5))),implication(less_equal(1,$(epsilonK)),not_equal(5,0)),member($(visibilityRange),total_function(cartesian_product($(field),$(orientations)),pow_subset(cartesian_product('INTEGER','INTEGER')))),equal($(visibilityRange),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),union(event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(add($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(1,0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),minus($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,unary_minus(1))),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),add($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,1)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field)))),event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(minus($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(unary_minus(1),0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field)))))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(conjunct(conjunct(forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))))),member($(alphaMax),'NATURAL1'),conjunct(less($(alphaInt),$(alphaMax)),member($(alphaInt),'NATURAL')),less_equal(function($(radiation),$(baseStation)),$(alphaMax)),member($(baseStation),domain($(radiation))),conjunct(less(0,$(epsilonS)),less_equal($(epsilonS),div($('B'),5))),implication(less_equal(1,$(epsilonS)),not_equal(5,0)),member($(sensorRange),total_function($(field),pow_subset($(field)))),equal($(sensorRange),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(conjunct(less(unary_minus(add($(epsilonS),1)),minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')))),less(unary_minus(add($(epsilonS),1)),minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),less(minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),less(minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),member(couple($(x),$(y)),$(field))))),member($('Pos'),$(field)))),member($(findInterestingFields),total_function($(field),pow_subset($(field)))),equal($(findInterestingFields),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(less($(alphaInt),function($(radiation),couple($(x),$(y)))),less(function($(radiation),couple($(x),$(y))),$(alphaMax))),member(couple($(x),$(y)),$(field))),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))))),member($('Pos'),$(field)))),forall([$('Pos')],member($('Pos'),$(field)),forall([$(x),$(y)],truth,conjunct(conjunct(implication(conjunct(member(couple($(x),$(y)),$(field)),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))),conjunct(member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),member(couple($(x),$(y)),domain($(radiation))))),member($('Pos'),domain($(sensorRange)))),member($(sensorRange),partial_function(cartesian_product('INTEGER','INTEGER'),pow_subset(cartesian_product('INTEGER','INTEGER'))))))),member($(orientation),$(orientations)),conjunct(less_equal($(battery),$(betaMax)),member($(battery),'NATURAL')),conjunct(less($(betaMin),$(betaMax)),member($(betaMin),'NATURAL')),less_equal(1,$(battery)),subset($(freeFields),$(field)),subset($(occupiedFields),$(field)),member($(baseStation),$(freeFields)),equal(intersection($(obstacles),$(freeFields)),empty_set),subset($(occupiedFields),$(obstacles)),member($(rover),$(freeFields))])])."
      }
    },
    {
      "name": "and_r",
      "destState": {
        "xtl_state": "state(sequent([member($(radiation),total_function($(field),'NATURAL')),subset(set_extension([$(rover)]),$(field)),member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER'))],member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),sequent([member($(radiation),total_function($(field),'NATURAL')),subset(set_extension([$(rover)]),$(field)),member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER'))],member($(rover),domain($(radiation))),success(1))),[ids_types([b(identifier(field),set(couple(integer,integer)),[]),b(identifier(orientations),set(global(orientations)),[]),b(identifier(radiation),set(couple(couple(integer,integer),integer)),[]),b(identifier(rover),couple(integer,integer),[])]),rawsets([deferred_set(none,orientations),deferred_set(none,fieldTypes)]),des_hyps([conjunct(less_equal(10,$('B')),member($('B'),'NATURAL1')),conjunct(less_equal(10,$('L')),member($('L'),'NATURAL1')),equal($(field),cartesian_product(interval(1,$('B')),interval(1,$('L')))),member($(baseStation),$(field)),partition($(orientations),[set_extension([$('N')]),set_extension([$('O')]),set_extension([$('S')]),set_extension([$('W')])]),member($(initialOrientation),$(orientations)),member($('Offset'),total_function($(orientations),cartesian_product(interval(unary_minus(1),1),interval(unary_minus(1),1)))),equal($('Offset'),set_extension([couple($('N'),couple(0,1)),couple($('O'),couple(1,0)),couple($('S'),couple(0,unary_minus(1))),couple($('W'),couple(unary_minus(1),0))])),equal($(frontPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(add(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),equal($(rearPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(minus(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))),minus(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),member($(newOrientation),total_function($(orientations),$(orientations))),equal($(newOrientation),set_extension([couple($('W'),$('N')),couple($('N'),$('O')),couple($('O'),$('S')),couple($('S'),$('W'))])),subset($(obstacles),$(field)),not_member($(baseStation),$(obstacles)),conjunct(less_equal($(betaMax),multiplication($('B'),2)),member($(betaMax),'NATURAL1')),conjunct(less(0,$(epsilonK)),less_equal($(epsilonK),div($('B'),5))),implication(less_equal(1,$(epsilonK)),not_equal(5,0)),member($(visibilityRange),total_function(cartesian_product($(field),$(orientations)),pow_subset(cartesian_product('INTEGER','INTEGER')))),equal($(visibilityRange),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),union(event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(add($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(1,0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),minus($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,unary_minus(1))),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),add($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,1)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field)))),event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(minus($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(unary_minus(1),0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field)))))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(conjunct(conjunct(forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))))),member($(alphaMax),'NATURAL1'),conjunct(less($(alphaInt),$(alphaMax)),member($(alphaInt),'NATURAL')),less_equal(function($(radiation),$(baseStation)),$(alphaMax)),member($(baseStation),domain($(radiation))),conjunct(less(0,$(epsilonS)),less_equal($(epsilonS),div($('B'),5))),implication(less_equal(1,$(epsilonS)),not_equal(5,0)),member($(sensorRange),total_function($(field),pow_subset($(field)))),equal($(sensorRange),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(conjunct(less(unary_minus(add($(epsilonS),1)),minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')))),less(unary_minus(add($(epsilonS),1)),minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),less(minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),less(minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),member(couple($(x),$(y)),$(field))))),member($('Pos'),$(field)))),member($(findInterestingFields),total_function($(field),pow_subset($(field)))),equal($(findInterestingFields),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(less($(alphaInt),function($(radiation),couple($(x),$(y)))),less(function($(radiation),couple($(x),$(y))),$(alphaMax))),member(couple($(x),$(y)),$(field))),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))))),member($('Pos'),$(field)))),forall([$('Pos')],member($('Pos'),$(field)),forall([$(x),$(y)],truth,conjunct(conjunct(implication(conjunct(member(couple($(x),$(y)),$(field)),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))),conjunct(member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),member(couple($(x),$(y)),domain($(radiation))))),member($('Pos'),domain($(sensorRange)))),member($(sensorRange),partial_function(cartesian_product('INTEGER','INTEGER'),pow_subset(cartesian_product('INTEGER','INTEGER'))))))),member($(orientation),$(orientations)),conjunct(less_equal($(battery),$(betaMax)),member($(battery),'NATURAL')),conjunct(less($(betaMin),$(betaMax)),member($(betaMin),'NATURAL')),less_equal(1,$(battery)),subset($(freeFields),$(field)),subset($(occupiedFields),$(field)),member($(baseStation),$(freeFields)),equal(intersection($(obstacles),$(freeFields)),empty_set),subset($(occupiedFields),$(obstacles)),member($(rover),$(freeFields))])])."
      }
    },
    {
      "name": "hyp",
      "destState": {
        "xtl_state": "state(sequent([member($(radiation),total_function($(field),'NATURAL')),subset(set_extension([$(rover)]),$(field)),member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER'))],member($(rover),domain($(radiation))),success(1)),[ids_types([b(identifier(field),set(couple(integer,integer)),[]),b(identifier(orientations),set(global(orientations)),[]),b(identifier(radiation),set(couple(couple(integer,integer),integer)),[]),b(identifier(rover),couple(integer,integer),[])]),rawsets([deferred_set(none,orientations),deferred_set(none,fieldTypes)]),des_hyps([conjunct(less_equal(10,$('B')),member($('B'),'NATURAL1')),conjunct(less_equal(10,$('L')),member($('L'),'NATURAL1')),equal($(field),cartesian_product(interval(1,$('B')),interval(1,$('L')))),member($(baseStation),$(field)),partition($(orientations),[set_extension([$('N')]),set_extension([$('O')]),set_extension([$('S')]),set_extension([$('W')])]),member($(initialOrientation),$(orientations)),member($('Offset'),total_function($(orientations),cartesian_product(interval(unary_minus(1),1),interval(unary_minus(1),1)))),equal($('Offset'),set_extension([couple($('N'),couple(0,1)),couple($('O'),couple(1,0)),couple($('S'),couple(0,unary_minus(1))),couple($('W'),couple(unary_minus(1),0))])),equal($(frontPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(add(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),equal($(rearPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(minus(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))),minus(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),member($(newOrientation),total_function($(orientations),$(orientations))),equal($(newOrientation),set_extension([couple($('W'),$('N')),couple($('N'),$('O')),couple($('O'),$('S')),couple($('S'),$('W'))])),subset($(obstacles),$(field)),not_member($(baseStation),$(obstacles)),conjunct(less_equal($(betaMax),multiplication($('B'),2)),member($(betaMax),'NATURAL1')),conjunct(less(0,$(epsilonK)),less_equal($(epsilonK),div($('B'),5))),implication(less_equal(1,$(epsilonK)),not_equal(5,0)),member($(visibilityRange),total_function(cartesian_product($(field),$(orientations)),pow_subset(cartesian_product('INTEGER','INTEGER')))),equal($(visibilityRange),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),union(event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(add($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(1,0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),minus($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,unary_minus(1))),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),add($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,1)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field)))),event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(minus($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(unary_minus(1),0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field)))))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(conjunct(conjunct(forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))))),member($(alphaMax),'NATURAL1'),conjunct(less($(alphaInt),$(alphaMax)),member($(alphaInt),'NATURAL')),less_equal(function($(radiation),$(baseStation)),$(alphaMax)),member($(baseStation),domain($(radiation))),conjunct(less(0,$(epsilonS)),less_equal($(epsilonS),div($('B'),5))),implication(less_equal(1,$(epsilonS)),not_equal(5,0)),member($(sensorRange),total_function($(field),pow_subset($(field)))),equal($(sensorRange),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(conjunct(less(unary_minus(add($(epsilonS),1)),minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')))),less(unary_minus(add($(epsilonS),1)),minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),less(minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),less(minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),member(couple($(x),$(y)),$(field))))),member($('Pos'),$(field)))),member($(findInterestingFields),total_function($(field),pow_subset($(field)))),equal($(findInterestingFields),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(less($(alphaInt),function($(radiation),couple($(x),$(y)))),less(function($(radiation),couple($(x),$(y))),$(alphaMax))),member(couple($(x),$(y)),$(field))),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))))),member($('Pos'),$(field)))),forall([$('Pos')],member($('Pos'),$(field)),forall([$(x),$(y)],truth,conjunct(conjunct(implication(conjunct(member(couple($(x),$(y)),$(field)),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))),conjunct(member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),member(couple($(x),$(y)),domain($(radiation))))),member($('Pos'),domain($(sensorRange)))),member($(sensorRange),partial_function(cartesian_product('INTEGER','INTEGER'),pow_subset(cartesian_product('INTEGER','INTEGER'))))))),member($(orientation),$(orientations)),conjunct(less_equal($(battery),$(betaMax)),member($(battery),'NATURAL')),conjunct(less($(betaMin),$(betaMax)),member($(betaMin),'NATURAL')),less_equal(1,$(battery)),subset($(freeFields),$(field)),subset($(occupiedFields),$(field)),member($(baseStation),$(freeFields)),equal(intersection($(obstacles),$(freeFields)),empty_set),subset($(occupiedFields),$(obstacles)),member($(rover),$(freeFields))])])."
      }
    },
    {
      "name": "simplify_hyp",
      "params": {
        "para1": "'DEF_IN_TFCT'",
        "para2": "member($(radiation),total_function($(field),'NATURAL'))"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(radiation),partial_function($(field),'NATURAL')),equal(domain($(radiation)),$(field)),subset(set_extension([$(rover)]),$(field)),member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER'))],member($(rover),domain($(radiation))),success(1)),[ids_types([b(identifier(field),set(couple(integer,integer)),[]),b(identifier(orientations),set(global(orientations)),[]),b(identifier(radiation),set(couple(couple(integer,integer),integer)),[]),b(identifier(rover),couple(integer,integer),[])]),rawsets([deferred_set(none,orientations),deferred_set(none,fieldTypes)]),des_hyps([conjunct(less_equal(10,$('B')),member($('B'),'NATURAL1')),conjunct(less_equal(10,$('L')),member($('L'),'NATURAL1')),equal($(field),cartesian_product(interval(1,$('B')),interval(1,$('L')))),member($(baseStation),$(field)),partition($(orientations),[set_extension([$('N')]),set_extension([$('O')]),set_extension([$('S')]),set_extension([$('W')])]),member($(initialOrientation),$(orientations)),member($('Offset'),total_function($(orientations),cartesian_product(interval(unary_minus(1),1),interval(unary_minus(1),1)))),equal($('Offset'),set_extension([couple($('N'),couple(0,1)),couple($('O'),couple(1,0)),couple($('S'),couple(0,unary_minus(1))),couple($('W'),couple(unary_minus(1),0))])),equal($(frontPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(add(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),equal($(rearPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(minus(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))),minus(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),member($(newOrientation),total_function($(orientations),$(orientations))),equal($(newOrientation),set_extension([couple($('W'),$('N')),couple($('N'),$('O')),couple($('O'),$('S')),couple($('S'),$('W'))])),subset($(obstacles),$(field)),not_member($(baseStation),$(obstacles)),conjunct(less_equal($(betaMax),multiplication($('B'),2)),member($(betaMax),'NATURAL1')),conjunct(less(0,$(epsilonK)),less_equal($(epsilonK),div($('B'),5))),implication(less_equal(1,$(epsilonK)),not_equal(5,0)),member($(visibilityRange),total_function(cartesian_product($(field),$(orientations)),pow_subset(cartesian_product('INTEGER','INTEGER')))),equal($(visibilityRange),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),union(event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(add($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(1,0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),minus($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,unary_minus(1))),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),add($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,1)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field)))),event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(minus($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(unary_minus(1),0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field)))))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(conjunct(conjunct(forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))))),member($(alphaMax),'NATURAL1'),conjunct(less($(alphaInt),$(alphaMax)),member($(alphaInt),'NATURAL')),less_equal(function($(radiation),$(baseStation)),$(alphaMax)),member($(baseStation),domain($(radiation))),conjunct(less(0,$(epsilonS)),less_equal($(epsilonS),div($('B'),5))),implication(less_equal(1,$(epsilonS)),not_equal(5,0)),member($(sensorRange),total_function($(field),pow_subset($(field)))),equal($(sensorRange),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(conjunct(less(unary_minus(add($(epsilonS),1)),minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')))),less(unary_minus(add($(epsilonS),1)),minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),less(minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),less(minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),member(couple($(x),$(y)),$(field))))),member($('Pos'),$(field)))),member($(findInterestingFields),total_function($(field),pow_subset($(field)))),equal($(findInterestingFields),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(less($(alphaInt),function($(radiation),couple($(x),$(y)))),less(function($(radiation),couple($(x),$(y))),$(alphaMax))),member(couple($(x),$(y)),$(field))),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))))),member($('Pos'),$(field)))),forall([$('Pos')],member($('Pos'),$(field)),forall([$(x),$(y)],truth,conjunct(conjunct(implication(conjunct(member(couple($(x),$(y)),$(field)),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))),conjunct(member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),member(couple($(x),$(y)),domain($(radiation))))),member($('Pos'),domain($(sensorRange)))),member($(sensorRange),partial_function(cartesian_product('INTEGER','INTEGER'),pow_subset(cartesian_product('INTEGER','INTEGER'))))))),member($(orientation),$(orientations)),conjunct(less_equal($(battery),$(betaMax)),member($(battery),'NATURAL')),conjunct(less($(betaMin),$(betaMax)),member($(betaMin),'NATURAL')),less_equal(1,$(battery)),subset($(freeFields),$(field)),subset($(occupiedFields),$(field)),member($(baseStation),$(freeFields)),equal(intersection($(obstacles),$(freeFields)),empty_set),subset($(occupiedFields),$(obstacles)),member($(rover),$(freeFields))])])."
      }
    },
    {
      "name": "eq",
      "params": {
        "para1": "lr",
        "para2": "domain($(radiation))",
        "para3": "$(field)"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(radiation),partial_function($(field),'NATURAL')),subset(set_extension([$(rover)]),$(field)),member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER'))],member($(rover),$(field)),success(1)),[ids_types([b(identifier(field),set(couple(integer,integer)),[]),b(identifier(orientations),set(global(orientations)),[]),b(identifier(radiation),set(couple(couple(integer,integer),integer)),[]),b(identifier(rover),couple(integer,integer),[])]),rawsets([deferred_set(none,orientations),deferred_set(none,fieldTypes)]),des_hyps([conjunct(less_equal(10,$('B')),member($('B'),'NATURAL1')),conjunct(less_equal(10,$('L')),member($('L'),'NATURAL1')),equal($(field),cartesian_product(interval(1,$('B')),interval(1,$('L')))),member($(baseStation),$(field)),partition($(orientations),[set_extension([$('N')]),set_extension([$('O')]),set_extension([$('S')]),set_extension([$('W')])]),member($(initialOrientation),$(orientations)),member($('Offset'),total_function($(orientations),cartesian_product(interval(unary_minus(1),1),interval(unary_minus(1),1)))),equal($('Offset'),set_extension([couple($('N'),couple(0,1)),couple($('O'),couple(1,0)),couple($('S'),couple(0,unary_minus(1))),couple($('W'),couple(unary_minus(1),0))])),equal($(frontPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(add(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),equal($(rearPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(minus(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))),minus(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),member($(newOrientation),total_function($(orientations),$(orientations))),equal($(newOrientation),set_extension([couple($('W'),$('N')),couple($('N'),$('O')),couple($('O'),$('S')),couple($('S'),$('W'))])),subset($(obstacles),$(field)),not_member($(baseStation),$(obstacles)),conjunct(less_equal($(betaMax),multiplication($('B'),2)),member($(betaMax),'NATURAL1')),conjunct(less(0,$(epsilonK)),less_equal($(epsilonK),div($('B'),5))),implication(less_equal(1,$(epsilonK)),not_equal(5,0)),member($(visibilityRange),total_function(cartesian_product($(field),$(orientations)),pow_subset(cartesian_product('INTEGER','INTEGER')))),equal($(visibilityRange),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),union(event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(add($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(1,0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),minus($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,unary_minus(1))),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),add($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,1)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field)))),event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(minus($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(unary_minus(1),0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field)))))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(conjunct(conjunct(forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))))),member($(alphaMax),'NATURAL1'),conjunct(less($(alphaInt),$(alphaMax)),member($(alphaInt),'NATURAL')),less_equal(function($(radiation),$(baseStation)),$(alphaMax)),member($(baseStation),domain($(radiation))),conjunct(less(0,$(epsilonS)),less_equal($(epsilonS),div($('B'),5))),implication(less_equal(1,$(epsilonS)),not_equal(5,0)),member($(sensorRange),total_function($(field),pow_subset($(field)))),equal($(sensorRange),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(conjunct(less(unary_minus(add($(epsilonS),1)),minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')))),less(unary_minus(add($(epsilonS),1)),minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),less(minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),less(minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),member(couple($(x),$(y)),$(field))))),member($('Pos'),$(field)))),member($(findInterestingFields),total_function($(field),pow_subset($(field)))),equal($(findInterestingFields),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(less($(alphaInt),function($(radiation),couple($(x),$(y)))),less(function($(radiation),couple($(x),$(y))),$(alphaMax))),member(couple($(x),$(y)),$(field))),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))))),member($('Pos'),$(field)))),forall([$('Pos')],member($('Pos'),$(field)),forall([$(x),$(y)],truth,conjunct(conjunct(implication(conjunct(member(couple($(x),$(y)),$(field)),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))),conjunct(member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),member(couple($(x),$(y)),domain($(radiation))))),member($('Pos'),domain($(sensorRange)))),member($(sensorRange),partial_function(cartesian_product('INTEGER','INTEGER'),pow_subset(cartesian_product('INTEGER','INTEGER'))))))),member($(orientation),$(orientations)),conjunct(less_equal($(battery),$(betaMax)),member($(battery),'NATURAL')),conjunct(less($(betaMin),$(betaMax)),member($(betaMin),'NATURAL')),less_equal(1,$(battery)),subset($(freeFields),$(field)),subset($(occupiedFields),$(field)),member($(baseStation),$(freeFields)),equal(intersection($(obstacles),$(freeFields)),empty_set),subset($(occupiedFields),$(obstacles)),member($(rover),$(freeFields))])])."
      }
    },
    {
      "name": "simplify_hyp",
      "params": {
        "para1": "'SIMP_SUBSETEQ_SING'",
        "para2": "subset(set_extension([$(rover)]),$(field))"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(radiation),partial_function($(field),'NATURAL')),member($(rover),$(field)),member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER'))],member($(rover),$(field)),success(1)),[ids_types([b(identifier(field),set(couple(integer,integer)),[]),b(identifier(orientations),set(global(orientations)),[]),b(identifier(radiation),set(couple(couple(integer,integer),integer)),[]),b(identifier(rover),couple(integer,integer),[])]),rawsets([deferred_set(none,orientations),deferred_set(none,fieldTypes)]),des_hyps([conjunct(less_equal(10,$('B')),member($('B'),'NATURAL1')),conjunct(less_equal(10,$('L')),member($('L'),'NATURAL1')),equal($(field),cartesian_product(interval(1,$('B')),interval(1,$('L')))),member($(baseStation),$(field)),partition($(orientations),[set_extension([$('N')]),set_extension([$('O')]),set_extension([$('S')]),set_extension([$('W')])]),member($(initialOrientation),$(orientations)),member($('Offset'),total_function($(orientations),cartesian_product(interval(unary_minus(1),1),interval(unary_minus(1),1)))),equal($('Offset'),set_extension([couple($('N'),couple(0,1)),couple($('O'),couple(1,0)),couple($('S'),couple(0,unary_minus(1))),couple($('W'),couple(unary_minus(1),0))])),equal($(frontPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(add(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),equal($(rearPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(minus(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))),minus(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),member($(newOrientation),total_function($(orientations),$(orientations))),equal($(newOrientation),set_extension([couple($('W'),$('N')),couple($('N'),$('O')),couple($('O'),$('S')),couple($('S'),$('W'))])),subset($(obstacles),$(field)),not_member($(baseStation),$(obstacles)),conjunct(less_equal($(betaMax),multiplication($('B'),2)),member($(betaMax),'NATURAL1')),conjunct(less(0,$(epsilonK)),less_equal($(epsilonK),div($('B'),5))),implication(less_equal(1,$(epsilonK)),not_equal(5,0)),member($(visibilityRange),total_function(cartesian_product($(field),$(orientations)),pow_subset(cartesian_product('INTEGER','INTEGER')))),equal($(visibilityRange),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),union(event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(add($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(1,0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),minus($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,unary_minus(1))),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),add($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,1)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field)))),event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(minus($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(unary_minus(1),0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field)))))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(conjunct(conjunct(forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))))),member($(alphaMax),'NATURAL1'),conjunct(less($(alphaInt),$(alphaMax)),member($(alphaInt),'NATURAL')),less_equal(function($(radiation),$(baseStation)),$(alphaMax)),member($(baseStation),domain($(radiation))),conjunct(less(0,$(epsilonS)),less_equal($(epsilonS),div($('B'),5))),implication(less_equal(1,$(epsilonS)),not_equal(5,0)),member($(sensorRange),total_function($(field),pow_subset($(field)))),equal($(sensorRange),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(conjunct(less(unary_minus(add($(epsilonS),1)),minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')))),less(unary_minus(add($(epsilonS),1)),minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),less(minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),less(minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),member(couple($(x),$(y)),$(field))))),member($('Pos'),$(field)))),member($(findInterestingFields),total_function($(field),pow_subset($(field)))),equal($(findInterestingFields),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(less($(alphaInt),function($(radiation),couple($(x),$(y)))),less(function($(radiation),couple($(x),$(y))),$(alphaMax))),member(couple($(x),$(y)),$(field))),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))))),member($('Pos'),$(field)))),forall([$('Pos')],member($('Pos'),$(field)),forall([$(x),$(y)],truth,conjunct(conjunct(implication(conjunct(member(couple($(x),$(y)),$(field)),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))),conjunct(member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),member(couple($(x),$(y)),domain($(radiation))))),member($('Pos'),domain($(sensorRange)))),member($(sensorRange),partial_function(cartesian_product('INTEGER','INTEGER'),pow_subset(cartesian_product('INTEGER','INTEGER'))))))),member($(orientation),$(orientations)),conjunct(less_equal($(battery),$(betaMax)),member($(battery),'NATURAL')),conjunct(less($(betaMin),$(betaMax)),member($(betaMin),'NATURAL')),less_equal(1,$(battery)),subset($(freeFields),$(field)),subset($(occupiedFields),$(field)),member($(baseStation),$(freeFields)),equal(intersection($(obstacles),$(freeFields)),empty_set),subset($(occupiedFields),$(obstacles)),member($(rover),$(freeFields))])])."
      }
    },
    {
      "name": "hyp",
      "destState": {
        "xtl_state": "state(success(1),[ids_types([b(identifier(field),set(couple(integer,integer)),[]),b(identifier(orientations),set(global(orientations)),[]),b(identifier(radiation),set(couple(couple(integer,integer),integer)),[]),b(identifier(rover),couple(integer,integer),[])]),rawsets([deferred_set(none,orientations),deferred_set(none,fieldTypes)]),des_hyps([conjunct(less_equal(10,$('B')),member($('B'),'NATURAL1')),conjunct(less_equal(10,$('L')),member($('L'),'NATURAL1')),equal($(field),cartesian_product(interval(1,$('B')),interval(1,$('L')))),member($(baseStation),$(field)),partition($(orientations),[set_extension([$('N')]),set_extension([$('O')]),set_extension([$('S')]),set_extension([$('W')])]),member($(initialOrientation),$(orientations)),member($('Offset'),total_function($(orientations),cartesian_product(interval(unary_minus(1),1),interval(unary_minus(1),1)))),equal($('Offset'),set_extension([couple($('N'),couple(0,1)),couple($('O'),couple(1,0)),couple($('S'),couple(0,unary_minus(1))),couple($('W'),couple(unary_minus(1),0))])),equal($(frontPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(add(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation))),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),equal($(rearPosition),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),couple(minus(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))),minus(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),function($('Offset'),$(orientation)))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),member($(newOrientation),total_function($(orientations),$(orientations))),equal($(newOrientation),set_extension([couple($('W'),$('N')),couple($('N'),$('O')),couple($('O'),$('S')),couple($('S'),$('W'))])),subset($(obstacles),$(field)),not_member($(baseStation),$(obstacles)),conjunct(less_equal($(betaMax),multiplication($('B'),2)),member($(betaMax),'NATURAL1')),conjunct(less(0,$(epsilonK)),less_equal($(epsilonK),div($('B'),5))),implication(less_equal(1,$(epsilonK)),not_equal(5,0)),member($(visibilityRange),total_function(cartesian_product($(field),$(orientations)),pow_subset(cartesian_product('INTEGER','INTEGER')))),equal($(visibilityRange),event_b_comprehension_set([$('Pos'),$(orientation)],couple(couple($('Pos'),$(orientation)),union(event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(add($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(1,0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),minus($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,unary_minus(1))),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field)))),union(event_b_comprehension_set([$(x),$(l),$(y),$(k)],couple(add($(x),$(l)),add($(y),$(k))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(0,1)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field)))),event_b_comprehension_set([$(x),$(k),$(y),$(l)],couple(minus($(x),$(k)),add($(y),$(l))),conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function($('Offset'),$(orientation)),couple(unary_minus(1),0)),equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x))),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field)))))))),conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))))),forall([$('Pos'),$(orientation)],conjunct(member($('Pos'),$(field)),member($(orientation),$(orientations))),conjunct(conjunct(conjunct(forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(k)),add($(y),1)),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))),forall([$(x),$(k),$(y),$(l)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(minus($(x),$(k)),add($(y),$(l))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),add($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset')))))),forall([$(x),$(l),$(y),$(k)],conjunct(conjunct(conjunct(conjunct(conjunct(conjunct(equal(function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(x)),equal(function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')),$(y))),member($(k),'NATURAL')),member($(k),interval(1,$(epsilonK)))),member($(l),'INTEGER')),member($(l),interval(unary_minus($(k)),$(k)))),member(couple(add($(x),$(l)),minus($(y),$(k))),$(field))),conjunct(member($('Offset'),partial_function($(orientations),cartesian_product('INTEGER','INTEGER'))),member($(orientation),domain($('Offset'))))))),member($(alphaMax),'NATURAL1'),conjunct(less($(alphaInt),$(alphaMax)),member($(alphaInt),'NATURAL')),less_equal(function($(radiation),$(baseStation)),$(alphaMax)),member($(baseStation),domain($(radiation))),conjunct(less(0,$(epsilonS)),less_equal($(epsilonS),div($('B'),5))),implication(less_equal(1,$(epsilonS)),not_equal(5,0)),member($(sensorRange),total_function($(field),pow_subset($(field)))),equal($(sensorRange),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(conjunct(less(unary_minus(add($(epsilonS),1)),minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos')))),less(unary_minus(add($(epsilonS),1)),minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))))),less(minus($(x),function(typeof(event_b_first_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),less(minus($(y),function(typeof(event_b_second_projection_v2,pow_subset(cartesian_product(cartesian_product('INTEGER','INTEGER'),'INTEGER'))),$('Pos'))),add($(epsilonS),1))),member(couple($(x),$(y)),$(field))))),member($('Pos'),$(field)))),member($(findInterestingFields),total_function($(field),pow_subset($(field)))),equal($(findInterestingFields),event_b_comprehension_set([$('Pos')],couple($('Pos'),event_b_comprehension_set([$(x),$(y)],couple($(x),$(y)),conjunct(conjunct(conjunct(less($(alphaInt),function($(radiation),couple($(x),$(y)))),less(function($(radiation),couple($(x),$(y))),$(alphaMax))),member(couple($(x),$(y)),$(field))),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))))),member($('Pos'),$(field)))),forall([$('Pos')],member($('Pos'),$(field)),forall([$(x),$(y)],truth,conjunct(conjunct(implication(conjunct(member(couple($(x),$(y)),$(field)),member(couple($(x),$(y)),function($(sensorRange),$('Pos')))),conjunct(member($(radiation),partial_function(cartesian_product('INTEGER','INTEGER'),'INTEGER')),member(couple($(x),$(y)),domain($(radiation))))),member($('Pos'),domain($(sensorRange)))),member($(sensorRange),partial_function(cartesian_product('INTEGER','INTEGER'),pow_subset(cartesian_product('INTEGER','INTEGER'))))))),member($(orientation),$(orientations)),conjunct(less_equal($(battery),$(betaMax)),member($(battery),'NATURAL')),conjunct(less($(betaMin),$(betaMax)),member($(betaMin),'NATURAL')),less_equal(1,$(battery)),subset($(freeFields),$(field)),subset($(occupiedFields),$(field)),member($(baseStation),$(freeFields)),equal(intersection($(obstacles),$(freeFields)),empty_set),subset($(occupiedFields),$(obstacles)),member($(rover),$(freeFields))])])."
      }
    }
  ],
  "machineOperationInfos": {
    "pp": {
      "operationName": "pp",
      "topLevel": true,
      "type": "XTL"
    },
    "dis_binter_r": {
      "operationName": "dis_binter_r",
      "parameterNames": [
        "PFun"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "dis_binter_l": {
      "operationName": "dis_binter_l",
      "parameterNames": [
        "PFun"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "fin_fun_dom_r": {
      "operationName": "fin_fun_dom_r",
      "parameterNames": [
        "PFun"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "dis_setminus_l": {
      "operationName": "dis_setminus_l",
      "parameterNames": [
        "PFun"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "fin_rel_r": {
      "operationName": "fin_rel_r",
      "parameterNames": [
        "Rel"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "fin_fun_img_r": {
      "operationName": "fin_fun_img_r",
      "parameterNames": [
        "PFun"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "fin_fun2_r": {
      "operationName": "fin_fun2_r",
      "parameterNames": [
        "PFun"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "fin_fun1_r": {
      "operationName": "fin_fun1_r",
      "parameterNames": [
        "PFun"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "rewrite_hyp": {
      "operationName": "rewrite_hyp",
      "parameterNames": [
        "HypNr",
        "NewHyp"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "ml_pp": {
      "operationName": "ml_pp",
      "topLevel": true,
      "type": "XTL"
    },
    "distinct_case": {
      "operationName": "distinct_case",
      "parameterNames": [
        "Pred"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "exists_inst": {
      "operationName": "exists_inst",
      "parameterNames": [
        "Inst"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "dis_setminus_r": {
      "operationName": "dis_setminus_r",
      "parameterNames": [
        "PFun"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "derive_hyp": {
      "operationName": "derive_hyp",
      "parameterNames": [
        "HypNrs",
        "NewHyp"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "prob_wd_prover": {
      "operationName": "prob_wd_prover",
      "topLevel": true,
      "type": "XTL"
    },
    "fin_fun_ran_r": {
      "operationName": "fin_fun_ran_r",
      "parameterNames": [
        "PFun"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "ml": {
      "operationName": "ml",
      "topLevel": true,
      "type": "XTL"
    },
    "prob_disprover": {
      "operationName": "prob_disprover",
      "topLevel": true,
      "type": "XTL"
    },
    "fin_subseteq_r": {
      "operationName": "fin_subseteq_r",
      "parameterNames": [
        "Set"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "add_hyp": {
      "operationName": "add_hyp",
      "parameterNames": [
        "Hyp"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "forall_inst_mt": {
      "operationName": "forall_inst_mt",
      "parameterNames": [
        "HypNr",
        "Inst"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "forall_inst": {
      "operationName": "forall_inst",
      "parameterNames": [
        "HypNr",
        "Inst"
      ],
      "topLevel": true,
      "type": "XTL"
    },
    "z3": {
      "operationName": "z3",
      "topLevel": true,
      "type": "XTL"
    },
    "forall_inst_mp": {
      "operationName": "forall_inst_mp",
      "parameterNames": [
        "HypNr",
        "Inst"
      ],
      "topLevel": true,
      "type": "XTL"
    }
  },
  "metadata": {
    "fileType": "Trace",
    "formatVersion": 6,
    "savedAt": "2026-05-29T16:36:50.532067Z",
    "creator": "traceReplay",
    "proB2KernelVersion": "4.15.2-SNAPSHOT",
    "proBCliVersion": "1.16.0-nightly",
    "modelName": "Rover3_mch"
  }
}