for questions or link request: module admin

Substitution of Proof Lines

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


This module declares the general rule for substituting variables.

Uses the following modules:

Is used by the following modules:

If a proof line could be derived by using <a href="propaxiom 1 .00.00 1 .00.00.html#rule4">rename proposition variable</a>, <a href="predaxiom 1 .00.00 1 .00.00.html#predrule1">rename bound subject variable</a> and <a href="predaxiom 1 .00.00 1 .00.00.html#predrule2">rename free subject variable</a> 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.

This module is used by the following modules: