(* generated by Ott 0.23 from: caml_typedef_reduction.ott caml_typedef_typing.ott caml_typedef_syntax.ott *)
open import Pervasives

type index = nat (* index variables (subscripts) *)
type ident = string
type integer_literal = integer
type float_literal = nat
type char_literal = nat
type string_literal = string
type infix_symbol = string
type prefix_symbol = string
type location = nat (* store locations (not in the source syntax) *)
type lowercase_ident = string
type capitalized_ident = string

type typeconstr_name = 
 | TCN_id of lowercase_ident


type typeconstr =  (* type constructors: named, and built-in *)
 | TC_name of typeconstr_name
 | TC_int
 | TC_char
 | TC_string
 | TC_float
 | TC_bool
 | TC_unit
 | TC_exn
 | TC_list
 | TC_option
 | TC_ref


type idx = nat


type typevar = 
 | TV_ident of ident


type constr_name = 
 | CN_id of capitalized_ident


type typexpr = 
 | TE_var of typevar
 | TE_idxvar of idx * idx (* de Bruijn represenataion of type variables.  idx allows each binder (\ie a polymorphic $\ottkw{let}$) to introduce an arbitrary number of binders *)
 | TE_any
 | TE_arrow of typexpr * typexpr
 | TE_tuple of list typexpr
 | TE_constr of list typexpr * typeconstr


type field_name = 
 | FN_id of lowercase_ident


type infix_op = 
 | IO_symbol of infix_symbol
 | IO_star
 | IO_equal
 | IO_colonequal


type constr_decl = 
 | CD_nullary of constr_name
 | CD_nary of constr_name * list typexpr


type field_decl = 
 | FD_immutable of field_name * typexpr


type operator_name = 
 | ON_symbol of prefix_symbol
 | ON_infix of infix_op


type constr =  (* constructors: named, and built-in (including exceptions) *)
 | C_name of constr_name
 | C_invalidargument
 | C_notfound
 | C_assertfailure
 | C_matchfailure
 | C_div_by_0
 | C_none
 | C_some


type intn = integer


type type_param = 
 | TP_var of typevar


type type_representation = 
 | TR_variant of list constr_decl
 | TR_record of list field_decl


type type_equation = 
 | TE_te of typexpr


type value_name = 
 | VN_id of lowercase_ident
 | VN_op of operator_name


type fieldl = 
 | F_name of field_name


type constantl = 
 | CONST_int of intn
 | CONST_float of float_literal
 | CONST_char of char_literal
 | CONST_string of string_literal
 | CONST_constr of constr
 | CONST_false
 | CONST_true
 | CONST_nil
 | CONST_unit


type type_params_opt = 
 | TPS_nary of list type_param


type type_information = 
 | TI_eq of type_equation
 | TI_def of type_representation


type patternl = 
 | P_var of value_name
 | P_any
 | P_constant of constantl
 | P_alias of patternl * value_name
 | P_typed of patternl * typexpr
 | P_or of patternl * patternl
 | P_construct of constr * list patternl
 | P_construct_any of constr
 | P_tuple of list patternl
 | P_record of list (fieldl * patternl)
 | P_cons of patternl * patternl


type unary_prim =  (* primitive functions with one argument *)
 | Uprim_raise
 | Uprim_not
 | Uprim_minus
 | Uprim_ref
 | Uprim_deref


type binary_prim =  (* primitive functions with two arguments *)
 | Bprim_equal
 | Bprim_plus
 | Bprim_minus
 | Bprim_times
 | Bprim_div
 | Bprim_assign


type for_dirn = 
 | FD_upto
 | FD_downto


type typedef = 
 | TD_td of type_params_opt * typeconstr_name * type_information


type exception_definition = 
 | ED_def of constr_decl


type expr = 
 | Expr_uprim of unary_prim (* a unary primitive function value *)
 | Expr_bprim of binary_prim (* a binary primitive function value *)
 | Expr_ident of value_name
 | Expr_constant of constantl
 | Expr_typed of expr * typexpr
 | Expr_tuple of list expr
 | Expr_construct of constr * list expr (* potentially empty constructors to work around ott parser restriction *)
 | Expr_cons of expr * expr
 | Expr_record of list (fieldl * expr)
 | Expr_override of expr * list (fieldl * expr)
 | Expr_apply of expr * expr
 | Expr_and of expr * expr
 | Expr_or of expr * expr
 | Expr_field of expr * fieldl
 | Expr_ifthenelse of expr * expr * expr
 | Expr_while of expr * expr
 | Expr_for of value_name * expr * for_dirn * expr * expr
 | Expr_sequence of expr * expr
 | Expr_match of expr * pattern_matching
 | Expr_function of pattern_matching
 | Expr_try of expr * pattern_matching
 | Expr_let of let_binding * expr (* omitting multiple bindings, i.e.\ $\ottkw{and}$ *)
 | Expr_letrec of letrec_bindings * expr
 | Expr_assert of expr
 | Expr_location of location

and pattern_matching = 
 | PM_pm of list pat_exp

and pat_exp = 
 | PE_inj of patternl * expr

and let_binding = 
 | LB_simple of patternl * expr

and letrec_bindings = 
 | LRBs_inj of list letrec_binding

and letrec_binding = 
 | LRB_simple of value_name * pattern_matching


type type_definition = 
 | TDF_tdf of list typedef (* potentially empty definitions to work around Ott parser restrictions *)


type definition = 
 | D_let of let_binding (* omitting multiple bindings, i.e.\ $\ottkw{and}$ *)
 | D_letrec of letrec_bindings
 | D_type of type_definition
 | D_exception of exception_definition


type kind = nat


type typexprs = 
 | Typexprs_inj of list typexpr


type typescheme = 
 | TS_forall of typexpr


type trans_label =  (* reduction label (denoting a side effect) *)
 | Lab_nil
 | Lab_alloc of expr * location
 | Lab_deref of location * expr
 | Lab_assign of location * expr


type definitions = 
 | Ds_nil
 | Ds_cons of definition * definitions


type name =  (* environment lookup key *)
 | Name_tv
 | Name_vn of value_name
 | Name_cn of constr_name
 | Name_tcn of typeconstr_name
 | Name_fn of field_name
 | Name_l of location


type environment_binding = 
 | EB_tv (* type variable *)
 | EB_vn of value_name * typescheme (* value binding *)
 | EB_cc of constr_name * typeconstr (* constant constructor *)
 | EB_pc of constr_name * type_params_opt * typexprs * typeconstr (* parameterised constructor *)
 | EB_fn of field_name * type_params_opt * typeconstr_name * typexpr (* field name a record destructor *)
 | EB_td of typeconstr_name * kind (* type name, bound to a fresh type *)
 | EB_tr of typeconstr_name * kind * list field_name (* type name which is a record type definition *)
 | EB_ta of type_params_opt * typeconstr_name * typexpr (* type name which is an abbreviation *)
 | EB_l of location * typexpr (* location (memory cell) *)


type labelled_arrow = trans_label


type program = 
 | Prog_defs of definitions
 | Prog_raise of expr


type store = (list (location*expr))


type names = (list name)


type environment = (list environment_binding)


type Tsigma = list (typevar*typexpr)


type substs_x =  (* substitutions of expressions for variables *)
 | Substs_x_xs of list (value_name * expr)


type value_path = 
 | VP_name of value_name

let aux_constr_names_constr_decl_of_constr_decl (constr_decl5:constr_decl) : list constr_name =
  match constr_decl5 with
   | (CD_nullary constr_name) -> [constr_name]
   | (CD_nary constr_name (typexpr_list)) -> [constr_name]
  end

let aux_constr_names_type_representation_of_type_representation (type_representation5:type_representation) : list constr_name =
  match type_representation5 with
   | (TR_variant (constr_decl_list)) ->  (List.concat (List.map aux_constr_names_constr_decl_of_constr_decl (constr_decl_list)))
   | (TR_record (field_decl_list)) -> []
  end

let aux_constr_names_type_information_of_type_information (type_information5:type_information) : list constr_name =
  match type_information5 with
   | (TI_eq type_equation) -> []
   | (TI_def type_representation) -> (aux_constr_names_type_representation_of_type_representation type_representation)
  end

let rec aux_xs_patternl_of_patternl (pat5:patternl) : list value_name =
  match pat5 with
   | (P_var value_name) -> [value_name]
   | P_any -> []
   | (P_constant constantl) -> []
   | (P_alias patternl value_name) -> (aux_xs_patternl_of_patternl patternl) ++ [value_name]
   | (P_typed patternl typexpr) -> (aux_xs_patternl_of_patternl patternl)
   | (P_or patternl1 patternl2) -> (aux_xs_patternl_of_patternl patternl1)
   | (P_construct constr (patternl_list)) ->  (List.concat (List.map aux_xs_patternl_of_patternl (patternl_list)))
   | (P_construct_any constr) -> []
   | (P_tuple (patternl_list)) ->  (List.concat (List.map aux_xs_patternl_of_patternl (patternl_list)))
   | (P_record (fieldl_patternl_list)) ->  (List.concat (List.map aux_xs_patternl_of_patternl ((List.map (fun (fieldl_,patternl_) -> patternl_) fieldl_patternl_list))))
   | (P_cons patternl1 patternl2) -> (aux_xs_patternl_of_patternl patternl1) ++ (aux_xs_patternl_of_patternl patternl2)
  end

let aux_xs_letrec_binding_of_letrec_binding (letrec_binding5:letrec_binding) : list value_name =
  match letrec_binding5 with
   | (LRB_simple value_name pattern_matching) -> [value_name]
  end

let aux_field_names_field_decl_of_field_decl (field_decl5:field_decl) : list field_name =
  match field_decl5 with
   | (FD_immutable field_name typexpr) -> [field_name]
  end

let aux_constr_names_typedef_of_typedef (typedef5:typedef) : list constr_name =
  match typedef5 with
   | (TD_td type_params_opt typeconstr_name type_information) -> (aux_constr_names_type_information_of_type_information type_information)
  end

let aux_typevars_type_param_of_type_param (tp5:type_param) : list typevar =
  match tp5 with
   | (TP_var typevar) -> [typevar]
  end

let aux_type_names_typedef_of_typedef (typedef5:typedef) : list typeconstr_name =
  match typedef5 with
   | (TD_td type_params_opt typeconstr_name type_information) -> [typeconstr_name]
  end

let aux_xs_let_binding_of_let_binding (let_binding5:let_binding) : list value_name =
  match let_binding5 with
   | (LB_simple patternl expr) -> (aux_xs_patternl_of_patternl patternl)
  end

let aux_xs_letrec_bindings_of_letrec_bindings (letrec_bindings5:letrec_bindings) : list value_name =
  match letrec_bindings5 with
   | (LRBs_inj (letrec_binding_list)) ->  (List.concat (List.map aux_xs_letrec_binding_of_letrec_binding (letrec_binding_list)))
  end

let aux_field_names_type_representation_of_type_representation (type_representation5:type_representation) : list field_name =
  match type_representation5 with
   | (TR_variant (constr_decl_list)) -> []
   | (TR_record (field_decl_list)) ->  (List.concat (List.map aux_field_names_field_decl_of_field_decl (field_decl_list)))
  end

let aux_constr_names_type_definition_of_type_definition (type_definition5:type_definition) : list constr_name =
  match type_definition5 with
   | (TDF_tdf (typedef_list)) ->  (List.concat (List.map aux_constr_names_typedef_of_typedef (typedef_list)))
  end

let aux_typevars_type_params_opt_of_type_params_opt (type_params_opt5:type_params_opt) : list typevar =
  match type_params_opt5 with
   | (TPS_nary (type_param_list)) ->  (List.concat (List.map aux_typevars_type_param_of_type_param (type_param_list)))
  end

let aux_type_names_type_definition_of_type_definition (type_definition5:type_definition) : list typeconstr_name =
  match type_definition5 with
   | (TDF_tdf (typedef_list)) ->  (List.concat (List.map aux_type_names_typedef_of_typedef (typedef_list)))
  end

let aux_xs_definition_of_definition (d5:definition) : list value_name =
  match d5 with
   | (D_let let_binding) -> (aux_xs_let_binding_of_let_binding let_binding)
   | (D_letrec letrec_bindings) -> (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings)
   | (D_type type_definition) -> []
   | (D_exception exception_definition) -> []
  end

let aux_field_names_type_information_of_type_information (type_information5:type_information) : list field_name =
  match type_information5 with
   | (TI_eq type_equation) -> []
   | (TI_def type_representation) -> (aux_field_names_type_representation_of_type_representation type_representation)
  end


(** subrules *)
let is_binary_prim_app_value_of_expr (e5:expr) : bool =
  match e5 with
   | (Expr_uprim unary_prim) -> false
   | (Expr_bprim binary_prim) -> (true)
   | (Expr_ident value_name) -> false
   | (Expr_constant constantl) -> false
   | (Expr_typed expr typexpr) -> false
   | (Expr_tuple (expr_list)) -> false
   | (Expr_construct constr (expr_list)) -> false
   | (Expr_cons expr1 expr2) -> false
   | (Expr_record (fieldl_expr_list)) -> false
   | (Expr_override expr (fieldl_expr_list)) -> false
   | (Expr_apply expr1 expr2) -> false
   | (Expr_and expr1 expr2) -> false
   | (Expr_or expr1 expr2) -> false
   | (Expr_field expr fieldl) -> false
   | (Expr_ifthenelse expr0 expr1 expr2) -> false
   | (Expr_while expr1 expr2) -> false
   | (Expr_for x expr1 for_dirn expr2 expr3) -> false
   | (Expr_sequence expr1 expr2) -> false
   | (Expr_match expr pattern_matching) -> false
   | (Expr_function pattern_matching) -> false
   | (Expr_try expr pattern_matching) -> false
   | (Expr_let let_binding expr) -> false
   | (Expr_letrec letrec_bindings expr) -> false
   | (Expr_assert expr) -> false
   | (Expr_location location) -> false
  end

let is_definition_value_of_definition (d5:definition) : bool =
  match d5 with
   | (D_let let_binding) -> false
   | (D_letrec letrec_bindings) -> false
   | (D_type type_definition) -> (true)
   | (D_exception exception_definition) -> (true)
  end

let rec is_value_of_expr (e5:expr) : bool =
  match e5 with
   | (Expr_uprim unary_prim) -> (true)
   | (Expr_bprim binary_prim) -> (true)
   | (Expr_ident value_name) -> false
   | (Expr_constant constantl) -> (true)
   | (Expr_typed expr typexpr) -> false
   | (Expr_tuple (expr_list)) -> ( (List.all (fun expr_ -> (is_value_of_expr expr_)) expr_list))
   | (Expr_construct constr (expr_list)) -> ( (List.all (fun expr_ -> (is_value_of_expr expr_)) expr_list))
   | (Expr_cons expr1 expr2) -> ((is_value_of_expr expr1) && (is_value_of_expr expr2))
   | (Expr_record (fieldl_expr_list)) -> ( (List.all (fun (fieldl_,expr_) -> (is_value_of_expr expr_)) fieldl_expr_list))
   | (Expr_override expr (fieldl_expr_list)) -> false
   | (Expr_apply expr1 expr2) -> ((is_binary_prim_app_value_of_expr expr1) && (is_value_of_expr expr2))
   | (Expr_and expr1 expr2) -> false
   | (Expr_or expr1 expr2) -> false
   | (Expr_field expr fieldl) -> false
   | (Expr_ifthenelse expr0 expr1 expr2) -> false
   | (Expr_while expr1 expr2) -> false
   | (Expr_for x expr1 for_dirn expr2 expr3) -> false
   | (Expr_sequence expr1 expr2) -> false
   | (Expr_match expr pattern_matching) -> false
   | (Expr_function pattern_matching) -> (true)
   | (Expr_try expr pattern_matching) -> false
   | (Expr_let let_binding expr) -> false
   | (Expr_letrec letrec_bindings expr) -> false
   | (Expr_assert expr) -> false
   | (Expr_location location) -> (true)
  end

let rec is_non_expansive_of_expr (e5:expr) : bool =
  match e5 with
   | (Expr_uprim unary_prim) -> (true)
   | (Expr_bprim binary_prim) -> (true)
   | (Expr_ident value_name) -> (true)
   | (Expr_constant constantl) -> (true)
   | (Expr_typed expr typexpr) -> ((is_non_expansive_of_expr expr))
   | (Expr_tuple (expr_list)) -> ( (List.all (fun expr_ -> (is_non_expansive_of_expr expr_)) expr_list))
   | (Expr_construct constr (expr_list)) -> ( (List.all (fun expr_ -> (is_non_expansive_of_expr expr_)) expr_list))
   | (Expr_cons expr1 expr2) -> ((is_non_expansive_of_expr expr1) && (is_non_expansive_of_expr expr2))
   | (Expr_record (fieldl_expr_list)) -> ( (List.all (fun (fieldl_,expr_) -> (is_non_expansive_of_expr expr_)) fieldl_expr_list))
   | (Expr_override expr (fieldl_expr_list)) -> false
   | (Expr_apply expr1 expr2) -> ((is_binary_prim_app_value_of_expr expr1) && (is_non_expansive_of_expr expr2))
   | (Expr_and expr1 expr2) -> false
   | (Expr_or expr1 expr2) -> false
   | (Expr_field expr fieldl) -> false
   | (Expr_ifthenelse expr0 expr1 expr2) -> false
   | (Expr_while expr1 expr2) -> false
   | (Expr_for x expr1 for_dirn expr2 expr3) -> false
   | (Expr_sequence expr1 expr2) -> false
   | (Expr_match expr pattern_matching) -> false
   | (Expr_function pattern_matching) -> (true)
   | (Expr_try expr pattern_matching) -> false
   | (Expr_let let_binding expr) -> false
   | (Expr_letrec letrec_bindings expr) -> ((is_non_expansive_of_expr expr))
   | (Expr_assert expr) -> false
   | (Expr_location location) -> (true)
  end

let rec is_src_typexpr_of_typexpr (t_5:typexpr) : bool =
  match t_5 with
   | (TE_var typevar) -> (true)
   | (TE_idxvar idx num) -> false
   | TE_any -> (true)
   | (TE_arrow typexpr1 typexpr2) -> ((is_src_typexpr_of_typexpr typexpr1) && (is_src_typexpr_of_typexpr typexpr2))
   | (TE_tuple (typexpr_list)) -> ( (List.all (fun typexpr_ -> (is_src_typexpr_of_typexpr typexpr_)) typexpr_list))
   | (TE_constr (typexpr_list) typeconstr) -> ( (List.all (fun typexpr_ -> (is_src_typexpr_of_typexpr typexpr_)) typexpr_list))
  end

let rec is_definitions_value_of_definitions (ds5:definitions) : bool =
  match ds5 with
   | Ds_nil -> (true)
   | (Ds_cons definition definitions) -> ((is_definition_value_of_definition definition) && (is_definitions_value_of_definitions definitions))
  end

let is_trans_label_of_trans_label (L5:trans_label) : bool =
  match L5 with
   | Lab_nil -> (true)
   | (Lab_alloc v location) -> ((is_value_of_expr v))
   | (Lab_deref location v) -> ((is_value_of_expr v))
   | (Lab_assign location v) -> ((is_value_of_expr v))
  end

(** library functions *)
let rec list_minus (l1:list 'a) (l2:list 'a) : list 'a=
  match l1 with
  | [] -> []
  | h::t -> if (List.elem h l2) then list_minus t l2 else h::(list_minus t l2)
  end


(** free variables *)
let rec ftv_typexpr (t_5:typexpr) :  list typevar =
  match t_5 with
   | (TE_var typevar) -> [typevar]
   | (TE_idxvar idx num) -> []
   | TE_any -> []
   | (TE_arrow typexpr1 typexpr2) -> (ftv_typexpr typexpr1) ++ (ftv_typexpr typexpr2)
   | (TE_tuple (typexpr_list)) -> (List.concat (List.map (fun typexpr_ -> (ftv_typexpr typexpr_)) typexpr_list))
   | (TE_constr (typexpr_list) typeconstr) -> (List.concat (List.map (fun typexpr_ -> (ftv_typexpr typexpr_)) typexpr_list))
  end

let ftv_constr_decl (constr_decl5:constr_decl) :  list typevar =
  match constr_decl5 with
   | (CD_nullary constr_name) -> []
   | (CD_nary constr_name (typexpr_list)) -> (List.concat (List.map (fun typexpr_ -> (ftv_typexpr typexpr_)) typexpr_list))
  end

let ftv_field_decl (field_decl5:field_decl) :  list typevar =
  match field_decl5 with
   | (FD_immutable field_name typexpr) -> (ftv_typexpr typexpr)
  end

let ftv_type_equation (type_equation5:type_equation) :  list typevar =
  match type_equation5 with
   | (TE_te typexpr) -> (ftv_typexpr typexpr)
  end

let ftv_type_representation (type_representation5:type_representation) :  list typevar =
  match type_representation5 with
   | (TR_variant (constr_decl_list)) -> (List.concat (List.map (fun constr_decl_ -> (ftv_constr_decl constr_decl_)) constr_decl_list))
   | (TR_record (field_decl_list)) -> (List.concat (List.map (fun field_decl_ -> (ftv_field_decl field_decl_)) field_decl_list))
  end

let ftv_type_information (type_information5:type_information) :  list typevar =
  match type_information5 with
   | (TI_eq type_equation) -> (ftv_type_equation type_equation)
   | (TI_def type_representation) -> (ftv_type_representation type_representation)
  end

let rec ftv_patternl (pat5:patternl) :  list typevar =
  match pat5 with
   | (P_var value_name) -> []
   | P_any -> []
   | (P_constant constantl) -> []
   | (P_alias patternl value_name) -> (ftv_patternl patternl)
   | (P_typed patternl typexpr) -> (ftv_patternl patternl) ++ (ftv_typexpr typexpr)
   | (P_or patternl1 patternl2) -> (ftv_patternl patternl1) ++ (ftv_patternl patternl2)
   | (P_construct constr (patternl_list)) -> (List.concat (List.map (fun patternl_ -> (ftv_patternl patternl_)) patternl_list))
   | (P_construct_any constr) -> []
   | (P_tuple (patternl_list)) -> (List.concat (List.map (fun patternl_ -> (ftv_patternl patternl_)) patternl_list))
   | (P_record (fieldl_patternl_list)) -> (List.concat (List.map (fun (fieldl_,patternl_) -> (ftv_patternl patternl_)) fieldl_patternl_list))
   | (P_cons patternl1 patternl2) -> (ftv_patternl patternl1) ++ (ftv_patternl patternl2)
  end

let ftv_typedef (typedef5:typedef) :  list typevar =
  match typedef5 with
   | (TD_td type_params_opt typeconstr_name type_information) -> (list_minus (ftv_type_information type_information) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))
  end

let rec ftv_letrec_binding (letrec_binding5:letrec_binding) :  list typevar =
  match letrec_binding5 with
   | (LRB_simple value_name pattern_matching) -> (ftv_pattern_matching pattern_matching)
  end
and
ftv_letrec_bindings (letrec_bindings5:letrec_bindings) :  list typevar =
  match letrec_bindings5 with
   | (LRBs_inj (letrec_binding_list)) -> (List.concat (List.map (fun letrec_binding_ -> (ftv_letrec_binding letrec_binding_)) letrec_binding_list))
  end
and
ftv_let_binding (let_binding5:let_binding) :  list typevar =
  match let_binding5 with
   | (LB_simple patternl expr) -> (ftv_patternl patternl) ++ (ftv_expr expr)
  end
and
ftv_pat_exp (pat_exp5:pat_exp) :  list typevar =
  match pat_exp5 with
   | (PE_inj patternl expr) -> (ftv_patternl patternl) ++ (ftv_expr expr)
  end
and
ftv_pattern_matching (pm5:pattern_matching) :  list typevar =
  match pm5 with
   | (PM_pm (pat_exp_list)) -> (List.concat (List.map (fun pat_exp_ -> (ftv_pat_exp pat_exp_)) pat_exp_list))
  end
