(* Signature definition. *)

Inductive term : Set :=
    __aux_47 : term -> term
  | fun_main : term -> term
  | __aux_50 : term -> term
  | __aux_23 : term -> term
  | __aux_1 : term -> term
  | __aux_58 : term -> term
  | __aux_30 : term -> term
  | __aux_49 : term -> term
  | __aux_21 : term -> term
  | __aux_56 : term -> term
  | _1 : term
  | __aux_29 : term -> term
  | nil : term
  | __aux_6 : term -> term
  | __aux_32 : term -> term
  | __aux_9 : term -> term
  | __aux_55 : term -> term
  | __aux_28 : term -> term
  | x3 : term
  | __aux_24 : term -> term
  | __aux_10 : term -> term
  | myarray : term
  | __aux_59 : term -> term
  | __aux_69 : term -> term
  | __aux_31 : term -> term
  | __aux_82 : term -> term
  | __aux_5 : term -> term
  | __aux_22 : term -> term
  | %false(clause_conj) : term
  | __aux_81 : term -> term
  | __aux_46 : term -> term
  | __aux_20 : term -> term
  | __aux_61 : term -> term
  | __aux_34 : term -> term
  | __aux_8 : term -> term
  | x9 : term
  | __aux_41 : term -> term
  | __aux_75 : term -> term
  | address : term -> term
  | __aux_17 : term -> term
  | x8 : term
  | __aux_44 : term -> term
  | __aux_74 : term -> term
  | __aux_36 : term -> term
  | __aux_11 : term -> term
  | __aux_4 : term -> term
  | __aux_19 : term -> term
  | __aux_62 : term -> term
  | __aux_35 : term -> term
  | offset : term -> term -> term
  | __aux_3 : term -> term
  | __aux_65 : term -> term
  | x2 : term
  | __aux_18 : term -> term
  | values : term -> term -> term
  | __aux_64 : term -> term
  | __aux_16 : term -> term
  | x14 : term
  | __aux_43 : term -> term
  | __aux_12 : term -> term
  | x15 : term
  | __aux_40 : term -> term
  | __aux_70 : term -> term
  | __aux_33 : term -> term
  | __aux_2 : term -> term
.
Parameter %false(clause_conj) : Prop.
Parameter __aux_47, fun_main, __aux_50, __aux_23, __aux_1, __aux_58, __aux_30, __aux_49, __aux_21, __aux_56, __aux_29, __aux_6, __aux_32, __aux_9, __aux_55, __aux_28, __aux_24, __aux_10, __aux_59, __aux_69, __aux_31, __aux_82, __aux_5, __aux_22, __aux_81, __aux_46, __aux_20, __aux_61, __aux_34, __aux_8, __aux_41, __aux_75, __aux_17, __aux_44, __aux_74, __aux_36, __aux_11, __aux_4, __aux_19, __aux_62, __aux_35, __aux_3, __aux_65, __aux_18, __aux_64, __aux_16, __aux_43, __aux_12, __aux_40, __aux_70, __aux_33, __aux_2 : term -> Prop.
Parameter values : term -> term -> Prop.

Parameter __star__ : term.

(* Definitions. *)

Definition __aux_61 := [_x1:term] Cases (_x1) of
    ((offset X1 X2)) => (EX X3:term | (__aux_60 X2 X3 X1))
  | _ => False
  end.
Definition __aux_23 := [_x1:term] Cases (_x1) of
    (x9) => (fun_main nil)
  | _ => False
  end.
Definition __aux_21 := [_x1:term] Cases (_x1) of
    (x10) => (EX X1:term | (__aux_20 X1))
  | _ => False
  end.
Definition __aux_29 := [_x1:term] Cases (_x1) of
    (_2) => (fun_main nil)
  | _ => False
  end.
Definition __aux_86 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X5:term | (EX X2:term | (EX X4:term | (__aux_80 X2 X3 X4 X1 X5)))))
  | _ => False
  end.
Definition __aux_18 := [_x1:term] Cases (_x1) of
    (x7) => (EX X1:term | (__aux_3 X1))
  | _ => False
  end.
Definition __aux_26 := [_x1:term] Cases (_x1) of
    (x10) => (fun_main nil)
  | _ => False
  end.
Definition __aux_62 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X2:term | (__aux_60 X2 X1 X3)))
  | _ => False
  end.
Definition __aux_42 := [_x1,_x2,_x3:term] Cases (_x1,_x2,_x3) of
    (X1,X2,X3) => (EX X4:term | (values X4 (address X1)) /\ (values (field X4 X2) X3))
  | _ => False
  end.
Definition __aux_44 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X2:term | (__aux_42 X2 X3 X1)))
  | _ => False
  end.
