for questions or link request: module admin

Substitution of Proof Lines

name: subst, module version: 1.00.00, rule version: 1.01.00, original: subst, author of this module: Michael Meyling

Description

This module declares the general rule for substituting variables.

References

This document uses the results of the following documents:

Content

If a proof line could be derived by using rule4 (rename proposition variable), predrule1 (rename bound subject variable) and predrule2 (rename free subject variable) multiple times, we declare a new rule to shorten that derivation:

1. Rule Declaration
      Substitute Variables     (rule8)

The use of this rule could always be replaced by proof lines that make only use of the referenced rules.

Cross References

This document is used by the following documents: