diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/hol4/betree/Holmakefile | 5 | ||||
| -rw-r--r-- | tests/hol4/betree/betreeMain_FunsScript.sml | 1214 | ||||
| -rw-r--r-- | tests/hol4/betree/betreeMain_FunsTheory.sig | 1240 | ||||
| -rw-r--r-- | tests/hol4/betree/betreeMain_OpaqueScript.sml | 26 | ||||
| -rw-r--r-- | tests/hol4/betree/betreeMain_OpaqueTheory.sig | 11 | ||||
| -rw-r--r-- | tests/hol4/betree/betreeMain_TypesScript.sml | 76 | ||||
| -rw-r--r-- | tests/hol4/betree/betreeMain_TypesTheory.sig | 1751 |
7 files changed, 4323 insertions, 0 deletions
diff --git a/tests/hol4/betree/Holmakefile b/tests/hol4/betree/Holmakefile new file mode 100644 index 00000000..3c4b8973 --- /dev/null +++ b/tests/hol4/betree/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/betree/betreeMain_FunsScript.sml b/tests/hol4/betree/betreeMain_FunsScript.sml new file mode 100644 index 00000000..df0c6a24 --- /dev/null +++ b/tests/hol4/betree/betreeMain_FunsScript.sml @@ -0,0 +1,1214 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: function definitions *) +open primitivesLib divDefLib +open betreeMain_TypesTheory betreeMain_OpaqueTheory + +val _ = new_theory "betreeMain_Funs" + + +val betree_load_internal_node_fwd_def = Define ‘ + (** [betree_main::betree::load_internal_node] *) + betree_load_internal_node_fwd + (id : u64) (st : state) : + (state # (u64 # betree_message_t) betree_list_t) result + = + betree_utils_load_internal_node_fwd id st +’ + +val betree_store_internal_node_fwd_def = Define ‘ + (** [betree_main::betree::store_internal_node] *) + betree_store_internal_node_fwd + (id : u64) (content : (u64 # betree_message_t) betree_list_t) (st : state) + : + (state # unit) result + = + do + (st0, _) <- betree_utils_store_internal_node_fwd id content st; + Return (st0, ()) + od +’ + +val betree_load_leaf_node_fwd_def = Define ‘ + (** [betree_main::betree::load_leaf_node] *) + betree_load_leaf_node_fwd + (id : u64) (st : state) : (state # (u64 # u64) betree_list_t) result = + betree_utils_load_leaf_node_fwd id st +’ + +val betree_store_leaf_node_fwd_def = Define ‘ + (** [betree_main::betree::store_leaf_node] *) + betree_store_leaf_node_fwd + (id : u64) (content : (u64 # u64) betree_list_t) (st : state) : + (state # unit) result + = + do + (st0, _) <- betree_utils_store_leaf_node_fwd id content st; + Return (st0, ()) + od +’ + +val betree_fresh_node_id_fwd_def = Define ‘ + (** [betree_main::betree::fresh_node_id] *) + betree_fresh_node_id_fwd (counter : u64) : u64 result = + do + _ <- u64_add counter (int_to_u64 1); + Return counter + od +’ + +val betree_fresh_node_id_back_def = Define ‘ + (** [betree_main::betree::fresh_node_id] *) + betree_fresh_node_id_back (counter : u64) : u64 result = + u64_add counter (int_to_u64 1) +’ + +val betree_node_id_counter_new_fwd_def = Define ‘ + (** [betree_main::betree::NodeIdCounter::{0}::new] *) + betree_node_id_counter_new_fwd : betree_node_id_counter_t result = + Return (<| betree_node_id_counter_next_node_id := (int_to_u64 0) |>) +’ + +val betree_node_id_counter_fresh_id_fwd_def = Define ‘ + (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) + betree_node_id_counter_fresh_id_fwd + (self : betree_node_id_counter_t) : u64 result = + do + _ <- u64_add self.betree_node_id_counter_next_node_id (int_to_u64 1); + Return self.betree_node_id_counter_next_node_id + od +’ + +val betree_node_id_counter_fresh_id_back_def = Define ‘ + (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) + betree_node_id_counter_fresh_id_back + (self : betree_node_id_counter_t) : betree_node_id_counter_t result = + do + i <- u64_add self.betree_node_id_counter_next_node_id (int_to_u64 1); + Return (<| betree_node_id_counter_next_node_id := i |>) + od +’ + +(** [core::num::u64::{10}::MAX] *) +Definition core_num_u64_max_body_def: + core_num_u64_max_body : u64 result = Return (int_to_u64 18446744073709551615) +End +Definition core_num_u64_max_c_def: + core_num_u64_max_c : u64 = get_return_value core_num_u64_max_body +End + +val betree_upsert_update_fwd_def = Define ‘ + (** [betree_main::betree::upsert_update] *) + betree_upsert_update_fwd + (prev : u64 option) (st : betree_upsert_fun_state_t) : u64 result = + (case prev of + | NONE => + (case st of + | BetreeUpsertFunStateAdd v => Return v + | BetreeUpsertFunStateSub i => Return (int_to_u64 0)) + | SOME prev0 => + (case st of + | BetreeUpsertFunStateAdd v => + do + margin <- u64_sub core_num_u64_max_c prev0; + if u64_ge margin v then u64_add prev0 v else Return core_num_u64_max_c + od + | BetreeUpsertFunStateSub v => + if u64_ge prev0 v then u64_sub prev0 v else Return (int_to_u64 0))) +’ + +val [betree_list_len_fwd_def] = DefineDiv ‘ + (** [betree_main::betree::List::{1}::len] *) + betree_list_len_fwd (self : 't betree_list_t) : u64 result = + (case self of + | BetreeListCons t tl => + do + i <- betree_list_len_fwd tl; + u64_add (int_to_u64 1) i + od + | BetreeListNil => Return (int_to_u64 0)) +’ + +val [betree_list_split_at_fwd_def] = DefineDiv ‘ + (** [betree_main::betree::List::{1}::split_at] *) + betree_list_split_at_fwd + (self : 't betree_list_t) (n : u64) : + ('t betree_list_t # 't betree_list_t) result + = + if n = int_to_u64 0 + then Return (BetreeListNil, self) + else + (case self of + | BetreeListCons hd tl => + do + i <- u64_sub n (int_to_u64 1); + p <- betree_list_split_at_fwd tl i; + let (ls0, ls1) = p in let l = ls0 in Return (BetreeListCons hd l, ls1) + od + | BetreeListNil => Fail Failure) +’ + +val betree_list_push_front_fwd_back_def = Define ‘ + (** [betree_main::betree::List::{1}::push_front] *) + betree_list_push_front_fwd_back + (self : 't betree_list_t) (x : 't) : 't betree_list_t result = + let tl = mem_replace_fwd self BetreeListNil in + let l = tl in + Return (BetreeListCons x l) +’ + +val betree_list_pop_front_fwd_def = Define ‘ + (** [betree_main::betree::List::{1}::pop_front] *) + betree_list_pop_front_fwd (self : 't betree_list_t) : 't result = + let ls = mem_replace_fwd self BetreeListNil in + (case ls of + | BetreeListCons x tl => Return x + | BetreeListNil => Fail Failure) +’ + +val betree_list_pop_front_back_def = Define ‘ + (** [betree_main::betree::List::{1}::pop_front] *) + betree_list_pop_front_back + (self : 't betree_list_t) : 't betree_list_t result = + let ls = mem_replace_fwd self BetreeListNil in + (case ls of + | BetreeListCons x tl => Return tl + | BetreeListNil => Fail Failure) +’ + +val betree_list_hd_fwd_def = Define ‘ + (** [betree_main::betree::List::{1}::hd] *) + betree_list_hd_fwd (self : 't betree_list_t) : 't result = + (case self of + | BetreeListCons hd l => Return hd + | BetreeListNil => Fail Failure) +’ + +val betree_list_head_has_key_fwd_def = Define ‘ + (** [betree_main::betree::List::{2}::head_has_key] *) + betree_list_head_has_key_fwd + (self : (u64 # 't) betree_list_t) (key : u64) : bool result = + (case self of + | BetreeListCons hd l => let (i, _) = hd in Return (i = key) + | BetreeListNil => Return F) +’ + +val [betree_list_partition_at_pivot_fwd_def] = DefineDiv ‘ + (** [betree_main::betree::List::{2}::partition_at_pivot] *) + betree_list_partition_at_pivot_fwd + (self : (u64 # 't) betree_list_t) (pivot : u64) : + ((u64 # 't) betree_list_t # (u64 # 't) betree_list_t) result + = + (case self of + | BetreeListCons hd tl => + let (i, t) = hd in + if u64_ge i pivot + then Return (BetreeListNil, BetreeListCons (i, t) tl) + else ( + do + p <- betree_list_partition_at_pivot_fwd tl pivot; + let (ls0, ls1) = p in + let l = ls0 in + Return (BetreeListCons (i, t) l, ls1) + od) + | BetreeListNil => Return (BetreeListNil, BetreeListNil)) +’ + +val betree_leaf_split_fwd_def = Define ‘ + (** [betree_main::betree::Leaf::{3}::split] *) + betree_leaf_split_fwd + (self : betree_leaf_t) (content : (u64 # u64) betree_list_t) + (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) + (st : state) : + (state # betree_internal_t) result + = + do + p <- betree_list_split_at_fwd content params.betree_params_split_size; + let (content0, content1) = p in + do + p0 <- betree_list_hd_fwd content1; + let (pivot, _) = p0 in + do + id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; + id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; + (st0, _) <- betree_store_leaf_node_fwd id0 content0 st; + (st1, _) <- betree_store_leaf_node_fwd id1 content1 st0; + let n = BetreeNodeLeaf + (<| + betree_leaf_id := id0; + betree_leaf_size := params.betree_params_split_size + |>) in + let n0 = BetreeNodeLeaf + (<| + betree_leaf_id := id1; + betree_leaf_size := params.betree_params_split_size + |>) in + Return (st1, + <| + betree_internal_id := self.betree_leaf_id; + betree_internal_pivot := pivot; + betree_internal_left := n; + betree_internal_right := n0 + |>) + od + od + od +’ + +val betree_leaf_split_back_def = Define ‘ + (** [betree_main::betree::Leaf::{3}::split] *) + betree_leaf_split_back + (self : betree_leaf_t) (content : (u64 # u64) betree_list_t) + (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) + (st : state) : + betree_node_id_counter_t result + = + do + p <- betree_list_split_at_fwd content params.betree_params_split_size; + let (content0, content1) = p in + do + _ <- betree_list_hd_fwd content1; + id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; + id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; + (st0, _) <- betree_store_leaf_node_fwd id0 content0 st; + _ <- betree_store_leaf_node_fwd id1 content1 st0; + betree_node_id_counter_fresh_id_back node_id_cnt0 + od + od +’ + +val [betree_node_lookup_in_bindings_fwd_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::lookup_in_bindings] *) + betree_node_lookup_in_bindings_fwd + (key : u64) (bindings : (u64 # u64) betree_list_t) : u64 option result = + (case bindings of + | BetreeListCons hd tl => + let (i, i0) = hd in + if i = key + then Return (SOME i0) + else + if u64_gt i key + then Return NONE + else betree_node_lookup_in_bindings_fwd key tl + | BetreeListNil => Return NONE) +’ + +val [betree_node_lookup_first_message_for_key_fwd_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *) + betree_node_lookup_first_message_for_key_fwd + (key : u64) (msgs : (u64 # betree_message_t) betree_list_t) : + (u64 # betree_message_t) betree_list_t result + = + (case msgs of + | BetreeListCons x next_msgs => + let (i, m) = x in + if u64_ge i key + then Return (BetreeListCons (i, m) next_msgs) + else betree_node_lookup_first_message_for_key_fwd key next_msgs + | BetreeListNil => Return BetreeListNil) +’ + +val [betree_node_lookup_first_message_for_key_back_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *) + betree_node_lookup_first_message_for_key_back + (key : u64) (msgs : (u64 # betree_message_t) betree_list_t) + (ret : (u64 # betree_message_t) betree_list_t) : + (u64 # betree_message_t) betree_list_t result + = + (case msgs of + | BetreeListCons x next_msgs => + let (i, m) = x in + if u64_ge i key + then Return ret + else ( + do + next_msgs0 <- + betree_node_lookup_first_message_for_key_back key next_msgs ret; + Return (BetreeListCons (i, m) next_msgs0) + od) + | BetreeListNil => Return ret) +’ + +val [betree_node_apply_upserts_fwd_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::apply_upserts] *) + betree_node_apply_upserts_fwd + (msgs : (u64 # betree_message_t) betree_list_t) (prev : u64 option) + (key : u64) (st : state) : + (state # u64) result + = + do + b <- betree_list_head_has_key_fwd msgs key; + if b + then ( + do + msg <- betree_list_pop_front_fwd msgs; + let (_, m) = msg in + (case m of + | BetreeMessageInsert i => Fail Failure + | BetreeMessageDelete => Fail Failure + | BetreeMessageUpsert s => + do + v <- betree_upsert_update_fwd prev s; + msgs0 <- betree_list_pop_front_back msgs; + betree_node_apply_upserts_fwd msgs0 (SOME v) key st + od) + od) + else ( + do + (st0, v) <- core_option_option_unwrap_fwd prev st; + _ <- betree_list_push_front_fwd_back msgs (key, BetreeMessageInsert v); + Return (st0, v) + od) + od +’ + +val [betree_node_apply_upserts_back_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::apply_upserts] *) + betree_node_apply_upserts_back + (msgs : (u64 # betree_message_t) betree_list_t) (prev : u64 option) + (key : u64) (st : state) : + (u64 # betree_message_t) betree_list_t result + = + do + b <- betree_list_head_has_key_fwd msgs key; + if b + then ( + do + msg <- betree_list_pop_front_fwd msgs; + let (_, m) = msg in + (case m of + | BetreeMessageInsert i => Fail Failure + | BetreeMessageDelete => Fail Failure + | BetreeMessageUpsert s => + do + v <- betree_upsert_update_fwd prev s; + msgs0 <- betree_list_pop_front_back msgs; + betree_node_apply_upserts_back msgs0 (SOME v) key st + od) + od) + else ( + do + (_, v) <- core_option_option_unwrap_fwd prev st; + betree_list_push_front_fwd_back msgs (key, BetreeMessageInsert v) + od) + od +’ + +val [betree_node_lookup_fwd_def, betree_node_lookup_back_def, betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_children_back_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::lookup] *) + (betree_node_lookup_fwd + (self : betree_node_t) (key : u64) (st : state) : + (state # u64 option) result + = + (case self of + | BetreeNodeInternal node => + do + (st0, msgs) <- betree_load_internal_node_fwd node.betree_internal_id st; + pending <- betree_node_lookup_first_message_for_key_fwd key msgs; + (case pending of + | BetreeListCons p l => + let (k, msg) = p in + if k <> key + then ( + do + (st1, opt) <- betree_internal_lookup_in_children_fwd node key st0; + _ <- + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, msg) l); + Return (st1, opt) + od) + else + (case msg of + | BetreeMessageInsert v => + do + _ <- + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, BetreeMessageInsert v) l); + Return (st0, SOME v) + od + | BetreeMessageDelete => + do + _ <- + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, BetreeMessageDelete) l); + Return (st0, NONE) + od + | BetreeMessageUpsert ufs => + do + (st1, v) <- betree_internal_lookup_in_children_fwd node key st0; + (st2, v0) <- + betree_node_apply_upserts_fwd (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + node0 <- betree_internal_lookup_in_children_back node key st0; + pending0 <- + betree_node_apply_upserts_back (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + msgs0 <- + betree_node_lookup_first_message_for_key_back key msgs pending0; + (st3, _) <- + betree_store_internal_node_fwd node0.betree_internal_id msgs0 st2; + Return (st3, SOME v0) + od) + | BetreeListNil => + do + (st1, opt) <- betree_internal_lookup_in_children_fwd node key st0; + _ <- + betree_node_lookup_first_message_for_key_back key msgs BetreeListNil; + Return (st1, opt) + od) + od + | BetreeNodeLeaf node => + do + (st0, bindings) <- betree_load_leaf_node_fwd node.betree_leaf_id st; + opt <- betree_node_lookup_in_bindings_fwd key bindings; + Return (st0, opt) + od)) + /\ + + (** [betree_main::betree::Node::{5}::lookup] *) + (betree_node_lookup_back + (self : betree_node_t) (key : u64) (st : state) : betree_node_t result = + (case self of + | BetreeNodeInternal node => + do + (st0, msgs) <- betree_load_internal_node_fwd node.betree_internal_id st; + pending <- betree_node_lookup_first_message_for_key_fwd key msgs; + (case pending of + | BetreeListCons p l => + let (k, msg) = p in + if k <> key + then ( + do + _ <- + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, msg) l); + node0 <- betree_internal_lookup_in_children_back node key st0; + Return (BetreeNodeInternal node0) + od) + else + (case msg of + | BetreeMessageInsert v => + do + _ <- + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, BetreeMessageInsert v) l); + Return (BetreeNodeInternal node) + od + | BetreeMessageDelete => + do + _ <- + betree_node_lookup_first_message_for_key_back key msgs + (BetreeListCons (k, BetreeMessageDelete) l); + Return (BetreeNodeInternal node) + od + | BetreeMessageUpsert ufs => + do + (st1, v) <- betree_internal_lookup_in_children_fwd node key st0; + (st2, _) <- + betree_node_apply_upserts_fwd (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + node0 <- betree_internal_lookup_in_children_back node key st0; + pending0 <- + betree_node_apply_upserts_back (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + msgs0 <- + betree_node_lookup_first_message_for_key_back key msgs pending0; + _ <- + betree_store_internal_node_fwd node0.betree_internal_id msgs0 st2; + Return (BetreeNodeInternal node0) + od) + | BetreeListNil => + do + _ <- + betree_node_lookup_first_message_for_key_back key msgs BetreeListNil; + node0 <- betree_internal_lookup_in_children_back node key st0; + Return (BetreeNodeInternal node0) + od) + od + | BetreeNodeLeaf node => + do + (_, bindings) <- betree_load_leaf_node_fwd node.betree_leaf_id st; + _ <- betree_node_lookup_in_bindings_fwd key bindings; + Return (BetreeNodeLeaf node) + od)) + /\ + + (** [betree_main::betree::Internal::{4}::lookup_in_children] *) + (betree_internal_lookup_in_children_fwd + (self : betree_internal_t) (key : u64) (st : state) : + (state # u64 option) result + = + if u64_lt key self.betree_internal_pivot + then betree_node_lookup_fwd self.betree_internal_left key st + else betree_node_lookup_fwd self.betree_internal_right key st) + /\ + + (** [betree_main::betree::Internal::{4}::lookup_in_children] *) + betree_internal_lookup_in_children_back + (self : betree_internal_t) (key : u64) (st : state) : + betree_internal_t result + = + if u64_lt key self.betree_internal_pivot + then ( + do + n <- betree_node_lookup_back self.betree_internal_left key st; + Return (self with <| betree_internal_left := n |>) + od) + else ( + do + n <- betree_node_lookup_back self.betree_internal_right key st; + Return (self with <| betree_internal_right := n |>) + od) +’ + +val [betree_node_lookup_mut_in_bindings_fwd_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) + betree_node_lookup_mut_in_bindings_fwd + (key : u64) (bindings : (u64 # u64) betree_list_t) : + (u64 # u64) betree_list_t result + = + (case bindings of + | BetreeListCons hd tl => + let (i, i0) = hd in + if u64_ge i key + then Return (BetreeListCons (i, i0) tl) + else betree_node_lookup_mut_in_bindings_fwd key tl + | BetreeListNil => Return BetreeListNil) +’ + +val [betree_node_lookup_mut_in_bindings_back_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) + betree_node_lookup_mut_in_bindings_back + (key : u64) (bindings : (u64 # u64) betree_list_t) + (ret : (u64 # u64) betree_list_t) : + (u64 # u64) betree_list_t result + = + (case bindings of + | BetreeListCons hd tl => + let (i, i0) = hd in + if u64_ge i key + then Return ret + else ( + do + tl0 <- betree_node_lookup_mut_in_bindings_back key tl ret; + Return (BetreeListCons (i, i0) tl0) + od) + | BetreeListNil => Return ret) +’ + +val betree_node_apply_to_leaf_fwd_back_def = Define ‘ + (** [betree_main::betree::Node::{5}::apply_to_leaf] *) + betree_node_apply_to_leaf_fwd_back + (bindings : (u64 # u64) betree_list_t) (key : u64) + (new_msg : betree_message_t) : + (u64 # u64) betree_list_t result + = + do + bindings0 <- betree_node_lookup_mut_in_bindings_fwd key bindings; + b <- betree_list_head_has_key_fwd bindings0 key; + if b + then ( + do + hd <- betree_list_pop_front_fwd bindings0; + (case new_msg of + | BetreeMessageInsert v => + do + bindings1 <- betree_list_pop_front_back bindings0; + bindings2 <- betree_list_push_front_fwd_back bindings1 (key, v); + betree_node_lookup_mut_in_bindings_back key bindings bindings2 + od + | BetreeMessageDelete => + do + bindings1 <- betree_list_pop_front_back bindings0; + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + od + | BetreeMessageUpsert s => + let (_, i) = hd in + do + v <- betree_upsert_update_fwd (SOME i) s; + bindings1 <- betree_list_pop_front_back bindings0; + bindings2 <- betree_list_push_front_fwd_back bindings1 (key, v); + betree_node_lookup_mut_in_bindings_back key bindings bindings2 + od) + od) + else + (case new_msg of + | BetreeMessageInsert v => + do + bindings1 <- betree_list_push_front_fwd_back bindings0 (key, v); + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + od + | BetreeMessageDelete => + betree_node_lookup_mut_in_bindings_back key bindings bindings0 + | BetreeMessageUpsert s => + do + v <- betree_upsert_update_fwd NONE s; + bindings1 <- betree_list_push_front_fwd_back bindings0 (key, v); + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + od) + od +’ + +val [betree_node_apply_messages_to_leaf_fwd_back_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *) + betree_node_apply_messages_to_leaf_fwd_back + (bindings : (u64 # u64) betree_list_t) + (new_msgs : (u64 # betree_message_t) betree_list_t) : + (u64 # u64) betree_list_t result + = + (case new_msgs of + | BetreeListCons new_msg new_msgs_tl => + let (i, m) = new_msg in + do + bindings0 <- betree_node_apply_to_leaf_fwd_back bindings i m; + betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl + od + | BetreeListNil => Return bindings) +’ + +val [betree_node_filter_messages_for_key_fwd_back_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::filter_messages_for_key] *) + betree_node_filter_messages_for_key_fwd_back + (key : u64) (msgs : (u64 # betree_message_t) betree_list_t) : + (u64 # betree_message_t) betree_list_t result + = + (case msgs of + | BetreeListCons p l => + let (k, m) = p in + if k = key + then ( + do + msgs0 <- betree_list_pop_front_back (BetreeListCons (k, m) l); + betree_node_filter_messages_for_key_fwd_back key msgs0 + od) + else Return (BetreeListCons (k, m) l) + | BetreeListNil => Return BetreeListNil) +’ + +val [betree_node_lookup_first_message_after_key_fwd_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *) + betree_node_lookup_first_message_after_key_fwd + (key : u64) (msgs : (u64 # betree_message_t) betree_list_t) : + (u64 # betree_message_t) betree_list_t result + = + (case msgs of + | BetreeListCons p next_msgs => + let (k, m) = p in + if k = key + then betree_node_lookup_first_message_after_key_fwd key next_msgs + else Return (BetreeListCons (k, m) next_msgs) + | BetreeListNil => Return BetreeListNil) +’ + +val [betree_node_lookup_first_message_after_key_back_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *) + betree_node_lookup_first_message_after_key_back + (key : u64) (msgs : (u64 # betree_message_t) betree_list_t) + (ret : (u64 # betree_message_t) betree_list_t) : + (u64 # betree_message_t) betree_list_t result + = + (case msgs of + | BetreeListCons p next_msgs => + let (k, m) = p in + if k = key + then ( + do + next_msgs0 <- + betree_node_lookup_first_message_after_key_back key next_msgs ret; + Return (BetreeListCons (k, m) next_msgs0) + od) + else Return ret + | BetreeListNil => Return ret) +’ + +val betree_node_apply_to_internal_fwd_back_def = Define ‘ + (** [betree_main::betree::Node::{5}::apply_to_internal] *) + betree_node_apply_to_internal_fwd_back + (msgs : (u64 # betree_message_t) betree_list_t) (key : u64) + (new_msg : betree_message_t) : + (u64 # betree_message_t) betree_list_t result + = + do + msgs0 <- betree_node_lookup_first_message_for_key_fwd key msgs; + b <- betree_list_head_has_key_fwd msgs0 key; + if b + then + (case new_msg of + | BetreeMessageInsert i => + do + msgs1 <- betree_node_filter_messages_for_key_fwd_back key msgs0; + msgs2 <- + betree_list_push_front_fwd_back msgs1 (key, BetreeMessageInsert i); + betree_node_lookup_first_message_for_key_back key msgs msgs2 + od + | BetreeMessageDelete => + do + msgs1 <- betree_node_filter_messages_for_key_fwd_back key msgs0; + msgs2 <- + betree_list_push_front_fwd_back msgs1 (key, BetreeMessageDelete); + betree_node_lookup_first_message_for_key_back key msgs msgs2 + od + | BetreeMessageUpsert s => + do + p <- betree_list_hd_fwd msgs0; + let (_, m) = p in + (case m of + | BetreeMessageInsert prev => + do + v <- betree_upsert_update_fwd (SOME prev) s; + msgs1 <- betree_list_pop_front_back msgs0; + msgs2 <- + betree_list_push_front_fwd_back msgs1 (key, BetreeMessageInsert v); + betree_node_lookup_first_message_for_key_back key msgs msgs2 + od + | BetreeMessageDelete => + do + v <- betree_upsert_update_fwd NONE s; + msgs1 <- betree_list_pop_front_back msgs0; + msgs2 <- + betree_list_push_front_fwd_back msgs1 (key, BetreeMessageInsert v); + betree_node_lookup_first_message_for_key_back key msgs msgs2 + od + | BetreeMessageUpsert ufs => + do + msgs1 <- betree_node_lookup_first_message_after_key_fwd key msgs0; + msgs2 <- + betree_list_push_front_fwd_back msgs1 (key, BetreeMessageUpsert s); + msgs3 <- + betree_node_lookup_first_message_after_key_back key msgs0 msgs2; + betree_node_lookup_first_message_for_key_back key msgs msgs3 + od) + od) + else ( + do + msgs1 <- betree_list_push_front_fwd_back msgs0 (key, new_msg); + betree_node_lookup_first_message_for_key_back key msgs msgs1 + od) + od +’ + +val [betree_node_apply_messages_to_internal_fwd_back_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::apply_messages_to_internal] *) + betree_node_apply_messages_to_internal_fwd_back + (msgs : (u64 # betree_message_t) betree_list_t) + (new_msgs : (u64 # betree_message_t) betree_list_t) : + (u64 # betree_message_t) betree_list_t result + = + (case new_msgs of + | BetreeListCons new_msg new_msgs_tl => + let (i, m) = new_msg in + do + msgs0 <- betree_node_apply_to_internal_fwd_back msgs i m; + betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl + od + | BetreeListNil => Return msgs) +’ + +val [betree_node_apply_messages_fwd_def, betree_node_apply_messages_back_def, betree_internal_flush_fwd_def, betree_internal_flush_back_def] = DefineDiv ‘ + (** [betree_main::betree::Node::{5}::apply_messages] *) + (betree_node_apply_messages_fwd + (self : betree_node_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (msgs : (u64 # betree_message_t) betree_list_t) (st : state) : + (state # unit) result + = + (case self of + | BetreeNodeInternal node => + do + (st0, content) <- + betree_load_internal_node_fwd node.betree_internal_id st; + content0 <- betree_node_apply_messages_to_internal_fwd_back content msgs; + num_msgs <- betree_list_len_fwd content0; + if u64_ge num_msgs params.betree_params_min_flush_size + then ( + do + (st1, content1) <- + betree_internal_flush_fwd node params node_id_cnt content0 st0; + (node0, _) <- + betree_internal_flush_back node params node_id_cnt content0 st0; + (st2, _) <- + betree_store_internal_node_fwd node0.betree_internal_id content1 st1; + Return (st2, ()) + od) + else ( + do + (st1, _) <- + betree_store_internal_node_fwd node.betree_internal_id content0 st0; + Return (st1, ()) + od) + od + | BetreeNodeLeaf node => + do + (st0, content) <- betree_load_leaf_node_fwd node.betree_leaf_id st; + content0 <- betree_node_apply_messages_to_leaf_fwd_back content msgs; + len <- betree_list_len_fwd content0; + i <- u64_mul (int_to_u64 2) params.betree_params_split_size; + if u64_ge len i + then ( + do + (st1, _) <- betree_leaf_split_fwd node content0 params node_id_cnt st0; + (st2, _) <- + betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1; + Return (st2, ()) + od) + else ( + do + (st1, _) <- + betree_store_leaf_node_fwd node.betree_leaf_id content0 st0; + Return (st1, ()) + od) + od)) + /\ + + (** [betree_main::betree::Node::{5}::apply_messages] *) + (betree_node_apply_messages_back + (self : betree_node_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (msgs : (u64 # betree_message_t) betree_list_t) (st : state) : + (betree_node_t # betree_node_id_counter_t) result + = + (case self of + | BetreeNodeInternal node => + do + (st0, content) <- + betree_load_internal_node_fwd node.betree_internal_id st; + content0 <- betree_node_apply_messages_to_internal_fwd_back content msgs; + num_msgs <- betree_list_len_fwd content0; + if u64_ge num_msgs params.betree_params_min_flush_size + then ( + do + (st1, content1) <- + betree_internal_flush_fwd node params node_id_cnt content0 st0; + (node0, node_id_cnt0) <- + betree_internal_flush_back node params node_id_cnt content0 st0; + _ <- + betree_store_internal_node_fwd node0.betree_internal_id content1 st1; + Return (BetreeNodeInternal node0, node_id_cnt0) + od) + else ( + do + _ <- + betree_store_internal_node_fwd node.betree_internal_id content0 st0; + Return (BetreeNodeInternal node, node_id_cnt) + od) + od + | BetreeNodeLeaf node => + do + (st0, content) <- betree_load_leaf_node_fwd node.betree_leaf_id st; + content0 <- betree_node_apply_messages_to_leaf_fwd_back content msgs; + len <- betree_list_len_fwd content0; + i <- u64_mul (int_to_u64 2) params.betree_params_split_size; + if u64_ge len i + then ( + do + (st1, new_node) <- + betree_leaf_split_fwd node content0 params node_id_cnt st0; + _ <- betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1; + node_id_cnt0 <- + betree_leaf_split_back node content0 params node_id_cnt st0; + Return (BetreeNodeInternal new_node, node_id_cnt0) + od) + else ( + do + _ <- betree_store_leaf_node_fwd node.betree_leaf_id content0 st0; + Return (BetreeNodeLeaf (node with <| betree_leaf_size := len |>), + node_id_cnt) + od) + od)) + /\ + + (** [betree_main::betree::Internal::{4}::flush] *) + (betree_internal_flush_fwd + (self : betree_internal_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (content : (u64 # betree_message_t) betree_list_t) (st : state) : + (state # (u64 # betree_message_t) betree_list_t) result + = + do + p <- betree_list_partition_at_pivot_fwd content self.betree_internal_pivot; + let (msgs_left, msgs_right) = p in + do + len_left <- betree_list_len_fwd msgs_left; + if u64_ge len_left params.betree_params_min_flush_size + then ( + do + (st0, _) <- + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st; + (_, node_id_cnt0) <- + betree_node_apply_messages_back self.betree_internal_left params + node_id_cnt msgs_left st; + len_right <- betree_list_len_fwd msgs_right; + if u64_ge len_right params.betree_params_min_flush_size + then ( + do + (st1, _) <- + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt0 msgs_right st0; + _ <- + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt0 msgs_right st0; + Return (st1, BetreeListNil) + od) + else Return (st0, msgs_right) + od) + else ( + do + (st0, _) <- + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt msgs_right st; + _ <- + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt msgs_right st; + Return (st0, msgs_left) + od) + od + od) + /\ + + (** [betree_main::betree::Internal::{4}::flush] *) + betree_internal_flush_back + (self : betree_internal_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (content : (u64 # betree_message_t) betree_list_t) (st : state) : + (betree_internal_t # betree_node_id_counter_t) result + = + do + p <- betree_list_partition_at_pivot_fwd content self.betree_internal_pivot; + let (msgs_left, msgs_right) = p in + do + len_left <- betree_list_len_fwd msgs_left; + if u64_ge len_left params.betree_params_min_flush_size + then ( + do + (st0, _) <- + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st; + (n, node_id_cnt0) <- + betree_node_apply_messages_back self.betree_internal_left params + node_id_cnt msgs_left st; + len_right <- betree_list_len_fwd msgs_right; + if u64_ge len_right params.betree_params_min_flush_size + then ( + do + (n0, node_id_cnt1) <- + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt0 msgs_right st0; + Return + (self + with + <| + betree_internal_left := n; betree_internal_right := n0 + |>, node_id_cnt1) + od) + else Return (self with <| betree_internal_left := n |>, node_id_cnt0) + od) + else ( + do + (n, node_id_cnt0) <- + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt msgs_right st; + Return (self with <| betree_internal_right := n |>, node_id_cnt0) + od) + od + od +’ + +val betree_node_apply_fwd_def = Define ‘ + (** [betree_main::betree::Node::{5}::apply] *) + betree_node_apply_fwd + (self : betree_node_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) (key : u64) + (new_msg : betree_message_t) (st : state) : + (state # unit) result + = + let l = BetreeListNil in + do + (st0, _) <- + betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons + (key, new_msg) l) st; + _ <- + betree_node_apply_messages_back self params node_id_cnt (BetreeListCons + (key, new_msg) l) st; + Return (st0, ()) + od +’ + +val betree_node_apply_back_def = Define ‘ + (** [betree_main::betree::Node::{5}::apply] *) + betree_node_apply_back + (self : betree_node_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) (key : u64) + (new_msg : betree_message_t) (st : state) : + (betree_node_t # betree_node_id_counter_t) result + = + let l = BetreeListNil in + betree_node_apply_messages_back self params node_id_cnt (BetreeListCons + (key, new_msg) l) st +’ + +val betree_be_tree_new_fwd_def = Define ‘ + (** [betree_main::betree::BeTree::{6}::new] *) + betree_be_tree_new_fwd + (min_flush_size : u64) (split_size : u64) (st : state) : + (state # betree_be_tree_t) result + = + do + node_id_cnt <- betree_node_id_counter_new_fwd; + id <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + (st0, _) <- betree_store_leaf_node_fwd id BetreeListNil st; + node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; + Return (st0, + <| + betree_be_tree_params := + (<| + betree_params_min_flush_size := min_flush_size; + betree_params_split_size := split_size + |>); + betree_be_tree_node_id_cnt := node_id_cnt0; + betree_be_tree_root := + (BetreeNodeLeaf + (<| betree_leaf_id := id; betree_leaf_size := (int_to_u64 0) |>)) + |>) + od +’ + +val betree_be_tree_apply_fwd_def = Define ‘ + (** [betree_main::betree::BeTree::{6}::apply] *) + betree_be_tree_apply_fwd + (self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state) + : + (state # unit) result + = + do + (st0, _) <- + betree_node_apply_fwd self.betree_be_tree_root self.betree_be_tree_params + self.betree_be_tree_node_id_cnt key msg st; + _ <- + betree_node_apply_back self.betree_be_tree_root + self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st; + Return (st0, ()) + od +’ + +val betree_be_tree_apply_back_def = Define ‘ + (** [betree_main::betree::BeTree::{6}::apply] *) + betree_be_tree_apply_back + (self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state) + : + betree_be_tree_t result + = + do + (n, nic) <- + betree_node_apply_back self.betree_be_tree_root + self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st; + Return + (self + with + <| + betree_be_tree_node_id_cnt := nic; betree_be_tree_root := n + |>) + od +’ + +val betree_be_tree_insert_fwd_def = Define ‘ + (** [betree_main::betree::BeTree::{6}::insert] *) + betree_be_tree_insert_fwd + (self : betree_be_tree_t) (key : u64) (value : u64) (st : state) : + (state # unit) result + = + do + (st0, _) <- + betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st; + _ <- betree_be_tree_apply_back self key (BetreeMessageInsert value) st; + Return (st0, ()) + od +’ + +val betree_be_tree_insert_back_def = Define ‘ + (** [betree_main::betree::BeTree::{6}::insert] *) + betree_be_tree_insert_back + (self : betree_be_tree_t) (key : u64) (value : u64) (st : state) : + betree_be_tree_t result + = + betree_be_tree_apply_back self key (BetreeMessageInsert value) st +’ + +val betree_be_tree_delete_fwd_def = Define ‘ + (** [betree_main::betree::BeTree::{6}::delete] *) + betree_be_tree_delete_fwd + (self : betree_be_tree_t) (key : u64) (st : state) : + (state # unit) result + = + do + (st0, _) <- betree_be_tree_apply_fwd self key BetreeMessageDelete st; + _ <- betree_be_tree_apply_back self key BetreeMessageDelete st; + Return (st0, ()) + od +’ + +val betree_be_tree_delete_back_def = Define ‘ + (** [betree_main::betree::BeTree::{6}::delete] *) + betree_be_tree_delete_back + (self : betree_be_tree_t) (key : u64) (st : state) : + betree_be_tree_t result + = + betree_be_tree_apply_back self key BetreeMessageDelete st +’ + +val betree_be_tree_upsert_fwd_def = Define ‘ + (** [betree_main::betree::BeTree::{6}::upsert] *) + betree_be_tree_upsert_fwd + (self : betree_be_tree_t) (key : u64) (upd : betree_upsert_fun_state_t) + (st : state) : + (state # unit) result + = + do + (st0, _) <- betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st; + _ <- betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st; + Return (st0, ()) + od +’ + +val betree_be_tree_upsert_back_def = Define ‘ + (** [betree_main::betree::BeTree::{6}::upsert] *) + betree_be_tree_upsert_back + (self : betree_be_tree_t) (key : u64) (upd : betree_upsert_fun_state_t) + (st : state) : + betree_be_tree_t result + = + betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st +’ + +val betree_be_tree_lookup_fwd_def = Define ‘ + (** [betree_main::betree::BeTree::{6}::lookup] *) + betree_be_tree_lookup_fwd + (self : betree_be_tree_t) (key : u64) (st : state) : + (state # u64 option) result + = + betree_node_lookup_fwd self.betree_be_tree_root key st +’ + +val betree_be_tree_lookup_back_def = Define ‘ + (** [betree_main::betree::BeTree::{6}::lookup] *) + betree_be_tree_lookup_back + (self : betree_be_tree_t) (key : u64) (st : state) : + betree_be_tree_t result + = + do + n <- betree_node_lookup_back self.betree_be_tree_root key st; + Return (self with <| betree_be_tree_root := n |>) + od +’ + +val main_fwd_def = Define ‘ + (** [betree_main::main] *) + main_fwd : unit result = + Return () +’ + +(** Unit test for [betree_main::main] *) +val _ = assert_return (“main_fwd”) + +val _ = export_theory () diff --git a/tests/hol4/betree/betreeMain_FunsTheory.sig b/tests/hol4/betree/betreeMain_FunsTheory.sig new file mode 100644 index 00000000..6c249f70 --- /dev/null +++ b/tests/hol4/betree/betreeMain_FunsTheory.sig @@ -0,0 +1,1240 @@ +signature betreeMain_FunsTheory = +sig + type thm = Thm.thm + + (* Definitions *) + val betree_be_tree_apply_back_def : thm + val betree_be_tree_apply_fwd_def : thm + val betree_be_tree_delete_back_def : thm + val betree_be_tree_delete_fwd_def : thm + val betree_be_tree_insert_back_def : thm + val betree_be_tree_insert_fwd_def : thm + val betree_be_tree_lookup_back_def : thm + val betree_be_tree_lookup_fwd_def : thm + val betree_be_tree_new_fwd_def : thm + val betree_be_tree_upsert_back_def : thm + val betree_be_tree_upsert_fwd_def : thm + val betree_fresh_node_id_back_def : thm + val betree_fresh_node_id_fwd_def : thm + val betree_internal_flush_back_def : thm + val betree_internal_flush_fwd_def : thm + val betree_internal_lookup_in_children_back_def : thm + val betree_internal_lookup_in_children_fwd_def : thm + val betree_leaf_split_back_def : thm + val betree_leaf_split_fwd_def : thm + val betree_list_hd_fwd_def : thm + val betree_list_head_has_key_fwd_def : thm + val betree_list_len_fwd_def : thm + val betree_list_partition_at_pivot_fwd_def : thm + val betree_list_pop_front_back_def : thm + val betree_list_pop_front_fwd_def : thm + val betree_list_push_front_fwd_back_def : thm + val betree_list_split_at_fwd_def : thm + val betree_load_internal_node_fwd_def : thm + val betree_load_leaf_node_fwd_def : thm + val betree_node_apply_back_def : thm + val betree_node_apply_fwd_def : thm + val betree_node_apply_messages_back_def : thm + val betree_node_apply_messages_fwd_def : thm + val betree_node_apply_messages_to_internal_fwd_back_def : thm + val betree_node_apply_messages_to_leaf_fwd_back_def : thm + val betree_node_apply_to_internal_fwd_back_def : thm + val betree_node_apply_to_leaf_fwd_back_def : thm + val betree_node_apply_upserts_back_def : thm + val betree_node_apply_upserts_fwd_def : thm + val betree_node_filter_messages_for_key_fwd_back_def : thm + val betree_node_id_counter_fresh_id_back_def : thm + val betree_node_id_counter_fresh_id_fwd_def : thm + val betree_node_id_counter_new_fwd_def : thm + val betree_node_lookup_back_def : thm + val betree_node_lookup_first_message_after_key_back_def : thm + val betree_node_lookup_first_message_after_key_fwd_def : thm + val betree_node_lookup_first_message_for_key_back_def : thm + val betree_node_lookup_first_message_for_key_fwd_def : thm + val betree_node_lookup_fwd_def : thm + val betree_node_lookup_in_bindings_fwd_def : thm + val betree_node_lookup_mut_in_bindings_back_def : thm + val betree_node_lookup_mut_in_bindings_fwd_def : thm + val betree_store_internal_node_fwd_def : thm + val betree_store_leaf_node_fwd_def : thm + val betree_upsert_update_fwd_def : thm + val core_num_u64_max_body_def : thm + val core_num_u64_max_c_def : thm + val main_fwd_def : thm + + val betreeMain_Funs_grammars : type_grammar.grammar * term_grammar.grammar +(* + [betreeMain_Opaque] Parent theory of "betreeMain_Funs" + + [betree_be_tree_apply_back_def] Definition + + ⊢ ∀self key msg st. + betree_be_tree_apply_back self key msg st = + do + (n,nic) <- + betree_node_apply_back self.betree_be_tree_root + self.betree_be_tree_params self.betree_be_tree_node_id_cnt + key msg st; + Return + (self with + <|betree_be_tree_node_id_cnt := nic; + betree_be_tree_root := n|>) + od + + [betree_be_tree_apply_fwd_def] Definition + + ⊢ ∀self key msg st. + betree_be_tree_apply_fwd self key msg st = + do + (st0,_) <- + betree_node_apply_fwd self.betree_be_tree_root + self.betree_be_tree_params self.betree_be_tree_node_id_cnt + key msg st; + monad_ignore_bind + (betree_node_apply_back self.betree_be_tree_root + self.betree_be_tree_params self.betree_be_tree_node_id_cnt + key msg st) (Return (st0,())) + od + + [betree_be_tree_delete_back_def] Definition + + ⊢ ∀self key st. + betree_be_tree_delete_back self key st = + betree_be_tree_apply_back self key BetreeMessageDelete st + + [betree_be_tree_delete_fwd_def] Definition + + ⊢ ∀self key st. + betree_be_tree_delete_fwd self key st = + do + (st0,_) <- + betree_be_tree_apply_fwd self key BetreeMessageDelete st; + monad_ignore_bind + (betree_be_tree_apply_back self key BetreeMessageDelete st) + (Return (st0,())) + od + + [betree_be_tree_insert_back_def] Definition + + ⊢ ∀self key value st. + betree_be_tree_insert_back self key value st = + betree_be_tree_apply_back self key (BetreeMessageInsert value) st + + [betree_be_tree_insert_fwd_def] Definition + + ⊢ ∀self key value st. + betree_be_tree_insert_fwd self key value st = + do + (st0,_) <- + betree_be_tree_apply_fwd self key (BetreeMessageInsert value) + st; + monad_ignore_bind + (betree_be_tree_apply_back self key + (BetreeMessageInsert value) st) (Return (st0,())) + od + + [betree_be_tree_lookup_back_def] Definition + + ⊢ ∀self key st. + betree_be_tree_lookup_back self key st = + do + n <- betree_node_lookup_back self.betree_be_tree_root key st; + Return (self with betree_be_tree_root := n) + od + + [betree_be_tree_lookup_fwd_def] Definition + + ⊢ ∀self key st. + betree_be_tree_lookup_fwd self key st = + betree_node_lookup_fwd self.betree_be_tree_root key st + + [betree_be_tree_new_fwd_def] Definition + + ⊢ ∀min_flush_size split_size st. + betree_be_tree_new_fwd min_flush_size split_size st = + do + node_id_cnt <- betree_node_id_counter_new_fwd; + id <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + (st0,_) <- betree_store_leaf_node_fwd id BetreeListNil st; + node_id_cnt0 <- + betree_node_id_counter_fresh_id_back node_id_cnt; + Return + (st0, + <|betree_be_tree_params := + <|betree_params_min_flush_size := min_flush_size; + betree_params_split_size := split_size|>; + betree_be_tree_node_id_cnt := node_id_cnt0; + betree_be_tree_root := + BetreeNodeLeaf + <|betree_leaf_id := id; + betree_leaf_size := int_to_u64 0|> |>) + od + + [betree_be_tree_upsert_back_def] Definition + + ⊢ ∀self key upd st. + betree_be_tree_upsert_back self key upd st = + betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st + + [betree_be_tree_upsert_fwd_def] Definition + + ⊢ ∀self key upd st. + betree_be_tree_upsert_fwd self key upd st = + do + (st0,_) <- + betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) + st; + monad_ignore_bind + (betree_be_tree_apply_back self key (BetreeMessageUpsert upd) + st) (Return (st0,())) + od + + [betree_fresh_node_id_back_def] Definition + + ⊢ ∀counter. + betree_fresh_node_id_back counter = + u64_add counter (int_to_u64 1) + + [betree_fresh_node_id_fwd_def] Definition + + ⊢ ∀counter. + betree_fresh_node_id_fwd counter = + monad_ignore_bind (u64_add counter (int_to_u64 1)) + (Return counter) + + [betree_internal_flush_back_def] Definition + + ⊢ ∀self params node_id_cnt content st. + betree_internal_flush_back self params node_id_cnt content st = + do + p <- + betree_list_partition_at_pivot_fwd content + self.betree_internal_pivot; + (msgs_left,msgs_right) <<- p; + len_left <- betree_list_len_fwd msgs_left; + if u64_ge len_left params.betree_params_min_flush_size then + do + (st0,_) <- + betree_node_apply_messages_fwd self.betree_internal_left + params node_id_cnt msgs_left st; + (n,node_id_cnt0) <- + betree_node_apply_messages_back self.betree_internal_left + params node_id_cnt msgs_left st; + len_right <- betree_list_len_fwd msgs_right; + if + u64_ge len_right params.betree_params_min_flush_size + then + do + (n0,node_id_cnt1) <- + betree_node_apply_messages_back + self.betree_internal_right params node_id_cnt0 + msgs_right st0; + Return + (self with + <|betree_internal_left := n; + betree_internal_right := n0|>,node_id_cnt1) + od + else + Return (self with betree_internal_left := n,node_id_cnt0) + od + else + do + (n,node_id_cnt0) <- + betree_node_apply_messages_back + self.betree_internal_right params node_id_cnt + msgs_right st; + Return (self with betree_internal_right := n,node_id_cnt0) + od + od + + [betree_internal_flush_fwd_def] Definition + + ⊢ ∀self params node_id_cnt content st. + betree_internal_flush_fwd self params node_id_cnt content st = + do + p <- + betree_list_partition_at_pivot_fwd content + self.betree_internal_pivot; + (msgs_left,msgs_right) <<- p; + len_left <- betree_list_len_fwd msgs_left; + if u64_ge len_left params.betree_params_min_flush_size then + do + (st0,_) <- + betree_node_apply_messages_fwd self.betree_internal_left + params node_id_cnt msgs_left st; + (_,node_id_cnt0) <- + betree_node_apply_messages_back self.betree_internal_left + params node_id_cnt msgs_left st; + len_right <- betree_list_len_fwd msgs_right; + if + u64_ge len_right params.betree_params_min_flush_size + then + do + (st1,_) <- + betree_node_apply_messages_fwd + self.betree_internal_right params node_id_cnt0 + msgs_right st0; + monad_ignore_bind + (betree_node_apply_messages_back + self.betree_internal_right params node_id_cnt0 + msgs_right st0) (Return (st1,BetreeListNil)) + od + else Return (st0,msgs_right) + od + else + do + (st0,_) <- + betree_node_apply_messages_fwd self.betree_internal_right + params node_id_cnt msgs_right st; + monad_ignore_bind + (betree_node_apply_messages_back + self.betree_internal_right params node_id_cnt + msgs_right st) (Return (st0,msgs_left)) + od + od + + [betree_internal_lookup_in_children_back_def] Definition + + ⊢ ∀self key st. + betree_internal_lookup_in_children_back self key st = + if u64_lt key self.betree_internal_pivot then + do + n <- betree_node_lookup_back self.betree_internal_left key st; + Return (self with betree_internal_left := n) + od + else + do + n <- + betree_node_lookup_back self.betree_internal_right key st; + Return (self with betree_internal_right := n) + od + + [betree_internal_lookup_in_children_fwd_def] Definition + + ⊢ ∀self key st. + betree_internal_lookup_in_children_fwd self key st = + if u64_lt key self.betree_internal_pivot then + betree_node_lookup_fwd self.betree_internal_left key st + else betree_node_lookup_fwd self.betree_internal_right key st + + [betree_leaf_split_back_def] Definition + + ⊢ ∀self content params node_id_cnt st. + betree_leaf_split_back self content params node_id_cnt st = + do + p <- + betree_list_split_at_fwd content + params.betree_params_split_size; + (content0,content1) <<- p; + monad_ignore_bind (betree_list_hd_fwd content1) + do + id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + node_id_cnt0 <- + betree_node_id_counter_fresh_id_back node_id_cnt; + id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; + (st0,_) <- betree_store_leaf_node_fwd id0 content0 st; + monad_ignore_bind + (betree_store_leaf_node_fwd id1 content1 st0) + (betree_node_id_counter_fresh_id_back node_id_cnt0) + od + od + + [betree_leaf_split_fwd_def] Definition + + ⊢ ∀self content params node_id_cnt st. + betree_leaf_split_fwd self content params node_id_cnt st = + do + p <- + betree_list_split_at_fwd content + params.betree_params_split_size; + (content0,content1) <<- p; + p0 <- betree_list_hd_fwd content1; + (pivot,_) <<- p0; + id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + node_id_cnt0 <- + betree_node_id_counter_fresh_id_back node_id_cnt; + id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; + (st0,_) <- betree_store_leaf_node_fwd id0 content0 st; + (st1,_) <- betree_store_leaf_node_fwd id1 content1 st0; + n <<- + BetreeNodeLeaf + <|betree_leaf_id := id0; + betree_leaf_size := params.betree_params_split_size|>; + n0 <<- + BetreeNodeLeaf + <|betree_leaf_id := id1; + betree_leaf_size := params.betree_params_split_size|>; + Return + (st1, + <|betree_internal_id := self.betree_leaf_id; + betree_internal_pivot := pivot; betree_internal_left := n; + betree_internal_right := n0|>) + od + + [betree_list_hd_fwd_def] Definition + + ⊢ ∀self. + betree_list_hd_fwd self = + case self of + BetreeListCons hd l => Return hd + | BetreeListNil => Fail Failure + + [betree_list_head_has_key_fwd_def] Definition + + ⊢ ∀self key. + betree_list_head_has_key_fwd self key = + case self of + BetreeListCons hd l => (let (i,_) = hd in Return (i = key)) + | BetreeListNil => Return F + + [betree_list_len_fwd_def] Definition + + ⊢ ∀self. + betree_list_len_fwd self = + case self of + BetreeListCons t tl => + do i <- betree_list_len_fwd tl; u64_add (int_to_u64 1) i od + | BetreeListNil => Return (int_to_u64 0) + + [betree_list_partition_at_pivot_fwd_def] Definition + + ⊢ ∀self pivot. + betree_list_partition_at_pivot_fwd self pivot = + case self of + BetreeListCons hd tl => + (let + (i,t) = hd + in + if u64_ge i pivot then + Return (BetreeListNil,BetreeListCons (i,t) tl) + else + do + p <- betree_list_partition_at_pivot_fwd tl pivot; + (ls0,ls1) <<- p; + l <<- ls0; + Return (BetreeListCons (i,t) l,ls1) + od) + | BetreeListNil => Return (BetreeListNil,BetreeListNil) + + [betree_list_pop_front_back_def] Definition + + ⊢ ∀self. + betree_list_pop_front_back self = + (let + ls = mem_replace_fwd self BetreeListNil + in + case ls of + BetreeListCons x tl => Return tl + | BetreeListNil => Fail Failure) + + [betree_list_pop_front_fwd_def] Definition + + ⊢ ∀self. + betree_list_pop_front_fwd self = + (let + ls = mem_replace_fwd self BetreeListNil + in + case ls of + BetreeListCons x tl => Return x + | BetreeListNil => Fail Failure) + + [betree_list_push_front_fwd_back_def] Definition + + ⊢ ∀self x. + betree_list_push_front_fwd_back self x = + (let + tl = mem_replace_fwd self BetreeListNil; + l = tl + in + Return (BetreeListCons x l)) + + [betree_list_split_at_fwd_def] Definition + + ⊢ ∀self n. + betree_list_split_at_fwd self n = + if n = int_to_u64 0 then Return (BetreeListNil,self) + else + case self of + BetreeListCons hd tl => + do + i <- u64_sub n (int_to_u64 1); + p <- betree_list_split_at_fwd tl i; + (ls0,ls1) <<- p; + l <<- ls0; + Return (BetreeListCons hd l,ls1) + od + | BetreeListNil => Fail Failure + + [betree_load_internal_node_fwd_def] Definition + + ⊢ ∀id st. + betree_load_internal_node_fwd id st = + betree_utils_load_internal_node_fwd id st + + [betree_load_leaf_node_fwd_def] Definition + + ⊢ ∀id st. + betree_load_leaf_node_fwd id st = + betree_utils_load_leaf_node_fwd id st + + [betree_node_apply_back_def] Definition + + ⊢ ∀self params node_id_cnt key new_msg st. + betree_node_apply_back self params node_id_cnt key new_msg st = + (let + l = BetreeListNil + in + betree_node_apply_messages_back self params node_id_cnt + (BetreeListCons (key,new_msg) l) st) + + [betree_node_apply_fwd_def] Definition + + ⊢ ∀self params node_id_cnt key new_msg st. + betree_node_apply_fwd self params node_id_cnt key new_msg st = + (let + l = BetreeListNil + in + do + (st0,_) <- + betree_node_apply_messages_fwd self params node_id_cnt + (BetreeListCons (key,new_msg) l) st; + monad_ignore_bind + (betree_node_apply_messages_back self params node_id_cnt + (BetreeListCons (key,new_msg) l) st) (Return (st0,())) + od) + + [betree_node_apply_messages_back_def] Definition + + ⊢ ∀self params node_id_cnt msgs st. + betree_node_apply_messages_back self params node_id_cnt msgs st = + case self of + BetreeNodeInternal node => + do + (st0,content) <- + betree_load_internal_node_fwd node.betree_internal_id st; + content0 <- + betree_node_apply_messages_to_internal_fwd_back content + msgs; + num_msgs <- betree_list_len_fwd content0; + if u64_ge num_msgs params.betree_params_min_flush_size then + do + (st1,content1) <- + betree_internal_flush_fwd node params node_id_cnt + content0 st0; + (node0,node_id_cnt0) <- + betree_internal_flush_back node params node_id_cnt + content0 st0; + monad_ignore_bind + (betree_store_internal_node_fwd + node0.betree_internal_id content1 st1) + (Return (BetreeNodeInternal node0,node_id_cnt0)) + od + else + monad_ignore_bind + (betree_store_internal_node_fwd node.betree_internal_id + content0 st0) + (Return (BetreeNodeInternal node,node_id_cnt)) + od + | BetreeNodeLeaf node' => + do + (st0,content) <- + betree_load_leaf_node_fwd node'.betree_leaf_id st; + content0 <- + betree_node_apply_messages_to_leaf_fwd_back content msgs; + len <- betree_list_len_fwd content0; + i <- u64_mul (int_to_u64 2) params.betree_params_split_size; + if u64_ge len i then + do + (st1,new_node) <- + betree_leaf_split_fwd node' content0 params node_id_cnt + st0; + monad_ignore_bind + (betree_store_leaf_node_fwd node'.betree_leaf_id + BetreeListNil st1) + do + node_id_cnt0 <- + betree_leaf_split_back node' content0 params + node_id_cnt st0; + Return (BetreeNodeInternal new_node,node_id_cnt0) + od + od + else + monad_ignore_bind + (betree_store_leaf_node_fwd node'.betree_leaf_id content0 + st0) + (Return + (BetreeNodeLeaf (node' with betree_leaf_size := len), + node_id_cnt)) + od + + [betree_node_apply_messages_fwd_def] Definition + + ⊢ ∀self params node_id_cnt msgs st. + betree_node_apply_messages_fwd self params node_id_cnt msgs st = + case self of + BetreeNodeInternal node => + do + (st0,content) <- + betree_load_internal_node_fwd node.betree_internal_id st; + content0 <- + betree_node_apply_messages_to_internal_fwd_back content + msgs; + num_msgs <- betree_list_len_fwd content0; + if u64_ge num_msgs params.betree_params_min_flush_size then + do + (st1,content1) <- + betree_internal_flush_fwd node params node_id_cnt + content0 st0; + (node0,_) <- + betree_internal_flush_back node params node_id_cnt + content0 st0; + (st2,_) <- + betree_store_internal_node_fwd + node0.betree_internal_id content1 st1; + Return (st2,()) + od + else + do + (st1,_) <- + betree_store_internal_node_fwd + node.betree_internal_id content0 st0; + Return (st1,()) + od + od + | BetreeNodeLeaf node' => + do + (st0,content) <- + betree_load_leaf_node_fwd node'.betree_leaf_id st; + content0 <- + betree_node_apply_messages_to_leaf_fwd_back content msgs; + len <- betree_list_len_fwd content0; + i <- u64_mul (int_to_u64 2) params.betree_params_split_size; + if u64_ge len i then + do + (st1,_) <- + betree_leaf_split_fwd node' content0 params node_id_cnt + st0; + (st2,_) <- + betree_store_leaf_node_fwd node'.betree_leaf_id + BetreeListNil st1; + Return (st2,()) + od + else + do + (st1,_) <- + betree_store_leaf_node_fwd node'.betree_leaf_id + content0 st0; + Return (st1,()) + od + od + + [betree_node_apply_messages_to_internal_fwd_back_def] Definition + + ⊢ ∀msgs new_msgs. + betree_node_apply_messages_to_internal_fwd_back msgs new_msgs = + case new_msgs of + BetreeListCons new_msg new_msgs_tl => + (let + (i,m) = new_msg + in + do + msgs0 <- betree_node_apply_to_internal_fwd_back msgs i m; + betree_node_apply_messages_to_internal_fwd_back msgs0 + new_msgs_tl + od) + | BetreeListNil => Return msgs + + [betree_node_apply_messages_to_leaf_fwd_back_def] Definition + + ⊢ ∀bindings new_msgs. + betree_node_apply_messages_to_leaf_fwd_back bindings new_msgs = + case new_msgs of + BetreeListCons new_msg new_msgs_tl => + (let + (i,m) = new_msg + in + do + bindings0 <- + betree_node_apply_to_leaf_fwd_back bindings i m; + betree_node_apply_messages_to_leaf_fwd_back bindings0 + new_msgs_tl + od) + | BetreeListNil => Return bindings + + [betree_node_apply_to_internal_fwd_back_def] Definition + + ⊢ ∀msgs key new_msg. + betree_node_apply_to_internal_fwd_back msgs key new_msg = + do + msgs0 <- betree_node_lookup_first_message_for_key_fwd key msgs; + b <- betree_list_head_has_key_fwd msgs0 key; + if b then + case new_msg of + BetreeMessageInsert i => + do + msgs1 <- + betree_node_filter_messages_for_key_fwd_back key + msgs0; + msgs2 <- + betree_list_push_front_fwd_back msgs1 + (key,BetreeMessageInsert i); + betree_node_lookup_first_message_for_key_back key msgs + msgs2 + od + | BetreeMessageDelete => + do + msgs1 <- + betree_node_filter_messages_for_key_fwd_back key msgs0; + msgs2 <- + betree_list_push_front_fwd_back msgs1 + (key,BetreeMessageDelete); + betree_node_lookup_first_message_for_key_back key msgs + msgs2 + od + | BetreeMessageUpsert s => + do + p <- betree_list_hd_fwd msgs0; + (_,m) <<- p; + case m of + BetreeMessageInsert prev => + do + v <- betree_upsert_update_fwd (SOME prev) s; + msgs1 <- betree_list_pop_front_back msgs0; + msgs2 <- + betree_list_push_front_fwd_back msgs1 + (key,BetreeMessageInsert v); + betree_node_lookup_first_message_for_key_back key + msgs msgs2 + od + | BetreeMessageDelete => + do + v <- betree_upsert_update_fwd NONE s; + msgs1 <- betree_list_pop_front_back msgs0; + msgs2 <- + betree_list_push_front_fwd_back msgs1 + (key,BetreeMessageInsert v); + betree_node_lookup_first_message_for_key_back key + msgs msgs2 + od + | BetreeMessageUpsert ufs => + do + msgs1 <- + betree_node_lookup_first_message_after_key_fwd key + msgs0; + msgs2 <- + betree_list_push_front_fwd_back msgs1 + (key,BetreeMessageUpsert s); + msgs3 <- + betree_node_lookup_first_message_after_key_back key + msgs0 msgs2; + betree_node_lookup_first_message_for_key_back key + msgs msgs3 + od + od + else + do + msgs1 <- + betree_list_push_front_fwd_back msgs0 (key,new_msg); + betree_node_lookup_first_message_for_key_back key msgs + msgs1 + od + od + + [betree_node_apply_to_leaf_fwd_back_def] Definition + + ⊢ ∀bindings key new_msg. + betree_node_apply_to_leaf_fwd_back bindings key new_msg = + do + bindings0 <- + betree_node_lookup_mut_in_bindings_fwd key bindings; + b <- betree_list_head_has_key_fwd bindings0 key; + if b then + do + hd <- betree_list_pop_front_fwd bindings0; + case new_msg of + BetreeMessageInsert v => + do + bindings1 <- betree_list_pop_front_back bindings0; + bindings2 <- + betree_list_push_front_fwd_back bindings1 (key,v); + betree_node_lookup_mut_in_bindings_back key bindings + bindings2 + od + | BetreeMessageDelete => + do + bindings1 <- betree_list_pop_front_back bindings0; + betree_node_lookup_mut_in_bindings_back key bindings + bindings1 + od + | BetreeMessageUpsert s => + (let + (_,i) = hd + in + do + v <- betree_upsert_update_fwd (SOME i) s; + bindings1 <- betree_list_pop_front_back bindings0; + bindings2 <- + betree_list_push_front_fwd_back bindings1 (key,v); + betree_node_lookup_mut_in_bindings_back key bindings + bindings2 + od) + od + else + case new_msg of + BetreeMessageInsert v => + do + bindings1 <- + betree_list_push_front_fwd_back bindings0 (key,v); + betree_node_lookup_mut_in_bindings_back key bindings + bindings1 + od + | BetreeMessageDelete => + betree_node_lookup_mut_in_bindings_back key bindings + bindings0 + | BetreeMessageUpsert s => + do + v <- betree_upsert_update_fwd NONE s; + bindings1 <- + betree_list_push_front_fwd_back bindings0 (key,v); + betree_node_lookup_mut_in_bindings_back key bindings + bindings1 + od + od + + [betree_node_apply_upserts_back_def] Definition + + ⊢ ∀msgs prev key st. + betree_node_apply_upserts_back msgs prev key st = + do + b <- betree_list_head_has_key_fwd msgs key; + if b then + do + msg <- betree_list_pop_front_fwd msgs; + (_,m) <<- msg; + case m of + BetreeMessageInsert i => Fail Failure + | BetreeMessageDelete => Fail Failure + | BetreeMessageUpsert s => + do + v <- betree_upsert_update_fwd prev s; + msgs0 <- betree_list_pop_front_back msgs; + betree_node_apply_upserts_back msgs0 (SOME v) key st + od + od + else + do + (_,v) <- core_option_option_unwrap_fwd prev st; + betree_list_push_front_fwd_back msgs + (key,BetreeMessageInsert v) + od + od + + [betree_node_apply_upserts_fwd_def] Definition + + ⊢ ∀msgs prev key st. + betree_node_apply_upserts_fwd msgs prev key st = + do + b <- betree_list_head_has_key_fwd msgs key; + if b then + do + msg <- betree_list_pop_front_fwd msgs; + (_,m) <<- msg; + case m of + BetreeMessageInsert i => Fail Failure + | BetreeMessageDelete => Fail Failure + | BetreeMessageUpsert s => + do + v <- betree_upsert_update_fwd prev s; + msgs0 <- betree_list_pop_front_back msgs; + betree_node_apply_upserts_fwd msgs0 (SOME v) key st + od + od + else + do + (st0,v) <- core_option_option_unwrap_fwd prev st; + monad_ignore_bind + (betree_list_push_front_fwd_back msgs + (key,BetreeMessageInsert v)) (Return (st0,v)) + od + od + + [betree_node_filter_messages_for_key_fwd_back_def] Definition + + ⊢ ∀key msgs. + betree_node_filter_messages_for_key_fwd_back key msgs = + case msgs of + BetreeListCons p l => + (let + (k,m) = p + in + if k = key then + do + msgs0 <- + betree_list_pop_front_back (BetreeListCons (k,m) l); + betree_node_filter_messages_for_key_fwd_back key msgs0 + od + else Return (BetreeListCons (k,m) l)) + | BetreeListNil => Return BetreeListNil + + [betree_node_id_counter_fresh_id_back_def] Definition + + ⊢ ∀self. + betree_node_id_counter_fresh_id_back self = + do + i <- + u64_add self.betree_node_id_counter_next_node_id + (int_to_u64 1); + Return <|betree_node_id_counter_next_node_id := i|> + od + + [betree_node_id_counter_fresh_id_fwd_def] Definition + + ⊢ ∀self. + betree_node_id_counter_fresh_id_fwd self = + monad_ignore_bind + (u64_add self.betree_node_id_counter_next_node_id + (int_to_u64 1)) + (Return self.betree_node_id_counter_next_node_id) + + [betree_node_id_counter_new_fwd_def] Definition + + ⊢ betree_node_id_counter_new_fwd = + Return <|betree_node_id_counter_next_node_id := int_to_u64 0|> + + [betree_node_lookup_back_def] Definition + + ⊢ ∀self key st. + betree_node_lookup_back self key st = + case self of + BetreeNodeInternal node => + do + (st0,msgs) <- + betree_load_internal_node_fwd node.betree_internal_id st; + pending <- + betree_node_lookup_first_message_for_key_fwd key msgs; + case pending of + BetreeListCons p l => + (let + (k,msg) = p + in + if k ≠ key then + monad_ignore_bind + (betree_node_lookup_first_message_for_key_back + key msgs (BetreeListCons (k,msg) l)) + do + node0 <- + betree_internal_lookup_in_children_back node + key st0; + Return (BetreeNodeInternal node0) + od + else + case msg of + BetreeMessageInsert v => + monad_ignore_bind + (betree_node_lookup_first_message_for_key_back + key msgs + (BetreeListCons (k,BetreeMessageInsert v) + l)) (Return (BetreeNodeInternal node)) + | BetreeMessageDelete => + monad_ignore_bind + (betree_node_lookup_first_message_for_key_back + key msgs + (BetreeListCons (k,BetreeMessageDelete) l)) + (Return (BetreeNodeInternal node)) + | BetreeMessageUpsert ufs => + do + (st1,v) <- + betree_internal_lookup_in_children_fwd node + key st0; + (st2,_) <- + betree_node_apply_upserts_fwd + (BetreeListCons + (k,BetreeMessageUpsert ufs) l) v key + st1; + node0 <- + betree_internal_lookup_in_children_back node + key st0; + pending0 <- + betree_node_apply_upserts_back + (BetreeListCons + (k,BetreeMessageUpsert ufs) l) v key + st1; + msgs0 <- + betree_node_lookup_first_message_for_key_back + key msgs pending0; + monad_ignore_bind + (betree_store_internal_node_fwd + node0.betree_internal_id msgs0 st2) + (Return (BetreeNodeInternal node0)) + od) + | BetreeListNil => + monad_ignore_bind + (betree_node_lookup_first_message_for_key_back key msgs + BetreeListNil) + do + node0 <- + betree_internal_lookup_in_children_back node key + st0; + Return (BetreeNodeInternal node0) + od + od + | BetreeNodeLeaf node' => + do + (_,bindings) <- + betree_load_leaf_node_fwd node'.betree_leaf_id st; + monad_ignore_bind + (betree_node_lookup_in_bindings_fwd key bindings) + (Return (BetreeNodeLeaf node')) + od + + [betree_node_lookup_first_message_after_key_back_def] Definition + + ⊢ ∀key msgs ret. + betree_node_lookup_first_message_after_key_back key msgs ret = + case msgs of + BetreeListCons p next_msgs => + (let + (k,m) = p + in + if k = key then + do + next_msgs0 <- + betree_node_lookup_first_message_after_key_back key + next_msgs ret; + Return (BetreeListCons (k,m) next_msgs0) + od + else Return ret) + | BetreeListNil => Return ret + + [betree_node_lookup_first_message_after_key_fwd_def] Definition + + ⊢ ∀key msgs. + betree_node_lookup_first_message_after_key_fwd key msgs = + case msgs of + BetreeListCons p next_msgs => + (let + (k,m) = p + in + if k = key then + betree_node_lookup_first_message_after_key_fwd key + next_msgs + else Return (BetreeListCons (k,m) next_msgs)) + | BetreeListNil => Return BetreeListNil + + [betree_node_lookup_first_message_for_key_back_def] Definition + + ⊢ ∀key msgs ret. + betree_node_lookup_first_message_for_key_back key msgs ret = + case msgs of + BetreeListCons x next_msgs => + (let + (i,m) = x + in + if u64_ge i key then Return ret + else + do + next_msgs0 <- + betree_node_lookup_first_message_for_key_back key + next_msgs ret; + Return (BetreeListCons (i,m) next_msgs0) + od) + | BetreeListNil => Return ret + + [betree_node_lookup_first_message_for_key_fwd_def] Definition + + ⊢ ∀key msgs. + betree_node_lookup_first_message_for_key_fwd key msgs = + case msgs of + BetreeListCons x next_msgs => + (let + (i,m) = x + in + if u64_ge i key then + Return (BetreeListCons (i,m) next_msgs) + else + betree_node_lookup_first_message_for_key_fwd key + next_msgs) + | BetreeListNil => Return BetreeListNil + + [betree_node_lookup_fwd_def] Definition + + ⊢ ∀self key st. + betree_node_lookup_fwd self key st = + case self of + BetreeNodeInternal node => + do + (st0,msgs) <- + betree_load_internal_node_fwd node.betree_internal_id st; + pending <- + betree_node_lookup_first_message_for_key_fwd key msgs; + case pending of + BetreeListCons p l => + (let + (k,msg) = p + in + if k ≠ key then + do + (st1,opt) <- + betree_internal_lookup_in_children_fwd node + key st0; + monad_ignore_bind + (betree_node_lookup_first_message_for_key_back + key msgs (BetreeListCons (k,msg) l)) + (Return (st1,opt)) + od + else + case msg of + BetreeMessageInsert v => + monad_ignore_bind + (betree_node_lookup_first_message_for_key_back + key msgs + (BetreeListCons (k,BetreeMessageInsert v) + l)) (Return (st0,SOME v)) + | BetreeMessageDelete => + monad_ignore_bind + (betree_node_lookup_first_message_for_key_back + key msgs + (BetreeListCons (k,BetreeMessageDelete) l)) + (Return (st0,NONE)) + | BetreeMessageUpsert ufs => + do + (st1,v) <- + betree_internal_lookup_in_children_fwd node + key st0; + (st2,v0) <- + betree_node_apply_upserts_fwd + (BetreeListCons + (k,BetreeMessageUpsert ufs) l) v key + st1; + node0 <- + betree_internal_lookup_in_children_back node + key st0; + pending0 <- + betree_node_apply_upserts_back + (BetreeListCons + (k,BetreeMessageUpsert ufs) l) v key + st1; + msgs0 <- + betree_node_lookup_first_message_for_key_back + key msgs pending0; + (st3,_) <- + betree_store_internal_node_fwd + node0.betree_internal_id msgs0 st2; + Return (st3,SOME v0) + od) + | BetreeListNil => + do + (st1,opt) <- + betree_internal_lookup_in_children_fwd node key st0; + monad_ignore_bind + (betree_node_lookup_first_message_for_key_back key + msgs BetreeListNil) (Return (st1,opt)) + od + od + | BetreeNodeLeaf node' => + do + (st0,bindings) <- + betree_load_leaf_node_fwd node'.betree_leaf_id st; + opt <- betree_node_lookup_in_bindings_fwd key bindings; + Return (st0,opt) + od + + [betree_node_lookup_in_bindings_fwd_def] Definition + + ⊢ ∀key bindings. + betree_node_lookup_in_bindings_fwd key bindings = + case bindings of + BetreeListCons hd tl => + (let + (i,i0) = hd + in + if i = key then Return (SOME i0) + else if u64_gt i key then Return NONE + else betree_node_lookup_in_bindings_fwd key tl) + | BetreeListNil => Return NONE + + [betree_node_lookup_mut_in_bindings_back_def] Definition + + ⊢ ∀key bindings ret. + betree_node_lookup_mut_in_bindings_back key bindings ret = + case bindings of + BetreeListCons hd tl => + (let + (i,i0) = hd + in + if u64_ge i key then Return ret + else + do + tl0 <- + betree_node_lookup_mut_in_bindings_back key tl ret; + Return (BetreeListCons (i,i0) tl0) + od) + | BetreeListNil => Return ret + + [betree_node_lookup_mut_in_bindings_fwd_def] Definition + + ⊢ ∀key bindings. + betree_node_lookup_mut_in_bindings_fwd key bindings = + case bindings of + BetreeListCons hd tl => + (let + (i,i0) = hd + in + if u64_ge i key then Return (BetreeListCons (i,i0) tl) + else betree_node_lookup_mut_in_bindings_fwd key tl) + | BetreeListNil => Return BetreeListNil + + [betree_store_internal_node_fwd_def] Definition + + ⊢ ∀id content st. + betree_store_internal_node_fwd id content st = + do + (st0,_) <- betree_utils_store_internal_node_fwd id content st; + Return (st0,()) + od + + [betree_store_leaf_node_fwd_def] Definition + + ⊢ ∀id content st. + betree_store_leaf_node_fwd id content st = + do + (st0,_) <- betree_utils_store_leaf_node_fwd id content st; + Return (st0,()) + od + + [betree_upsert_update_fwd_def] Definition + + ⊢ ∀prev st. + betree_upsert_update_fwd prev st = + case prev of + NONE => + (case st of + BetreeUpsertFunStateAdd v => Return v + | BetreeUpsertFunStateSub i => Return (int_to_u64 0)) + | SOME prev0 => + case st of + BetreeUpsertFunStateAdd v => + do + margin <- u64_sub core_num_u64_max_c prev0; + if u64_ge margin v then u64_add prev0 v + else Return core_num_u64_max_c + od + | BetreeUpsertFunStateSub v' => + if u64_ge prev0 v' then u64_sub prev0 v' + else Return (int_to_u64 0) + + [core_num_u64_max_body_def] Definition + + ⊢ core_num_u64_max_body = Return (int_to_u64 18446744073709551615) + + [core_num_u64_max_c_def] Definition + + ⊢ core_num_u64_max_c = get_return_value core_num_u64_max_body + + [main_fwd_def] Definition + + ⊢ main_fwd = Return () + + +*) +end diff --git a/tests/hol4/betree/betreeMain_OpaqueScript.sml b/tests/hol4/betree/betreeMain_OpaqueScript.sml new file mode 100644 index 00000000..a6f0cf15 --- /dev/null +++ b/tests/hol4/betree/betreeMain_OpaqueScript.sml @@ -0,0 +1,26 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: opaque function definitions *) +open primitivesLib divDefLib +open betreeMain_TypesTheory + +val _ = new_theory "betreeMain_Opaque" + + +val _ = new_constant ("betree_utils_load_internal_node_fwd", + “:u64 -> state -> (state # (u64 # betree_message_t) betree_list_t) + result”) + +val _ = new_constant ("betree_utils_store_internal_node_fwd", + “:u64 -> (u64 # betree_message_t) betree_list_t -> state -> (state # unit) + result”) + +val _ = new_constant ("betree_utils_load_leaf_node_fwd", + “:u64 -> state -> (state # (u64 # u64) betree_list_t) result”) + +val _ = new_constant ("betree_utils_store_leaf_node_fwd", + “:u64 -> (u64 # u64) betree_list_t -> state -> (state # unit) result”) + +val _ = new_constant ("core_option_option_unwrap_fwd", + “:'t option -> state -> (state # 't) result”) + +val _ = export_theory () diff --git a/tests/hol4/betree/betreeMain_OpaqueTheory.sig b/tests/hol4/betree/betreeMain_OpaqueTheory.sig new file mode 100644 index 00000000..da7559a0 --- /dev/null +++ b/tests/hol4/betree/betreeMain_OpaqueTheory.sig @@ -0,0 +1,11 @@ +signature betreeMain_OpaqueTheory = +sig + type thm = Thm.thm + + val betreeMain_Opaque_grammars : type_grammar.grammar * term_grammar.grammar +(* + [betreeMain_Types] Parent theory of "betreeMain_Opaque" + + +*) +end diff --git a/tests/hol4/betree/betreeMain_TypesScript.sml b/tests/hol4/betree/betreeMain_TypesScript.sml new file mode 100644 index 00000000..c43421c2 --- /dev/null +++ b/tests/hol4/betree/betreeMain_TypesScript.sml @@ -0,0 +1,76 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: type definitions *) +open primitivesLib divDefLib + +val _ = new_theory "betreeMain_Types" + + +Datatype: + (** [betree_main::betree::List] *) + betree_list_t = | BetreeListCons 't betree_list_t | BetreeListNil +End + +Datatype: + (** [betree_main::betree::UpsertFunState] *) + betree_upsert_fun_state_t = + | BetreeUpsertFunStateAdd u64 + | BetreeUpsertFunStateSub u64 +End + +Datatype: + (** [betree_main::betree::Message] *) + betree_message_t = + | BetreeMessageInsert u64 + | BetreeMessageDelete + | BetreeMessageUpsert betree_upsert_fun_state_t +End + +Datatype: + (** [betree_main::betree::Leaf] *) + betree_leaf_t = <| betree_leaf_id : u64; betree_leaf_size : u64; |> +End + +Datatype: + (** [betree_main::betree::Node] *) + betree_node_t = + | BetreeNodeInternal betree_internal_t + | BetreeNodeLeaf betree_leaf_t + ; + + (** [betree_main::betree::Internal] *) + betree_internal_t = + <| + betree_internal_id : u64; + betree_internal_pivot : u64; + betree_internal_left : betree_node_t; + betree_internal_right : betree_node_t; + |> +End + +Datatype: + (** [betree_main::betree::Params] *) + betree_params_t = + <| + betree_params_min_flush_size : u64; betree_params_split_size : u64; + |> +End + +Datatype: + (** [betree_main::betree::NodeIdCounter] *) + betree_node_id_counter_t = <| betree_node_id_counter_next_node_id : u64; |> +End + +Datatype: + (** [betree_main::betree::BeTree] *) + betree_be_tree_t = + <| + betree_be_tree_params : betree_params_t; + betree_be_tree_node_id_cnt : betree_node_id_counter_t; + betree_be_tree_root : betree_node_t; + |> +End + +(** The state type used in the state-error monad *) +val _ = new_type ("state", 0) + +val _ = export_theory () diff --git a/tests/hol4/betree/betreeMain_TypesTheory.sig b/tests/hol4/betree/betreeMain_TypesTheory.sig new file mode 100644 index 00000000..5cbe4c6b --- /dev/null +++ b/tests/hol4/betree/betreeMain_TypesTheory.sig @@ -0,0 +1,1751 @@ +signature betreeMain_TypesTheory = +sig + type thm = Thm.thm + + (* Definitions *) + val betree_be_tree_t_TY_DEF : thm + val betree_be_tree_t_case_def : thm + val betree_be_tree_t_size_def : thm + val betree_internal_t_TY_DEF : thm + val betree_internal_t_case_def : thm + val betree_leaf_t_TY_DEF : thm + val betree_leaf_t_case_def : thm + val betree_leaf_t_size_def : thm + val betree_list_t_TY_DEF : thm + val betree_list_t_case_def : thm + val betree_list_t_size_def : thm + val betree_message_t_TY_DEF : thm + val betree_message_t_case_def : thm + val betree_message_t_size_def : thm + val betree_node_id_counter_t_TY_DEF : thm + val betree_node_id_counter_t_case_def : thm + val betree_node_id_counter_t_size_def : thm + val betree_node_t_TY_DEF : thm + val betree_node_t_case_def : thm + val betree_node_t_size_def : thm + val betree_params_t_TY_DEF : thm + val betree_params_t_case_def : thm + val betree_params_t_size_def : thm + val betree_upsert_fun_state_t_TY_DEF : thm + val betree_upsert_fun_state_t_case_def : thm + val betree_upsert_fun_state_t_size_def : thm + val recordtype_betree_be_tree_t_seldef_betree_be_tree_node_id_cnt_def : thm + val recordtype_betree_be_tree_t_seldef_betree_be_tree_node_id_cnt_fupd_def : thm + val recordtype_betree_be_tree_t_seldef_betree_be_tree_params_def : thm + val recordtype_betree_be_tree_t_seldef_betree_be_tree_params_fupd_def : thm + val recordtype_betree_be_tree_t_seldef_betree_be_tree_root_def : thm + val recordtype_betree_be_tree_t_seldef_betree_be_tree_root_fupd_def : thm + val recordtype_betree_internal_t_seldef_betree_internal_id_def : thm + val recordtype_betree_internal_t_seldef_betree_internal_id_fupd_def : thm + val recordtype_betree_internal_t_seldef_betree_internal_left_def : thm + val recordtype_betree_internal_t_seldef_betree_internal_left_fupd_def : thm + val recordtype_betree_internal_t_seldef_betree_internal_pivot_def : thm + val recordtype_betree_internal_t_seldef_betree_internal_pivot_fupd_def : thm + val recordtype_betree_internal_t_seldef_betree_internal_right_def : thm + val recordtype_betree_internal_t_seldef_betree_internal_right_fupd_def : thm + val recordtype_betree_leaf_t_seldef_betree_leaf_id_def : thm + val recordtype_betree_leaf_t_seldef_betree_leaf_id_fupd_def : thm + val recordtype_betree_leaf_t_seldef_betree_leaf_size_def : thm + val recordtype_betree_leaf_t_seldef_betree_leaf_size_fupd_def : thm + val recordtype_betree_node_id_counter_t_seldef_betree_node_id_counter_next_node_id_def : thm + val recordtype_betree_node_id_counter_t_seldef_betree_node_id_counter_next_node_id_fupd_def : thm + val recordtype_betree_params_t_seldef_betree_params_min_flush_size_def : thm + val recordtype_betree_params_t_seldef_betree_params_min_flush_size_fupd_def : thm + val recordtype_betree_params_t_seldef_betree_params_split_size_def : thm + val recordtype_betree_params_t_seldef_betree_params_split_size_fupd_def : thm + + (* Theorems *) + val EXISTS_betree_be_tree_t : thm + val EXISTS_betree_internal_t : thm + val EXISTS_betree_leaf_t : thm + val EXISTS_betree_node_id_counter_t : thm + val EXISTS_betree_params_t : thm + val FORALL_betree_be_tree_t : thm + val FORALL_betree_internal_t : thm + val FORALL_betree_leaf_t : thm + val FORALL_betree_node_id_counter_t : thm + val FORALL_betree_params_t : thm + val betree_be_tree_t_11 : thm + val betree_be_tree_t_Axiom : thm + val betree_be_tree_t_accessors : thm + val betree_be_tree_t_accfupds : thm + val betree_be_tree_t_case_cong : thm + val betree_be_tree_t_case_eq : thm + val betree_be_tree_t_component_equality : thm + val betree_be_tree_t_fn_updates : thm + val betree_be_tree_t_fupdcanon : thm + val betree_be_tree_t_fupdcanon_comp : thm + val betree_be_tree_t_fupdfupds : thm + val betree_be_tree_t_fupdfupds_comp : thm + val betree_be_tree_t_induction : thm + val betree_be_tree_t_literal_11 : thm + val betree_be_tree_t_literal_nchotomy : thm + val betree_be_tree_t_nchotomy : thm + val betree_be_tree_t_updates_eq_literal : thm + val betree_internal_t_11 : thm + val betree_internal_t_Axiom : thm + val betree_internal_t_accessors : thm + val betree_internal_t_accfupds : thm + val betree_internal_t_case_cong : thm + val betree_internal_t_case_eq : thm + val betree_internal_t_component_equality : thm + val betree_internal_t_fn_updates : thm + val betree_internal_t_fupdcanon : thm + val betree_internal_t_fupdcanon_comp : thm + val betree_internal_t_fupdfupds : thm + val betree_internal_t_fupdfupds_comp : thm + val betree_internal_t_induction : thm + val betree_internal_t_literal_11 : thm + val betree_internal_t_literal_nchotomy : thm + val betree_internal_t_nchotomy : thm + val betree_internal_t_updates_eq_literal : thm + val betree_leaf_t_11 : thm + val betree_leaf_t_Axiom : thm + val betree_leaf_t_accessors : thm + val betree_leaf_t_accfupds : thm + val betree_leaf_t_case_cong : thm + val betree_leaf_t_case_eq : thm + val betree_leaf_t_component_equality : thm + val betree_leaf_t_fn_updates : thm + val betree_leaf_t_fupdcanon : thm + val betree_leaf_t_fupdcanon_comp : thm + val betree_leaf_t_fupdfupds : thm + val betree_leaf_t_fupdfupds_comp : thm + val betree_leaf_t_induction : thm + val betree_leaf_t_literal_11 : thm + val betree_leaf_t_literal_nchotomy : thm + val betree_leaf_t_nchotomy : thm + val betree_leaf_t_updates_eq_literal : thm + val betree_list_t_11 : thm + val betree_list_t_Axiom : thm + val betree_list_t_case_cong : thm + val betree_list_t_case_eq : thm + val betree_list_t_distinct : thm + val betree_list_t_induction : thm + val betree_list_t_nchotomy : thm + val betree_message_t_11 : thm + val betree_message_t_Axiom : thm + val betree_message_t_case_cong : thm + val betree_message_t_case_eq : thm + val betree_message_t_distinct : thm + val betree_message_t_induction : thm + val betree_message_t_nchotomy : thm + val betree_node_id_counter_t_11 : thm + val betree_node_id_counter_t_Axiom : thm + val betree_node_id_counter_t_accessors : thm + val betree_node_id_counter_t_accfupds : thm + val betree_node_id_counter_t_case_cong : thm + val betree_node_id_counter_t_case_eq : thm + val betree_node_id_counter_t_component_equality : thm + val betree_node_id_counter_t_fn_updates : thm + val betree_node_id_counter_t_fupdfupds : thm + val betree_node_id_counter_t_fupdfupds_comp : thm + val betree_node_id_counter_t_induction : thm + val betree_node_id_counter_t_literal_11 : thm + val betree_node_id_counter_t_literal_nchotomy : thm + val betree_node_id_counter_t_nchotomy : thm + val betree_node_id_counter_t_updates_eq_literal : thm + val betree_node_t_11 : thm + val betree_node_t_Axiom : thm + val betree_node_t_case_cong : thm + val betree_node_t_case_eq : thm + val betree_node_t_distinct : thm + val betree_node_t_induction : thm + val betree_node_t_nchotomy : thm + val betree_params_t_11 : thm + val betree_params_t_Axiom : thm + val betree_params_t_accessors : thm + val betree_params_t_accfupds : thm + val betree_params_t_case_cong : thm + val betree_params_t_case_eq : thm + val betree_params_t_component_equality : thm + val betree_params_t_fn_updates : thm + val betree_params_t_fupdcanon : thm + val betree_params_t_fupdcanon_comp : thm + val betree_params_t_fupdfupds : thm + val betree_params_t_fupdfupds_comp : thm + val betree_params_t_induction : thm + val betree_params_t_literal_11 : thm + val betree_params_t_literal_nchotomy : thm + val betree_params_t_nchotomy : thm + val betree_params_t_updates_eq_literal : thm + val betree_upsert_fun_state_t_11 : thm + val betree_upsert_fun_state_t_Axiom : thm + val betree_upsert_fun_state_t_case_cong : thm + val betree_upsert_fun_state_t_case_eq : thm + val betree_upsert_fun_state_t_distinct : thm + val betree_upsert_fun_state_t_induction : thm + val betree_upsert_fun_state_t_nchotomy : thm + val datatype_betree_be_tree_t : thm + val datatype_betree_leaf_t : thm + val datatype_betree_list_t : thm + val datatype_betree_message_t : thm + val datatype_betree_node_id_counter_t : thm + val datatype_betree_node_t : thm + val datatype_betree_params_t : thm + val datatype_betree_upsert_fun_state_t : thm + + val betreeMain_Types_grammars : type_grammar.grammar * term_grammar.grammar +(* + [divDef] Parent theory of "betreeMain_Types" + + [betree_be_tree_t_TY_DEF] Definition + + ⊢ ∃rep. + TYPE_DEFINITION + (λa0'. + ∀ $var$('betree_be_tree_t'). + (∀a0'. + (∃a0 a1 a2. + a0' = + (λa0 a1 a2. + ind_type$CONSTR 0 (a0,a1,a2) + (λn. ind_type$BOTTOM)) a0 a1 a2) ⇒ + $var$('betree_be_tree_t') a0') ⇒ + $var$('betree_be_tree_t') a0') rep + + [betree_be_tree_t_case_def] Definition + + ⊢ ∀a0 a1 a2 f. + betree_be_tree_t_CASE (betree_be_tree_t a0 a1 a2) f = f a0 a1 a2 + + [betree_be_tree_t_size_def] Definition + + ⊢ ∀a0 a1 a2. + betree_be_tree_t_size (betree_be_tree_t a0 a1 a2) = + 1 + + (betree_params_t_size a0 + + (betree_node_id_counter_t_size a1 + betree_node_t_size a2)) + + [betree_internal_t_TY_DEF] Definition + + ⊢ ∃rep. + TYPE_DEFINITION + (λa1'. + ∀ $var$('betree_node_t') $var$('betree_internal_t'). + (∀a0'. + (∃a. a0' = + (λa. + ind_type$CONSTR 0 (ARB,ARB,ARB) + (ind_type$FCONS a (λn. ind_type$BOTTOM))) + a ∧ $var$('betree_internal_t') a) ∨ + (∃a. a0' = + (λa. + ind_type$CONSTR (SUC 0) (a,ARB,ARB) + (λn. ind_type$BOTTOM)) a) ⇒ + $var$('betree_node_t') a0') ∧ + (∀a1'. + (∃a0 a1 a2 a3. + a1' = + (λa0 a1 a2 a3. + ind_type$CONSTR (SUC (SUC 0)) (ARB,a0,a1) + (ind_type$FCONS a2 + (ind_type$FCONS a3 (λn. ind_type$BOTTOM)))) + a0 a1 a2 a3 ∧ $var$('betree_node_t') a2 ∧ + $var$('betree_node_t') a3) ⇒ + $var$('betree_internal_t') a1') ⇒ + $var$('betree_internal_t') a1') rep + + [betree_internal_t_case_def] Definition + + ⊢ ∀a0 a1 a2 a3 f. + betree_internal_t_CASE (betree_internal_t a0 a1 a2 a3) f = + f a0 a1 a2 a3 + + [betree_leaf_t_TY_DEF] Definition + + ⊢ ∃rep. + TYPE_DEFINITION + (λa0'. + ∀ $var$('betree_leaf_t'). + (∀a0'. + (∃a0 a1. + a0' = + (λa0 a1. + ind_type$CONSTR 0 (a0,a1) + (λn. ind_type$BOTTOM)) a0 a1) ⇒ + $var$('betree_leaf_t') a0') ⇒ + $var$('betree_leaf_t') a0') rep + + [betree_leaf_t_case_def] Definition + + ⊢ ∀a0 a1 f. betree_leaf_t_CASE (betree_leaf_t a0 a1) f = f a0 a1 + + [betree_leaf_t_size_def] Definition + + ⊢ ∀a0 a1. betree_leaf_t_size (betree_leaf_t a0 a1) = 1 + + [betree_list_t_TY_DEF] Definition + + ⊢ ∃rep. + TYPE_DEFINITION + (λa0'. + ∀ $var$('betree_list_t'). + (∀a0'. + (∃a0 a1. + a0' = + (λa0 a1. + ind_type$CONSTR 0 a0 + (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) + a0 a1 ∧ $var$('betree_list_t') a1) ∨ + a0' = + ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒ + $var$('betree_list_t') a0') ⇒ + $var$('betree_list_t') a0') rep + + [betree_list_t_case_def] Definition + + ⊢ (∀a0 a1 f v. + betree_list_t_CASE (BetreeListCons a0 a1) f v = f a0 a1) ∧ + ∀f v. betree_list_t_CASE BetreeListNil f v = v + + [betree_list_t_size_def] Definition + + ⊢ (∀f a0 a1. + betree_list_t_size f (BetreeListCons a0 a1) = + 1 + (f a0 + betree_list_t_size f a1)) ∧ + ∀f. betree_list_t_size f BetreeListNil = 0 + + [betree_message_t_TY_DEF] Definition + + ⊢ ∃rep. + TYPE_DEFINITION + (λa0. + ∀ $var$('betree_message_t'). + (∀a0. + (∃a. a0 = + (λa. + ind_type$CONSTR 0 (a,ARB) + (λn. ind_type$BOTTOM)) a) ∨ + a0 = + ind_type$CONSTR (SUC 0) (ARB,ARB) + (λn. ind_type$BOTTOM) ∨ + (∃a. a0 = + (λa. + ind_type$CONSTR (SUC (SUC 0)) (ARB,a) + (λn. ind_type$BOTTOM)) a) ⇒ + $var$('betree_message_t') a0) ⇒ + $var$('betree_message_t') a0) rep + + [betree_message_t_case_def] Definition + + ⊢ (∀a f v f1. + betree_message_t_CASE (BetreeMessageInsert a) f v f1 = f a) ∧ + (∀f v f1. betree_message_t_CASE BetreeMessageDelete f v f1 = v) ∧ + ∀a f v f1. + betree_message_t_CASE (BetreeMessageUpsert a) f v f1 = f1 a + + [betree_message_t_size_def] Definition + + ⊢ (∀a. betree_message_t_size (BetreeMessageInsert a) = 1) ∧ + betree_message_t_size BetreeMessageDelete = 0 ∧ + ∀a. betree_message_t_size (BetreeMessageUpsert a) = + 1 + betree_upsert_fun_state_t_size a + + [betree_node_id_counter_t_TY_DEF] Definition + + ⊢ ∃rep. + TYPE_DEFINITION + (λa0. + ∀ $var$('betree_node_id_counter_t'). + (∀a0. + (∃a. a0 = + (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM)) + a) ⇒ + $var$('betree_node_id_counter_t') a0) ⇒ + $var$('betree_node_id_counter_t') a0) rep + + [betree_node_id_counter_t_case_def] Definition + + ⊢ ∀a f. + betree_node_id_counter_t_CASE (betree_node_id_counter_t a) f = + f a + + [betree_node_id_counter_t_size_def] Definition + + ⊢ ∀a. betree_node_id_counter_t_size (betree_node_id_counter_t a) = 1 + + [betree_node_t_TY_DEF] Definition + + ⊢ ∃rep. + TYPE_DEFINITION + (λa0'. + ∀ $var$('betree_node_t') $var$('betree_internal_t'). + (∀a0'. + (∃a. a0' = + (λa. + ind_type$CONSTR 0 (ARB,ARB,ARB) + (ind_type$FCONS a (λn. ind_type$BOTTOM))) + a ∧ $var$('betree_internal_t') a) ∨ + (∃a. a0' = + (λa. + ind_type$CONSTR (SUC 0) (a,ARB,ARB) + (λn. ind_type$BOTTOM)) a) ⇒ + $var$('betree_node_t') a0') ∧ + (∀a1'. + (∃a0 a1 a2 a3. + a1' = + (λa0 a1 a2 a3. + ind_type$CONSTR (SUC (SUC 0)) (ARB,a0,a1) + (ind_type$FCONS a2 + (ind_type$FCONS a3 (λn. ind_type$BOTTOM)))) + a0 a1 a2 a3 ∧ $var$('betree_node_t') a2 ∧ + $var$('betree_node_t') a3) ⇒ + $var$('betree_internal_t') a1') ⇒ + $var$('betree_node_t') a0') rep + + [betree_node_t_case_def] Definition + + ⊢ (∀a f f1. betree_node_t_CASE (BetreeNodeInternal a) f f1 = f a) ∧ + ∀a f f1. betree_node_t_CASE (BetreeNodeLeaf a) f f1 = f1 a + + [betree_node_t_size_def] Definition + + ⊢ (∀a. betree_node_t_size (BetreeNodeInternal a) = + 1 + betree_internal_t_size a) ∧ + (∀a. betree_node_t_size (BetreeNodeLeaf a) = + 1 + betree_leaf_t_size a) ∧ + ∀a0 a1 a2 a3. + betree_internal_t_size (betree_internal_t a0 a1 a2 a3) = + 1 + (betree_node_t_size a2 + betree_node_t_size a3) + + [betree_params_t_TY_DEF] Definition + + ⊢ ∃rep. + TYPE_DEFINITION + (λa0'. + ∀ $var$('betree_params_t'). + (∀a0'. + (∃a0 a1. + a0' = + (λa0 a1. + ind_type$CONSTR 0 (a0,a1) + (λn. ind_type$BOTTOM)) a0 a1) ⇒ + $var$('betree_params_t') a0') ⇒ + $var$('betree_params_t') a0') rep + + [betree_params_t_case_def] Definition + + ⊢ ∀a0 a1 f. betree_params_t_CASE (betree_params_t a0 a1) f = f a0 a1 + + [betree_params_t_size_def] Definition + + ⊢ ∀a0 a1. betree_params_t_size (betree_params_t a0 a1) = 1 + + [betree_upsert_fun_state_t_TY_DEF] Definition + + ⊢ ∃rep. + TYPE_DEFINITION + (λa0. + ∀ $var$('betree_upsert_fun_state_t'). + (∀a0. + (∃a. a0 = + (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM)) + a) ∨ + (∃a. a0 = + (λa. + ind_type$CONSTR (SUC 0) a + (λn. ind_type$BOTTOM)) a) ⇒ + $var$('betree_upsert_fun_state_t') a0) ⇒ + $var$('betree_upsert_fun_state_t') a0) rep + + [betree_upsert_fun_state_t_case_def] Definition + + ⊢ (∀a f f1. + betree_upsert_fun_state_t_CASE (BetreeUpsertFunStateAdd a) f f1 = + f a) ∧ + ∀a f f1. + betree_upsert_fun_state_t_CASE (BetreeUpsertFunStateSub a) f f1 = + f1 a + + [betree_upsert_fun_state_t_size_def] Definition + + ⊢ (∀a. betree_upsert_fun_state_t_size (BetreeUpsertFunStateAdd a) = 1) ∧ + ∀a. betree_upsert_fun_state_t_size (BetreeUpsertFunStateSub a) = 1 + + [recordtype_betree_be_tree_t_seldef_betree_be_tree_node_id_cnt_def] Definition + + ⊢ ∀b b0 b1. + (betree_be_tree_t b b0 b1).betree_be_tree_node_id_cnt = b0 + + [recordtype_betree_be_tree_t_seldef_betree_be_tree_node_id_cnt_fupd_def] Definition + + ⊢ ∀f b b0 b1. + betree_be_tree_t b b0 b1 with + betree_be_tree_node_id_cnt updated_by f = + betree_be_tree_t b (f b0) b1 + + [recordtype_betree_be_tree_t_seldef_betree_be_tree_params_def] Definition + + ⊢ ∀b b0 b1. (betree_be_tree_t b b0 b1).betree_be_tree_params = b + + [recordtype_betree_be_tree_t_seldef_betree_be_tree_params_fupd_def] Definition + + ⊢ ∀f b b0 b1. + betree_be_tree_t b b0 b1 with betree_be_tree_params updated_by f = + betree_be_tree_t (f b) b0 b1 + + [recordtype_betree_be_tree_t_seldef_betree_be_tree_root_def] Definition + + ⊢ ∀b b0 b1. (betree_be_tree_t b b0 b1).betree_be_tree_root = b1 + + [recordtype_betree_be_tree_t_seldef_betree_be_tree_root_fupd_def] Definition + + ⊢ ∀f b b0 b1. + betree_be_tree_t b b0 b1 with betree_be_tree_root updated_by f = + betree_be_tree_t b b0 (f b1) + + [recordtype_betree_internal_t_seldef_betree_internal_id_def] Definition + + ⊢ ∀u u0 b b0. (betree_internal_t u u0 b b0).betree_internal_id = u + + [recordtype_betree_internal_t_seldef_betree_internal_id_fupd_def] Definition + + ⊢ ∀f u u0 b b0. + betree_internal_t u u0 b b0 with betree_internal_id updated_by f = + betree_internal_t (f u) u0 b b0 + + [recordtype_betree_internal_t_seldef_betree_internal_left_def] Definition + + ⊢ ∀u u0 b b0. (betree_internal_t u u0 b b0).betree_internal_left = b + + [recordtype_betree_internal_t_seldef_betree_internal_left_fupd_def] Definition + + ⊢ ∀f u u0 b b0. + betree_internal_t u u0 b b0 with + betree_internal_left updated_by f = + betree_internal_t u u0 (f b) b0 + + [recordtype_betree_internal_t_seldef_betree_internal_pivot_def] Definition + + ⊢ ∀u u0 b b0. + (betree_internal_t u u0 b b0).betree_internal_pivot = u0 + + [recordtype_betree_internal_t_seldef_betree_internal_pivot_fupd_def] Definition + + ⊢ ∀f u u0 b b0. + betree_internal_t u u0 b b0 with + betree_internal_pivot updated_by f = + betree_internal_t u (f u0) b b0 + + [recordtype_betree_internal_t_seldef_betree_internal_right_def] Definition + + ⊢ ∀u u0 b b0. + (betree_internal_t u u0 b b0).betree_internal_right = b0 + + [recordtype_betree_internal_t_seldef_betree_internal_right_fupd_def] Definition + + ⊢ ∀f u u0 b b0. + betree_internal_t u u0 b b0 with + betree_internal_right updated_by f = + betree_internal_t u u0 b (f b0) + + [recordtype_betree_leaf_t_seldef_betree_leaf_id_def] Definition + + ⊢ ∀u u0. (betree_leaf_t u u0).betree_leaf_id = u + + [recordtype_betree_leaf_t_seldef_betree_leaf_id_fupd_def] Definition + + ⊢ ∀f u u0. + betree_leaf_t u u0 with betree_leaf_id updated_by f = + betree_leaf_t (f u) u0 + + [recordtype_betree_leaf_t_seldef_betree_leaf_size_def] Definition + + ⊢ ∀u u0. (betree_leaf_t u u0).betree_leaf_size = u0 + + [recordtype_betree_leaf_t_seldef_betree_leaf_size_fupd_def] Definition + + ⊢ ∀f u u0. + betree_leaf_t u u0 with betree_leaf_size updated_by f = + betree_leaf_t u (f u0) + + [recordtype_betree_node_id_counter_t_seldef_betree_node_id_counter_next_node_id_def] Definition + + ⊢ ∀u. (betree_node_id_counter_t u). + betree_node_id_counter_next_node_id = + u + + [recordtype_betree_node_id_counter_t_seldef_betree_node_id_counter_next_node_id_fupd_def] Definition + + ⊢ ∀f u. + betree_node_id_counter_t u with + betree_node_id_counter_next_node_id updated_by f = + betree_node_id_counter_t (f u) + + [recordtype_betree_params_t_seldef_betree_params_min_flush_size_def] Definition + + ⊢ ∀u u0. (betree_params_t u u0).betree_params_min_flush_size = u + + [recordtype_betree_params_t_seldef_betree_params_min_flush_size_fupd_def] Definition + + ⊢ ∀f u u0. + betree_params_t u u0 with + betree_params_min_flush_size updated_by f = + betree_params_t (f u) u0 + + [recordtype_betree_params_t_seldef_betree_params_split_size_def] Definition + + ⊢ ∀u u0. (betree_params_t u u0).betree_params_split_size = u0 + + [recordtype_betree_params_t_seldef_betree_params_split_size_fupd_def] Definition + + ⊢ ∀f u u0. + betree_params_t u u0 with betree_params_split_size updated_by f = + betree_params_t u (f u0) + + [EXISTS_betree_be_tree_t] Theorem + + ⊢ ∀P. (∃b. P b) ⇔ + ∃b2 b1 b0. + P + <|betree_be_tree_params := b2; + betree_be_tree_node_id_cnt := b1; + betree_be_tree_root := b0|> + + [EXISTS_betree_internal_t] Theorem + + ⊢ ∀P. (∃b. P b) ⇔ + ∃u0 u b1 b0. + P + <|betree_internal_id := u0; betree_internal_pivot := u; + betree_internal_left := b1; betree_internal_right := b0|> + + [EXISTS_betree_leaf_t] Theorem + + ⊢ ∀P. (∃b. P b) ⇔ + ∃u0 u. P <|betree_leaf_id := u0; betree_leaf_size := u|> + + [EXISTS_betree_node_id_counter_t] Theorem + + ⊢ ∀P. (∃b. P b) ⇔ ∃u. P <|betree_node_id_counter_next_node_id := u|> + + [EXISTS_betree_params_t] Theorem + + ⊢ ∀P. (∃b. P b) ⇔ + ∃u0 u. + P + <|betree_params_min_flush_size := u0; + betree_params_split_size := u|> + + [FORALL_betree_be_tree_t] Theorem + + ⊢ ∀P. (∀b. P b) ⇔ + ∀b2 b1 b0. + P + <|betree_be_tree_params := b2; + betree_be_tree_node_id_cnt := b1; + betree_be_tree_root := b0|> + + [FORALL_betree_internal_t] Theorem + + ⊢ ∀P. (∀b. P b) ⇔ + ∀u0 u b1 b0. + P + <|betree_internal_id := u0; betree_internal_pivot := u; + betree_internal_left := b1; betree_internal_right := b0|> + + [FORALL_betree_leaf_t] Theorem + + ⊢ ∀P. (∀b. P b) ⇔ + ∀u0 u. P <|betree_leaf_id := u0; betree_leaf_size := u|> + + [FORALL_betree_node_id_counter_t] Theorem + + ⊢ ∀P. (∀b. P b) ⇔ ∀u. P <|betree_node_id_counter_next_node_id := u|> + + [FORALL_betree_params_t] Theorem + + ⊢ ∀P. (∀b. P b) ⇔ + ∀u0 u. + P + <|betree_params_min_flush_size := u0; + betree_params_split_size := u|> + + [betree_be_tree_t_11] Theorem + + ⊢ ∀a0 a1 a2 a0' a1' a2'. + betree_be_tree_t a0 a1 a2 = betree_be_tree_t a0' a1' a2' ⇔ + a0 = a0' ∧ a1 = a1' ∧ a2 = a2' + + [betree_be_tree_t_Axiom] Theorem + + ⊢ ∀f. ∃fn. ∀a0 a1 a2. fn (betree_be_tree_t a0 a1 a2) = f a0 a1 a2 + + [betree_be_tree_t_accessors] Theorem + + ⊢ (∀b b0 b1. (betree_be_tree_t b b0 b1).betree_be_tree_params = b) ∧ + (∀b b0 b1. + (betree_be_tree_t b b0 b1).betree_be_tree_node_id_cnt = b0) ∧ + ∀b b0 b1. (betree_be_tree_t b b0 b1).betree_be_tree_root = b1 + + [betree_be_tree_t_accfupds] Theorem + + ⊢ (∀f b. + (b with betree_be_tree_node_id_cnt updated_by f). + betree_be_tree_params = + b.betree_be_tree_params) ∧ + (∀f b. + (b with betree_be_tree_root updated_by f).betree_be_tree_params = + b.betree_be_tree_params) ∧ + (∀f b. + (b with betree_be_tree_params updated_by f). + betree_be_tree_node_id_cnt = + b.betree_be_tree_node_id_cnt) ∧ + (∀f b. + (b with betree_be_tree_root updated_by f). + betree_be_tree_node_id_cnt = + b.betree_be_tree_node_id_cnt) ∧ + (∀f b. + (b with betree_be_tree_params updated_by f).betree_be_tree_root = + b.betree_be_tree_root) ∧ + (∀f b. + (b with betree_be_tree_node_id_cnt updated_by f). + betree_be_tree_root = + b.betree_be_tree_root) ∧ + (∀f b. + (b with betree_be_tree_params updated_by f). + betree_be_tree_params = + f b.betree_be_tree_params) ∧ + (∀f b. + (b with betree_be_tree_node_id_cnt updated_by f). + betree_be_tree_node_id_cnt = + f b.betree_be_tree_node_id_cnt) ∧ + ∀f b. + (b with betree_be_tree_root updated_by f).betree_be_tree_root = + f b.betree_be_tree_root + + [betree_be_tree_t_case_cong] Theorem + + ⊢ ∀M M' f. + M = M' ∧ + (∀a0 a1 a2. + M' = betree_be_tree_t a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒ + betree_be_tree_t_CASE M f = betree_be_tree_t_CASE M' f' + + [betree_be_tree_t_case_eq] Theorem + + ⊢ betree_be_tree_t_CASE x f = v ⇔ + ∃b b0 b1. x = betree_be_tree_t b b0 b1 ∧ f b b0 b1 = v + + [betree_be_tree_t_component_equality] Theorem + + ⊢ ∀b1 b2. + b1 = b2 ⇔ + b1.betree_be_tree_params = b2.betree_be_tree_params ∧ + b1.betree_be_tree_node_id_cnt = b2.betree_be_tree_node_id_cnt ∧ + b1.betree_be_tree_root = b2.betree_be_tree_root + + [betree_be_tree_t_fn_updates] Theorem + + ⊢ (∀f b b0 b1. + betree_be_tree_t b b0 b1 with betree_be_tree_params updated_by f = + betree_be_tree_t (f b) b0 b1) ∧ + (∀f b b0 b1. + betree_be_tree_t b b0 b1 with + betree_be_tree_node_id_cnt updated_by f = + betree_be_tree_t b (f b0) b1) ∧ + ∀f b b0 b1. + betree_be_tree_t b b0 b1 with betree_be_tree_root updated_by f = + betree_be_tree_t b b0 (f b1) + + [betree_be_tree_t_fupdcanon] Theorem + + ⊢ (∀g f b. + b with + <|betree_be_tree_node_id_cnt updated_by f; + betree_be_tree_params updated_by g|> = + b with + <|betree_be_tree_params updated_by g; + betree_be_tree_node_id_cnt updated_by f|>) ∧ + (∀g f b. + b with + <|betree_be_tree_root updated_by f; + betree_be_tree_params updated_by g|> = + b with + <|betree_be_tree_params updated_by g; + betree_be_tree_root updated_by f|>) ∧ + ∀g f b. + b with + <|betree_be_tree_root updated_by f; + betree_be_tree_node_id_cnt updated_by g|> = + b with + <|betree_be_tree_node_id_cnt updated_by g; + betree_be_tree_root updated_by f|> + + [betree_be_tree_t_fupdcanon_comp] Theorem + + ⊢ ((∀g f. + betree_be_tree_node_id_cnt_fupd f ∘ + betree_be_tree_params_fupd g = + betree_be_tree_params_fupd g ∘ + betree_be_tree_node_id_cnt_fupd f) ∧ + ∀h g f. + betree_be_tree_node_id_cnt_fupd f ∘ + betree_be_tree_params_fupd g ∘ h = + betree_be_tree_params_fupd g ∘ + betree_be_tree_node_id_cnt_fupd f ∘ h) ∧ + ((∀g f. + betree_be_tree_root_fupd f ∘ betree_be_tree_params_fupd g = + betree_be_tree_params_fupd g ∘ betree_be_tree_root_fupd f) ∧ + ∀h g f. + betree_be_tree_root_fupd f ∘ betree_be_tree_params_fupd g ∘ h = + betree_be_tree_params_fupd g ∘ betree_be_tree_root_fupd f ∘ h) ∧ + (∀g f. + betree_be_tree_root_fupd f ∘ betree_be_tree_node_id_cnt_fupd g = + betree_be_tree_node_id_cnt_fupd g ∘ betree_be_tree_root_fupd f) ∧ + ∀h g f. + betree_be_tree_root_fupd f ∘ betree_be_tree_node_id_cnt_fupd g ∘ + h = + betree_be_tree_node_id_cnt_fupd g ∘ betree_be_tree_root_fupd f ∘ + h + + [betree_be_tree_t_fupdfupds] Theorem + + ⊢ (∀g f b. + b with + <|betree_be_tree_params updated_by f; + betree_be_tree_params updated_by g|> = + b with betree_be_tree_params updated_by f ∘ g) ∧ + (∀g f b. + b with + <|betree_be_tree_node_id_cnt updated_by f; + betree_be_tree_node_id_cnt updated_by g|> = + b with betree_be_tree_node_id_cnt updated_by f ∘ g) ∧ + ∀g f b. + b with + <|betree_be_tree_root updated_by f; + betree_be_tree_root updated_by g|> = + b with betree_be_tree_root updated_by f ∘ g + + [betree_be_tree_t_fupdfupds_comp] Theorem + + ⊢ ((∀g f. + betree_be_tree_params_fupd f ∘ betree_be_tree_params_fupd g = + betree_be_tree_params_fupd (f ∘ g)) ∧ + ∀h g f. + betree_be_tree_params_fupd f ∘ betree_be_tree_params_fupd g ∘ h = + betree_be_tree_params_fupd (f ∘ g) ∘ h) ∧ + ((∀g f. + betree_be_tree_node_id_cnt_fupd f ∘ + betree_be_tree_node_id_cnt_fupd g = + betree_be_tree_node_id_cnt_fupd (f ∘ g)) ∧ + ∀h g f. + betree_be_tree_node_id_cnt_fupd f ∘ + betree_be_tree_node_id_cnt_fupd g ∘ h = + betree_be_tree_node_id_cnt_fupd (f ∘ g) ∘ h) ∧ + (∀g f. + betree_be_tree_root_fupd f ∘ betree_be_tree_root_fupd g = + betree_be_tree_root_fupd (f ∘ g)) ∧ + ∀h g f. + betree_be_tree_root_fupd f ∘ betree_be_tree_root_fupd g ∘ h = + betree_be_tree_root_fupd (f ∘ g) ∘ h + + [betree_be_tree_t_induction] Theorem + + ⊢ ∀P. (∀b b0 b1. P (betree_be_tree_t b b0 b1)) ⇒ ∀b. P b + + [betree_be_tree_t_literal_11] Theorem + + ⊢ ∀b21 b11 b01 b22 b12 b02. + <|betree_be_tree_params := b21; + betree_be_tree_node_id_cnt := b11; betree_be_tree_root := b01|> = + <|betree_be_tree_params := b22; + betree_be_tree_node_id_cnt := b12; betree_be_tree_root := b02|> ⇔ + b21 = b22 ∧ b11 = b12 ∧ b01 = b02 + + [betree_be_tree_t_literal_nchotomy] Theorem + + ⊢ ∀b. ∃b2 b1 b0. + b = + <|betree_be_tree_params := b2; betree_be_tree_node_id_cnt := b1; + betree_be_tree_root := b0|> + + [betree_be_tree_t_nchotomy] Theorem + + ⊢ ∀bb. ∃b b0 b1. bb = betree_be_tree_t b b0 b1 + + [betree_be_tree_t_updates_eq_literal] Theorem + + ⊢ ∀b b2 b1 b0. + b with + <|betree_be_tree_params := b2; betree_be_tree_node_id_cnt := b1; + betree_be_tree_root := b0|> = + <|betree_be_tree_params := b2; betree_be_tree_node_id_cnt := b1; + betree_be_tree_root := b0|> + + [betree_internal_t_11] Theorem + + ⊢ ∀a0 a1 a2 a3 a0' a1' a2' a3'. + betree_internal_t a0 a1 a2 a3 = betree_internal_t a0' a1' a2' a3' ⇔ + a0 = a0' ∧ a1 = a1' ∧ a2 = a2' ∧ a3 = a3' + + [betree_internal_t_Axiom] Theorem + + ⊢ ∀f0 f1 f2. ∃fn0 fn1. + (∀a. fn0 (BetreeNodeInternal a) = f0 a (fn1 a)) ∧ + (∀a. fn0 (BetreeNodeLeaf a) = f1 a) ∧ + ∀a0 a1 a2 a3. + fn1 (betree_internal_t a0 a1 a2 a3) = + f2 a0 a1 a2 a3 (fn0 a2) (fn0 a3) + + [betree_internal_t_accessors] Theorem + + ⊢ (∀u u0 b b0. (betree_internal_t u u0 b b0).betree_internal_id = u) ∧ + (∀u u0 b b0. + (betree_internal_t u u0 b b0).betree_internal_pivot = u0) ∧ + (∀u u0 b b0. (betree_internal_t u u0 b b0).betree_internal_left = b) ∧ + ∀u u0 b b0. + (betree_internal_t u u0 b b0).betree_internal_right = b0 + + [betree_internal_t_accfupds] Theorem + + ⊢ (∀f b. + (b with betree_internal_pivot updated_by f).betree_internal_id = + b.betree_internal_id) ∧ + (∀f b. + (b with betree_internal_left updated_by f).betree_internal_id = + b.betree_internal_id) ∧ + (∀f b. + (b with betree_internal_right updated_by f).betree_internal_id = + b.betree_internal_id) ∧ + (∀f b. + (b with betree_internal_id updated_by f).betree_internal_pivot = + b.betree_internal_pivot) ∧ + (∀f b. + (b with betree_internal_left updated_by f).betree_internal_pivot = + b.betree_internal_pivot) ∧ + (∀f b. + (b with betree_internal_right updated_by f). + betree_internal_pivot = + b.betree_internal_pivot) ∧ + (∀f b. + (b with betree_internal_id updated_by f).betree_internal_left = + b.betree_internal_left) ∧ + (∀f b. + (b with betree_internal_pivot updated_by f).betree_internal_left = + b.betree_internal_left) ∧ + (∀f b. + (b with betree_internal_right updated_by f).betree_internal_left = + b.betree_internal_left) ∧ + (∀f b. + (b with betree_internal_id updated_by f).betree_internal_right = + b.betree_internal_right) ∧ + (∀f b. + (b with betree_internal_pivot updated_by f). + betree_internal_right = + b.betree_internal_right) ∧ + (∀f b. + (b with betree_internal_left updated_by f).betree_internal_right = + b.betree_internal_right) ∧ + (∀f b. + (b with betree_internal_id updated_by f).betree_internal_id = + f b.betree_internal_id) ∧ + (∀f b. + (b with betree_internal_pivot updated_by f). + betree_internal_pivot = + f b.betree_internal_pivot) ∧ + (∀f b. + (b with betree_internal_left updated_by f).betree_internal_left = + f b.betree_internal_left) ∧ + ∀f b. + (b with betree_internal_right updated_by f).betree_internal_right = + f b.betree_internal_right + + [betree_internal_t_case_cong] Theorem + + ⊢ ∀M M' f. + M = M' ∧ + (∀a0 a1 a2 a3. + M' = betree_internal_t a0 a1 a2 a3 ⇒ + f a0 a1 a2 a3 = f' a0 a1 a2 a3) ⇒ + betree_internal_t_CASE M f = betree_internal_t_CASE M' f' + + [betree_internal_t_case_eq] Theorem + + ⊢ betree_internal_t_CASE x f = v ⇔ + ∃u0 u b b0. x = betree_internal_t u0 u b b0 ∧ f u0 u b b0 = v + + [betree_internal_t_component_equality] Theorem + + ⊢ ∀b1 b2. + b1 = b2 ⇔ + b1.betree_internal_id = b2.betree_internal_id ∧ + b1.betree_internal_pivot = b2.betree_internal_pivot ∧ + b1.betree_internal_left = b2.betree_internal_left ∧ + b1.betree_internal_right = b2.betree_internal_right + + [betree_internal_t_fn_updates] Theorem + + ⊢ (∀f u u0 b b0. + betree_internal_t u u0 b b0 with betree_internal_id updated_by f = + betree_internal_t (f u) u0 b b0) ∧ + (∀f u u0 b b0. + betree_internal_t u u0 b b0 with + betree_internal_pivot updated_by f = + betree_internal_t u (f u0) b b0) ∧ + (∀f u u0 b b0. + betree_internal_t u u0 b b0 with + betree_internal_left updated_by f = + betree_internal_t u u0 (f b) b0) ∧ + ∀f u u0 b b0. + betree_internal_t u u0 b b0 with + betree_internal_right updated_by f = + betree_internal_t u u0 b (f b0) + + [betree_internal_t_fupdcanon] Theorem + + ⊢ (∀g f b. + b with + <|betree_internal_pivot updated_by f; + betree_internal_id updated_by g|> = + b with + <|betree_internal_id updated_by g; + betree_internal_pivot updated_by f|>) ∧ + (∀g f b. + b with + <|betree_internal_left updated_by f; + betree_internal_id updated_by g|> = + b with + <|betree_internal_id updated_by g; + betree_internal_left updated_by f|>) ∧ + (∀g f b. + b with + <|betree_internal_left updated_by f; + betree_internal_pivot updated_by g|> = + b with + <|betree_internal_pivot updated_by g; + betree_internal_left updated_by f|>) ∧ + (∀g f b. + b with + <|betree_internal_right updated_by f; + betree_internal_id updated_by g|> = + b with + <|betree_internal_id updated_by g; + betree_internal_right updated_by f|>) ∧ + (∀g f b. + b with + <|betree_internal_right updated_by f; + betree_internal_pivot updated_by g|> = + b with + <|betree_internal_pivot updated_by g; + betree_internal_right updated_by f|>) ∧ + ∀g f b. + b with + <|betree_internal_right updated_by f; + betree_internal_left updated_by g|> = + b with + <|betree_internal_left updated_by g; + betree_internal_right updated_by f|> + + [betree_internal_t_fupdcanon_comp] Theorem + + ⊢ ((∀g f. + betree_internal_pivot_fupd f ∘ betree_internal_id_fupd g = + betree_internal_id_fupd g ∘ betree_internal_pivot_fupd f) ∧ + ∀h g f. + betree_internal_pivot_fupd f ∘ betree_internal_id_fupd g ∘ h = + betree_internal_id_fupd g ∘ betree_internal_pivot_fupd f ∘ h) ∧ + ((∀g f. + betree_internal_left_fupd f ∘ betree_internal_id_fupd g = + betree_internal_id_fupd g ∘ betree_internal_left_fupd f) ∧ + ∀h g f. + betree_internal_left_fupd f ∘ betree_internal_id_fupd g ∘ h = + betree_internal_id_fupd g ∘ betree_internal_left_fupd f ∘ h) ∧ + ((∀g f. + betree_internal_left_fupd f ∘ betree_internal_pivot_fupd g = + betree_internal_pivot_fupd g ∘ betree_internal_left_fupd f) ∧ + ∀h g f. + betree_internal_left_fupd f ∘ betree_internal_pivot_fupd g ∘ h = + betree_internal_pivot_fupd g ∘ betree_internal_left_fupd f ∘ h) ∧ + ((∀g f. + betree_internal_right_fupd f ∘ betree_internal_id_fupd g = + betree_internal_id_fupd g ∘ betree_internal_right_fupd f) ∧ + ∀h g f. + betree_internal_right_fupd f ∘ betree_internal_id_fupd g ∘ h = + betree_internal_id_fupd g ∘ betree_internal_right_fupd f ∘ h) ∧ + ((∀g f. + betree_internal_right_fupd f ∘ betree_internal_pivot_fupd g = + betree_internal_pivot_fupd g ∘ betree_internal_right_fupd f) ∧ + ∀h g f. + betree_internal_right_fupd f ∘ betree_internal_pivot_fupd g ∘ h = + betree_internal_pivot_fupd g ∘ betree_internal_right_fupd f ∘ h) ∧ + (∀g f. + betree_internal_right_fupd f ∘ betree_internal_left_fupd g = + betree_internal_left_fupd g ∘ betree_internal_right_fupd f) ∧ + ∀h g f. + betree_internal_right_fupd f ∘ betree_internal_left_fupd g ∘ h = + betree_internal_left_fupd g ∘ betree_internal_right_fupd f ∘ h + + [betree_internal_t_fupdfupds] Theorem + + ⊢ (∀g f b. + b with + <|betree_internal_id updated_by f; + betree_internal_id updated_by g|> = + b with betree_internal_id updated_by f ∘ g) ∧ + (∀g f b. + b with + <|betree_internal_pivot updated_by f; + betree_internal_pivot updated_by g|> = + b with betree_internal_pivot updated_by f ∘ g) ∧ + (∀g f b. + b with + <|betree_internal_left updated_by f; + betree_internal_left updated_by g|> = + b with betree_internal_left updated_by f ∘ g) ∧ + ∀g f b. + b with + <|betree_internal_right updated_by f; + betree_internal_right updated_by g|> = + b with betree_internal_right updated_by f ∘ g + + [betree_internal_t_fupdfupds_comp] Theorem + + ⊢ ((∀g f. + betree_internal_id_fupd f ∘ betree_internal_id_fupd g = + betree_internal_id_fupd (f ∘ g)) ∧ + ∀h g f. + betree_internal_id_fupd f ∘ betree_internal_id_fupd g ∘ h = + betree_internal_id_fupd (f ∘ g) ∘ h) ∧ + ((∀g f. + betree_internal_pivot_fupd f ∘ betree_internal_pivot_fupd g = + betree_internal_pivot_fupd (f ∘ g)) ∧ + ∀h g f. + betree_internal_pivot_fupd f ∘ betree_internal_pivot_fupd g ∘ h = + betree_internal_pivot_fupd (f ∘ g) ∘ h) ∧ + ((∀g f. + betree_internal_left_fupd f ∘ betree_internal_left_fupd g = + betree_internal_left_fupd (f ∘ g)) ∧ + ∀h g f. + betree_internal_left_fupd f ∘ betree_internal_left_fupd g ∘ h = + betree_internal_left_fupd (f ∘ g) ∘ h) ∧ + (∀g f. + betree_internal_right_fupd f ∘ betree_internal_right_fupd g = + betree_internal_right_fupd (f ∘ g)) ∧ + ∀h g f. + betree_internal_right_fupd f ∘ betree_internal_right_fupd g ∘ h = + betree_internal_right_fupd (f ∘ g) ∘ h + + [betree_internal_t_induction] Theorem + + ⊢ ∀P0 P1. + (∀b. P1 b ⇒ P0 (BetreeNodeInternal b)) ∧ + (∀b. P0 (BetreeNodeLeaf b)) ∧ + (∀b b0. P0 b ∧ P0 b0 ⇒ ∀u u0. P1 (betree_internal_t u0 u b b0)) ⇒ + (∀b. P0 b) ∧ ∀b. P1 b + + [betree_internal_t_literal_11] Theorem + + ⊢ ∀u01 u1 b11 b01 u02 u2 b12 b02. + <|betree_internal_id := u01; betree_internal_pivot := u1; + betree_internal_left := b11; betree_internal_right := b01|> = + <|betree_internal_id := u02; betree_internal_pivot := u2; + betree_internal_left := b12; betree_internal_right := b02|> ⇔ + u01 = u02 ∧ u1 = u2 ∧ b11 = b12 ∧ b01 = b02 + + [betree_internal_t_literal_nchotomy] Theorem + + ⊢ ∀b. ∃u0 u b1 b0. + b = + <|betree_internal_id := u0; betree_internal_pivot := u; + betree_internal_left := b1; betree_internal_right := b0|> + + [betree_internal_t_nchotomy] Theorem + + ⊢ ∀bb. ∃u0 u b b0. bb = betree_internal_t u0 u b b0 + + [betree_internal_t_updates_eq_literal] Theorem + + ⊢ ∀b u0 u b1 b0. + b with + <|betree_internal_id := u0; betree_internal_pivot := u; + betree_internal_left := b1; betree_internal_right := b0|> = + <|betree_internal_id := u0; betree_internal_pivot := u; + betree_internal_left := b1; betree_internal_right := b0|> + + [betree_leaf_t_11] Theorem + + ⊢ ∀a0 a1 a0' a1'. + betree_leaf_t a0 a1 = betree_leaf_t a0' a1' ⇔ a0 = a0' ∧ a1 = a1' + + [betree_leaf_t_Axiom] Theorem + + ⊢ ∀f. ∃fn. ∀a0 a1. fn (betree_leaf_t a0 a1) = f a0 a1 + + [betree_leaf_t_accessors] Theorem + + ⊢ (∀u u0. (betree_leaf_t u u0).betree_leaf_id = u) ∧ + ∀u u0. (betree_leaf_t u u0).betree_leaf_size = u0 + + [betree_leaf_t_accfupds] Theorem + + ⊢ (∀f b. + (b with betree_leaf_size updated_by f).betree_leaf_id = + b.betree_leaf_id) ∧ + (∀f b. + (b with betree_leaf_id updated_by f).betree_leaf_size = + b.betree_leaf_size) ∧ + (∀f b. + (b with betree_leaf_id updated_by f).betree_leaf_id = + f b.betree_leaf_id) ∧ + ∀f b. + (b with betree_leaf_size updated_by f).betree_leaf_size = + f b.betree_leaf_size + + [betree_leaf_t_case_cong] Theorem + + ⊢ ∀M M' f. + M = M' ∧ (∀a0 a1. M' = betree_leaf_t a0 a1 ⇒ f a0 a1 = f' a0 a1) ⇒ + betree_leaf_t_CASE M f = betree_leaf_t_CASE M' f' + + [betree_leaf_t_case_eq] Theorem + + ⊢ betree_leaf_t_CASE x f = v ⇔ + ∃u u0. x = betree_leaf_t u u0 ∧ f u u0 = v + + [betree_leaf_t_component_equality] Theorem + + ⊢ ∀b1 b2. + b1 = b2 ⇔ + b1.betree_leaf_id = b2.betree_leaf_id ∧ + b1.betree_leaf_size = b2.betree_leaf_size + + [betree_leaf_t_fn_updates] Theorem + + ⊢ (∀f u u0. + betree_leaf_t u u0 with betree_leaf_id updated_by f = + betree_leaf_t (f u) u0) ∧ + ∀f u u0. + betree_leaf_t u u0 with betree_leaf_size updated_by f = + betree_leaf_t u (f u0) + + [betree_leaf_t_fupdcanon] Theorem + + ⊢ ∀g f b. + b with + <|betree_leaf_size updated_by f; betree_leaf_id updated_by g|> = + b with + <|betree_leaf_id updated_by g; betree_leaf_size updated_by f|> + + [betree_leaf_t_fupdcanon_comp] Theorem + + ⊢ (∀g f. + betree_leaf_size_fupd f ∘ betree_leaf_id_fupd g = + betree_leaf_id_fupd g ∘ betree_leaf_size_fupd f) ∧ + ∀h g f. + betree_leaf_size_fupd f ∘ betree_leaf_id_fupd g ∘ h = + betree_leaf_id_fupd g ∘ betree_leaf_size_fupd f ∘ h + + [betree_leaf_t_fupdfupds] Theorem + + ⊢ (∀g f b. + b with + <|betree_leaf_id updated_by f; betree_leaf_id updated_by g|> = + b with betree_leaf_id updated_by f ∘ g) ∧ + ∀g f b. + b with + <|betree_leaf_size updated_by f; betree_leaf_size updated_by g|> = + b with betree_leaf_size updated_by f ∘ g + + [betree_leaf_t_fupdfupds_comp] Theorem + + ⊢ ((∀g f. + betree_leaf_id_fupd f ∘ betree_leaf_id_fupd g = + betree_leaf_id_fupd (f ∘ g)) ∧ + ∀h g f. + betree_leaf_id_fupd f ∘ betree_leaf_id_fupd g ∘ h = + betree_leaf_id_fupd (f ∘ g) ∘ h) ∧ + (∀g f. + betree_leaf_size_fupd f ∘ betree_leaf_size_fupd g = + betree_leaf_size_fupd (f ∘ g)) ∧ + ∀h g f. + betree_leaf_size_fupd f ∘ betree_leaf_size_fupd g ∘ h = + betree_leaf_size_fupd (f ∘ g) ∘ h + + [betree_leaf_t_induction] Theorem + + ⊢ ∀P. (∀u u0. P (betree_leaf_t u u0)) ⇒ ∀b. P b + + [betree_leaf_t_literal_11] Theorem + + ⊢ ∀u01 u1 u02 u2. + <|betree_leaf_id := u01; betree_leaf_size := u1|> = + <|betree_leaf_id := u02; betree_leaf_size := u2|> ⇔ + u01 = u02 ∧ u1 = u2 + + [betree_leaf_t_literal_nchotomy] Theorem + + ⊢ ∀b. ∃u0 u. b = <|betree_leaf_id := u0; betree_leaf_size := u|> + + [betree_leaf_t_nchotomy] Theorem + + ⊢ ∀bb. ∃u u0. bb = betree_leaf_t u u0 + + [betree_leaf_t_updates_eq_literal] Theorem + + ⊢ ∀b u0 u. + b with <|betree_leaf_id := u0; betree_leaf_size := u|> = + <|betree_leaf_id := u0; betree_leaf_size := u|> + + [betree_list_t_11] Theorem + + ⊢ ∀a0 a1 a0' a1'. + BetreeListCons a0 a1 = BetreeListCons a0' a1' ⇔ + a0 = a0' ∧ a1 = a1' + + [betree_list_t_Axiom] Theorem + + ⊢ ∀f0 f1. ∃fn. + (∀a0 a1. fn (BetreeListCons a0 a1) = f0 a0 a1 (fn a1)) ∧ + fn BetreeListNil = f1 + + [betree_list_t_case_cong] Theorem + + ⊢ ∀M M' f v. + M = M' ∧ + (∀a0 a1. M' = BetreeListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧ + (M' = BetreeListNil ⇒ v = v') ⇒ + betree_list_t_CASE M f v = betree_list_t_CASE M' f' v' + + [betree_list_t_case_eq] Theorem + + ⊢ betree_list_t_CASE x f v = v' ⇔ + (∃t b. x = BetreeListCons t b ∧ f t b = v') ∨ + x = BetreeListNil ∧ v = v' + + [betree_list_t_distinct] Theorem + + ⊢ ∀a1 a0. BetreeListCons a0 a1 ≠ BetreeListNil + + [betree_list_t_induction] Theorem + + ⊢ ∀P. (∀b. P b ⇒ ∀t. P (BetreeListCons t b)) ∧ P BetreeListNil ⇒ + ∀b. P b + + [betree_list_t_nchotomy] Theorem + + ⊢ ∀bb. (∃t b. bb = BetreeListCons t b) ∨ bb = BetreeListNil + + [betree_message_t_11] Theorem + + ⊢ (∀a a'. BetreeMessageInsert a = BetreeMessageInsert a' ⇔ a = a') ∧ + ∀a a'. BetreeMessageUpsert a = BetreeMessageUpsert a' ⇔ a = a' + + [betree_message_t_Axiom] Theorem + + ⊢ ∀f0 f1 f2. ∃fn. + (∀a. fn (BetreeMessageInsert a) = f0 a) ∧ + fn BetreeMessageDelete = f1 ∧ + ∀a. fn (BetreeMessageUpsert a) = f2 a + + [betree_message_t_case_cong] Theorem + + ⊢ ∀M M' f v f1. + M = M' ∧ (∀a. M' = BetreeMessageInsert a ⇒ f a = f' a) ∧ + (M' = BetreeMessageDelete ⇒ v = v') ∧ + (∀a. M' = BetreeMessageUpsert a ⇒ f1 a = f1' a) ⇒ + betree_message_t_CASE M f v f1 = + betree_message_t_CASE M' f' v' f1' + + [betree_message_t_case_eq] Theorem + + ⊢ betree_message_t_CASE x f v f1 = v' ⇔ + (∃u. x = BetreeMessageInsert u ∧ f u = v') ∨ + x = BetreeMessageDelete ∧ v = v' ∨ + ∃b. x = BetreeMessageUpsert b ∧ f1 b = v' + + [betree_message_t_distinct] Theorem + + ⊢ (∀a. BetreeMessageInsert a ≠ BetreeMessageDelete) ∧ + (∀a' a. BetreeMessageInsert a ≠ BetreeMessageUpsert a') ∧ + ∀a. BetreeMessageDelete ≠ BetreeMessageUpsert a + + [betree_message_t_induction] Theorem + + ⊢ ∀P. (∀u. P (BetreeMessageInsert u)) ∧ P BetreeMessageDelete ∧ + (∀b. P (BetreeMessageUpsert b)) ⇒ + ∀b. P b + + [betree_message_t_nchotomy] Theorem + + ⊢ ∀bb. + (∃u. bb = BetreeMessageInsert u) ∨ bb = BetreeMessageDelete ∨ + ∃b. bb = BetreeMessageUpsert b + + [betree_node_id_counter_t_11] Theorem + + ⊢ ∀a a'. + betree_node_id_counter_t a = betree_node_id_counter_t a' ⇔ a = a' + + [betree_node_id_counter_t_Axiom] Theorem + + ⊢ ∀f. ∃fn. ∀a. fn (betree_node_id_counter_t a) = f a + + [betree_node_id_counter_t_accessors] Theorem + + ⊢ ∀u. (betree_node_id_counter_t u). + betree_node_id_counter_next_node_id = + u + + [betree_node_id_counter_t_accfupds] Theorem + + ⊢ ∀f b. + (b with betree_node_id_counter_next_node_id updated_by f). + betree_node_id_counter_next_node_id = + f b.betree_node_id_counter_next_node_id + + [betree_node_id_counter_t_case_cong] Theorem + + ⊢ ∀M M' f. + M = M' ∧ (∀a. M' = betree_node_id_counter_t a ⇒ f a = f' a) ⇒ + betree_node_id_counter_t_CASE M f = + betree_node_id_counter_t_CASE M' f' + + [betree_node_id_counter_t_case_eq] Theorem + + ⊢ betree_node_id_counter_t_CASE x f = v ⇔ + ∃u. x = betree_node_id_counter_t u ∧ f u = v + + [betree_node_id_counter_t_component_equality] Theorem + + ⊢ ∀b1 b2. + b1 = b2 ⇔ + b1.betree_node_id_counter_next_node_id = + b2.betree_node_id_counter_next_node_id + + [betree_node_id_counter_t_fn_updates] Theorem + + ⊢ ∀f u. + betree_node_id_counter_t u with + betree_node_id_counter_next_node_id updated_by f = + betree_node_id_counter_t (f u) + + [betree_node_id_counter_t_fupdfupds] Theorem + + ⊢ ∀g f b. + b with + <|betree_node_id_counter_next_node_id updated_by f; + betree_node_id_counter_next_node_id updated_by g|> = + b with betree_node_id_counter_next_node_id updated_by f ∘ g + + [betree_node_id_counter_t_fupdfupds_comp] Theorem + + ⊢ (∀g f. + betree_node_id_counter_next_node_id_fupd f ∘ + betree_node_id_counter_next_node_id_fupd g = + betree_node_id_counter_next_node_id_fupd (f ∘ g)) ∧ + ∀h g f. + betree_node_id_counter_next_node_id_fupd f ∘ + betree_node_id_counter_next_node_id_fupd g ∘ h = + betree_node_id_counter_next_node_id_fupd (f ∘ g) ∘ h + + [betree_node_id_counter_t_induction] Theorem + + ⊢ ∀P. (∀u. P (betree_node_id_counter_t u)) ⇒ ∀b. P b + + [betree_node_id_counter_t_literal_11] Theorem + + ⊢ ∀u1 u2. + <|betree_node_id_counter_next_node_id := u1|> = + <|betree_node_id_counter_next_node_id := u2|> ⇔ u1 = u2 + + [betree_node_id_counter_t_literal_nchotomy] Theorem + + ⊢ ∀b. ∃u. b = <|betree_node_id_counter_next_node_id := u|> + + [betree_node_id_counter_t_nchotomy] Theorem + + ⊢ ∀bb. ∃u. bb = betree_node_id_counter_t u + + [betree_node_id_counter_t_updates_eq_literal] Theorem + + ⊢ ∀b u. + b with betree_node_id_counter_next_node_id := u = + <|betree_node_id_counter_next_node_id := u|> + + [betree_node_t_11] Theorem + + ⊢ (∀a a'. BetreeNodeInternal a = BetreeNodeInternal a' ⇔ a = a') ∧ + ∀a a'. BetreeNodeLeaf a = BetreeNodeLeaf a' ⇔ a = a' + + [betree_node_t_Axiom] Theorem + + ⊢ ∀f0 f1 f2. ∃fn0 fn1. + (∀a. fn0 (BetreeNodeInternal a) = f0 a (fn1 a)) ∧ + (∀a. fn0 (BetreeNodeLeaf a) = f1 a) ∧ + ∀a0 a1 a2 a3. + fn1 (betree_internal_t a0 a1 a2 a3) = + f2 a0 a1 a2 a3 (fn0 a2) (fn0 a3) + + [betree_node_t_case_cong] Theorem + + ⊢ ∀M M' f f1. + M = M' ∧ (∀a. M' = BetreeNodeInternal a ⇒ f a = f' a) ∧ + (∀a. M' = BetreeNodeLeaf a ⇒ f1 a = f1' a) ⇒ + betree_node_t_CASE M f f1 = betree_node_t_CASE M' f' f1' + + [betree_node_t_case_eq] Theorem + + ⊢ betree_node_t_CASE x f f1 = v ⇔ + (∃b. x = BetreeNodeInternal b ∧ f b = v) ∨ + ∃b. x = BetreeNodeLeaf b ∧ f1 b = v + + [betree_node_t_distinct] Theorem + + ⊢ ∀a' a. BetreeNodeInternal a ≠ BetreeNodeLeaf a' + + [betree_node_t_induction] Theorem + + ⊢ ∀P0 P1. + (∀b. P1 b ⇒ P0 (BetreeNodeInternal b)) ∧ + (∀b. P0 (BetreeNodeLeaf b)) ∧ + (∀b b0. P0 b ∧ P0 b0 ⇒ ∀u u0. P1 (betree_internal_t u0 u b b0)) ⇒ + (∀b. P0 b) ∧ ∀b. P1 b + + [betree_node_t_nchotomy] Theorem + + ⊢ ∀bb. (∃b. bb = BetreeNodeInternal b) ∨ ∃b. bb = BetreeNodeLeaf b + + [betree_params_t_11] Theorem + + ⊢ ∀a0 a1 a0' a1'. + betree_params_t a0 a1 = betree_params_t a0' a1' ⇔ + a0 = a0' ∧ a1 = a1' + + [betree_params_t_Axiom] Theorem + + ⊢ ∀f. ∃fn. ∀a0 a1. fn (betree_params_t a0 a1) = f a0 a1 + + [betree_params_t_accessors] Theorem + + ⊢ (∀u u0. (betree_params_t u u0).betree_params_min_flush_size = u) ∧ + ∀u u0. (betree_params_t u u0).betree_params_split_size = u0 + + [betree_params_t_accfupds] Theorem + + ⊢ (∀f b. + (b with betree_params_split_size updated_by f). + betree_params_min_flush_size = + b.betree_params_min_flush_size) ∧ + (∀f b. + (b with betree_params_min_flush_size updated_by f). + betree_params_split_size = + b.betree_params_split_size) ∧ + (∀f b. + (b with betree_params_min_flush_size updated_by f). + betree_params_min_flush_size = + f b.betree_params_min_flush_size) ∧ + ∀f b. + (b with betree_params_split_size updated_by f). + betree_params_split_size = + f b.betree_params_split_size + + [betree_params_t_case_cong] Theorem + + ⊢ ∀M M' f. + M = M' ∧ + (∀a0 a1. M' = betree_params_t a0 a1 ⇒ f a0 a1 = f' a0 a1) ⇒ + betree_params_t_CASE M f = betree_params_t_CASE M' f' + + [betree_params_t_case_eq] Theorem + + ⊢ betree_params_t_CASE x f = v ⇔ + ∃u u0. x = betree_params_t u u0 ∧ f u u0 = v + + [betree_params_t_component_equality] Theorem + + ⊢ ∀b1 b2. + b1 = b2 ⇔ + b1.betree_params_min_flush_size = b2.betree_params_min_flush_size ∧ + b1.betree_params_split_size = b2.betree_params_split_size + + [betree_params_t_fn_updates] Theorem + + ⊢ (∀f u u0. + betree_params_t u u0 with + betree_params_min_flush_size updated_by f = + betree_params_t (f u) u0) ∧ + ∀f u u0. + betree_params_t u u0 with betree_params_split_size updated_by f = + betree_params_t u (f u0) + + [betree_params_t_fupdcanon] Theorem + + ⊢ ∀g f b. + b with + <|betree_params_split_size updated_by f; + betree_params_min_flush_size updated_by g|> = + b with + <|betree_params_min_flush_size updated_by g; + betree_params_split_size updated_by f|> + + [betree_params_t_fupdcanon_comp] Theorem + + ⊢ (∀g f. + betree_params_split_size_fupd f ∘ + betree_params_min_flush_size_fupd g = + betree_params_min_flush_size_fupd g ∘ + betree_params_split_size_fupd f) ∧ + ∀h g f. + betree_params_split_size_fupd f ∘ + betree_params_min_flush_size_fupd g ∘ h = + betree_params_min_flush_size_fupd g ∘ + betree_params_split_size_fupd f ∘ h + + [betree_params_t_fupdfupds] Theorem + + ⊢ (∀g f b. + b with + <|betree_params_min_flush_size updated_by f; + betree_params_min_flush_size updated_by g|> = + b with betree_params_min_flush_size updated_by f ∘ g) ∧ + ∀g f b. + b with + <|betree_params_split_size updated_by f; + betree_params_split_size updated_by g|> = + b with betree_params_split_size updated_by f ∘ g + + [betree_params_t_fupdfupds_comp] Theorem + + ⊢ ((∀g f. + betree_params_min_flush_size_fupd f ∘ + betree_params_min_flush_size_fupd g = + betree_params_min_flush_size_fupd (f ∘ g)) ∧ + ∀h g f. + betree_params_min_flush_size_fupd f ∘ + betree_params_min_flush_size_fupd g ∘ h = + betree_params_min_flush_size_fupd (f ∘ g) ∘ h) ∧ + (∀g f. + betree_params_split_size_fupd f ∘ + betree_params_split_size_fupd g = + betree_params_split_size_fupd (f ∘ g)) ∧ + ∀h g f. + betree_params_split_size_fupd f ∘ + betree_params_split_size_fupd g ∘ h = + betree_params_split_size_fupd (f ∘ g) ∘ h + + [betree_params_t_induction] Theorem + + ⊢ ∀P. (∀u u0. P (betree_params_t u u0)) ⇒ ∀b. P b + + [betree_params_t_literal_11] Theorem + + ⊢ ∀u01 u1 u02 u2. + <|betree_params_min_flush_size := u01; + betree_params_split_size := u1|> = + <|betree_params_min_flush_size := u02; + betree_params_split_size := u2|> ⇔ u01 = u02 ∧ u1 = u2 + + [betree_params_t_literal_nchotomy] Theorem + + ⊢ ∀b. ∃u0 u. + b = + <|betree_params_min_flush_size := u0; + betree_params_split_size := u|> + + [betree_params_t_nchotomy] Theorem + + ⊢ ∀bb. ∃u u0. bb = betree_params_t u u0 + + [betree_params_t_updates_eq_literal] Theorem + + ⊢ ∀b u0 u. + b with + <|betree_params_min_flush_size := u0; + betree_params_split_size := u|> = + <|betree_params_min_flush_size := u0; + betree_params_split_size := u|> + + [betree_upsert_fun_state_t_11] Theorem + + ⊢ (∀a a'. + BetreeUpsertFunStateAdd a = BetreeUpsertFunStateAdd a' ⇔ a = a') ∧ + ∀a a'. + BetreeUpsertFunStateSub a = BetreeUpsertFunStateSub a' ⇔ a = a' + + [betree_upsert_fun_state_t_Axiom] Theorem + + ⊢ ∀f0 f1. ∃fn. + (∀a. fn (BetreeUpsertFunStateAdd a) = f0 a) ∧ + ∀a. fn (BetreeUpsertFunStateSub a) = f1 a + + [betree_upsert_fun_state_t_case_cong] Theorem + + ⊢ ∀M M' f f1. + M = M' ∧ (∀a. M' = BetreeUpsertFunStateAdd a ⇒ f a = f' a) ∧ + (∀a. M' = BetreeUpsertFunStateSub a ⇒ f1 a = f1' a) ⇒ + betree_upsert_fun_state_t_CASE M f f1 = + betree_upsert_fun_state_t_CASE M' f' f1' + + [betree_upsert_fun_state_t_case_eq] Theorem + + ⊢ betree_upsert_fun_state_t_CASE x f f1 = v ⇔ + (∃u. x = BetreeUpsertFunStateAdd u ∧ f u = v) ∨ + ∃u. x = BetreeUpsertFunStateSub u ∧ f1 u = v + + [betree_upsert_fun_state_t_distinct] Theorem + + ⊢ ∀a' a. BetreeUpsertFunStateAdd a ≠ BetreeUpsertFunStateSub a' + + [betree_upsert_fun_state_t_induction] Theorem + + ⊢ ∀P. (∀u. P (BetreeUpsertFunStateAdd u)) ∧ + (∀u. P (BetreeUpsertFunStateSub u)) ⇒ + ∀b. P b + + [betree_upsert_fun_state_t_nchotomy] Theorem + + ⊢ ∀bb. + (∃u. bb = BetreeUpsertFunStateAdd u) ∨ + ∃u. bb = BetreeUpsertFunStateSub u + + [datatype_betree_be_tree_t] Theorem + + ⊢ DATATYPE + (record betree_be_tree_t betree_be_tree_params + betree_be_tree_node_id_cnt betree_be_tree_root) + + [datatype_betree_leaf_t] Theorem + + ⊢ DATATYPE (record betree_leaf_t betree_leaf_id betree_leaf_size) + + [datatype_betree_list_t] Theorem + + ⊢ DATATYPE (betree_list_t BetreeListCons BetreeListNil) + + [datatype_betree_message_t] Theorem + + ⊢ DATATYPE + (betree_message_t BetreeMessageInsert BetreeMessageDelete + BetreeMessageUpsert) + + [datatype_betree_node_id_counter_t] Theorem + + ⊢ DATATYPE + (record betree_node_id_counter_t + betree_node_id_counter_next_node_id) + + [datatype_betree_node_t] Theorem + + ⊢ DATATYPE + (betree_node_t BetreeNodeInternal BetreeNodeLeaf ∧ + record betree_internal_t betree_internal_id + betree_internal_pivot betree_internal_left + betree_internal_right) + + [datatype_betree_params_t] Theorem + + ⊢ DATATYPE + (record betree_params_t betree_params_min_flush_size + betree_params_split_size) + + [datatype_betree_upsert_fun_state_t] Theorem + + ⊢ DATATYPE + (betree_upsert_fun_state_t BetreeUpsertFunStateAdd + BetreeUpsertFunStateSub) + + +*) +end |