Lazi

Théorème de preuves d'égalités sur les arguments

Contexte

Quand on a des vérités dérivées, en lazi.0.0, d'une formule prouvée par une déduction d'ajout, comme ces vérités peuvent servir à une déduction d'application, il faut pouvoir non seulement retrouver la déduction d'application, mais aussi prouver l'égalité entre les arguments. En effet, cela est nécessaire pour la traduction. Nous cherchons ici à prouver que l'on peut extraire une preuve d'égalité pour chaque argument.

Énoncé

Variables

m, p, f, n, a1, ..., an, b1, ..., bn

Conditions

  • f est un mot non lazi.a.0
  • m est la mathématique lazi.a.0 où des mots — dont f — sont ajoutés.
  • n ∈ ℕ
  • p est une preuve dans m
  • l'objet de p est $CT[ (f +f a1+f ... +f an ) ⊢ f +f b1+f ... +f bn ]

Conclusion

Pour tout 1 k ≤ n il existe une preuve dans m qk sans condition et ayant pour objet ak *=* bk.

Preuve

Soit ma la mathématique m où l'on ajoute une déduction déduisant uniquement f +f a''1''+f ... +f a''n''.
D'après le théorème "toute vérité lazi.0.0 + ajout", pour 1 ≤ k ≤ n on a ak =c bk.
D'après le théorème de la preuve de l'égalité par calcul il existe pour 1 ≤ k ≤ n une preuve dans m de ak =c bk.

CQFD

Recherche d'une preuve

Forme de la preuve

Soit d la dernière déduction de p. Une vérité dont la fonction minimale n'est pas l'égalité ne peut provenir que de la règle "égalité et vérité". Soit x et y les variables de la règle. D'après le théorème "toute vérité lazi.0.0 + ajout, x se calcule en une formule de fonction minimale f, donc la fonction minimale de x ne peut être l'égalité.
Donc par récurrence il existe une liste de formule v1,...,vm tq v1 = f +f a1+f ... +f an, vm = f +f b''1''+f ... +f b''n'' et tq pour 1 ≤ k < m vk p contienne la déduction égalité et vérité ayant pour valeur de variables $T[ vk , vk+1 ].

Essai 1

D'après le théorème de remplacement de variable, si on remplace f dans p par une formule au sens m, alors p reste valide et son objet est celui de p ayant subi le même remplacement.

Pour 1 ≤ k ≤ n, soit qk = p où l'on remplace f par $F x1,...,xn → xk = ak .

Et si ak contient f ?