Proof that all natural numbers are interesting

Leslie Lamport

December 1, 1993

Abstract:

HTML version of a sample proof that uses Lamport's proof style [1], illustrating how structured proofs can be converted to HTML pages via L^ATEX2HTML enriched with extensions for Lamport's proof style.

Theorem All natural numbers are interesting. Assume:$n$ a natural number. Prove:$n$ is interesting.

show proof

hide proof

<1>1: A number is interesting if it is the smallest number not in an interesting set.

show proof

hide proof

Proof: By definition of interesting.

<1>2: Case: $n=0$

show proof

hide proof

Proof: By <1>1, since $0$ is the smallest natural number not in $\emptyset$.

<1>3: Case:

1. $n>0$
2. $n-1$ is interesting

show proof

hide proof

Proof: By <1>1, since case assumption <1> implies that $\{k : k \leq n-1\}$ is interesting.

<1>4Q.E.D.

show proof

hide proof

Proof: Steps <1>2 and <1>3, assumption <0>, and mathematical induction.

Bibliography

1

Leslie Lamport, 1993, How to write a proof. In Global Analysis of Modern Mathematics, pp. 311-321. Publish or Perish, Houston, Texas, February 1993. A symposium in honor of Richard Palais' sixtieth birthday (also published as SRC Research Report 94). http://research.microsoft.com/users/lamport/proofs/src94.ps.Z

About this document ...

Proof that all natural numbers are interesting

This document was generated using the LaTeX2HTML translator Version 2K.1beta (1.56)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html ll2

The translation was initiated by Glowacki Martin / TU Wien Studenten Account Kopie on 2002-10-01

URL of this proof as currently expanded for referencing and bookmarking purposes.

This HTML file was generated using the pf2html extension, version 0.03.
LaTeX2HTML + pf.sty (hypertext proofs).

Project homepage at http://www.dbai.tuwien.ac.at/proj/pf2html