and
ftv_expr (e5:expr) :  list typevar =
  match e5 with
   | (Expr_uprim unary_prim) -> []
   | (Expr_bprim binary_prim) -> []
   | (Expr_ident value_name) -> []
   | (Expr_constant constantl) -> []
   | (Expr_typed expr typexpr) -> (ftv_expr expr) ++ (ftv_typexpr typexpr)
   | (Expr_tuple (expr_list)) -> (List.concat (List.map (fun expr_ -> (ftv_expr expr_)) expr_list))
   | (Expr_construct constr (expr_list)) -> (List.concat (List.map (fun expr_ -> (ftv_expr expr_)) expr_list))
   | (Expr_cons expr1 expr2) -> (ftv_expr expr1) ++ (ftv_expr expr2)
   | (Expr_record (fieldl_expr_list)) -> (List.concat (List.map (fun (fieldl_,expr_) -> (ftv_expr expr_)) fieldl_expr_list))
   | (Expr_override expr (fieldl_expr_list)) -> (ftv_expr expr) ++ (List.concat (List.map (fun (fieldl_,expr_) -> (ftv_expr expr_)) fieldl_expr_list))
   | (Expr_apply expr1 expr2) -> (ftv_expr expr1) ++ (ftv_expr expr2)
   | (Expr_and expr1 expr2) -> (ftv_expr expr1) ++ (ftv_expr expr2)
   | (Expr_or expr1 expr2) -> (ftv_expr expr1) ++ (ftv_expr expr2)
   | (Expr_field expr fieldl) -> (ftv_expr expr)
   | (Expr_ifthenelse expr0 expr1 expr2) -> (ftv_expr expr0) ++ (ftv_expr expr1) ++ (ftv_expr expr2)
   | (Expr_while expr1 expr2) -> (ftv_expr expr1) ++ (ftv_expr expr2)
   | (Expr_for x expr1 for_dirn expr2 expr3) -> (ftv_expr expr1) ++ (ftv_expr expr2) ++ (ftv_expr expr3)
   | (Expr_sequence expr1 expr2) -> (ftv_expr expr1) ++ (ftv_expr expr2)
   | (Expr_match expr pattern_matching) -> (ftv_expr expr) ++ (ftv_pattern_matching pattern_matching)
   | (Expr_function pattern_matching) -> (ftv_pattern_matching pattern_matching)
   | (Expr_try expr pattern_matching) -> (ftv_expr expr) ++ (ftv_pattern_matching pattern_matching)
   | (Expr_let let_binding expr) -> (ftv_let_binding let_binding) ++ (ftv_expr expr)
   | (Expr_letrec letrec_bindings expr) -> (ftv_letrec_bindings letrec_bindings) ++ (ftv_expr expr)
   | (Expr_assert expr) -> (ftv_expr expr)
   | (Expr_location location) -> []
  end

let ftv_type_definition (type_definition5:type_definition) :  list typevar =
  match type_definition5 with
   | (TDF_tdf (typedef_list)) -> (List.concat (List.map (fun typedef_ -> (ftv_typedef typedef_)) typedef_list))
  end

let ftv_exception_definition (exception_definition5:exception_definition) :  list typevar =
  match exception_definition5 with
   | (ED_def constr_decl) -> (ftv_constr_decl constr_decl)
  end

let rec fv_letrec_binding (letrec_binding5:letrec_binding) :  list value_name =
  match letrec_binding5 with
   | (LRB_simple value_name pattern_matching) -> (fv_pattern_matching pattern_matching)
  end
and
fv_letrec_bindings (letrec_bindings5:letrec_bindings) :  list value_name =
  match letrec_bindings5 with
   | (LRBs_inj (letrec_binding_list)) -> (List.concat (List.map (fun letrec_binding_ -> (fv_letrec_binding letrec_binding_)) letrec_binding_list))
  end
and
fv_let_binding (let_binding5:let_binding) :  list value_name =
  match let_binding5 with
   | (LB_simple patternl expr) -> (fv_expr expr)
  end
and
fv_pat_exp (pat_exp5:pat_exp) :  list value_name =
  match pat_exp5 with
   | (PE_inj patternl expr) -> (list_minus (fv_expr expr) (aux_xs_patternl_of_patternl patternl))
  end
and
fv_pattern_matching (pm5:pattern_matching) :  list value_name =
  match pm5 with
   | (PM_pm (pat_exp_list)) -> (List.concat (List.map (fun pat_exp_ -> (fv_pat_exp pat_exp_)) pat_exp_list))
  end
and
fv_expr (e5:expr) :  list value_name =
  match e5 with
   | (Expr_uprim unary_prim) -> []
   | (Expr_bprim binary_prim) -> []
   | (Expr_ident value_name) -> [value_name]
   | (Expr_constant constantl) -> []
   | (Expr_typed expr typexpr) -> (fv_expr expr)
   | (Expr_tuple (expr_list)) -> (List.concat (List.map (fun expr_ -> (fv_expr expr_)) expr_list))
   | (Expr_construct constr (expr_list)) -> (List.concat (List.map (fun expr_ -> (fv_expr expr_)) expr_list))
   | (Expr_cons expr1 expr2) -> (fv_expr expr1) ++ (fv_expr expr2)
   | (Expr_record (fieldl_expr_list)) -> (List.concat (List.map (fun (fieldl_,expr_) -> (fv_expr expr_)) fieldl_expr_list))
   | (Expr_override expr (fieldl_expr_list)) -> (fv_expr expr) ++ (List.concat (List.map (fun (fieldl_,expr_) -> (fv_expr expr_)) fieldl_expr_list))
   | (Expr_apply expr1 expr2) -> (fv_expr expr1) ++ (fv_expr expr2)
   | (Expr_and expr1 expr2) -> (fv_expr expr1) ++ (fv_expr expr2)
   | (Expr_or expr1 expr2) -> (fv_expr expr1) ++ (fv_expr expr2)
   | (Expr_field expr fieldl) -> (fv_expr expr)
   | (Expr_ifthenelse expr0 expr1 expr2) -> (fv_expr expr0) ++ (fv_expr expr1) ++ (fv_expr expr2)
   | (Expr_while expr1 expr2) -> (fv_expr expr1) ++ (fv_expr expr2)
   | (Expr_for x expr1 for_dirn expr2 expr3) -> (fv_expr expr1) ++ (fv_expr expr2) ++ (list_minus (fv_expr expr3) [x])
   | (Expr_sequence expr1 expr2) -> (fv_expr expr1) ++ (fv_expr expr2)
   | (Expr_match expr pattern_matching) -> (fv_expr expr) ++ (fv_pattern_matching pattern_matching)
   | (Expr_function pattern_matching) -> (fv_pattern_matching pattern_matching)
   | (Expr_try expr pattern_matching) -> (fv_expr expr) ++ (fv_pattern_matching pattern_matching)
   | (Expr_let let_binding expr) -> (fv_let_binding let_binding) ++ (list_minus (fv_expr expr) (aux_xs_let_binding_of_let_binding let_binding))
   | (Expr_letrec letrec_bindings expr) -> (list_minus (fv_letrec_bindings letrec_bindings) (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings)) ++ (list_minus (fv_expr expr) (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings))
   | (Expr_assert expr) -> (fv_expr expr)
   | (Expr_location location) -> []
  end

let rec fl_letrec_binding (letrec_binding5:letrec_binding) :  list location =
  match letrec_binding5 with
   | (LRB_simple value_name pattern_matching) -> (fl_pattern_matching pattern_matching)
  end
and
fl_letrec_bindings (letrec_bindings5:letrec_bindings) :  list location =
  match letrec_bindings5 with
   | (LRBs_inj (letrec_binding_list)) -> (List.concat (List.map (fun letrec_binding_ -> (fl_letrec_binding letrec_binding_)) letrec_binding_list))
  end
and
fl_let_binding (let_binding5:let_binding) :  list location =
  match let_binding5 with
   | (LB_simple patternl expr) -> (fl_expr expr)
  end
and
fl_pat_exp (pat_exp5:pat_exp) :  list location =
  match pat_exp5 with
   | (PE_inj patternl expr) -> (fl_expr expr)
  end
and
fl_pattern_matching (pm5:pattern_matching) :  list location =
  match pm5 with
   | (PM_pm (pat_exp_list)) -> (List.concat (List.map (fun pat_exp_ -> (fl_pat_exp pat_exp_)) pat_exp_list))
  end
and
fl_expr (e5:expr) :  list location =
  match e5 with
   | (Expr_uprim unary_prim) -> []
   | (Expr_bprim binary_prim) -> []
   | (Expr_ident value_name) -> []
   | (Expr_constant constantl) -> []
   | (Expr_typed expr typexpr) -> (fl_expr expr)
   | (Expr_tuple (expr_list)) -> (List.concat (List.map (fun expr_ -> (fl_expr expr_)) expr_list))
   | (Expr_construct constr (expr_list)) -> (List.concat (List.map (fun expr_ -> (fl_expr expr_)) expr_list))
   | (Expr_cons expr1 expr2) -> (fl_expr expr1) ++ (fl_expr expr2)
   | (Expr_record (fieldl_expr_list)) -> (List.concat (List.map (fun (fieldl_,expr_) -> (fl_expr expr_)) fieldl_expr_list))
   | (Expr_override expr (fieldl_expr_list)) -> (fl_expr expr) ++ (List.concat (List.map (fun (fieldl_,expr_) -> (fl_expr expr_)) fieldl_expr_list))
   | (Expr_apply expr1 expr2) -> (fl_expr expr1) ++ (fl_expr expr2)
   | (Expr_and expr1 expr2) -> (fl_expr expr1) ++ (fl_expr expr2)
   | (Expr_or expr1 expr2) -> (fl_expr expr1) ++ (fl_expr expr2)
   | (Expr_field expr fieldl) -> (fl_expr expr)
   | (Expr_ifthenelse expr0 expr1 expr2) -> (fl_expr expr0) ++ (fl_expr expr1) ++ (fl_expr expr2)
   | (Expr_while expr1 expr2) -> (fl_expr expr1) ++ (fl_expr expr2)
   | (Expr_for x expr1 for_dirn expr2 expr3) -> (fl_expr expr1) ++ (fl_expr expr2) ++ (fl_expr expr3)
   | (Expr_sequence expr1 expr2) -> (fl_expr expr1) ++ (fl_expr expr2)
   | (Expr_match expr pattern_matching) -> (fl_expr expr) ++ (fl_pattern_matching pattern_matching)
   | (Expr_function pattern_matching) -> (fl_pattern_matching pattern_matching)
   | (Expr_try expr pattern_matching) -> (fl_expr expr) ++ (fl_pattern_matching pattern_matching)
   | (Expr_let let_binding expr) -> (fl_let_binding let_binding) ++ (fl_expr expr)
   | (Expr_letrec letrec_bindings expr) -> (fl_letrec_bindings letrec_bindings) ++ (fl_expr expr)
   | (Expr_assert expr) -> (fl_expr expr)
   | (Expr_location location) -> [location]
  end

let ftv_definition (d5:definition) :  list typevar =
  match d5 with
   | (D_let let_binding) -> (ftv_let_binding let_binding)
   | (D_letrec letrec_bindings) -> (ftv_letrec_bindings letrec_bindings)
   | (D_type type_definition) -> (ftv_type_definition type_definition)
   | (D_exception exception_definition) -> (ftv_exception_definition exception_definition)
  end

let fv_definition (d5:definition) :  list value_name =
  match d5 with
   | (D_let let_binding) -> (fv_let_binding let_binding)
   | (D_letrec letrec_bindings) -> (list_minus (fv_letrec_bindings letrec_bindings) (aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings))
   | (D_type type_definition) -> []
   | (D_exception exception_definition) -> []
  end

let fl_definition (d5:definition) :  list location =
  match d5 with
   | (D_let let_binding) -> (fl_let_binding let_binding)
   | (D_letrec letrec_bindings) -> (fl_letrec_bindings letrec_bindings)
   | (D_type type_definition) -> []
   | (D_exception exception_definition) -> []
  end

let rec ftv_definitions (ds5:definitions) :  list typevar =
  match ds5 with
   | Ds_nil -> []
   | (Ds_cons definition definitions) -> (ftv_definition definition) ++ (ftv_definitions definitions)
  end

let ftv_typescheme (ts5:typescheme) :  list typevar =
  match ts5 with
   | (TS_forall typexpr) -> (ftv_typexpr typexpr)
  end

let ftv_typexprs (typexprs5:typexprs) :  list typevar =
  match typexprs5 with
   | (Typexprs_inj (typexpr_list)) -> (List.concat (List.map (fun typexpr_ -> (ftv_typexpr typexpr_)) typexpr_list))
  end

let rec fv_definitions (ds5:definitions) :  list value_name =
  match ds5 with
   | Ds_nil -> []
   | (Ds_cons definition definitions) -> (fv_definition definition) ++ (list_minus (fv_definitions definitions) (aux_xs_definition_of_definition definition))
  end

let rec fl_definitions (ds5:definitions) :  list location =
  match ds5 with
   | Ds_nil -> []
   | (Ds_cons definition definitions) -> (fl_definition definition) ++ (fl_definitions definitions)
  end

let ftv_substs_x (substs_x_5:substs_x) :  list typevar =
  match substs_x_5 with
   | (Substs_x_xs (value_name_expr_list)) -> (List.concat (List.map (fun (value_name_,expr_) -> (ftv_expr expr_)) value_name_expr_list))
  end

let ftv_program (program5:program) :  list typevar =
  match program5 with
   | (Prog_defs definitions) -> (ftv_definitions definitions)
   | (Prog_raise expr) -> (ftv_expr expr)
  end

let ftv_environment_binding (EB5:environment_binding) :  list typevar =
  match EB5 with
   | EB_tv -> []
   | (EB_vn value_name typescheme) -> (ftv_typescheme typescheme)
   | (EB_cc constr_name typeconstr) -> []
   | (EB_pc constr_name type_params_opt typexprs typeconstr) -> (list_minus (ftv_typexprs typexprs) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))
   | (EB_fn field_name type_params_opt typeconstr_name typexpr) -> (list_minus (ftv_typexpr typexpr) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))
   | (EB_td typeconstr_name kind) -> []
   | (EB_tr typeconstr_name kind (field_name_list)) -> []
   | (EB_ta type_params_opt typeconstr_name typexpr) -> (list_minus (ftv_typexpr typexpr) (aux_typevars_type_params_opt_of_type_params_opt type_params_opt))
   | (EB_l location typexpr) -> (ftv_typexpr typexpr)
  end

let ftv_trans_label (L5:trans_label) :  list typevar =
  match L5 with
   | Lab_nil -> []
   | (Lab_alloc v location) -> []
   | (Lab_deref location v) -> []
   | (Lab_assign location v) -> []
  end

let fv_substs_x (substs_x_5:substs_x) :  list value_name =
  match substs_x_5 with
   | (Substs_x_xs (value_name_expr_list)) -> (List.concat (List.map (fun (value_name_,expr_) -> (fv_expr expr_)) value_name_expr_list))
  end

let fv_program (program5:program) :  list value_name =
  match program5 with
   | (Prog_defs definitions) -> (fv_definitions definitions)
   | (Prog_raise expr) -> (fv_expr expr)
  end

let fv_trans_label (L5:trans_label) :  list value_name =
  match L5 with
   | Lab_nil -> []
   | (Lab_alloc v location) -> []
   | (Lab_deref location v) -> []
   | (Lab_assign location v) -> []
  end

let fl_substs_x (substs_x_5:substs_x) :  list location =
  match substs_x_5 with
   | (Substs_x_xs (value_name_expr_list)) -> (List.concat (List.map (fun (value_name_,expr_) -> (fl_expr expr_)) value_name_expr_list))
  end

let fl_program (program5:program) :  list location =
  match program5 with
   | (Prog_defs definitions) -> (fl_definitions definitions)
   | (Prog_raise expr) -> (fl_expr expr)
  end

let fl_trans_label (L5:trans_label) :  list location =
  match L5 with
   | Lab_nil -> []
   | (Lab_alloc v location) -> []
   | (Lab_deref location v) -> []
   | (Lab_assign location v) -> []
  end

(** library functions *)
let rec list_assoc_option x0 xys =
  match xys with
  | [] -> Nothing
  | (x,y)::xys' -> if x0=x then Just y else list_assoc_option x0 xys'
  end


(** substitutions *)
let rec substs_typevar_typexpr (sub: list (typevar*typexpr)) (t__6:typexpr) : typexpr =
  match t__6 with
   | (TE_var typevar) -> (match list_assoc_option typevar sub with | Nothing -> (TE_var typevar)| Just t_5 -> t_5 end)
   | (TE_idxvar idx num) -> TE_idxvar idx num
   | TE_any -> TE_any 
   | (TE_arrow typexpr1 typexpr2) -> TE_arrow (substs_typevar_typexpr sub typexpr1) (substs_typevar_typexpr sub typexpr2)
   | (TE_tuple (typexpr_list)) -> TE_tuple  (List.map (fun typexpr_ -> (substs_typevar_typexpr sub typexpr_)) typexpr_list)
   | (TE_constr (typexpr_list) typeconstr) -> TE_constr  (List.map (fun typexpr_ -> (substs_typevar_typexpr sub typexpr_)) typexpr_list) typeconstr
  end

let substs_typevar_constr_decl (sub: list (typevar*typexpr)) (constr_decl5:constr_decl) : constr_decl =
  match constr_decl5 with
   | (CD_nullary constr_name) -> CD_nullary constr_name
   | (CD_nary constr_name (typexpr_list)) -> CD_nary constr_name  (List.map (fun typexpr_ -> (substs_typevar_typexpr sub typexpr_)) typexpr_list)
  end

let substs_typevar_field_decl (sub: list (typevar*typexpr)) (field_decl5:field_decl) : field_decl =
  match field_decl5 with
   | (FD_immutable field_name typexpr) -> FD_immutable field_name (substs_typevar_typexpr sub typexpr)
  end

let substs_typevar_type_equation (sub: list (typevar*typexpr)) (type_equation5:type_equation) : type_equation =
  match type_equation5 with
   | (TE_te typexpr) -> TE_te (substs_typevar_typexpr sub typexpr)
  end

let substs_typevar_type_representation (sub: list (typevar*typexpr)) (type_representation5:type_representation) : type_representation =
  match type_representation5 with
   | (TR_variant (constr_decl_list)) -> TR_variant  (List.map (fun constr_decl_ -> (substs_typevar_constr_decl sub constr_decl_)) constr_decl_list)
   | (TR_record (field_decl_list)) -> TR_record  (List.map (fun field_decl_ -> (substs_typevar_field_decl sub field_decl_)) field_decl_list)
  end

let substs_typevar_type_information (sub: list (typevar*typexpr)) (type_information5:type_information) : type_information =
  match type_information5 with
   | (TI_eq type_equation) -> TI_eq (substs_typevar_type_equation sub type_equation)
   | (TI_def type_representation) -> TI_def (substs_typevar_type_representation sub type_representation)
  end

let rec substs_typevar_patternl (sub: list (typevar*typexpr)) (pat5:patternl) : patternl =
  match pat5 with
   | (P_var value_name) -> P_var value_name
   | P_any -> P_any 
   | (P_constant constantl) -> P_constant constantl
   | (P_alias patternl value_name) -> P_alias (substs_typevar_patternl sub patternl) value_name
   | (P_typed patternl typexpr) -> P_typed (substs_typevar_patternl sub patternl) (substs_typevar_typexpr sub typexpr)
   | (P_or patternl1 patternl2) -> P_or (substs_typevar_patternl sub patternl1) (substs_typevar_patternl sub patternl2)
   | (P_construct constr (patternl_list)) -> P_construct constr  (List.map (fun patternl_ -> (substs_typevar_patternl sub patternl_)) patternl_list)
   | (P_construct_any constr) -> P_construct_any constr
   | (P_tuple (patternl_list)) -> P_tuple  (List.map (fun patternl_ -> (substs_typevar_patternl sub patternl_)) patternl_list)
   | (P_record (fieldl_patternl_list)) -> P_record  (List.map (fun (fieldl_,patternl_) -> (fieldl_,(substs_typevar_patternl sub patternl_))) fieldl_patternl_list)
   | (P_cons patternl1 patternl2) -> P_cons (substs_typevar_patternl sub patternl1) (substs_typevar_patternl sub patternl2)
  end

let substs_typevar_typedef (sub: list (typevar*typexpr)) (typedef5:typedef) : typedef =
  match typedef5 with
   | (TD_td type_params_opt typeconstr_name type_information) -> TD_td type_params_opt typeconstr_name (substs_typevar_type_information (List.filter (fun (tv5,t5) -> not( List.elem tv5 ((aux_typevars_type_params_opt_of_type_params_opt type_params_opt)))) sub) type_information)
  end

let rec substs_typevar_letrec_binding (sub: list (typevar*typexpr)) (letrec_binding5:letrec_binding) : letrec_binding =
  match letrec_binding5 with
   | (LRB_simple value_name pattern_matching) -> LRB_simple value_name (substs_typevar_pattern_matching sub pattern_matching)
  end
and
substs_typevar_letrec_bindings (sub: list (typevar*typexpr)) (letrec_bindings5:letrec_bindings) : letrec_bindings =
  match letrec_bindings5 with
   | (LRBs_inj (letrec_binding_list)) -> LRBs_inj  (List.map (fun letrec_binding_ -> (substs_typevar_letrec_binding sub letrec_binding_)) letrec_binding_list)
  end
and
substs_typevar_let_binding (sub: list (typevar*typexpr)) (let_binding5:let_binding) : let_binding =
  match let_binding5 with
   | (LB_simple patternl expr) -> LB_simple (substs_typevar_patternl sub patternl) (substs_typevar_expr sub expr)
  end
and
substs_typevar_pat_exp (sub: list (typevar*typexpr)) (pat_exp5:pat_exp) : pat_exp =
  match pat_exp5 with
   | (PE_inj patternl expr) -> PE_inj (substs_typevar_patternl sub patternl) (substs_typevar_expr sub expr)
  end
and
substs_typevar_pattern_matching (sub: list (typevar*typexpr)) (pm5:pattern_matching) : pattern_matching =
  match pm5 with
   | (PM_pm (pat_exp_list)) -> PM_pm  (List.map (fun pat_exp_ -> (substs_typevar_pat_exp sub pat_exp_)) pat_exp_list)
  end
and
substs_typevar_expr (sub: list (typevar*typexpr)) (e5:expr) : expr =
  match e5 with
   | (Expr_uprim unary_prim) -> Expr_uprim unary_prim
   | (Expr_bprim binary_prim) -> Expr_bprim binary_prim
   | (Expr_ident value_name) -> Expr_ident value_name
   | (Expr_constant constantl) -> Expr_constant constantl
   | (Expr_typed expr typexpr) -> Expr_typed (substs_typevar_expr sub expr) (substs_typevar_typexpr sub typexpr)
   | (Expr_tuple (expr_list)) -> Expr_tuple  (List.map (fun expr_ -> (substs_typevar_expr sub expr_)) expr_list)
   | (Expr_construct constr (expr_list)) -> Expr_construct constr  (List.map (fun expr_ -> (substs_typevar_expr sub expr_)) expr_list)
   | (Expr_cons expr1 expr2) -> Expr_cons (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2)
   | (Expr_record (fieldl_expr_list)) -> Expr_record  (List.map (fun (fieldl_,expr_) -> (fieldl_,(substs_typevar_expr sub expr_))) fieldl_expr_list)
   | (Expr_override expr (fieldl_expr_list)) -> Expr_override (substs_typevar_expr sub expr)  (List.map (fun (fieldl_,expr_) -> (fieldl_,(substs_typevar_expr sub expr_))) fieldl_expr_list)
   | (Expr_apply expr1 expr2) -> Expr_apply (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2)
   | (Expr_and expr1 expr2) -> Expr_and (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2)
   | (Expr_or expr1 expr2) -> Expr_or (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2)
   | (Expr_field expr fieldl) -> Expr_field (substs_typevar_expr sub expr) fieldl
   | (Expr_ifthenelse expr0 expr1 expr2) -> Expr_ifthenelse (substs_typevar_expr sub expr0) (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2)
   | (Expr_while expr1 expr2) -> Expr_while (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2)
   | (Expr_for x expr1 for_dirn expr2 expr3) -> Expr_for x (substs_typevar_expr sub expr1) for_dirn (substs_typevar_expr sub expr2) (substs_typevar_expr sub expr3)
   | (Expr_sequence expr1 expr2) -> Expr_sequence (substs_typevar_expr sub expr1) (substs_typevar_expr sub expr2)
   | (Expr_match expr pattern_matching) -> Expr_match (substs_typevar_expr sub expr) (substs_typevar_pattern_matching sub pattern_matching)
   | (Expr_function pattern_matching) -> Expr_function (substs_typevar_pattern_matching sub pattern_matching)
   | (Expr_try expr pattern_matching) -> Expr_try (substs_typevar_expr sub expr) (substs_typevar_pattern_matching sub pattern_matching)
   | (Expr_let let_binding expr) -> Expr_let (substs_typevar_let_binding sub let_binding) (substs_typevar_expr sub expr)
   | (Expr_letrec letrec_bindings expr) -> Expr_letrec (substs_typevar_letrec_bindings sub letrec_bindings) (substs_typevar_expr sub expr)
   | (Expr_assert expr) -> Expr_assert (substs_typevar_expr sub expr)
   | (Expr_location location) -> Expr_location location
  end

