summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/hol4/divDefProtoScript.sml525
-rw-r--r--backends/hol4/divDefProtoTheory.sig10
2 files changed, 12 insertions, 523 deletions
diff --git a/backends/hol4/divDefProtoScript.sml b/backends/hol4/divDefProtoScript.sml
index 64d4b9f0..6280fa7e 100644
--- a/backends/hol4/divDefProtoScript.sml
+++ b/backends/hol4/divDefProtoScript.sml
@@ -101,7 +101,7 @@ Proof
QED
(* TODO: I think we can merge this with the theorem below *)
-Theorem fix_fixed_termination_rec_case:
+Theorem fix_fixed_termination_rec_case_aux:
∀x y n m.
is_valid_fp_body f ⇒
(∀g. f g x = g y) ⇒
@@ -128,7 +128,7 @@ Theorem fix_fixed_termination_rec_case:
Proof
rw [] >>
imp_res_tac fix_fuel_mono_least >>
- irule fix_fixed_termination_rec_case >>
+ irule fix_fixed_termination_rec_case_aux >>
fs [] >>
(* TODO: factorize *)
qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
@@ -249,525 +249,4 @@ Proof
simp_tac arith_ss []
QED
-(************************** FAILED TESTS *)
-
-(*
-Datatype:
- fresult = FReturn 'b | FFail error | FRec 'a
-End
-
-(* TODO: monad converter from fresult to result + rewrite rules *)
-val fres_to_res_def = Define ‘
- fres_to_res (f : 'a -> 'b result) (r : ('a, 'b) fresult) : 'b result =
- case r of
- | FReturn x => Return x
- | FFail e => Fail e
- | FRec y => f y
-’
-
-val fixa_fuel_def = Define ‘
- (fixa_fuel (0 : num) (f : 'a -> ('a, 'b) fresult) (x : 'a) : 'b result = Diverge) ∧
- (fixa_fuel (SUC n) (f : 'a -> ('a, 'b) fresult) (x : 'a) : 'b result =
- fres_to_res (fixa_fuel n f) (f x))
-’
-
-val fixa_fuel_P_def = Define ‘
- fixa_fuel_P f x n = ~(is_diverge (fixa_fuel n f x))
-’
-
-val fixa_def = Define ‘
- fixa (f : 'a -> ('a, 'b) fresult) (x : 'a) : 'b result =
- if (∃ n. fixa_fuel_P f x n) then fixa_fuel ($LEAST (fixa_fuel_P f x)) f x else Diverge
-’
-
-Theorem fixa_fuel_mono:
- ∀n m. n <= m ⇒ (∀f x. fixa_fuel_P f x n ⇒ fixa_fuel n f x = fixa_fuel m f x)
-Proof
- Induct_on ‘n’ >> rpt strip_tac
- >- (fs [fixa_fuel_P_def, is_diverge_def, fixa_fuel_def, fres_to_res_def]) >>
- Cases_on ‘m’ >- int_tac >> fs [] >>
- last_x_assum imp_res_tac >>
- fs [fixa_fuel_P_def, is_diverge_def, fixa_fuel_def, fres_to_res_def] >>
- Cases_on ‘f x’ >> fs []
-QED
-
-(* TODO: remove ? *)
-Theorem fixa_fuel_P_least:
- ∀f x n. fixa_fuel_P f x n ⇒ fixa_fuel_P f x ($LEAST (fixa_fuel_P f x))
-Proof
- rw [] >>
- (* Use the "fundamental" property about $LEAST *)
- qspec_assume ‘fixa_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
- (* Prove the premise *)
- pop_assum sg_premise_tac >- metis_tac [] >>
- rw []
-QED
-
-Theorem fixa_fuel_mono_least:
- ∀n f x. fixa_fuel_P f x n ⇒ fixa_fuel n f x = fixa_fuel ($LEAST (fixa_fuel_P f x)) f x
-Proof
- rw [] >>
- (* Use the "fundamental" property about $LEAST *)
- qspec_assume ‘fixa_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
- (* Prove the premise *)
- pop_assum sg_premise_tac >- metis_tac [] >>
- (* Prove that $LEAST ... ≤ n *)
- sg ‘n >= $LEAST (fixa_fuel_P f x)’ >-(
- spose_not_then assume_tac >>
- fs [not_ge_eq_lt]) >>
- pure_once_rewrite_tac [EQ_SYM_EQ] >>
- irule fixa_fuel_mono >>
- fs []
-QED
-
-Theorem fixa_fixed_eq:
- ∀f x. fixa f x = fres_to_res (fixa f) (f x)
-Proof
- rw [fixa_def, fres_to_res_def]
- >- (
- (* Termination case *)
- imp_res_tac fixa_fuel_P_least >>
- Cases_on ‘$LEAST (fixa_fuel_P f x)’ >>
- fs [fixa_fuel_P_def, is_diverge_def, fixa_fuel_def, fres_to_res_def] >>
- Cases_on ‘f x’ >> fs [] >>
- rw [] >> fs [] >>
- irule fixa_fuel_mono_least >>
- fs [fixa_fuel_P_def, is_diverge_def, fixa_fuel_def]) >>
- (* Divergence case *)
- fs [fres_to_res_def] >>
- sg ‘∀n. ~(fixa_fuel_P f x (SUC n))’ >- fs [] >>
- Cases_on ‘f x’ >> fs [] >>
- fs [fixa_fuel_P_def, is_diverge_def, fixa_fuel_def, fres_to_res_def] >>
- rw []
-QED
-
-val fix_fuel_def = Define ‘
- (fix_fuel (0 : num) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = Diverge) ∧
- (fix_fuel (SUC n) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = f (fix_fuel n f) x)
-’
-
-val fix_fuel_P_def = Define ‘
- fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
-’
-
-val fix_def = Define ‘
- fix (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result =
- if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
-’
-
-Theorem fixa_fuel_eq_fix_fuel:
- ∀n (f : 'a -> ('a, 'b) fresult) (x : 'a).
- fixa_fuel n f x = fix_fuel n (\g y. fres_to_res g (f y)) x
-Proof
- Induct_on ‘n’ >> rw [fixa_fuel_def, fix_fuel_def, fres_to_res_def]
-QED
-
-Theorem fixa_fuel_P_eq_fix_fuel_P:
- ∀(f : 'a -> ('a, 'b) fresult) (x : 'a).
- fixa_fuel_P f x = fix_fuel_P (\g y. fres_to_res g (f y)) x
-Proof
- rw [] >> irule EQ_EXT >> rw [] >>
- qspecl_assume [‘x'’, ‘f’, ‘x’] fixa_fuel_eq_fix_fuel >>
- fs [fixa_fuel_P_def, fix_fuel_P_def]
-QED
-
-Theorem fixa_fuel_eq_fix_fuel:
- ∀(f : 'a -> ('a, 'b) fresult) (x : 'a).
- fixa f x = fix (\g y. fres_to_res g (f y)) x
-Proof
- rw [fixa_def, fix_def, fixa_fuel_P_eq_fix_fuel_P, fixa_fuel_eq_fix_fuel]
-QED
-
-(*
- The annoying thing is that to make this work, we need to rewrite the
- body by swapping matches, which is not easy to automate.
-*)
-
-(*
-f x =
- case _ of
- | _ => Fail e
- | _ => Return x
- | _ => f y
-
-f x (g : ('a, 'b) result => 'c)
-
-f x (fres_to_res g) = f x g
-
-*)
-
-(*
-val fix_fuel_def = Define ‘
- (fix_fuel (0 : num) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = Diverge) ∧
- (fix_fuel (SUC n) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = f (fix_fuel n f) x)
-’
-
-val fix_fuel_P_def = Define ‘
- fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
-’
-*)
-
-
-(*
-val is_valid_FP_body_def = Define ‘
- is_valid_FP_body (f : (('a, 'b) fresult -> 'c) -> ('a, 'b) fresult -> 'c) =
- ∃ (fa: (('a, 'b) fresult -> ('a, 'b) fresult) -> ('a, 'b) fresult -> ('a, 'b) fresult).
- ∀ (g : ('a, 'b) fresult -> 'c) x.
- f g x = g (fa (\x. x) x)
-
-val fix_fuel_def = Define ‘
- (fix_fuel (0 : num) (f : (('a, 'b) fresult -> 'b result) -> ('a, 'b) fresult -> 'b result) (x : ('a, 'b) fresult) : 'b result = Diverge) ∧
- (fix_fuel (SUC n) (f : (('a, 'b) fresult -> 'b result) -> ('a, 'b) fresult -> 'b result) (x : ('a, 'b) fresult) : 'b result = f (fix_fuel n f) x)
-’
-
-val fix_fuel_P_def = Define ‘
- fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
-’
-
-val fix_def = Define ‘
- fix f x : 'b result =
- if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
-
-
-Theorem fix_fuel_mono:
- ∀f. is_valid_FP_body f ⇒
- ∀n m. n <= m ⇒ (∀x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel m f x)
-Proof
- strip_tac >> strip_tac >>
- Induct_on ‘n’ >> rpt strip_tac
- >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
- Cases_on ‘m’ >- int_tac >>
- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
- fs [is_valid_FP_body] >>
- last_x_assum (qspec_assume ‘fix_fuel n f’) >>
- fs []
-QED
-
-’*)
-
-(*
- * Test with a validity predicate which gives monotonicity.
-
- TODO: not enough to prove the fixed-point equation.
- *)
-val fix_fuel_def = Define ‘
- (fix_fuel (0 : num) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = Diverge) ∧
- (fix_fuel (SUC n) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = f (fix_fuel n f) x)
-’
-
-val fix_fuel_P_def = Define ‘
- fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
-’
-
-val fix_def = Define ‘
- fix (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result =
- if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
-’
-
-Theorem fix_eq:
- fix f = \x. if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
-Proof
- irule EQ_EXT >> fs [fix_def]
-QED
-
-val is_valid_fp_body_def = Define ‘
- is_valid_fp_body (f : ('a -> 'b result) -> 'a -> 'b result) =
- ∀n m. n ≤ m ⇒ ∀x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel m f x
-’
-
-Theorem fix_fuel_mono_least:
- ∀f. is_valid_fp_body f ⇒
- ∀n x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x
-Proof
- rw [] >>
- (* Use the "fundamental" property about $LEAST *)
- qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
- (* Prove the premise *)
- pop_assum sg_premise_tac >- metis_tac [] >> fs [] >>
- (* Prove that $LEAST ... ≤ n *)
- sg ‘n >= $LEAST (fix_fuel_P f x)’ >-(
- spose_not_then assume_tac >>
- fs [not_ge_eq_lt]) >>
- pure_once_rewrite_tac [EQ_SYM_EQ] >>
- (* Finish by using the monotonicity property *)
- fs [is_valid_fp_body_def]
-QED
-
-
-(* TODO: remove ? *)
-Theorem fix_fuel_P_least:
- ∀f x n. fix_fuel_P f x n ⇒ fix_fuel_P f x ($LEAST (fix_fuel_P f x))
-Proof
- rw [] >>
- (* Use the "fundamental" property about $LEAST *)
- qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
- (* Prove the premise *)
- pop_assum sg_premise_tac >- metis_tac [] >>
- rw []
-QED
-
-(*Theorem test:
- fix_fuel_P f x (SUC n) ⇒
- (∀m. n ≤ m ⇒ f (fix_fuel n f) x = f (fix_fuel m f) x) ⇒
- f (fix_fuel n f) x = f (fix f) x
-Proof
- rw [] >>
- spose_not_then assume_tac >>
- fs [fix_eq]
-*)
-Theorem fix_fixed_eq:
- ∀f. is_valid_fp_body f ⇒ ∀x. fix f x = f (fix f) x
-Proof
- rw [fix_def] >> CASE_TAC >> fs []
- >- (
- (* Termination case *)
- sg ‘$LEAST (fix_fuel_P f x) <= n’ >- cheat >>
- imp_res_tac fix_fuel_P_least >>
- Cases_on ‘$LEAST (fix_fuel_P f x)’ >>
- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
- Cases_on ‘n’ >>
- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
- (* Use the validity assumption *)
- fs [is_valid_fp_body_def] >>
-
-(* last_x_assum imp_res_tac >> *)
- last_assum (qspecl_assume [‘SUC n'’, ‘SUC n''’]) >> fs [] >>
- pop_assum imp_res_tac >>
- pop_assum (qspec_assume ‘x’) >>
- pop_assum sg_premise_tac >- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
-
- fs [fix_fuel_def] >>
-
-
- fs [fix_fuel_P_def] >>
- rfs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
-
- fs [fix_eq] >>
-
- Cases_on ‘fix_fuel n' f x’ >> fs [] >>
- last_assum (qspecl_then [‘n'’, ‘’
- f (fix_fuel n' f) x >>
-
- Cases_on ‘f x’ >> fs [] >>
- rw [] >> fs [] >>
- irule fix_fuel_mono_least >>
- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
- (* Divergence case *)
- fs [fres_to_res_def] >>
- sg ‘∀n. ~(fix_fuel_P f x (SUC n))’ >- fs [] >>
- Cases_on ‘f x’ >> fs [] >>
- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
- rw []
-QED
-
-
-(* A slightly weaker and more precise validity criteria.
-
- We simply extracted the part of the inductive proof that we can't prove without
- knowing ‘f’.
- *)
-val is_valid_fp_body_weak_def = Define ‘
- is_valid_fp_body_weak f =
- ∀n m x.
- ((∀x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel m f x) ⇒
- n ≤ m ⇒
- fix_fuel_P f x (SUC n) ⇒
- fix_fuel (SUC n) f x = fix_fuel (SUC m) f x)
-’
-
-Theorem is_valid_fp_body_weak_imp_is_valid:
- ∀f. is_valid_fp_body_weak f ⇒ is_valid_fp_body f
-Proof
- rpt strip_tac >> fs [is_valid_fp_body_def] >>
- Induct_on ‘n’ >- fs [fix_fuel_P_def, fix_fuel_def, is_diverge_def] >>
- Cases_on ‘m’ >> fs [] >>
- fs [is_valid_fp_body_weak_def]
-QED
-
-(* Testing on an example *)
-Datatype:
- list_t =
- ListCons 't list_t
- | ListNil
-End
-
-val nth_body_def = Define ‘
- nth_body (f : ('t list_t # u32) -> 't result) (x : ('t list_t # u32)) : 't result =
- let (ls, i) = x in
- case ls of
- | ListCons x tl =>
- if u32_to_int i = (0:int)
- then (Return x)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- f (tl, i0)
- od
- | ListNil => (Fail Failure)
-’
-
-(* The general proof of is_valid_fp_body. We isolate a more precise property below. *)
-Theorem nth_body_is_valid:
- is_valid_fp_body nth_body
-Proof
- pure_rewrite_tac [is_valid_fp_body_def] >>
- Induct_on ‘n’ >- fs [fix_fuel_P_def, fix_fuel_def, is_diverge_def] >>
- Cases_on ‘m’ >- fs [] >>
- rpt strip_tac >>
- (* TODO: here *)
- last_assum imp_res_tac >>
- (* TODO: here? *)
- fs [fix_fuel_def, nth_body_def, fix_fuel_P_def, is_diverge_def, bind_def] >>
- Cases_on ‘x’ >> fs [] >> (* TODO: automate this *)
- (* Explore all paths *)
- Cases_on ‘q’ >> fs [] >>
- Cases_on ‘u32_to_int r = 0’ >> fs [] >>
- Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs []
-QED
-
-
-Theorem nth_body_is_valid_weak:
- is_valid_fp_body_weak nth_body
-Proof
- pure_rewrite_tac [is_valid_fp_body_weak_def] >>
- rpt strip_tac >>
- (* TODO: automate this - we may need to destruct a variable number of times *)
- Cases_on ‘x’ >> fs [] >>
- (* Expand all *)
- fs [fix_fuel_def, nth_body_def, fix_fuel_P_def, is_diverge_def, bind_def] >>
- (* Explore all paths *)
- Cases_on ‘q’ >> fs [] >>
- Cases_on ‘u32_to_int r = 0’ >> fs [] >>
- Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs []
-QED
-
-(*
- * Test with a more general validity predicate.
- *)
-(* We need to control the way calls to the continuation are performed, so
- that we can inspect the inputs (otherwise we can't prove anything).
- *)
-val is_valid_FP_body_def = Define ‘
- is_valid_FP_body (f : (('a, 'b) fresult -> 'c) -> 'a -> 'c) =
- ∃ (fa: (('a, 'b) fresult -> ('a, 'b) fresult) -> 'a -> ('a, 'b) fresult).
- ∀ (g : ('a, 'b) fresult -> 'c) x.
- f g x = g (fa (\x. x) x)
-’
-
-
-val fix_fuel_def = Define ‘
- (fix_fuel (0 : num) (f : (('a, 'b) fresult -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = Diverge) ∧
- (fix_fuel (SUC n) (f : (('a, 'b) fresult -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result =
- f (fres_to_res (fix_fuel n f)) x)
-’
-
-val fix_fuel_P_def = Define ‘
- fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
-’
-
-val fix_def = Define ‘
- fix f x : 'b result =
- if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
-’
-
-Theorem fix_fuel_mono:
- ∀f. is_valid_FP_body f ⇒
- ∀n m. n <= m ⇒ (∀x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel m f x)
-Proof
- strip_tac >> strip_tac >>
- Induct_on ‘n’ >> rpt strip_tac
- >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def, fres_to_res_def] >>
- Cases_on ‘m’ >- int_tac >>
- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
- fs [is_valid_FP_body_def, fres_to_res_def] >>
- CASE_TAC >>
- last_x_assum (qspec_assume ‘fres_to_res (fix_fuel n f)’) >>
- fs [fres_to_res_def]
-QED
-
-(* Tests *)
-
-
-
-Datatype:
- list_t =
- ListCons 't list_t
- | ListNil
-End
-
-(*
-val def_qt = ‘
- nth_mut_fwd (ls : 't list_t) (i : u32) : 't result =
- case ls of
- | ListCons x tl =>
- if u32_to_int i = (0:int)
- then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- nth_mut_fwd tl i0
- od
- | ListNil =>
- Fail Failure
-’
-*)
-
-val nth_body_def = Define ‘
- nth_body (f : ('t list_t # u32, 't) fresult -> 'c) (ls : 't list_t, i : u32) : 'c =
- case ls of
- | ListCons x tl =>
- if u32_to_int i = (0:int)
- then f (FReturn x)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- f (FRec (tl, i0))
- od
- | ListNil => f (FFail Failure)
-’
-
-Theorem nth_body_is_valid_FP_body:
- is_valid_FP_body nth_body
-Proof
- fs [is_valid_FP_body_def] >>
- exists_tac “nth_body” >>
-QED
-
-“nth_body”
-
-(* TODO: abbreviation for ‘(\g y. fres_to_res g (f y))’ *)
-Theorem fix_fixed_eq:
- ∀f x. fix (\g y. fres_to_res g (f y)) x =
- (f x)
- fres_to_res (\g y. fres_to_res g (f y))
-
-
-
-(*
-TODO: can't prove that
-
-Theorem fix_fuel_mono:
- ∀n m. n <= m ⇒ (∀f x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel m f x)
-Proof
- Induct_on ‘n’ >> rpt strip_tac
- >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
- Cases_on ‘m’ >- int_tac >>
- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
-
- sg ‘fix_fuel n f = fix_fuel n' f’ >>
-
- last_x_assum imp_res_tac >>
- pop_assum (qspecl_assume [‘x’, ‘f’]) >>
-
-Theorem fix_def_eq:
- ∀f x. fix f x = f (fix f) x
-Proof
-
-*)
-*)
-
-
val _ = export_theory ()
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) ∧