La terminaison d'un calcul est indépendante du dernier argument
Contexte
Lemme sur le calcul.
Énoncé
Variables
x, y, z
Conditions
- x, y et z sont des formules
- x +f y est un calcul terminé
Conclusion
x +f z est un calcul terminé
Preuve
Reprenons la définition de →c1 :
Si les règles de 1 à 4 ne s'applique pas parce qu'il n'y a pas le bon nombre d'argument, alors c'est aussi le cas pour x +f z.
Si les règles 1,2 et 3 ne s'appliquent pas à cause de l'argument du if, comme cet argument se trouve dans a c'est aussi le cas pour x +f z.
Donc les règles 1 à 4 ne s'appliquent pas à x +f z.
La règle "calcul de la fonction" est indépendante du dernier argument, donc elle ne s'applique pas à x +f z.
Donc aucune règle ne s'applique à x +f z qui est donc un calcul terminé.