Lazi

Théorème de remplacement de variable

Contexte

Que ce soit pour prouver la validité de l'extension "forAll" ou pour prouver le théorème de preuves d'égalités sur les arguments, nous avons besoin de prouver qu'une preuve reste valide si on remplace un mot n'ayant pas de sens (c'est à dire ne faisant l'objet d'aucune règle) par n'importe quelle formule.

Énoncé

Variables

m,p,q,w,f

Conditions

  • m est lazi.0.0 à laquelle des mots sont ajoutés
  • p est une preuve en m
  • w est l'un des mots ajoutés à lazi.0.0
  • f est une formule pour m
  • q est p où l'on a remplacé w par f

Conclusion

  • q est une preuve valide de m
  • l'objet de q est l'objet de p où le remplacement est effectué

Preuve

Nous allons le prouver par récurrence sur la longeur de p. Nous construisons l'hypothèse de récurrence en reprenant les conditions (plus évendement la condition sur la longueur de p) et en ajoutant à la conclusion que les ctruths déduites par q sont les ctruths déduites par p auxquelles on a appliqué le remplacement.

Si p est de longueur 1

Les règles lazi.0.0 sont des règles simples, c'est règles sont exprimées directement par la ctruth à déduire, après remplacement des variables. De plus ces règles ne contiennent pas les les nouveaux mots clés. Donc le remplacement de w dans les valeurs des variables laissent les déductions valides, et la ctruth déduite après remplacement de w est équivalente à la ctruth déduite avant remplacement à laquelle on applique le remplacement.

Si le théorème est prouvé jusqu'à n - 1 et que p est de longueur n

Le théorème étant vrai pour n - 1, et pour la dernière déduction isolée, les conditions et les conclusions (on tient compte des conclusions de toutes les déductions, voir proofT .o'conditions du fichier "05-deductions.def.lazi" ) de q privé de la dernière déductions sont celles de p où l'on a effectué les remplacements sur les ctruth. Comme c'est aussi le cas pour la dernière déduction, les conditions vérifiée par la dernière déduction dans p et q moins la dernière déduction se correspondent.
Donc les conditions et conclusions de p et q se correspondent au remplacement près.