| Description: This series of theorems
allow swapping any two antecedents in an
implication chain. The theorem names follow a pattern wl-impchain-com-n.m
with integral numbers n < m, that swaps the m-th antecedent with n-th
one
in an implication chain. It is sufficient to restrict the length of the
chain to m, too, since the consequent can be assumed to be the tail right
of the m-th antecedent of any arbitrary sized implication chain. We
further assume n > 1, since the wl-impchain-com-1.x 35549 series already
covers the special case n = 1.
Being able to swap any two antecedents in an implication chain lays the
foundation of permuting its antecedents arbitrarily.
The proofs of this series aim at automated proofing using a simple scheme.
Any instance of this series is a triple step of swapping the first and
n-th antecedent, then the first and the m-th, then the first and the n-th
antecedent again. Each of these steps is an instance of the
wl-impchain-com-1.x 35549 series. (Contributed by Wolf
Lammen,
17-Nov-2019.) |
