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é.