Logiweb expansion of prove in pyk

Up Help

"File page.tex
\documentclass [fleqn,titlepage]{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]{}}

% tilfoejede pakker
\usepackage{lscape}
\usepackage{multicol}
\usepackage{float}
\usepackage[latin1]{inputenc}
\usepackage[dvips]{graphicx}
\usepackage{verbatim}
\usepackage[danish]{babel}
\usepackage{graphpap}

\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 130 490 730}}
%\hypersetup{pdftitle=}
\hypersetup{colorlinks=false}
\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}

\floatplacement{figure}{h!}
\floatplacement{table}{h!}
\hyphenation{her-ud-over ek-si-stens-va-ri-ab-le an-dre dob-belt-im-pli-ka-ti-on ob-jekt-kvan-tor de-fi-ni-tions-lem-ma ens-be-tyd-en-de
und-er-af-snit slut-ning-en inde-hol-der for-klar-ing-en si-de-be-ting-el-sen
des-uden be-vis-check-er-en}

ny----

" [ math define tex of var x < <<test#2." end text end define end math ] "

" [ math define tex of < )" end text end define end math ] "

" [ math define macro of var x <
" [ math define value of <
(*****)

" [ math the set of ph in power the set of ph in power the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end power such that not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 placeholder-var var f end var imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 placeholder-var var f end var imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 placeholder-var var f end var imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 placeholder-var var f end var end set end power such that for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var d end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ var a ; metavar var m end metavar ] + [ var b ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var d end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ var a ; metavar var m end metavar ] + [ var b ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | = object var var ep end var end set end math ] " 1

" [ math the set of ph in power the set of ph in power the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end power such that not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 placeholder-var var f end var imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 placeholder-var var f end var imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 placeholder-var var f end var imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 placeholder-var var f end var end set end power such that for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var d end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var d end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ var a ; metavar var m end metavar ] + [ var b ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] + [ var c ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var d end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var d end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ var a ; metavar var m end metavar ] + [ var b ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] + [ var c ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | = object var var ep end var end set end math ] " 2

" [ math the set of ph in power the set of ph in power the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end power such that not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 placeholder-var var f end var imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 placeholder-var var f end var imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 placeholder-var var f end var imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 placeholder-var var f end var end set end power such that for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ var a ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ var a ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | = object var var ep end var end set end math ] " 3

" [ math the set of ph in power the set of ph in power the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end power such that not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 placeholder-var var f end var imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 placeholder-var var f end var imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 placeholder-var var f end var imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 placeholder-var var f end var end set end power such that for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ var a ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ var a ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | = object var var ep end var end set end math ] " 4

" [ math the set of ph in power the set of ph in power the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end power such that not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 placeholder-var var f end var imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 placeholder-var var f end var imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 placeholder-var var f end var imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 placeholder-var var f end var end set end power such that for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ var a ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ var a ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | = object var var ep end var end set end math ] " 5

" [ math the set of ph in power the set of ph in power the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end power such that not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 placeholder-var var f end var imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 placeholder-var var f end var imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 placeholder-var var f end var imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 placeholder-var var f end var end set end power such that for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ var a ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ var a ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | = object var var ep end var end set end math ] " 6

" [ math the set of ph in power the set of ph in power the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end power such that not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 placeholder-var var f end var imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 placeholder-var var f end var imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 placeholder-var var f end var imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 placeholder-var var f end var end set end power such that for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ var a ; metavar var m end metavar ] * [ var b ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ var a ; metavar var m end metavar ] * [ var b ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | = object var var ep end var end set end math ] " 7

" [ math the set of ph in power the set of ph in power the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end power such that not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 placeholder-var var f end var imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 placeholder-var var f end var imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 placeholder-var var f end var imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 placeholder-var var f end var end set end power such that for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ var a ; metavar var m end metavar ] * [ var b ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ var a ; metavar var m end metavar ] * [ var b ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | = object var var ep end var end set end math ] " 8