Definition __aux_20 := [_x1:term] Cases (_x1) of
    (X1) => (__aux_20 X1)
  | _ => False
  end.
Definition __aux_27 := [_x1:term] Cases (_x1) of
    (x12) => (fun_main nil)
  | _ => False
  end.
Definition __aux_17 := [_x1:term] Cases (_x1) of
    (_1) => (fun_main nil)
  | _ => False
  end.
Definition __aux_81 := [_x1:term] Cases (_x1) of
    ((field X1 X2)) => (__aux_84 X2) /\ (__aux_83 X1)
  | _ => False
  end.
Definition __aux_20 := [_x1:term] Cases (_x1) of
    (X1) => (fun_main nil) /\ (values x11 X1)
  | _ => False
  end.
Definition __aux_8 := [_x1:term] Cases (_x1) of
    (X1) => (fun_main nil) /\ (values x5 X1)
  | _ => False
  end.
Definition __aux_6 := [_x1:term] Cases (_x1) of
    ((address X1)) => (__aux_7 X1)
  | _ => False
  end.
Definition __aux_57 := [_x1,_x2,_x3:term] Cases (_x1,_x2,_x3) of
    (X1,X2,X3) => (EX X5:term | (EX X4:term | (values X5 (address X4)) /\ (values (offset X5 X2) X3) /\ (values X1 (address X4))))
  | _ => False
  end.
Definition __aux_19 := [_x1:term] Cases (_x1) of
    (x11) => (fun_main nil)
  | _ => False
  end.
Definition __aux_58 := [_x1:term] Cases (_x1) of
    ((offset X1 X2)) => (EX X3:term | (__aux_57 X1 X2 X3))
  | _ => False
  end.
Definition __aux_43 := [_x1:term] Cases (_x1) of
    ((field X1 X2)) => (EX X3:term | (__aux_42 X1 X2 X3))
  | _ => False
  end.
Definition __aux_47 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X2:term | (__aux_45 X2 X3 X1)))
  | _ => False
  end.
Definition __aux_83 := [_x1:term] Cases (_x1) of
    ((field X1 X2)) => (__aux_86 X2) /\ (__aux_85 X1)
  | _ => False
  end.
Definition __aux_28 := [_x1:term] Cases (_x1) of
    (x8) => (EX X1:term | (__aux_3 X1))
  | _ => False
  end.
Definition __aux_84 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X5:term | (EX X2:term | (EX X4:term | (__aux_80 X2 X1 X3 X4 X5)))))
  | _ => False
  end.
Definition __aux_59 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X2:term | (__aux_57 X2 X3 X1)))
  | _ => False
  end.
Definition __aux_41 := [_x1:term] Cases (_x1) of
    (main_return) => (fun_main nil)
  | _ => False
  end.
Definition __aux_45 := [_x1,_x2,_x3:term] Cases (_x1,_x2,_x3) of
    (X1,X2,X3) => (EX X5:term | (EX X4:term | (values X5 (address X4)) /\ (values X1 (address X4)) /\ (values (field X5 X2) X3)))
  | _ => False
  end.
Definition __aux_2 := [_x1:term] Cases (_x1) of
    (_0) => (fun_main nil)
  | _ => False
  end.
Definition __aux_22 := [_x1:term] Cases (_x1) of
    (x12) => (EX X1:term | (__aux_3 X1))
  | _ => False
  end.
Definition __aux_80 := [_x1,_x2,_x3,_x4,_x5:term] Cases (_x1,_x2,_x3,_x4,_x5) of
    (X1,X2,X3,X4,X5) => (EX X6:term | (values X6 (address X2)) /\ (values X5 (address X2)) /\ (values (field (field (field X6 X1) X4) X2) X3))
  | _ => False
  end.
Definition __aux_82 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X5:term | (EX X2:term | (EX X4:term | (__aux_80 X2 X3 X1 X4 X5)))))
  | _ => False
  end.
Definition __aux_85 := [_x1:term] Cases (_x1) of
    ((field X1 X2)) => (EX X3:term | (EX X5:term | (EX X4:term | (__aux_80 X2 X3 X4 X5 X1))))
  | _ => False
  end.
Definition __aux_24 := [_x1:term] Cases (_x1) of
    ((address X1)) => (__aux_25 X1)
  | _ => False
  end.
Definition __aux_8 := [_x1:term] Cases (_x1) of
    (X1) => (__aux_8 X1)
  | _ => False
  end.
Definition __aux_9 := [_x1:term] Cases (_x1) of
    (x4) => (EX X1:term | (__aux_8 X1))
  | _ => False
  end.
Definition __aux_25 := [_x1:term] Cases (_x1) of
    ((offset X1 X2)) => (__aux_27 X2) /\ (__aux_26 X1)
  | _ => False
  end.
