| Description: If an implication chain
is assumed (hypothesis) or proven (theorem) to
hold, then we may add any extra antecedent to it, without changing its
truth. This is expressed in its simplest form in wl-luk-a1i 35527, that
allows us prepending an arbitrary antecedent to an implication chain.
Using our antecedent swapping theorems described in
wl-impchain-com-n.m 35554, we may then move such a prepended
antecedent to
any desired location within all antecedents. The first series of theorems
of this kind adds a single antecedent somewhere to an implication chain.
The appended number in the theorem name indicates its position within all
antecedents, 1 denoting the head position. A second theorem series
extends this idea to multiple additions (TODO).
Adding antecedents to an implication chain usually weakens their
universality. The consequent afterwards dependends on more conditions
than before, which renders the implication chain less versatile. So you
find this proof technique mostly when you adjust a chain to a hypothesis
of a rule. A common case are syllogisms merging two implication chains
into one.
The first elements of the first series correspond to a1i 11, a1d 25 and
a1dd 50 in the main part.
The proofs of this series aim at automated proving using a simple
recursive scheme. It employs the previous theorem in the series along
with a sample from the wl-impchain-com-1.x 35549 series developed before.
(Contributed by Wolf Lammen, 20-Jun-2020.) |
