(* Signature definition. *)

Inductive extterm : Set :=
    x4 : extterm
  | x6 : extterm
  | y1 : extterm
  | x11 : extterm
  | _1 : extterm
  | __tuple____aux_55 : extterm -> extterm -> extterm -> extterm
  | i : extterm
  | nil : extterm
  | x10 : extterm
  | x3 : extterm
  | _3 : extterm
  | x8 : extterm
  | x2 : extterm
  | __tuple__values : extterm -> extterm -> extterm
  | _10 : extterm
  | myarray : extterm
  | main_return : extterm
  | x5 : extterm
  | _0 : extterm
  | __tuple____aux_49 : extterm -> extterm -> extterm -> extterm
  | field : extterm -> extterm -> extterm
  | __tuple__inf : extterm -> extterm -> extterm
  | __tuple____aux_7 : extterm
  | x13 : extterm
  | address : extterm -> extterm
  | __tuple____aux_75 : extterm -> extterm -> extterm -> extterm -> extterm -> extterm
  | plus : extterm -> extterm -> extterm
  | __tuple____aux_58 : extterm -> extterm -> extterm -> extterm -> extterm
  | offset : extterm -> extterm -> extterm
  | __tuple____aux_37 : extterm -> extterm -> extterm -> extterm
  | x7 : extterm
  | __tuple____aux_68 : extterm -> extterm -> extterm -> extterm -> extterm -> extterm
  | x12 : extterm
  | __tuple____aux_52 : extterm -> extterm -> extterm -> extterm
  | __tuple____aux_43 : extterm -> extterm -> extterm -> extterm -> extterm
  | __tuple____aux_40 : extterm -> extterm -> extterm -> extterm
  | x9 : extterm
  | _00 : extterm
  | __tuple____aux_63 : extterm -> extterm -> extterm -> extterm -> extterm
  | __star__clause_conj : extterm
.
(* Model definition. *)

Require Refine.

Inductive auto___aux_19 : extterm -> Prop :=
    trans___aux_19_address_1 : (X1:extterm)(auto___aux_20 X1) -> (auto___aux_19 (address X1))
with auto___aux_4 : extterm -> Prop :=
    trans___aux_4_x2_1 : (auto___aux_4 x2)
with auto___aux_53 : extterm -> Prop :=
    trans___aux_53_offset_1 : (X1,X2:extterm)(auto___aux_16 X1) -> (auto___aux_22 X2) -> (auto___aux_53 (offset X1 X2))
  | trans___aux_53_offset_2 : (X1,X2:extterm)(auto___aux_12 X1) -> (auto___aux_22 X2) -> (auto___aux_53 (offset X1 X2))
  | trans___aux_53_offset_3 : (X1,X2:extterm)(auto___aux_16 X1) -> (auto___aux_3 X2) -> (auto___aux_53 (offset X1 X2))
  | trans___aux_53_offset_4 : (X1,X2:extterm)(auto___aux_12 X1) -> (auto___aux_3 X2) -> (auto___aux_53 (offset X1 X2))
with auto___aux_9 : extterm -> Prop :=
    trans___aux_9__10_1 : (auto___aux_9 _10)
with auto___aux_35 : extterm -> Prop :=
    trans___aux_35_x3_1 : (auto___aux_35 x3)
with auto___aux_36 : extterm -> Prop :=
    trans___aux_36_main_return_1 : (auto___aux_36 main_return)
with auto___aux_34 : extterm -> Prop :=
    trans___aux_34_x5_1 : (auto___aux_34 x5)
with auto___aux_2 : extterm -> Prop :=
    trans___aux_2__0_1 : (auto___aux_2 _0)
with auto_fun_main : extterm -> Prop :=
    trans_fun_main_nil_1 : (auto_fun_main nil)
with auto___aux_54 : extterm -> Prop :=
    trans___aux_54__0_1 : (auto___aux_54 _0)
  | trans___aux_54_plus_1 : (X1,X2:extterm)(auto___aux_32 X1) -> (auto___aux_33 X2) -> (auto___aux_54 (plus X1 X2))
with auto___aux_26 : extterm -> Prop :=
    trans___aux_26_y1_1 : (auto___aux_26 y1)
