device-56.home 2026-3-24:22:24:27

fonction récursive primitive.md

@@ -137,6 +137,7 @@ Dans cette section, on démontre que quelques fonctions élémentaires sont réc
 > > Notons $\operatorname{prec} = \lambda x.x \dot{-}1$. On a démontré dans le lemme précédent que cette fontion est récursive primitive.
 > > Maintenant, on peut définir $\operatorname{sub} = \lambda xy.x \dot{-} y$ comme :
 > > $\operatorname{sub} = \rho(P_1^{1}, \operatorname{prec}(P_3^{3}))$
+^soustraction-positive
 
 > [!proposition]- La fonction signe est récursive primitive
 > On définit la [[fonction signe]] par :