From 73fd1921f90824e481c0f8e0c52003d37af5a2e5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 10 May 2023 19:22:32 +0200
Subject: Cleanup divDefProtoScript

---
 backends/hol4/divDefProtoTheory.sig | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'backends/hol4/divDefProtoTheory.sig')

diff --git a/backends/hol4/divDefProtoTheory.sig b/backends/hol4/divDefProtoTheory.sig
index 6e4e5950..e74c2fd4 100644
--- a/backends/hol4/divDefProtoTheory.sig
+++ b/backends/hol4/divDefProtoTheory.sig
@@ -18,6 +18,7 @@ sig
     val fix_fixed_eq : thm
     val fix_fixed_terminates : thm
     val fix_fixed_termination_rec_case : thm
+    val fix_fixed_termination_rec_case_aux : thm
     val fix_fuel_compute : thm
     val fix_fuel_mono : thm
     val fix_fuel_mono_least : thm
@@ -128,6 +129,15 @@ sig
           fix_fuel ($LEAST (fix_fuel_P f x)) f x =
           fix_fuel ($LEAST (fix_fuel_P f y)) f y
    
+   [fix_fixed_termination_rec_case_aux]  Theorem
+      
+      ⊢ ∀x y n m.
+          is_valid_fp_body f ⇒
+          (∀g. f g x = g y) ⇒
+          fix_fuel_P f x n ⇒
+          fix_fuel_P f y m ⇒
+          fix_fuel n f x = fix_fuel m f y
+   
    [fix_fuel_compute]  Theorem
       
       ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧
-- 
cgit v1.2.3