| 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 33,
com13 89,
com14 97 and com15 102 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 38015 series developed before.
(Contributed by Wolf Lammen, 17-Nov-2019.) |
