{
  "transitionList": [
    {
      "name": "start_xtl_system",
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],conjunct(conjunct(conjunct(exists([$(b)],forall([$(x)],member($(x),range($(arr))),less_equal($(x),$(b)))),member($(arr),partial_function('INTEGER','INTEGER'))),member($(mxi),domain($(arr)))),not_equal(range($(arr)),empty_set)),success(2)),[rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "and_r",
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],exists([$(b)],forall([$(x)],member($(x),range($(arr))),less_equal($(x),$(b)))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(mxi),domain($(arr))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],not_equal(range($(arr)),empty_set),success(2))))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "upper_bound_r",
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],finite(range($(arr))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(mxi),domain($(arr))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],not_equal(range($(arr)),empty_set),success(2))))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "fin_rel_ran_r",
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],finite($(arr)),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(mxi),domain($(arr))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],not_equal(range($(arr)),empty_set),success(2))))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "fin_fun1_r",
      "params": {
        "PFun": "'1..n +-> NATURAL1'"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function(interval(1,$(n)),'NATURAL1')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],finite(interval(1,$(n))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(mxi),domain($(arr))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],not_equal(range($(arr)),empty_set),success(2)))))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_hyp",
      "params": {
        "para1": "'DEF_IN_TFCT'",
        "para2": "member($(arr),total_function(interval(1,$(n)),'NATURAL1'))"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(member($(arr),partial_function(interval(1,$(n)),'NATURAL1')),equal(domain($(arr)),interval(1,$(n)))),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function(interval(1,$(n)),'NATURAL1')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],finite(interval(1,$(n))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(mxi),domain($(arr))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],not_equal(range($(arr)),empty_set),success(2)))))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "and_l",
      "params": {
        "para1": "conjunct(member($(arr),partial_function(interval(1,$(n)),'NATURAL1')),equal(domain($(arr)),interval(1,$(n))))"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi)))),member($(arr),partial_function(interval(1,$(n)),'NATURAL1')),equal(domain($(arr)),interval(1,$(n)))],member($(arr),partial_function(interval(1,$(n)),'NATURAL1')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],finite(interval(1,$(n))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(mxi),domain($(arr))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],not_equal(range($(arr)),empty_set),success(2)))))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "hyp",
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],finite(interval(1,$(n))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(mxi),domain($(arr))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],not_equal(range($(arr)),empty_set),success(2))))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'Evaluate tautology'"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],truth,sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(mxi),domain($(arr))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],not_equal(range($(arr)),empty_set),success(2))))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "true_goal",
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(mxi),domain($(arr))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],not_equal(range($(arr)),empty_set),success(2)))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "fun_goal",
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(mxi),domain($(arr))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],not_equal(range($(arr)),empty_set),success(2))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_hyp",
      "params": {
        "para1": "'DEF_IN_TFCT'",
        "para2": "member($(arr),total_function(interval(1,$(n)),'NATURAL1'))"
      },
      "destState": {
        "xtl_state": "state(sequent([conjunct(member($(arr),partial_function(interval(1,$(n)),'NATURAL1')),equal(domain($(arr)),interval(1,$(n)))),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(mxi),domain($(arr))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],not_equal(range($(arr)),empty_set),success(2))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "and_l",
      "params": {
        "para1": "conjunct(member($(arr),partial_function(interval(1,$(n)),'NATURAL1')),equal(domain($(arr)),interval(1,$(n))))"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi)))),member($(arr),partial_function(interval(1,$(n)),'NATURAL1')),equal(domain($(arr)),interval(1,$(n)))],member($(mxi),domain($(arr))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],not_equal(range($(arr)),empty_set),success(2))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "eq",
      "params": {
        "para1": "lr",
        "para2": "domain($(arr))",
        "para3": "interval(1,$(n))"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi)))),member($(arr),partial_function(interval(1,$(n)),'NATURAL1'))],member($(mxi),interval(1,$(n))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],not_equal(range($(arr)),empty_set),success(2))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "hyp",
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],not_equal(range($(arr)),empty_set),success(2)),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'SIMP_NOTEQUAL'"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],negation(equal(range($(arr)),empty_set)),success(2)),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'DEF_SPECIAL_NOT_EQUAL'"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],exists([$(x)],member($(x),range($(arr)))),success(2)),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "exists_inst",
      "params": {
        "Inst": "'arr(1)'"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member(1,domain($(arr))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member(function($(arr),1),range($(arr))),success(2)))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'DERIV_DOM_TOTALREL'(interval(1,$(n)))"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member(1,interval(1,$(n))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member(function($(arr),1),range($(arr))),success(2)))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'DEF_IN_UPTO'"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],conjunct(less_equal(1,1),less_equal(1,$(n))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member(function($(arr),1),range($(arr))),success(2)))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'SIMP_LIT_LE'"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],conjunct(truth,less_equal(1,$(n))),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member(function($(arr),1),range($(arr))),success(2)))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'SIMP_SPECIAL_AND_BTRUE'"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],less_equal(1,$(n)),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member(function($(arr),1),range($(arr))),success(2)))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_hyp",
      "params": {
        "para1": "'DEF_IN_NATURAL1'",
        "para2": "member($(n),'NATURAL1')"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),less_equal(1,$(n)),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],less_equal(1,$(n)),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member(function($(arr),1),range($(arr))),success(2)))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "hyp",
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member($(arr),partial_function('INTEGER','INTEGER')),sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member(function($(arr),1),range($(arr))),success(2))),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "fun_goal",
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member(function($(arr),1),range($(arr))),success(2)),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'DEF_IN_RAN'"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],exists([$(x)],member(couple($(x),function($(arr),1)),$(arr))),success(2)),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "exists_inst",
      "params": {
        "Inst": "'1'"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],member(couple(1,function($(arr),1)),$(arr)),success(2)),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "simplify_goal",
      "params": {
        "para1": "'SIMP_IN_FUNIMAGE'"
      },
      "destState": {
        "xtl_state": "state(sequent([member($(arr),total_function(interval(1,$(n)),'NATURAL1')),member($(mxi),interval(1,$(n))),member($(n),'NATURAL1'),forall([$(j)],member($(j),interval(1,$(n))),less_equal(function($(arr),$(j)),function($(arr),$(mxi))))],truth,success(2)),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),integer,[])]),rawsets([]),des_hyps([])])."
      }
    },
    {
      "name": "true_goal",
      "destState": {
        "xtl_state": "state(success(2),[ids_types([b(identifier(arr),set(couple(integer,integer)),[]),b(identifier(mxi),integer,[]),b(identifier(n),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-26T13:56:43.241223Z",
    "creator": "traceReplay",
    "proB2KernelVersion": "4.15.2-SNAPSHOT",
    "proBCliVersion": "1.16.0-nightly",
    "modelName": "find_ctx"
  }
}