" [ math the set of ph in power the set of ph in power the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end power such that not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 placeholder-var var f end var imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 placeholder-var var f end var imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 placeholder-var var f end var imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 placeholder-var var f end var end set end power such that for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ metavar var fx end metavar ; metavar var m end metavar ] * [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects object var var crs1 end var indeed not0 placeholder-var var c end var = zermelo pair zermelo pair object var var crs1 end var comma object var var crs1 end var end pair comma zermelo pair object var var crs1 end var comma 0 end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ metavar var fx end metavar ; metavar var m end metavar ] * [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects object var var crs1 end var indeed not0 placeholder-var var c end var = zermelo pair zermelo pair object var var crs1 end var comma object var var crs1 end var end pair comma zermelo pair object var var crs1 end var comma 0 end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | = object var var ep end var end set end math ] " 8a

" [ math the set of ph in power the set of ph in power the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end power such that not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 placeholder-var var f end var imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 placeholder-var var f end var imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 placeholder-var var f end var imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 placeholder-var var f end var end set end power such that for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ metavar var fx end metavar ; metavar var m end metavar ] * [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects object var var crs1 end var indeed not0 placeholder-var var c end var = zermelo pair zermelo pair object var var crs1 end var comma object var var crs1 end var end pair comma zermelo pair object var var crs1 end var comma 0 end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ metavar var fx end metavar ; metavar var m end metavar ] * [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects object var var crs1 end var indeed not0 placeholder-var var c end var = zermelo pair zermelo pair object var var crs1 end var comma object var var crs1 end var end pair comma zermelo pair object var var crs1 end var comma 0 end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | = object var var ep end var end set end math ] " 8b


" [ math the set of ph in power the set of ph in power the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end power such that not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 placeholder-var var f end var imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 placeholder-var var f end var imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 placeholder-var var f end var imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 placeholder-var var f end var end set end power such that for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ var a ; metavar var m end metavar ] * [ var b ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] * [ var c ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ var a ; metavar var m end metavar ] * [ var b ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] * [ var c ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | = object var var ep end var end set end math ] " 8

" [ math the set of ph in power the set of ph in power the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end power such that not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 placeholder-var var f end var imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 placeholder-var var f end var imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 placeholder-var var f end var imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 placeholder-var var f end var end set end power such that for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var d end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ var a ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] * [ var b ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] + [ var c ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var d end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ var a ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] * [ var b ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] + [ var c ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | = object var var ep end var end set end math ] " 9

" [ math not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n end var <= object var var m end var imply [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ var a ; metavar var m end metavar ] * [ var b ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] * [ var c ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] <= [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var d end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var e end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ var a ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] * [ var b ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] + [ var c ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - object var var ep end var end math ] " 10

" [ math not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n end var <= object var var m end var imply [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma - [ var a ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] <= [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var d end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ the set of ph in the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set such that not0 for all objects metavar var m end metavar indeed not0 placeholder-var var d end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma [ var b ; metavar var m end metavar ] + [ var b ; metavar var m end metavar ] end pair end pair end set ; metavar var m end metavar ] + [ var c ; metavar var m end metavar ] end pair end pair end set ; object var var m end var ] + - object var var ep end var end math ] " 11

" [ math the set of ph in power the set of ph in power the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end power such that not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 placeholder-var var f end var imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 placeholder-var var f end var imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 placeholder-var var f end var imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 placeholder-var var f end var end set end power such that for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ var a ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ var a ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | = object var var ep end var end set end math ] " 12

" [ math the set of ph in power the set of ph in power the set of ph in power power U( zermelo pair N comma Q end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end power such that not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 placeholder-var var f end var imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 placeholder-var var f end var imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 placeholder-var var f end var imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 placeholder-var var f end var end set end power such that for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ var b ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ var b ; object var var m end var ] + - [ placeholder-var var d end var ; object var var m end var ] | = object var var ep end var end set end math ] " 13

" [ math not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n end var <= object var var m end var imply [ var a ; object var var m end var ] <= [ var b ; object var var m end var ] + - object var var ep end var end math ] " 14

" [ math var b end math ] " 15





venter----


\appendix

