From ce8f5c8f67e41a74bfdf8f6d664ff4e45e9de850 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 7 Sep 2023 16:06:14 +0200
Subject: Regenerate the test files and fix a proof

---
 tests/hol4/betree/betreeMain_FunsTheory.sig | 14 ++------------
 1 file changed, 2 insertions(+), 12 deletions(-)

(limited to 'tests/hol4/betree/betreeMain_FunsTheory.sig')

diff --git a/tests/hol4/betree/betreeMain_FunsTheory.sig b/tests/hol4/betree/betreeMain_FunsTheory.sig
index 6c249f70..c922ca9f 100644
--- a/tests/hol4/betree/betreeMain_FunsTheory.sig
+++ b/tests/hol4/betree/betreeMain_FunsTheory.sig
@@ -58,8 +58,6 @@ sig
     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
@@ -1215,22 +1213,14 @@ sig
             case st of
               BetreeUpsertFunStateAdd v =>
                 do
-                  margin <- u64_sub core_num_u64_max_c prev0;
+                  margin <- u64_sub core_u64_max prev0;
                   if u64_ge margin v then u64_add prev0 v
-                  else Return core_num_u64_max_c
+                  else Return core_u64_max
                 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 ()
-- 
cgit v1.2.3