let substs_typevar_type_definition (sub: list (typevar*typexpr)) (type_definition5:type_definition) : type_definition =
  match type_definition5 with
   | (TDF_tdf (typedef_list)) -> TDF_tdf  (List.map (fun typedef_ -> (substs_typevar_typedef sub typedef_)) typedef_list)
  end

let substs_typevar_exception_definition (sub: list (typevar*typexpr)) (exception_definition5:exception_definition) : exception_definition =
  match exception_definition5 with
   | (ED_def constr_decl) -> ED_def (substs_typevar_constr_decl sub constr_decl)
  end

let rec substs_value_name_letrec_binding (sub: list (value_name*expr)) (letrec_binding5:letrec_binding) : letrec_binding =
  match letrec_binding5 with
   | (LRB_simple value_name pattern_matching) -> LRB_simple value_name (substs_value_name_pattern_matching sub pattern_matching)
  end
and
substs_value_name_letrec_bindings (sub: list (value_name*expr)) (letrec_bindings5:letrec_bindings) : letrec_bindings =
  match letrec_bindings5 with
   | (LRBs_inj (letrec_binding_list)) -> LRBs_inj  (List.map (fun letrec_binding_ -> (substs_value_name_letrec_binding sub letrec_binding_)) letrec_binding_list)
  end
and
substs_value_name_let_binding (sub: list (value_name*expr)) (let_binding5:let_binding) : let_binding =
  match let_binding5 with
   | (LB_simple patternl expr) -> LB_simple patternl (substs_value_name_expr sub expr)
  end
and
substs_value_name_pat_exp (sub: list (value_name*expr)) (pat_exp5:pat_exp) : pat_exp =
  match pat_exp5 with
   | (PE_inj patternl expr) -> PE_inj patternl (substs_value_name_expr (List.filter (fun (x5,e5) -> not( List.elem x5 ((aux_xs_patternl_of_patternl patternl)))) sub) expr)
  end
and
substs_value_name_pattern_matching (sub: list (value_name*expr)) (pm5:pattern_matching) : pattern_matching =
  match pm5 with
   | (PM_pm (pat_exp_list)) -> PM_pm  (List.map (fun pat_exp_ -> (substs_value_name_pat_exp sub pat_exp_)) pat_exp_list)
  end
and
substs_value_name_expr (sub: list (value_name*expr)) (e_6:expr) : expr =
  match e_6 with
   | (Expr_uprim unary_prim) -> Expr_uprim unary_prim
   | (Expr_bprim binary_prim) -> Expr_bprim binary_prim
   | (Expr_ident value_name) -> (match list_assoc_option value_name sub with | Nothing -> (Expr_ident value_name)| Just e5 -> e5 end)
   | (Expr_constant constantl) -> Expr_constant constantl
   | (Expr_typed expr typexpr) -> Expr_typed (substs_value_name_expr sub expr) typexpr
   | (Expr_tuple (expr_list)) -> Expr_tuple  (List.map (fun expr_ -> (substs_value_name_expr sub expr_)) expr_list)
   | (Expr_construct constr (expr_list)) -> Expr_construct constr  (List.map (fun expr_ -> (substs_value_name_expr sub expr_)) expr_list)
   | (Expr_cons expr1 expr2) -> Expr_cons (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2)
   | (Expr_record (fieldl_expr_list)) -> Expr_record  (List.map (fun (fieldl_,expr_) -> (fieldl_,(substs_value_name_expr sub expr_))) fieldl_expr_list)
   | (Expr_override expr (fieldl_expr_list)) -> Expr_override (substs_value_name_expr sub expr)  (List.map (fun (fieldl_,expr_) -> (fieldl_,(substs_value_name_expr sub expr_))) fieldl_expr_list)
   | (Expr_apply expr1 expr2) -> Expr_apply (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2)
   | (Expr_and expr1 expr2) -> Expr_and (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2)
   | (Expr_or expr1 expr2) -> Expr_or (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2)
   | (Expr_field expr fieldl) -> Expr_field (substs_value_name_expr sub expr) fieldl
   | (Expr_ifthenelse expr0 expr1 expr2) -> Expr_ifthenelse (substs_value_name_expr sub expr0) (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2)
   | (Expr_while expr1 expr2) -> Expr_while (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2)
   | (Expr_for x expr1 for_dirn expr2 expr3) -> Expr_for x (substs_value_name_expr sub expr1) for_dirn (substs_value_name_expr sub expr2) (substs_value_name_expr (List.filter (fun (x5,e5) -> not( List.elem x5 ([x]))) sub) expr3)
   | (Expr_sequence expr1 expr2) -> Expr_sequence (substs_value_name_expr sub expr1) (substs_value_name_expr sub expr2)
   | (Expr_match expr pattern_matching) -> Expr_match (substs_value_name_expr sub expr) (substs_value_name_pattern_matching sub pattern_matching)
   | (Expr_function pattern_matching) -> Expr_function (substs_value_name_pattern_matching sub pattern_matching)
   | (Expr_try expr pattern_matching) -> Expr_try (substs_value_name_expr sub expr) (substs_value_name_pattern_matching sub pattern_matching)
   | (Expr_let let_binding expr) -> Expr_let (substs_value_name_let_binding sub let_binding) (substs_value_name_expr (List.filter (fun (x5,e5) -> not( List.elem x5 ((aux_xs_let_binding_of_let_binding let_binding)))) sub) expr)
   | (Expr_letrec letrec_bindings expr) -> Expr_letrec (substs_value_name_letrec_bindings (List.filter (fun (x5,e5) -> not( List.elem x5 ((aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings)))) sub) letrec_bindings) (substs_value_name_expr (List.filter (fun (x5,e5) -> not( List.elem x5 ((aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings)))) sub) expr)
   | (Expr_assert expr) -> Expr_assert (substs_value_name_expr sub expr)
   | (Expr_location location) -> Expr_location location
  end

let rec subst_value_name_letrec_binding (e5:expr) (x5:value_name) (letrec_binding5:letrec_binding) : letrec_binding =
  match letrec_binding5 with
   | (LRB_simple value_name pattern_matching) -> LRB_simple value_name (subst_value_name_pattern_matching e5 x5 pattern_matching)
  end
and
subst_value_name_letrec_bindings (e5:expr) (x5:value_name) (letrec_bindings5:letrec_bindings) : letrec_bindings =
  match letrec_bindings5 with
   | (LRBs_inj (letrec_binding_list)) -> LRBs_inj  (List.map (fun letrec_binding_ -> (subst_value_name_letrec_binding e5 x5 letrec_binding_)) letrec_binding_list)
  end
and
subst_value_name_let_binding (e5:expr) (x5:value_name) (let_binding5:let_binding) : let_binding =
  match let_binding5 with
   | (LB_simple patternl expr) -> LB_simple patternl (subst_value_name_expr e5 x5 expr)
  end
and
subst_value_name_pat_exp (e5:expr) (x5:value_name) (pat_exp5:pat_exp) : pat_exp =
  match pat_exp5 with
   | (PE_inj patternl expr) -> PE_inj patternl (if  List.elem x5 ((aux_xs_patternl_of_patternl patternl)) then expr else (subst_value_name_expr e5 x5 expr))
  end
and
subst_value_name_pattern_matching (e5:expr) (x5:value_name) (pm5:pattern_matching) : pattern_matching =
  match pm5 with
   | (PM_pm (pat_exp_list)) -> PM_pm  (List.map (fun pat_exp_ -> (subst_value_name_pat_exp e5 x5 pat_exp_)) pat_exp_list)
  end
and
subst_value_name_expr (e5:expr) (x5:value_name) (e_6:expr) : expr =
  match e_6 with
   | (Expr_uprim unary_prim) -> Expr_uprim unary_prim
   | (Expr_bprim binary_prim) -> Expr_bprim binary_prim
   | (Expr_ident value_name) -> (if value_name=x5 then e5 else (Expr_ident value_name))
   | (Expr_constant constantl) -> Expr_constant constantl
   | (Expr_typed expr typexpr) -> Expr_typed (subst_value_name_expr e5 x5 expr) typexpr
   | (Expr_tuple (expr_list)) -> Expr_tuple  (List.map (fun expr_ -> (subst_value_name_expr e5 x5 expr_)) expr_list)
   | (Expr_construct constr (expr_list)) -> Expr_construct constr  (List.map (fun expr_ -> (subst_value_name_expr e5 x5 expr_)) expr_list)
   | (Expr_cons expr1 expr2) -> Expr_cons (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2)
   | (Expr_record (fieldl_expr_list)) -> Expr_record  (List.map (fun (fieldl_,expr_) -> (fieldl_,(subst_value_name_expr e5 x5 expr_))) fieldl_expr_list)
   | (Expr_override expr (fieldl_expr_list)) -> Expr_override (subst_value_name_expr e5 x5 expr)  (List.map (fun (fieldl_,expr_) -> (fieldl_,(subst_value_name_expr e5 x5 expr_))) fieldl_expr_list)
   | (Expr_apply expr1 expr2) -> Expr_apply (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2)
   | (Expr_and expr1 expr2) -> Expr_and (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2)
   | (Expr_or expr1 expr2) -> Expr_or (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2)
   | (Expr_field expr fieldl) -> Expr_field (subst_value_name_expr e5 x5 expr) fieldl
   | (Expr_ifthenelse expr0 expr1 expr2) -> Expr_ifthenelse (subst_value_name_expr e5 x5 expr0) (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2)
   | (Expr_while expr1 expr2) -> Expr_while (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2)
   | (Expr_for x expr1 for_dirn expr2 expr3) -> Expr_for x (subst_value_name_expr e5 x5 expr1) for_dirn (subst_value_name_expr e5 x5 expr2) (if  List.elem x5 ([x]) then expr3 else (subst_value_name_expr e5 x5 expr3))
   | (Expr_sequence expr1 expr2) -> Expr_sequence (subst_value_name_expr e5 x5 expr1) (subst_value_name_expr e5 x5 expr2)
   | (Expr_match expr pattern_matching) -> Expr_match (subst_value_name_expr e5 x5 expr) (subst_value_name_pattern_matching e5 x5 pattern_matching)
   | (Expr_function pattern_matching) -> Expr_function (subst_value_name_pattern_matching e5 x5 pattern_matching)
   | (Expr_try expr pattern_matching) -> Expr_try (subst_value_name_expr e5 x5 expr) (subst_value_name_pattern_matching e5 x5 pattern_matching)
   | (Expr_let let_binding expr) -> Expr_let (subst_value_name_let_binding e5 x5 let_binding) (if  List.elem x5 ((aux_xs_let_binding_of_let_binding let_binding)) then expr else (subst_value_name_expr e5 x5 expr))
   | (Expr_letrec letrec_bindings expr) -> Expr_letrec (if  List.elem x5 ((aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings)) then letrec_bindings else (subst_value_name_letrec_bindings e5 x5 letrec_bindings)) (if  List.elem x5 ((aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings)) then expr else (subst_value_name_expr e5 x5 expr))
   | (Expr_assert expr) -> Expr_assert (subst_value_name_expr e5 x5 expr)
   | (Expr_location location) -> Expr_location location
  end

let substs_typevar_definition (sub: list (typevar*typexpr)) (d5:definition) : definition =
  match d5 with
   | (D_let let_binding) -> D_let (substs_typevar_let_binding sub let_binding)
   | (D_letrec letrec_bindings) -> D_letrec (substs_typevar_letrec_bindings sub letrec_bindings)
   | (D_type type_definition) -> D_type (substs_typevar_type_definition sub type_definition)
   | (D_exception exception_definition) -> D_exception (substs_typevar_exception_definition sub exception_definition)
  end

let substs_value_name_definition (sub: list (value_name*expr)) (d5:definition) : definition =
  match d5 with
   | (D_let let_binding) -> D_let (substs_value_name_let_binding sub let_binding)
   | (D_letrec letrec_bindings) -> D_letrec (substs_value_name_letrec_bindings (List.filter (fun (x5,e5) -> not( List.elem x5 ((aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings)))) sub) letrec_bindings)
   | (D_type type_definition) -> D_type type_definition
   | (D_exception exception_definition) -> D_exception exception_definition
  end

let subst_value_name_definition (e5:expr) (x5:value_name) (d5:definition) : definition =
  match d5 with
   | (D_let let_binding) -> D_let (subst_value_name_let_binding e5 x5 let_binding)
   | (D_letrec letrec_bindings) -> D_letrec (if  List.elem x5 ((aux_xs_letrec_bindings_of_letrec_bindings letrec_bindings)) then letrec_bindings else (subst_value_name_letrec_bindings e5 x5 letrec_bindings))
   | (D_type type_definition) -> D_type type_definition
   | (D_exception exception_definition) -> D_exception exception_definition
  end

let rec substs_typevar_definitions (sub: list (typevar*typexpr)) (ds5:definitions) : definitions =
  match ds5 with
   | Ds_nil -> Ds_nil 
   | (Ds_cons definition definitions) -> Ds_cons (substs_typevar_definition sub definition) (substs_typevar_definitions sub definitions)
  end

let substs_typevar_typescheme (sub: list (typevar*typexpr)) (ts5:typescheme) : typescheme =
  match ts5 with
   | (TS_forall typexpr) -> TS_forall (substs_typevar_typexpr sub typexpr)
  end

let substs_typevar_typexprs (sub: list (typevar*typexpr)) (typexprs5:typexprs) : typexprs =
  match typexprs5 with
   | (Typexprs_inj (typexpr_list)) -> Typexprs_inj  (List.map (fun typexpr_ -> (substs_typevar_typexpr sub typexpr_)) typexpr_list)
  end

let rec substs_value_name_definitions (sub: list (value_name*expr)) (ds5:definitions) : definitions =
  match ds5 with
   | Ds_nil -> Ds_nil 
   | (Ds_cons definition definitions) -> Ds_cons (substs_value_name_definition sub definition) (substs_value_name_definitions (List.filter (fun (x5,e5) -> not( List.elem x5 ((aux_xs_definition_of_definition definition)))) sub) definitions)
  end

let rec subst_value_name_definitions (e5:expr) (x5:value_name) (ds5:definitions) : definitions =
  match ds5 with
   | Ds_nil -> Ds_nil 
   | (Ds_cons definition definitions) -> Ds_cons (subst_value_name_definition e5 x5 definition) (if  List.elem x5 ((aux_xs_definition_of_definition definition)) then definitions else (subst_value_name_definitions e5 x5 definitions))
  end

let substs_typevar_substs_x (sub: list (typevar*typexpr)) (substs_x_5:substs_x) : substs_x =
  match substs_x_5 with
   | (Substs_x_xs (value_name_expr_list)) -> Substs_x_xs  (List.map (fun (value_name_,expr_) -> (value_name_,(substs_typevar_expr sub expr_))) value_name_expr_list)
  end

let substs_typevar_program (sub: list (typevar*typexpr)) (program5:program) : program =
  match program5 with
   | (Prog_defs definitions) -> Prog_defs (substs_typevar_definitions sub definitions)
   | (Prog_raise expr) -> Prog_raise (substs_typevar_expr sub expr)
  end

let substs_typevar_environment_binding (sub: list (typevar*typexpr)) (EB5:environment_binding) : environment_binding =
  match EB5 with
   | EB_tv -> EB_tv 
   | (EB_vn value_name typescheme) -> EB_vn value_name (substs_typevar_typescheme sub typescheme)
   | (EB_cc constr_name typeconstr) -> EB_cc constr_name typeconstr
   | (EB_pc constr_name type_params_opt typexprs typeconstr) -> EB_pc constr_name type_params_opt (substs_typevar_typexprs (List.filter (fun (tv5,t5) -> not( List.elem tv5 ((aux_typevars_type_params_opt_of_type_params_opt type_params_opt)))) sub) typexprs) typeconstr
   | (EB_fn field_name type_params_opt typeconstr_name typexpr) -> EB_fn field_name type_params_opt typeconstr_name (substs_typevar_typexpr (List.filter (fun (tv5,t5) -> not( List.elem tv5 ((aux_typevars_type_params_opt_of_type_params_opt type_params_opt)))) sub) typexpr)
   | (EB_td typeconstr_name kind) -> EB_td typeconstr_name kind
   | (EB_tr typeconstr_name kind (field_name_list)) -> EB_tr typeconstr_name kind field_name_list
   | (EB_ta type_params_opt typeconstr_name typexpr) -> EB_ta type_params_opt typeconstr_name (substs_typevar_typexpr (List.filter (fun (tv5,t5) -> not( List.elem tv5 ((aux_typevars_type_params_opt_of_type_params_opt type_params_opt)))) sub) typexpr)
   | (EB_l location typexpr) -> EB_l location (substs_typevar_typexpr sub typexpr)
  end

let substs_typevar_trans_label (sub: list (typevar*typexpr)) (L5:trans_label) : trans_label =
  match L5 with
   | Lab_nil -> Lab_nil 
   | (Lab_alloc v location) -> Lab_alloc v location
   | (Lab_deref location v) -> Lab_deref location v
   | (Lab_assign location v) -> Lab_assign location v
  end

let substs_value_name_substs_x (sub: list (value_name*expr)) (substs_x_5:substs_x) : substs_x =
  match substs_x_5 with
   | (Substs_x_xs (value_name_expr_list)) -> Substs_x_xs  (List.map (fun (value_name_,expr_) -> (value_name_,(substs_value_name_expr sub expr_))) value_name_expr_list)
  end

let substs_value_name_program (sub: list (value_name*expr)) (program5:program) : program =
  match program5 with
   | (Prog_defs definitions) -> Prog_defs (substs_value_name_definitions sub definitions)
   | (Prog_raise expr) -> Prog_raise (substs_value_name_expr sub expr)
  end

let substs_value_name_trans_label (sub: list (value_name*expr)) (L5:trans_label) : trans_label =
  match L5 with
   | Lab_nil -> Lab_nil 
   | (Lab_alloc v location) -> Lab_alloc v location
   | (Lab_deref location v) -> Lab_deref location v
   | (Lab_assign location v) -> Lab_assign location v
  end

let subst_value_name_substs_x (e5:expr) (x5:value_name) (substs_x_5:substs_x) : substs_x =
  match substs_x_5 with
   | (Substs_x_xs (value_name_expr_list)) -> Substs_x_xs  (List.map (fun (value_name_,expr_) -> (value_name_,(subst_value_name_expr e5 x5 expr_))) value_name_expr_list)
  end

let subst_value_name_program (e5:expr) (x5:value_name) (program5:program) : program =
  match program5 with
   | (Prog_defs definitions) -> Prog_defs (subst_value_name_definitions e5 x5 definitions)
   | (Prog_raise expr) -> Prog_raise (subst_value_name_expr e5 x5 expr)
  end

let subst_value_name_trans_label (e5:expr) (x5:value_name) (L5:trans_label) : trans_label =
  match L5 with
   | Lab_nil -> Lab_nil 
   | (Lab_alloc v location) -> Lab_alloc v location
   | (Lab_deref location v) -> Lab_deref location v
   | (Lab_assign location v) -> Lab_assign location v
  end


let rec list_distinct xs = 
  match xs with
    | [] -> true
    | [x] -> true
    | x::xs -> not(List.elem x xs) && list_distinct xs
  end

(* insert x at all positions into l and return the list of results *)
let rec insert x l = match l with
| [] -> [ [x] ]
| a::m -> (x::l) :: (List.map (fun y -> a::y) (insert x m))
end

(* list of all permutations of l *)
let rec perms l = match l with
| a::m -> List.concat (List.map (insert a) (perms m))
| _ -> [l]
end
(* nb this is very inefficient *)
let rec list_perm xs ys = List.elem xs (perms ys)


let fold_pat pats expr = List.foldr (fun p e -> Expr_function (PM_pm [PE_inj p e])) expr pats

let rec
shiftt m n (TE_var typevar) = TE_var typevar
and
shiftt m n (TE_idxvar idx num) = 
  if (idx < m) then TE_idxvar idx num else TE_idxvar (idx + n) num
and
shiftt m n TE_any = TE_any
and
shiftt m n (TE_arrow typexpr1 typexpr2) =
  TE_arrow (shiftt m n typexpr1) (shiftt m n typexpr2)
and
shiftt m n (TE_tuple typexprs) = TE_tuple (List.map (shiftt m n) typexprs)
and
shiftt m n (TE_constr typexprs tc) = TE_constr (List.map (shiftt m n) typexprs) tc


let shifttes m n (Typexprs_inj tes) = Typexprs_inj (List.map (shiftt m n) tes)

let shiftts m n (TS_forall typexpr) = TS_forall (shiftt (m + 1) n typexpr)

let rec
shiftEB m n EB_tv = EB_tv
and
shiftEB m n (EB_vn value_name typescheme) =
  EB_vn value_name (shiftts m n typescheme)
and
shiftEB m n (EB_cc constr_name typeconstr) = 
  EB_cc constr_name typeconstr
and
shiftEB m n (EB_pc constr_name type_params_opt typexprs typeconstr) =
  EB_pc constr_name type_params_opt (shifttes m n typexprs ) typeconstr
and
shiftEB m n (EB_fn field_name type_params_opt typeconstr_name typexpr) =
  EB_fn field_name type_params_opt typeconstr_name (shiftt m n typexpr)
and
shiftEB m n (EB_td typeconstr_name kind) =
  EB_td typeconstr_name kind
and
shiftEB m n (EB_tr tcn k field_names) = EB_tr tcn k field_names
and
shiftEB m n (EB_ta type_params_opt typeconstr_name typexpr) =
  EB_ta type_params_opt typeconstr_name (shiftt m n typexpr) 
and
shiftEB m n (EB_l location typexpr) = 
  EB_l location (shiftt m n typexpr)

let rec
num_tv [] = (0:nat)
and
num_tv (EB_tv::E) = 1 + num_tv E
and
num_tv (EB::E) = num_tv E

let rec
shiftE m n [] = []
and
shiftE m n (EB::E) = shiftEB (m + num_tv E) n EB::shiftE m n E

let shiftTsig m n Tsig = List.map (fun (tv, t) -> (tv, shiftt m n t)) Tsig

let rec
definitions_snoc Ds_nil d = Ds_cons d Ds_nil
and
definitions_snoc (Ds_cons d ds) d' = Ds_cons d (definitions_snoc ds d')

let rec
remv_tyvar_typexpr (TE_var typevar) = TE_any
and
remv_tyvar_typexpr (TE_idxvar idx num) = TE_idxvar idx num
and
remv_tyvar_typexpr TE_any = TE_any
and
remv_tyvar_typexpr (TE_arrow typexpr1 typexpr2) = 
    TE_arrow (remv_tyvar_typexpr typexpr1) (remv_tyvar_typexpr typexpr2)
and
remv_tyvar_typexpr (TE_tuple (typexpr_list)) =
    TE_tuple (List.map (fun typexpr_ -> (remv_tyvar_typexpr typexpr_)) typexpr_list)
and
remv_tyvar_typexpr (TE_constr (typexpr_list) typeconstr) = 
    TE_constr (List.map (fun typexpr_ -> (remv_tyvar_typexpr typexpr_)) typexpr_list) typeconstr

let rec
remv_tyvar_pattern (P_var value_name) = P_var value_name
and
remv_tyvar_pattern P_any = P_any
and
remv_tyvar_pattern (P_constant constantl) = P_constant constantl
and
remv_tyvar_pattern (P_alias patternl value_name) =
     P_alias (remv_tyvar_pattern patternl) value_name
and 
remv_tyvar_pattern (P_typed patternl typexpr) = 
     P_typed (remv_tyvar_pattern patternl) (remv_tyvar_typexpr typexpr)
and
remv_tyvar_pattern (P_or pattern1 pattern2) = 
     P_or (remv_tyvar_pattern pattern1) (remv_tyvar_pattern pattern2)
and
remv_tyvar_pattern (P_construct constr (pattern_list)) = 
     P_construct constr (List.map (fun pattern_ -> (remv_tyvar_pattern pattern_)) pattern_list)
and
remv_tyvar_pattern (P_construct_any constr) = P_construct_any constr
and
remv_tyvar_pattern (P_tuple (pattern_list)) = 
     P_tuple (List.map (fun pattern_ -> (remv_tyvar_pattern pattern_)) pattern_list)
and
remv_tyvar_pattern (P_record (field_pattern_list)) = 
     P_record (List.map (fun (field_,pattern_) -> (field_,(remv_tyvar_pattern pattern_))) field_pattern_list)
and
remv_tyvar_pattern (P_cons pattern1 pattern2) = 
     P_cons (remv_tyvar_pattern pattern1) (remv_tyvar_pattern pattern2)

let rec
remv_tyvar_letrec_binding (LRB_simple value_name pattern_matching) = 
     LRB_simple value_name (remv_tyvar_pattern_matching pattern_matching)
and
remv_tyvar_letrec_bindings (LRBs_inj (letrec_binding_list)) = 
     LRBs_inj (List.map (fun letrec_binding_ -> (remv_tyvar_letrec_binding letrec_binding_)) letrec_binding_list)
and
remv_tyvar_let_binding (LB_simple patternl expr) = 
     LB_simple (remv_tyvar_pattern patternl) (remv_tyvar_expr expr)
and
remv_tyvar_pat_exp (PE_inj patternl expr) = 
     PE_inj (remv_tyvar_pattern patternl) (remv_tyvar_expr expr)
and
remv_tyvar_pattern_matching (PM_pm (pat_exp_list)) = 
     PM_pm (List.map (fun pat_exp_ -> (remv_tyvar_pat_exp pat_exp_)) pat_exp_list)
and
remv_tyvar_expr (Expr_uprim unary_prim) = Expr_uprim unary_prim
and
remv_tyvar_expr (Expr_bprim binary_prim) = Expr_bprim binary_prim
and
remv_tyvar_expr (Expr_ident value_name) = Expr_ident value_name
and
remv_tyvar_expr (Expr_constant constantl) = Expr_constant constantl
and
remv_tyvar_expr (Expr_typed expr typexpr) = 
     Expr_typed (remv_tyvar_expr expr) (remv_tyvar_typexpr typexpr)
and
remv_tyvar_expr (Expr_tuple (expr_list)) = 
     Expr_tuple (List.map (fun expr_ -> (remv_tyvar_expr expr_)) expr_list)
and
remv_tyvar_expr (Expr_construct constr (expr_list)) =
     Expr_construct constr (List.map (fun expr_ -> (remv_tyvar_expr expr_)) expr_list)
and
remv_tyvar_expr (Expr_cons expr1 expr2) = 
     Expr_cons (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)
and
remv_tyvar_expr (Expr_record (field_expr_list)) = 
     Expr_record (List.map (fun (field_,expr_) -> (field_,(remv_tyvar_expr expr_))) field_expr_list)
and
remv_tyvar_expr (Expr_override expr (field_expr_list)) = 
     Expr_override (remv_tyvar_expr expr) 
                   (List.map (fun (field_,expr_) -> (field_,(remv_tyvar_expr expr_))) field_expr_list)
and
remv_tyvar_expr (Expr_apply expr1 expr2) = 
     Expr_apply (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)
and
remv_tyvar_expr (Expr_and expr1 expr2) = 
     Expr_and (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)
and
remv_tyvar_expr (Expr_or expr1 expr2) = 
     Expr_or (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)
and
remv_tyvar_expr (Expr_field expr fieldl) = Expr_field (remv_tyvar_expr expr) fieldl
and
remv_tyvar_expr (Expr_ifthenelse expr0 expr1 expr2) = 
     Expr_ifthenelse (remv_tyvar_expr expr0) (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)
and
remv_tyvar_expr (Expr_while expr1 expr2) = 
     Expr_while (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)
and
remv_tyvar_expr (Expr_for x expr1 for_dirn expr2 expr3) = 
     Expr_for x (remv_tyvar_expr expr1) for_dirn (remv_tyvar_expr expr2) (remv_tyvar_expr expr3)
and
remv_tyvar_expr (Expr_sequence expr1 expr2) = 
     Expr_sequence (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)
and
remv_tyvar_expr (Expr_match expr pattern_matching) = 
     Expr_match (remv_tyvar_expr expr) (remv_tyvar_pattern_matching pattern_matching)
and
remv_tyvar_expr (Expr_function pattern_matching) = 
     Expr_function (remv_tyvar_pattern_matching pattern_matching)
and
remv_tyvar_expr (Expr_try expr pattern_matching) = 
     Expr_try (remv_tyvar_expr expr) (remv_tyvar_pattern_matching pattern_matching)
and
remv_tyvar_expr (Expr_let let_binding expr) = 
     Expr_let (remv_tyvar_let_binding let_binding) (remv_tyvar_expr expr)
and
remv_tyvar_expr (Expr_letrec letrec_bindings expr) = 
     Expr_letrec (remv_tyvar_letrec_bindings letrec_bindings) (remv_tyvar_expr expr)
and
remv_tyvar_expr (Expr_assert expr) = Expr_assert (remv_tyvar_expr expr)
and
remv_tyvar_expr (Expr_location location) = Expr_location location

 

(** definitions *)
(* defns JdomEB *)
indreln
[JdomEB : environment_binding -> name -> bool witness type JdomEBwitness; check JdomEBcheck; (*genName : input -> output*)]
(* defn domEB *)

JdomEB_type_param: forall .
true
 ==> 
JdomEB EB_tv Name_tv

and
JdomEB_value_name: forall value_name typescheme .
true
 ==> 
JdomEB (EB_vn value_name typescheme) (Name_vn value_name)

and
JdomEB_const_constr_name: forall constr_name typeconstr .
true
 ==> 
JdomEB (EB_cc constr_name typeconstr) (Name_cn constr_name)

and
JdomEB_constr_name: forall t_list constr_name type_params_opt typeconstr .
true
 ==> 
JdomEB (EB_pc constr_name type_params_opt (Typexprs_inj (t_list)) typeconstr) (Name_cn constr_name)

and
JdomEB_opaque_typeconstr_name: forall typeconstr_name kind .
true
 ==> 
JdomEB (EB_td typeconstr_name kind) (Name_tcn typeconstr_name)

and
JdomEB_trans_typeconstr_name: forall type_params_opt typeconstr_name t .
true
 ==> 
JdomEB (EB_ta type_params_opt typeconstr_name t) (Name_tcn typeconstr_name)

and
JdomEB_record_typeconstr_name: forall field_name_list typeconstr_name kind .
true
 ==> 
JdomEB (EB_tr typeconstr_name kind (field_name_list)) (Name_tcn typeconstr_name)

and
JdomEB_record_field_name: forall field_name type_params_opt typeconstr_name typexpr .
true
 ==> 
JdomEB (EB_fn field_name type_params_opt typeconstr_name typexpr) (Name_fn field_name)

and
JdomEB_location: forall location t .
true
 ==> 
JdomEB (EB_l location t) (Name_l location)


(** definitions *)
(* defns JdomE *)
indreln
[JdomE : environment -> names -> bool witness type JdomEwitness; check JdomE_check;]
(* defn domE *)

JdomE_empty: forall .
true
 ==> 
JdomE  []   [] 

and
JdomE_cons: forall name_list E EB name .
(JdomE E  (name_list) ) &&
(JdomEB EB name)
 ==> 
JdomE  ( EB :: E )   ([(name)] ++ name_list) 


(** definitions *)
(* defns Jlookup *)
indreln
[Jlookup_EB : environment -> name -> environment_binding -> bool witness type JlookupEBwitness; check Jlookup_EB_check;]
(* defn EB *)

