| 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 35713, that
allows prepending an arbitrary antecedent to an implication chain. Using
our antecedent swapping theorems described in wl-impchain-com-n.m 35740, 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 35735 series developed before.
(Contributed by Wolf Lammen, 20-Jun-2020.) |