Definition __aux_63 := [_x1,_x2,_x3,_x4:term] Cases (_x1,_x2,_x3,_x4) of
    (X1,X2,X3,X4) => (EX X5:term | (values X5 (address X4)) /\ (values (field (field X5 X1) X3) X2))
  | _ => False
  end.
Definition __aux_60 := [_x1,_x2,_x3:term] Cases (_x1,_x2,_x3) of
    (X1,X2,X3) => (EX X4:term | (values X4 X1) /\ (values (offset X3 X4) X2))
  | _ => False
  end.
Definition __aux_46 := [_x1:term] Cases (_x1) of
    ((field X1 X2)) => (EX X3:term | (__aux_45 X1 X2 X3))
  | _ => False
  end.
Definition __aux_55 := [_x1:term] Cases (_x1) of
    ((offset X1 X2)) => (EX X3:term | (__aux_54 X1 X2 X3))
  | _ => False
  end.
Definition __aux_3 := [_x1:term] Cases (_x1) of
    (X1) => (fun_main nil) /\ (values x X1)
  | _ => False
  end.
Definition __aux_31 := [_x1:term] Cases (_x1) of
    (x17) => (fun_main nil)
  | _ => False
  end.
Definition __aux_64 := [_x1:term] Cases (_x1) of
    ((field X1 X2)) => (__aux_67 X2) /\ (__aux_66 X1)
  | _ => False
  end.
Definition __aux_13 := [_x1:term] Cases (_x1) of
    ((offset X1 X2)) => (__aux_15 X2) /\ (__aux_14 X1)
  | _ => False
  end.
Definition __aux_70 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X2:term | (EX X4:term | (__aux_68 X2 X1 X3 X4))))
  | _ => False
  end.
Definition __aux_32 := [_x1:term] Cases (_x1) of
    (X1) => (__aux_32 X1)
  | _ => False
  end.
Definition __aux_54 := [_x1,_x2,_x3:term] Cases (_x1,_x2,_x3) of
    (X1,X2,X3) => (EX X4:term | (values X4 (address X1)) /\ (values (offset X4 X2) X3))
  | _ => False
  end.
Definition __aux_5 := [_x1:term] Cases (_x1) of
    (x5) => (fun_main nil)
  | _ => False
  end.
Definition __aux_14 := [_x1:term] Cases (_x1) of
    (x4) => (fun_main nil)
  | _ => False
  end.
Definition __aux_74 := [_x1:term] Cases (_x1) of
    ((field X1 X2)) => (__aux_77 X2) /\ (__aux_76 X1)
  | _ => False
  end.
Definition __aux_76 := [_x1:term] Cases (_x1) of
    ((field X1 X2)) => (__aux_79 X2) /\ (__aux_78 X1)
  | _ => False
  end.
Definition __aux_32 := [_x1:term] Cases (_x1) of
    (X1) => (fun_main nil) /\ (values x17 X1)
  | _ => False
  end.
Definition __aux_73 := [_x1,_x2,_x3,_x4,_x5:term] Cases (_x1,_x2,_x3,_x4,_x5) of
    (X1,X2,X3,X4,X5) => (EX X6:term | (values X6 (address X5)) /\ (values (field (field (field X6 X1) X4) X2) X3))
  | _ => False
  end.
Definition __aux_75 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X5:term | (EX X2:term | (EX X4:term | (__aux_73 X2 X3 X1 X4 X5)))))
  | _ => False
  end.
Definition __aux_71 := [_x1:term] Cases (_x1) of
    ((field X1 X2)) => (EX X3:term | (EX X4:term | (__aux_68 X2 X3 X4 X1)))
  | _ => False
  end.
Definition __aux_68 := [_x1,_x2,_x3,_x4:term] Cases (_x1,_x2,_x3,_x4) of
    (X1,X2,X3,X4) => (EX X6:term | (EX X5:term | (values X5 (address X6)) /\ (values X4 (address X6)) /\ (values (field (field X5 X1) X3) X2)))
  | _ => False
  end.
Definition __aux_34 := [_x1:term] Cases (_x1) of
    (x18) => (EX X1:term | (__aux_3 X1))
  | _ => False
  end.
Definition __aux_56 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X2:term | (__aux_54 X2 X3 X1)))
  | _ => False
  end.
Definition __aux_12 := [_x1:term] Cases (_x1) of
    ((address X1)) => (__aux_13 X1)
  | _ => False
  end.
Definition __aux_7 := [_x1:term] Cases (_x1) of
    (myarray) => (fun_main nil)
  | _ => False
  end.
Definition __aux_36 := [_x1:term] Cases (_x1) of
    ((address X1)) => (__aux_37 X1)
  | _ => False
  end.
