Page 386 of 800
| Page 386 of 800 | Search internet |
The multzero page states and proves a simple lemma. The page uses the definition of Peano arithmetic, a lemma, and a lot of proof tactics from the Peano page. A numbered version of the multzero.lgs source text is included below. Also see the original, unnumbered lgs file, the main pdf, and the document root.
1 "";;014E20344F3D486370710A10269E83D974EB8E9787EFB994A0BBD8BB0806
2 ""P multzero
3 ""R check
4 ""R Peano
5 ""R base
6
7 ""D 0
8 3.2l
9
10 ""B
11 page ( ""N , ""C )
12 title "Multiplication by zero"
13 bib "
14 @Book {Mendelson87,
15 author = {E. Mendelson},
16 title = {Introduction to Mathematical Logic},
17 publisher = {Wadsworth and Brooks},
18 year = {1987},
19 edition = {3.}}
20 "
21 main text "
22 \title{Multiplication by zero}
23 \author{A. U. Thor}
24 \maketitle
25 \tableofcontents
26 "[ make macro expanded version ragged right ]"
27 "[ prepare proof indentation ]"
28 \section{Theorem}
29 We now state Lemma 3.2l of \cite{Mendelson87}:
30 "[ PA lemma 3.2l : all x : 0 * x = 0 end lemma ]"
31 \section{Proof}
32 "[ PA proof of 3.2l :
33 line L01 : S7 >> 0 * 0 = 0 ;
34 line L02 : Block >> Begin ;
35 line L03 : Hypothesis >> 0 * x = 0 ;
36 line L04 : S8 >> 0 * x suc = 0 * x + 0 ;
37 line L05 : S5 >> 0 * x + 0 = 0 * x ;
38 line L06 : 3.2c mp L04 mp L05 >> 0 * x suc = 0 * x ;
39 line L07 : 3.2c mp L06 mp L03 >> 0 * x suc = 0 ;
40 line L08 : Block >> End ;
41 line L09 : Induction at x ponens L01 ponens L08 >> 0 * x = 0 ;
42 line L10 : Gen1 ponens L09 >> all x : 0 * x = 0 qed ]"
43 \bibliography{./page}
44 "
45 appendix "
46 \title{Multiplication by zero - appendix}
47 \author{A. U. Thor}
48 \maketitle
49 \tableofcontents
50 \section{\TeX\ definitions}
51 \begin{statements}
52 \item "[[ tex show define 3.2l as "
53 \mathbf{3.2l}" end define ]]"
54 \end{statements}
55 "
56 end page
57
| Page 386 of 800 | Search logiweb.eu |