{
  "transitionList": [
    {
      "name": "start_xtl_system",
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),implication(equal($(elements),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))))],implication(equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))),success(11)),[rawsets([]),des_hyps([subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset($(pos),$('ELEMENTS')),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))))])])."
      }
    },
    {
      "name": "reselect_hyp",
      "params": {
        "para1": "subset($(pos),$('ELEMENTS'))"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),implication(equal($(elements),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))),subset($(pos),$('ELEMENTS'))],implication(equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(pos),set(integer),[])]),rawsets([]),des_hyps([subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),subset($(elements),$('ELEMENTS')),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))))])])."
      }
    },
    {
      "name": "reselect_hyp",
      "params": {
        "para1": "subset($(elements),$('ELEMENTS'))"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),implication(equal($(elements),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))),subset($(pos),$('ELEMENTS')),subset($(elements),$('ELEMENTS'))],implication(equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(pos),set(integer),[])]),rawsets([]),des_hyps([subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))))])])."
      }
    },
    {
      "name": "reselect_hyp",
      "params": {
        "para1": "subset_strict($('ELEMENTS'),'INTEGER')"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),implication(equal($(elements),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))),subset($(pos),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER')],implication(equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(pos),set(integer),[])]),rawsets([]),des_hyps([finite($('ELEMENTS')),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))))])])."
      }
    },
    {
      "name": "reselect_hyp",
      "params": {
        "para1": "equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))))"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),implication(equal($(elements),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))),subset($(pos),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))))],implication(equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(pos),set(integer),[])]),rawsets([]),des_hyps([finite($('ELEMENTS'))])])."
      }
    },
    {
      "name": "reselect_hyp",
      "params": {
        "para1": "finite($('ELEMENTS'))"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),implication(equal($(elements),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))),subset($(pos),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),finite($('ELEMENTS'))],implication(equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(pos),set(integer),[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "imp_r",
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),implication(equal($(elements),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))),subset($(pos),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set)],equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(pos),set(integer),[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "imp_case",
      "params": {
        "para1": "implication(equal($(elements),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))))"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset($(pos),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset($(pos),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))],equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))),success(11))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(pos),set(integer),[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "skip_to_cont",
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset($(pos),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))],equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset($(pos),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))),success(11))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(pos),set(integer),[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "hyp",
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset($(pos),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],equal($(pos),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(pos),set(integer),[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "eq",
      "params": {
        "para1": "lr",
        "para2": "$(pos)",
        "para3": "event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],equal(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(pos),set(integer),[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'DERIV_EQUAL'"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),success(11))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_hyp",
      "params": {
        "para1": "'DEF_SUBSETEQ'",
        "para2": "subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS'))"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),forall([$(y)],member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),member($(y),$('ELEMENTS'))),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),success(11))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'DEF_SUBSETEQ'"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),forall([$(y)],member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),member($(y),$('ELEMENTS'))),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],forall([$(y)],member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),success(11))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "all_r",
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),forall([$(y)],member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),member($(y),$('ELEMENTS'))),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],implication(member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),success(11))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "imp_r",
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),forall([$(y)],member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),member($(y),$('ELEMENTS'))),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set)),member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))))],member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),success(11))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_hyp",
      "params": {
        "para1": "'SIMP_IN_COMPSET_ONEPOINT'",
        "para2": "member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))))"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),forall([$(y)],member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),member($(y),$('ELEMENTS'))),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),set_subtraction($('ELEMENTS'),$(elements)))],member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),success(11))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'SIMP_IN_COMPSET_ONEPOINT'"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),forall([$(y)],member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),member($(y),$('ELEMENTS'))),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),set_subtraction($('ELEMENTS'),$(elements)))],less(0,$(y)),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),forall([$(y)],member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),member($(y),$('ELEMENTS'))),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),set_subtraction($('ELEMENTS'),$(elements)))],member($(y),$('ELEMENTS')),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),success(11)))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "hyp",
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),forall([$(y)],member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),member($(y),$('ELEMENTS'))),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),set_subtraction($('ELEMENTS'),$(elements)))],member($(y),$('ELEMENTS')),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),success(11))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_hyp",
      "params": {
        "para1": "'DEF_IN_SETMINUS'",
        "para2": "member($(y),set_subtraction($('ELEMENTS'),$(elements)))"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),forall([$(y)],member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),member($(y),$('ELEMENTS'))),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS')),negation(member($(y),$(elements)))],member($(y),$('ELEMENTS')),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),success(11))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "hyp",
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'DEF_SUBSETEQ'"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],forall([$(y)],member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))),member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "all_r",
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set))],implication(member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS'))))),member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "imp_r",
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set)),member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))],member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_hyp",
      "params": {
        "para1": "'SIMP_IN_COMPSET_ONEPOINT'",
        "para2": "member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),$('ELEMENTS')))))"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS'))],member($(y),event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements)))))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'SIMP_IN_COMPSET_ONEPOINT'"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS'))],less(0,$(y)),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS'))],member($(y),set_subtraction($('ELEMENTS'),$(elements))),success(11))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "hyp",
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),equal(set_subtraction($(elements),set_extension([$(e)])),empty_set),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS'))],member($(y),set_subtraction($('ELEMENTS'),$(elements))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_hyp",
      "params": {
        "para1": "'SIMP_SETMINUS_EQUAL_EMPTY'",
        "para2": "equal(set_subtraction($(elements),set_extension([$(e)])),empty_set)"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),subset($(elements),set_extension([$(e)])),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS'))],member($(y),set_subtraction($('ELEMENTS'),$(elements))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_hyp",
      "params": {
        "para1": "'DEF_SUBSETEQ'",
        "para2": "subset($(elements),set_extension([$(e)]))"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),forall([$(x)],member($(x),$(elements)),member($(x),set_extension([$(e)]))),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS'))],member($(y),set_subtraction($('ELEMENTS'),$(elements))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "forall_inst",
      "params": {
        "Inst": "y",
        "HypNr": "6"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),forall([$(x)],member($(x),$(elements)),member($(x),set_extension([$(e)]))),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS'))],truth,sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),implication(member($(y),$(elements)),member($(y),set_extension([$(e)]))),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS'))],member($(y),set_subtraction($('ELEMENTS'),$(elements))),success(11))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "true_goal",
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),implication(member($(y),$(elements)),member($(y),set_extension([$(e)]))),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS'))],member($(y),set_subtraction($('ELEMENTS'),$(elements))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "imp_case",
      "params": {
        "para1": "implication(member($(y),$(elements)),member($(y),set_extension([$(e)])))"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS')),negation(member($(y),$(elements)))],member($(y),set_subtraction($('ELEMENTS'),$(elements))),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS')),member($(y),set_extension([$(e)]))],member($(y),set_subtraction($('ELEMENTS'),$(elements))),success(11))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'DEF_IN_SETMINUS'"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS')),negation(member($(y),$(elements)))],member($(y),$('ELEMENTS')),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS')),negation(member($(y),$(elements)))],negation(member($(y),$(elements))),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS')),member($(y),set_extension([$(e)]))],member($(y),set_subtraction($('ELEMENTS'),$(elements))),success(11)))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "hyp",
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS')),negation(member($(y),$(elements)))],negation(member($(y),$(elements))),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS')),member($(y),set_extension([$(e)]))],member($(y),set_subtraction($('ELEMENTS'),$(elements))),success(11))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "hyp",
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS')),member($(y),set_extension([$(e)]))],member($(y),set_subtraction($('ELEMENTS'),$(elements))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'DEF_IN_SETMINUS'"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS')),member($(y),set_extension([$(e)]))],member($(y),$('ELEMENTS')),sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS')),member($(y),set_extension([$(e)]))],negation(member($(y),$(elements))),success(11))),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "hyp",
      "destState": {
        "xtl_state": "state(sequent([conjunct(less_equal($(e),0),member($(e),$(elements))),subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS')),member($(y),set_extension([$(e)]))],negation(member($(y),$(elements))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "and_l",
      "params": {
        "para1": "conjunct(less_equal($(e),0),member($(e),$(elements)))"
      },
      "destState": {
        "xtl_state": "state(sequent([subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS')),member($(y),set_extension([$(e)])),less_equal($(e),0),member($(e),$(elements))],negation(member($(y),$(elements))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_hyp",
      "params": {
        "para1": "'SIMP_IN_SING'",
        "para2": "member($(y),set_extension([$(e)]))"
      },
      "destState": {
        "xtl_state": "state(sequent([subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS')),equal($(y),$(e)),less_equal($(e),0),member($(e),$(elements))],negation(member($(y),$(elements))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "eq",
      "params": {
        "para1": "rl",
        "para2": "$(y)",
        "para3": "$(e)"
      },
      "destState": {
        "xtl_state": "state(sequent([subset(event_b_comprehension_set([$(x)],$(x),conjunct(less(0,$(x)),member($(x),set_subtraction($('ELEMENTS'),$(elements))))),$('ELEMENTS')),subset($(elements),$('ELEMENTS')),subset_strict($('ELEMENTS'),'INTEGER'),finite($('ELEMENTS')),negation(equal($(elements),empty_set)),less(0,$(y)),member($(y),$('ELEMENTS')),less_equal($(y),0),member($(y),$(elements))],negation(member($(y),$(elements))),success(11)),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(e),integer,[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "cntr",
      "destState": {
        "xtl_state": "state(success(11),[ids_types([b(identifier('ELEMENTS'),set(integer),[]),b(identifier(elements),set(integer),[]),b(identifier(y),integer,[])]),rawsets([]),des_hyps([])])."
      }
    }
  ],
  "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-01-26T10:25:01.471481Z",
    "creator": "traceReplay",
    "proB2KernelVersion": "4.15.2-SNAPSHOT",
    "proBCliVersion": "1.16.0-nightly",
    "modelName": "GetPositiveElements"
  }
}