Definition __aux_69 := [_x1:term] Cases (_x1) of
    ((field X1 X2)) => (__aux_72 X2) /\ (__aux_71 X1)
  | _ => False
  end.
Definition __aux_1 := [_x1:term] Cases (_x1) of
    (x) => (fun_main nil)
  | _ => False
  end.
Definition __aux_40 := [_x1:term] Cases (_x1) of
    (x14) => (EX X1:term | (__aux_3 X1))
  | _ => False
  end.
Definition __aux_15 := [_x1:term] Cases (_x1) of
    (x6) => (fun_main nil)
  | _ => False
  end.
Definition __aux_49 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X2:term | (EX X4:term | (__aux_48 X2 X1 X3 X4))))
  | _ => False
  end.
Definition __aux_37 := [_x1:term] Cases (_x1) of
    ((offset X1 X2)) => (__aux_39 X2) /\ (__aux_38 X1)
  | _ => False
  end.
Definition __aux_35 := [_x1:term] Cases (_x1) of
    (x15) => (fun_main nil)
  | _ => False
  end.
Definition __aux_38 := [_x1:term] Cases (_x1) of
    (x16) => (fun_main nil)
  | _ => False
  end.
Definition __aux_77 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X5:term | (EX X2:term | (EX X4:term | (__aux_73 X2 X1 X3 X4 X5)))))
  | _ => False
  end.
Definition __aux_51 := [_x1:term] Cases (_x1) of
    ((field X1 X2)) => (__aux_53 X2) /\ (__aux_52 X1)
  | _ => False
  end.
Definition __aux_3 := [_x1:term] Cases (_x1) of
    (X1) => (__aux_3 X1)
  | _ => False
  end.
Definition __aux_16 := [_x1:term] Cases (_x1) of
    (x2) => (EX X1:term | (__aux_3 X1))
  | _ => False
  end.
Definition __aux_78 := [_x1:term] Cases (_x1) of
    ((field X1 X2)) => (EX X3:term | (EX X5:term | (EX X4:term | (__aux_73 X2 X3 X4 X5 X1))))
  | _ => False
  end.
Definition __aux_72 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X2:term | (EX X4:term | (__aux_68 X2 X3 X1 X4))))
  | _ => False
  end.
Definition __aux_30 := [_x1:term] Cases (_x1) of
    (x13) => (EX X1:term | (__aux_3 X1))
  | _ => False
  end.
Definition __aux_11 := [_x1:term] Cases (_x1) of
    (x3) => (fun_main nil)
  | _ => False
  end.
Definition __aux_67 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X2:term | (EX X4:term | (__aux_63 X2 X3 X1 X4))))
  | _ => False
  end.
Definition __aux_39 := [_x1:term] Cases (_x1) of
    (x18) => (fun_main nil)
  | _ => False
  end.
Definition __aux_33 := [_x1:term] Cases (_x1) of
    (x16) => (EX X1:term | (__aux_32 X1))
  | _ => False
  end.
Definition __aux_4 := [_x1:term] Cases (_x1) of
    (x1) => (EX X1:term | (__aux_3 X1))
  | _ => False
  end.
Definition __aux_10 := [_x1:term] Cases (_x1) of
    (x6) => (EX X1:term | (__aux_3 X1))
  | _ => False
  end.
Definition __aux_48 := [_x1,_x2,_x3,_x4:term] Cases (_x1,_x2,_x3,_x4) of
    (X1,X2,X3,X4) => (EX X5:term | (values X2 (address (field X5 X3))) /\ (values X5 (address (field X4 X1))))
  | _ => False
  end.
Definition __aux_66 := [_x1:term] Cases (_x1) of
    ((field X1 X2)) => (EX X3:term | (EX X4:term | (__aux_63 X2 X3 X4 X1)))
  | _ => False
  end.
Definition __aux_65 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X2:term | (EX X4:term | (__aux_63 X2 X1 X3 X4))))
  | _ => False
  end.
Definition __aux_79 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X5:term | (EX X2:term | (EX X4:term | (__aux_73 X2 X3 X4 X1 X5)))))
  | _ => False
  end.
Definition __aux_50 := [_x1:term] Cases (_x1) of
    ((address X1)) => (__aux_51 X1)
  | _ => False
  end.
Definition __aux_53 := [_x1:term] Cases (_x1) of
    (X1) => (EX X3:term | (EX X2:term | (EX X4:term | (__aux_48 X2 X3 X1 X4))))
  | _ => False
  end.
Definition __aux_52 := [_x1:term] Cases (_x1) of
    ((field X1 X2)) => (EX X3:term | (EX X4:term | (__aux_48 X2 X3 X4 X1)))
  | _ => False
  end.
