Correctness_Algebras.Recursion_Strict