" [ flush left math define priority of prove as preassociative priority prove equal priority base equal priority bracket x end bracket equal priority big bracket x end bracket equal priority math x end math equal priority flush left x end left equal priority var x equal priority var y equal priority var z equal priority proclaim x as x end proclaim equal priority define x of x as x end define equal priority pyk equal priority tex equal priority tex name equal priority priority equal priority x equal priority true equal priority if x then x else x end if equal priority introduce x of x as x end introduce equal priority value equal priority claim equal priority bottom equal priority function f of x end function equal priority identity x end identity equal priority false equal priority untagged zero equal priority untagged one equal priority untagged two equal priority untagged three equal priority untagged four equal priority untagged five equal priority untagged six equal priority untagged seven equal priority untagged eight equal priority untagged nine equal priority zero equal priority one equal priority two equal priority three equal priority four equal priority five equal priority six equal priority seven equal priority eight equal priority nine equal priority var a equal priority var b equal priority var c equal priority var d equal priority var e equal priority var f equal priority var g equal priority var h equal priority var i equal priority var j equal priority var k equal priority var l equal priority var m equal priority var n equal priority var o equal priority var p equal priority var q equal priority var r equal priority var s equal priority var t equal priority var u equal priority var v equal priority var w equal priority tagged parenthesis x end tagged equal priority tagged if x then x else x end if equal priority array x is x end array equal priority left equal priority center equal priority right equal priority empty equal priority substitute x set x to x end substitute equal priority map tag x end tag equal priority raw map untag x end untag equal priority map untag x end untag equal priority normalizing untag x end untag equal priority apply x to x end apply equal priority apply one x to x end apply equal priority identifier x end identifier equal priority identifier one x plus id x end identifier equal priority array plus x and x end plus equal priority array remove x array x level x end remove equal priority array put x value x array x level x end put equal priority array add x value x index x value x level x end add equal priority bit x of x end bit equal priority bit one x of x end bit equal priority example rack equal priority vector hook equal priority bibliography hook equal priority dictionary hook equal priority body hook equal priority codex hook equal priority expansion hook equal priority code hook equal priority cache hook equal priority diagnose hook equal priority pyk aspect equal priority tex aspect equal priority texname aspect equal priority value aspect equal priority message aspect equal priority macro aspect equal priority definition aspect equal priority unpack aspect equal priority claim aspect equal priority priority aspect equal priority lambda identifier equal priority apply identifier equal priority true identifier equal priority if identifier equal priority quote identifier equal priority proclaim identifier equal priority define identifier equal priority introduce identifier equal priority hide identifier equal priority pre identifier equal priority post identifier equal priority eval x stack x cache x end eval equal priority eval two x ref x id x stack x cache x end eval equal priority eval three x function x stack x cache x end eval equal priority eval four x arguments x stack x cache x end eval equal priority lookup x stack x default x end lookup equal priority abstract x term x stack x cache x end abstract equal priority quote x end quote equal priority expand x state x cache x end expand equal priority expand two x definition x state x cache x end expand equal priority expand list x state x cache x end expand equal priority macro equal priority macro state equal priority zip x with x end zip equal priority assoc one x address x index x end assoc equal priority protect x end protect equal priority self equal priority macro define x as x end define equal priority value define x as x end define equal priority intro define x as x end define equal priority pyk define x as x end define equal priority tex define x as x end define equal priority tex name define x as x end define equal priority priority table x end table equal priority macro define one equal priority macro define two x end define equal priority macro define three x end define equal priority macro define four x state x cache x definition x end define equal priority state expand x state x cache x end expand equal priority quote expand x term x stack x end expand equal priority quote expand two x term x stack x end expand equal priority quote expand three x term x stack x value x end expand equal priority quote expand star x term x stack x end expand equal priority parenthesis x end parenthesis equal priority big parenthesis x end parenthesis equal priority display x end display equal priority statement x end statement equal priority spying test x end test equal priority false spying test x end test equal priority aspect x subcodex x end aspect equal priority aspect x term x cache x end aspect equal priority tuple x end tuple equal priority tuple one x end tuple equal priority tuple two x end tuple equal priority let two x apply x end let equal priority let one x apply x end let equal priority claim define x as x end define equal priority checker equal priority check x cache x end check equal priority check two x cache x def x end check equal priority check three x cache x def x end check equal priority check list x cache x end check equal priority check list two x cache x value x end check equal priority test x end test equal priority false test x end test equal priority raw test x end test equal priority message equal priority message define x as x end define equal priority the statement aspect equal priority statement equal priority statement define x as x end define equal priority example axiom equal priority example scheme equal priority example rule equal priority absurdity equal priority contraexample equal priority example theory primed equal priority example lemma equal priority metavar x end metavar equal priority meta a equal priority meta b equal priority meta c equal priority meta d equal priority meta e equal priority meta f equal priority meta g equal priority meta h equal priority meta i equal priority meta j equal priority meta k equal priority meta l equal priority meta m equal priority meta n equal priority meta o equal priority meta p equal priority meta q equal priority meta r equal priority meta s equal priority meta t equal priority meta u equal priority meta v equal priority meta w equal priority meta x equal priority meta y equal priority meta z equal priority sub x set x to x end sub equal priority sub star x set x to x end sub equal priority the empty set equal priority example remainder equal priority make visible x end visible equal priority intro x index x pyk x tex x end intro equal priority intro x pyk x tex x end intro equal priority error x term x end error equal priority error two x term x end error equal priority proof x term x cache x end proof equal priority proof two x term x end proof equal priority sequent eval x term x end eval equal priority seqeval init x term x end eval equal priority seqeval modus x term x end eval equal priority seqeval modus one x term x sequent x end eval equal priority seqeval verify x term x end eval equal priority seqeval verify one x term x sequent x end eval equal priority sequent eval plus x term x end eval equal priority seqeval plus one x term x sequent x end eval equal priority seqeval minus x term x end eval equal priority seqeval minus one x term x sequent x end eval equal priority seqeval deref x term x end eval equal priority seqeval deref one x term x sequent x end eval equal priority seqeval deref two x term x sequent x def x end eval equal priority seqeval at x term x end eval equal priority seqeval at one x term x sequent x end eval equal priority seqeval infer x term x end eval equal priority seqeval infer one x term x premise x sequent x end eval equal priority seqeval endorse x term x end eval equal priority seqeval endorse one x term x side x sequent x end eval equal priority seqeval est x term x end eval equal priority seqeval est one x term x name x sequent x end eval equal priority seqeval est two x term x name x sequent x def x end eval equal priority seqeval all x term x end eval equal priority seqeval all one x term x variable x sequent x end eval equal priority seqeval cut x term x end eval equal priority seqeval cut one x term x forerunner x end eval equal priority seqeval cut two x term x forerunner x sequent x end eval equal priority computably true x end true equal priority claims x cache x ref x end claims equal priority claims two x cache x ref x end claims equal priority the proof aspect equal priority proof equal priority lemma x says x end lemma equal priority proof of x reads x end proof equal priority in theory x lemma x says x end lemma equal priority in theory x antilemma x says x end antilemma equal priority in theory x rule x says x end rule equal priority in theory x antirule x says x end antirule equal priority verifier equal priority verify one x end verify equal priority verify two x proofs x end verify equal priority verify three x ref x sequents x diagnose x end verify equal priority verify four x premises x end verify equal priority verify five x ref x array x sequents x end verify equal priority verify six x ref x list x sequents x end verify equal priority verify seven x ref x id x sequents x end verify equal priority cut x and x end cut equal priority head x end head equal priority tail x end tail equal priority rule one x theory x end rule equal priority rule x subcodex x end rule equal priority rule tactic equal priority plus x and x end plus equal priority theory x end theory equal priority theory two x cache x end theory equal priority theory three x name x end theory equal priority theory four x name x sum x end theory equal priority example axiom lemma primed equal priority example scheme lemma primed equal priority example rule lemma primed equal priority contraexample lemma primed equal priority example axiom lemma equal priority example scheme lemma equal priority example rule lemma equal priority contraexample lemma equal priority example theory equal priority ragged right equal priority ragged right expansion equal priority parameter term x stack x seed x end parameter equal priority parameter term star x stack x seed x end parameter equal priority instantiate x with x end instantiate equal priority instantiate star x with x end instantiate equal priority occur x in x substitution x end occur equal priority occur star x in x substitution x end occur equal priority unify x with x substitution x end unify equal priority unify star x with x substitution x end unify equal priority unify two x with x substitution x end unify equal priority ell a equal priority ell b equal priority ell c equal priority ell d equal priority ell e equal priority ell f equal priority ell g equal priority ell h equal priority ell i equal priority ell j equal priority ell k equal priority ell l equal priority ell m equal priority ell n equal priority ell o equal priority ell p equal priority ell q equal priority ell r equal priority ell s equal priority ell t equal priority ell u equal priority ell v equal priority ell w equal priority ell x equal priority ell y equal priority ell z equal priority ell big a equal priority ell big b equal priority ell big c equal priority ell big d equal priority ell big e equal priority ell big f equal priority ell big g equal priority ell big h equal priority ell big i equal priority ell big j equal priority ell big k equal priority ell big l equal priority ell big m equal priority ell big n equal priority ell big o equal priority ell big p equal priority ell big q equal priority ell big r equal priority ell big s equal priority ell big t equal priority ell big u equal priority ell big v equal priority ell big w equal priority ell big x equal priority ell big y equal priority ell big z equal priority ell dummy equal priority sequent reflexivity equal priority tactic reflexivity equal priority sequent commutativity equal priority tactic commutativity equal priority the tactic aspect equal priority tactic equal priority tactic define x as x end define equal priority proof expand x state x cache x end expand equal priority proof expand list x state x cache x end expand equal priority proof state equal priority conclude one x cache x end conclude equal priority conclude two x proves x cache x end conclude equal priority conclude three x proves x lemma x substitution x end conclude equal priority conclude four x lemma x end conclude equal priority check equal priority general macro define x as x end define equal priority make root visible x end visible equal priority sequent example axiom equal priority sequent example rule equal priority sequent example contradiction equal priority sequent example theory equal priority sequent example lemma equal priority set x end set equal priority object var x end var equal priority object a equal priority object b equal priority object c equal priority object d equal priority object e equal priority object f equal priority object g equal priority object h equal priority object i equal priority object j equal priority object k equal priority object l equal priority object m equal priority object n equal priority object o equal priority object p equal priority object q equal priority object r equal priority object s equal priority object t equal priority object u equal priority object v equal priority object w equal priority object x equal priority object y equal priority object z equal priority sub x is x where x is x end sub equal priority sub zero x is x where x is x end sub equal priority sub one x is x where x is x end sub equal priority sub star x is x where x is x end sub equal priority deduction x conclude x end deduction equal priority deduction zero x conclude x end deduction equal priority deduction one x conclude x condition x end deduction equal priority deduction two x conclude x condition x end deduction equal priority deduction three x conclude x condition x bound x end deduction equal priority deduction four x conclude x condition x bound x end deduction equal priority deduction four star x conclude x condition x bound x end deduction equal priority deduction five x condition x bound x end deduction equal priority deduction six x conclude x exception x bound x end deduction equal priority deduction six star x conclude x exception x bound x end deduction equal priority deduction seven x end deduction equal priority deduction eight x bound x end deduction equal priority deduction eight star x bound x end deduction equal priority system s equal priority double negation equal priority rule mp equal priority rule gen equal priority deduction equal priority axiom s one equal priority axiom s two equal priority axiom s three equal priority axiom s four equal priority axiom s five equal priority axiom s six equal priority axiom s seven equal priority axiom s eight equal priority axiom s nine equal priority repetition equal priority lemma a one equal priority lemma a two equal priority lemma a four equal priority lemma a five equal priority prop three two a equal priority prop three two b equal priority prop three two c equal priority prop three two d equal priority prop three two e one equal priority prop three two e two equal priority prop three two e equal priority prop three two f one equal priority prop three two f two equal priority prop three two f equal priority prop three two g one equal priority prop three two g two equal priority prop three two g equal priority prop three two h one equal priority prop three two h two equal priority prop three two h equal priority block one x state x cache x end block equal priority block two x end block equal priority kvanti equal priority lemma uniqueMember equal priority lemma uniqueMember(Type) equal priority lemma sameSeries equal priority lemma a4 equal priority lemma sameMember equal priority 1rule Qclosed(Addition) equal priority 1rule Qclosed(Multiplication) equal priority 1rule fromCartProd(1) equal priority 1rule fromCartProd(2) equal priority constantRationalSeries( x ) equal priority cartProd( x , x ) equal priority P( x ) equal priority binaryUnion( x , x ) equal priority setOfRationalSeries equal priority isSubset( x , x ) equal priority (p x , x ) equal priority (s x ) equal priority cdots equal priority object-var equal priority ex-var equal priority ph-var equal priority vaerdi equal priority variabel equal priority op x end op equal priority op2 x comma x end op2 equal priority define-equal x comma x end equal equal priority contains-empty x end empty equal priority Nat( x ) equal priority 1deduction x conclude x end 1deduction equal priority 1deduction zero x conclude x end 1deduction equal priority 1deduction side x conclude x condition x end 1deduction equal priority 1deduction one x conclude x condition x end 1deduction equal priority 1deduction two x conclude x condition x end 1deduction equal priority 1deduction three x conclude x condition x bound x end 1deduction equal priority 1deduction four x conclude x condition x bound x end 1deduction equal priority 1deduction four star x conclude x condition x bound x end 1deduction equal priority 1deduction five x condition x bound x end 1deduction equal priority 1deduction six x conclude x exception x bound x end 1deduction equal priority 1deduction six star x conclude x exception x bound x end 1deduction equal priority 1deduction seven x end 1deduction equal priority 1deduction eight x bound x end 1deduction equal priority 1deduction eight star x bound x end 1deduction equal priority ex1 equal priority ex2 equal priority ex3 equal priority ex10 equal priority ex20 equal priority existential var x end var equal priority x is existential var equal priority exist-sub x is x where x is x end sub equal priority exist-sub0 x is x where x is x end sub equal priority exist-sub1 x is x where x is x end sub equal priority exist-sub* x is x where x is x end sub equal priority ph1 equal priority ph2 equal priority ph3 equal priority placeholder-var x end var equal priority x is placeholder-var equal priority ph-sub x is x where x is x end sub equal priority ph-sub0 x is x where x is x end sub equal priority ph-sub1 x is x where x is x end sub equal priority ph-sub* x is x where x is x end sub equal priority meta-sub x is x where x is x end sub equal priority meta-sub1 x is x where x is x end sub equal priority meta-sub* x is x where x is x end sub equal priority var big set equal priority object big set equal priority meta big set equal priority zermelo empty set equal priority system Q equal priority 1rule mp equal priority 1rule gen equal priority 1rule repetition equal priority 1rule ad absurdum equal priority 1rule deduction equal priority 1rule exist intro equal priority axiom extensionality equal priority axiom empty set equal priority axiom pair definition equal priority axiom union definition equal priority axiom power definition equal priority axiom separation definition equal priority prop lemma add double neg equal priority prop lemma remove double neg equal priority prop lemma and commutativity equal priority prop lemma auto imply equal priority prop lemma contrapositive equal priority prop lemma first conjunct equal priority prop lemma second conjunct equal priority prop lemma from contradiction equal priority prop lemma from disjuncts equal priority prop lemma iff commutativity equal priority prop lemma iff first equal priority prop lemma iff second equal priority prop lemma imply transitivity equal priority prop lemma join conjuncts equal priority prop lemma mp2 equal priority prop lemma mp3 equal priority prop lemma mp4 equal priority prop lemma mp5 equal priority prop lemma mt equal priority prop lemma negative mt equal priority prop lemma technicality equal priority prop lemma weakening equal priority prop lemma weaken or first equal priority prop lemma weaken or second equal priority lemma formula2pair equal priority lemma pair2formula equal priority lemma formula2union equal priority lemma union2formula equal priority lemma formula2separation equal priority lemma separation2formula equal priority lemma formula2power equal priority lemma subset in power set equal priority lemma power set is subset0 equal priority lemma power set is subset equal priority lemma power set is subset0-switch equal priority lemma power set is subset-switch equal priority lemma set equality suff condition equal priority lemma set equality suff condition(t)0 equal priority lemma set equality suff condition(t) equal priority lemma set equality skip quantifier equal priority lemma set equality nec condition equal priority lemma reflexivity0 equal priority lemma reflexivity equal priority lemma symmetry0 equal priority lemma symmetry equal priority lemma transitivity0 equal priority lemma transitivity equal priority lemma er is reflexive equal priority lemma er is symmetric equal priority lemma er is transitive equal priority lemma empty set is subset equal priority lemma member not empty0 equal priority lemma member not empty equal priority lemma unique empty set0 equal priority lemma unique empty set equal priority lemma ==Reflexivity equal priority lemma ==Symmetry equal priority lemma ==Transitivity0 equal priority lemma ==Transitivity equal priority lemma transfer ~is0 equal priority lemma transfer ~is equal priority lemma pair subset0 equal priority lemma pair subset1 equal priority lemma pair subset equal priority lemma same pair equal priority lemma same singleton equal priority lemma union subset equal priority lemma same union equal priority lemma separation subset equal priority lemma same separation equal priority lemma same binary union equal priority lemma intersection subset equal priority lemma same intersection equal priority lemma auto member equal priority lemma eq-system not empty0 equal priority lemma eq-system not empty equal priority lemma eq subset0 equal priority lemma eq subset equal priority lemma equivalence nec condition0 equal priority lemma equivalence nec condition equal priority lemma none-equivalence nec condition0 equal priority lemma none-equivalence nec condition1 equal priority lemma none-equivalence nec condition equal priority lemma equivalence class is subset equal priority lemma equivalence classes are disjoint equal priority lemma all disjoint equal priority lemma all disjoint-imply equal priority lemma bs subset union(bs/r) equal priority lemma union(bs/r) subset bs equal priority lemma union(bs/r) is bs equal priority theorem eq-system is partition equal priority var x1 equal priority var x2 equal priority var y1 equal priority var y2 equal priority var v1 equal priority var v2 equal priority var v3 equal priority var v4 equal priority var v2n equal priority var m1 equal priority var m2 equal priority var n1 equal priority var n2 equal priority var n3 equal priority var ep equal priority var ep1 equal priority var ep2 equal priority var fep equal priority var fx equal priority var fy equal priority var fz equal priority var fu equal priority var fv equal priority var fw equal priority var rx equal priority var ry equal priority var rz equal priority var ru equal priority var sx equal priority var sx1 equal priority var sy equal priority var sy1 equal priority var sz equal priority var sz1 equal priority var su equal priority var su1 equal priority var fxs equal priority var fys equal priority var crs1 equal priority var f1 equal priority var f2 equal priority var f3 equal priority var f4 equal priority var op1 equal priority var op2 equal priority var r1 equal priority var s1 equal priority var s2 equal priority meta x1 equal priority meta x2 equal priority meta y1 equal priority meta y2 equal priority meta v1 equal priority meta v2 equal priority meta v3 equal priority meta v4 equal priority meta v2n equal priority meta m1 equal priority meta m2 equal priority meta n1 equal priority meta n2 equal priority meta n3 equal priority meta ep equal priority meta ep1 equal priority meta ep2 equal priority meta fx equal priority meta fy equal priority meta fz equal priority meta fu equal priority meta fv equal priority meta fw equal priority meta fep equal priority meta rx equal priority meta ry equal priority meta rz equal priority meta ru equal priority meta sx equal priority meta sx1 equal priority meta sy equal priority meta sy1 equal priority meta sz equal priority meta sz1 equal priority meta su equal priority meta su1 equal priority meta fxs equal priority meta fys equal priority meta f1 equal priority meta f2 equal priority meta f3 equal priority meta f4 equal priority meta op1 equal priority meta op2 equal priority meta r1 equal priority meta s1 equal priority meta s2 equal priority object ep equal priority object crs1 equal priority object f1 equal priority object f2 equal priority object f3 equal priority object f4 equal priority object n1 equal priority object n2 equal priority object op1 equal priority object op2 equal priority object r1 equal priority object s1 equal priority object s2 equal priority ph4 equal priority ph5 equal priority ph6 equal priority NAT equal priority RATIONAL_SERIES equal priority SERIES equal priority setOfReals equal priority setOfFxs equal priority N equal priority Q equal priority X equal priority xs equal priority xsF equal priority ysF equal priority us equal priority usF equal priority 0 equal priority 1 equal priority (-1) equal priority 2 equal priority 3 equal priority 1/2 equal priority 1/3 equal priority 2/3 equal priority 0f equal priority 1f equal priority 00 equal priority 01 equal priority (--01) equal priority 02 equal priority 01//02 equal priority lemma plus0Left equal priority lemma times1Left equal priority lemma eqAdditionLeft equal priority lemma eqMultiplicationLeft equal priority lemma plusAssociativity(R) equal priority lemma plusAssociativity(R)XX equal priority lemma plus0(R) equal priority lemma negative(R) equal priority lemma times1(R) equal priority lemma lessAddition(R) equal priority lemma plusCommutativity(R) equal priority lemma leqAntisymmetry(R) equal priority lemma leqTransitivity(R) equal priority lemma leqAddition(R) equal priority lemma distribution(R) equal priority axiom a4 equal priority axiom induction equal priority axiom equality equal priority axiom eqLeq equal priority axiom eqAddition equal priority axiom eqMultiplication equal priority axiom QisClosed(reciprocal) equal priority lemma QisClosed(reciprocal) equal priority axiom QisClosed(negative) equal priority lemma QisClosed(negative) equal priority axiom leqReflexivity equal priority axiom leqAntisymmetry equal priority axiom leqTransitivity equal priority axiom leqTotality equal priority axiom leqAddition equal priority axiom leqMultiplication equal priority axiom plusAssociativity equal priority axiom plusCommutativity equal priority axiom negative equal priority axiom plus0 equal priority axiom timesAssociativity equal priority axiom timesCommutativity equal priority axiom reciprocal equal priority axiom times1 equal priority axiom distribution equal priority axiom 0not1 equal priority lemma eqLeq(R) equal priority lemma timesAssociativity(R) equal priority lemma timesCommutativity(R) equal priority lemma =f to sameF equal priority lemma plusF(Sym) equal priority lemma timesF(Sym) equal priority lemma separation2formula(1) equal priority lemma separation2formula(2) equal priority 1rule ifThenElse true equal priority 1rule ifThenElse false equal priority axiom cauchy equal priority axiom plusF equal priority axiom reciprocalF equal priority 1rule from== equal priority 1rule to== equal priority 1rule from<< equal priority 1rule to<< equal priority 1rule fromInR equal priority axiom plusR equal priority lemma plusR(Sym) equal priority axiom timesR equal priority lemma timesR(Sym) equal priority axiom reciprocalR equal priority 1rule lessMinus1(N) equal priority axiom nonnegative(N) equal priority axiom US0 equal priority 1rule nextXS(upperBound) equal priority 1rule nextXS(noUpperBound) equal priority 1rule nextUS(upperBound) equal priority 1rule nextUS(noUpperBound) equal priority 1rule expZero equal priority 1rule expPositive equal priority 1rule expZero(R) equal priority 1rule expPositive(R) equal priority 1rule base(1/2)Sum zero equal priority 1rule base(1/2)Sum positive equal priority 1rule UStelescope zero equal priority 1rule UStelescope positive equal priority 1rule adhoc eqAddition(R) equal priority 1rule unminus(R) equal priority 1rule fromLimit equal priority 1rule toUpperBound equal priority 1rule fromUpperBound equal priority axiom USisUpperBound equal priority axiom 0not1(R) equal priority 1rule expUnbounded equal priority 1rule fromLeq(Advanced)(N) equal priority 1rule fromLeastUpperBound equal priority 1rule toLeastUpperBound equal priority axiom XSisNotUpperBound equal priority axiom ysFGreater equal priority axiom ysFLess equal priority 1rule smallInverse equal priority axiom natType equal priority axiom rationalType equal priority axiom seriesType equal priority axiom max equal priority axiom numerical equal priority axiom memberOfSeries equal priority prop lemma doubly conditioned join conjuncts equal priority prop lemma imply negation equal priority prop lemma tertium non datur equal priority prop lemma from negated imply equal priority prop lemma to negated imply equal priority prop lemma from negated double imply equal priority prop lemma from negated and equal priority prop lemma from negated or equal priority prop lemma to negated or equal priority prop lemma from negations equal priority prop lemma from three disjuncts equal priority prop lemma from two times two disjuncts equal priority prop lemma negate first disjunct equal priority prop lemma negate second disjunct equal priority prop lemma expand disjuncts equal priority lemma set equality nec condition(1) equal priority lemma set equality nec condition(2) equal priority lemma lessLeq(R) equal priority lemma memberOfSeries equal priority lemma memberOfSeries(Type) equal priority <
\section{Pyk definitioner} \label{sec:pyk}

\begin{flushleft}
" [ math define pyk of < \end{flushleft}

\newpage

\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}

\item " [ math define tex of prove as text "prove" end text end define end math ] "

\item " [ math define tex of tester1 as text "Tester1" end text end define end math ] "

\item " [ math define tex of tester2 as text "Tester2" end text end define end math ] "

\item " [ math define tex of tester3 as text "Tester3" end text end define end math ] "

\item " [ math define tex of tester4 as text "Tester4" end text end define end math ] "

\item " [ math define tex of tester5 as text "Tester5" end text end define end math ] "

\item " [ math define tex of tester6 as text "Tester6" end text end define end math ] "




\end{list}

\end{document}

End of file
latex page
latex page
dvipdfm page"