summaryrefslogtreecommitdiff
path: root/tests/hol4/misc-no_nested_borrows
diff options
context:
space:
mode:
Diffstat (limited to 'tests/hol4/misc-no_nested_borrows')
-rw-r--r--tests/hol4/misc-no_nested_borrows/Holmakefile5
-rw-r--r--tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml590
-rw-r--r--tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig1596
3 files changed, 2191 insertions, 0 deletions
diff --git a/tests/hol4/misc-no_nested_borrows/Holmakefile b/tests/hol4/misc-no_nested_borrows/Holmakefile
new file mode 100644
index 00000000..3c4b8973
--- /dev/null
+++ b/tests/hol4/misc-no_nested_borrows/Holmakefile
@@ -0,0 +1,5 @@
+# This file was automatically generated - modify ../Holmakefile.template instead
+INCLUDES = ../../../backends/hol4
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml
new file mode 100644
index 00000000..c8b106cd
--- /dev/null
+++ b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml
@@ -0,0 +1,590 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [no_nested_borrows] *)
+open primitivesLib divDefLib
+
+val _ = new_theory "noNestedBorrows"
+
+
+Datatype:
+ (** [no_nested_borrows::Pair] *)
+ pair_t = <| pair_x : 't1; pair_y : 't2; |>
+End
+
+Datatype:
+ (** [no_nested_borrows::List] *)
+ list_t = | ListCons 't list_t | ListNil
+End
+
+Datatype:
+ (** [no_nested_borrows::One] *)
+ one_t = | OneOne 't1
+End
+
+Datatype:
+ (** [no_nested_borrows::EmptyEnum] *)
+ empty_enum_t = | EmptyEnumEmpty
+End
+
+Datatype:
+ (** [no_nested_borrows::Enum] *)
+ enum_t = | EnumVariant1 | EnumVariant2
+End
+
+Type empty_struct_t = “: unit”
+
+Datatype:
+ (** [no_nested_borrows::Sum] *)
+ sum_t = | SumLeft 't1 | SumRight 't2
+End
+
+val neg_test_fwd_def = Define ‘
+ (** [no_nested_borrows::neg_test] *)
+ neg_test_fwd (x : i32) : i32 result =
+ i32_neg x
+’
+
+val add_test_fwd_def = Define ‘
+ (** [no_nested_borrows::add_test] *)
+ add_test_fwd (x : u32) (y : u32) : u32 result =
+ u32_add x y
+’
+
+val subs_test_fwd_def = Define ‘
+ (** [no_nested_borrows::subs_test] *)
+ subs_test_fwd (x : u32) (y : u32) : u32 result =
+ u32_sub x y
+’
+
+val div_test_fwd_def = Define ‘
+ (** [no_nested_borrows::div_test] *)
+ div_test_fwd (x : u32) (y : u32) : u32 result =
+ u32_div x y
+’
+
+val div_test1_fwd_def = Define ‘
+ (** [no_nested_borrows::div_test1] *)
+ div_test1_fwd (x : u32) : u32 result =
+ u32_div x (int_to_u32 2)
+’
+
+val rem_test_fwd_def = Define ‘
+ (** [no_nested_borrows::rem_test] *)
+ rem_test_fwd (x : u32) (y : u32) : u32 result =
+ u32_rem x y
+’
+
+val cast_test_fwd_def = Define ‘
+ (** [no_nested_borrows::cast_test] *)
+ cast_test_fwd (x : u32) : i32 result =
+ mk_i32 (u32_to_int x)
+’
+
+val test2_fwd_def = Define ‘
+ (** [no_nested_borrows::test2] *)
+ test2_fwd : unit result =
+ do
+ _ <- u32_add (int_to_u32 23) (int_to_u32 44);
+ Return ()
+ od
+’
+
+(** Unit test for [no_nested_borrows::test2] *)
+val _ = assert_return (“test2_fwd”)
+
+val get_max_fwd_def = Define ‘
+ (** [no_nested_borrows::get_max] *)
+ get_max_fwd (x : u32) (y : u32) : u32 result =
+ if u32_ge x y then Return x else Return y
+’
+
+val test3_fwd_def = Define ‘
+ (** [no_nested_borrows::test3] *)
+ test3_fwd : unit result =
+ do
+ x <- get_max_fwd (int_to_u32 4) (int_to_u32 3);
+ y <- get_max_fwd (int_to_u32 10) (int_to_u32 11);
+ z <- u32_add x y;
+ if ~ (z = int_to_u32 15) then Fail Failure else Return ()
+ od
+’
+
+(** Unit test for [no_nested_borrows::test3] *)
+val _ = assert_return (“test3_fwd”)
+
+val test_neg1_fwd_def = Define ‘
+ (** [no_nested_borrows::test_neg1] *)
+ test_neg1_fwd : unit result =
+ do
+ y <- i32_neg (int_to_i32 3);
+ if ~ (y = int_to_i32 (-3)) then Fail Failure else Return ()
+ od
+’
+
+(** Unit test for [no_nested_borrows::test_neg1] *)
+val _ = assert_return (“test_neg1_fwd”)
+
+val refs_test1_fwd_def = Define ‘
+ (** [no_nested_borrows::refs_test1] *)
+ refs_test1_fwd : unit result =
+ if ~ (int_to_i32 1 = int_to_i32 1) then Fail Failure else Return ()
+’
+
+(** Unit test for [no_nested_borrows::refs_test1] *)
+val _ = assert_return (“refs_test1_fwd”)
+
+val refs_test2_fwd_def = Define ‘
+ (** [no_nested_borrows::refs_test2] *)
+ refs_test2_fwd : unit result =
+ if ~ (int_to_i32 2 = int_to_i32 2)
+ then Fail Failure
+ else
+ if ~ (int_to_i32 0 = int_to_i32 0)
+ then Fail Failure
+ else
+ if ~ (int_to_i32 2 = int_to_i32 2)
+ then Fail Failure
+ else
+ if ~ (int_to_i32 2 = int_to_i32 2) then Fail Failure else Return ()
+’
+
+(** Unit test for [no_nested_borrows::refs_test2] *)
+val _ = assert_return (“refs_test2_fwd”)
+
+val test_list1_fwd_def = Define ‘
+ (** [no_nested_borrows::test_list1] *)
+ test_list1_fwd : unit result =
+ Return ()
+’
+
+(** Unit test for [no_nested_borrows::test_list1] *)
+val _ = assert_return (“test_list1_fwd”)
+
+val test_box1_fwd_def = Define ‘
+ (** [no_nested_borrows::test_box1] *)
+ test_box1_fwd : unit result =
+ let b = int_to_i32 1 in
+ let x = b in
+ if ~ (x = int_to_i32 1) then Fail Failure else Return ()
+’
+
+(** Unit test for [no_nested_borrows::test_box1] *)
+val _ = assert_return (“test_box1_fwd”)
+
+val copy_int_fwd_def = Define ‘
+ (** [no_nested_borrows::copy_int] *)
+ copy_int_fwd (x : i32) : i32 result =
+ Return x
+’
+
+val test_unreachable_fwd_def = Define ‘
+ (** [no_nested_borrows::test_unreachable] *)
+ test_unreachable_fwd (b : bool) : unit result =
+ if b then Fail Failure else Return ()
+’
+
+val test_panic_fwd_def = Define ‘
+ (** [no_nested_borrows::test_panic] *)
+ test_panic_fwd (b : bool) : unit result =
+ if b then Fail Failure else Return ()
+’
+
+val test_copy_int_fwd_def = Define ‘
+ (** [no_nested_borrows::test_copy_int] *)
+ test_copy_int_fwd : unit result =
+ do
+ y <- copy_int_fwd (int_to_i32 0);
+ if ~ (int_to_i32 0 = y) then Fail Failure else Return ()
+ od
+’
+
+(** Unit test for [no_nested_borrows::test_copy_int] *)
+val _ = assert_return (“test_copy_int_fwd”)
+
+val is_cons_fwd_def = Define ‘
+ (** [no_nested_borrows::is_cons] *)
+ is_cons_fwd (l : 't list_t) : bool result =
+ (case l of | ListCons t l0 => Return T | ListNil => Return F)
+’
+
+val test_is_cons_fwd_def = Define ‘
+ (** [no_nested_borrows::test_is_cons] *)
+ test_is_cons_fwd : unit result =
+ let l = ListNil in
+ do
+ b <- is_cons_fwd (ListCons (int_to_i32 0) l);
+ if ~ b then Fail Failure else Return ()
+ od
+’
+
+(** Unit test for [no_nested_borrows::test_is_cons] *)
+val _ = assert_return (“test_is_cons_fwd”)
+
+val split_list_fwd_def = Define ‘
+ (** [no_nested_borrows::split_list] *)
+ split_list_fwd (l : 't list_t) : ('t # 't list_t) result =
+ (case l of | ListCons hd tl => Return (hd, tl) | ListNil => Fail Failure)
+’
+
+val test_split_list_fwd_def = Define ‘
+ (** [no_nested_borrows::test_split_list] *)
+ test_split_list_fwd : unit result =
+ let l = ListNil in
+ do
+ p <- split_list_fwd (ListCons (int_to_i32 0) l);
+ let (hd, _) = p in
+ if ~ (hd = int_to_i32 0) then Fail Failure else Return ()
+ od
+’
+
+(** Unit test for [no_nested_borrows::test_split_list] *)
+val _ = assert_return (“test_split_list_fwd”)
+
+val choose_fwd_def = Define ‘
+ (** [no_nested_borrows::choose] *)
+ choose_fwd (b : bool) (x : 't) (y : 't) : 't result =
+ if b then Return x else Return y
+’
+
+val choose_back_def = Define ‘
+ (** [no_nested_borrows::choose] *)
+ choose_back (b : bool) (x : 't) (y : 't) (ret : 't) : ('t # 't) result =
+ if b then Return (ret, y) else Return (x, ret)
+’
+
+val choose_test_fwd_def = Define ‘
+ (** [no_nested_borrows::choose_test] *)
+ choose_test_fwd : unit result =
+ do
+ z <- choose_fwd T (int_to_i32 0) (int_to_i32 0);
+ z0 <- i32_add z (int_to_i32 1);
+ if ~ (z0 = int_to_i32 1)
+ then Fail Failure
+ else (
+ do
+ (x, y) <- choose_back T (int_to_i32 0) (int_to_i32 0) z0;
+ if ~ (x = int_to_i32 1)
+ then Fail Failure
+ else if ~ (y = int_to_i32 0) then Fail Failure else Return ()
+ od)
+ od
+’
+
+(** Unit test for [no_nested_borrows::choose_test] *)
+val _ = assert_return (“choose_test_fwd”)
+
+val test_char_fwd_def = Define ‘
+ (** [no_nested_borrows::test_char] *)
+ test_char_fwd : char result =
+ Return #"a"
+’
+
+Datatype:
+ (** [no_nested_borrows::NodeElem] *)
+ node_elem_t = | NodeElemCons tree_t node_elem_t | NodeElemNil ;
+
+ (** [no_nested_borrows::Tree] *)
+ tree_t = | TreeLeaf 't | TreeNode 't node_elem_t tree_t
+End
+
+val [list_length_fwd_def] = DefineDiv ‘
+ (** [no_nested_borrows::list_length] *)
+ list_length_fwd (l : 't list_t) : u32 result =
+ (case l of
+ | ListCons t l1 => do
+ i <- list_length_fwd l1;
+ u32_add (int_to_u32 1) i
+ od
+ | ListNil => Return (int_to_u32 0))
+’
+
+val [list_nth_shared_fwd_def] = DefineDiv ‘
+ (** [no_nested_borrows::list_nth_shared] *)
+ list_nth_shared_fwd (l : 't list_t) (i : u32) : 't result =
+ (case l of
+ | ListCons x tl =>
+ if i = int_to_u32 0
+ then Return x
+ else (do
+ i0 <- u32_sub i (int_to_u32 1);
+ list_nth_shared_fwd tl i0
+ od)
+ | ListNil => Fail Failure)
+’
+
+val [list_nth_mut_fwd_def] = DefineDiv ‘
+ (** [no_nested_borrows::list_nth_mut] *)
+ list_nth_mut_fwd (l : 't list_t) (i : u32) : 't result =
+ (case l of
+ | ListCons x tl =>
+ if i = int_to_u32 0
+ then Return x
+ else (do
+ i0 <- u32_sub i (int_to_u32 1);
+ list_nth_mut_fwd tl i0
+ od)
+ | ListNil => Fail Failure)
+’
+
+val [list_nth_mut_back_def] = DefineDiv ‘
+ (** [no_nested_borrows::list_nth_mut] *)
+ list_nth_mut_back (l : 't list_t) (i : u32) (ret : 't) : 't list_t result =
+ (case l of
+ | ListCons x tl =>
+ if i = int_to_u32 0
+ then Return (ListCons ret tl)
+ else (
+ do
+ i0 <- u32_sub i (int_to_u32 1);
+ tl0 <- list_nth_mut_back tl i0 ret;
+ Return (ListCons x tl0)
+ od)
+ | ListNil => Fail Failure)
+’
+
+val [list_rev_aux_fwd_def] = DefineDiv ‘
+ (** [no_nested_borrows::list_rev_aux] *)
+ list_rev_aux_fwd (li : 't list_t) (lo : 't list_t) : 't list_t result =
+ (case li of
+ | ListCons hd tl => list_rev_aux_fwd tl (ListCons hd lo)
+ | ListNil => Return lo)
+’
+
+val list_rev_fwd_back_def = Define ‘
+ (** [no_nested_borrows::list_rev] *)
+ list_rev_fwd_back (l : 't list_t) : 't list_t result =
+ let li = mem_replace_fwd l ListNil in list_rev_aux_fwd li ListNil
+’
+
+val test_list_functions_fwd_def = Define ‘
+ (** [no_nested_borrows::test_list_functions] *)
+ test_list_functions_fwd : unit result =
+ let l = ListNil in
+ let l0 = ListCons (int_to_i32 2) l in
+ let l1 = ListCons (int_to_i32 1) l0 in
+ do
+ i <- list_length_fwd (ListCons (int_to_i32 0) l1);
+ if ~ (i = int_to_u32 3)
+ then Fail Failure
+ else (
+ do
+ i0 <- list_nth_shared_fwd (ListCons (int_to_i32 0) l1) (int_to_u32 0);
+ if ~ (i0 = int_to_i32 0)
+ then Fail Failure
+ else (
+ do
+ i1 <- list_nth_shared_fwd (ListCons (int_to_i32 0) l1) (int_to_u32 1);
+ if ~ (i1 = int_to_i32 1)
+ then Fail Failure
+ else (
+ do
+ i2 <-
+ list_nth_shared_fwd (ListCons (int_to_i32 0) l1) (int_to_u32 2);
+ if ~ (i2 = int_to_i32 2)
+ then Fail Failure
+ else (
+ do
+ ls <-
+ list_nth_mut_back (ListCons (int_to_i32 0) l1) (int_to_u32 1)
+ (int_to_i32 3);
+ i3 <- list_nth_shared_fwd ls (int_to_u32 0);
+ if ~ (i3 = int_to_i32 0)
+ then Fail Failure
+ else (
+ do
+ i4 <- list_nth_shared_fwd ls (int_to_u32 1);
+ if ~ (i4 = int_to_i32 3)
+ then Fail Failure
+ else (
+ do
+ i5 <- list_nth_shared_fwd ls (int_to_u32 2);
+ if ~ (i5 = int_to_i32 2) then Fail Failure else Return ()
+ od)
+ od)
+ od)
+ od)
+ od)
+ od)
+ od
+’
+
+(** Unit test for [no_nested_borrows::test_list_functions] *)
+val _ = assert_return (“test_list_functions_fwd”)
+
+val id_mut_pair1_fwd_def = Define ‘
+ (** [no_nested_borrows::id_mut_pair1] *)
+ id_mut_pair1_fwd (x : 't1) (y : 't2) : ('t1 # 't2) result =
+ Return (x, y)
+’
+
+val id_mut_pair1_back_def = Define ‘
+ (** [no_nested_borrows::id_mut_pair1] *)
+ id_mut_pair1_back
+ (x : 't1) (y : 't2) (ret : ('t1 # 't2)) : ('t1 # 't2) result =
+ let (t, t0) = ret in Return (t, t0)
+’
+
+val id_mut_pair2_fwd_def = Define ‘
+ (** [no_nested_borrows::id_mut_pair2] *)
+ id_mut_pair2_fwd (p : ('t1 # 't2)) : ('t1 # 't2) result =
+ let (t, t0) = p in Return (t, t0)
+’
+
+val id_mut_pair2_back_def = Define ‘
+ (** [no_nested_borrows::id_mut_pair2] *)
+ id_mut_pair2_back
+ (p : ('t1 # 't2)) (ret : ('t1 # 't2)) : ('t1 # 't2) result =
+ let (t, t0) = ret in Return (t, t0)
+’
+
+val id_mut_pair3_fwd_def = Define ‘
+ (** [no_nested_borrows::id_mut_pair3] *)
+ id_mut_pair3_fwd (x : 't1) (y : 't2) : ('t1 # 't2) result =
+ Return (x, y)
+’
+
+val id_mut_pair3_back'a_def = Define ‘
+ (** [no_nested_borrows::id_mut_pair3] *)
+ id_mut_pair3_back'a (x : 't1) (y : 't2) (ret : 't1) : 't1 result =
+ Return ret
+’
+
+val id_mut_pair3_back'b_def = Define ‘
+ (** [no_nested_borrows::id_mut_pair3] *)
+ id_mut_pair3_back'b (x : 't1) (y : 't2) (ret : 't2) : 't2 result =
+ Return ret
+’
+
+val id_mut_pair4_fwd_def = Define ‘
+ (** [no_nested_borrows::id_mut_pair4] *)
+ id_mut_pair4_fwd (p : ('t1 # 't2)) : ('t1 # 't2) result =
+ let (t, t0) = p in Return (t, t0)
+’
+
+val id_mut_pair4_back'a_def = Define ‘
+ (** [no_nested_borrows::id_mut_pair4] *)
+ id_mut_pair4_back'a (p : ('t1 # 't2)) (ret : 't1) : 't1 result =
+ Return ret
+’
+
+val id_mut_pair4_back'b_def = Define ‘
+ (** [no_nested_borrows::id_mut_pair4] *)
+ id_mut_pair4_back'b (p : ('t1 # 't2)) (ret : 't2) : 't2 result =
+ Return ret
+’
+
+Datatype:
+ (** [no_nested_borrows::StructWithTuple] *)
+ struct_with_tuple_t = <| struct_with_tuple_p : ('t1 # 't2); |>
+End
+
+val new_tuple1_fwd_def = Define ‘
+ (** [no_nested_borrows::new_tuple1] *)
+ new_tuple1_fwd : (u32, u32) struct_with_tuple_t result =
+ Return (<| struct_with_tuple_p := (int_to_u32 1, int_to_u32 2) |>)
+’
+
+val new_tuple2_fwd_def = Define ‘
+ (** [no_nested_borrows::new_tuple2] *)
+ new_tuple2_fwd : (i16, i16) struct_with_tuple_t result =
+ Return (<| struct_with_tuple_p := (int_to_i16 1, int_to_i16 2) |>)
+’
+
+val new_tuple3_fwd_def = Define ‘
+ (** [no_nested_borrows::new_tuple3] *)
+ new_tuple3_fwd : (u64, i64) struct_with_tuple_t result =
+ Return (<| struct_with_tuple_p := (int_to_u64 1, int_to_i64 2) |>)
+’
+
+Datatype:
+ (** [no_nested_borrows::StructWithPair] *)
+ struct_with_pair_t = <| struct_with_pair_p : ('t1, 't2) pair_t; |>
+End
+
+val new_pair1_fwd_def = Define ‘
+ (** [no_nested_borrows::new_pair1] *)
+ new_pair1_fwd : (u32, u32) struct_with_pair_t result =
+ Return
+ (<|
+ struct_with_pair_p :=
+ (<| pair_x := (int_to_u32 1); pair_y := (int_to_u32 2) |>)
+ |>)
+’
+
+val test_constants_fwd_def = Define ‘
+ (** [no_nested_borrows::test_constants] *)
+ test_constants_fwd : unit result =
+ do
+ swt <- new_tuple1_fwd;
+ let (i, _) = swt.struct_with_tuple_p in
+ if ~ (i = int_to_u32 1)
+ then Fail Failure
+ else (
+ do
+ swt0 <- new_tuple2_fwd;
+ let (i0, _) = swt0.struct_with_tuple_p in
+ if ~ (i0 = int_to_i16 1)
+ then Fail Failure
+ else (
+ do
+ swt1 <- new_tuple3_fwd;
+ let (i1, _) = swt1.struct_with_tuple_p in
+ if ~ (i1 = int_to_u64 1)
+ then Fail Failure
+ else (
+ do
+ swp <- new_pair1_fwd;
+ if ~ (swp.struct_with_pair_p.pair_x = int_to_u32 1)
+ then Fail Failure
+ else Return ()
+ od)
+ od)
+ od)
+ od
+’
+
+(** Unit test for [no_nested_borrows::test_constants] *)
+val _ = assert_return (“test_constants_fwd”)
+
+val test_weird_borrows1_fwd_def = Define ‘
+ (** [no_nested_borrows::test_weird_borrows1] *)
+ test_weird_borrows1_fwd : unit result =
+ Return ()
+’
+
+(** Unit test for [no_nested_borrows::test_weird_borrows1] *)
+val _ = assert_return (“test_weird_borrows1_fwd”)
+
+val test_mem_replace_fwd_back_def = Define ‘
+ (** [no_nested_borrows::test_mem_replace] *)
+ test_mem_replace_fwd_back (px : u32) : u32 result =
+ let y = mem_replace_fwd px (int_to_u32 1) in
+ if ~ (y = int_to_u32 0) then Fail Failure else Return (int_to_u32 2)
+’
+
+val test_shared_borrow_bool1_fwd_def = Define ‘
+ (** [no_nested_borrows::test_shared_borrow_bool1] *)
+ test_shared_borrow_bool1_fwd (b : bool) : u32 result =
+ if b then Return (int_to_u32 0) else Return (int_to_u32 1)
+’
+
+val test_shared_borrow_bool2_fwd_def = Define ‘
+ (** [no_nested_borrows::test_shared_borrow_bool2] *)
+ test_shared_borrow_bool2_fwd : u32 result =
+ Return (int_to_u32 0)
+’
+
+val test_shared_borrow_enum1_fwd_def = Define ‘
+ (** [no_nested_borrows::test_shared_borrow_enum1] *)
+ test_shared_borrow_enum1_fwd (l : u32 list_t) : u32 result =
+ (case l of
+ | ListCons i l0 => Return (int_to_u32 1)
+ | ListNil => Return (int_to_u32 0))
+’
+
+val test_shared_borrow_enum2_fwd_def = Define ‘
+ (** [no_nested_borrows::test_shared_borrow_enum2] *)
+ test_shared_borrow_enum2_fwd : u32 result =
+ Return (int_to_u32 0)
+’
+
+val _ = export_theory ()
diff --git a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig
new file mode 100644
index 00000000..82c842be
--- /dev/null
+++ b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig
@@ -0,0 +1,1596 @@
+signature noNestedBorrowsTheory =
+sig
+ type thm = Thm.thm
+
+ (* Definitions *)
+ val add_test_fwd_def : thm
+ val cast_test_fwd_def : thm
+ val choose_back_def : thm
+ val choose_fwd_def : thm
+ val choose_test_fwd_def : thm
+ val copy_int_fwd_def : thm
+ val div_test1_fwd_def : thm
+ val div_test_fwd_def : thm
+ val empty_enum_t_BIJ : thm
+ val empty_enum_t_CASE : thm
+ val empty_enum_t_TY_DEF : thm
+ val empty_enum_t_size_def : thm
+ val enum_t_BIJ : thm
+ val enum_t_CASE : thm
+ val enum_t_TY_DEF : thm
+ val enum_t_size_def : thm
+ val get_max_fwd_def : thm
+ val id_mut_pair1_back_def : thm
+ val id_mut_pair1_fwd_def : thm
+ val id_mut_pair2_back_def : thm
+ val id_mut_pair2_fwd_def : thm
+ val id_mut_pair3_back'a_def : thm
+ val id_mut_pair3_back'b_def : thm
+ val id_mut_pair3_fwd_def : thm
+ val id_mut_pair4_back'a_def : thm
+ val id_mut_pair4_back'b_def : thm
+ val id_mut_pair4_fwd_def : thm
+ val is_cons_fwd_def : thm
+ val list_length_fwd_def : thm
+ val list_nth_mut_back_def : thm
+ val list_nth_mut_fwd_def : thm
+ val list_nth_shared_fwd_def : thm
+ val list_rev_aux_fwd_def : thm
+ val list_rev_fwd_back_def : thm
+ val list_t_TY_DEF : thm
+ val list_t_case_def : thm
+ val list_t_size_def : thm
+ val neg_test_fwd_def : thm
+ val new_pair1_fwd_def : thm
+ val new_tuple1_fwd_def : thm
+ val new_tuple2_fwd_def : thm
+ val new_tuple3_fwd_def : thm
+ val node_elem_t_TY_DEF : thm
+ val node_elem_t_case_def : thm
+ val node_elem_t_size_def : thm
+ val one_t_TY_DEF : thm
+ val one_t_case_def : thm
+ val one_t_size_def : thm
+ val pair_t_TY_DEF : thm
+ val pair_t_case_def : thm
+ val pair_t_size_def : thm
+ val recordtype_pair_t_seldef_pair_x_def : thm
+ val recordtype_pair_t_seldef_pair_x_fupd_def : thm
+ val recordtype_pair_t_seldef_pair_y_def : thm
+ val recordtype_pair_t_seldef_pair_y_fupd_def : thm
+ val recordtype_struct_with_pair_t_seldef_struct_with_pair_p_def : thm
+ val recordtype_struct_with_pair_t_seldef_struct_with_pair_p_fupd_def : thm
+ val recordtype_struct_with_tuple_t_seldef_struct_with_tuple_p_def : thm
+ val recordtype_struct_with_tuple_t_seldef_struct_with_tuple_p_fupd_def : thm
+ val refs_test1_fwd_def : thm
+ val refs_test2_fwd_def : thm
+ val rem_test_fwd_def : thm
+ val split_list_fwd_def : thm
+ val struct_with_pair_t_TY_DEF : thm
+ val struct_with_pair_t_case_def : thm
+ val struct_with_pair_t_size_def : thm
+ val struct_with_tuple_t_TY_DEF : thm
+ val struct_with_tuple_t_case_def : thm
+ val struct_with_tuple_t_size_def : thm
+ val subs_test_fwd_def : thm
+ val sum_t_TY_DEF : thm
+ val sum_t_case_def : thm
+ val sum_t_size_def : thm
+ val test2_fwd_def : thm
+ val test3_fwd_def : thm
+ val test_box1_fwd_def : thm
+ val test_char_fwd_def : thm
+ val test_constants_fwd_def : thm
+ val test_copy_int_fwd_def : thm
+ val test_is_cons_fwd_def : thm
+ val test_list1_fwd_def : thm
+ val test_list_functions_fwd_def : thm
+ val test_mem_replace_fwd_back_def : thm
+ val test_neg1_fwd_def : thm
+ val test_panic_fwd_def : thm
+ val test_shared_borrow_bool1_fwd_def : thm
+ val test_shared_borrow_bool2_fwd_def : thm
+ val test_shared_borrow_enum1_fwd_def : thm
+ val test_shared_borrow_enum2_fwd_def : thm
+ val test_split_list_fwd_def : thm
+ val test_unreachable_fwd_def : thm
+ val test_weird_borrows1_fwd_def : thm
+ val tree_t_TY_DEF : thm
+ val tree_t_case_def : thm
+
+ (* Theorems *)
+ val EXISTS_pair_t : thm
+ val EXISTS_struct_with_pair_t : thm
+ val EXISTS_struct_with_tuple_t : thm
+ val FORALL_pair_t : thm
+ val FORALL_struct_with_pair_t : thm
+ val FORALL_struct_with_tuple_t : thm
+ val datatype_empty_enum_t : thm
+ val datatype_enum_t : thm
+ val datatype_list_t : thm
+ val datatype_node_elem_t : thm
+ val datatype_one_t : thm
+ val datatype_pair_t : thm
+ val datatype_struct_with_pair_t : thm
+ val datatype_struct_with_tuple_t : thm
+ val datatype_sum_t : thm
+ val empty_enum_t2num_11 : thm
+ val empty_enum_t2num_ONTO : thm
+ val empty_enum_t2num_num2empty_enum_t : thm
+ val empty_enum_t2num_thm : thm
+ val empty_enum_t_Axiom : thm
+ val empty_enum_t_EQ_empty_enum_t : thm
+ val empty_enum_t_case_cong : thm
+ val empty_enum_t_case_def : thm
+ val empty_enum_t_case_eq : thm
+ val empty_enum_t_induction : thm
+ val empty_enum_t_nchotomy : thm
+ val enum_t2num_11 : thm
+ val enum_t2num_ONTO : thm
+ val enum_t2num_num2enum_t : thm
+ val enum_t2num_thm : thm
+ val enum_t_Axiom : thm
+ val enum_t_EQ_enum_t : thm
+ val enum_t_case_cong : thm
+ val enum_t_case_def : thm
+ val enum_t_case_eq : thm
+ val enum_t_distinct : thm
+ val enum_t_induction : thm
+ val enum_t_nchotomy : thm
+ val list_t_11 : thm
+ val list_t_Axiom : thm
+ val list_t_case_cong : thm
+ val list_t_case_eq : thm
+ val list_t_distinct : thm
+ val list_t_induction : thm
+ val list_t_nchotomy : thm
+ val node_elem_t_11 : thm
+ val node_elem_t_Axiom : thm
+ val node_elem_t_case_cong : thm
+ val node_elem_t_case_eq : thm
+ val node_elem_t_distinct : thm
+ val node_elem_t_induction : thm
+ val node_elem_t_nchotomy : thm
+ val num2empty_enum_t_11 : thm
+ val num2empty_enum_t_ONTO : thm
+ val num2empty_enum_t_empty_enum_t2num : thm
+ val num2empty_enum_t_thm : thm
+ val num2enum_t_11 : thm
+ val num2enum_t_ONTO : thm
+ val num2enum_t_enum_t2num : thm
+ val num2enum_t_thm : thm
+ val one_t_11 : thm
+ val one_t_Axiom : thm
+ val one_t_case_cong : thm
+ val one_t_case_eq : thm
+ val one_t_induction : thm
+ val one_t_nchotomy : thm
+ val pair_t_11 : thm
+ val pair_t_Axiom : thm
+ val pair_t_accessors : thm
+ val pair_t_accfupds : thm
+ val pair_t_case_cong : thm
+ val pair_t_case_eq : thm
+ val pair_t_component_equality : thm
+ val pair_t_fn_updates : thm
+ val pair_t_fupdcanon : thm
+ val pair_t_fupdcanon_comp : thm
+ val pair_t_fupdfupds : thm
+ val pair_t_fupdfupds_comp : thm
+ val pair_t_induction : thm
+ val pair_t_literal_11 : thm
+ val pair_t_literal_nchotomy : thm
+ val pair_t_nchotomy : thm
+ val pair_t_updates_eq_literal : thm
+ val struct_with_pair_t_11 : thm
+ val struct_with_pair_t_Axiom : thm
+ val struct_with_pair_t_accessors : thm
+ val struct_with_pair_t_accfupds : thm
+ val struct_with_pair_t_case_cong : thm
+ val struct_with_pair_t_case_eq : thm
+ val struct_with_pair_t_component_equality : thm
+ val struct_with_pair_t_fn_updates : thm
+ val struct_with_pair_t_fupdfupds : thm
+ val struct_with_pair_t_fupdfupds_comp : thm
+ val struct_with_pair_t_induction : thm
+ val struct_with_pair_t_literal_11 : thm
+ val struct_with_pair_t_literal_nchotomy : thm
+ val struct_with_pair_t_nchotomy : thm
+ val struct_with_pair_t_updates_eq_literal : thm
+ val struct_with_tuple_t_11 : thm
+ val struct_with_tuple_t_Axiom : thm
+ val struct_with_tuple_t_accessors : thm
+ val struct_with_tuple_t_accfupds : thm
+ val struct_with_tuple_t_case_cong : thm
+ val struct_with_tuple_t_case_eq : thm
+ val struct_with_tuple_t_component_equality : thm
+ val struct_with_tuple_t_fn_updates : thm
+ val struct_with_tuple_t_fupdfupds : thm
+ val struct_with_tuple_t_fupdfupds_comp : thm
+ val struct_with_tuple_t_induction : thm
+ val struct_with_tuple_t_literal_11 : thm
+ val struct_with_tuple_t_literal_nchotomy : thm
+ val struct_with_tuple_t_nchotomy : thm
+ val struct_with_tuple_t_updates_eq_literal : thm
+ val sum_t_11 : thm
+ val sum_t_Axiom : thm
+ val sum_t_case_cong : thm
+ val sum_t_case_eq : thm
+ val sum_t_distinct : thm
+ val sum_t_induction : thm
+ val sum_t_nchotomy : thm
+ val tree_t_11 : thm
+ val tree_t_Axiom : thm
+ val tree_t_case_cong : thm
+ val tree_t_case_eq : thm
+ val tree_t_distinct : thm
+ val tree_t_induction : thm
+ val tree_t_nchotomy : thm
+
+ val noNestedBorrows_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+ [divDef] Parent theory of "noNestedBorrows"
+
+ [add_test_fwd_def] Definition
+
+ ⊢ ∀x y. add_test_fwd x y = u32_add x y
+
+ [cast_test_fwd_def] Definition
+
+ ⊢ ∀x. cast_test_fwd x = mk_i32 (u32_to_int x)
+
+ [choose_back_def] Definition
+
+ ⊢ ∀b x y ret.
+ choose_back b x y ret =
+ if b then Return (ret,y) else Return (x,ret)
+
+ [choose_fwd_def] Definition
+
+ ⊢ ∀b x y. choose_fwd b x y = if b then Return x else Return y
+
+ [choose_test_fwd_def] Definition
+
+ ⊢ choose_test_fwd =
+ do
+ z <- choose_fwd T (int_to_i32 0) (int_to_i32 0);
+ z0 <- i32_add z (int_to_i32 1);
+ if z0 ≠ int_to_i32 1 then Fail Failure
+ else
+ do
+ (x,y) <- choose_back T (int_to_i32 0) (int_to_i32 0) z0;
+ if x ≠ int_to_i32 1 then Fail Failure
+ else if y ≠ int_to_i32 0 then Fail Failure
+ else Return ()
+ od
+ od
+
+ [copy_int_fwd_def] Definition
+
+ ⊢ ∀x. copy_int_fwd x = Return x
+
+ [div_test1_fwd_def] Definition
+
+ ⊢ ∀x. div_test1_fwd x = u32_div x (int_to_u32 2)
+
+ [div_test_fwd_def] Definition
+
+ ⊢ ∀x y. div_test_fwd x y = u32_div x y
+
+ [empty_enum_t_BIJ] Definition
+
+ ⊢ (∀a. num2empty_enum_t (empty_enum_t2num a) = a) ∧
+ ∀r. (λn. n < 1) r ⇔ empty_enum_t2num (num2empty_enum_t r) = r
+
+ [empty_enum_t_CASE] Definition
+
+ ⊢ ∀x v0.
+ (case x of EmptyEnumEmpty => v0) = (λm. v0) (empty_enum_t2num x)
+
+ [empty_enum_t_TY_DEF] Definition
+
+ ⊢ ∃rep. TYPE_DEFINITION (λn. n < 1) rep
+
+ [empty_enum_t_size_def] Definition
+
+ ⊢ ∀x. empty_enum_t_size x = 0
+
+ [enum_t_BIJ] Definition
+
+ ⊢ (∀a. num2enum_t (enum_t2num a) = a) ∧
+ ∀r. (λn. n < 2) r ⇔ enum_t2num (num2enum_t r) = r
+
+ [enum_t_CASE] Definition
+
+ ⊢ ∀x v0 v1.
+ (case x of EnumVariant1 => v0 | EnumVariant2 => v1) =
+ (λm. if m = 0 then v0 else v1) (enum_t2num x)
+
+ [enum_t_TY_DEF] Definition
+
+ ⊢ ∃rep. TYPE_DEFINITION (λn. n < 2) rep
+
+ [enum_t_size_def] Definition
+
+ ⊢ ∀x. enum_t_size x = 0
+
+ [get_max_fwd_def] Definition
+
+ ⊢ ∀x y. get_max_fwd x y = if u32_ge x y then Return x else Return y
+
+ [id_mut_pair1_back_def] Definition
+
+ ⊢ ∀x y ret.
+ id_mut_pair1_back x y ret = (let (t,t0) = ret in Return (t,t0))
+
+ [id_mut_pair1_fwd_def] Definition
+
+ ⊢ ∀x y. id_mut_pair1_fwd x y = Return (x,y)
+
+ [id_mut_pair2_back_def] Definition
+
+ ⊢ ∀p ret.
+ id_mut_pair2_back p ret = (let (t,t0) = ret in Return (t,t0))
+
+ [id_mut_pair2_fwd_def] Definition
+
+ ⊢ ∀p. id_mut_pair2_fwd p = (let (t,t0) = p in Return (t,t0))
+
+ [id_mut_pair3_back'a_def] Definition
+
+ ⊢ ∀x y ret. id_mut_pair3_back'a x y ret = Return ret
+
+ [id_mut_pair3_back'b_def] Definition
+
+ ⊢ ∀x y ret. id_mut_pair3_back'b x y ret = Return ret
+
+ [id_mut_pair3_fwd_def] Definition
+
+ ⊢ ∀x y. id_mut_pair3_fwd x y = Return (x,y)
+
+ [id_mut_pair4_back'a_def] Definition
+
+ ⊢ ∀p ret. id_mut_pair4_back'a p ret = Return ret
+
+ [id_mut_pair4_back'b_def] Definition
+
+ ⊢ ∀p ret. id_mut_pair4_back'b p ret = Return ret
+
+ [id_mut_pair4_fwd_def] Definition
+
+ ⊢ ∀p. id_mut_pair4_fwd p = (let (t,t0) = p in Return (t,t0))
+
+ [is_cons_fwd_def] Definition
+
+ ⊢ ∀l. is_cons_fwd l =
+ case l of ListCons t l0 => Return T | ListNil => Return F
+
+ [list_length_fwd_def] Definition
+
+ ⊢ ∀l. list_length_fwd l =
+ case l of
+ ListCons t l1 =>
+ do i <- list_length_fwd l1; u32_add (int_to_u32 1) i od
+ | ListNil => Return (int_to_u32 0)
+
+ [list_nth_mut_back_def] Definition
+
+ ⊢ ∀l i ret.
+ list_nth_mut_back l i ret =
+ case l of
+ ListCons x tl =>
+ if i = int_to_u32 0 then Return (ListCons ret tl)
+ else
+ do
+ i0 <- u32_sub i (int_to_u32 1);
+ tl0 <- list_nth_mut_back tl i0 ret;
+ Return (ListCons x tl0)
+ od
+ | ListNil => Fail Failure
+
+ [list_nth_mut_fwd_def] Definition
+
+ ⊢ ∀l i.
+ list_nth_mut_fwd l i =
+ case l of
+ ListCons x tl =>
+ if i = int_to_u32 0 then Return x
+ else
+ do
+ i0 <- u32_sub i (int_to_u32 1);
+ list_nth_mut_fwd tl i0
+ od
+ | ListNil => Fail Failure
+
+ [list_nth_shared_fwd_def] Definition
+
+ ⊢ ∀l i.
+ list_nth_shared_fwd l i =
+ case l of
+ ListCons x tl =>
+ if i = int_to_u32 0 then Return x
+ else
+ do
+ i0 <- u32_sub i (int_to_u32 1);
+ list_nth_shared_fwd tl i0
+ od
+ | ListNil => Fail Failure
+
+ [list_rev_aux_fwd_def] Definition
+
+ ⊢ ∀li lo.
+ list_rev_aux_fwd li lo =
+ case li of
+ ListCons hd tl => list_rev_aux_fwd tl (ListCons hd lo)
+ | ListNil => Return lo
+
+ [list_rev_fwd_back_def] Definition
+
+ ⊢ ∀l. list_rev_fwd_back l =
+ (let
+ li = mem_replace_fwd l ListNil
+ in
+ list_rev_aux_fwd li ListNil)
+
+ [list_t_TY_DEF] Definition
+
+ ⊢ ∃rep.
+ TYPE_DEFINITION
+ (λa0'.
+ ∀ $var$('list_t').
+ (∀a0'.
+ (∃a0 a1.
+ a0' =
+ (λa0 a1.
+ ind_type$CONSTR 0 a0
+ (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
+ a0 a1 ∧ $var$('list_t') a1) ∨
+ a0' =
+ ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
+ $var$('list_t') a0') ⇒
+ $var$('list_t') a0') rep
+
+ [list_t_case_def] Definition
+
+ ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
+ ∀f v. list_t_CASE ListNil f v = v
+
+ [list_t_size_def] Definition
+
+ ⊢ (∀f a0 a1.
+ list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
+ ∀f. list_t_size f ListNil = 0
+
+ [neg_test_fwd_def] Definition
+
+ ⊢ ∀x. neg_test_fwd x = i32_neg x
+
+ [new_pair1_fwd_def] Definition
+
+ ⊢ new_pair1_fwd =
+ Return
+ <|struct_with_pair_p :=
+ <|pair_x := int_to_u32 1; pair_y := int_to_u32 2|> |>
+
+ [new_tuple1_fwd_def] Definition
+
+ ⊢ new_tuple1_fwd =
+ Return <|struct_with_tuple_p := (int_to_u32 1,int_to_u32 2)|>
+
+ [new_tuple2_fwd_def] Definition
+
+ ⊢ new_tuple2_fwd =
+ Return <|struct_with_tuple_p := (int_to_i16 1,int_to_i16 2)|>
+
+ [new_tuple3_fwd_def] Definition
+
+ ⊢ new_tuple3_fwd =
+ Return <|struct_with_tuple_p := (int_to_u64 1,int_to_i64 2)|>
+
+ [node_elem_t_TY_DEF] Definition
+
+ ⊢ ∃rep.
+ TYPE_DEFINITION
+ (λa0'.
+ ∀ $var$('node_elem_t') $var$('tree_t').
+ (∀a0'.
+ (∃a0 a1.
+ a0' =
+ (λa0 a1.
+ ind_type$CONSTR 0 ARB
+ (ind_type$FCONS a0
+ (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
+ a0 a1 ∧ $var$('tree_t') a0 ∧
+ $var$('node_elem_t') a1) ∨
+ a0' =
+ ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
+ $var$('node_elem_t') a0') ∧
+ (∀a1'.
+ (∃a. a1' =
+ (λa.
+ ind_type$CONSTR (SUC (SUC 0)) a
+ (λn. ind_type$BOTTOM)) a) ∨
+ (∃a0 a1 a2.
+ a1' =
+ (λa0 a1 a2.
+ ind_type$CONSTR (SUC (SUC (SUC 0))) a0
+ (ind_type$FCONS a1
+ (ind_type$FCONS a2 (λn. ind_type$BOTTOM))))
+ a0 a1 a2 ∧ $var$('node_elem_t') a1 ∧
+ $var$('tree_t') a2) ⇒
+ $var$('tree_t') a1') ⇒
+ $var$('node_elem_t') a0') rep
+
+ [node_elem_t_case_def] Definition
+
+ ⊢ (∀a0 a1 f v. node_elem_t_CASE (NodeElemCons a0 a1) f v = f a0 a1) ∧
+ ∀f v. node_elem_t_CASE NodeElemNil f v = v
+
+ [node_elem_t_size_def] Definition
+
+ ⊢ (∀f a0 a1.
+ node_elem_t_size f (NodeElemCons a0 a1) =
+ 1 + (tree_t_size f a0 + node_elem_t_size f a1)) ∧
+ (∀f. node_elem_t_size f NodeElemNil = 0) ∧
+ (∀f a. tree_t_size f (TreeLeaf a) = 1 + f a) ∧
+ ∀f a0 a1 a2.
+ tree_t_size f (TreeNode a0 a1 a2) =
+ 1 + (f a0 + (node_elem_t_size f a1 + tree_t_size f a2))
+
+ [one_t_TY_DEF] Definition
+
+ ⊢ ∃rep.
+ TYPE_DEFINITION
+ (λa0.
+ ∀ $var$('one_t').
+ (∀a0.
+ (∃a. a0 =
+ (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
+ a) ⇒
+ $var$('one_t') a0) ⇒
+ $var$('one_t') a0) rep
+
+ [one_t_case_def] Definition
+
+ ⊢ ∀a f. one_t_CASE (OneOne a) f = f a
+
+ [one_t_size_def] Definition
+
+ ⊢ ∀f a. one_t_size f (OneOne a) = 1 + f a
+
+ [pair_t_TY_DEF] Definition
+
+ ⊢ ∃rep.
+ TYPE_DEFINITION
+ (λa0'.
+ ∀ $var$('pair_t').
+ (∀a0'.
+ (∃a0 a1.
+ a0' =
+ (λa0 a1.
+ ind_type$CONSTR 0 (a0,a1)
+ (λn. ind_type$BOTTOM)) a0 a1) ⇒
+ $var$('pair_t') a0') ⇒
+ $var$('pair_t') a0') rep
+
+ [pair_t_case_def] Definition
+
+ ⊢ ∀a0 a1 f. pair_t_CASE (pair_t a0 a1) f = f a0 a1
+
+ [pair_t_size_def] Definition
+
+ ⊢ ∀f f1 a0 a1. pair_t_size f f1 (pair_t a0 a1) = 1 + (f a0 + f1 a1)
+
+ [recordtype_pair_t_seldef_pair_x_def] Definition
+
+ ⊢ ∀t t0. (pair_t t t0).pair_x = t
+
+ [recordtype_pair_t_seldef_pair_x_fupd_def] Definition
+
+ ⊢ ∀f t t0. pair_t t t0 with pair_x updated_by f = pair_t (f t) t0
+
+ [recordtype_pair_t_seldef_pair_y_def] Definition
+
+ ⊢ ∀t t0. (pair_t t t0).pair_y = t0
+
+ [recordtype_pair_t_seldef_pair_y_fupd_def] Definition
+
+ ⊢ ∀f t t0. pair_t t t0 with pair_y updated_by f = pair_t t (f t0)
+
+ [recordtype_struct_with_pair_t_seldef_struct_with_pair_p_def] Definition
+
+ ⊢ ∀p. (struct_with_pair_t p).struct_with_pair_p = p
+
+ [recordtype_struct_with_pair_t_seldef_struct_with_pair_p_fupd_def] Definition
+
+ ⊢ ∀f p.
+ struct_with_pair_t p with struct_with_pair_p updated_by f =
+ struct_with_pair_t (f p)
+
+ [recordtype_struct_with_tuple_t_seldef_struct_with_tuple_p_def] Definition
+
+ ⊢ ∀p. (struct_with_tuple_t p).struct_with_tuple_p = p
+
+ [recordtype_struct_with_tuple_t_seldef_struct_with_tuple_p_fupd_def] Definition
+
+ ⊢ ∀f p.
+ struct_with_tuple_t p with struct_with_tuple_p updated_by f =
+ struct_with_tuple_t (f p)
+
+ [refs_test1_fwd_def] Definition
+
+ ⊢ refs_test1_fwd =
+ if int_to_i32 1 ≠ int_to_i32 1 then Fail Failure else Return ()
+
+ [refs_test2_fwd_def] Definition
+
+ ⊢ refs_test2_fwd =
+ if int_to_i32 2 ≠ int_to_i32 2 then Fail Failure
+ else if int_to_i32 0 ≠ int_to_i32 0 then Fail Failure
+ else if int_to_i32 2 ≠ int_to_i32 2 then Fail Failure
+ else if int_to_i32 2 ≠ int_to_i32 2 then Fail Failure
+ else Return ()
+
+ [rem_test_fwd_def] Definition
+
+ ⊢ ∀x y. rem_test_fwd x y = u32_rem x y
+
+ [split_list_fwd_def] Definition
+
+ ⊢ ∀l. split_list_fwd l =
+ case l of
+ ListCons hd tl => Return (hd,tl)
+ | ListNil => Fail Failure
+
+ [struct_with_pair_t_TY_DEF] Definition
+
+ ⊢ ∃rep.
+ TYPE_DEFINITION
+ (λa0.
+ ∀ $var$('struct_with_pair_t').
+ (∀a0.
+ (∃a. a0 =
+ (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
+ a) ⇒
+ $var$('struct_with_pair_t') a0) ⇒
+ $var$('struct_with_pair_t') a0) rep
+
+ [struct_with_pair_t_case_def] Definition
+
+ ⊢ ∀a f. struct_with_pair_t_CASE (struct_with_pair_t a) f = f a
+
+ [struct_with_pair_t_size_def] Definition
+
+ ⊢ ∀f f1 a.
+ struct_with_pair_t_size f f1 (struct_with_pair_t a) =
+ 1 + pair_t_size f f1 a
+
+ [struct_with_tuple_t_TY_DEF] Definition
+
+ ⊢ ∃rep.
+ TYPE_DEFINITION
+ (λa0.
+ ∀ $var$('struct_with_tuple_t').
+ (∀a0.
+ (∃a. a0 =
+ (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
+ a) ⇒
+ $var$('struct_with_tuple_t') a0) ⇒
+ $var$('struct_with_tuple_t') a0) rep
+
+ [struct_with_tuple_t_case_def] Definition
+
+ ⊢ ∀a f. struct_with_tuple_t_CASE (struct_with_tuple_t a) f = f a
+
+ [struct_with_tuple_t_size_def] Definition
+
+ ⊢ ∀f f1 a.
+ struct_with_tuple_t_size f f1 (struct_with_tuple_t a) =
+ 1 + pair_size f f1 a
+
+ [subs_test_fwd_def] Definition
+
+ ⊢ ∀x y. subs_test_fwd x y = u32_sub x y
+
+ [sum_t_TY_DEF] Definition
+
+ ⊢ ∃rep.
+ TYPE_DEFINITION
+ (λa0.
+ ∀ $var$('sum_t').
+ (∀a0.
+ (∃a. a0 =
+ (λa.
+ ind_type$CONSTR 0 (a,ARB)
+ (λn. ind_type$BOTTOM)) a) ∨
+ (∃a. a0 =
+ (λa.
+ ind_type$CONSTR (SUC 0) (ARB,a)
+ (λn. ind_type$BOTTOM)) a) ⇒
+ $var$('sum_t') a0) ⇒
+ $var$('sum_t') a0) rep
+
+ [sum_t_case_def] Definition
+
+ ⊢ (∀a f f1. sum_t_CASE (SumLeft a) f f1 = f a) ∧
+ ∀a f f1. sum_t_CASE (SumRight a) f f1 = f1 a
+
+ [sum_t_size_def] Definition
+
+ ⊢ (∀f f1 a. sum_t_size f f1 (SumLeft a) = 1 + f a) ∧
+ ∀f f1 a. sum_t_size f f1 (SumRight a) = 1 + f1 a
+
+ [test2_fwd_def] Definition
+
+ ⊢ test2_fwd =
+ monad_ignore_bind (u32_add (int_to_u32 23) (int_to_u32 44))
+ (Return ())
+
+ [test3_fwd_def] Definition
+
+ ⊢ test3_fwd =
+ do
+ x <- get_max_fwd (int_to_u32 4) (int_to_u32 3);
+ y <- get_max_fwd (int_to_u32 10) (int_to_u32 11);
+ z <- u32_add x y;
+ if z ≠ int_to_u32 15 then Fail Failure else Return ()
+ od
+
+ [test_box1_fwd_def] Definition
+
+ ⊢ test_box1_fwd =
+ (let
+ b = int_to_i32 1;
+ x = b
+ in
+ if x ≠ int_to_i32 1 then Fail Failure else Return ())
+
+ [test_char_fwd_def] Definition
+
+ ⊢ test_char_fwd = Return #"a"
+
+ [test_constants_fwd_def] Definition
+
+ ⊢ test_constants_fwd =
+ do
+ swt <- new_tuple1_fwd;
+ (i,_) <<- swt.struct_with_tuple_p;
+ if i ≠ int_to_u32 1 then Fail Failure
+ else
+ do
+ swt0 <- new_tuple2_fwd;
+ (i0,_) <<- swt0.struct_with_tuple_p;
+ if i0 ≠ int_to_i16 1 then Fail Failure
+ else
+ do
+ swt1 <- new_tuple3_fwd;
+ (i1,_) <<- swt1.struct_with_tuple_p;
+ if i1 ≠ int_to_u64 1 then Fail Failure
+ else
+ do
+ swp <- new_pair1_fwd;
+ if swp.struct_with_pair_p.pair_x ≠ int_to_u32 1 then
+ Fail Failure
+ else Return ()
+ od
+ od
+ od
+ od
+
+ [test_copy_int_fwd_def] Definition
+
+ ⊢ test_copy_int_fwd =
+ do
+ y <- copy_int_fwd (int_to_i32 0);
+ if int_to_i32 0 ≠ y then Fail Failure else Return ()
+ od
+
+ [test_is_cons_fwd_def] Definition
+
+ ⊢ test_is_cons_fwd =
+ (let
+ l = ListNil
+ in
+ do
+ b <- is_cons_fwd (ListCons (int_to_i32 0) l);
+ if ¬b then Fail Failure else Return ()
+ od)
+
+ [test_list1_fwd_def] Definition
+
+ ⊢ test_list1_fwd = Return ()
+
+ [test_list_functions_fwd_def] Definition
+
+ ⊢ test_list_functions_fwd =
+ (let
+ l = ListNil;
+ l0 = ListCons (int_to_i32 2) l;
+ l1 = ListCons (int_to_i32 1) l0
+ in
+ do
+ i <- list_length_fwd (ListCons (int_to_i32 0) l1);
+ if i ≠ int_to_u32 3 then Fail Failure
+ else
+ do
+ i0 <-
+ list_nth_shared_fwd (ListCons (int_to_i32 0) l1)
+ (int_to_u32 0);
+ if i0 ≠ int_to_i32 0 then Fail Failure
+ else
+ do
+ i1 <-
+ list_nth_shared_fwd (ListCons (int_to_i32 0) l1)
+ (int_to_u32 1);
+ if i1 ≠ int_to_i32 1 then Fail Failure
+ else
+ do
+ i2 <-
+ list_nth_shared_fwd (ListCons (int_to_i32 0) l1)
+ (int_to_u32 2);
+ if i2 ≠ int_to_i32 2 then Fail Failure
+ else
+ do
+ ls <-
+ list_nth_mut_back
+ (ListCons (int_to_i32 0) l1)
+ (int_to_u32 1) (int_to_i32 3);
+ i3 <- list_nth_shared_fwd ls (int_to_u32 0);
+ if i3 ≠ int_to_i32 0 then Fail Failure
+ else
+ do
+ i4 <-
+ list_nth_shared_fwd ls (int_to_u32 1);
+ if i4 ≠ int_to_i32 3 then Fail Failure
+ else
+ do
+ i5 <-
+ list_nth_shared_fwd ls
+ (int_to_u32 2);
+ if i5 ≠ int_to_i32 2 then Fail Failure
+ else Return ()
+ od
+ od
+ od
+ od
+ od
+ od
+ od)
+
+ [test_mem_replace_fwd_back_def] Definition
+
+ ⊢ ∀px.
+ test_mem_replace_fwd_back px =
+ (let
+ y = mem_replace_fwd px (int_to_u32 1)
+ in
+ if y ≠ int_to_u32 0 then Fail Failure
+ else Return (int_to_u32 2))
+
+ [test_neg1_fwd_def] Definition
+
+ ⊢ test_neg1_fwd =
+ do
+ y <- i32_neg (int_to_i32 3);
+ if y ≠ int_to_i32 (-3) then Fail Failure else Return ()
+ od
+
+ [test_panic_fwd_def] Definition
+
+ ⊢ ∀b. test_panic_fwd b = if b then Fail Failure else Return ()
+
+ [test_shared_borrow_bool1_fwd_def] Definition
+
+ ⊢ ∀b. test_shared_borrow_bool1_fwd b =
+ if b then Return (int_to_u32 0) else Return (int_to_u32 1)
+
+ [test_shared_borrow_bool2_fwd_def] Definition
+
+ ⊢ test_shared_borrow_bool2_fwd = Return (int_to_u32 0)
+
+ [test_shared_borrow_enum1_fwd_def] Definition
+
+ ⊢ ∀l. test_shared_borrow_enum1_fwd l =
+ case l of
+ ListCons i l0 => Return (int_to_u32 1)
+ | ListNil => Return (int_to_u32 0)
+
+ [test_shared_borrow_enum2_fwd_def] Definition
+
+ ⊢ test_shared_borrow_enum2_fwd = Return (int_to_u32 0)
+
+ [test_split_list_fwd_def] Definition
+
+ ⊢ test_split_list_fwd =
+ (let
+ l = ListNil
+ in
+ do
+ p <- split_list_fwd (ListCons (int_to_i32 0) l);
+ (hd,_) <<- p;
+ if hd ≠ int_to_i32 0 then Fail Failure else Return ()
+ od)
+
+ [test_unreachable_fwd_def] Definition
+
+ ⊢ ∀b. test_unreachable_fwd b = if b then Fail Failure else Return ()
+
+ [test_weird_borrows1_fwd_def] Definition
+
+ ⊢ test_weird_borrows1_fwd = Return ()
+
+ [tree_t_TY_DEF] Definition
+
+ ⊢ ∃rep.
+ TYPE_DEFINITION
+ (λa1'.
+ ∀ $var$('node_elem_t') $var$('tree_t').
+ (∀a0'.
+ (∃a0 a1.
+ a0' =
+ (λa0 a1.
+ ind_type$CONSTR 0 ARB
+ (ind_type$FCONS a0
+ (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
+ a0 a1 ∧ $var$('tree_t') a0 ∧
+ $var$('node_elem_t') a1) ∨
+ a0' =
+ ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
+ $var$('node_elem_t') a0') ∧
+ (∀a1'.
+ (∃a. a1' =
+ (λa.
+ ind_type$CONSTR (SUC (SUC 0)) a
+ (λn. ind_type$BOTTOM)) a) ∨
+ (∃a0 a1 a2.
+ a1' =
+ (λa0 a1 a2.
+ ind_type$CONSTR (SUC (SUC (SUC 0))) a0
+ (ind_type$FCONS a1
+ (ind_type$FCONS a2 (λn. ind_type$BOTTOM))))
+ a0 a1 a2 ∧ $var$('node_elem_t') a1 ∧
+ $var$('tree_t') a2) ⇒
+ $var$('tree_t') a1') ⇒
+ $var$('tree_t') a1') rep
+
+ [tree_t_case_def] Definition
+
+ ⊢ (∀a f f1. tree_t_CASE (TreeLeaf a) f f1 = f a) ∧
+ ∀a0 a1 a2 f f1. tree_t_CASE (TreeNode a0 a1 a2) f f1 = f1 a0 a1 a2
+
+ [EXISTS_pair_t] Theorem
+
+ ⊢ ∀P. (∃p. P p) ⇔ ∃t0 t. P <|pair_x := t0; pair_y := t|>
+
+ [EXISTS_struct_with_pair_t] Theorem
+
+ ⊢ ∀P. (∃s. P s) ⇔ ∃p. P <|struct_with_pair_p := p|>
+
+ [EXISTS_struct_with_tuple_t] Theorem
+
+ ⊢ ∀P. (∃s. P s) ⇔ ∃p. P <|struct_with_tuple_p := p|>
+
+ [FORALL_pair_t] Theorem
+
+ ⊢ ∀P. (∀p. P p) ⇔ ∀t0 t. P <|pair_x := t0; pair_y := t|>
+
+ [FORALL_struct_with_pair_t] Theorem
+
+ ⊢ ∀P. (∀s. P s) ⇔ ∀p. P <|struct_with_pair_p := p|>
+
+ [FORALL_struct_with_tuple_t] Theorem
+
+ ⊢ ∀P. (∀s. P s) ⇔ ∀p. P <|struct_with_tuple_p := p|>
+
+ [datatype_empty_enum_t] Theorem
+
+ ⊢ DATATYPE (empty_enum_t EmptyEnumEmpty)
+
+ [datatype_enum_t] Theorem
+
+ ⊢ DATATYPE (enum_t EnumVariant1 EnumVariant2)
+
+ [datatype_list_t] Theorem
+
+ ⊢ DATATYPE (list_t ListCons ListNil)
+
+ [datatype_node_elem_t] Theorem
+
+ ⊢ DATATYPE
+ (node_elem_t NodeElemCons NodeElemNil ∧ tree_t TreeLeaf TreeNode)
+
+ [datatype_one_t] Theorem
+
+ ⊢ DATATYPE (one_t OneOne)
+
+ [datatype_pair_t] Theorem
+
+ ⊢ DATATYPE (record pair_t pair_x pair_y)
+
+ [datatype_struct_with_pair_t] Theorem
+
+ ⊢ DATATYPE (record struct_with_pair_t struct_with_pair_p)
+
+ [datatype_struct_with_tuple_t] Theorem
+
+ ⊢ DATATYPE (record struct_with_tuple_t struct_with_tuple_p)
+
+ [datatype_sum_t] Theorem
+
+ ⊢ DATATYPE (sum_t SumLeft SumRight)
+
+ [empty_enum_t2num_11] Theorem
+
+ ⊢ ∀a a'. empty_enum_t2num a = empty_enum_t2num a' ⇔ a = a'
+
+ [empty_enum_t2num_ONTO] Theorem
+
+ ⊢ ∀r. r < 1 ⇔ ∃a. r = empty_enum_t2num a
+
+ [empty_enum_t2num_num2empty_enum_t] Theorem
+
+ ⊢ ∀r. r < 1 ⇔ empty_enum_t2num (num2empty_enum_t r) = r
+
+ [empty_enum_t2num_thm] Theorem
+
+ ⊢ empty_enum_t2num EmptyEnumEmpty = 0
+
+ [empty_enum_t_Axiom] Theorem
+
+ ⊢ ∀x0. ∃f. f EmptyEnumEmpty = x0
+
+ [empty_enum_t_EQ_empty_enum_t] Theorem
+
+ ⊢ ∀a a'. a = a' ⇔ empty_enum_t2num a = empty_enum_t2num a'
+
+ [empty_enum_t_case_cong] Theorem
+
+ ⊢ ∀M M' v0.
+ M = M' ∧ (M' = EmptyEnumEmpty ⇒ v0 = v0') ⇒
+ (case M of EmptyEnumEmpty => v0) =
+ case M' of EmptyEnumEmpty => v0'
+
+ [empty_enum_t_case_def] Theorem
+
+ ⊢ ∀v0. (case EmptyEnumEmpty of EmptyEnumEmpty => v0) = v0
+
+ [empty_enum_t_case_eq] Theorem
+
+ ⊢ (case x of EmptyEnumEmpty => v0) = v ⇔ x = EmptyEnumEmpty ∧ v0 = v
+
+ [empty_enum_t_induction] Theorem
+
+ ⊢ ∀P. P EmptyEnumEmpty ⇒ ∀a. P a
+
+ [empty_enum_t_nchotomy] Theorem
+
+ ⊢ ∀a. a = EmptyEnumEmpty
+
+ [enum_t2num_11] Theorem
+
+ ⊢ ∀a a'. enum_t2num a = enum_t2num a' ⇔ a = a'
+
+ [enum_t2num_ONTO] Theorem
+
+ ⊢ ∀r. r < 2 ⇔ ∃a. r = enum_t2num a
+
+ [enum_t2num_num2enum_t] Theorem
+
+ ⊢ ∀r. r < 2 ⇔ enum_t2num (num2enum_t r) = r
+
+ [enum_t2num_thm] Theorem
+
+ ⊢ enum_t2num EnumVariant1 = 0 ∧ enum_t2num EnumVariant2 = 1
+
+ [enum_t_Axiom] Theorem
+
+ ⊢ ∀x0 x1. ∃f. f EnumVariant1 = x0 ∧ f EnumVariant2 = x1
+
+ [enum_t_EQ_enum_t] Theorem
+
+ ⊢ ∀a a'. a = a' ⇔ enum_t2num a = enum_t2num a'
+
+ [enum_t_case_cong] Theorem
+
+ ⊢ ∀M M' v0 v1.
+ M = M' ∧ (M' = EnumVariant1 ⇒ v0 = v0') ∧
+ (M' = EnumVariant2 ⇒ v1 = v1') ⇒
+ (case M of EnumVariant1 => v0 | EnumVariant2 => v1) =
+ case M' of EnumVariant1 => v0' | EnumVariant2 => v1'
+
+ [enum_t_case_def] Theorem
+
+ ⊢ (∀v0 v1.
+ (case EnumVariant1 of EnumVariant1 => v0 | EnumVariant2 => v1) =
+ v0) ∧
+ ∀v0 v1.
+ (case EnumVariant2 of EnumVariant1 => v0 | EnumVariant2 => v1) =
+ v1
+
+ [enum_t_case_eq] Theorem
+
+ ⊢ (case x of EnumVariant1 => v0 | EnumVariant2 => v1) = v ⇔
+ x = EnumVariant1 ∧ v0 = v ∨ x = EnumVariant2 ∧ v1 = v
+
+ [enum_t_distinct] Theorem
+
+ ⊢ EnumVariant1 ≠ EnumVariant2
+
+ [enum_t_induction] Theorem
+
+ ⊢ ∀P. P EnumVariant1 ∧ P EnumVariant2 ⇒ ∀a. P a
+
+ [enum_t_nchotomy] Theorem
+
+ ⊢ ∀a. a = EnumVariant1 ∨ a = EnumVariant2
+
+ [list_t_11] Theorem
+
+ ⊢ ∀a0 a1 a0' a1'.
+ ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
+
+ [list_t_Axiom] Theorem
+
+ ⊢ ∀f0 f1. ∃fn.
+ (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
+ fn ListNil = f1
+
+ [list_t_case_cong] Theorem
+
+ ⊢ ∀M M' f v.
+ M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
+ (M' = ListNil ⇒ v = v') ⇒
+ list_t_CASE M f v = list_t_CASE M' f' v'
+
+ [list_t_case_eq] Theorem
+
+ ⊢ list_t_CASE x f v = v' ⇔
+ (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
+
+ [list_t_distinct] Theorem
+
+ ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
+
+ [list_t_induction] Theorem
+
+ ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
+
+ [list_t_nchotomy] Theorem
+
+ ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
+
+ [node_elem_t_11] Theorem
+
+ ⊢ ∀a0 a1 a0' a1'.
+ NodeElemCons a0 a1 = NodeElemCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
+
+ [node_elem_t_Axiom] Theorem
+
+ ⊢ ∀f0 f1 f2 f3. ∃fn0 fn1.
+ (∀a0 a1. fn0 (NodeElemCons a0 a1) = f0 a0 a1 (fn1 a0) (fn0 a1)) ∧
+ fn0 NodeElemNil = f1 ∧ (∀a. fn1 (TreeLeaf a) = f2 a) ∧
+ ∀a0 a1 a2.
+ fn1 (TreeNode a0 a1 a2) = f3 a0 a1 a2 (fn0 a1) (fn1 a2)
+
+ [node_elem_t_case_cong] Theorem
+
+ ⊢ ∀M M' f v.
+ M = M' ∧ (∀a0 a1. M' = NodeElemCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
+ (M' = NodeElemNil ⇒ v = v') ⇒
+ node_elem_t_CASE M f v = node_elem_t_CASE M' f' v'
+
+ [node_elem_t_case_eq] Theorem
+
+ ⊢ node_elem_t_CASE x f v = v' ⇔
+ (∃t n. x = NodeElemCons t n ∧ f t n = v') ∨
+ x = NodeElemNil ∧ v = v'
+
+ [node_elem_t_distinct] Theorem
+
+ ⊢ ∀a1 a0. NodeElemCons a0 a1 ≠ NodeElemNil
+
+ [node_elem_t_induction] Theorem
+
+ ⊢ ∀P0 P1.
+ (∀t n. P1 t ∧ P0 n ⇒ P0 (NodeElemCons t n)) ∧ P0 NodeElemNil ∧
+ (∀t. P1 (TreeLeaf t)) ∧
+ (∀n t. P0 n ∧ P1 t ⇒ ∀t0. P1 (TreeNode t0 n t)) ⇒
+ (∀n. P0 n) ∧ ∀t. P1 t
+
+ [node_elem_t_nchotomy] Theorem
+
+ ⊢ ∀nn. (∃t n. nn = NodeElemCons t n) ∨ nn = NodeElemNil
+
+ [num2empty_enum_t_11] Theorem
+
+ ⊢ ∀r r'.
+ r < 1 ⇒
+ r' < 1 ⇒
+ (num2empty_enum_t r = num2empty_enum_t r' ⇔ r = r')
+
+ [num2empty_enum_t_ONTO] Theorem
+
+ ⊢ ∀a. ∃r. a = num2empty_enum_t r ∧ r < 1
+
+ [num2empty_enum_t_empty_enum_t2num] Theorem
+
+ ⊢ ∀a. num2empty_enum_t (empty_enum_t2num a) = a
+
+ [num2empty_enum_t_thm] Theorem
+
+ ⊢ num2empty_enum_t 0 = EmptyEnumEmpty
+
+ [num2enum_t_11] Theorem
+
+ ⊢ ∀r r'. r < 2 ⇒ r' < 2 ⇒ (num2enum_t r = num2enum_t r' ⇔ r = r')
+
+ [num2enum_t_ONTO] Theorem
+
+ ⊢ ∀a. ∃r. a = num2enum_t r ∧ r < 2
+
+ [num2enum_t_enum_t2num] Theorem
+
+ ⊢ ∀a. num2enum_t (enum_t2num a) = a
+
+ [num2enum_t_thm] Theorem
+
+ ⊢ num2enum_t 0 = EnumVariant1 ∧ num2enum_t 1 = EnumVariant2
+
+ [one_t_11] Theorem
+
+ ⊢ ∀a a'. OneOne a = OneOne a' ⇔ a = a'
+
+ [one_t_Axiom] Theorem
+
+ ⊢ ∀f. ∃fn. ∀a. fn (OneOne a) = f a
+
+ [one_t_case_cong] Theorem
+
+ ⊢ ∀M M' f.
+ M = M' ∧ (∀a. M' = OneOne a ⇒ f a = f' a) ⇒
+ one_t_CASE M f = one_t_CASE M' f'
+
+ [one_t_case_eq] Theorem
+
+ ⊢ one_t_CASE x f = v ⇔ ∃t. x = OneOne t ∧ f t = v
+
+ [one_t_induction] Theorem
+
+ ⊢ ∀P. (∀t. P (OneOne t)) ⇒ ∀ $o. P $o
+
+ [one_t_nchotomy] Theorem
+
+ ⊢ ∀oo. ∃t. oo = OneOne t
+
+ [pair_t_11] Theorem
+
+ ⊢ ∀a0 a1 a0' a1'. pair_t a0 a1 = pair_t a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
+
+ [pair_t_Axiom] Theorem
+
+ ⊢ ∀f. ∃fn. ∀a0 a1. fn (pair_t a0 a1) = f a0 a1
+
+ [pair_t_accessors] Theorem
+
+ ⊢ (∀t t0. (pair_t t t0).pair_x = t) ∧
+ ∀t t0. (pair_t t t0).pair_y = t0
+
+ [pair_t_accfupds] Theorem
+
+ ⊢ (∀p f. (p with pair_y updated_by f).pair_x = p.pair_x) ∧
+ (∀p f. (p with pair_x updated_by f).pair_y = p.pair_y) ∧
+ (∀p f. (p with pair_x updated_by f).pair_x = f p.pair_x) ∧
+ ∀p f. (p with pair_y updated_by f).pair_y = f p.pair_y
+
+ [pair_t_case_cong] Theorem
+
+ ⊢ ∀M M' f.
+ M = M' ∧ (∀a0 a1. M' = pair_t a0 a1 ⇒ f a0 a1 = f' a0 a1) ⇒
+ pair_t_CASE M f = pair_t_CASE M' f'
+
+ [pair_t_case_eq] Theorem
+
+ ⊢ pair_t_CASE x f = v ⇔ ∃t t0. x = pair_t t t0 ∧ f t t0 = v
+
+ [pair_t_component_equality] Theorem
+
+ ⊢ ∀p1 p2. p1 = p2 ⇔ p1.pair_x = p2.pair_x ∧ p1.pair_y = p2.pair_y
+
+ [pair_t_fn_updates] Theorem
+
+ ⊢ (∀f t t0. pair_t t t0 with pair_x updated_by f = pair_t (f t) t0) ∧
+ ∀f t t0. pair_t t t0 with pair_y updated_by f = pair_t t (f t0)
+
+ [pair_t_fupdcanon] Theorem
+
+ ⊢ ∀p g f.
+ p with <|pair_y updated_by f; pair_x updated_by g|> =
+ p with <|pair_x updated_by g; pair_y updated_by f|>
+
+ [pair_t_fupdcanon_comp] Theorem
+
+ ⊢ (∀g f.
+ pair_y_fupd f ∘ pair_x_fupd g = pair_x_fupd g ∘ pair_y_fupd f) ∧
+ ∀h g f.
+ pair_y_fupd f ∘ pair_x_fupd g ∘ h =
+ pair_x_fupd g ∘ pair_y_fupd f ∘ h
+
+ [pair_t_fupdfupds] Theorem
+
+ ⊢ (∀p g f.
+ p with <|pair_x updated_by f; pair_x updated_by g|> =
+ p with pair_x updated_by f ∘ g) ∧
+ ∀p g f.
+ p with <|pair_y updated_by f; pair_y updated_by g|> =
+ p with pair_y updated_by f ∘ g
+
+ [pair_t_fupdfupds_comp] Theorem
+
+ ⊢ ((∀g f. pair_x_fupd f ∘ pair_x_fupd g = pair_x_fupd (f ∘ g)) ∧
+ ∀h g f.
+ pair_x_fupd f ∘ pair_x_fupd g ∘ h = pair_x_fupd (f ∘ g) ∘ h) ∧
+ (∀g f. pair_y_fupd f ∘ pair_y_fupd g = pair_y_fupd (f ∘ g)) ∧
+ ∀h g f. pair_y_fupd f ∘ pair_y_fupd g ∘ h = pair_y_fupd (f ∘ g) ∘ h
+
+ [pair_t_induction] Theorem
+
+ ⊢ ∀P. (∀t t0. P (pair_t t t0)) ⇒ ∀p. P p
+
+ [pair_t_literal_11] Theorem
+
+ ⊢ ∀t01 t1 t02 t2.
+ <|pair_x := t01; pair_y := t1|> = <|pair_x := t02; pair_y := t2|> ⇔
+ t01 = t02 ∧ t1 = t2
+
+ [pair_t_literal_nchotomy] Theorem
+
+ ⊢ ∀p. ∃t0 t. p = <|pair_x := t0; pair_y := t|>
+
+ [pair_t_nchotomy] Theorem
+
+ ⊢ ∀pp. ∃t t0. pp = pair_t t t0
+
+ [pair_t_updates_eq_literal] Theorem
+
+ ⊢ ∀p t0 t.
+ p with <|pair_x := t0; pair_y := t|> =
+ <|pair_x := t0; pair_y := t|>
+
+ [struct_with_pair_t_11] Theorem
+
+ ⊢ ∀a a'. struct_with_pair_t a = struct_with_pair_t a' ⇔ a = a'
+
+ [struct_with_pair_t_Axiom] Theorem
+
+ ⊢ ∀f. ∃fn. ∀a. fn (struct_with_pair_t a) = f a
+
+ [struct_with_pair_t_accessors] Theorem
+
+ ⊢ ∀p. (struct_with_pair_t p).struct_with_pair_p = p
+
+ [struct_with_pair_t_accfupds] Theorem
+
+ ⊢ ∀s f.
+ (s with struct_with_pair_p updated_by f).struct_with_pair_p =
+ f s.struct_with_pair_p
+
+ [struct_with_pair_t_case_cong] Theorem
+
+ ⊢ ∀M M' f.
+ M = M' ∧ (∀a. M' = struct_with_pair_t a ⇒ f a = f' a) ⇒
+ struct_with_pair_t_CASE M f = struct_with_pair_t_CASE M' f'
+
+ [struct_with_pair_t_case_eq] Theorem
+
+ ⊢ struct_with_pair_t_CASE x f = v ⇔
+ ∃p. x = struct_with_pair_t p ∧ f p = v
+
+ [struct_with_pair_t_component_equality] Theorem
+
+ ⊢ ∀s1 s2. s1 = s2 ⇔ s1.struct_with_pair_p = s2.struct_with_pair_p
+
+ [struct_with_pair_t_fn_updates] Theorem
+
+ ⊢ ∀f p.
+ struct_with_pair_t p with struct_with_pair_p updated_by f =
+ struct_with_pair_t (f p)
+
+ [struct_with_pair_t_fupdfupds] Theorem
+
+ ⊢ ∀s g f.
+ s with
+ <|struct_with_pair_p updated_by f;
+ struct_with_pair_p updated_by g|> =
+ s with struct_with_pair_p updated_by f ∘ g
+
+ [struct_with_pair_t_fupdfupds_comp] Theorem
+
+ ⊢ (∀g f.
+ struct_with_pair_p_fupd f ∘ struct_with_pair_p_fupd g =
+ struct_with_pair_p_fupd (f ∘ g)) ∧
+ ∀h g f.
+ struct_with_pair_p_fupd f ∘ struct_with_pair_p_fupd g ∘ h =
+ struct_with_pair_p_fupd (f ∘ g) ∘ h
+
+ [struct_with_pair_t_induction] Theorem
+
+ ⊢ ∀P. (∀p. P (struct_with_pair_t p)) ⇒ ∀s. P s
+
+ [struct_with_pair_t_literal_11] Theorem
+
+ ⊢ ∀p1 p2.
+ <|struct_with_pair_p := p1|> = <|struct_with_pair_p := p2|> ⇔
+ p1 = p2
+
+ [struct_with_pair_t_literal_nchotomy] Theorem
+
+ ⊢ ∀s. ∃p. s = <|struct_with_pair_p := p|>
+
+ [struct_with_pair_t_nchotomy] Theorem
+
+ ⊢ ∀ss. ∃p. ss = struct_with_pair_t p
+
+ [struct_with_pair_t_updates_eq_literal] Theorem
+
+ ⊢ ∀s p. s with struct_with_pair_p := p = <|struct_with_pair_p := p|>
+
+ [struct_with_tuple_t_11] Theorem
+
+ ⊢ ∀a a'. struct_with_tuple_t a = struct_with_tuple_t a' ⇔ a = a'
+
+ [struct_with_tuple_t_Axiom] Theorem
+
+ ⊢ ∀f. ∃fn. ∀a. fn (struct_with_tuple_t a) = f a
+
+ [struct_with_tuple_t_accessors] Theorem
+
+ ⊢ ∀p. (struct_with_tuple_t p).struct_with_tuple_p = p
+
+ [struct_with_tuple_t_accfupds] Theorem
+
+ ⊢ ∀s f.
+ (s with struct_with_tuple_p updated_by f).struct_with_tuple_p =
+ f s.struct_with_tuple_p
+
+ [struct_with_tuple_t_case_cong] Theorem
+
+ ⊢ ∀M M' f.
+ M = M' ∧ (∀a. M' = struct_with_tuple_t a ⇒ f a = f' a) ⇒
+ struct_with_tuple_t_CASE M f = struct_with_tuple_t_CASE M' f'
+
+ [struct_with_tuple_t_case_eq] Theorem
+
+ ⊢ struct_with_tuple_t_CASE x f = v ⇔
+ ∃p. x = struct_with_tuple_t p ∧ f p = v
+
+ [struct_with_tuple_t_component_equality] Theorem
+
+ ⊢ ∀s1 s2. s1 = s2 ⇔ s1.struct_with_tuple_p = s2.struct_with_tuple_p
+
+ [struct_with_tuple_t_fn_updates] Theorem
+
+ ⊢ ∀f p.
+ struct_with_tuple_t p with struct_with_tuple_p updated_by f =
+ struct_with_tuple_t (f p)
+
+ [struct_with_tuple_t_fupdfupds] Theorem
+
+ ⊢ ∀s g f.
+ s with
+ <|struct_with_tuple_p updated_by f;
+ struct_with_tuple_p updated_by g|> =
+ s with struct_with_tuple_p updated_by f ∘ g
+
+ [struct_with_tuple_t_fupdfupds_comp] Theorem
+
+ ⊢ (∀g f.
+ struct_with_tuple_p_fupd f ∘ struct_with_tuple_p_fupd g =
+ struct_with_tuple_p_fupd (f ∘ g)) ∧
+ ∀h g f.
+ struct_with_tuple_p_fupd f ∘ struct_with_tuple_p_fupd g ∘ h =
+ struct_with_tuple_p_fupd (f ∘ g) ∘ h
+
+ [struct_with_tuple_t_induction] Theorem
+
+ ⊢ ∀P. (∀p. P (struct_with_tuple_t p)) ⇒ ∀s. P s
+
+ [struct_with_tuple_t_literal_11] Theorem
+
+ ⊢ ∀p1 p2.
+ <|struct_with_tuple_p := p1|> = <|struct_with_tuple_p := p2|> ⇔
+ p1 = p2
+
+ [struct_with_tuple_t_literal_nchotomy] Theorem
+
+ ⊢ ∀s. ∃p. s = <|struct_with_tuple_p := p|>
+
+ [struct_with_tuple_t_nchotomy] Theorem
+
+ ⊢ ∀ss. ∃p. ss = struct_with_tuple_t p
+
+ [struct_with_tuple_t_updates_eq_literal] Theorem
+
+ ⊢ ∀s p.
+ s with struct_with_tuple_p := p = <|struct_with_tuple_p := p|>
+
+ [sum_t_11] Theorem
+
+ ⊢ (∀a a'. SumLeft a = SumLeft a' ⇔ a = a') ∧
+ ∀a a'. SumRight a = SumRight a' ⇔ a = a'
+
+ [sum_t_Axiom] Theorem
+
+ ⊢ ∀f0 f1. ∃fn.
+ (∀a. fn (SumLeft a) = f0 a) ∧ ∀a. fn (SumRight a) = f1 a
+
+ [sum_t_case_cong] Theorem
+
+ ⊢ ∀M M' f f1.
+ M = M' ∧ (∀a. M' = SumLeft a ⇒ f a = f' a) ∧
+ (∀a. M' = SumRight a ⇒ f1 a = f1' a) ⇒
+ sum_t_CASE M f f1 = sum_t_CASE M' f' f1'
+
+ [sum_t_case_eq] Theorem
+
+ ⊢ sum_t_CASE x f f1 = v ⇔
+ (∃t. x = SumLeft t ∧ f t = v) ∨ ∃t. x = SumRight t ∧ f1 t = v
+
+ [sum_t_distinct] Theorem
+
+ ⊢ ∀a' a. SumLeft a ≠ SumRight a'
+
+ [sum_t_induction] Theorem
+
+ ⊢ ∀P. (∀t. P (SumLeft t)) ∧ (∀t. P (SumRight t)) ⇒ ∀s. P s
+
+ [sum_t_nchotomy] Theorem
+
+ ⊢ ∀ss. (∃t. ss = SumLeft t) ∨ ∃t. ss = SumRight t
+
+ [tree_t_11] Theorem
+
+ ⊢ (∀a a'. TreeLeaf a = TreeLeaf a' ⇔ a = a') ∧
+ ∀a0 a1 a2 a0' a1' a2'.
+ TreeNode a0 a1 a2 = TreeNode a0' a1' a2' ⇔
+ a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
+
+ [tree_t_Axiom] Theorem
+
+ ⊢ ∀f0 f1 f2 f3. ∃fn0 fn1.
+ (∀a0 a1. fn0 (NodeElemCons a0 a1) = f0 a0 a1 (fn1 a0) (fn0 a1)) ∧
+ fn0 NodeElemNil = f1 ∧ (∀a. fn1 (TreeLeaf a) = f2 a) ∧
+ ∀a0 a1 a2.
+ fn1 (TreeNode a0 a1 a2) = f3 a0 a1 a2 (fn0 a1) (fn1 a2)
+
+ [tree_t_case_cong] Theorem
+
+ ⊢ ∀M M' f f1.
+ M = M' ∧ (∀a. M' = TreeLeaf a ⇒ f a = f' a) ∧
+ (∀a0 a1 a2. M' = TreeNode a0 a1 a2 ⇒ f1 a0 a1 a2 = f1' a0 a1 a2) ⇒
+ tree_t_CASE M f f1 = tree_t_CASE M' f' f1'
+
+ [tree_t_case_eq] Theorem
+
+ ⊢ tree_t_CASE x f f1 = v ⇔
+ (∃t. x = TreeLeaf t ∧ f t = v) ∨
+ ∃t0 n t. x = TreeNode t0 n t ∧ f1 t0 n t = v
+
+ [tree_t_distinct] Theorem
+
+ ⊢ ∀a2 a1 a0 a. TreeLeaf a ≠ TreeNode a0 a1 a2
+
+ [tree_t_induction] Theorem
+
+ ⊢ ∀P0 P1.
+ (∀t n. P1 t ∧ P0 n ⇒ P0 (NodeElemCons t n)) ∧ P0 NodeElemNil ∧
+ (∀t. P1 (TreeLeaf t)) ∧
+ (∀n t. P0 n ∧ P1 t ⇒ ∀t0. P1 (TreeNode t0 n t)) ⇒
+ (∀n. P0 n) ∧ ∀t. P1 t
+
+ [tree_t_nchotomy] Theorem
+
+ ⊢ ∀tt. (∃t. tt = TreeLeaf t) ∨ ∃t0 n t. tt = TreeNode t0 n t
+
+
+*)
+end