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, a₁, ..., a_n, b₁, ..., b_n

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 a₁+f ... +f a_n ) ⊢ f +f b₁+f ... +f b_n ]

Conclusion

Pour tout 1 k ≤ n il existe une preuve dans m q_k sans condition et ayant pour objet a_k *=* b_k.

Preuve

Soit ma la mathématique m où l'on ajoute une déduction déduisant uniquement f +f a₁+f ... +f a_n.
D'après le théorème "toute vérité lazi.0.0 + ajout", pour 1 ≤ k ≤ n on a a_k =c b_k.
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 a_k =c b_k.

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 v₁,...,v_m tq v₁ = f +f a₁+f ... +f a_n, v_m = f +f b₁+f ... +f b_n et tq pour 1 ≤ k < m v_k p contienne la déduction égalité et vérité ayant pour valeur de variables $T[ v_k , v_k+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 q_k = p où l'on remplace f par $F x₁,...,x_n → x_k = a_k .

Et si a_k contient f ?