"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} - fjernet 3.5.06
%\makeindex - fjernet 3.5.06
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}
\newlength{\bracketwidth}
\settowidth{\bracketwidth}{$[{}$}
\newcommand{\back}{\protect\makebox[-1.0\bracketwidth]{}}
% FE-pakker
\usepackage[latin1]{inputenc}
\usepackage[dvips]{graphicx}
\usepackage{verbatim}
\usepackage[danish]{babel}
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 130 490 730}}
%\hypersetup{pdftitle=}
\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}
\begin {document}
\title {\ae{}kvivalensrelationer i Logiweb}
\author {}
\maketitle
\tableofcontents
" [ ragged right expansion ] "
\section{Indledning}
\begin{figure}
\resizebox{\textwidth}{!}{
\includegraphics[0cm,0cm][20cm,30cm]{/home/disk15/eriksen/.logiweb/grafik/peano.eps}
}
\end{figure}
Denne rapport indeholder et aksiomsystem for en reduceret version af ZF m\ae{}ngdel\ae{}re. Ud fra dette aksiomsystem vil jeg vise en r\ae{}kke
\section{Chores}
\begin{flushleft}
" [ math protect define pyk of contains-empty x end empty as text "contains-empty "! end empty" end text end define linebreak define pyk of 1deduction x conclude x end 1deduction as text "1deduction "! conclude "! end 1deduction" end text end define linebreak define pyk of 1deduction zero x conclude x end 1deduction as text "1deduction zero "! conclude "! end 1deduction" end text end define linebreak define pyk of 1deduction side x conclude x condition x end 1deduction as text "1deduction side "! conclude "! condition "! end 1deduction" end text end define linebreak define pyk of 1deduction one x conclude x condition x end 1deduction as text "1deduction one "! conclude "! condition "! end 1deduction" end text end define linebreak define pyk of 1deduction two x conclude x condition x end 1deduction as text "1deduction two "! conclude "! condition "! end 1deduction" end text end define linebreak define pyk of 1deduction three x conclude x condition x bound x end 1deduction as text "1deduction three "! conclude "! condition "! bound "! end 1deduction" end text end define linebreak define pyk of 1deduction four x conclude x condition x bound x end 1deduction as text "1deduction four "! conclude "! condition "! bound "! end 1deduction" end text end define linebreak define pyk of 1deduction four star x conclude x condition x bound x end 1deduction as text "1deduction four star "! conclude "! condition "! bound "! end 1deduction" end text end define linebreak define pyk of 1deduction five x condition x bound x end 1deduction as text "1deduction five "! condition "! bound "! end 1deduction" end text end define linebreak define pyk of 1deduction six x conclude x exception x bound x end 1deduction as text "1deduction six "! conclude "! exception "! bound "! end 1deduction" end text end define linebreak define pyk of 1deduction six star x conclude x exception x bound x end 1deduction as text "1deduction six star "! conclude "! exception "! bound "! end 1deduction" end text end define linebreak define pyk of 1deduction seven x end 1deduction as text "1deduction seven "! end 1deduction" end text end define linebreak define pyk of 1deduction eight x bound x end 1deduction as text "1deduction eight "! bound "! end 1deduction" end text end define linebreak define pyk of 1deduction eight star x bound x end 1deduction as text "1deduction eight star "! bound "! end 1deduction" end text end define linebreak define pyk of cdots as text "cdots" end text end define linebreak define pyk of object-var as text "object-var" end text end define linebreak define pyk of ex-var as text "ex-var" end text end define linebreak define pyk of ph-var as text "ph-var" end text end define linebreak define pyk of vaerdi as text "vaerdi" end text end define linebreak define pyk of variabel as text "variabel" end text end define linebreak define pyk of op2 x comma x end op2 as text "op2 "! comma "! end op2" end text end define linebreak define pyk of op x end op as text "op "! end op" end text end define linebreak define pyk of placeholder-var1 as text "placeholder-var1" end text end define linebreak define pyk of placeholder-var2 as text "placeholder-var2" end text end define linebreak define pyk of placeholder-var3 as text "placeholder-var3" end text end define linebreak define pyk of placeholder-var x end var as text "placeholder-var "! end var" end text end define linebreak define pyk of x is placeholder-var as text ""! is placeholder-var" end text end define linebreak define pyk of ph-sub x is x where x is x end sub as text "ph-sub "! is "! where "! is "! end sub" end text end define linebreak define pyk of ph-sub0 x is x where x is x end sub as text "ph-sub0 "! is "! where "! is "! end sub" end text end define linebreak define pyk of ph-sub1 x is x where x is x end sub as text "ph-sub1 "! is "! where "! is "! end sub" end text end define linebreak define pyk of ph-sub* x is x where x is x end sub as text "ph-sub* "! is "! where "! is "! end sub" end text end define linebreak define pyk of existential var x end var as text "existential var "! end var" end text end define linebreak define pyk of x is existential var as text ""! is existential var" end text end define linebreak define pyk of ex1 as text "ex1" end text end define linebreak define pyk of ex2 as text "ex2" end text end define linebreak define pyk of ex10 as text "ex10" end text end define linebreak define pyk of ex20 as text "ex20" end text end define linebreak define pyk of exist-sub x is x where x is x end sub as text "exist-sub "! is "! where "! is "! end sub" end text end define linebreak define pyk of exist-sub0 x is x where x is x end sub as text "exist-sub0 "! is "! where "! is "! end sub" end text end define linebreak define pyk of exist-sub1 x is x where x is x end sub as text "exist-sub1 "! is "! where "! is "! end sub" end text end define linebreak define pyk of exist-sub* x is x where x is x end sub as text "exist-sub* "! is "! where "! is "! end sub" end text end define linebreak define pyk of var big set as text "var big set" end text end define linebreak define pyk of object big set as text "object big set" end text end define linebreak define pyk of meta big set as text "meta big set" end text end define linebreak define pyk of system zf as text "system zf" end text end define linebreak define pyk of 1rule mp as text "1rule mp" end text end define linebreak define pyk of 1rule gen as text "1rule gen" end text end define linebreak define pyk of 1rule deduction as text "1rule deduction" end text end define linebreak define pyk of 1rule ad absurdum as text "1rule ad absurdum" end text end define linebreak define pyk of 1rule repetition as text "1rule repetition" end text end define linebreak define pyk of 1rule exist intro as text "1rule exist intro" end text end define linebreak define pyk of axiom extensionality as text "axiom extensionality" end text end define linebreak define pyk of axiom separation definition as text "axiom separation definition" end text end define linebreak define pyk of axiom pair definition as text "axiom pair definition" end text end define linebreak define pyk of axiom union definition as text "axiom union definition" end text end define linebreak define pyk of axiom power definition as text "axiom power definition" end text end define linebreak define pyk of axiom empty set as text "axiom empty set" end text end define linebreak define pyk of cheating axiom all disjoint as text "cheating axiom all disjoint" end text end define linebreak define pyk of zermelo empty set as text "zermelo empty set" end text end define linebreak define pyk of lemma separation2formula as text "lemma separation2formula" end text end define linebreak define pyk of lemma formula2separation as text "lemma formula2separation" end text end define linebreak define pyk of lemma equivalence nec condition0 as text "lemma equivalence nec condition0" end text end define linebreak define pyk of lemma equivalence nec condition as text "lemma equivalence nec condition" end text end define linebreak define pyk of lemma eq subset0 as text "lemma eq subset0" end text end define linebreak define pyk of lemma eq subset as text "lemma eq subset" end text end define linebreak define pyk of lemma set equality suff condition as text "lemma set equality suff condition" end text end define linebreak define pyk of prop lemma weakening as text "prop lemma weakening" end text end define linebreak define pyk of prop lemma negative mt as text "prop lemma negative mt" end text end define linebreak define pyk of prop lemma mp2 as text "prop lemma mp2" end text end define linebreak define pyk of prop lemma mp3 as text "prop lemma mp3" end text end define linebreak define pyk of prop lemma mp4 as text "prop lemma mp4" end text end define linebreak define pyk of prop lemma mp5 as text "prop lemma mp5" end text end define linebreak define pyk of prop lemma technicality as text "prop lemma technicality" end text end define linebreak define pyk of prop lemma mt as text "prop lemma mt" end text end define linebreak define pyk of prop lemma add double neg as text "prop lemma add double neg" end text end define linebreak define pyk of prop lemma remove double neg as text "prop lemma remove double neg" end text end define linebreak define pyk of prop lemma and commutativity as text "prop lemma and commutativity" end text end define linebreak define pyk of prop lemma first conjunct as text "prop lemma first conjunct" end text end define linebreak define pyk of prop lemma second conjunct as text "prop lemma second conjunct" end text end define linebreak define pyk of prop lemma join conjuncts as text "prop lemma join conjuncts" end text end define linebreak define pyk of prop lemma iff first as text "prop lemma iff first" end text end define linebreak define pyk of prop lemma iff second as text "prop lemma iff second" end text end define linebreak define pyk of prop lemma contrapositive as text "prop lemma contrapositive" end text end define linebreak define pyk of prop lemma from contradiction as text "prop lemma from contradiction" end text end define linebreak define pyk of lemma er is reflexive as text "lemma er is reflexive" end text end define linebreak define pyk of lemma er is symmetric as text "lemma er is symmetric" end text end define linebreak define pyk of lemma er is transitive as text "lemma er is transitive" end text end define linebreak define pyk of lemma reflexivity0 as text "lemma reflexivity0" end text end define linebreak define pyk of lemma reflexivity as text "lemma reflexivity" end text end define linebreak define pyk of lemma symmetry0 as text "lemma symmetry0" end text end define linebreak define pyk of lemma symmetry as text "lemma symmetry" end text end define linebreak define pyk of lemma transitivity0 as text "lemma transitivity0" end text end define linebreak define pyk of lemma transitivity as text "lemma transitivity" end text end define linebreak define pyk of lemma auto member as text "lemma auto member" end text end define linebreak define pyk of lemma set equality skip quantifier as text "lemma set equality skip quantifier" end text end define linebreak define pyk of lemma set equality nec condition as text "lemma set equality nec condition" end text end define linebreak define pyk of lemma empty set is subset as text "lemma empty set is subset" end text end define linebreak define pyk of lemma unique empty set0 as text "lemma unique empty set0" end text end define linebreak define pyk of lemma unique empty set as text "lemma unique empty set" end text end define linebreak define pyk of lemma none-equivalence nec condition0 as text "lemma none-equivalence nec condition0" end text end define linebreak define pyk of lemma none-equivalence nec condition1 as text "lemma none-equivalence nec condition1" end text end define linebreak define pyk of lemma none-equivalence nec condition as text "lemma none-equivalence nec condition" end text end define linebreak define pyk of prop lemma auto imply as text "prop lemma auto imply" end text end define linebreak define pyk of prop lemma imply transitivity as text "prop lemma imply transitivity" end text end define linebreak define pyk of lemma member not empty as text "lemma member not empty" end text end define linebreak define pyk of lemma member not empty0 as text "lemma member not empty0" end text end define linebreak define pyk of lemma =reflexivity as text "lemma =reflexivity" end text end define linebreak define pyk of lemma =symmetry as text "lemma =symmetry" end text end define linebreak define pyk of lemma =transitivity0 as text "lemma =transitivity0" end text end define linebreak define pyk of lemma =transitivity as text "lemma =transitivity" end text end define linebreak define pyk of lemma formula2union as text "lemma formula2union" end text end define linebreak define pyk of lemma union2formula as text "lemma union2formula" end text end define linebreak define pyk of lemma subset transitive as text "lemma subset transitive" end text end define linebreak define pyk of lemma subset in power set as text "lemma subset in power set" end text end define linebreak define pyk of lemma power set is subset0 as text "lemma power set is subset0" end text end define linebreak define pyk of lemma power set is subset0-switch as text "lemma power set is subset0-switch" end text end define linebreak define pyk of lemma power set is subset as text "lemma power set is subset" end text end define linebreak define pyk of lemma power set is subset-switch as text "lemma power set is subset-switch" end text end define linebreak define pyk of lemma equivalence class is subset as text "lemma equivalence class is subset" end text end define linebreak define pyk of lemma bs subset union(bs/r) as text "lemma bs subset union(bs/r)" end text end define linebreak define pyk of lemma union(bs/r) subset bs as text "lemma union(bs/r) subset bs" end text end define linebreak define pyk of lemma union(bs/r) is bs as text "lemma union(bs/r) is bs" end text end define linebreak define pyk of lemma eq-system not empty0 as text "lemma eq-system not empty0" end text end define linebreak define pyk of lemma eq-system not empty as text "lemma eq-system not empty" end text end define linebreak define pyk of prop lemma weaken or first as text "prop lemma weaken or first" end text end define linebreak define pyk of prop lemma weaken or second as text "prop lemma weaken or second" end text end define linebreak define pyk of prop lemma from disjuncts as text "prop lemma from disjuncts" end text end define linebreak define pyk of prop lemma iff commutativity as text "prop lemma iff commutativity" end text end define linebreak define pyk of lemma pair2formula as text "lemma pair2formula" end text end define linebreak define pyk of lemma set equality suff condition(t)0 as text "lemma set equality suff condition(t)0" end text end define linebreak define pyk of lemma set equality suff condition(t) as text "lemma set equality suff condition(t)" end text end define linebreak define pyk of lemma formula2pair as text "lemma formula2pair" end text end define linebreak define pyk of lemma pair subset0 as text "lemma pair subset0" end text end define linebreak define pyk of lemma pair subset1 as text "lemma pair subset1" end text end define linebreak define pyk of lemma pair subset as text "lemma pair subset" end text end define linebreak define pyk of lemma same pair as text "lemma same pair" end text end define linebreak define pyk of lemma same singleton as text "lemma same singleton" end text end define linebreak define pyk of lemma union subset as text "lemma union subset" end text end define linebreak define pyk of lemma same union as text "lemma same union" end text end define linebreak define pyk of lemma separation subset as text "lemma separation subset" end text end define linebreak define pyk of lemma same binary union as text "lemma same binary union" end text end define linebreak define pyk of lemma same separation as text "lemma same separation" end text end define linebreak define pyk of lemma intersection subset as text "lemma intersection subset" end text end define linebreak define pyk of lemma same intersection as text "lemma same intersection" end text end define linebreak define pyk of lemma equivalence classes are disjoint as text "lemma equivalence classes are disjoint" end text end define linebreak define pyk of lemma transfer ~is0 as text "lemma transfer ~is0" end text end define linebreak define pyk of lemma transfer ~is as text "lemma transfer ~is" end text end define linebreak define pyk of lemma all disjoint as text "lemma all disjoint" end text end define linebreak define pyk of lemma all disjoint-imply as text "lemma all disjoint-imply" end text end define linebreak define pyk of theorem eq-system is partition as text "theorem eq-system is partition" end text end define linebreak define pyk of intersection x comma x end intersection as text "intersection "! comma "! end intersection" end text end define linebreak define pyk of eq-system of x modulo x as text "eq-system of "! modulo "!" end text end define linebreak define pyk of union x end union as text "union "! end union" end text end define linebreak define pyk of power x end power as text "power "! end power" end text end define linebreak define pyk of binary-union x comma x end union as text "binary-union "! comma "! end union" end text end define linebreak define pyk of zermelo singleton x end singleton as text "zermelo singleton "! end singleton" end text end define linebreak define pyk of x zermelo pair x as text ""! zermelo pair "!" end text end define linebreak define pyk of x zermelo ordered pair x as text ""! zermelo ordered pair "!" end text end define linebreak define pyk of x zermelo in x as text ""! zermelo in "!" end text end define linebreak define pyk of x zermelo ~in x as text ""! zermelo ~in "!" end text end define linebreak define pyk of x is partition of x as text ""! is partition of "!" end text end define linebreak define pyk of x is related to x under x as text ""! is related to "! under "!" end text end define linebreak define pyk of x is reflexive relation in x as text ""! is reflexive relation in "!" end text end define linebreak define pyk of x is symmetric relation in x as text ""! is symmetric relation in "!" end text end define linebreak define pyk of x is transitive relation in x as text ""! is transitive relation in "!" end text end define linebreak define pyk of x is equivalence relation in x as text ""! is equivalence relation in "!" end text end define linebreak define pyk of equivalence class of x in x modulo x as text "equivalence class of "! in "! modulo "!" end text end define linebreak define pyk of x zermelo is x as text ""! zermelo is "!" end text end define linebreak define pyk of x is subset of x as text ""! is subset of "!" end text end define linebreak define pyk of not0 x as text "not0 "!" end text end define linebreak define pyk of x zermelo ~is x as text ""! zermelo ~is "!" end text end define linebreak define pyk of x and0 x as text ""! and0 "!" end text end define linebreak define pyk of x or0 x as text ""! or0 "!" end text end define linebreak define pyk of x iff x as text ""! iff "!" end text end define linebreak define pyk of the set of ph in x such that x end set as text "the set of ph in "! such that "! end set" end text end define linebreak define pyk of eriksen as text "eriksen" end text end define linebreak unicode end of text end protect end math ] "
\end{flushleft}
" [ math var a end math ] "
\display{" [ math tex define eriksen as "Frozen" end define end math ] "}
\display{" [ math tex define meta big set as "\mathsf {BS}" end define end math ] "}
\display{" [ math tex define var x and0 var y as "#1.
\mathrel{\dot{\wedge}} #2." end define end math ] "}
\display{" [ math tex define zermelo empty set as "\mathrm{\O}" end define end math ] "}
\display{" [ math tex define not0 var x as "\dot{\neg}\, #1." end define end math ] "}
" [ math tex define var x iff var y as "#1.
\mathrel{\dot{\Leftrightarrow}} #2." end define end math ] "
\display{" [ math tex define var x zermelo pair var y as "\{#1.
,#2.
\}" end define end math ] "}
\display{" [ math tex define zermelo singleton var x end singleton as "\{#1.
\}" end define end math ] "},
\display{" [ math tex define axiom pair definition as "PairDef" end define end math ] "}
\display{" [ math tex define var x zermelo is var y as "#1.
\mathrel{=} #2." end define end math ] "}
\display{" [ math tex define var x zermelo in var y as "#1.
\mathrel{\in} #2." end define end math ] "}
\display{" [ math tex define var x zermelo ordered pair var y as "\langle #1.
,#2.
\rangle" end define end math ] "},
\display{" [ math tex define var r is reflexive relation in var x as "ReflRel(#1.
,#2.
)" end define end math ] "},
\display{" [ math tex define var r is symmetric relation in var x as "SymRel(#1.
,#2.
)" end define end math ] "},
\display{" [ math tex define var r is transitive relation in var x as "TransRel(#1.
,#2.
)" end define end math ] "},
\display{" [ math tex define var r is equivalence relation in var x as "EqRel(#1.
,#2.
)" end define end math ] "},
\display{" [ math tex define var x is related to var y under var z as "#3.
(#1.
,#2.
)" end define end math ] "},
" [ math tex define ph-sub var x is var y where var z is var u end sub as "\langle #1.
{\equiv} #2.
| #3.
{:=} #4.
\rangle_{Ph} " end define end math ] "
" [ math tex define ph-sub0 var x is var y where var z is var u end sub as "\langle #1.
{\equiv}^0 #2.
| #3.
{:=} #4.
\rangle_{Ph} " end define end math ] "
" [ math tex define ph-sub1 var x is var y where var z is var u end sub as "\langle #1.
{\equiv}^1 #2.
| #3.
{:=} #4.
\rangle_{Ph} " end define end math ] "
" [ math tex define ph-sub* var x is var y where var z is var u end sub as "\langle #1.
{\equiv}^* #2.
| #3.
{:=} #4.
\rangle_{Ph} " end define end math ] "
\display{" [ math tex define system zf as "ZF\ast{}" end define end math ] "}
\display{" [ math tex define 1rule mp as "MP" end define end math ] "}
\display{" [ math tex define 1rule deduction as "Ded" end define end math ] "}
\display{" [ math tex define 1rule gen as "Gen" end define end math ] "}
\display{" [ math tex define 1rule ad absurdum as "Neg" end define end math ] "}
\display{" [ math tex define op2 var x comma var y end op2 as "Op(#1.
,#2.
)" end define end math ] "}
\display{" [ math tex define op var x end op as "Op(#1.
)" end define end math ] "}
\display{" [ math tex define 1rule repetition as "Repetition" end define end math ] "}
\display{" [ math tex define axiom extensionality as "Extensionality" end define end math ] "}
\display{" [ math tex define axiom separation definition as "SeparationDef" end define end math ] "}
\display{" [ math tex define the set of ph in var x such that var a end set as " \{ ph \mathrel{\in} #1.
\mid #2.
\}" end define end math ] "}
\display{" [ math tex define var x or0 var y as "#1.
\mathrel{\dot{\vee}} #2." end define end math ] "}
\display{" [ math tex define cdots as "(\cdots{})" end define end math ] "}
\display{" [ math tex define equivalence class of var x in var big set modulo var r as "[#1.
\mathrel{\in} #2.
]_{#3.
}" end define end math ] "}
\display{" [ math tex define object big set as " \mathsf {OBS}" end define end math ] "}
\display{" [ math tex define axiom union definition as "UnionDef" end define end math ] "}
\display{" [ math tex define union var x end union as "\cup #1." end define end math ] "}
\display{" [ math tex define placeholder-var1 as "ph_{1}" end define end math ] "}
\display{" [ math tex define placeholder-var2 as "ph_{2}" end define end math ] "}
\display{" [ math tex define placeholder-var3 as "ph_{3}" end define end math ] "}
\display{" [ math tex define cheating axiom all disjoint as "Cheat-AllDisjoint" end define end math ] "}
\display{" [ math tex define power var x end power as "P(#1.
)" end define end math ] "}
\display{" [ math tex define axiom power definition as "PowerDef" end define end math ] "}
\display{" [ math tex define intersection var x comma var y end intersection as "#1.
\cap #2." end define end math ] "}
\display{" [ math tex define var x zermelo ~is var y as "#1.
\mathrel{\neq} #2." end define end math ] "}
\display{" [ math tex define var x is partition of var y as "Partition(#1.
,#2.
)" end define end math ] "}
\display{" [ math tex define var x zermelo ~in var y as "#1.
\mathrel{\notin} #2." end define end math ] "}
\display{" [ math tex define binary-union var x comma var y end union as "#1.
\mathrel{\cup} #2." end define end math ] "}
\display{" [ math tex define var x is subset of var y as "#1.
\mathrel{\subseteq} #2." end define end math ] "}
\display{" [ math tex define eq-system of var x modulo var y as "#1.
\mathrel{\setminus} #2." end define end math ] "}
\display{" [ math tex define ex1 as "Ex_{1}" end define end math ] "}
\display{" [ math tex define ex2 as "Ex_{2}" end define end math ] "}
\display{" [ math tex define ex10 as "Ex_{10}" end define end math ] "}
\display{" [ math tex define ex20 as "Ex_{20}" end define end math ] "}
\display{" [ math tex define object-var as "\texttt{Objekt-var}" end define end math ] "}
\display{" [ math tex define contains-empty var x end empty as "ContainsEmpty(#1.
)" end define end math ] "}
\display{" [ math tex define ex-var as "\texttt{Ex-var}" end define end math ] "}
\display{" [ math tex define ph-var as "\texttt{Ph-var}" end define end math ] "}
\display{" [ math tex define vaerdi as "\texttt{V\ae{}rdi}" end define end math ] "}
\display{" [ math tex define variabel as "\texttt{Variabel}" end define end math ] "}
\display{" [ math tex define 1rule exist intro as "ExistIntro" end define end math ] "}
\display{" [ math tex define existential var var x end var as "#1.
_{Ex}" end define end math ] "}
\display{" [ math tex define var x is existential var as "#1.
^{Ex}" end define end math ] "}
\display{" [ math tex define placeholder-var var x end var as "#1.
_{Ph} " end define end math ] "}
\display{" [ math tex define var x is placeholder-var as "#1.
^{Ph}" end define end math ] "}
" [ math tex define exist-sub var x is var y where var z is var u end sub as "\langle #1.
{\equiv} #2.
| #3.
{:=} #4.
\rangle_{Ex} " end define end math ] "
" [ math tex define exist-sub0 var x is var y where var z is var u end sub as "\langle #1.
{\equiv}^0 #2.
| #3.
{:=} #4.
\rangle_{Ex} " end define end math ] "
" [ math tex define exist-sub1 var x is var y where var z is var u end sub as "\langle #1.
{\equiv}^1 #2.
| #3.
{:=} #4.
\rangle_{Ex} " end define end math ] "
" [ math tex define exist-sub* var x is var y where var z is var u end sub as "\langle #1.
{\equiv}^* #2.
| #3.
{:=} #4.
\rangle_{Ex} " end define end math ] "
" [ math tex define 1deduction var x conclude var y end 1deduction as "
Dedu(#1.
,#2.
)" end define end math ] "
" [ math tex define 1deduction zero var x conclude var y end 1deduction as "
Dedu_0(#1.
,#2.
)" end define end math ] "
" [ math tex define 1deduction side var x conclude var y condition var z end 1deduction as "Dedu_{s}(#1.
,#2.
,#3.
)" end define end math ] "
" [ math tex define 1deduction one var x conclude var y condition var z end 1deduction as "
Dedu_1(#1.
,#2.
,#3.
)" end define end math ] "
" [ math tex define 1deduction two var x conclude var y condition var z end 1deduction as "
Dedu_2(#1.
,#2.
,#3.
)" end define end math ] "
" [ math tex define 1deduction three var x conclude var y condition var z bound var u end 1deduction as "
Dedu_3(#1.
,#2.
,#3.
,#4.
)" end define end math ] "
" [ math tex define 1deduction four var x conclude var y condition var z bound var u end 1deduction as "
Dedu_4(#1.
,#2.
,#3.
,#4.
)" end define end math ] "
" [ math tex define 1deduction four star var x conclude var y condition var z bound var u end 1deduction as "
Dedu_4^*(#1.
,#2.
,#3.
,#4.
)" end define end math ] "
" [ math tex define 1deduction five var x condition var y bound var z end 1deduction as "
Dedu_5(#1.
,#2.
,#3.
)" end define end math ] "
" [ math tex define 1deduction six var p conclude var c exception var e bound var b end 1deduction as "
Dedu_6(#1.
,#2.
,#3.
,#4.
)" end define end math ] "
" [ math tex define 1deduction six star var p conclude var c exception var e bound var b end 1deduction as "
Dedu_6^*(#1.
,#2.
,#3.
,#4.
)" end define end math ] "
" [ math tex define 1deduction seven var p end 1deduction as "
Dedu_7(#1.
)" end define end math ] "
" [ math tex define 1deduction eight var p bound var b end 1deduction as "
Dedu_8(#1.
,#2.
)" end define end math ] "
" [ math tex define 1deduction eight star var p bound var b end 1deduction as "
Dedu_8^*(#1.
,#2.
)" end define end math ] "
" [ math tex define meta big set as "{\cal BS}" end define end math ] "
\display{" [ math tex define lemma reflexivity as "Reflexivity" end define end math ] "}
\display{" [ math tex define lemma symmetry as "Symmetry" end define end math ] "}
\display{" [ math tex define lemma transitivity as "Transitivity" end define end math ] "},
\display{" [ math tex define prop lemma weakening as "Weakening" end define end math ] "}
\display{" [ math tex define prop lemma negative mt as "NegativeMT" end define end math ] "}
\display{" [ math tex define prop lemma technicality as "Technicality" end define end math ] "}
\display{" [ math tex define prop lemma mt as "MT" end define end math ] "}
\display{" [ math tex define prop lemma add double neg as "AddDoubleNeg" end define end math ] "}
\display{" [ math tex define prop lemma remove double neg as "RemoveDoubleNeg" end define end math ] "}
\display{" [ math tex define prop lemma first conjunct as "FirstConjunct" end define end math ] "}
\display{" [ math tex define prop lemma and commutativity as "AndCommutativity" end define end math ] "}
\display{" [ math tex define prop lemma second conjunct as "SecondConjunct" end define end math ] "}
\display{" [ math tex define prop lemma join conjuncts as "JoinConjuncts" end define end math ] "}
\display{" [ math tex define lemma separation2formula as "Sep2Formula" end define end math ] "}
\display{" [ math tex define lemma formula2separation as "Formula2Sep" end define end math ] "}
\display{" [ math tex define lemma set equality suff condition as "ToSetEquality" end define end math ] "}
\display{" [ math tex define lemma er is transitive as "ERisTransitive" end define end math ] "}
\display{" [ math tex define lemma er is symmetric as "ERisSymmetric" end define end math ] "}
\display{" [ math tex define lemma equivalence nec condition as "EqNecessary" end define end math ] "}
\display{" [ math tex define lemma equivalence nec condition0 as "HelperEqNecessary" end define end math ] "}
\display{" [ math tex define lemma eq subset0 as "HelperTransSubset" end define end math ] "}
\display{" [ math tex define lemma eq subset as "TransSubset" end define end math ] "}
\display{" [ math tex define prop lemma mp2 as "MP2" end define end math ] "}
\display{" [ math tex define prop lemma mp3 as "MP3" end define end math ] "}
\display{" [ math tex define prop lemma mp4 as "MP4" end define end math ] "}
\display{" [ math tex define prop lemma mp5 as "MP5" end define end math ] "}
\display{" [ math tex define prop lemma iff first as "IffFirst" end define end math ] "}
\display{" [ math tex define prop lemma iff second as "IffSecond" end define end math ] "}
\display{" [ math tex define prop lemma contrapositive as "Contrapositive" end define end math ] "}
\display{" [ math tex define prop lemma from contradiction as "FromContradiction" end define end math ] "}
\display{" [ math tex define lemma reflexivity0 as "HelperReflexivity" end define end math ] "}
\display{" [ math tex define lemma symmetry0 as "HelperSymmetry" end define end math ] "}
\display{" [ math tex define lemma transitivity0 as "HelperTransitivity" end define end math ] "}
\display{" [ math tex define lemma auto member as "AutoMember" end define end math ] "}
\display{" [ math tex define lemma set equality skip quantifier as "HelperFromSetEquality" end define end math ] "}
\display{" [ math tex define lemma set equality nec condition as "FromSetEquality" end define end math ] "}
\display{" [ math tex define lemma empty set is subset as "EmptySetSub" end define end math ] "}
\display{" [ math tex define lemma unique empty set0 as "HelperUniqueEmptySet" end define end math ] "}
\display{" [ math tex define lemma unique empty set as "UniqueEmptySet" end define end math ] "}
\display{" [ math tex define lemma none-equivalence nec condition0 as "HelperNoneEqNecessary" end define end math ] "}
\display{" [ math tex define lemma none-equivalence nec condition1 as "Helper(2)NoneEqNecessary" end define end math ] "}
\display{" [ math tex define lemma none-equivalence nec condition as "NoneEqNecessary" end define end math ] "}
\display{" [ math tex define prop lemma auto imply as "AutoImply" end define end math ] "}
\display{" [ math tex define prop lemma imply transitivity as "ImplyTransitivity" end define end math ] "}
\display{" [ math tex define lemma member not empty as "MemberNotEmpty" end define end math ] "}
\display{" [ math tex define lemma member not empty0 as "HelperMemberNotEmpty" end define end math ] "}
\display{" [ math tex define lemma =reflexivity as "=Reflexivity" end define end math ] "}
\display{" [ math tex define lemma =symmetry as "=Symmetry" end define end math ] "}
\display{" [ math tex define lemma =transitivity0 as "Helper=Transitivity" end define end math ] "}
\display{" [ math tex define lemma =transitivity as "=Transitivity" end define end math ] "}
\display{" [ math tex define lemma formula2union as "Formula2Union" end define end math ] "}
\display{" [ math tex define lemma union2formula as "Union2Formula" end define end math ] "}
\display{" [ math tex define lemma subset transitive as "SubsetTransitive" end define end math ] "}
\display{" [ math tex define lemma subset in power set as "SubsetInPower" end define end math ] "}
\display{" [ math tex define lemma power set is subset0 as "HelperPowerIsSub" end define end math ] "}
\display{" [ math tex define lemma power set is subset0-switch as "Helper(Switch)PowerIsSub" end define end math ] "}
\display{" [ math tex define lemma power set is subset as "PowerIsSub" end define end math ] "}
\display{" [ math tex define lemma power set is subset-switch as "PowerIsSub-Switch" end define end math ] "}
\display{" [ math tex define lemma equivalence class is subset as "EqClassIsSubset" end define end math ] "}
\display{" [ math tex define lemma bs subset union(bs/r) as "BS-subset" end define end math ] "}
\display{" [ math tex define lemma union(bs/r) subset bs as "Union(BS-R)-subset" end define end math ] "}
\display{" [ math tex define lemma union(bs/r) is bs as "Union-Identity" end define end math ] "}
\display{" [ math tex define lemma eq-system not empty0 as "HelperEqSysNot\O{}" end define end math ] "}
\display{" [ math tex define lemma eq-system not empty as "EqSysNot\O{}" end define end math ] "}
\display{" [ math tex define prop lemma weaken or first as "WeakenOr1" end define end math ] "}
\display{" [ math tex define prop lemma weaken or second as "WeakenOr2" end define end math ] "}
\display{" [ math tex define prop lemma from disjuncts as "FromDisjuncts" end define end math ] "}
\display{" [ math tex define prop lemma iff commutativity as "IffCommutativity" end define end math ] "}
\display{" [ math tex define lemma union subset as "HelperSameUnion" end define end math ] "}
\display{" [ math tex define lemma same union as "SameUnion" end define end math ] "}
\display{" [ math tex define lemma pair2formula as "Pair2Formula" end define end math ] "}
\display{" [ math tex define lemma formula2pair as "Formula2Pair" end define end math ] "}
\display{" [ math tex define lemma pair subset0 as "HelperPairSubset" end define end math ] "}
\display{" [ math tex define lemma pair subset1 as "Helper(2)PairSubset" end define end math ] "}
\display{" [ math tex define lemma pair subset as "PairSubset" end define end math ] "}
\display{" [ math tex define lemma same pair as "SamePair" end define end math ] "}
\display{" [ math tex define lemma same singleton as "SameSingleton" end define end math ] "}
\display{" [ math tex define lemma separation subset as "SeparationSubset" end define end math ] "}
\display{" [ math tex define lemma same binary union as "SameBinaryUnion" end define end math ] "}
\display{" [ math tex define lemma same separation as "SameSeparation" end define end math ] "}
\display{" [ math tex define lemma intersection subset as "IntersectionSubset" end define end math ] "}
\display{" [ math tex define lemma same intersection as "SameIntersection" end define end math ] "}
\display{" [ math tex define lemma equivalence classes are disjoint as "EqClassesAreDisjoint" end define end math ] "}
\display{" [ math tex define lemma transfer ~is0 as "HelperTransfer\neq{}" end define end math ] "}
\display{" [ math tex define lemma transfer ~is as "Transfer\neq{}" end define end math ] "}
\display{" [ math tex define lemma all disjoint as "AllDisjoint" end define end math ] "}
\display{" [ math tex define lemma all disjoint-imply as "Imply-AllDisjoint" end define end math ] "}
\display{" [ math tex define theorem eq-system is partition as "Eq-SystemIsPartition" end define end math ] "}
\end{document}
End of file
latex page
latex page
dvipdfm page"
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,