**Description: **Alternate proof of dfbi1 195. This proof, discovered by Gregory Bush on
8-Mar-2004, has several curious properties. First, it has only 17 steps
directly from the axioms and df-bi 189, compared to over 800 steps were the
proof of dfbi1 195 expanded into axioms. Second, step 2 demands
only the
property of "true"; any axiom (or theorem) could be used. It
might be
thought, therefore, that it is in some sense redundant, but in fact no
proof is shorter than this (measured by number of steps). Third, it
illustrates how intermediate steps can "blow up" in size even in
short
proofs. Fourth, the compressed proof is only 182 bytes (or 17 bytes in
D-proof notation), but the generated web page is over 200kB with
intermediate steps that are essentially incomprehensible to humans (other
than Gregory Bush). If there were an obfuscated code contest for proofs,
this would be a contender. This "blowing up" and
incomprehensibility of
the intermediate steps vividly demonstrate the advantages of using many
layered intermediate theorems, since each theorem is easier to
understand. (Contributed by Gregory Bush, 10-Mar-2004.)
(New usage is discouraged.) (Proof modification is
discouraged.) |