**Description: **This proof of dfbi1 184, 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 177, compared to over 800 steps were the proof of
dfbi1 184
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.) |