"File page.sty
% thebibliography environment from
% /usr/share/texmf/tex/latex/base/book.cls
% with \chapter removed
\renewenvironment{thebibliography}[1]
{\list{\@biblabel{\@arabic\c@enumiv}}%
{\settowidth\labelwidth{\@biblabel{#1}}%
\leftmargin\labelwidth
\advance\leftmargin\labelsep
\@openbib@code
\usecounter{enumiv}%
\let\p@enumiv\@empty
\renewcommand\theenumiv{\@arabic\c@enumiv}}%
\sloppy
\clubpenalty4000
\@clubpenalty \clubpenalty
\widowpenalty4000%
\sfcode`\.\@m}
{\def\@noitemerr
{\@latex@warning{Empty `thebibliography' environment}}%
\endlist}
End of file
File page.tex
\documentclass [fleqn]{article}
\setlength {\overfullrule }{1mm}
\input{lgwinclude}
\usepackage{latexsym}
%\setlength{\parindent}{0em}
%\setlength{\parskip}{1ex}
% The font of each Logiweb construct is under tight control except that
% strings are typeset in whatever font is in effect at the time of
% typesetting. This is done to enhance the readability of strings in the
% TeX source generated by Logiweb. The default font for typesetting
% strings is \rm:
\everymath{\rm}
\usepackage{makeidx}
\usepackage{page}
\makeindex
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}
\newlength{\bracketwidth}
\settowidth{\bracketwidth}{$[{}$}
\newcommand{\back}{\protect\makebox[-1.0\bracketwidth]{}}
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 130 490 730}}
\hypersetup{pdftitle=A Logiweb base page}
\hypersetup{colorlinks=true}
\bibliographystyle{plain}
% \tex{something} writes something to page.otx for later inclusion
\newwrite\outex
\newtoks\toktex
\immediate\openout\outex=page.otx
\newcommand{\tex}[1]{\toktex={\item #1}\immediate\write\outex{\the\toktex}}
% \test{something} writes something to page.tst for later inclusion
\newwrite\outest
\immediate\openout\outest=page.tst
\newcommand{\test}[1]{\toktex={\item #1}\immediate\write\outest{\the\toktex}}
% Concerning \catcode`\@=11 : See the TeXbook, Appendix B (page 344).
% \afterheading suppresses indentation once, c.f. latex.ltx.
% \display{something} displays something as a displayed equation except
% that linebreaking is possible and displaymath is not turned on by default.
% The first paragraph after \display{something} is unindented.
% Glue below formulas may be wrong. The definition of \display misses
% something like \addvspace{\belowdisplayskip}.
\catcode`\@=11
\def\afterheading{\@afterheading}
\catcode`\@=12
\newcommand{\display}[1]{\begin{list}{}{\setlength{\leftmargin}{\mathindent}}
\item #1\end{list}
\afterheading}
\newcommand{\statement}[1]{\begin{list}{}{\setlength{\leftmargin}{0mm}}
\item #1\end{list}
\afterheading}
\usepackage{pstricks, pst-node, pst-tree}
\begin{document}
% *********** Enkel bevisstruktur, 18. juni ************
%\newpsobject{showgrid}{psgrid}{subgriddiv=1,griddots=10,gridlabels=6pt}
\begin{pspicture}(0,8)(3,12)
%\showgrid
\psset{arrows=->}
\rput(6,10){\rnode{H}{\psframebox{H}}}
\rput(0, 7){\rnode{C}{\psframebox{C}}}
\rput(4.5, 8){\rnode{G}{\psframebox{G}}}
\rput(6, 7){\rnode{D}{\psframebox{D}}}
\rput(12, 7){\rnode{F}{\psframebox{F}}}
\rput(0, 5){\rnode{B}{\psframebox{B}}}
\rput(0, 3){\rnode{A}{\psframebox{A}}}
\ncline{C}{H}
\ncline{C}{D}
\ncline{C}{G}
\ncline{D}{F}
\ncline{D}{G}
\ncline{D}{H}
\ncline{F}{H}
\ncline{G}{H}
\ncline{A}{B}
\ncline{B}{C}
\ncline{B}{D}
\ncline{B}{F}
\end{pspicture}
\newpage
\appendix
\section{Navnet p\aa{} dette dokument} \label{sec:navn}
Den f\o{}lgende definition fastl\ae{}gger dette dokuments Logiweb-navn:
"
begin math pyk define clueless as "clueless" end define end math
end "
\section{TeX definitioner} \label{sec:texdefinitioner}
"
begin math tex define nani kata kene...:1 as "Weakening" end define end math
end "
"
begin math tex define nani kata kene...:25 as "DoubleMP" end define end math
end "
"
begin math tex define nani kata kene...:2 as "Conditioned MP" end define end math
end "
"
begin math tex define nani kata kene...:28 as "DoubleConditionedMP" end define end math
end "
"
begin math tex define nani kata kene...:4 as "ImplyTransitivity" end define end math
end "
"
begin math tex define nani kata kene...:3 as "PermuteAntecedents" end define end math
end "
"
begin math tex define nani kata kene...:17 as "AddOne" end define end math
end "
"
begin math tex define nani kata kene...:9 as "substantiation" end define end math
end "
"
begin math tex define nani kata kene...:26 as "InductionMacro" end define end math
end "
"
begin math tex define nani kata kene...:5 as "EqualReflexivity" end define end math
end "
"
begin math tex define nani kata kene...:6 as "EqualSymmetry" end define end math
end "
"
begin math tex define nani kata kene...:27 as "EqualSymmetryRule" end define end math
end "
"
begin math tex define nani kata kene...:7 as "EqualTransitivity" end define end math
end "
"
begin math tex define nani kata kene...:20 as "EqualTransitivityRule" end define end math
end "
"
begin math tex define nani kata kene...:21 as "EqualTransitivityConditionedRule" end define end math
end "
"
begin math tex define nani kata kene...:8 as "Mendelson32d" end define end math
end "
"
begin math tex define nani kata kene...:18 as "Mendelson32dRule" end define end math
end "
"
begin math tex define nani kata kene...:19 as "Mendelson32dConditionedRule" end define end math
end "
"
begin math tex define nani kata kene...:10 as "Mendelson32fBase" end define end math
end "
"
begin math tex define nani kata kene...:11 as "Mendelson32fInduction" end define end math
end "
"
begin math tex define nani kata kene...:12 as "Mendelson32f" end define end math
end "
"
begin math tex define nani kata kene...:13 as "Mendelson32gBase" end define end math
end "
"
begin math tex define nani kata kene...:14 as "Mendelson32gInduction" end define end math
end "
"
begin math tex define nani kata kene...:15 as "Mendelson32g" end define end math
end "
"
begin math tex define nani kata kene...:16 as "Switch" end define end math
end "
"
begin math tex define nani kata kene...:22 as "PlusCommutativityBase" end define end math
end "
"
begin math tex define nani kata kene...:23 as "PlusCommutativityInduction" end define end math
end "
"
begin math tex define nani kata kene...:24 as "PlusCommutativity" end define end math
end "
\end{document}
*Beviset i denne rapport er ; den overordnede struktur i de to beviser er den samme.
*Jeg har ikke fors\o{}gt at bevise deduktionsteoremet i Peano aritmetik.
*Hvis "
begin math rule prime mp end math
end " havde v\ae{}ret et lemma (og ikke en slutningsregel), ville jeg have rubriceret "
begin math nani kata kene...:2 end math
end " som et betinget regellemma.
End of file
latex page"
The pyk compiler, version 0.grue.20050603 by Klaus Grue,