MODULE ( HEADER ( SPEC ( NAME ("subst"), VERSION ("1.00.00"), VERSION ("1.01.00"), LOCATIONS ( LOCATION ("http://www.qedeq.org/0_00_53") ) ), HEADLINE ("Substitution of Proof Lines"), DESCRIPTION ( "This module declares the general rule for substituting variables." ), EMAIL ("module@qedeq.org"), AUTHORS ( AUTHOR ("Michael Meyling",EMAIL ("mime@qedeq.org")) ) ), IMPORTS ( IMPORT ( SPEC ( NAME ("propaxiom"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION ("."), LOCATION ("http://www.qedeq.org/0_00_53") ) ) ), IMPORT ( SPEC ( NAME ("predaxiom"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION (".") ) ) ) ), USEDBY ( SPEC ( NAME ("prophilbert1"), VERSION ("1.00.00"), VERSION ("1.02.00"), LOCATIONS ( LOCATION (".") ) ) ), PARAGRAPHS ( PARAGRAPH ( LABEL ("rule8"), "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:", DECLARERULE ( "SUBSTLINE", "Substitute Variables" ), "The use of this rule could always be replaced by proof lines that make only use of the referenced rules." ) ) )