with auto___aux_18 : extterm -> Prop :=
    trans___aux_18_x10_1 : (auto___aux_18 x10)
with auto___aux_5 : extterm -> Prop :=
    trans___aux_5_x8_1 : (auto___aux_5 x8)
with auto___aux_55 : extterm -> Prop :=
    trans___aux_55___tuple____aux_55_1 : (X1,X2,X3:extterm)(auto___aux_3 X1) -> (auto___aux_54 X2) -> (auto___aux_12 X3) -> (auto___aux_55 (__tuple____aux_55 X1 X2 X3))
  | trans___aux_55___tuple____aux_55_2 : (X1,X2,X3:extterm)(auto___aux_3 X1) -> (auto___aux_51 X2) -> (auto___aux_14 X3) -> (auto___aux_55 (__tuple____aux_55 X1 X2 X3))
  | trans___aux_55___tuple____aux_55_3 : (X1,X2,X3:extterm)(auto___aux_3 X1) -> (auto___aux_54 X2) -> (auto___aux_16 X3) -> (auto___aux_55 (__tuple____aux_55 X1 X2 X3))
with auto___aux_25 : extterm -> Prop :=
    trans___aux_25_offset_1 : (X1,X2:extterm)(auto___aux_21 X1) -> (auto___aux_22 X2) -> (auto___aux_25 (offset X1 X2))
with auto___aux_49 : extterm -> Prop :=
    trans___aux_49___tuple____aux_49_1 : (X1,X2,X3:extterm)(auto___aux_14 X1) -> (auto___aux_3 X2) -> (auto___aux_57 X3) -> (auto___aux_49 (__tuple____aux_49 X1 X2 X3))
  | trans___aux_49___tuple____aux_49_2 : (X1,X2,X3:extterm)(auto___aux_14 X1) -> (auto___aux_22 X2) -> (auto___aux_54 X3) -> (auto___aux_49 (__tuple____aux_49 X1 X2 X3))
with auto_values : extterm -> Prop :=
    trans_values___tuple__values_1 : (X1,X2:extterm)(auto___aux_50 X1) -> (auto___aux_51 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_2 : (X1,X2:extterm)(auto___aux_53 X1) -> (auto___aux_54 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_3 : (X1,X2:extterm)(auto___aux_16 X1) -> (auto___aux_15 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_4 : (X1,X2:extterm)(auto___aux_23 X1) -> (auto___aux_3 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_5 : (X1,X2:extterm)(auto___aux_26 X1) -> (auto___aux_3 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_6 : (X1,X2:extterm)(auto___aux_5 X1) -> (auto___aux_6 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_7 : (X1,X2:extterm)(auto___aux_1 X1) -> (auto___aux_31 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_8 : (X1,X2:extterm)(auto___aux_12 X1) -> (auto___aux_13 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_9 : (X1,X2:extterm)(auto___aux_18 X1) -> (auto___aux_19 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_10 : (X1,X2:extterm)(auto___aux_36 X1) -> (auto___aux_2 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_11 : (X1,X2:extterm)(auto___aux_28 X1) -> (auto___aux_27 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_12 : (X1,X2:extterm)(auto___aux_17 X1) -> (auto___aux_3 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_13 : (X1,X2:extterm)(auto___aux_34 X1) -> (auto___aux_3 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_14 : (X1,X2:extterm)(auto___aux_35 X1) -> (auto___aux_27 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_15 : (X1,X2:extterm)(auto___aux_10 X1) -> (auto___aux_11 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_16 : (X1,X2:extterm)(auto___aux_56 X1) -> (auto___aux_57 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_17 : (X1,X2:extterm)(auto___aux_29 X1) -> (auto___aux_30 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_18 : (X1,X2:extterm)(auto___aux_1 X1) -> (auto___aux_2 X2) -> (auto_values (__tuple__values X1 X2))
  | trans_values___tuple__values_19 : (X1,X2:extterm)(auto___aux_4 X1) -> (auto___aux_3 X2) -> (auto_values (__tuple__values X1 X2))
with auto___aux_27 : extterm -> Prop :=
    trans___aux_27__0_1 : (auto___aux_27 _0)
  | trans___aux_27_plus_1 : (X1,X2:extterm)(auto___aux_32 X1) -> (auto___aux_33 X2) -> (auto___aux_27 (plus X1 X2))
with auto___aux_31 : extterm -> Prop :=
    trans___aux_31_plus_1 : (X1,X2:extterm)(auto___aux_32 X1) -> (auto___aux_33 X2) -> (auto___aux_31 (plus X1 X2))
with auto___aux_29 : extterm -> Prop :=
    trans___aux_29_x6_1 : (auto___aux_29 x6)
with auto___aux_30 : extterm -> Prop :=
    trans___aux_30__1_1 : (auto___aux_30 _1)
with auto___aux_51 : extterm -> Prop :=
    trans___aux_51__0_1 : (auto___aux_51 _0)
  | trans___aux_51_plus_1 : (X1,X2:extterm)(auto___aux_32 X1) -> (auto___aux_33 X2) -> (auto___aux_51 (plus X1 X2))
with auto___aux_15 : extterm -> Prop :=
    trans___aux_15_address_1 : (X1:extterm)(auto___aux_14 X1) -> (auto___aux_15 (address X1))
with auto___aux_28 : extterm -> Prop :=
    trans___aux_28_x4_1 : (auto___aux_28 x4)
with auto___aux_12 : extterm -> Prop :=
    trans___aux_12_x12_1 : (auto___aux_12 x12)
with auto___aux_10 : extterm -> Prop :=
    trans___aux_10_x7_1 : (auto___aux_10 x7)
with auto___aux_3 : extterm -> Prop :=
    trans___aux_3__0_1 : (auto___aux_3 _0)
  | trans___aux_3_plus_1 : (X1,X2:extterm)(auto___aux_32 X1) -> (auto___aux_33 X2) -> (auto___aux_3 (plus X1 X2))
with auto___aux_20 : extterm -> Prop :=
    trans___aux_20_offset_1 : (X1,X2:extterm)(auto___aux_21 X1) -> (auto___aux_22 X2) -> (auto___aux_20 (offset X1 X2))
with auto___aux_57 : extterm -> Prop :=
    trans___aux_57__0_1 : (auto___aux_57 _0)
  | trans___aux_57_plus_1 : (X1,X2:extterm)(auto___aux_32 X1) -> (auto___aux_33 X2) -> (auto___aux_57 (plus X1 X2))
with auto___aux_56 : extterm -> Prop :=
    trans___aux_56_offset_1 : (X1,X2:extterm)(auto___aux_14 X1) -> (auto___aux_3 X2) -> (auto___aux_56 (offset X1 X2))
  | trans___aux_56_offset_2 : (X1,X2:extterm)(auto___aux_16 X1) -> (auto___aux_3 X2) -> (auto___aux_56 (offset X1 X2))
  | trans___aux_56_offset_3 : (X1,X2:extterm)(auto___aux_12 X1) -> (auto___aux_3 X2) -> (auto___aux_56 (offset X1 X2))
with auto___aux_23 : extterm -> Prop :=
    trans___aux_23_x9_1 : (auto___aux_23 x9)
with auto___aux_11 : extterm -> Prop :=
    trans___aux_11__00_1 : (auto___aux_11 _00)
with auto___aux_1 : extterm -> Prop :=
    trans___aux_1_i_1 : (auto___aux_1 i)
with auto___aux_24 : extterm -> Prop :=
    trans___aux_24__0_1 : (auto___aux_24 _0)
  | trans___aux_24_plus_1 : (X1,X2:extterm)(auto___aux_32 X1) -> (auto___aux_33 X2) -> (auto___aux_24 (plus X1 X2))
with auto___aux_16 : extterm -> Prop :=
    trans___aux_16_x11_1 : (auto___aux_16 x11)
with auto___aux_21 : extterm -> Prop :=
    trans___aux_21_x11_1 : (auto___aux_21 x11)
with auto___aux_50 : extterm -> Prop :=
    trans___aux_50_offset_1 : (X1,X2:extterm)(auto___aux_14 X1) -> (auto___aux_3 X2) -> (auto___aux_50 (offset X1 X2))
  | trans___aux_50_offset_2 : (X1,X2:extterm)(auto___aux_14 X1) -> (auto___aux_22 X2) -> (auto___aux_50 (offset X1 X2))
with auto___aux_33 : extterm -> Prop :=
    trans___aux_33_x6_1 : (auto___aux_33 x6)
with auto___aux_8 : extterm -> Prop :=
    trans___aux_8_x7_1 : (auto___aux_8 x7)
with auto___aux_6 : extterm -> Prop :=
    trans___aux_6__3_1 : (auto___aux_6 _3)
with auto___aux_32 : extterm -> Prop :=
    trans___aux_32_i_1 : (auto___aux_32 i)
with auto___aux_17 : extterm -> Prop :=
    trans___aux_17_x13_1 : (auto___aux_17 x13)
with auto___aux_22 : extterm -> Prop :=
    trans___aux_22_x13_1 : (auto___aux_22 x13)
with auto___aux_13 : extterm -> Prop :=
    trans___aux_13_address_1 : (X1:extterm)(auto___aux_14 X1) -> (auto___aux_13 (address X1))
with auto___aux_52 : extterm -> Prop :=
    trans___aux_52___tuple____aux_52_1 : (X1,X2,X3:extterm)(auto___aux_12 X1) -> (auto___aux_3 X2) -> (auto___aux_57 X3) -> (auto___aux_52 (__tuple____aux_52 X1 X2 X3))
  | trans___aux_52___tuple____aux_52_2 : (X1,X2,X3:extterm)(auto___aux_16 X1) -> (auto___aux_22 X2) -> (auto___aux_24 X3) -> (auto___aux_52 (__tuple____aux_52 X1 X2 X3))
  | trans___aux_52___tuple____aux_52_3 : (X1,X2,X3:extterm)(auto___aux_16 X1) -> (auto___aux_3 X2) -> (auto___aux_57 X3) -> (auto___aux_52 (__tuple____aux_52 X1 X2 X3))
  | trans___aux_52___tuple____aux_52_4 : (X1,X2,X3:extterm)(auto___aux_12 X1) -> (auto___aux_22 X2) -> (auto___aux_24 X3) -> (auto___aux_52 (__tuple____aux_52 X1 X2 X3))
with auto___aux_14 : extterm -> Prop :=
    trans___aux_14_myarray_1 : (auto___aux_14 myarray)
with auto___aux_77 : extterm -> Prop :=
with auto___aux_44 : extterm -> Prop :=
with auto___aux_7 : extterm -> Prop :=
with auto___aux_61 : extterm -> Prop :=
with auto___aux_66 : extterm -> Prop :=
with auto___aux_58 : extterm -> Prop :=
with auto___aux_39 : extterm -> Prop :=
with auto___aux_74 : extterm -> Prop :=
with auto___aux_69 : extterm -> Prop :=
with auto___aux_42 : extterm -> Prop :=
with auto___aux_76 : extterm -> Prop :=
with auto___aux_81 : extterm -> Prop :=
with auto___aux_45 : extterm -> Prop :=
with auto___aux_64 : extterm -> Prop :=
with auto___aux_38 : extterm -> Prop :=
with auto___aux_70 : extterm -> Prop :=
with auto___aux_68 : extterm -> Prop :=
with auto___aux_41 : extterm -> Prop :=
with auto___aux_75 : extterm -> Prop :=
with auto___aux_47 : extterm -> Prop :=
with auto___aux_65 : extterm -> Prop :=
with auto___aux_59 : extterm -> Prop :=
with auto_inf : extterm -> Prop :=
with auto___aux_71 : extterm -> Prop :=
with auto___aux_43 : extterm -> Prop :=
with auto___aux_78 : extterm -> Prop :=
with auto___aux_48 : extterm -> Prop :=
with auto___aux_73 : extterm -> Prop :=
with auto___false__clause_conj : extterm -> Prop :=
with auto___aux_72 : extterm -> Prop :=
with auto___aux_79 : extterm -> Prop :=
with auto___aux_80 : extterm -> Prop :=
with auto___aux_46 : extterm -> Prop :=
with auto___aux_67 : extterm -> Prop :=
with auto___aux_60 : extterm -> Prop :=
with auto___aux_62 : extterm -> Prop :=
with auto___aux_40 : extterm -> Prop :=
with auto___aux_37 : extterm -> Prop :=
with auto___aux_63 : extterm -> Prop :=
.