Jlookup_EB_rec1: forall E EB name EB' name' .
(JdomEB EB name') &&
( (not ( name  =  name' )) ) &&
( (not ( name'  =  Name_tv )) ) &&
(Jlookup_EB E name EB')
 ==> 
Jlookup_EB  ( EB :: E )  name EB'

and
Jlookup_EB_rec2: forall E name EB' .
( (not ( name  =  Name_tv )) ) &&
(Jlookup_EB E name EB')
 ==> 
Jlookup_EB  ( EB_tv :: E )  name  (shiftEB   0     1    EB' ) 

and
Jlookup_EB_head: forall E EB name .
(JdomEB EB name)
 ==> 
Jlookup_EB  ( EB :: E )  name EB


(** definitions *)
(* defns Jidx *)
indreln
[Jidx_bound : environment -> idx -> bool witness type Jidx_boundwitness; check Jidx_bound_check; (*idx_is_bound : input -> input -> input -> option *)]
(* defn bound *)

Jidx_bound_skip1: forall E EB idx name .
(Jidx_bound E idx) &&
(JdomEB EB name) &&
( (not ( name  =  Name_tv )) )
 ==> 
Jidx_bound  ( EB :: E )  idx

and
Jidx_bound_skip2: forall E idx .
(Jidx_bound E idx)
 ==> 
Jidx_bound  ( EB_tv :: E )   ( idx  +   1  ) 

and
Jidx_bound_found: forall E .
true
 ==> 
Jidx_bound  ( EB_tv :: E )   0 


(** definitions *)
(* defns JTtps_kind *)
indreln
[JTtps_kind : type_params_opt -> kind -> bool witness type JTtps_kindwitness; check JTtps_kind_check;]
(* defn tps_kind *)

JTtps_kind_kind: forall tp_list n .
( (list_distinct ( (tp_list) )) ) &&
( ( n  = List.length ( (tp_list) )) )
 ==> 
JTtps_kind (TPS_nary (tp_list))   n  


(** definitions *)
(* defns JTEok *)
indreln
[JTEok : environment -> bool witness type JTEok_witness; check JTEok_check;]

 and [JTtypeconstr : environment -> typeconstr -> kind -> bool witness type JTtypeconstrwitness; check JTtypeconstr_check;(* getKind : input -> input -> output *)]

 and [JTts : environment -> typescheme -> kind -> bool witness type JTtswitness; check JTts_check;]

 and [JTtsnamed : environment -> type_params_opt -> typexpr -> kind -> bool witness type JTtsnamedwitness; check JTtsnamed_check;]

 and [JTt : environment -> typexpr -> kind -> bool witness type t_witness; check t_check; (*get_kind : input -> input -> output*)]
(* defn Eok *)

JTEok_empty: forall .
true
 ==> 
JTEok  [] 

and
JTEok_typevar: forall E .
(JTEok E)
 ==> 
JTEok  ( EB_tv :: E ) 

and
JTEok_value_name: forall E value_name t .
(JTts E (TS_forall t)  0 )
 ==> 
JTEok  (  (EB_vn value_name (TS_forall t))  :: E ) 

and
JTEok_constr_name_c: forall E constr_name typeconstr_name kind names .
(JTEok E) &&
(Jlookup_EB E (Name_tcn typeconstr_name) (EB_td typeconstr_name kind)) &&
(JdomE E names) &&
( (not (List.elem  (Name_cn constr_name)   names )) )
 ==> 
JTEok  (  (EB_cc constr_name (TC_name typeconstr_name))  :: E ) 

and
JTEok_exn_constr_name_c: forall E constr_name names .
(JTEok E) &&
(JdomE E names) &&
( (not (List.elem  (Name_cn constr_name)   names )) )
 ==> 
JTEok  (  (EB_cc constr_name TC_exn)  :: E ) 

and
JTEok_constr_name_p: forall t_list tv_list E constr_name typeconstr_name type_params_opt m names .
( ( type_params_opt  =  (TPS_nary ((List.map (fun tv_ -> (TP_var tv_)) tv_list))) ) ) &&
((List.all (fun b -> b) ((List.map (fun t_ -> JTtsnamed E type_params_opt t_  0 ) t_list)))) &&
(Jlookup_EB E (Name_tcn typeconstr_name) (EB_td typeconstr_name   m  )) &&
(JdomE E names) &&
( (not (List.elem  (Name_cn constr_name)   names )) ) &&
( (List.length ( (t_list) ) >=   1  ) ) &&
( ( m  = List.length ( ((List.map (fun tv_ -> (TP_var tv_)) tv_list)) )) )
 ==> 
JTEok  (  (EB_pc constr_name (TPS_nary ((List.map (fun tv_ -> (TP_var tv_)) tv_list))) (Typexprs_inj (t_list)) (TC_name typeconstr_name))  :: E ) 

and
JTEok_exn_constr_name_p: forall t_list E constr_name names .
((List.all (fun b -> b) ((List.map (fun t_ -> JTt E t_  0 ) t_list)))) &&
(JdomE E names) &&
( (not (List.elem  (Name_cn constr_name)   names )) ) &&
( (List.length ( (t_list) ) >=   1  ) )
 ==> 
JTEok  (  (EB_pc constr_name  (TPS_nary [])  (Typexprs_inj (t_list)) TC_exn)  :: E ) 

and
JTEok_record_destr: forall field_name_list tv_list E field_name typeconstr_name t names m .
(JTtsnamed E (TPS_nary ((List.map (fun tv_ -> (TP_var tv_)) tv_list))) t  0 ) &&
(JdomE E names) &&
( (not (List.elem  (Name_fn field_name)   names )) ) &&
(Jlookup_EB E (Name_tcn typeconstr_name) (EB_tr typeconstr_name   m   (field_name_list))) &&
( ( m  = List.length ( ((List.map (fun tv_ -> (TP_var tv_)) tv_list)) )) ) &&
( (List.elem  field_name   (field_name_list) ) )
 ==> 
JTEok  (  (EB_fn field_name (TPS_nary ((List.map (fun tv_ -> (TP_var tv_)) tv_list))) typeconstr_name t)  :: E ) 

and
JTEok_typeconstr_name: forall E typeconstr_name kind names .
(JTEok E) &&
(JdomE E names) &&
( (not (List.elem  (Name_tcn typeconstr_name)   names )) )
 ==> 
JTEok  (  (EB_td typeconstr_name kind)  :: E ) 

and
JTEok_typeconstr_eqn: forall tv_list E typeconstr_name t names .
(JdomE E names) &&
( (not (List.elem  (Name_tcn typeconstr_name)   names )) ) &&
(JTtsnamed E (TPS_nary ((List.map (fun tv_ -> (TP_var tv_)) tv_list))) t  0 )
 ==> 
JTEok  (  (EB_ta (TPS_nary ((List.map (fun tv_ -> (TP_var tv_)) tv_list))) typeconstr_name t)  :: E ) 

and
JTEok_typeconstr_record: forall field_name_list E typeconstr_name kind names .
(JTEok E) &&
(JdomE E names) &&
( (not (List.elem  (Name_tcn typeconstr_name)   names )) ) &&
( (list_distinct ( ((List.map (fun field_name_ -> (Name_fn field_name_)) field_name_list)) )) )
 ==> 
JTEok  (  (EB_tr typeconstr_name kind (field_name_list))  :: E ) 

and
JTEok_location: forall E location t names .
(JTt E t  0 ) &&
(JdomE E names) &&
( (not (List.elem  (Name_l location)   names )) )
 ==> 
JTEok  (  (EB_l location t)  :: E ) 


and
(* defn typeconstr *)

JTtypeconstr_abstract: forall E typeconstr_name kind .
(JTEok E) &&
(Jlookup_EB E (Name_tcn typeconstr_name) (EB_td typeconstr_name kind))
 ==> 
JTtypeconstr E (TC_name typeconstr_name) kind

and
JTtypeconstr_concrete: forall E typeconstr_name kind type_params_opt t .
(JTEok E) &&
(Jlookup_EB E (Name_tcn typeconstr_name) (EB_ta type_params_opt typeconstr_name t)) &&
(JTtps_kind type_params_opt kind)
 ==> 
JTtypeconstr E (TC_name typeconstr_name) kind

and
JTtypeconstr_record: forall field_name_list E typeconstr_name kind .
(JTEok E) &&
(Jlookup_EB E (Name_tcn typeconstr_name) (EB_tr typeconstr_name kind (field_name_list)))
 ==> 
JTtypeconstr E (TC_name typeconstr_name) kind

and
JTtypeconstr_int: forall E .
(JTEok E)
 ==> 
JTtypeconstr E TC_int  0 

and
JTtypeconstr_char: forall E .
(JTEok E)
 ==> 
JTtypeconstr E TC_char  0 

and
JTtypeconstr_string: forall E .
(JTEok E)
 ==> 
JTtypeconstr E TC_string  0 

and
JTtypeconstr_float: forall E .
(JTEok E)
 ==> 
JTtypeconstr E TC_float  0 

and
JTtypeconstr_bool: forall E .
(JTEok E)
 ==> 
JTtypeconstr E TC_bool  0 

and
JTtypeconstr_unit: forall E .
(JTEok E)
 ==> 
JTtypeconstr E TC_unit  0 

and
JTtypeconstr_exn: forall E .
(JTEok E)
 ==> 
JTtypeconstr E TC_exn  0 

and
JTtypeconstr_list: forall E .
(JTEok E)
 ==> 
JTtypeconstr E TC_list   1  

and
JTtypeconstr_option: forall E .
(JTEok E)
 ==> 
JTtypeconstr E TC_option   1  

and
JTtypeconstr_ref: forall E .
(JTEok E)
 ==> 
JTtypeconstr E TC_ref   1  


and
(* defn ts *)

JTts_forall: forall E t .
(JTt  ( EB_tv :: E )  t  0 )
 ==> 
JTts E (TS_forall t)  0 


and
(* defn tsnamed *)

JTtsnamed_forall: forall tv_list E t .
(JTt E  (substs_typevar_typexpr   ((List.map (fun tv_ -> (tv_, (TE_constr []  TC_unit ) )) tv_list))    t )   0 ) &&
( (list_distinct ( ((List.map (fun tv_ -> (TP_var tv_)) tv_list)) )) )
 ==> 
JTtsnamed E (TPS_nary ((List.map (fun tv_ -> (TP_var tv_)) tv_list))) t  0 


and
(* defn t *)

JTt_var: forall E idx num .
(JTEok E) &&
(Jidx_bound E idx)
 ==> 
JTt E (TE_idxvar idx num)  0 

and
JTt_arrow: forall E t t' .
(JTt E t  0 ) &&
(JTt E t'  0 )
 ==> 
JTt E (TE_arrow t t')  0 

and
JTt_tuple: forall t_list E .
((List.all (fun b -> b) ((List.map (fun t_ -> JTt E t_  0 ) t_list)))) &&
( (List.length ( (t_list) ) >=   2  ) )
 ==> 
JTt E (TE_tuple (t_list))  0 

and
JTt_constr: forall t_list E typeconstr n .
(JTtypeconstr E typeconstr   n  ) &&
((List.all (fun b -> b) ((List.map (fun t_ -> JTt E t_  0 ) t_list)))) &&
( (  n   = List.length ( (t_list) )) )
 ==> 
JTt E (TE_constr (t_list) typeconstr)  0 


(** definitions *)
(* defns JTeq *)
indreln
[JTeq : environment -> typexpr -> typexpr -> bool witness type JTeq_witness; check JTeq_check;]
(* defn eq *)

JTeq_refl: forall E t .
(JTt E t  0 )
 ==> 
JTeq E t t

and
JTeq_sym: forall E t t' .
(JTeq E t' t)
 ==> 
JTeq E t t'

and
JTeq_trans: forall E t t'' t' .
(JTeq E t t') &&
(JTeq E t' t'')
 ==> 
JTeq E t t''

and
JTeq_expand: forall t_typevar_list E typeconstr_name t .
(JTEok E) &&
(Jlookup_EB E (Name_tcn typeconstr_name) (EB_ta (TPS_nary ((List.map (fun (t_,typevar_) -> (TP_var typevar_)) t_typevar_list))) typeconstr_name t)) &&
((List.all (fun b -> b) ((List.map (fun (t_,typevar_) -> JTt E t_  0 ) t_typevar_list))))
 ==> 
JTeq E (TE_constr ((List.map (fun (t_,typevar_) -> t_) t_typevar_list)) (TC_name typeconstr_name))  (substs_typevar_typexpr   ((List.map (fun (t_,typevar_) -> (typevar_,t_)) t_typevar_list))    t ) 

and
JTeq_arrow: forall E t1 t2 t1' t2' .
(JTeq E t1 t1') &&
(JTeq E t2 t2')
 ==> 
JTeq E (TE_arrow t1 t2) (TE_arrow t1' t2')

and
JTeq_tuple: forall t_t'_list E .
((List.all (fun b -> b) ((List.map (fun (t_,t_') -> JTeq E t_ t_') t_t'_list)))) &&
( (List.length ( ((List.map (fun (t_,t_') -> t_) t_t'_list)) ) >=   2  ) )
 ==> 
JTeq E (TE_tuple ((List.map (fun (t_,t_') -> t_) t_t'_list))) (TE_tuple ((List.map (fun (t_,t_') -> t_') t_t'_list)))

and
JTeq_constr: forall t_t'_list E typeconstr n .
(JTtypeconstr E typeconstr   n  ) &&
((List.all (fun b -> b) ((List.map (fun (t_,t_') -> JTeq E t_ t_') t_t'_list)))) &&
( (  n   = List.length ( ((List.map (fun (t_,t_') -> t_) t_t'_list)) )) )
 ==> 
JTeq E (TE_constr ((List.map (fun (t_,t_') -> t_) t_t'_list)) typeconstr) (TE_constr ((List.map (fun (t_,t_') -> t_') t_t'_list)) typeconstr)


(** definitions *)
(* defns JTidxsub *)
indreln
[JTidxsub : list typexpr -> typexpr -> typexpr -> bool witness type JTidxsub_witness; check JTidxsub_check;]
(* defn idxsub *)

JTinxsub_alpha: forall t_list typevar .
true
 ==> 
JTidxsub (t_list) (TE_var typevar) (TE_var typevar)

and
JTinxsub_idx0: forall t''_list t_list t' num .
( ( num  = List.length ( (t_list) )) )
 ==> 
JTidxsub (t_list ++ [(t')] ++ t''_list) (TE_idxvar  0  num) t'

and
JTinxsub_idx1: forall t_list num .
( (List.length ( (t_list) ) <=  num ) )
 ==> 
JTidxsub (t_list) (TE_idxvar  0  num)  (TE_constr []  TC_unit ) 

and
JTinxsub_idx2: forall t_list idx num .
true
 ==> 
JTidxsub (t_list) (TE_idxvar  ( idx  +   1  )  num) (TE_idxvar idx num)

and
JTinxsub_any: forall t_list .
true
 ==> 
JTidxsub (t_list) TE_any TE_any

and
JTinxsub_arrow: forall t_list t1' t2' t1'' t2'' .
(JTidxsub (t_list) t1' t1'') &&
(JTidxsub (t_list) t2' t2'')
 ==> 
JTidxsub (t_list)  (TE_arrow t1' t2')  (TE_arrow t1'' t2'')

and
JTinxsub_tuple: forall t'_t''_list t_list .
((List.all (fun b -> b) ((List.map (fun (t_',t_'') -> JTidxsub (t_list) t_' t_'') t'_t''_list))))
 ==> 
JTidxsub (t_list)  (TE_tuple ((List.map (fun (t_',t_'') -> t_') t'_t''_list)))   (TE_tuple ((List.map (fun (t_',t_'') -> t_'') t'_t''_list))) 

and
JTinxsub_tc: forall t'_t''_list t_list typeconstr .
((List.all (fun b -> b) ((List.map (fun (t_',t_'') -> JTidxsub (t_list) t_' t_'') t'_t''_list))))
 ==> 
JTidxsub (t_list) (TE_constr ((List.map (fun (t_',t_'') -> t_') t'_t''_list)) typeconstr) (TE_constr ((List.map (fun (t_',t_'') -> t_'') t'_t''_list)) typeconstr)


(** definitions *)
(* defns JTinst *)
indreln
[JTinst : environment -> typexpr -> typescheme -> bool witness type JTinst_witness; check JTinst_check;]
(* defn inst *)

JTinst_idx: forall t_list E t'' t' .
(JTts E (TS_forall t')  0 ) &&
((List.all (fun b -> b) ((List.map (fun t_ -> JTt E t_  0 ) t_list)))) &&
(JTidxsub (t_list) t' t'')
 ==> 
JTinst E t'' (TS_forall t')


(** definitions *)
(* defns JTinst_named *)
indreln
[JTinst_named : environment -> typexpr -> type_params_opt -> typexpr -> bool witness type JTinst_named_witness; check JTinst_named_check;]
(* defn inst_named *)

JTinst_named_named: forall typevar_t_list E t .
(JTtsnamed E (TPS_nary ((List.map (fun (typevar_,t_) -> (TP_var typevar_)) typevar_t_list))) t  0 ) &&
((List.all (fun b -> b) ((List.map (fun (typevar_,t_) -> JTt E t_  0 ) typevar_t_list))))
 ==> 
JTinst_named E  (substs_typevar_typexpr   (typevar_t_list)    t )  (TPS_nary ((List.map (fun (typevar_,t_) -> (TP_var typevar_)) typevar_t_list))) t


(** definitions *)
(* defns JTinst_any *)
indreln
[JTinst_any : environment -> typexpr -> typexpr -> bool witness type JTinst_any_witness; check JTinst_any_check;]
(* defn inst_any *)

JTinst_any_tyvar: forall E idx num .
(JTt E (TE_idxvar idx num)  0 )
 ==> 
JTinst_any E (TE_idxvar idx num) (TE_idxvar idx num)

and
JTinst_any_any: forall E t .
(JTt E t  0 )
 ==> 
JTinst_any E t TE_any

and
JTinst_any_arrow: forall E t1 t2 t1' t2' .
(JTinst_any E t1 t1') &&
(JTinst_any E t2 t2')
 ==> 
JTinst_any E (TE_arrow t1 t2) (TE_arrow t1' t2')

and
JTinst_any_tuple: forall t_t'_list E .
((List.all (fun b -> b) ((List.map (fun (t_,t_') -> JTinst_any E t_ t_') t_t'_list)))) &&
( (List.length ( ((List.map (fun (t_,t_') -> t_) t_t'_list)) ) >=   2  ) )
 ==> 
JTinst_any E (TE_tuple ((List.map (fun (t_,t_') -> t_) t_t'_list))) (TE_tuple ((List.map (fun (t_,t_') -> t_') t_t'_list)))

and
JTinst_any_ctor: forall t_t'_list E typeconstr n .
((List.all (fun b -> b) ((List.map (fun (t_,t_') -> JTinst_any E t_ t_') t_t'_list)))) &&
(JTtypeconstr E typeconstr   n  ) &&
( (  n   = List.length ( ((List.map (fun (t_,t_') -> t_) t_t'_list)) )) )
 ==> 
JTinst_any E (TE_constr ((List.map (fun (t_,t_') -> t_) t_t'_list)) typeconstr) (TE_constr ((List.map (fun (t_,t_') -> t_') t_t'_list)) typeconstr)


(** definitions *)
(* defns JTval *)
indreln
[JTvalue_name : environment -> value_name -> typexpr -> bool witness type JTval_witness; check JTval_check;]
(* defn value_name *)

JTvalue_name_value_name: forall E value_name t ts .
(Jlookup_EB E (Name_vn value_name) (EB_vn value_name ts)) &&
(JTinst E t ts)
 ==> 
JTvalue_name E value_name t


(** definitions *)
(* defns JTfield *)
indreln
[JTfield : environment -> field_name -> typexpr -> typexpr -> bool witness type JTfield_witness; check JTfield_check;]
(* defn field *)

JTfield_name: forall t'_tv_list E field_name typeconstr_name t'' t .
(Jlookup_EB E (Name_fn field_name) (EB_fn field_name (TPS_nary ((List.map (fun (t_',tv_) -> (TP_var tv_)) t'_tv_list))) typeconstr_name t)) &&
(JTinst_named E (TE_arrow (TE_constr ((List.map (fun (t_',tv_) -> t_') t'_tv_list)) (TC_name typeconstr_name)) t'') (TPS_nary ((List.map (fun (t_',tv_) -> (TP_var tv_)) t'_tv_list))) (TE_arrow (TE_constr ((List.map (fun (t_',tv_) -> (TE_var tv_)) t'_tv_list)) (TC_name typeconstr_name)) t))
 ==> 
JTfield E field_name (TE_constr ((List.map (fun (t_',tv_) -> t_') t'_tv_list)) (TC_name typeconstr_name)) t''


(** definitions *)
(* defns JTconstr_p *)
indreln
[JTconstr_p : environment -> constr -> list typexpr -> typexpr -> bool witness type JTconstr_p_witness; check JTconstr_p_check;]
(* defn constr_p *)

JTconstr_p_name: forall t'_t_list t''_tv_list E constr_name typeconstr .
(Jlookup_EB E (Name_cn constr_name) (EB_pc constr_name (TPS_nary ((List.map (fun (t_'',tv_) -> (TP_var tv_)) t''_tv_list))) (Typexprs_inj ((List.map (fun (t_',t_) -> t_) t'_t_list))) typeconstr)) &&
(JTinst_named E (TE_arrow  (TE_tuple ((List.map (fun (t_',t_) -> t_') t'_t_list)))  (TE_constr ((List.map (fun (t_'',tv_) -> t_'') t''_tv_list)) typeconstr)) (TPS_nary ((List.map (fun (t_'',tv_) -> (TP_var tv_)) t''_tv_list))) (TE_arrow  (TE_tuple ((List.map (fun (t_',t_) -> t_) t'_t_list)))  (TE_constr ((List.map (fun (t_'',tv_) -> (TE_var tv_)) t''_tv_list)) typeconstr)))
 ==> 
JTconstr_p E (C_name constr_name) ((List.map (fun (t_',t_) -> t_') t'_t_list)) (TE_constr ((List.map (fun (t_'',tv_) -> t_'') t''_tv_list)) typeconstr)

and
JTconstr_p_invarg: forall E .
(JTEok E)
 ==> 
JTconstr_p E C_invalidargument ([( (TE_constr []  TC_string ) )])  (TE_constr []  TC_exn ) 

and
JTconstr_p_some: forall E t .
(JTt E t  0 )
 ==> 
JTconstr_p E C_some ([(t)])   (TE_constr ([  t  ])  TC_option )  


(** definitions *)
(* defns JTconstr_c *)
indreln
[JTconstr_c : environment -> constr -> typexpr -> bool witness type JTconstr_c_witness; check JTconstr_c_check;]
(* defn constr_c *)

JTconstr_c_constr: forall t_list E constr_name typeconstr_name n .
(JTEok E) &&
(Jlookup_EB E (Name_cn constr_name) (EB_cc constr_name (TC_name typeconstr_name))) &&
(Jlookup_EB E (Name_tcn typeconstr_name) (EB_td typeconstr_name   n  )) &&
((List.all (fun b -> b) ((List.map (fun t_ -> JTt E t_  0 ) t_list)))) &&
( (  n   = List.length ( (t_list) )) )
 ==> 
JTconstr_c E (C_name constr_name) (TE_constr (t_list) (TC_name typeconstr_name))

and
JTconstr_c_exn_constr: forall E constr_name .
(JTEok E) &&
(Jlookup_EB E (Name_cn constr_name) (EB_cc constr_name TC_exn))
 ==> 
JTconstr_c E (C_name constr_name)  (TE_constr []  TC_exn ) 

and
JTconstr_c_notfound: forall E .
(JTEok E)
 ==> 
JTconstr_c E C_notfound  (TE_constr []  TC_exn ) 

and
JTconstr_c_assert_fail: forall E .
(JTEok E)
 ==> 
JTconstr_c E C_assertfailure  (TE_constr []  TC_exn ) 

and
JTconstr_c_match_fail: forall E .
(JTEok E)
 ==> 
JTconstr_c E C_matchfailure  (TE_constr []  TC_exn ) 

and
JTconstr_c_div_by_0: forall E .
(JTEok E)
 ==> 
JTconstr_c E C_div_by_0  (TE_constr []  TC_exn ) 

and
JTconstr_c_none: forall E t .
(JTt E t  0 )
 ==> 
JTconstr_c E C_none  (TE_constr ([  t  ])  TC_option ) 


(** definitions *)
(* defns JTconst *)
indreln
[JTconst : environment -> constantl -> typexpr -> bool witness type JTconst_witness; check JTconst_check;]
(* defn const *)

JTconst_int: forall E integer_literal .
(JTEok E)
 ==> 
JTconst E (CONST_int  integer_literal )  (TE_constr []  TC_int ) 

and
JTconst_float: forall E float_literal .
(JTEok E)
 ==> 
JTconst E (CONST_float float_literal)  (TE_constr []  TC_float ) 

and
JTconst_char: forall E char_literal .
(JTEok E)
 ==> 
JTconst E (CONST_char char_literal)  (TE_constr []  TC_char ) 

and
JTconst_string: forall E string_literal .
(JTEok E)
 ==> 
JTconst E (CONST_string string_literal)  (TE_constr []  TC_string ) 

and
JTconst_constr: forall E constr t .
(JTconstr_c E constr t)
 ==> 
JTconst E (CONST_constr constr) t

and
JTconst_false: forall E .
(JTEok E)
 ==> 
JTconst E CONST_false  (TE_constr []  TC_bool ) 

and
JTconst_true: forall E .
(JTEok E)
 ==> 
JTconst E CONST_true  (TE_constr []  TC_bool ) 

and
JTconst_unit: forall E .
(JTEok E)
 ==> 
JTconst E CONST_unit  (TE_constr []  TC_unit ) 

and
JTconst_nil: forall E t .
(JTt E t  0 )
 ==> 
JTconst E CONST_nil  (TE_constr ([  t  ])  TC_list ) 


(** definitions *)
(* defns JTpat *)
indreln
[JTpat : Tsigma -> environment -> patternl -> typexpr -> environment -> bool witness type JTpat_witness; check JTpat_check;]
(* defn pat *)

JTpat_var: forall Tsigma E x t .
(JTt E t  0 )
 ==> 
JTpat Tsigma E (P_var x) t  (  (EB_vn  x  (TS_forall (shiftt 0 1  t )))  ::  []  ) 

and
JTpat_any: forall Tsigma E t .
(JTt E t  0 )
 ==> 
JTpat Tsigma E P_any t  [] 

and
JTpat_constant: forall Tsigma E constantl t .
(JTconst E constantl t)
 ==> 
JTpat Tsigma E (P_constant constantl) t  [] 

and
JTpat_alias: forall name_list Tsigma E patternl x t E' .
(JTpat Tsigma E patternl t E') &&
(JdomE  (  (EB_vn  x  (TS_forall (shiftt 0 1  t )))  :: E' )   (name_list) ) &&
( (list_distinct ( (name_list) )) )
 ==> 
JTpat Tsigma E (P_alias patternl x) t  (  (EB_vn  x  (TS_forall (shiftt 0 1  t )))  :: E' ) 

and
JTpat_typed: forall Tsigma E patternl src_t t E' t' .
(is_src_typexpr_of_typexpr src_t) &&
(JTpat Tsigma E patternl t E') &&
(JTinst_any E t'  (substs_typevar_typexpr  Tsigma   src_t ) ) &&
(JTeq E t t')
 ==> 
JTpat Tsigma E (P_typed patternl src_t) t E'

and
JTpat_or: forall Tsigma E patternl patternl' t E' E'' .
(JTpat Tsigma E patternl t E') &&
(JTpat Tsigma E patternl' t E'') &&
( (list_perm ( E' ) ( E'' )) )
 ==> 
JTpat Tsigma E (P_or patternl patternl') t E'

and
JTpat_construct: forall name_list patternl_E_t_list Tsigma E constr t .
(JTconstr_p E constr ((List.map (fun (patternl_,E_,t_) -> t_) patternl_E_t_list)) t) &&
((List.all (fun b -> b) ((List.map (fun (patternl_,E_,t_) -> JTpat Tsigma E patternl_ t_ E_) patternl_E_t_list)))) &&
(JdomE  (List.concat (List.reverse  ((List.map (fun (patternl_,E_,t_) -> E_) patternl_E_t_list)) ))   (name_list) ) &&
( (list_distinct ( (name_list) )) )
 ==> 
JTpat Tsigma E (P_construct constr ((List.map (fun (patternl_,E_,t_) -> patternl_) patternl_E_t_list))) t  (List.concat (List.reverse  ((List.map (fun (patternl_,E_,t_) -> E_) patternl_E_t_list)) )) 

and
JTpat_construct_any: forall t_list Tsigma E constr t .
(JTconstr_p E constr (t_list) t)
 ==> 
JTpat Tsigma E (P_construct_any constr) t  [] 

and
JTpat_tuple: forall name_list patternl_t_E_list Tsigma E .
((List.all (fun b -> b) ((List.map (fun (patternl_,t_,E_) -> JTpat Tsigma E patternl_ t_ E_) patternl_t_E_list)))) &&
( (List.length ( ((List.map (fun (patternl_,t_,E_) -> patternl_) patternl_t_E_list)) ) >=  2 ) ) &&
(JdomE  (List.concat (List.reverse  ((List.map (fun (patternl_,t_,E_) -> E_) patternl_t_E_list)) ))   (name_list) ) &&
( (list_distinct ( (name_list) )) )
 ==> 
JTpat Tsigma E (P_tuple ((List.map (fun (patternl_,t_,E_) -> patternl_) patternl_t_E_list))) (TE_tuple ((List.map (fun (patternl_,t_,E_) -> t_) patternl_t_E_list)))  (List.concat (List.reverse  ((List.map (fun (patternl_,t_,E_) -> E_) patternl_t_E_list)) )) 

and
JTpat_record: forall name_list field_name_patternl_E_t_list Tsigma E t .
((List.all (fun b -> b) ((List.map (fun (field_name_,patternl_,E_,t_) -> JTpat Tsigma E patternl_ t_ E_) field_name_patternl_E_t_list)))) &&
((List.all (fun b -> b) ((List.map (fun (field_name_,patternl_,E_,t_) -> JTfield E field_name_ t t_) field_name_patternl_E_t_list)))) &&
( (List.length ( ((List.map (fun (field_name_,patternl_,E_,t_) -> patternl_) field_name_patternl_E_t_list)) ) >=  1 ) ) &&
(JdomE  (List.concat (List.reverse  ((List.map (fun (field_name_,patternl_,E_,t_) -> E_) field_name_patternl_E_t_list)) ))   (name_list) ) &&
( (list_distinct ( (name_list) )) )
 ==> 
JTpat Tsigma E (P_record ((List.map (fun (field_name_,patternl_,E_,t_) -> ((F_name field_name_),patternl_)) field_name_patternl_E_t_list))) t  (List.concat (List.reverse  ((List.map (fun (field_name_,patternl_,E_,t_) -> E_) field_name_patternl_E_t_list)) )) 

and
JTpat_cons: forall name'_list name_list Tsigma E patternl patternl' t E' E'' .
(JTpat Tsigma E patternl t E') &&
(JTpat Tsigma E patternl'  (TE_constr ([  t  ])  TC_list )  E'') &&
(JdomE E'  (name_list) ) &&
(JdomE E''  (name'_list) ) &&
( (list_distinct ( (name_list ++ name'_list) )) )
 ==> 
JTpat Tsigma E (P_cons patternl patternl')  (TE_constr ([  t  ])  TC_list )   (List.concat (List.reverse  ([(E')] ++ [(E'')]) )) 


(** definitions *)
(* defns JTuprim *)
indreln
[JTuprim : environment -> unary_prim -> typexpr -> bool witness type JTuprim_witness; check JTuprim_check;]
(* defn uprim *)

JTuprim_raise: forall E t .
(JTt E t  0 )
 ==> 
JTuprim E Uprim_raise (TE_arrow  (TE_constr []  TC_exn )  t)

and
JTuprim_not: forall E .
(JTEok E)
 ==> 
JTuprim E Uprim_not (TE_arrow  (TE_constr []  TC_bool )   (TE_constr []  TC_bool ) )

and
JTuprim_uminus: forall E .
(JTEok E)
 ==> 
JTuprim E Uprim_minus (TE_arrow  (TE_constr []  TC_int )   (TE_constr []  TC_int ) )

and
JTuprim_ref: forall E t .
(JTt E t  0 )
 ==> 
JTuprim E Uprim_ref (TE_arrow t   (TE_constr ([  t  ])  TC_ref )  )

and
JTuprim_deref: forall E t .
(JTt E t  0 )
 ==> 
JTuprim E Uprim_deref (TE_arrow   (TE_constr ([  t  ])  TC_ref )   t)


(** definitions *)
(* defns JTbprim *)
indreln
[JTbprim : environment -> binary_prim -> typexpr -> bool witness type JTbprim_witness; check JTbprim_check;]
(* defn bprim *)

JTbprim_equal: forall E t .
(JTt E t  0 )
 ==> 
JTbprim E Bprim_equal (TE_arrow t  (TE_arrow t  (TE_constr []  TC_bool ) ) )

and
JTbprim_plus: forall E .
(JTEok E)
 ==> 
JTbprim E Bprim_plus (TE_arrow  (TE_constr []  TC_int )   (TE_arrow  (TE_constr []  TC_int )   (TE_constr []  TC_int ) ) )

and
JTbprim_minus: forall E .
(JTEok E)
 ==> 
JTbprim E Bprim_minus (TE_arrow  (TE_constr []  TC_int )   (TE_arrow  (TE_constr []  TC_int )   (TE_constr []  TC_int ) ) )

and
JTbprim_times: forall E .
(JTEok E)
 ==> 
JTbprim E Bprim_times (TE_arrow  (TE_constr []  TC_int )   (TE_arrow  (TE_constr []  TC_int )   (TE_constr []  TC_int ) ) )

and
JTbprim_div: forall E .
(JTEok E)
 ==> 
JTbprim E Bprim_div (TE_arrow  (TE_constr []  TC_int )   (TE_arrow  (TE_constr []  TC_int )   (TE_constr []  TC_int ) ) )

and
JTbprim_assign: forall E t .
(JTt E t  0 )
 ==> 
JTbprim E Bprim_assign (TE_arrow  (TE_constr ([  t  ])  TC_ref )   (TE_arrow t  (TE_constr []  TC_unit ) ) )


(** definitions *)
(* defns JTe *)
indreln
[JTe : Tsigma -> environment -> expr -> typexpr -> bool witness type JTe_witness; check JTe_check;]

 and [JTpat_matching : Tsigma -> environment -> pattern_matching -> typexpr -> typexpr -> bool witness type JTepat_witness; check JTepat_check;]

 and [JTlet_binding : Tsigma -> environment -> let_binding -> environment -> bool witness type JTeletb_witness; check JTeletb_check;]

 and [JTletrec_binding : Tsigma -> environment -> letrec_bindings -> environment -> bool witness type JTelrb_witness; check JTelrb_check;]
(* defn e *)

JTe_uprim: forall Tsigma E unary_prim t' t .
(JTuprim E unary_prim t) &&
(JTeq E t t')
 ==> 
JTe Tsigma E (Expr_uprim unary_prim) t'

and
JTe_bprim: forall Tsigma E binary_prim t' t .
(JTbprim E binary_prim t) &&
(JTeq E t t')
 ==> 
JTe Tsigma E (Expr_bprim binary_prim) t'

and
JTe_ident: forall Tsigma E value_name t' t .
(JTvalue_name E value_name t) &&
(JTeq E t t')
 ==> 
JTe Tsigma E (Expr_ident value_name) t'

and
JTe_constant: forall Tsigma E constantl t' t .
(JTconst E constantl t) &&
(JTeq E t t')
 ==> 
JTe Tsigma E (Expr_constant constantl) t'

and
JTe_typed: forall Tsigma E e src_t t t' .
(is_src_typexpr_of_typexpr src_t) &&
(JTe Tsigma E e t) &&
(JTinst_any E t'  (substs_typevar_typexpr  Tsigma   src_t ) ) &&
(JTeq E t t')
 ==> 
JTe Tsigma E (Expr_typed e src_t) t

and
JTe_tuple: forall e_t_list Tsigma E t' .
((List.all (fun b -> b) ((List.map (fun (e_,t_) -> JTe Tsigma E e_ t_) e_t_list)))) &&
( (List.length ( ((List.map (fun (e_,t_) -> e_) e_t_list)) ) >=  2 ) ) &&
(JTeq E (TE_tuple ((List.map (fun (e_,t_) -> t_) e_t_list))) t')
 ==> 
JTe Tsigma E (Expr_tuple ((List.map (fun (e_,t_) -> e_) e_t_list))) t'

and
JTe_construct: forall e_t_list Tsigma E constr t' t .
(JTconstr_p E constr ((List.map (fun (e_,t_) -> t_) e_t_list)) t) &&
((List.all (fun b -> b) ((List.map (fun (e_,t_) -> JTe Tsigma E e_ t_) e_t_list)))) &&
(JTeq E t t')
 ==> 
JTe Tsigma E (Expr_construct constr ((List.map (fun (e_,t_) -> e_) e_t_list))) t'

and
JTe_cons: forall Tsigma E e1 e2 t' t .
(JTe Tsigma E e1 t) &&
(JTe Tsigma E e2  (TE_constr ([  t  ])  TC_list ) ) &&
(JTeq E  (TE_constr ([  t  ])  TC_list )  t')
 ==> 
JTe Tsigma E (Expr_cons e1 e2) t'

and
JTe_record_constr: forall field_name'_list t'_list field_name_e_t_list Tsigma E t' t typeconstr_name kind .
((List.all (fun b -> b) ((List.map (fun (field_name_,e_,t_) -> JTe Tsigma E e_ t_) field_name_e_t_list)))) &&
((List.all (fun b -> b) ((List.map (fun (field_name_,e_,t_) -> JTfield E field_name_ t t_) field_name_e_t_list)))) &&
( ( t  =  (TE_constr (t'_list) (TC_name typeconstr_name)) ) ) &&
(Jlookup_EB E (Name_tcn typeconstr_name) (EB_tr typeconstr_name kind (field_name'_list))) &&
( (list_perm ( ((List.map (fun (field_name_,e_,t_) -> field_name_) field_name_e_t_list)) ) ( (field_name'_list) )) ) &&
( (List.length ( ((List.map (fun (field_name_,e_,t_) -> e_) field_name_e_t_list)) ) >=  1 ) ) &&
(JTeq E t t')
 ==> 
JTe Tsigma E (Expr_record ((List.map (fun (field_name_,e_,t_) -> ((F_name field_name_),e_)) field_name_e_t_list))) t'

and
JTe_record_with: forall field_name_e_t_list Tsigma E expr t' t .
(JTe Tsigma E expr t) &&
((List.all (fun b -> b) ((List.map (fun (field_name_,e_,t_) -> JTfield E field_name_ t t_) field_name_e_t_list)))) &&
((List.all (fun b -> b) ((List.map (fun (field_name_,e_,t_) -> JTe Tsigma E e_ t_) field_name_e_t_list)))) &&
( (list_distinct ( ((List.map (fun (field_name_,e_,t_) -> (Name_fn field_name_)) field_name_e_t_list)) )) ) &&
( (List.length ( ((List.map (fun (field_name_,e_,t_) -> e_) field_name_e_t_list)) ) >=  1 ) ) &&
(JTeq E t t')
 ==> 
JTe Tsigma E (Expr_override expr ((List.map (fun (field_name_,e_,t_) -> ((F_name field_name_),e_)) field_name_e_t_list))) t'

and
JTe_apply: forall Tsigma E e e1 t t1 .
(JTe Tsigma E e (TE_arrow t1 t)) &&
(JTe Tsigma E e1 t1)
 ==> 
JTe Tsigma E (Expr_apply e e1) t

and
JTe_record_proj: forall Tsigma E e field_name t'' t t' .
(JTe Tsigma E e t) &&
(JTfield E field_name t t') &&
(JTeq E t' t'')
 ==> 
JTe Tsigma E (Expr_field e (F_name field_name)) t''

and
JTe_and: forall Tsigma E e1 e2 t .
(JTe Tsigma E e1  (TE_constr []  TC_bool ) ) &&
(JTe Tsigma E e2  (TE_constr []  TC_bool ) ) &&
(JTeq E  (TE_constr []  TC_bool )  t)
 ==> 
JTe Tsigma E (Expr_and e1 e2) t

and
JTe_or: forall Tsigma E e1 e2 t .
(JTe Tsigma E e1  (TE_constr []  TC_bool ) ) &&
(JTe Tsigma E e2  (TE_constr []  TC_bool ) ) &&
(JTeq E  (TE_constr []  TC_bool )  t)
 ==> 
JTe Tsigma E (Expr_or e1 e2) t

and
JTe_ifthenelse: forall Tsigma E e1 e2 e3 t .
(JTe Tsigma E e1  (TE_constr []  TC_bool ) ) &&
(JTe Tsigma E e2 t) &&
(JTe Tsigma E e3 t)
 ==> 
JTe Tsigma E (Expr_ifthenelse e1 e2 e3) t

and
JTe_while: forall Tsigma E e1 e2 t .
(JTe Tsigma E e1  (TE_constr []  TC_bool ) ) &&
(JTe Tsigma E e2  (TE_constr []  TC_unit ) ) &&
(JTeq E  (TE_constr []  TC_unit )  t)
 ==> 
JTe Tsigma E (Expr_while e1 e2) t

and
JTe_for: forall Tsigma E lowercase_ident e1 for_dirn e2 e3 t .
(JTe Tsigma E e1  (TE_constr []  TC_int ) ) &&
(JTe Tsigma E e2  (TE_constr []  TC_int ) ) &&
(JTe Tsigma  (  (EB_vn  (VN_id lowercase_ident)  (TS_forall (shiftt 0 1   (TE_constr []  TC_int )  )))  :: E )  e3  (TE_constr []  TC_unit ) ) &&
(JTeq E  (TE_constr []  TC_unit )  t)
 ==> 
JTe Tsigma E (Expr_for (VN_id lowercase_ident) e1 for_dirn e2 e3) t

and
JTe_sequence: forall Tsigma E e1 e2 t .
(JTe Tsigma E e1  (TE_constr []  TC_unit ) ) &&
(JTe Tsigma E e2 t)
 ==> 
JTe Tsigma E (Expr_sequence e1 e2) t

and
JTe_match: forall Tsigma E e pattern_matching t' t .
(JTe Tsigma E e t) &&
(JTpat_matching Tsigma E pattern_matching t t')
 ==> 
JTe Tsigma E (Expr_match e pattern_matching) t'

and
JTe_function: forall Tsigma E pattern_matching t'' t t' .
(JTpat_matching Tsigma E pattern_matching t t') &&
(JTeq E (TE_arrow t t') t'')
 ==> 
JTe Tsigma E (Expr_function pattern_matching) t''

and
JTe_try: forall Tsigma E e pattern_matching t .
(JTe Tsigma E e t) &&
(JTpat_matching Tsigma E pattern_matching  (TE_constr []  TC_exn )  t)
 ==> 
JTe Tsigma E (Expr_try e pattern_matching) t

and
JTe_let_mono: forall x_t_list Tsigma E pat expr e t .
(JTlet_binding Tsigma E (LB_simple pat expr)  (List.reverse  ((List.map (fun (x_,t_) ->  (EB_vn  x_  (TS_forall (shiftt 0 1  t_ ))) ) x_t_list)) ) ) &&
(JTe Tsigma  (List.concat (List.reverse  ([(E)] ++ [( (List.reverse  ((List.map (fun (x_,t_) ->  (EB_vn  x_  (TS_forall (shiftt 0 1  t_ ))) ) x_t_list)) ) )]) ))  e t)
 ==> 
JTe Tsigma E (Expr_let (LB_simple pat expr) e) t

and
JTe_let_poly: forall x_t_list Tsigma E pat nexp e t .
(is_non_expansive_of_expr nexp) &&
(JTlet_binding  (shiftTsig   0     1    Tsigma )   ( EB_tv :: E )  (LB_simple pat nexp)  (List.reverse  ((List.map (fun (x_,t_) ->  (EB_vn  x_  (TS_forall (shiftt 0 1  t_ ))) ) x_t_list)) ) ) &&
(JTe Tsigma  (List.concat (List.reverse  ([(E)] ++ [( (List.reverse  ((List.map (fun (x_,t_) -> (EB_vn x_ (TS_forall t_))) x_t_list)) ) )]) ))  e t)
 ==> 
JTe Tsigma E (Expr_let (LB_simple pat nexp) e) t

and
JTe_letrec: forall x_t_list Tsigma E letrec_bindings e t .
(JTletrec_binding  (shiftTsig   0     1    Tsigma )   ( EB_tv :: E )  letrec_bindings  (List.reverse  ((List.map (fun (x_,t_) ->  (EB_vn  x_  (TS_forall (shiftt 0 1  t_ ))) ) x_t_list)) ) ) &&
(JTe Tsigma  (List.concat (List.reverse  ([(E)] ++ [( (List.reverse  ((List.map (fun (x_,t_) ->  (EB_vn x_ (TS_forall t_)) ) x_t_list)) ) )]) ))  e t)
 ==> 
JTe Tsigma E (Expr_letrec letrec_bindings e) t

and
JTe_assert: forall Tsigma E e t .
(JTe Tsigma E e  (TE_constr []  TC_bool ) ) &&
(JTeq E  (TE_constr []  TC_unit )  t)
 ==> 
JTe Tsigma E (Expr_assert e) t

and
JTe_assertfalse: forall Tsigma E t .
(JTt E t  0 )
 ==> 
JTe Tsigma E (Expr_assert (Expr_constant CONST_false)) t

and
JTe_location: forall Tsigma E location t' t .
(JTEok E) &&
(Jlookup_EB E (Name_l location) (EB_l location t)) &&
(JTeq E  (TE_constr ([  t  ])  TC_ref )  t')
 ==> 
JTe Tsigma E (Expr_location location) t'


and
(* defn pat_matching *)

JTpat_matching_pm: forall patternl_e_E_list Tsigma E t t' .
((List.all (fun b -> b) ((List.map (fun (patternl_,e_,E_) -> JTpat Tsigma E patternl_ t E_) patternl_e_E_list)))) &&
((List.all (fun b -> b) ((List.map (fun (patternl_,e_,E_) -> JTe Tsigma  (List.concat (List.reverse  ([(E)] ++ [(E_)]) ))  e_ t') patternl_e_E_list)))) &&
( (List.length ( ((List.map (fun (patternl_,e_,E_) -> patternl_) patternl_e_E_list)) ) >=  1 ) )
 ==> 
JTpat_matching Tsigma E (PM_pm ((List.map (fun (patternl_,e_,E_) -> (PE_inj patternl_ e_)) patternl_e_E_list))) t t'


and
(* defn let_binding *)

JTlet_binding_poly: forall x_t_list Tsigma E patternl expr t .
(JTpat Tsigma E patternl t  (List.reverse  ((List.map (fun (x_,t_) ->  (EB_vn  x_  (TS_forall (shiftt 0 1  t_ ))) ) x_t_list)) ) ) &&
(JTe Tsigma E expr t)
 ==> 
JTlet_binding Tsigma E (LB_simple patternl expr)  (List.reverse  ((List.map (fun (x_,t_) ->   (EB_vn  x_  (TS_forall (shiftt 0 1  t_ )))  ) x_t_list)) ) 


and
(* defn letrec_binding *)

JTletrec_binding_equal_function: forall value_name_pattern_matching_t_t'_list Tsigma E E' .
( ( E'  =   (List.concat (List.reverse  ([(E)] ++ [( (List.reverse  ((List.map (fun (value_name_,pattern_matching_,t_,t_') ->  (EB_vn  value_name_  (TS_forall (shiftt 0 1  (TE_arrow t_ t_') ))) ) value_name_pattern_matching_t_t'_list)) ) )]) ))  ) ) &&
((List.all (fun b -> b) ((List.map (fun (value_name_,pattern_matching_,t_,t_') -> JTpat_matching Tsigma E' pattern_matching_ t_ t_') value_name_pattern_matching_t_t'_list)))) &&
( (list_distinct ( ((List.map (fun (value_name_,pattern_matching_,t_,t_') -> (Name_vn value_name_)) value_name_pattern_matching_t_t'_list)) )) )
 ==> 
JTletrec_binding Tsigma E (LRBs_inj ((List.map (fun (value_name_,pattern_matching_,t_,t_') -> (LRB_simple value_name_ pattern_matching_)) value_name_pattern_matching_t_t'_list)))  (List.reverse  ((List.map (fun (value_name_,pattern_matching_,t_,t_') ->  (EB_vn  value_name_  (TS_forall (shiftt 0 1  (TE_arrow t_ t_') ))) ) value_name_pattern_matching_t_t'_list)) ) 


(** definitions *)
(* defns JTconstr_decl *)
indreln
[JTconstr_decl : type_params_opt -> typeconstr -> constr_decl -> environment_binding -> bool witness type JTconstr_decl_witness; check JTconstr_decl_check;]
(* defn constr_decl *)

JTconstr_decl_nullary: forall tv_list typeconstr constr_name .
true
 ==> 
JTconstr_decl (TPS_nary ((List.map (fun tv_ -> (TP_var tv_)) tv_list))) typeconstr (CD_nullary constr_name) (EB_cc constr_name typeconstr)

and
JTconstr_decl_nary: forall tv_t_list typeconstr constr_name .
true
 ==> 
JTconstr_decl (TPS_nary ((List.map (fun (tv_,t_) -> (TP_var tv_)) tv_t_list))) typeconstr (CD_nary constr_name ((List.map (fun (tv_,t_) -> t_) tv_t_list))) (EB_pc constr_name (TPS_nary ((List.map (fun (tv_,t_) -> (TP_var tv_)) tv_t_list))) (Typexprs_inj ((List.map (fun (tv_,t_) -> t_) tv_t_list))) typeconstr)


(** definitions *)
(* defns JTfield_decl *)
indreln
[JTfield_decl : type_params_opt -> typeconstr_name -> field_decl -> environment_binding -> bool witness type JTfield_decl_witness; check JTfield_decl_check;]
(* defn field_decl *)

JTfield_decl_only: forall tv_list typeconstr_name fn t .
true
 ==> 
JTfield_decl (TPS_nary ((List.map (fun tv_ -> (TP_var tv_)) tv_list))) typeconstr_name (FD_immutable fn t) (EB_fn fn (TPS_nary ((List.map (fun tv_ -> (TP_var tv_)) tv_list))) typeconstr_name t)


(** definitions *)
(* defns JTtypedef *)
indreln
[JTtypedef : list typedef -> environment -> environment -> environment -> bool witness type JTtypedef_witness; check JTtypedef_check;]
(* defn typedef *)

JTtypedef_empty: forall .
true
 ==> 
JTtypedef []  []   []   [] 

and
JTtypedef_eq: forall typedef_list type_params_opt typeconstr_name t E E' E'' .
(JTtypedef (typedef_list) E E' E'')
 ==> 
JTtypedef ([((TD_td type_params_opt typeconstr_name (TI_eq (TE_te t))))] ++ typedef_list) E  (  (EB_ta type_params_opt typeconstr_name t)  :: E' )  E''

and
JTtypedef_def_sum: forall constr_decl_EB_list typedef_list type_params_opt typeconstr_name E kind E' E'' .
(JTtypedef (typedef_list) E E' E'') &&
(JTtps_kind type_params_opt kind) &&
((List.all (fun b -> b) ((List.map (fun (constr_decl_,EB_) -> JTconstr_decl type_params_opt (TC_name typeconstr_name) constr_decl_ EB_) constr_decl_EB_list))))
 ==> 
JTtypedef ([((TD_td type_params_opt typeconstr_name (TI_def (TR_variant ((List.map (fun (constr_decl_,EB_) -> constr_decl_) constr_decl_EB_list))))))] ++ typedef_list)  (  (EB_td typeconstr_name kind)  :: E )  E'  (List.concat (List.reverse  ([(E'')] ++ [( (List.reverse  ((List.map (fun (constr_decl_,EB_) -> EB_) constr_decl_EB_list)) ) )]) )) 

and
JTtypedef_def_record: forall field_name_t_EB_list typedef_list type_params_opt typeconstr_name E kind E' E'' .
(JTtypedef (typedef_list) E E' E'') &&
(JTtps_kind type_params_opt kind) &&
((List.all (fun b -> b) ((List.map (fun (field_name_,t_,EB_) -> JTfield_decl type_params_opt typeconstr_name (FD_immutable field_name_ t_) EB_) field_name_t_EB_list))))
 ==> 
JTtypedef ([((TD_td type_params_opt typeconstr_name (TI_def (TR_record ((List.map (fun (field_name_,t_,EB_) -> (FD_immutable field_name_ t_)) field_name_t_EB_list))))))] ++ typedef_list)  (  (EB_tr typeconstr_name kind ((List.map (fun (field_name_,t_,EB_) -> field_name_) field_name_t_EB_list)))  :: E )  E'  (List.concat (List.reverse  ([(E'')] ++ [( (List.reverse  ((List.map (fun (field_name_,t_,EB_) -> EB_) field_name_t_EB_list)) ) )]) )) 


(** definitions *)
(* defns JTtype_definition *)
indreln
[JTtype_definition : environment -> type_definition -> environment -> bool witness type JTtype_definition_witness; check JTtype_definition_check;]
(* defn type_definition *)

JTtype_definition_list: forall typedef_list E E'''' E' E'' E''' .
(JTtypedef (typedef_list) E' E'' E''') &&
( ( E''''  =   (List.concat (List.reverse  ([(E')] ++ [(E'')] ++ [(E''')]) ))  ) ) &&
(JTEok  (List.concat (List.reverse  ([(E)] ++ [(E'''')]) )) )
 ==> 
JTtype_definition E (TDF_tdf (typedef_list)) E''''

and
JTtype_definition_swap: forall typedef''_list typedef_list E typedef typedef' E' .
(JTtype_definition E (TDF_tdf (typedef_list ++ [(typedef')] ++ [(typedef)] ++ typedef''_list)) E')
 ==> 
JTtype_definition E (TDF_tdf (typedef_list ++ [(typedef)] ++ [(typedef')] ++ typedef''_list)) E'


(** definitions *)
(* defns JTdefinition *)
indreln
[JTdefinition : environment -> definition -> environment -> bool witness type JTdefinition_witness; check JTdefinition_check;]
(* defn definition *)

JTdefinition_let_poly: forall x_t'_list E pat nexp Tsigma .
(is_non_expansive_of_expr nexp) &&
(JTlet_binding Tsigma  ( EB_tv :: E )  (LB_simple pat nexp)  (List.reverse  ((List.map (fun (x_,t_') ->   (EB_vn  x_  (TS_forall (shiftt 0 1  t_' )))  ) x_t'_list)) ) )
 ==> 
JTdefinition E (D_let (LB_simple pat nexp))  (List.reverse  ((List.map (fun (x_,t_') ->  (EB_vn x_ (TS_forall t_')) ) x_t'_list)) ) 

and
JTdefinition_let_mono: forall x_t'_list E pat expr Tsigma .
(JTlet_binding Tsigma E (LB_simple pat expr)  (List.reverse  ((List.map (fun (x_,t_') ->   (EB_vn  x_  (TS_forall (shiftt 0 1  t_' )))  ) x_t'_list)) ) )
 ==> 
JTdefinition E (D_let (LB_simple pat expr))  (List.reverse  ((List.map (fun (x_,t_') ->   (EB_vn  x_  (TS_forall (shiftt 0 1  t_' )))  ) x_t'_list)) ) 

and
JTdefinition_letrec: forall x_t'_list E letrec_bindings Tsigma .
(JTletrec_binding Tsigma  ( EB_tv :: E )  letrec_bindings  (List.reverse  ((List.map (fun (x_,t_') ->   (EB_vn  x_  (TS_forall (shiftt 0 1  t_' )))  ) x_t'_list)) ) )
 ==> 
JTdefinition E (D_letrec letrec_bindings)  (List.reverse  ((List.map (fun (x_,t_') ->  (EB_vn x_ (TS_forall t_')) ) x_t'_list)) ) 

and
JTdefinition_typedef: forall typedef_list E E' .
(JTtype_definition E (TDF_tdf (typedef_list)) E')
 ==> 
JTdefinition E (D_type (TDF_tdf (typedef_list))) E'

and
JTdefinition_exndef: forall E constr_decl EB .
(JTEok E) &&
(JTconstr_decl  (TPS_nary [])  TC_exn constr_decl EB)
 ==> 
JTdefinition E (D_exception (ED_def constr_decl))  (List.reverse  ([(EB)]) ) 


(** definitions *)
(* defns JTdefinitions *)
indreln
[JTdefinitions : environment -> definitions -> environment -> bool witness type JTdefinitions_witness; check JTdefinitions_check;]
(* defn definitions *)

JTdefinitions_empty: forall E .
(JTEok E)
 ==> 
JTdefinitions E Ds_nil  (List.reverse  [] ) 

and
JTdefinitions_item: forall E definition definitions' E' E'' .
(JTdefinition E definition E') &&
(JTdefinitions  (List.concat (List.reverse  ([(E)] ++ [(E')]) ))  definitions' E'')
 ==> 
JTdefinitions E (Ds_cons definition definitions')  (List.concat (List.reverse  ([(E')] ++ [(E'')]) )) 


(** definitions *)
(* defns JTprog *)
indreln
[JTprog : environment -> program -> environment -> bool witness type JTprog_witness; check JTprog_check;]
(* defn prog *)

JTprog_defs: forall E definitions E' .
(JTdefinitions E definitions E')
 ==> 
JTprog E (Prog_defs definitions) E'

and
JTprog_raise: forall E v Tsigma t .
(is_value_of_expr v) &&
(JTe Tsigma E v t)
 ==> 
JTprog E (Prog_raise v)  (List.reverse  [] ) 


(** definitions *)
(* defns JTstore *)
indreln
[JTstore : environment -> store -> environment -> bool witness type JTstore_witness; check JTstore_check;]
(* defn store *)

JTstore_empty: forall E .
true
 ==> 
JTstore E  []   (List.reverse  [] ) 

and
JTstore_map: forall E store l v E' t .
(is_value_of_expr v) &&
(JTstore E store E') &&
(JTe  []  E v t)
 ==> 
JTstore E  (( l ,  v ):: store )   (  (EB_l l t)  :: E' ) 


(** definitions *)
(* defns JTtop *)
indreln
[JTtop : environment -> program -> store -> environment -> bool witness type JTtop_witness; check JTtop_check;]
(* defn top *)

JTtop_defs: forall E program store E' E'' .
(JTstore  (List.concat (List.reverse  ([(E)] ++ [(E')]) ))  store E') &&
(JTprog  (List.concat (List.reverse  ([(E)] ++ [(E')]) ))  program E'')
 ==> 
JTtop E program store  (List.concat (List.reverse  ([(E')] ++ [(E'')]) )) 


(** definitions *)
(* defns JTLin *)
indreln
[JTLin : Tsigma -> environment -> trans_label -> bool witness type JTLin_witness; check JTLin_check;]
(* defn Lin *)

JTLin_nil: forall Tsigma E .
true
 ==> 
JTLin Tsigma E Lab_nil

and
JTLin_alloc: forall Tsigma E v location names .
(JdomE E names) &&
( (not (List.elem  (Name_l location)   names )) )
 ==> 
JTLin Tsigma E (Lab_alloc v location)

and
JTLin_deref: forall Tsigma E location v t .
(is_value_of_expr v) &&
(JTe Tsigma E v t) &&
(Jlookup_EB E (Name_l location)  (EB_l location t) )
 ==> 
JTLin Tsigma E (Lab_deref location v)

and
JTLin_assign: forall Tsigma E location v .
true
 ==> 
JTLin Tsigma E (Lab_assign location v)


(** definitions *)
(* defns JTLout *)
indreln
[JTLout : Tsigma -> environment -> trans_label -> environment -> bool witness type JTLout_witness; check JTLout_check;]
(* defn Lout *)

JTLout_nil: forall Tsigma E .
true
 ==> 
JTLout Tsigma E Lab_nil  (List.reverse  [] ) 

and
JTLout_alloc: forall Tsigma E location t v .
(is_value_of_expr v) &&
(JTe Tsigma E v t)
 ==> 
JTLout Tsigma E (Lab_alloc v location)  (List.reverse  ([( (EB_l location t) )]) ) 

and
JTLout_deref: forall Tsigma E location v .
true
 ==> 
JTLout Tsigma E (Lab_deref location v)  (List.reverse  [] ) 

and
JTLout_assign: forall Tsigma E location v t .
(is_value_of_expr v) &&
(JTe Tsigma E v t) &&
(Jlookup_EB E (Name_l location)  (EB_l location t) )
 ==> 
JTLout Tsigma E (Lab_assign location v)  (List.reverse  [] ) 


(** definitions *)
(* defns JmatchP *)
indreln
[JM_matchP : expr -> patternl -> bool]
(* defn matchP *)

JM_matchP_var: forall v x .
(is_value_of_expr v)
 ==> 
JM_matchP v (P_var x)

and
JM_matchP_any: forall v .
(is_value_of_expr v)
 ==> 
JM_matchP v P_any

and
JM_matchP_constant: forall constantl .
true
 ==> 
JM_matchP (Expr_constant constantl) (P_constant constantl)

and
JM_matchP_alias: forall v pat x .
(is_value_of_expr v) &&
(JM_matchP v pat)
 ==> 
JM_matchP v (P_alias pat x)

and
JM_matchP_typed: forall v pat t .
(is_value_of_expr v) &&
(JM_matchP v pat)
 ==> 
JM_matchP v (P_typed pat t)

and
JM_matchP_or_left: forall v pat1 pat2 .
(is_value_of_expr v) &&
(JM_matchP v pat1)
 ==> 
JM_matchP v (P_or pat1 pat2)

and
JM_matchP_or_right: forall v pat1 pat2 .
(is_value_of_expr v) &&
(JM_matchP v pat2)
 ==> 
JM_matchP v (P_or pat1 pat2)

and
JM_matchP_construct: forall v_pat_list constr .
(List.all (fun (v_,pat_) -> is_value_of_expr v_) v_pat_list) &&
((List.all (fun b -> b) ((List.map (fun (v_,pat_) -> JM_matchP v_ pat_) v_pat_list))))
 ==> 
JM_matchP (Expr_construct constr ((List.map (fun (v_,pat_) -> v_) v_pat_list))) (P_construct constr ((List.map (fun (v_,pat_) -> pat_) v_pat_list)))

and
JM_matchP_construct_any: forall v_list constr .
(List.all (fun v_ -> is_value_of_expr v_) v_list)
 ==> 
JM_matchP (Expr_construct constr (v_list)) (P_construct_any constr)

and
JM_matchP_tuple: forall v_pat_list .
(List.all (fun (v_,pat_) -> is_value_of_expr v_) v_pat_list) &&
((List.all (fun b -> b) ((List.map (fun (v_,pat_) -> JM_matchP v_ pat_) v_pat_list))))
 ==> 
JM_matchP  (Expr_tuple ((List.map (fun (v_,pat_) -> v_) v_pat_list)))   (P_tuple ((List.map (fun (v_,pat_) -> pat_) v_pat_list))) 

and
JM_matchP_record: forall fn_v''_list field_name'_pat_v'_list field_name_v_list .
(List.all (fun (fn_,v_'') -> is_value_of_expr v_'') fn_v''_list) &&
(List.all (fun (field_name_',pat_,v_') -> is_value_of_expr v_') field_name'_pat_v'_list) &&
(List.all (fun (field_name_,v_) -> is_value_of_expr v_) field_name_v_list) &&
( (list_perm ( ((List.map (fun (field_name_',pat_,v_') -> (field_name_',v_')) field_name'_pat_v'_list) ++ fn_v''_list) ) ( (field_name_v_list) )) ) &&
((List.all (fun b -> b) ((List.map (fun (field_name_',pat_,v_') -> JM_matchP v_' pat_) field_name'_pat_v'_list)))) &&
( (list_distinct ( ((List.map (fun (field_name_,v_) -> (Name_fn field_name_)) field_name_v_list)) )) )
 ==> 
JM_matchP (Expr_record ((List.map (fun (field_name_,v_) -> ((F_name field_name_),v_)) field_name_v_list))) (P_record ((List.map (fun (field_name_',pat_,v_') -> ((F_name field_name_'),pat_)) field_name'_pat_v'_list)))

and
JM_matchP_cons: forall v1 v2 pat1 pat2 .
(is_value_of_expr v1) &&
(is_value_of_expr v2) &&
(JM_matchP v1 pat1) &&
(JM_matchP v2 pat2)
 ==> 
JM_matchP (Expr_cons v1 v2) (P_cons pat1 pat2)


(** definitions *)
(* defns Jmatch *)
indreln
[JM_match : expr -> patternl -> substs_x -> bool]
(* defn match *)

JM_match_var: forall v x .
(is_value_of_expr v)
 ==> 
JM_match v (P_var x) (Substs_x_xs ([(x,v)]))

and
JM_match_any: forall v .
(is_value_of_expr v)
 ==> 
JM_match v P_any (Substs_x_xs [])

and
JM_match_constant: forall constantl .
true
 ==> 
JM_match (Expr_constant constantl) (P_constant constantl) (Substs_x_xs [])

and
JM_match_alias: forall x_v_list v pat x .
(is_value_of_expr v) &&
(List.all (fun (x_,v_) -> is_value_of_expr v_) x_v_list) &&
(JM_match v pat (Substs_x_xs (x_v_list)))
 ==> 
JM_match v (P_alias pat x) (Substs_x_xs (x_v_list ++ [(x,v)]))

and
JM_match_typed: forall x_v_list v pat t .
(is_value_of_expr v) &&
(List.all (fun (x_,v_) -> is_value_of_expr v_) x_v_list) &&
(JM_match v pat (Substs_x_xs (x_v_list)))
 ==> 
JM_match v (P_typed pat t) (Substs_x_xs (x_v_list))

and
JM_match_or_left: forall x_v_list v pat1 pat2 .
(is_value_of_expr v) &&
(List.all (fun (x_,v_) -> is_value_of_expr v_) x_v_list) &&
(JM_match v pat1 (Substs_x_xs (x_v_list)))
 ==> 
JM_match v (P_or pat1 pat2) (Substs_x_xs (x_v_list))

and
JM_match_or_right: forall x_v_list pat1 pat2 v .
(is_value_of_expr v) &&
(List.all (fun (x_,v_) -> is_value_of_expr v_) x_v_list) &&
( (not (JM_matchP  v   pat1 )) ) &&
(JM_match v pat2 (Substs_x_xs (x_v_list)))
 ==> 
JM_match v (P_or pat1 pat2) (Substs_x_xs (x_v_list))

and
JM_match_construct: forall v_pat_substs_x_list constr .
(List.all (fun (v_,pat_,substs_x_) -> is_value_of_expr v_) v_pat_substs_x_list) &&
((List.all (fun b -> b) ((List.map (fun (v_,pat_,substs_x_) -> JM_match v_ pat_ substs_x_) v_pat_substs_x_list))))
 ==> 
JM_match (Expr_construct constr ((List.map (fun (v_,pat_,substs_x_) -> v_) v_pat_substs_x_list))) (P_construct constr ((List.map (fun (v_,pat_,substs_x_) -> pat_) v_pat_substs_x_list)))  (Substs_x_xs (List.concat (List.map (fun x -> match x with Substs_x_xs l -> l end)  ((List.map (fun (v_,pat_,substs_x_) -> substs_x_) v_pat_substs_x_list)) ))) 

and
JM_match_construct_any: forall v_list constr .
(List.all (fun v_ -> is_value_of_expr v_) v_list)
 ==> 
JM_match (Expr_construct constr (v_list)) (P_construct_any constr) (Substs_x_xs [])

and
JM_match_tuple: forall v_pat_substs_x_list .
(List.all (fun (v_,pat_,substs_x_) -> is_value_of_expr v_) v_pat_substs_x_list) &&
((List.all (fun b -> b) ((List.map (fun (v_,pat_,substs_x_) -> JM_match v_ pat_ substs_x_) v_pat_substs_x_list))))
 ==> 
JM_match  (Expr_tuple ((List.map (fun (v_,pat_,substs_x_) -> v_) v_pat_substs_x_list)))   (P_tuple ((List.map (fun (v_,pat_,substs_x_) -> pat_) v_pat_substs_x_list)))   (Substs_x_xs (List.concat (List.map (fun x -> match x with Substs_x_xs l -> l end)  ((List.map (fun (v_,pat_,substs_x_) -> substs_x_) v_pat_substs_x_list)) ))) 

and
JM_match_record: forall fn_v''_list field_name'_pat_substs_x_v'_list field_name_v_list .
(List.all (fun (fn_,v_'') -> is_value_of_expr v_'') fn_v''_list) &&
(List.all (fun (field_name_',pat_,substs_x_,v_') -> is_value_of_expr v_') field_name'_pat_substs_x_v'_list) &&
(List.all (fun (field_name_,v_) -> is_value_of_expr v_) field_name_v_list) &&
( (list_perm ( ((List.map (fun (field_name_',pat_,substs_x_,v_') -> (field_name_',v_')) field_name'_pat_substs_x_v'_list) ++ fn_v''_list) ) ( (field_name_v_list) )) ) &&
((List.all (fun b -> b) ((List.map (fun (field_name_',pat_,substs_x_,v_') -> JM_match v_' pat_ substs_x_) field_name'_pat_substs_x_v'_list)))) &&
( (list_distinct ( ((List.map (fun (field_name_,v_) -> (Name_fn field_name_)) field_name_v_list)) )) )
 ==> 
JM_match (Expr_record ((List.map (fun (field_name_,v_) -> ((F_name field_name_),v_)) field_name_v_list))) (P_record ((List.map (fun (field_name_',pat_,substs_x_,v_') -> ((F_name field_name_'),pat_)) field_name'_pat_substs_x_v'_list)))  (Substs_x_xs (List.concat (List.map (fun x -> match x with Substs_x_xs l -> l end)  ((List.map (fun (field_name_',pat_,substs_x_,v_') -> substs_x_) field_name'_pat_substs_x_v'_list)) ))) 

and
JM_match_cons: forall v1 v2 pat1 pat2 substs_x1 substs_x2 .
(is_value_of_expr v1) &&
(is_value_of_expr v2) &&
(JM_match v1 pat1 substs_x1) &&
(JM_match v2 pat2 substs_x2)
 ==> 
JM_match (Expr_cons v1 v2) (P_cons pat1 pat2)  (Substs_x_xs (List.concat (List.map (fun x -> match x with Substs_x_xs l -> l end)  ([(substs_x1)] ++ [(substs_x2)]) ))) 


(** definitions *)
(* defns Jrecfun *)
indreln
[Jrecfun : letrec_bindings -> pattern_matching -> expr -> bool]
(* defn recfun *)

Jrecfun_letrec: forall x_pattern_matching_list letrec_bindings pattern_matching .
( ( letrec_bindings  =  (LRBs_inj ((List.map (fun (x_,pattern_matching_) -> (LRB_simple x_ pattern_matching_)) x_pattern_matching_list))) ) )
 ==> 
Jrecfun letrec_bindings pattern_matching  (substs_value_name_expr (match  (Substs_x_xs ((List.map (fun (x_,pattern_matching_) -> (x_,(Expr_letrec letrec_bindings (Expr_ident x_)))) x_pattern_matching_list)))  with Substs_x_xs l -> l end)   (Expr_function pattern_matching)  ) 


(** definitions *)
(* defns Jfunval *)
indreln
[Jfunval : expr -> bool]
(* defn funval *)

Jfunval_up: forall unary_prim .
true
 ==> 
Jfunval (Expr_uprim unary_prim)

and
Jfunval_bp: forall binary_prim .
true
 ==> 
Jfunval (Expr_bprim binary_prim)

and
Jfunval_bp_app: forall binary_prim v .
(is_value_of_expr v)
 ==> 
Jfunval (Expr_apply (Expr_bprim binary_prim) v)

and
Jfunval_func: forall pattern_matching .
true
 ==> 
Jfunval (Expr_function pattern_matching)


(** definitions *)
(* defns JRuprim *)
indreln
[JRuprim : unary_prim -> expr -> labelled_arrow -> expr -> bool]
(* defn Ruprim *)

Juprim_not_true: forall .
true
 ==> 
JRuprim Uprim_not (Expr_constant CONST_true)  Lab_nil  (Expr_constant CONST_false)

and
Juprim_not_false: forall .
true
 ==> 
JRuprim Uprim_not (Expr_constant CONST_false)  Lab_nil  (Expr_constant CONST_true)

and
Juprim_uminus: forall intn .
true
 ==> 
JRuprim Uprim_minus (Expr_constant (CONST_int intn))  Lab_nil  (Expr_constant (CONST_int  (  0   -  intn ) ))

and
Juprim_ref_alloc: forall v l .
(is_value_of_expr v)
 ==> 
JRuprim Uprim_ref v   (Lab_alloc v l)   (Expr_location l)

and
Juprim_deref: forall l v .
(is_value_of_expr v)
 ==> 
JRuprim Uprim_deref (Expr_location l)   (Lab_deref l v)   v


(** definitions *)
(* defns JRbprim *)
indreln
[JRbprim : expr -> binary_prim -> expr -> labelled_arrow -> expr -> bool]
(* defn Rbprim *)

Jbprim_equal_fun: forall v v' .
(is_value_of_expr v) &&
(is_value_of_expr v') &&
(Jfunval v)
 ==> 
JRbprim v Bprim_equal v'  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise)  (Expr_construct C_invalidargument ([((Expr_constant  (CONST_string "equal: functional value") ))])) )

and
Jbprim_equal_const_true: forall constantl .
true
 ==> 
JRbprim (Expr_constant constantl) Bprim_equal (Expr_constant constantl)  Lab_nil  (Expr_constant CONST_true)

and
Jbprim_equal_const_false: forall constantl constantl' .
( (not ( constantl  =  constantl' )) )
 ==> 
JRbprim (Expr_constant constantl) Bprim_equal (Expr_constant constantl')  Lab_nil  (Expr_constant CONST_false)

and
Jbprim_equal_loc: forall l l' .
true
 ==> 
JRbprim (Expr_location l) Bprim_equal (Expr_location l')  Lab_nil  (Expr_apply  (Expr_apply (Expr_bprim Bprim_equal)  (Expr_apply (Expr_uprim Uprim_deref) (Expr_location l)) )   (Expr_apply (Expr_uprim Uprim_deref) (Expr_location l')) )

and
Jbprim_equal_cons: forall v1 v2 v1' v2' .
(is_value_of_expr v1) &&
(is_value_of_expr v2) &&
(is_value_of_expr v1') &&
(is_value_of_expr v2')
 ==> 
JRbprim  (Expr_cons v1 v2)  Bprim_equal  (Expr_cons v1' v2')   Lab_nil  (Expr_and  (Expr_apply  (Expr_apply (Expr_bprim Bprim_equal) v1)  v1')   (Expr_apply  (Expr_apply (Expr_bprim Bprim_equal) v2)  v2') )

and
Jbprim_equal_cons_nil: forall v1 v2 .
(is_value_of_expr v1) &&
(is_value_of_expr v2)
 ==> 
JRbprim  (Expr_cons v1 v2)  Bprim_equal (Expr_constant CONST_nil)  Lab_nil  (Expr_constant CONST_false)

and
Jbprim_equal_nil_cons: forall v1 v2 .
(is_value_of_expr v1) &&
(is_value_of_expr v2)
 ==> 
JRbprim (Expr_constant CONST_nil) Bprim_equal  (Expr_cons v1 v2)   Lab_nil  (Expr_constant CONST_false)

and
Jbprim_equal_tuple: forall v_v'_list .
(List.all (fun (v_,v_') -> is_value_of_expr v_) v_v'_list) &&
(List.all (fun (v_,v_') -> is_value_of_expr v_') v_v'_list) &&
( (List.length ( ((List.map (fun (v_,v_') -> v_) v_v'_list)) ) >=  2 ) )
 ==> 
JRbprim  (Expr_tuple ((List.map (fun (v_,v_') -> v_) v_v'_list)))  Bprim_equal  (Expr_tuple ((List.map (fun (v_,v_') -> v_') v_v'_list)))   Lab_nil   (List.foldr Expr_and (Expr_constant CONST_true)  ((List.map (fun (v_,v_') -> (Expr_apply  (Expr_apply (Expr_bprim Bprim_equal) v_)  v_')) v_v'_list)) ) 

and
Jbprim_equal_constr: forall v_v'_list constr .
(List.all (fun (v_,v_') -> is_value_of_expr v_) v_v'_list) &&
(List.all (fun (v_,v_') -> is_value_of_expr v_') v_v'_list)
 ==> 
JRbprim  (Expr_construct constr ((List.map (fun (v_,v_') -> v_) v_v'_list)))  Bprim_equal  (Expr_construct constr ((List.map (fun (v_,v_') -> v_') v_v'_list)))   Lab_nil   (List.foldr Expr_and (Expr_constant CONST_true)  ((List.map (fun (v_,v_') -> (Expr_apply  (Expr_apply (Expr_bprim Bprim_equal) v_)  v_')) v_v'_list)) ) 

and
Jbprim_equal_constr_false: forall v'_list v_list constr constr' .
(List.all (fun v_' -> is_value_of_expr v_') v'_list) &&
(List.all (fun v_ -> is_value_of_expr v_) v_list) &&
( (not ( (CONST_constr constr)  =  (CONST_constr constr') )) )
 ==> 
JRbprim (Expr_construct constr (v_list)) Bprim_equal (Expr_construct constr' (v'_list))  Lab_nil  (Expr_constant CONST_false)

and
Jbprim_equal_const_constr_false: forall v_list constr' constr .
(List.all (fun v_ -> is_value_of_expr v_) v_list)
 ==> 
JRbprim (Expr_constant (CONST_constr constr')) Bprim_equal (Expr_construct constr (v_list))  Lab_nil  (Expr_constant CONST_false)

and
Jbprim_equal_constr_const_false: forall v_list constr constr' .
(List.all (fun v_ -> is_value_of_expr v_) v_list)
 ==> 
JRbprim (Expr_construct constr (v_list)) Bprim_equal (Expr_constant (CONST_constr constr'))  Lab_nil  (Expr_constant CONST_false)

and
Jbprim_equal_rec: forall fn''_v''_list fn_v_list v' .
(is_value_of_expr v') &&
(List.all (fun (fn_'',v_'') -> is_value_of_expr v_'') fn''_v''_list) &&
(List.all (fun (fn_,v_) -> is_value_of_expr v_) fn_v_list) &&
( ( v'  =  (Expr_record ((List.map (fun (fn_'',v_'') -> ((F_name fn_''),v_'')) fn''_v''_list))) ) ) &&
( (list_perm ( ((List.map (fun (fn_,v_) -> fn_) fn_v_list)) ) ( ((List.map (fun (fn_'',v_'') -> fn_'') fn''_v''_list)) )) )
 ==> 
JRbprim (Expr_record ((List.map (fun (fn_,v_) -> ((F_name fn_),v_)) fn_v_list))) Bprim_equal v'  Lab_nil   (List.foldr Expr_and (Expr_constant CONST_true)  ((List.map (fun (fn_,v_) -> (Expr_apply  (Expr_apply (Expr_bprim Bprim_equal) v_)   (Expr_field v' (F_name fn_)) )) fn_v_list)) ) 

and
Jbprim_plus: forall intn1 intn2 .
true
 ==> 
JRbprim (Expr_constant (CONST_int intn1)) Bprim_plus (Expr_constant (CONST_int intn2))  Lab_nil  (Expr_constant (CONST_int  ( intn1  +  intn2 ) ))

and
Jbprim_minus: forall intn1 intn2 .
true
 ==> 
JRbprim (Expr_constant (CONST_int intn1)) Bprim_minus (Expr_constant (CONST_int intn2))  Lab_nil  (Expr_constant (CONST_int  ( intn1  -  intn2 ) ))

and
Jbprim_times: forall intn1 intn2 .
true
 ==> 
JRbprim (Expr_constant (CONST_int intn1)) Bprim_times (Expr_constant (CONST_int intn2))  Lab_nil  (Expr_constant (CONST_int  ( intn1  *  intn2 ) ))

and
Jbprim_div0: forall intn .
true
 ==> 
JRbprim (Expr_constant (CONST_int intn)) Bprim_div (Expr_constant (CONST_int  0 ))  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_div_by_0)))

and
Jbprim_div: forall intn1 intn2 .
( (not ( (CONST_int intn2)  =  (CONST_int  0 ) )) )
 ==> 
JRbprim (Expr_constant (CONST_int intn1)) Bprim_div (Expr_constant (CONST_int intn2))  Lab_nil  (Expr_constant (CONST_int  ( intn1  /  intn2 ) ))

and
Jbprim_assign: forall l v .
(is_value_of_expr v)
 ==> 
JRbprim (Expr_location l) Bprim_assign v   (Lab_assign l v)   (Expr_constant CONST_unit)


(** definitions *)
(* defns JRmatching_step *)
indreln
[JRmatching_step : expr -> pattern_matching -> pattern_matching -> bool]
(* defn matching_step *)

JRmatching_next: forall pat_e_list pat e v .
(is_value_of_expr v) &&
( (not (JM_matchP  v   pat )) ) &&
( (List.length ( ((List.map (fun (pat_,e_) -> e_) pat_e_list)) ) >=  1 ) )
 ==> 
JRmatching_step v (PM_pm ([((PE_inj pat e))] ++ (List.map (fun (pat_,e_) -> (PE_inj pat_ e_)) pat_e_list))) (PM_pm ((List.map (fun (pat_,e_) -> (PE_inj pat_ e_)) pat_e_list)))


(** definitions *)
(* defns JRmatching_success *)
indreln
[JRmatching_success : expr -> pattern_matching -> expr -> bool]
(* defn matching_success *)

JRmatching_found: forall x_v_list pat_e_list v pat e .
(is_value_of_expr v) &&
(List.all (fun (x_,v_) -> is_value_of_expr v_) x_v_list) &&
(JM_match v pat (Substs_x_xs (x_v_list)))
 ==> 
JRmatching_success v (PM_pm ([((PE_inj pat e))] ++ (List.map (fun (pat_,e_) -> (PE_inj pat_ e_)) pat_e_list)))  (substs_value_name_expr (match  (Substs_x_xs (x_v_list))  with Substs_x_xs l -> l end)  e ) 

and
JRmatching_fail: forall pat e v .
(is_value_of_expr v) &&
( (not (JM_matchP  v   pat )) )
 ==> 
JRmatching_success v (PM_pm ([((PE_inj pat e))])) (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_matchfailure)))


(** definitions *)
(* defns Jred *)
indreln
[JR_expr : expr -> labelled_arrow -> expr -> bool]
(* defn expr *)

JR_expr_uprim: forall unary_prim v L e .
(is_value_of_expr v) &&
(JRuprim unary_prim v  L  e)
 ==> 
JR_expr (Expr_apply (Expr_uprim unary_prim) v)  L  e

and
JR_expr_bprim: forall binary_prim v1 v2 L e .
(is_value_of_expr v1) &&
(is_value_of_expr v2) &&
(JRbprim v1 binary_prim v2  L  e)
 ==> 
JR_expr (Expr_apply  (Expr_apply (Expr_bprim binary_prim) v1)  v2)  L  e

and
JR_expr_typed_ctx: forall e t .
true
 ==> 
JR_expr (Expr_typed e t)  Lab_nil  e

and
JR_expr_apply_ctx_arg: forall e1 e0 L e0' .
(JR_expr e0  L  e0')
 ==> 
JR_expr (Expr_apply e1 e0)  L  (Expr_apply e1 e0')

and
JR_expr_apply_raise1: forall e v .
(is_value_of_expr v)
 ==> 
JR_expr (Expr_apply e  (Expr_apply (Expr_uprim Uprim_raise) v) )  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_apply_ctx_fun: forall e1 v0 L e1' .
(is_value_of_expr v0) &&
(JR_expr e1  L  e1')
 ==> 
JR_expr (Expr_apply e1 v0)  L  (Expr_apply e1' v0)

and
JR_expr_apply_raise2: forall v v' .
(is_value_of_expr v) &&
(is_value_of_expr v')
 ==> 
JR_expr (Expr_apply  (Expr_apply (Expr_uprim Uprim_raise) v)  v')  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_apply: forall pattern_matching v0 .
(is_value_of_expr v0)
 ==> 
JR_expr  (Expr_apply (Expr_function pattern_matching) v0)   Lab_nil  (Expr_match v0 pattern_matching)

and
JR_expr_let_ctx: forall pat e0 e L e0' .
(JR_expr e0  L  e0')
 ==> 
JR_expr (Expr_let (LB_simple pat e0) e)  L  (Expr_let (LB_simple pat e0') e)

and
JR_expr_let_raise: forall pat v e .
(is_value_of_expr v)
 ==> 
JR_expr (Expr_let (LB_simple pat (Expr_apply (Expr_uprim Uprim_raise) v)) e)  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_let_subst: forall x_v_list pat v e .
(is_value_of_expr v) &&
(List.all (fun (x_,v_) -> is_value_of_expr v_) x_v_list) &&
(JM_match v pat (Substs_x_xs (x_v_list)))
 ==> 
JR_expr (Expr_let (LB_simple pat v) e)  Lab_nil   (substs_value_name_expr (match  (Substs_x_xs (x_v_list))  with Substs_x_xs l -> l end)  e ) 

and
JR_expr_let_fail: forall pat e v .
(is_value_of_expr v) &&
( (not (JM_matchP  v   pat )) )
 ==> 
JR_expr (Expr_let (LB_simple pat v) e)  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_matchfailure)))

and
JR_expr_letrec: forall x_e_pattern_matching_list letrec_bindings e .
( ( letrec_bindings  =  (LRBs_inj ((List.map (fun (x_,e_,pattern_matching_) -> (LRB_simple x_ pattern_matching_)) x_e_pattern_matching_list))) ) ) &&
((List.all (fun b -> b) ((List.map (fun (x_,e_,pattern_matching_) -> Jrecfun letrec_bindings pattern_matching_ e_) x_e_pattern_matching_list))))
 ==> 
JR_expr (Expr_letrec letrec_bindings e)  Lab_nil   (substs_value_name_expr (match  (Substs_x_xs ((List.map (fun (x_,e_,pattern_matching_) -> (x_,e_)) x_e_pattern_matching_list)))  with Substs_x_xs l -> l end)  e ) 

and
JR_expr_sequence_ctx_left: forall e1 e2 L e1' .
(JR_expr e1  L  e1')
 ==> 
JR_expr (Expr_sequence e1 e2)  L  (Expr_sequence e1' e2)

and
JR_expr_sequence_raise: forall v e .
(is_value_of_expr v)
 ==> 
JR_expr (Expr_sequence  (Expr_apply (Expr_uprim Uprim_raise) v)  e)  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_sequence: forall v e2 .
(is_value_of_expr v)
 ==> 
JR_expr (Expr_sequence v e2)  Lab_nil  e2

and
JR_expr_ifthenelse_ctx: forall e1 e2 e3 L e1' .
(JR_expr e1  L  e1')
 ==> 
JR_expr (Expr_ifthenelse e1 e2 e3)  L  (Expr_ifthenelse e1' e2 e3)

and
JR_expr_if_raise: forall v e1 e2 .
(is_value_of_expr v)
 ==> 
JR_expr (Expr_ifthenelse (Expr_apply (Expr_uprim Uprim_raise) v) e1 e2)  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_ifthenelse_true: forall e2 e3 .
true
 ==> 
JR_expr (Expr_ifthenelse (Expr_constant CONST_true) e2 e3)  Lab_nil  e2

and
JR_expr_ifthenelse_false: forall e2 e3 .
true
 ==> 
JR_expr (Expr_ifthenelse (Expr_constant CONST_false) e2 e3)  Lab_nil  e3

and
JR_expr_match_ctx: forall e pattern_matching L e' .
(JR_expr e  L  e')
 ==> 
JR_expr (Expr_match e pattern_matching)  L  (Expr_match e' pattern_matching)

and
JR_expr_match_raise: forall v pattern_matching .
(is_value_of_expr v)
 ==> 
JR_expr (Expr_match (Expr_apply (Expr_uprim Uprim_raise) v) pattern_matching)  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_match_step: forall v pattern_matching pattern_matching' .
(is_value_of_expr v) &&
(JRmatching_step v pattern_matching pattern_matching')
 ==> 
JR_expr (Expr_match v pattern_matching)  Lab_nil  (Expr_match v pattern_matching')

and
JR_expr_match_success: forall v pattern_matching e' .
(is_value_of_expr v) &&
(JRmatching_success v pattern_matching e')
 ==> 
JR_expr (Expr_match v pattern_matching)  Lab_nil  e'

and
JR_expr_and: forall e1 e2 .
true
 ==> 
JR_expr (Expr_and e1 e2)  Lab_nil  (Expr_ifthenelse e1 e2 (Expr_constant CONST_false))

and
JR_expr_or: forall e1 e2 .
true
 ==> 
JR_expr (Expr_or e1 e2)  Lab_nil  (Expr_ifthenelse e1 (Expr_constant CONST_true) e2)

and
JR_expr_while: forall e1 e2 .
true
 ==> 
JR_expr (Expr_while e1 e2)  Lab_nil   (Expr_ifthenelse  e1    (Expr_sequence e2 (Expr_while e1 e2))   (Expr_constant CONST_unit)) 

and
JR_expr_for_ctx1: forall x e1 for_dirn e2 e3 L e1' .
(JR_expr e1  L  e1')
 ==> 
JR_expr (Expr_for x e1 for_dirn e2 e3)  L  (Expr_for x e1' for_dirn e2 e3)

and
JR_expr_for_raise1: forall x v for_dirn e2 e3 .
(is_value_of_expr v)
 ==> 
JR_expr (Expr_for x (Expr_apply (Expr_uprim Uprim_raise) v) for_dirn e2 e3)  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_for_ctx2: forall x v1 for_dirn e2 e3 L e2' .
(is_value_of_expr v1) &&
(JR_expr e2  L  e2')
 ==> 
JR_expr (Expr_for x v1 for_dirn e2 e3)  L  (Expr_for x v1 for_dirn e2' e3)

and
JR_expr_for_raise2: forall x v for_dirn v' e3 .
(is_value_of_expr v) &&
(is_value_of_expr v')
 ==> 
JR_expr (Expr_for x v for_dirn (Expr_apply (Expr_uprim Uprim_raise) v') e3)  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v')

and
JR_expr_for_to_do: forall x intn1 intn2 e .
( ( intn1  <=  intn2 ) )
 ==> 
JR_expr (Expr_for x (Expr_constant (CONST_int intn1)) FD_upto (Expr_constant (CONST_int intn2)) e)  Lab_nil  (Expr_sequence  (Expr_let (LB_simple (P_var x) (Expr_constant (CONST_int intn1))) e)  (Expr_for x (Expr_constant (CONST_int  ( intn1  +   1  ) )) FD_upto (Expr_constant (CONST_int intn2)) e))

and
JR_expr_for_to_done: forall x intn1 intn2 e .
( ( intn1  >  intn2 ) )
 ==> 
JR_expr (Expr_for x (Expr_constant (CONST_int intn1)) FD_upto (Expr_constant (CONST_int intn2)) e)  Lab_nil  (Expr_constant CONST_unit)

and
JR_expr_for_downto_do: forall x intn1 intn2 e .
( ( intn2  <=  intn1 ) )
 ==> 
JR_expr (Expr_for x (Expr_constant (CONST_int intn1)) FD_downto (Expr_constant (CONST_int intn2)) e)  Lab_nil  (Expr_sequence  (Expr_let (LB_simple (P_var x) (Expr_constant (CONST_int intn1))) e)  (Expr_for x (Expr_constant (CONST_int  ( intn1  -   1  ) )) FD_downto (Expr_constant (CONST_int intn2)) e))

and
JR_expr_for_downto_done: forall x intn1 intn2 e .
( ( intn2  >  intn1 ) )
 ==> 
JR_expr (Expr_for x (Expr_constant (CONST_int intn1)) FD_downto (Expr_constant (CONST_int intn2)) e)  Lab_nil  (Expr_constant CONST_unit)

and
JR_expr_try_ctx: forall e pattern_matching L e' .
(JR_expr e  L  e')
 ==> 
JR_expr (Expr_try e pattern_matching)  L  (Expr_try e' pattern_matching)

and
JR_expr_try_return: forall v pattern_matching .
(is_value_of_expr v)
 ==> 
JR_expr (Expr_try v pattern_matching)  Lab_nil  v

and
JR_expr_try_catch: forall pat_exp_list v .
(is_value_of_expr v)
 ==> 
JR_expr (Expr_try (Expr_apply (Expr_uprim Uprim_raise) v) (PM_pm (pat_exp_list)))  Lab_nil  (Expr_match v (PM_pm (pat_exp_list ++ [((PE_inj P_any  (Expr_apply (Expr_uprim Uprim_raise) v) ))])))

and
JR_expr_tuple_ctx: forall v_list e_list e L e' .
(List.all (fun v_ -> is_value_of_expr v_) v_list) &&
(JR_expr e  L  e')
 ==> 
JR_expr (Expr_tuple (e_list ++ [(e)] ++ v_list))  L  (Expr_tuple (e_list ++ [(e')] ++ v_list))

and
JR_expr_tuple_raise: forall v_list e_list v .
(is_value_of_expr v) &&
(List.all (fun v_ -> is_value_of_expr v_) v_list)
 ==> 
JR_expr (Expr_tuple (e_list ++ [( (Expr_apply (Expr_uprim Uprim_raise) v) )] ++ v_list))  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_constr_ctx: forall v_list e_list constr e L e' .
(List.all (fun v_ -> is_value_of_expr v_) v_list) &&
(JR_expr e  L  e')
 ==> 
JR_expr (Expr_construct constr (e_list ++ [(e)] ++ v_list))  L  (Expr_construct constr (e_list ++ [(e')] ++ v_list))

and
JR_expr_constr_raise: forall v_list e_list constr v .
(is_value_of_expr v) &&
(List.all (fun v_ -> is_value_of_expr v_) v_list)
 ==> 
JR_expr (Expr_construct constr (e_list ++ [( (Expr_apply (Expr_uprim Uprim_raise) v) )] ++ v_list))  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_cons_ctx1: forall e0 e L e' .
(JR_expr e  L  e')
 ==> 
JR_expr (Expr_cons e0 e)  L  (Expr_cons e0 e')

and
JR_expr_cons_raise1: forall e v .
(is_value_of_expr v)
 ==> 
JR_expr (Expr_cons e  (Expr_apply (Expr_uprim Uprim_raise) v) )  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_cons_ctx2: forall e v L e' .
(is_value_of_expr v) &&
(JR_expr e  L  e')
 ==> 
JR_expr (Expr_cons e v)  L  (Expr_cons e' v)

and
JR_expr_cons_raise2: forall v v' .
(is_value_of_expr v) &&
(is_value_of_expr v')
 ==> 
JR_expr (Expr_cons  (Expr_apply (Expr_uprim Uprim_raise) v)  v')  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_record_ctx: forall fn'_v_list fn_e_list field_name expr L expr' .
(List.all (fun (fn_',v_) -> is_value_of_expr v_) fn'_v_list) &&
(JR_expr expr  L  expr')
 ==> 
JR_expr (Expr_record ((List.map (fun (fn_,e_) -> ((F_name fn_),e_)) fn_e_list) ++ [((F_name field_name),expr)] ++ (List.map (fun (fn_',v_) -> ((F_name fn_'),v_)) fn'_v_list)))  L  (Expr_record ((List.map (fun (fn_,e_) -> ((F_name fn_),e_)) fn_e_list) ++ [((F_name field_name),expr')] ++ (List.map (fun (fn_',v_) -> ((F_name fn_'),v_)) fn'_v_list)))

and
JR_expr_record_raise: forall fn'_v_list fn_e_list fn v .
(is_value_of_expr v) &&
(List.all (fun (fn_',v_) -> is_value_of_expr v_) fn'_v_list)
 ==> 
JR_expr (Expr_record ((List.map (fun (fn_,e_) -> ((F_name fn_),e_)) fn_e_list) ++ [((F_name fn),(Expr_apply (Expr_uprim Uprim_raise) v))] ++ (List.map (fun (fn_',v_) -> ((F_name fn_'),v_)) fn'_v_list)))  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_record_with_ctx1: forall fn'_v_list fn_e_list v field_name e L e' .
(is_value_of_expr v) &&
(List.all (fun (fn_',v_) -> is_value_of_expr v_) fn'_v_list) &&
(JR_expr e  L  e')
 ==> 
JR_expr (Expr_override v ((List.map (fun (fn_,e_) -> ((F_name fn_),e_)) fn_e_list) ++ [((F_name field_name),e)] ++ (List.map (fun (fn_',v_) -> ((F_name fn_'),v_)) fn'_v_list)))  L  (Expr_override v ((List.map (fun (fn_,e_) -> ((F_name fn_),e_)) fn_e_list) ++ [((F_name field_name),e')] ++ (List.map (fun (fn_',v_) -> ((F_name fn_'),v_)) fn'_v_list)))

and
JR_expr_record_with_raise1: forall fn'_v_list fn_e_list v' fn v .
(is_value_of_expr v') &&
(is_value_of_expr v) &&
(List.all (fun (fn_',v_) -> is_value_of_expr v_) fn'_v_list)
 ==> 
JR_expr (Expr_override v' ((List.map (fun (fn_,e_) -> ((F_name fn_),e_)) fn_e_list) ++ [((F_name fn),(Expr_apply (Expr_uprim Uprim_raise) v))] ++ (List.map (fun (fn_',v_) -> ((F_name fn_'),v_)) fn'_v_list)))  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_record_with_ctx2: forall field_name_e_list e L e' .
(JR_expr e  L  e')
 ==> 
JR_expr (Expr_override e ((List.map (fun (field_name_,e_) -> ((F_name field_name_),e_)) field_name_e_list)))  L  (Expr_override e' ((List.map (fun (field_name_,e_) -> ((F_name field_name_),e_)) field_name_e_list)))

and
JR_expr_record_raise_ctx2: forall field_name_e_list v .
(is_value_of_expr v)
 ==> 
JR_expr (Expr_override (Expr_apply (Expr_uprim Uprim_raise) v) ((List.map (fun (field_name_,e_) -> ((F_name field_name_),e_)) field_name_e_list)))  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_record_with_many: forall fn''_v''_list fn'_v'_list fn_v_list field_name v v' .
(is_value_of_expr v) &&
(is_value_of_expr v') &&
(List.all (fun (fn_'',v_'') -> is_value_of_expr v_'') fn''_v''_list) &&
(List.all (fun (fn_',v_') -> is_value_of_expr v_') fn'_v'_list) &&
(List.all (fun (fn_,v_) -> is_value_of_expr v_) fn_v_list) &&
( (List.length ( ((List.map (fun (fn_'',v_'') -> v_'') fn''_v''_list)) ) >=  1 ) ) &&
( (not (List.elem  (Name_fn field_name)    ((List.map (fun (fn_,v_) -> (Name_fn fn_)) fn_v_list))  )) )
 ==> 
JR_expr (Expr_override (Expr_record ((List.map (fun (fn_,v_) -> ((F_name fn_),v_)) fn_v_list) ++ [((F_name field_name),v)] ++ (List.map (fun (fn_',v_') -> ((F_name fn_'),v_')) fn'_v'_list))) ([((F_name field_name),v')] ++ (List.map (fun (fn_'',v_'') -> ((F_name fn_''),v_'')) fn''_v''_list)))  Lab_nil  (Expr_override (Expr_record ((List.map (fun (fn_,v_) -> ((F_name fn_),v_)) fn_v_list) ++ [((F_name field_name),v')] ++ (List.map (fun (fn_',v_') -> ((F_name fn_'),v_')) fn'_v'_list))) ((List.map (fun (fn_'',v_'') -> ((F_name fn_''),v_'')) fn''_v''_list)))

and
JR_expr_record_with_1: forall fn'_v'_list fn_v_list field_name v v' .
(is_value_of_expr v) &&
(is_value_of_expr v') &&
(List.all (fun (fn_',v_') -> is_value_of_expr v_') fn'_v'_list) &&
(List.all (fun (fn_,v_) -> is_value_of_expr v_) fn_v_list) &&
( (not (List.elem  (Name_fn field_name)    ((List.map (fun (fn_,v_) -> (Name_fn fn_)) fn_v_list))  )) )
 ==> 
JR_expr (Expr_override (Expr_record ((List.map (fun (fn_,v_) -> ((F_name fn_),v_)) fn_v_list) ++ [((F_name field_name),v)] ++ (List.map (fun (fn_',v_') -> ((F_name fn_'),v_')) fn'_v'_list))) ([((F_name field_name),v')]))  Lab_nil  (Expr_record ((List.map (fun (fn_,v_) -> ((F_name fn_),v_)) fn_v_list) ++ [((F_name field_name),v')] ++ (List.map (fun (fn_',v_') -> ((F_name fn_'),v_')) fn'_v'_list)))

and
JR_expr_record_access_ctx: forall e field_name L e' .
(JR_expr e  L  e')
 ==> 
JR_expr (Expr_field e (F_name field_name))  L  (Expr_field e' (F_name field_name))

and
JR_expr_record_access_raise: forall v field_name .
(is_value_of_expr v)
 ==> 
JR_expr (Expr_field  (Expr_apply (Expr_uprim Uprim_raise) v)  (F_name field_name))  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_record_access: forall fn'_v'_list fn_v_list field_name v .
(is_value_of_expr v) &&
(List.all (fun (fn_',v_') -> is_value_of_expr v_') fn'_v'_list) &&
(List.all (fun (fn_,v_) -> is_value_of_expr v_) fn_v_list) &&
( (not (List.elem  (Name_fn field_name)    ((List.map (fun (fn_,v_) -> (Name_fn fn_)) fn_v_list))  )) )
 ==> 
JR_expr (Expr_field (Expr_record ((List.map (fun (fn_,v_) -> ((F_name fn_),v_)) fn_v_list) ++ [((F_name field_name),v)] ++ (List.map (fun (fn_',v_') -> ((F_name fn_'),v_')) fn'_v'_list))) (F_name field_name))  Lab_nil  v

and
JR_expr_assert_ctx: forall e L e' .
(JR_expr e  L  e')
 ==> 
JR_expr (Expr_assert e)  L  (Expr_assert e')

and
JR_expr_assert_raise: forall v .
(is_value_of_expr v)
 ==> 
JR_expr (Expr_assert  (Expr_apply (Expr_uprim Uprim_raise) v) )  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) v)

and
JR_expr_assert_true: forall .
true
 ==> 
JR_expr (Expr_assert (Expr_constant CONST_true))  Lab_nil  (Expr_constant CONST_unit)

and
JR_expr_assert_false: forall .
true
 ==> 
JR_expr (Expr_assert (Expr_constant CONST_false))  Lab_nil  (Expr_apply (Expr_uprim Uprim_raise) (Expr_constant (CONST_constr C_assertfailure)))


(** definitions *)
(* defns JRdefn *)
indreln
[JRdefn : definitions -> program -> labelled_arrow -> definitions -> program -> bool]
(* defn Rdefn *)

Jdefn_let_ctx: forall ds_value pat e definitions L e' .
(is_definitions_value_of_definitions ds_value) &&
(JR_expr e  L  e')
 ==> 
JRdefn ds_value (Prog_defs  (Ds_cons  (D_let (LB_simple pat e))   definitions ) )  L  ds_value (Prog_defs  (Ds_cons  (D_let (LB_simple pat e'))   definitions ) )

and
Jdefn_let_raise: forall ds_value pat v definitions .
(is_definitions_value_of_definitions ds_value) &&
(is_value_of_expr v)
 ==> 
JRdefn ds_value (Prog_defs  (Ds_cons  (D_let (LB_simple pat (Expr_apply (Expr_uprim Uprim_raise) v)))   definitions ) )  Lab_nil  ds_value (Prog_raise v)

and
Jdefn_let_match: forall x_v_list ds_value pat v definitions .
(is_definitions_value_of_definitions ds_value) &&
(is_value_of_expr v) &&
(List.all (fun (x_,v_) -> is_value_of_expr v_) x_v_list) &&
(JM_match v pat (Substs_x_xs (x_v_list)))
 ==> 
JRdefn ds_value (Prog_defs  (Ds_cons  (D_let (LB_simple pat v))   definitions ) )  Lab_nil  ds_value (Prog_defs  (substs_value_name_definitions (match  (Substs_x_xs ((List.map (fun (x_,v_) -> (x_, (remv_tyvar_expr  v_ ) )) x_v_list)))  with Substs_x_xs l -> l end)  definitions ) )

and
Jdefn_let_not_match: forall ds_value pat definitions v .
(is_definitions_value_of_definitions ds_value) &&
(is_value_of_expr v) &&
( (not (JM_matchP  v   pat )) )
 ==> 
JRdefn ds_value (Prog_defs  (Ds_cons  (D_let (LB_simple pat v))   definitions ) )  Lab_nil  ds_value (Prog_raise (Expr_constant (CONST_constr C_matchfailure)))

and
Jdefn_letrec: forall x_e_pattern_matching_list ds_value letrec_bindings definitions .
(is_definitions_value_of_definitions ds_value) &&
( ( letrec_bindings  =  (LRBs_inj ((List.map (fun (x_,e_,pattern_matching_) -> (LRB_simple x_ pattern_matching_)) x_e_pattern_matching_list))) ) ) &&
((List.all (fun b -> b) ((List.map (fun (x_,e_,pattern_matching_) -> Jrecfun letrec_bindings pattern_matching_ e_) x_e_pattern_matching_list))))
 ==> 
JRdefn ds_value (Prog_defs  (Ds_cons  (D_letrec letrec_bindings)   definitions ) )  Lab_nil  ds_value (Prog_defs  (substs_value_name_definitions (match  (Substs_x_xs ((List.map (fun (x_,e_,pattern_matching_) -> (x_, (remv_tyvar_expr  e_ ) )) x_e_pattern_matching_list)))  with Substs_x_xs l -> l end)  definitions ) )

and
Jdefn_type: forall ds_value type_definition definitions .
(is_definitions_value_of_definitions ds_value)
 ==> 
JRdefn ds_value (Prog_defs  (Ds_cons  (D_type type_definition)   definitions ) )  Lab_nil   (definitions_snoc  ds_value   (D_type type_definition) )  (Prog_defs definitions)

and
Jdefn_exn: forall ds_value exception_definition definitions .
(is_definitions_value_of_definitions ds_value)
 ==> 
JRdefn ds_value (Prog_defs  (Ds_cons  (D_exception exception_definition)   definitions ) )  Lab_nil   (definitions_snoc  ds_value   (D_exception exception_definition) )  (Prog_defs definitions)


(** definitions *)
(* defns JSlookup *)
indreln
[JSlookup : store -> location -> expr -> bool]
(* defn lookup *)

JSstlookup_rec: forall st l' e l e' .
(JSlookup st l e') &&
( (not ( (Name_l l)  =  (Name_l l') )) )
 ==> 
JSlookup  (( l' ,  e ):: st )  l e'

and
JSstlookup_found: forall st l e .
true
 ==> 
JSlookup  (( l ,  e ):: st )  l e


(** definitions *)
(* defns JRstore *)
indreln
[JRstore : store -> labelled_arrow -> store -> bool]
(* defn store *)

JRstore_empty: forall st .
true
 ==> 
JRstore st  Lab_nil  st

and
JRstore_lookup: forall st l v .
(is_value_of_expr v) &&
(JSlookup st l v)
 ==> 
JRstore st   (Lab_deref l v)   st

and
JRstore_assign: forall st l expr st' v .
(is_value_of_expr v) &&
( (forall v8. not (JSlookup  st'   l  v8)) )
 ==> 
JRstore  ( st' ++[( l ,  expr )]++ st )    (Lab_assign l v)    ( st' ++[( l ,   (remv_tyvar_expr  v )  )]++ st ) 

and
JRstore_alloc: forall st l v .
(is_value_of_expr v) &&
( (forall v8. not (JSlookup  st   l  v8)) )
 ==> 
JRstore st   (Lab_alloc v l)    (( l ,   (remv_tyvar_expr  v )  ):: st ) 


(** definitions *)
(* defns JRtop *)
indreln
[JRtop : definitions -> program -> store -> definitions -> program -> store -> bool]
(* defn top *)

JRtop_defs: forall definitions_value program store definitions program' store' L .
(is_definitions_value_of_definitions definitions_value) &&
(JRstore store  L  store') &&
(JRdefn definitions_value program  L  definitions program')
 ==> 
JRtop definitions_value program store definitions program' store'


(** definitions *)
(* defns Jebehaviour *)
indreln
[JRB_ebehaviour : expr -> bool]
(* defn ebehaviour *)

JRB_ebehaviour_value: forall v .
(is_value_of_expr v)
 ==> 
JRB_ebehaviour v

and
JRB_ebehaviour_reduces: forall e L e' .
(JR_expr e  L  e')
 ==> 
JRB_ebehaviour e

and
JRB_ebehaviour_raises: forall v .
(is_value_of_expr v)
 ==> 
JRB_ebehaviour (Expr_apply (Expr_uprim Uprim_raise) v)


(** definitions *)
(* defns Jdbehaviour *)
indreln
[JRB_dbehaviour : definitions -> program -> store -> bool]
(* defn dbehaviour *)

JRB_behaviour_value: forall definitions_value store .
(is_definitions_value_of_definitions definitions_value)
 ==> 
JRB_dbehaviour definitions_value (Prog_defs Ds_nil) store

and
JRB_behaviour_reduces: forall definitions_value program store definitions' program' store' .
(is_definitions_value_of_definitions definitions_value) &&
(JRtop definitions_value program store definitions' program' store')
 ==> 
JRB_dbehaviour definitions_value program store

and
JRB_behaviour_raises: forall definitions_value v store .
(is_definitions_value_of_definitions definitions_value) &&
(is_value_of_expr v)
 ==> 
JRB_dbehaviour definitions_value (Prog_raise v) store




