let tuple_example1() =
  begin
    printf "\ntuple_example1\n";
    
    let ctx       = mk_context [||] in

    let real_sort = Z3.mk_real_sort ctx in

    (* Create pair (tuple) type *)
    let mk_tuple_name = Z3.mk_string_symbol ctx "mk_pair" in
    let proj_names_0 = Z3.mk_string_symbol ctx "get_x" in
    let proj_names_1 = Z3.mk_string_symbol ctx "get_y" in
    let proj_names = [|proj_names_0; proj_names_1|] in
    let proj_sorts = [|real_sort;real_sort|] in
    (* Z3_mk_tuple_sort will set mk_tuple_decl and proj_decls *)
    let (pair_sort,mk_tuple_decl,proj_decls) = Z3.mk_tuple_sort ctx mk_tuple_name proj_names proj_sorts in
    let get_x_decl    = proj_decls.(0) in (* function that extracts the first element of a tuple. *)
    let get_y_decl    = proj_decls.(1) in (* function that extracts the second element of a tuple. *)

    printf "tuple_type: ";
    display_sort ctx stdout pair_sort;
    printf "\n";

    begin
      (* prove that get_x(mk_pair(x,y)) == 1 implies x = 1*)
      let x    = mk_real_var ctx "x" in
      let y    = mk_real_var ctx "y" in
      let app1 = mk_binary_app ctx mk_tuple_decl x y in
      let app2 = mk_unary_app ctx get_x_decl app1 in 
      let one  = Z3.mk_numeral ctx "1" real_sort in
      let eq1  = Z3.mk_eq ctx app2 one in
      let eq2  = Z3.mk_eq ctx x one in
      let thm  = Z3.mk_implies ctx eq1 eq2 in
      printf "prove: get_x(mk_pair(x, y)) = 1 implies x = 1\n";
      prove ctx thm true;

      (* disprove that get_x(mk_pair(x,y)) == 1 implies y = 1*)
      let eq3  = Z3.mk_eq ctx y one in
      let thm  = Z3.mk_implies ctx eq1 eq3 in
      printf "disprove: get_x(mk_pair(x, y)) = 1 implies y = 1\n";
      prove ctx thm false;
    end;

    begin
      (* prove that get_x(p1) = get_x(p2) and get_y(p1) = get_y(p2) implies p1 = p2 *)
      let p1          = mk_var ctx "p1" pair_sort in
      let p2          = mk_var ctx "p2" pair_sort in
      let x1          = mk_unary_app ctx get_x_decl p1 in
      let y1          = mk_unary_app ctx get_y_decl p1 in
      let x2          = mk_unary_app ctx get_x_decl p2 in
      let y2          = mk_unary_app ctx get_y_decl p2 in
      let antecedents_0 = Z3.mk_eq ctx x1 x2 in
      let antecedents_1 = Z3.mk_eq ctx y1 y2 in
      let antecedents = [|antecedents_0; antecedents_1|] in
      let antecedent  = Z3.mk_and ctx antecedents in
      let consequent  = Z3.mk_eq ctx p1 p2 in
      let thm         = Z3.mk_implies ctx antecedent consequent in
      printf "prove: get_x(p1) = get_x(p2) and get_y(p1) = get_y(p2) implies p1 = p2\n";
      prove ctx thm true;

      (* disprove that get_x(p1) = get_x(p2) implies p1 = p2 *)
      let thm         = Z3.mk_implies ctx (antecedents.(0)) consequent in
      printf "disprove: get_x(p1) = get_x(p2) implies p1 = p2\n";
      prove ctx thm false;
    end;

    begin
      (* demonstrate how to use the mk_tuple_update function *)
      (* prove that p2 = update(p1, 0, 10) implies get_x(p2) = 10 *)
      let p1             = mk_var ctx "p1" pair_sort in
      let p2             = mk_var ctx "p2" pair_sort in
      let one            = Z3.mk_numeral ctx "1" real_sort in
      let ten            = Z3.mk_numeral ctx "10" real_sort in
      let updt           = mk_tuple_update ctx p1 0 ten in
      let antecedent     = Z3.mk_eq ctx p2 updt in
      let x              = mk_unary_app ctx get_x_decl p2 in
      let consequent     = Z3.mk_eq ctx x ten in
      let thm            = Z3.mk_implies ctx antecedent consequent in
      printf "prove: p2 = update(p1, 0, 10) implies get_x(p2) = 10\n";
      prove ctx thm true;

      (* disprove that p2 = update(p1, 0, 10) implies get_y(p2) = 10 *)
      let y              = mk_unary_app ctx get_y_decl p2 in
      let consequent     = Z3.mk_eq ctx y ten in
      let thm            = Z3.mk_implies ctx antecedent consequent in
      printf "disprove: p2 = update(p1, 0, 10) implies get_y(p2) = 10\n";
      prove ctx thm false;
    end;

    Z3.del_context ctx;
  end