| Description: It is often convenient to
have the antecedent under focus in first
position, so we can apply immediate theorem forms (as opposed to
deduction, tautology form). This series of theorems swaps the first with
the last antecedent in an implication chain. This kind of swapping is
self-inverse, whence we prefer it over, say, rotating theorems. A
consequent can hide a tail of a longer chain, so theorems of this series
appear as swapping a pair of antecedents with fixed offsets. This form of
swapping antecedents is flexible enough to allow for any permutation of
antecedents in an implication chain.
The first elements of this series correspond to com12 32,
com13 88,
com14 96 and com15 101 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-mp-x 33269 series developed before.
(Contributed by Wolf Lammen, 17-Nov-2019.) |
