Logiweb expansion of kvanti 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}

" [ ragged right ] "

(*** MAKROER BEGYNDER ***)

" [ math define macro of ph1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define ph1 as placeholder-var var a end var end define end quote end define end define end math ] "

" [ math define macro of ph2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define ph2 as placeholder-var var b end var end define end quote end define end define end math ] "

" [ math define macro of ph3 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define ph3 as placeholder-var var c end var end define end quote end define end define end math ] "

" [ math define macro of ph4 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define ph4 as placeholder-var var d end var end define end quote end define end define end math ] "

" [ math define macro of ph5 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define ph5 as placeholder-var var e end var end define end quote end define end define end math ] "

" [ math define macro of ph6 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define ph6 as placeholder-var var f end var end define end quote end define end define end math ] "



" [ math define macro of var x and0 var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x and0 var y as not0 parenthesis var x imply not0 var y end parenthesis end define end quote end define end define end math ] "

" [ math define macro of var x or0 var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x or0 var y as not0 var x imply var y end define end quote end define end define end math ] "

" [ math define macro of var x iff var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x iff var y as parenthesis var x imply var y end parenthesis and0 parenthesis var y imply var x end parenthesis end define end quote end define end define end math ] "

" [ math define macro of var x zermelo ~is var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x zermelo ~is var y as not0 var x zermelo is var y end define end quote end define end define end math ] "

" [ math define macro of var x zermelo ~in var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x zermelo ~in var y as not0 var x in0 var y end define end quote end define end define end math ] "

" [ math define macro of var x is subset of var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x is subset of var y as for all object s1 indeed ( object s1 in0 var x imply object s1 in0 var y ) end define end quote end define end define end math ] "

" [ math define macro of zermelo singleton var x end singleton as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define zermelo singleton var x end singleton as zermelo pair var x comma var x end pair end define end quote end define end define end math ] "

" [ math define macro of binary-union var x comma var y end union as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define binary-union var x comma var y end union as union zermelo pair zermelo singleton var x end singleton comma zermelo singleton var y end singleton end pair end union end define end quote end define end define end math ] "

" [ math define macro of intersection var x comma var y end intersection as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define intersection var x comma var y end intersection as the set of ph in binary-union var x comma var y end union such that ph3 in0 var x and0 ph3 in0 var y end set end define end quote end define end define end math ] "

" [ math define macro of zermelo ordered pair var x comma var y end pair as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define zermelo ordered pair var x comma var y end pair as zermelo pair zermelo singleton var x end singleton comma zermelo pair var x comma var y end pair end pair end define end quote end define end define end math ] "


" [ math define macro of var x is related to var y under var r as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x is related to var y under var r as zermelo ordered pair var x comma var y end pair in0 var r end define end quote end define end define end math ] "


" [ math define macro of var r is reflexive relation in var x as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var r is reflexive relation in var x as for all object s indeed parenthesis object s in0 var x imply object s is related to object s under var r end parenthesis end define end quote end define end define end math ] "


" [ math define macro of var r is symmetric relation in var x as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var r is symmetric relation in var x as for all object s comma object t indeed parenthesis object s in0 var x imply object t in0 var x imply object s is related to object t under var r imply object t is related to object s under var r end parenthesis end define end quote end define end define end math ] "


" [ math define macro of var r is transitive relation in var x as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var r is transitive relation in var x as macro newline for all object s comma object t comma object u indeed parenthesis object s in0 var x imply object t in0 var x imply object u in0 var x imply object s is related to object t under var r imply object t is related to object u under var r imply object s is related to object u under var r end parenthesis end define end quote end define end define end math ] "


\display{" [ math define macro of var r is equivalence relation in var x as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var r is equivalence relation in var x as var r is reflexive relation in var x and0 var r is symmetric relation in var x and0 var r is transitive relation in var x end define end quote end define end define end math ] "}



" [ math define macro of meta big set as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta big set as metavar var big set end metavar end define end quote end define end define end math ] "

" [ math define macro of object big set as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define object big set as object var var big set end var end define end quote end define end define end math ] "


\display{
" [ math define macro of equivalence class of var x in var big set modulo var r as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define equivalence class of var x in var big set modulo var r as the set of ph in var big set such that ph1 is related to var x under var r end set end define end quote end define end define end math ] "
}

\display{
" [ math define macro of eq-system of var big set modulo var r as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define eq-system of var big set modulo var r as the set of ph in power var big set end power such that ex20 in0 var big set and0 equivalence class of ex20 in var big set modulo var r zermelo is ph2 end set end define end quote end define end define end math ] "
}

\display{
" [ math define macro of var p is partition of var big set as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var p is partition of var big set as parenthesis for all object s indeed parenthesis object s in0 var p imply object s zermelo ~is zermelo empty set end parenthesis end parenthesis and0 macro newline parenthesis for all object s comma object t indeed parenthesis object s in0 var p imply object t in0 var p imply object s zermelo ~is object t imply intersection object s comma object t end intersection zermelo is zermelo empty set end parenthesis end parenthesis and0 macro newline union var p end union zermelo is var big set end define end quote end define end define end math ] "
}

(*** EKSISTENS-VARIABLE ***)

\display{" [ math define value of var x is existential var as var x term root equal quote existential var var x end var end quote end define end math ] "
}

\display{
" [ math define macro of ex1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define ex1 as existential var var a end var end define end quote end define end define end math ] "
}

" [ math define macro of ex2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define ex2 as existential var var b end var end define end quote end define end define end math ] "

" [ math define macro of ex10 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define ex10 as existential var var j end var end define end quote end define end define end math ] "

" [ math define macro of ex20 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define ex20 as existential var var t end var end define end quote end define end define end math ] "

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

\item " [ math define macro of exist-sub var a is var b where var x is var t end sub as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define exist-sub var a is var b where var x is var t end sub as exist-sub0 quote var a end quote is quote var b end quote where quote var x end quote is quote var t end quote end sub end define end quote end define end define end math ] "

\item " [ math define value of exist-sub0 var a is var b where var x is var t end sub as lambda var c dot var x is existential var and exist-sub1 var a is var b where var x is var t end sub end define end math ] "

\item " [ math define value of exist-sub1 var a is var b where var x is var t end sub as var a tagged guard var x tagged guard var t tagged guard newline tagged if var b term root equal quote for all objects var u indeed var v end quote then false else newline tagged if var b is existential var and var b term equal var x then var a term equal var t else tagged if newline var a term root equal var b then exist-sub* var a tail is var b tail where var x is var t end sub else false end if end if end if end define end math ] "

\item " [ math define value of exist-sub* var a is var b where var x is var t end sub as var b tagged guard var x tagged guard var t tagged guard tagged if var a then true else tagged if exist-sub1 var a head is var b head where var x is var t end sub then exist-sub* var a tail is var b tail where var x is var t end sub else false end if end if end define end math ] "

\end{list}

(*** AKSIOMATISK SYSTEM ***)

" [ math define statement of system Q as all metavar var fx end metavar indeed all metavar var fy end metavar indeed R( metavar var fx end metavar ) ++ R( metavar var fy end metavar ) == R( metavar var fy end metavar ) ++ R( metavar var fx end metavar ) rule plus all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var fz end metavar indeed R( metavar var fx end metavar ) ** R( metavar var fy end metavar ) ** R( metavar var fz end metavar ) == R( metavar var fx end metavar ) ** R( metavar var fy end metavar ) ** R( metavar var fz end metavar ) rule plus all metavar var fx end metavar indeed all metavar var rx end metavar indeed all metavar var ry end metavar indeed metavar var rx end metavar == metavar var ry end metavar infer metavar var fx end metavar in0 metavar var rx end metavar infer metavar var fx end metavar in0 metavar var ry end metavar rule plus all metavar var m end metavar indeed upperBound( 01//02 ** [ xs ; metavar var m end metavar ] ++ [ us ; metavar var m end metavar ] , setOfReals ) infer [ xs ; metavar var m end metavar + 1 ] == [ xs ; metavar var m end metavar ] rule plus all metavar var x end metavar indeed all metavar var y end metavar indeed metavar var x end metavar <= metavar var y end metavar imply metavar var y end metavar <= metavar var x end metavar imply metavar var x end metavar = metavar var y end metavar rule plus all metavar var s end metavar indeed all metavar var x end metavar indeed all metavar var y end metavar indeed not0 metavar var s end metavar in0 zermelo pair metavar var x end metavar comma metavar var y end metavar end pair imply not0 metavar var s end metavar zermelo is metavar var x end metavar imply metavar var s end metavar zermelo is metavar var y end metavar imply not0 not0 metavar var s end metavar zermelo is metavar var x end metavar imply metavar var s end metavar zermelo is metavar var y end metavar imply metavar var s end metavar in0 zermelo pair metavar var x end metavar comma metavar var y end metavar end pair rule plus all metavar var m end metavar indeed all metavar var n end metavar indeed metavar var n end metavar = 0 infer base(1/2)Sum( metavar var m end metavar , metavar var n end metavar ) = 1/ 1 + 1 ^ metavar var m end metavar rule plus all metavar var x end metavar indeed metavar var x end metavar + 0 = metavar var x end metavar rule plus all metavar var fx end metavar indeed all metavar var fy end metavar indeed R( metavar var fx end metavar ) == R( metavar var fy end metavar ) infer metavar var fx end metavar sameF metavar var fy end metavar rule plus all metavar var x end metavar indeed all metavar var y end metavar indeed metavar var x end metavar = metavar var y end metavar imply metavar var x end metavar <= metavar var y end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar infer metavar var a end metavar infer metavar var b end metavar rule plus all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var fz end metavar indeed R( metavar var fx end metavar ) = R( metavar var fy end metavar ) infer R( metavar var fx end metavar ) ++ R( metavar var fz end metavar ) = R( metavar var fy end metavar ) ++ R( metavar var fz end metavar ) rule plus all metavar var fx end metavar indeed R( metavar var fx end metavar ) ++ R( 0f ) == R( metavar var fx end metavar ) rule plus all metavar var x end metavar indeed metavar var x end metavar * 1 = metavar var x end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer metavar var b end metavar rule plus all metavar var rx end metavar indeed all metavar var ry end metavar indeed metavar var rx end metavar == metavar var ry end metavar infer metavar var ry end metavar == metavar var rx end metavar rule plus all metavar var m end metavar indeed all metavar var x end metavar indeed metavar var m end metavar = 0 infer metavar var x end metavar ^ metavar var m end metavar = 1 rule plus all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed 0 <= metavar var z end metavar imply metavar var x end metavar <= metavar var y end metavar imply metavar var x end metavar * metavar var z end metavar <= metavar var y end metavar * metavar var z end metavar rule plus all metavar var fx end metavar indeed R( metavar var fx end metavar ) ** R( 1f ) == R( metavar var fx end metavar ) rule plus not0 0 = 1 rule plus all metavar var m end metavar indeed Nat( metavar var m end metavar ) endorse 0 <= metavar var m end metavar rule plus all metavar var x end metavar indeed all metavar var y end metavar indeed not0 metavar var x end metavar zermelo is metavar var y end metavar imply for all objects object var var s end var indeed not0 object var var s end var in0 metavar var x end metavar imply object var var s end var in0 metavar var y end metavar imply not0 object var var s end var in0 metavar var y end metavar imply object var var s end var in0 metavar var x end metavar imply not0 for all objects object var var s end var indeed not0 object var var s end var in0 metavar var x end metavar imply object var var s end var in0 metavar var y end metavar imply not0 object var var s end var in0 metavar var y end metavar imply object var var s end var in0 metavar var x end metavar imply metavar var x end metavar zermelo is metavar var y end metavar rule plus all metavar var rx end metavar indeed all metavar var ry end metavar indeed all metavar var rz end metavar indeed metavar var rx end metavar == metavar var ry end metavar infer metavar var ry end metavar == metavar var rz end metavar infer metavar var rx end metavar == metavar var rz end metavar rule plus all metavar var x end metavar indeed all metavar var y end metavar indeed metavar var x end metavar + metavar var y end metavar = metavar var y end metavar + metavar var x end metavar rule plus all metavar var m end metavar indeed all metavar var fx end metavar indeed all metavar var fy end metavar indeed [ metavar var fx end metavar +f metavar var fy end metavar ; metavar var m end metavar ] = [ metavar var fx end metavar ; metavar var m end metavar ] + [ metavar var fy end metavar ; metavar var m end metavar ] rule plus all metavar var v1 end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed meta-sub metavar var b end metavar is metavar var a end metavar where metavar var v1 end metavar is 0 end sub endorse meta-sub metavar var c end metavar is metavar var a end metavar where metavar var v1 end metavar is metavar var v1 end metavar + 1 end sub endorse metavar var b end metavar imply for all objects metavar var v1 end metavar indeed metavar var a end metavar imply metavar var c end metavar imply for all objects metavar var v1 end metavar indeed metavar var a end metavar rule plus all metavar var m end metavar indeed all metavar var n end metavar indeed metavar var n end metavar = 0 infer UStelescope( metavar var m end metavar , metavar var n end metavar ) = | [ us ; metavar var m end metavar ] + - [ us ; metavar var m end metavar + 1 ] | rule plus all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var fz end metavar indeed R( metavar var fx end metavar ) ++ R( metavar var fy end metavar ) ++ R( metavar var fz end metavar ) = R( metavar var fx end metavar ) ++ R( metavar var fy end metavar ) ++ R( metavar var fz end metavar ) rule plus all metavar var x end metavar indeed all metavar var y end metavar indeed metavar var x end metavar * metavar var y end metavar = metavar var y end metavar * metavar var x end metavar rule plus all metavar var fx end metavar indeed all metavar var fy end metavar indeed metavar var fx end metavar in0 R( metavar var fy end metavar ) infer metavar var fx end metavar sameF metavar var fy end metavar rule plus all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar = metavar var y end metavar imply metavar var x end metavar * metavar var z end metavar = metavar var y end metavar * metavar var z end metavar rule plus all metavar var a end metavar indeed metavar var a end metavar infer metavar var a end metavar rule plus all metavar var m end metavar indeed upperBound( 01//02 ** [ xs ; metavar var m end metavar ] ++ [ us ; metavar var m end metavar ] , setOfReals ) infer [ us ; metavar var m end metavar + 1 ] == 01//02 ** [ xs ; metavar var m end metavar ] ++ [ us ; metavar var m end metavar ] rule plus all metavar var x end metavar indeed all metavar var y end metavar indeed not0 metavar var x end metavar <= metavar var y end metavar imply metavar var y end metavar <= metavar var x end metavar rule plus all metavar var s end metavar indeed all metavar var x end metavar indeed not0 metavar var s end metavar in0 power metavar var x end metavar end power imply for all objects object var var s end var indeed object var var s end var in0 metavar var s end metavar imply object var var s end var in0 metavar var x end metavar imply not0 for all objects object var var s end var indeed object var var s end var in0 metavar var s end metavar imply object var var s end var in0 metavar var x end metavar imply metavar var s end metavar in0 power metavar var x end metavar end power rule plus [ us ; 0 ] == [ xs ; 0 ] ++ R( 1f ) rule plus all metavar var x end metavar indeed metavar var x end metavar <= metavar var x end metavar rule plus all metavar var s end metavar indeed not0 metavar var s end metavar in0 zermelo empty set rule plus all metavar var x end metavar indeed metavar var x end metavar + - metavar var x end metavar = 0 rule plus all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar = metavar var y end metavar imply metavar var x end metavar = metavar var z end metavar imply metavar var y end metavar = metavar var z end metavar rule plus all metavar var m end metavar indeed all metavar var n end metavar indeed not0 0 <= metavar var n end metavar imply not0 not0 0 = metavar var n end metavar infer UStelescope( metavar var m end metavar , metavar var n end metavar ) = | [ us ; metavar var m end metavar + metavar var n end metavar ] + - [ us ; metavar var m end metavar + metavar var n end metavar + 1 ] | + UStelescope( metavar var m end metavar , metavar var n end metavar + - 1 ) rule plus all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var fz end metavar indeed R( metavar var fx end metavar +f metavar var fy end metavar +f metavar var fz end metavar ) == R( metavar var fx end metavar +f metavar var fy end metavar +f metavar var fz end metavar ) rule plus all metavar var x end metavar indeed not0 metavar var x end metavar = 0 imply metavar var x end metavar * 1/ metavar var x end metavar = 1 rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed not0 metavar var b end metavar imply metavar var a end metavar infer not0 metavar var b end metavar imply not0 metavar var a end metavar infer metavar var b end metavar rule plus all metavar var rx end metavar indeed metavar var rx end metavar == metavar var rx end metavar rule plus all metavar var m end metavar indeed not0 upperBound( 01//02 ** [ xs ; metavar var m end metavar ] ++ [ us ; metavar var m end metavar ] , setOfReals ) infer [ us ; metavar var m end metavar + 1 ] == [ us ; metavar var m end metavar ] rule plus all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar <= metavar var y end metavar imply metavar var x end metavar + metavar var z end metavar <= metavar var y end metavar + metavar var z end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var p end metavar indeed all metavar var x end metavar indeed all metavar var z end metavar indeed metavar var p end metavar is placeholder-var and ph-sub metavar var b end metavar is metavar var a end metavar where metavar var p end metavar is metavar var z end metavar end sub endorse not0 metavar var z end metavar in0 the set of ph in metavar var x end metavar such that metavar var a end metavar end set imply not0 metavar var z end metavar in0 metavar var x end metavar imply not0 metavar var b end metavar imply not0 not0 metavar var z end metavar in0 metavar var x end metavar imply not0 metavar var b end metavar imply metavar var z end metavar in0 the set of ph in metavar var x end metavar such that metavar var a end metavar end set rule plus all metavar var m end metavar indeed all metavar var fx end metavar indeed R( metavar var fx end metavar ) ++ -- R( metavar var fx end metavar ) == R( 0f ) rule plus all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar * metavar var y end metavar + metavar var z end metavar = metavar var x end metavar * metavar var y end metavar + metavar var x end metavar * metavar var z end metavar rule plus all metavar var m end metavar indeed all metavar var n end metavar indeed Nat( metavar var m end metavar ) endorse Nat( metavar var n end metavar ) endorse not0 metavar var m end metavar <= metavar var n end metavar + 1 imply not0 not0 metavar var m end metavar = metavar var n end metavar + 1 infer metavar var m end metavar <= metavar var n end metavar rule plus all metavar var x end metavar indeed all metavar var t end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed exist-sub0 quote metavar var a end metavar end quote is quote metavar var b end metavar end quote where quote metavar var x end metavar end quote is quote metavar var t end metavar end quote end sub endorse metavar var a end metavar infer metavar var b end metavar rule plus all metavar var m end metavar indeed all metavar var x end metavar indeed not0 0 <= metavar var m end metavar imply not0 not0 0 = metavar var m end metavar infer metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar + - 1 rule plus all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar + metavar var y end metavar + metavar var z end metavar = metavar var x end metavar + metavar var y end metavar + metavar var z end metavar rule plus all metavar var v1 end metavar indeed all metavar var v2 end metavar indeed all metavar var n end metavar indeed all metavar var ep end metavar indeed all metavar var fx end metavar indeed for all objects metavar var ep end metavar indeed not0 for all objects metavar var n end metavar indeed not0 for all objects metavar var v1 end metavar indeed for all objects metavar var v2 end metavar indeed not0 0 <= metavar var ep end metavar imply not0 not0 0 = metavar var ep end metavar imply metavar var n end metavar <= metavar var v1 end metavar imply metavar var n end metavar <= metavar var v2 end metavar imply not0 | [ metavar var fx end metavar ; metavar var v1 end metavar ] + - [ metavar var fx end metavar ; metavar var v2 end metavar ] | <= metavar var ep end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var v1 end metavar ] + - [ metavar var fx end metavar ; metavar var v2 end metavar ] | = metavar var ep end metavar rule plus all metavar var x end metavar indeed all metavar var v1 end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed meta-sub metavar var a end metavar is metavar var b end metavar where metavar var v1 end metavar is metavar var x end metavar end sub endorse for all objects metavar var v1 end metavar indeed metavar var b end metavar imply metavar var a end metavar rule plus all metavar var m end metavar indeed all metavar var n end metavar indeed not0 0 <= metavar var n end metavar imply not0 not0 0 = metavar var n end metavar infer base(1/2)Sum( metavar var m end metavar , metavar var n end metavar ) = 1/ 1 + 1 ^ metavar var m end metavar + metavar var n end metavar + base(1/2)Sum( metavar var m end metavar , metavar var n end metavar + - 1 ) rule plus all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar * metavar var y end metavar * metavar var z end metavar = metavar var x end metavar * metavar var y end metavar * metavar var z end metavar rule plus all metavar var fx end metavar indeed all metavar var fy end metavar indeed metavar var fx end metavar sameF metavar var fy end metavar infer R( metavar var fx end metavar ) == R( metavar var fy end metavar ) rule plus all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar = metavar var y end metavar imply metavar var x end metavar + metavar var z end metavar = metavar var y end metavar + metavar var z end metavar rule plus all metavar var x end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer for all objects metavar var x end metavar indeed metavar var a end metavar rule plus all metavar var m end metavar indeed not0 upperBound( 01//02 ** [ xs ; metavar var m end metavar ] ++ [ us ; metavar var m end metavar ] , setOfReals ) infer [ xs ; metavar var m end metavar + 1 ] == 01//02 ** [ xs ; metavar var m end metavar ] ++ [ us ; metavar var m end metavar ] rule plus all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar <= metavar var y end metavar imply metavar var y end metavar <= metavar var z end metavar imply metavar var x end metavar <= metavar var z end metavar rule plus all metavar var s end metavar indeed all metavar var x end metavar indeed not0 metavar var s end metavar in0 union metavar var x end metavar end union imply not0 metavar var s end metavar in0 existential var var j end var imply not0 existential var var j end var in0 metavar var x end metavar imply not0 not0 metavar var s end metavar in0 existential var var j end var imply not0 existential var var j end var in0 metavar var x end metavar imply metavar var s end metavar in0 union metavar var x end metavar end union rule plus all metavar var fx end metavar indeed all metavar var fy end metavar indeed R( metavar var fx end metavar ) ** R( metavar var fy end metavar ) == R( metavar var fy end metavar ) ** R( metavar var fx end metavar ) rule plus all metavar var fx end metavar indeed all metavar var rx end metavar indeed all metavar var ry end metavar indeed metavar var rx end metavar == metavar var ry end metavar infer metavar var fx end metavar in0 metavar var ry end metavar infer metavar var fx end metavar in0 metavar var rx end metavar end define end math ] "

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

\item " [ math define statement of 1rule mp as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar infer metavar var a end metavar infer metavar var b end metavar end define , define proof of 1rule mp as rule tactic end define end math ] "

\item " [ math define statement of 1rule gen as system Q infer all metavar var x end metavar indeed all metavar var a end metavar indeed metavar var a end metavar infer for all objects metavar var x end metavar indeed metavar var a end metavar end define , define proof of 1rule gen as rule tactic end define end math ] "

\item " [ math define statement of 1rule repetition as system Q infer all metavar var a end metavar indeed metavar var a end metavar infer metavar var a end metavar end define , define proof of 1rule repetition as rule tactic end define end math ] "

\item " [ math define statement of 1rule ad absurdum as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed not0 metavar var b end metavar imply metavar var a end metavar infer not0 metavar var b end metavar imply not0 metavar var a end metavar infer metavar var b end metavar end define , define proof of 1rule ad absurdum as rule tactic end define end math ] "

\item " [ math define statement of 1rule deduction as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer metavar var b end metavar end define , define proof of 1rule deduction as rule tactic end define end math ] "

\item " [ math define statement of 1rule exist intro as system Q infer all metavar var x end metavar indeed all metavar var t end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed exist-sub0 quote metavar var a end metavar end quote is quote metavar var b end metavar end quote where quote metavar var x end metavar end quote is quote metavar var t end metavar end quote end sub endorse metavar var a end metavar infer metavar var b end metavar end define , define proof of 1rule exist intro as rule tactic end define end math ] "

\item " [ math define statement of axiom extensionality as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed not0 metavar var x end metavar zermelo is metavar var y end metavar imply for all objects object var var s end var indeed not0 object var var s end var in0 metavar var x end metavar imply object var var s end var in0 metavar var y end metavar imply not0 object var var s end var in0 metavar var y end metavar imply object var var s end var in0 metavar var x end metavar imply not0 for all objects object var var s end var indeed not0 object var var s end var in0 metavar var x end metavar imply object var var s end var in0 metavar var y end metavar imply not0 object var var s end var in0 metavar var y end metavar imply object var var s end var in0 metavar var x end metavar imply metavar var x end metavar zermelo is metavar var y end metavar end define , define proof of axiom extensionality as rule tactic end define end math ] "

\item " [ math define statement of axiom empty set as system Q infer all metavar var s end metavar indeed not0 metavar var s end metavar in0 zermelo empty set end define , define proof of axiom empty set as rule tactic end define end math ] "

\item " [ math define statement of axiom pair definition as system Q infer all metavar var s end metavar indeed all metavar var x end metavar indeed all metavar var y end metavar indeed not0 metavar var s end metavar in0 zermelo pair metavar var x end metavar comma metavar var y end metavar end pair imply not0 metavar var s end metavar zermelo is metavar var x end metavar imply metavar var s end metavar zermelo is metavar var y end metavar imply not0 not0 metavar var s end metavar zermelo is metavar var x end metavar imply metavar var s end metavar zermelo is metavar var y end metavar imply metavar var s end metavar in0 zermelo pair metavar var x end metavar comma metavar var y end metavar end pair end define , define proof of axiom pair definition as rule tactic end define end math ] "

\item " [ math define statement of axiom union definition as system Q infer all metavar var s end metavar indeed all metavar var x end metavar indeed not0 metavar var s end metavar in0 union metavar var x end metavar end union imply not0 metavar var s end metavar in0 existential var var j end var imply not0 existential var var j end var in0 metavar var x end metavar imply not0 not0 metavar var s end metavar in0 existential var var j end var imply not0 existential var var j end var in0 metavar var x end metavar imply metavar var s end metavar in0 union metavar var x end metavar end union end define , define proof of axiom union definition as rule tactic end define end math ] "

\item " [ math define statement of axiom power definition as system Q infer all metavar var s end metavar indeed all metavar var x end metavar indeed not0 metavar var s end metavar in0 power metavar var x end metavar end power imply for all objects object var var s end var indeed object var var s end var in0 metavar var s end metavar imply object var var s end var in0 metavar var x end metavar imply not0 for all objects object var var s end var indeed object var var s end var in0 metavar var s end metavar imply object var var s end var in0 metavar var x end metavar imply metavar var s end metavar in0 power metavar var x end metavar end power end define , define proof of axiom power definition as rule tactic end define end math ] "

\item " [ math define statement of axiom separation definition as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var p end metavar indeed all metavar var x end metavar indeed all metavar var z end metavar indeed metavar var p end metavar is placeholder-var and ph-sub metavar var b end metavar is metavar var a end metavar where metavar var p end metavar is metavar var z end metavar end sub endorse not0 metavar var z end metavar in0 the set of ph in metavar var x end metavar such that metavar var a end metavar end set imply not0 metavar var z end metavar in0 metavar var x end metavar imply not0 metavar var b end metavar imply not0 not0 metavar var z end metavar in0 metavar var x end metavar imply not0 metavar var b end metavar imply metavar var z end metavar in0 the set of ph in metavar var x end metavar such that metavar var a end metavar end set end define , define proof of axiom separation definition as rule tactic end define end math ] "

\end{list}

\appendix



------------- RRRRRRRRRRRRRRR -------------

(*** import fra A.M. ***)



" [ math define statement of lemma timesCommutativity(R) as system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed R( metavar var fx end metavar ) ** R( metavar var fy end metavar ) == R( metavar var fy end metavar ) ** R( metavar var fx end metavar ) end define , define proof of lemma timesCommutativity(R) as rule tactic end define end math ] "


(*** aksiomer ***)

" [ math define statement of axiom leqReflexivity as system Q infer all metavar var x end metavar indeed metavar var x end metavar <= metavar var x end metavar end define , define proof of axiom leqReflexivity as rule tactic end define end math ] "

" [ math define statement of axiom leqAntisymmetry as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed metavar var x end metavar <= metavar var y end metavar imply metavar var y end metavar <= metavar var x end metavar imply metavar var x end metavar = metavar var y end metavar end define , define proof of axiom leqAntisymmetry as rule tactic end define end math ] "

" [ math define statement of axiom leqTransitivity as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar <= metavar var y end metavar imply metavar var y end metavar <= metavar var z end metavar imply metavar var x end metavar <= metavar var z end metavar end define , define proof of axiom leqTransitivity as rule tactic end define end math ] "

" [ math define statement of axiom leqTotality as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed not0 metavar var x end metavar <= metavar var y end metavar imply metavar var y end metavar <= metavar var x end metavar end define , define proof of axiom leqTotality as rule tactic end define end math ] "

" [ math define statement of axiom leqAddition as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar <= metavar var y end metavar imply metavar var x end metavar + metavar var z end metavar <= metavar var y end metavar + metavar var z end metavar end define , define proof of axiom leqAddition as rule tactic end define end math ] "

" [ math define statement of axiom leqMultiplication as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed 0 <= metavar var z end metavar imply metavar var x end metavar <= metavar var y end metavar imply metavar var x end metavar * metavar var z end metavar <= metavar var y end metavar * metavar var z end metavar end define , define proof of axiom leqMultiplication as rule tactic end define end math ] "

" [ math define statement of axiom plusAssociativity as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar + metavar var y end metavar + metavar var z end metavar = metavar var x end metavar + metavar var y end metavar + metavar var z end metavar end define , define proof of axiom plusAssociativity as rule tactic end define end math ] "

" [ math define statement of axiom plusCommutativity as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed metavar var x end metavar + metavar var y end metavar = metavar var y end metavar + metavar var x end metavar end define , define proof of axiom plusCommutativity as rule tactic end define end math ] "

" [ math define statement of axiom negative as system Q infer all metavar var x end metavar indeed metavar var x end metavar + - metavar var x end metavar = 0 end define , define proof of axiom negative as rule tactic end define end math ] "

" [ math define statement of axiom plus0 as system Q infer all metavar var x end metavar indeed metavar var x end metavar + 0 = metavar var x end metavar end define , define proof of axiom plus0 as rule tactic end define end math ] "

" [ math define statement of axiom timesAssociativity as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar * metavar var y end metavar * metavar var z end metavar = metavar var x end metavar * metavar var y end metavar * metavar var z end metavar end define , define proof of axiom timesAssociativity as rule tactic end define end math ] "

" [ math define statement of axiom timesCommutativity as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed metavar var x end metavar * metavar var y end metavar = metavar var y end metavar * metavar var x end metavar end define , define proof of axiom timesCommutativity as rule tactic end define end math ] "

" [ math define statement of axiom reciprocal as system Q infer all metavar var x end metavar indeed not0 metavar var x end metavar = 0 imply metavar var x end metavar * 1/ metavar var x end metavar = 1 end define , define proof of axiom reciprocal as rule tactic end define end math ] "

" [ math define statement of axiom times1 as system Q infer all metavar var x end metavar indeed metavar var x end metavar * 1 = metavar var x end metavar end define , define proof of axiom times1 as rule tactic end define end math ] "

" [ math define statement of axiom distribution as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar * metavar var y end metavar + metavar var z end metavar = metavar var x end metavar * metavar var y end metavar + metavar var x end metavar * metavar var z end metavar end define , define proof of axiom distribution as rule tactic end define end math ] "

" [ math define statement of axiom 0not1 as system Q infer not0 0 = 1 end define , define proof of axiom 0not1 as rule tactic end define end math ] "

" [ math define statement of axiom equality as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar = metavar var y end metavar imply metavar var x end metavar = metavar var z end metavar imply metavar var y end metavar = metavar var z end metavar end define , define proof of axiom equality as rule tactic end define end math ] "

" [ math define statement of axiom eqLeq as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed metavar var x end metavar = metavar var y end metavar imply metavar var x end metavar <= metavar var y end metavar end define , define proof of axiom eqLeq as rule tactic end define end math ] "

" [ math define statement of axiom eqAddition as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar = metavar var y end metavar imply metavar var x end metavar + metavar var z end metavar = metavar var y end metavar + metavar var z end metavar end define , define proof of axiom eqAddition as rule tactic end define end math ] "

" [ math define statement of axiom eqMultiplication as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed metavar var x end metavar = metavar var y end metavar imply metavar var x end metavar * metavar var z end metavar = metavar var y end metavar * metavar var z end metavar end define , define proof of axiom eqMultiplication as rule tactic end define end math ] "

" [ math define statement of axiom a4 as system Q infer all metavar var x end metavar indeed all metavar var v1 end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed meta-sub metavar var a end metavar is metavar var b end metavar where metavar var v1 end metavar is metavar var x end metavar end sub endorse for all objects metavar var v1 end metavar indeed metavar var b end metavar imply metavar var a end metavar end define , define proof of axiom a4 as rule tactic end define end math ] "


(*** XX snydeaksiomer ***)

" [ math define statement of lemma ==Reflexivity as system Q infer all metavar var rx end metavar indeed metavar var rx end metavar == metavar var rx end metavar end define , define proof of lemma ==Reflexivity as rule tactic end define end math ] "

" [ math define statement of lemma ==Symmetry as system Q infer all metavar var rx end metavar indeed all metavar var ry end metavar indeed metavar var rx end metavar == metavar var ry end metavar infer metavar var ry end metavar == metavar var rx end metavar end define , define proof of lemma ==Symmetry as rule tactic end define end math ] "

" [ math define statement of lemma ==Transitivity as system Q infer all metavar var rx end metavar indeed all metavar var ry end metavar indeed all metavar var rz end metavar indeed metavar var rx end metavar == metavar var ry end metavar infer metavar var ry end metavar == metavar var rz end metavar infer metavar var rx end metavar == metavar var rz end metavar end define , define proof of lemma ==Transitivity as rule tactic end define end math ] "


XX ikke 100procent identisk med originalen fra equivalence-relations
" [ math define statement of lemma set equality nec condition(1) as system Q infer all metavar var fx end metavar indeed all metavar var rx end metavar indeed all metavar var ry end metavar indeed metavar var rx end metavar == metavar var ry end metavar infer metavar var fx end metavar in0 metavar var rx end metavar infer metavar var fx end metavar in0 metavar var ry end metavar end define , define proof of lemma set equality nec condition(1) as rule tactic end define end math ] "


XX boer bevises ud fra nummer 1
" [ math define statement of lemma set equality nec condition(2) as system Q infer all metavar var fx end metavar indeed all metavar var rx end metavar indeed all metavar var ry end metavar indeed metavar var rx end metavar == metavar var ry end metavar infer metavar var fx end metavar in0 metavar var ry end metavar infer metavar var fx end metavar in0 metavar var rx end metavar end define , define proof of lemma set equality nec condition(2) as rule tactic end define end math ] "

" [ math define statement of axiom plusF as system Q infer all metavar var m end metavar indeed all metavar var fx end metavar indeed all metavar var fy end metavar indeed [ metavar var fx end metavar +f metavar var fy end metavar ; metavar var m end metavar ] = [ metavar var fx end metavar ; metavar var m end metavar ] + [ metavar var fy end metavar ; metavar var m end metavar ] end define , define proof of axiom plusF as rule tactic end define end math ] "

" [ math define statement of 1rule from== as system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed R( metavar var fx end metavar ) == R( metavar var fy end metavar ) infer metavar var fx end metavar sameF metavar var fy end metavar end define , define proof of 1rule from== as rule tactic end define end math ] "

" [ math define statement of 1rule to== as system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed metavar var fx end metavar sameF metavar var fy end metavar infer R( metavar var fx end metavar ) == R( metavar var fy end metavar ) end define , define proof of 1rule to== as rule tactic end define end math ] "


" [ math define statement of 1rule fromInR as system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed metavar var fx end metavar in0 R( metavar var fy end metavar ) infer metavar var fx end metavar sameF metavar var fy end metavar end define , define proof of 1rule fromInR as rule tactic end define end math ] "



(*** makroer ***)

KVANTI

" [ math define macro of meta m1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta m1 as metavar var m1 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta m2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta m2 as metavar var m2 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta n1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta n1 as metavar var n1 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta n2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta n2 as metavar var n2 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta n3 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta n3 as metavar var n3 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta ep as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta ep as metavar var ep end metavar end define end quote end define end define end math ] "
" [ math define macro of meta ep1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta ep1 as metavar var ep1 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta ep2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta ep2 as metavar var ep2 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta x1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta x1 as metavar var x1 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta x2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta x2 as metavar var x2 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta y1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta y1 as metavar var y1 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta y2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta y2 as metavar var y2 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta v1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta v1 as metavar var v1 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta v2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta v2 as metavar var v2 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta v3 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta v3 as metavar var v3 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta v4 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta v4 as metavar var v4 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta v2n as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta v2n as metavar var v2n end metavar end define end quote end define end define end math ] "
" [ math define macro of meta fx as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta fx as metavar var fx end metavar end define end quote end define end define end math ] "
" [ math define macro of meta fy as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta fy as metavar var fy end metavar end define end quote end define end define end math ] "
" [ math define macro of meta fz as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta fz as metavar var fz end metavar end define end quote end define end define end math ] "
" [ math define macro of meta fu as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta fu as metavar var fu end metavar end define end quote end define end define end math ] "
" [ math define macro of meta fv as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta fv as metavar var fv end metavar end define end quote end define end define end math ] "
" [ math define macro of meta fw as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta fw as metavar var fw end metavar end define end quote end define end define end math ] "
" [ math define macro of meta fep as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta fep as metavar var fep end metavar end define end quote end define end define end math ] "
" [ math define macro of meta rx as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta rx as metavar var rx end metavar end define end quote end define end define end math ] "
" [ math define macro of meta ry as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta ry as metavar var ry end metavar end define end quote end define end define end math ] "
" [ math define macro of meta rz as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta rz as metavar var rz end metavar end define end quote end define end define end math ] "
" [ math define macro of meta ru as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta ru as metavar var ru end metavar end define end quote end define end define end math ] "
" [ math define macro of meta sx as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta sx as metavar var sx end metavar end define end quote end define end define end math ] "
" [ math define macro of meta sx1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta sx1 as metavar var sx1 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta sy as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta sy as metavar var sy end metavar end define end quote end define end define end math ] "
" [ math define macro of meta sy1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta sy1 as metavar var sy1 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta sz as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta sz as metavar var sz end metavar end define end quote end define end define end math ] "
" [ math define macro of meta sz1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta sz1 as metavar var sz1 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta su as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta su as metavar var su end metavar end define end quote end define end define end math ] "
" [ math define macro of meta su1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta su1 as metavar var su1 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta fxs as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta fxs as metavar var fxs end metavar end define end quote end define end define end math ] "
" [ math define macro of meta fys as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta fys as metavar var fys end metavar end define end quote end define end define end math ] "
" [ math define macro of meta f1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta f1 as metavar var f1 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta f2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta f2 as metavar var f2 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta f3 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta f3 as metavar var f3 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta f4 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta f4 as metavar var f4 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta op1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta op1 as metavar var op1 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta op2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta op2 as metavar var op2 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta r1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta r1 as metavar var r1 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta s1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta s1 as metavar var s1 end metavar end define end quote end define end define end math ] "
" [ math define macro of meta s2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define meta s2 as metavar var s2 end metavar end define end quote end define end define end math ] "

" [ math define macro of object ep as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define object ep as object var var ep end var end define end quote end define end define end math ] "
" [ math define macro of object crs1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define object crs1 as object var var crs1 end var end define end quote end define end define end math ] "
" [ math define macro of object f1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define object f1 as object var var f1 end var end define end quote end define end define end math ] "
" [ math define macro of object f2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define object f2 as object var var f2 end var end define end quote end define end define end math ] "
" [ math define macro of object f3 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define object f3 as object var var f3 end var end define end quote end define end define end math ] "
" [ math define macro of object f4 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define object f4 as object var var f4 end var end define end quote end define end define end math ] "
" [ math define macro of object n1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define object n1 as object var var n1 end var end define end quote end define end define end math ] "
" [ math define macro of object n2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define object n2 as object var var n2 end var end define end quote end define end define end math ] "
" [ math define macro of object op1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define object op1 as object var var op1 end var end define end quote end define end define end math ] "
" [ math define macro of object op2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define object op2 as object var var op2 end var end define end quote end define end define end math ] "
" [ math define macro of object r1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define object r1 as object var var r1 end var end define end quote end define end define end math ] "
" [ math define macro of object s1 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define object s1 as object var var s1 end var end define end quote end define end define end math ] "
" [ math define macro of object s2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define object s2 as object var var s2 end var end define end quote end define end define end math ] "





" [ math define macro of var fx <=f var fy as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var fx <=f var fy as var fx


" [ math define macro of ex3 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define ex3 as existential var var c end var end define end quote end define end define end math ] "

" [ math define macro of exist0 var v1 indeed var a as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define exist0 var v1 indeed var a as not0 for all var v1 indeed not0 var a end define end quote end define end define end math ] "

" [ math define macro of var x <<== var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x <<== var y as var x << var y or0 var x == var y end define end quote end define end define end math ] "

" [ math define macro of (-1) as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define (-1) as - 1 end define end quote end define end define end math ] "

" [ math define macro of 2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define 2 as 1 + 1 end define end quote end define end define end math ] "

" [ math define macro of 3 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define 3 as 2 + 1 end define end quote end define end define end math ] "

" [ math define macro of 1/2 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define 1/2 as 1/ 2 end define end quote end define end define end math ] "

" [ math define macro of 1/3 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define 1/3 as 1/ 3 end define end quote end define end define end math ] "

" [ math define macro of 2/3 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define 2/3 as 2 * 1/3 end define end quote end define end define end math ] "

" [ math define macro of var x < var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x < var y as var x <= var y and0 var x != var y end define end quote end define end define end math ] "

" [ math define macro of var x != var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x != var y as not0 var x = var y end define end quote end define end define end math ] "


" [ math define macro of var x - var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x - var y as var x + - var y end define end quote end define end define end math ] "

" [ math define macro of 00 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define 00 as R( 0f ) end define end quote end define end define end math ] "

" [ math define macro of 01 as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define 01 as R( 1f ) end define end quote end define end define end math ] "

" [ math define macro of var x !!== var y as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define var x !!== var y as not0 var x == var y end define end quote end define end define end math ] "




(*** REGELLEMMAER ***)




(*** UDSAGNSLOGIK ***)


" [ math define statement of prop lemma to negated imply as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer not0 metavar var b end metavar infer not0 metavar var a end metavar imply metavar var b end metavar end define end math ] "

" [ math define proof of prop lemma to negated imply as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer not0 metavar var b end metavar infer not0 not0 metavar var a end metavar imply metavar var b end metavar infer prop lemma remove double neg modus ponens not0 not0 metavar var a end metavar imply metavar var b end metavar conclude metavar var a end metavar imply metavar var b end metavar cut 1rule mp modus ponens metavar var a end metavar imply metavar var b end metavar modus ponens metavar var a end metavar conclude metavar var b end metavar cut prop lemma from contradiction modus ponens metavar var b end metavar modus ponens not0 metavar var b end metavar conclude not0 metavar var a end metavar imply metavar var b end metavar cut all metavar var a end metavar indeed all metavar var b end metavar indeed 1rule deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar infer not0 metavar var b end metavar infer not0 not0 metavar var a end metavar imply metavar var b end metavar infer not0 metavar var a end metavar imply metavar var b end metavar conclude metavar var a end metavar imply not0 metavar var b end metavar imply not0 not0 metavar var a end metavar imply metavar var b end metavar imply not0 metavar var a end metavar imply metavar var b end metavar cut metavar var a end metavar infer not0 metavar var b end metavar infer prop lemma mp2 modus ponens metavar var a end metavar imply not0 metavar var b end metavar imply not0 not0 metavar var a end metavar imply metavar var b end metavar imply not0 metavar var a end metavar imply metavar var b end metavar modus ponens metavar var a end metavar modus ponens not0 metavar var b end metavar conclude not0 not0 metavar var a end metavar imply metavar var b end metavar imply not0 metavar var a end metavar imply metavar var b end metavar cut prop lemma auto imply conclude not0 not0 metavar var a end metavar imply metavar var b end metavar imply not0 not0 metavar var a end metavar imply metavar var b end metavar cut 1rule ad absurdum modus ponens not0 not0 metavar var a end metavar imply metavar var b end metavar imply not0 metavar var a end metavar imply metavar var b end metavar modus ponens not0 not0 metavar var a end metavar imply metavar var b end metavar imply not0 not0 metavar var a end metavar imply metavar var b end metavar conclude not0 metavar var a end metavar imply metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "


" [ math define statement of prop lemma tertium non datur as system Q infer all metavar var a end metavar indeed not0 metavar var a end metavar imply not0 metavar var a end metavar end define end math ] "

" [ math define proof of prop lemma tertium non datur as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var a end metavar indeed prop lemma auto imply conclude not0 metavar var a end metavar imply not0 metavar var a end metavar cut 1rule repetition modus ponens not0 metavar var a end metavar imply not0 metavar var a end metavar conclude not0 metavar var a end metavar imply not0 metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "

" [ math define statement of prop lemma from negations as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar infer not0 metavar var a end metavar imply metavar var b end metavar infer metavar var b end metavar end define end math ] "

" [ math define proof of prop lemma from negations as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply metavar var b end metavar infer not0 metavar var a end metavar imply metavar var b end metavar infer prop lemma tertium non datur conclude not0 metavar var a end metavar imply not0 metavar var a end metavar cut prop lemma from disjuncts modus ponens not0 metavar var a end metavar imply not0 metavar var a end metavar modus ponens metavar var a end metavar imply metavar var b end metavar modus ponens not0 metavar var a end metavar imply metavar var b end metavar conclude metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "

" [ math define statement of prop lemma imply negation as system Q infer all metavar var a end metavar indeed metavar var a end metavar imply not0 metavar var a end metavar infer not0 metavar var a end metavar end define end math ] "

" [ math define proof of prop lemma imply negation as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var a end metavar indeed metavar var a end metavar imply not0 metavar var a end metavar infer prop lemma auto imply conclude not0 metavar var a end metavar imply not0 metavar var a end metavar cut prop lemma tertium non datur conclude not0 metavar var a end metavar imply not0 metavar var a end metavar cut prop lemma from disjuncts modus ponens not0 metavar var a end metavar imply not0 metavar var a end metavar modus ponens metavar var a end metavar imply not0 metavar var a end metavar modus ponens not0 metavar var a end metavar imply not0 metavar var a end metavar conclude not0 metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "

" [ math define statement of prop lemma from three disjuncts as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed not0 metavar var a end metavar imply not0 metavar var b end metavar imply metavar var c end metavar infer metavar var a end metavar imply metavar var d end metavar infer metavar var b end metavar imply metavar var d end metavar infer metavar var c end metavar imply metavar var d end metavar infer metavar var d end metavar end define end math ] "

" [ math define proof of prop lemma from three disjuncts as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed not0 metavar var a end metavar imply not0 metavar var b end metavar imply metavar var c end metavar infer metavar var b end metavar imply metavar var d end metavar infer metavar var c end metavar imply metavar var d end metavar infer not0 metavar var a end metavar infer 1rule repetition modus ponens not0 metavar var a end metavar imply not0 metavar var b end metavar imply metavar var c end metavar conclude not0 metavar var a end metavar imply not0 metavar var b end metavar imply metavar var c end metavar cut 1rule mp modus ponens not0 metavar var a end metavar imply not0 metavar var b end metavar imply metavar var c end metavar modus ponens not0 metavar var a end metavar conclude not0 metavar var b end metavar imply metavar var c end metavar cut prop lemma from disjuncts modus ponens not0 metavar var b end metavar imply metavar var c end metavar modus ponens metavar var b end metavar imply metavar var d end metavar modus ponens metavar var c end metavar imply metavar var d end metavar conclude metavar var d end metavar cut all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed 1rule deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed not0 metavar var a end metavar imply not0 metavar var b end metavar imply metavar var c end metavar infer metavar var b end metavar imply metavar var d end metavar infer metavar var c end metavar imply metavar var d end metavar infer not0 metavar var a end metavar infer metavar var d end metavar conclude not0 metavar var a end metavar imply not0 metavar var b end metavar imply metavar var c end metavar imply metavar var b end metavar imply metavar var d end metavar imply metavar var c end metavar imply metavar var d end metavar imply not0 metavar var a end metavar imply metavar var d end metavar cut prop lemma auto imply conclude metavar var a end metavar imply metavar var d end metavar imply metavar var a end metavar imply metavar var d end metavar cut not0 metavar var a end metavar imply not0 metavar var b end metavar imply metavar var c end metavar infer metavar var a end metavar imply metavar var d end metavar infer metavar var b end metavar imply metavar var d end metavar infer metavar var c end metavar imply metavar var d end metavar infer prop lemma mp3 modus ponens not0 metavar var a end metavar imply not0 metavar var b end metavar imply metavar var c end metavar imply metavar var b end metavar imply metavar var d end metavar imply metavar var c end metavar imply metavar var d end metavar imply not0 metavar var a end metavar imply metavar var d end metavar modus ponens not0 metavar var a end metavar imply not0 metavar var b end metavar imply metavar var c end metavar modus ponens metavar var b end metavar imply metavar var d end metavar modus ponens metavar var c end metavar imply metavar var d end metavar conclude not0 metavar var a end metavar imply metavar var d end metavar cut 1rule mp modus ponens metavar var a end metavar imply metavar var d end metavar imply metavar var a end metavar imply metavar var d end metavar modus ponens metavar var a end metavar imply metavar var d end metavar conclude metavar var a end metavar imply metavar var d end metavar cut prop lemma from negations modus ponens metavar var a end metavar imply metavar var d end metavar modus ponens not0 metavar var a end metavar imply metavar var d end metavar conclude metavar var d end metavar end quote state proof state cache var c end expand end define end math ] "

" [ math define statement of prop lemma negate first disjunct as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed not0 metavar var a end metavar imply metavar var b end metavar infer not0 metavar var a end metavar infer metavar var b end metavar end define end math ] "

" [ math define proof of prop lemma negate first disjunct as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed not0 metavar var a end metavar imply metavar var b end metavar infer not0 metavar var a end metavar infer 1rule repetition modus ponens not0 metavar var a end metavar imply metavar var b end metavar conclude not0 metavar var a end metavar imply metavar var b end metavar cut 1rule mp modus ponens not0 metavar var a end metavar imply metavar var b end metavar modus ponens not0 metavar var a end metavar conclude metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "


" [ math define statement of prop lemma negate second disjunct as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed not0 metavar var a end metavar imply metavar var b end metavar infer not0 metavar var b end metavar infer metavar var a end metavar end define end math ] "

" [ math define proof of prop lemma negate second disjunct as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed not0 metavar var a end metavar imply metavar var b end metavar infer not0 metavar var b end metavar infer 1rule repetition modus ponens not0 metavar var a end metavar imply metavar var b end metavar conclude not0 metavar var a end metavar imply metavar var b end metavar cut prop lemma negative mt modus ponens not0 metavar var a end metavar imply metavar var b end metavar modus ponens not0 metavar var b end metavar conclude metavar var a end metavar end quote state proof state cache var c end expand end define end math ] "

(***)

" [ math define statement of prop lemma expand disjuncts as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed not0 metavar var a end metavar imply metavar var b end metavar infer not0 metavar var c end metavar imply metavar var d end metavar infer not0 metavar var b end metavar imply not0 metavar var d end metavar imply not0 metavar var a end metavar imply not0 metavar var c end metavar end define end math ] "

" [ math define proof of prop lemma expand disjuncts as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed not0 metavar var a end metavar imply metavar var b end metavar infer not0 metavar var c end metavar imply metavar var d end metavar infer not0 metavar var b end metavar infer not0 metavar var d end metavar infer prop lemma negate second disjunct modus ponens not0 metavar var a end metavar imply metavar var b end metavar modus ponens not0 metavar var b end metavar conclude metavar var a end metavar cut prop lemma negate second disjunct modus ponens not0 metavar var c end metavar imply metavar var d end metavar modus ponens not0 metavar var d end metavar conclude metavar var c end metavar cut prop lemma join conjuncts modus ponens metavar var a end metavar modus ponens metavar var c end metavar conclude not0 metavar var a end metavar imply not0 metavar var c end metavar cut all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed 1rule deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed not0 metavar var a end metavar imply metavar var b end metavar infer not0 metavar var c end metavar imply metavar var d end metavar infer not0 metavar var b end metavar infer not0 metavar var d end metavar infer not0 metavar var a end metavar imply not0 metavar var c end metavar conclude not0 metavar var a end metavar imply metavar var b end metavar imply not0 metavar var c end metavar imply metavar var d end metavar imply not0 metavar var b end metavar imply not0 metavar var d end metavar imply not0 metavar var a end metavar imply not0 metavar var c end metavar cut not0 metavar var a end metavar imply metavar var b end metavar infer not0 metavar var c end metavar imply metavar var d end metavar infer prop lemma mp2 modus ponens not0 metavar var a end metavar imply metavar var b end metavar imply not0 metavar var c end metavar imply metavar var d end metavar imply not0 metavar var b end metavar imply not0 metavar var d end metavar imply not0 metavar var a end metavar imply not0 metavar var c end metavar modus ponens not0 metavar var a end metavar imply metavar var b end metavar modus ponens not0 metavar var c end metavar imply metavar var d end metavar conclude not0 metavar var b end metavar imply not0 metavar var d end metavar imply not0 metavar var a end metavar imply not0 metavar var c end metavar cut 1rule repetition modus ponens not0 metavar var b end metavar imply not0 metavar var d end metavar imply not0 metavar var a end metavar imply not0 metavar var c end metavar conclude not0 metavar var b end metavar imply not0 metavar var d end metavar imply not0 metavar var a end metavar imply not0 metavar var c end metavar end quote state proof state cache var c end expand end define end math ] "


" [ math define statement of prop lemma from two times two disjuncts as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed all metavar var e end metavar indeed not0 metavar var a end metavar imply metavar var b end metavar infer not0 metavar var c end metavar imply metavar var d end metavar infer metavar var a end metavar imply metavar var c end metavar imply metavar var e end metavar infer metavar var a end metavar imply metavar var d end metavar imply metavar var e end metavar infer metavar var b end metavar imply metavar var c end metavar imply metavar var e end metavar infer metavar var b end metavar imply metavar var d end metavar imply metavar var e end metavar infer metavar var e end metavar end define end math ] "

" [ math define proof of prop lemma from two times two disjuncts as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed all metavar var e end metavar indeed not0 metavar var c end metavar imply metavar var d end metavar infer metavar var a end metavar imply metavar var c end metavar imply metavar var e end metavar infer metavar var a end metavar imply metavar var d end metavar imply metavar var e end metavar infer metavar var a end metavar infer 1rule mp modus ponens metavar var a end metavar imply metavar var c end metavar imply metavar var e end metavar modus ponens metavar var a end metavar conclude metavar var c end metavar imply metavar var e end metavar cut 1rule mp modus ponens metavar var a end metavar imply metavar var d end metavar imply metavar var e end metavar modus ponens metavar var a end metavar conclude metavar var d end metavar imply metavar var e end metavar cut prop lemma from disjuncts modus ponens not0 metavar var c end metavar imply metavar var d end metavar modus ponens metavar var c end metavar imply metavar var e end metavar modus ponens metavar var d end metavar imply metavar var e end metavar conclude metavar var e end metavar cut all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed all metavar var e end metavar indeed not0 metavar var a end metavar imply metavar var b end metavar infer not0 metavar var c end metavar imply metavar var d end metavar infer metavar var b end metavar imply metavar var c end metavar imply metavar var e end metavar infer metavar var b end metavar imply metavar var d end metavar imply metavar var e end metavar infer not0 metavar var a end metavar infer prop lemma negate first disjunct modus ponens not0 metavar var a end metavar imply metavar var b end metavar modus ponens not0 metavar var a end metavar conclude metavar var b end metavar cut 1rule mp modus ponens metavar var b end metavar imply metavar var c end metavar imply metavar var e end metavar modus ponens metavar var b end metavar conclude metavar var c end metavar imply metavar var e end metavar cut 1rule mp modus ponens metavar var b end metavar imply metavar var d end metavar imply metavar var e end metavar modus ponens metavar var b end metavar conclude metavar var d end metavar imply metavar var e end metavar cut prop lemma from disjuncts modus ponens not0 metavar var c end metavar imply metavar var d end metavar modus ponens metavar var c end metavar imply metavar var e end metavar modus ponens metavar var d end metavar imply metavar var e end metavar conclude metavar var e end metavar cut all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed all metavar var e end metavar indeed 1rule deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed all metavar var e end metavar indeed not0 metavar var c end metavar imply metavar var d end metavar infer metavar var a end metavar imply metavar var c end metavar imply metavar var e end metavar infer metavar var a end metavar imply metavar var d end metavar imply metavar var e end metavar infer metavar var a end metavar infer metavar var e end metavar conclude not0 metavar var c end metavar imply metavar var d end metavar imply metavar var a end metavar imply metavar var c end metavar imply metavar var e end metavar imply metavar var a end metavar imply metavar var d end metavar imply metavar var e end metavar imply metavar var a end metavar imply metavar var e end metavar cut 1rule deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed all metavar var e end metavar indeed not0 metavar var a end metavar imply metavar var b end metavar infer not0 metavar var c end metavar imply metavar var d end metavar infer metavar var b end metavar imply metavar var c end metavar imply metavar var e end metavar infer metavar var b end metavar imply metavar var d end metavar imply metavar var e end metavar infer not0 metavar var a end metavar infer metavar var e end metavar conclude not0 metavar var a end metavar imply metavar var b end metavar imply not0 metavar var c end metavar imply metavar var d end metavar imply metavar var b end metavar imply metavar var c end metavar imply metavar var e end metavar imply metavar var b end metavar imply metavar var d end metavar imply metavar var e end metavar imply not0 metavar var a end metavar imply metavar var e end metavar cut not0 metavar var a end metavar imply metavar var b end metavar infer not0 metavar var c end metavar imply metavar var d end metavar infer metavar var a end metavar imply metavar var c end metavar imply metavar var e end metavar infer metavar var a end metavar imply metavar var d end metavar imply metavar var e end metavar infer metavar var b end metavar imply metavar var c end metavar imply metavar var e end metavar infer metavar var b end metavar imply metavar var d end metavar imply metavar var e end metavar infer prop lemma mp3 modus ponens not0 metavar var c end metavar imply metavar var d end metavar imply metavar var a end metavar imply metavar var c end metavar imply metavar var e end metavar imply metavar var a end metavar imply metavar var d end metavar imply metavar var e end metavar imply metavar var a end metavar imply metavar var e end metavar modus ponens not0 metavar var c end metavar imply metavar var d end metavar modus ponens metavar var a end metavar imply metavar var c end metavar imply metavar var e end metavar modus ponens metavar var a end metavar imply metavar var d end metavar imply metavar var e end metavar conclude metavar var a end metavar imply metavar var e end metavar cut prop lemma mp4 modus ponens not0 metavar var a end metavar imply metavar var b end metavar imply not0 metavar var c end metavar imply metavar var d end metavar imply metavar var b end metavar imply metavar var c end metavar imply metavar var e end metavar imply metavar var b end metavar imply metavar var d end metavar imply metavar var e end metavar imply not0 metavar var a end metavar imply metavar var e end metavar modus ponens not0 metavar var a end metavar imply metavar var b end metavar modus ponens not0 metavar var c end metavar imply metavar var d end metavar modus ponens metavar var b end metavar imply metavar var c end metavar imply metavar var e end metavar modus ponens metavar var b end metavar imply metavar var d end metavar imply metavar var e end metavar conclude not0 metavar var a end metavar imply metavar var e end metavar cut prop lemma from negations modus ponens metavar var a end metavar imply metavar var e end metavar modus ponens not0 metavar var a end metavar imply metavar var e end metavar conclude metavar var e end metavar end quote state proof state cache var c end expand end define end math ] "














(*** SAME-F ***)
XX-am

(*** R-AFDELINGEN ***)
XX-am


(*******************)

" [ math define statement of prop lemma from negated imply as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed not0 metavar var a end metavar imply metavar var b end metavar infer not0 metavar var a end metavar imply not0 not0 metavar var b end metavar end define end math ] "

" [ math define proof of prop lemma from negated imply as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply not0 not0 metavar var b end metavar infer metavar var a end metavar infer 1rule mp modus ponens metavar var a end metavar imply not0 not0 metavar var b end metavar modus ponens metavar var a end metavar conclude not0 not0 metavar var b end metavar cut prop lemma remove double neg modus ponens not0 not0 metavar var b end metavar conclude metavar var b end metavar cut all metavar var a end metavar indeed all metavar var b end metavar indeed 1rule deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed metavar var a end metavar imply not0 not0 metavar var b end metavar infer metavar var a end metavar infer metavar var b end metavar conclude metavar var a end metavar imply not0 not0 metavar var b end metavar imply metavar var a end metavar imply metavar var b end metavar cut not0 metavar var a end metavar imply metavar var b end metavar infer prop lemma mt modus ponens metavar var a end metavar imply not0 not0 metavar var b end metavar imply metavar var a end metavar imply metavar var b end metavar modus ponens not0 metavar var a end metavar imply metavar var b end metavar conclude not0 metavar var a end metavar imply not0 not0 metavar var b end metavar cut 1rule repetition modus ponens not0 metavar var a end metavar imply not0 not0 metavar var b end metavar conclude not0 metavar var a end metavar imply not0 not0 metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "

(***)


" [ math define statement of prop lemma from negated double imply as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not0 metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar infer not0 not0 metavar var a end metavar imply not0 metavar var b end metavar imply not0 not0 metavar var c end metavar end define end math ] "

" [ math define proof of prop lemma from negated double imply as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed not0 metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar infer prop lemma from negated imply modus ponens not0 metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar conclude not0 metavar var a end metavar imply not0 not0 metavar var b end metavar imply metavar var c end metavar cut prop lemma first conjunct modus ponens not0 metavar var a end metavar imply not0 not0 metavar var b end metavar imply metavar var c end metavar conclude metavar var a end metavar cut prop lemma second conjunct modus ponens not0 metavar var a end metavar imply not0 not0 metavar var b end metavar imply metavar var c end metavar conclude not0 metavar var b end metavar imply metavar var c end metavar cut prop lemma from negated imply modus ponens not0 metavar var b end metavar imply metavar var c end metavar conclude not0 metavar var b end metavar imply not0 not0 metavar var c end metavar cut prop lemma first conjunct modus ponens not0 metavar var b end metavar imply not0 not0 metavar var c end metavar conclude metavar var b end metavar cut prop lemma second conjunct modus ponens not0 metavar var b end metavar imply not0 not0 metavar var c end metavar conclude not0 metavar var c end metavar cut prop lemma join conjuncts modus ponens metavar var a end metavar modus ponens metavar var b end metavar conclude not0 metavar var a end metavar imply not0 metavar var b end metavar cut prop lemma join conjuncts modus ponens not0 metavar var a end metavar imply not0 metavar var b end metavar modus ponens not0 metavar var c end metavar conclude not0 not0 metavar var a end metavar imply not0 metavar var b end metavar imply not0 not0 metavar var c end metavar end quote state proof state cache var c end expand end define end math ] "





" [ math define statement of prop lemma from negated or as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed not0 not0 metavar var a end metavar imply metavar var b end metavar infer not0 not0 metavar var a end metavar imply not0 not0 metavar var b end metavar end define end math ] "

" [ math define proof of prop lemma from negated or as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed not0 not0 metavar var a end metavar imply metavar var b end metavar infer 1rule repetition modus ponens not0 not0 metavar var a end metavar imply metavar var b end metavar conclude not0 not0 metavar var a end metavar imply metavar var b end metavar cut prop lemma from negated imply modus ponens not0 not0 metavar var a end metavar imply metavar var b end metavar conclude not0 not0 metavar var a end metavar imply not0 not0 metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "


" [ math define statement of axiom induction as system Q infer all metavar var v1 end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed meta-sub metavar var b end metavar is metavar var a end metavar where metavar var v1 end metavar is 0 end sub endorse meta-sub metavar var c end metavar is metavar var a end metavar where metavar var v1 end metavar is metavar var v1 end metavar + 1 end sub endorse metavar var b end metavar imply for all objects metavar var v1 end metavar indeed metavar var a end metavar imply metavar var c end metavar imply for all objects metavar var v1 end metavar indeed metavar var a end metavar end define , define proof of axiom induction as rule tactic end define end math ] "


" [ math define statement of 1rule lessMinus1(N) as system Q infer all metavar var m end metavar indeed all metavar var n end metavar indeed Nat( metavar var m end metavar ) endorse Nat( metavar var n end metavar ) endorse not0 metavar var m end metavar <= metavar var n end metavar + 1 imply not0 not0 metavar var m end metavar = metavar var n end metavar + 1 infer metavar var m end metavar <= metavar var n end metavar end define , define proof of 1rule lessMinus1(N) as rule tactic end define end math ] "

" [ math define statement of axiom nonnegative(N) as system Q infer all metavar var m end metavar indeed Nat( metavar var m end metavar ) endorse 0 <= metavar var m end metavar end define , define proof of axiom nonnegative(N) as rule tactic end define end math ] "



--------------

" [ math define statement of axiom cauchy as system Q infer all metavar var v1 end metavar indeed all metavar var v2 end metavar indeed all metavar var n end metavar indeed all metavar var ep end metavar indeed all metavar var fx end metavar indeed for all objects metavar var ep end metavar indeed not0 for all objects metavar var n end metavar indeed not0 for all objects metavar var v1 end metavar indeed for all objects metavar var v2 end metavar indeed not0 0 <= metavar var ep end metavar imply not0 not0 0 = metavar var ep end metavar imply metavar var n end metavar <= metavar var v1 end metavar imply metavar var n end metavar <= metavar var v2 end metavar imply not0 | [ metavar var fx end metavar ; metavar var v1 end metavar ] + - [ metavar var fx end metavar ; metavar var v2 end metavar ] | <= metavar var ep end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var v1 end metavar ] + - [ metavar var fx end metavar ; metavar var v2 end metavar ] | = metavar var ep end metavar end define , define proof of axiom cauchy as rule tactic end define end math ] "

-------------





--------------

" [ math define statement of prop lemma doubly conditioned join conjuncts as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar infer metavar var a end metavar imply metavar var b end metavar imply metavar var d end metavar infer metavar var a end metavar imply metavar var b end metavar imply not0 metavar var c end metavar imply not0 metavar var d end metavar end define end math ] "

" [ math define proof of prop lemma doubly conditioned join conjuncts as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar infer metavar var a end metavar imply metavar var b end metavar imply metavar var d end metavar infer metavar var a end metavar infer metavar var b end metavar infer prop lemma mp2 modus ponens metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar modus ponens metavar var a end metavar modus ponens metavar var b end metavar conclude metavar var c end metavar cut prop lemma mp2 modus ponens metavar var a end metavar imply metavar var b end metavar imply metavar var d end metavar modus ponens metavar var a end metavar modus ponens metavar var b end metavar conclude metavar var d end metavar cut prop lemma join conjuncts modus ponens metavar var c end metavar modus ponens metavar var d end metavar conclude not0 metavar var c end metavar imply not0 metavar var d end metavar cut all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed 1rule deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar infer metavar var a end metavar imply metavar var b end metavar imply metavar var d end metavar infer metavar var a end metavar infer metavar var b end metavar infer not0 metavar var c end metavar imply not0 metavar var d end metavar conclude metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar imply metavar var a end metavar imply metavar var b end metavar imply metavar var d end metavar imply metavar var a end metavar imply metavar var b end metavar imply not0 metavar var c end metavar imply not0 metavar var d end metavar cut metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar infer metavar var a end metavar imply metavar var b end metavar imply metavar var d end metavar infer prop lemma mp2 modus ponens metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar imply metavar var a end metavar imply metavar var b end metavar imply metavar var d end metavar imply metavar var a end metavar imply metavar var b end metavar imply not0 metavar var c end metavar imply not0 metavar var d end metavar modus ponens metavar var a end metavar imply metavar var b end metavar imply metavar var c end metavar modus ponens metavar var a end metavar imply metavar var b end metavar imply metavar var d end metavar conclude metavar var a end metavar imply metavar var b end metavar imply not0 metavar var c end metavar imply not0 metavar var d end metavar end quote state proof state cache var c end expand end define end math ] "


----------------

" [ math define statement of prop lemma from negated and as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed not0 not0 metavar var a end metavar imply not0 metavar var b end metavar infer metavar var a end metavar infer not0 metavar var b end metavar end define end math ] "

" [ math define proof of prop lemma from negated and as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed not0 not0 metavar var a end metavar imply not0 metavar var b end metavar infer metavar var a end metavar infer 1rule repetition modus ponens not0 not0 metavar var a end metavar imply not0 metavar var b end metavar conclude not0 not0 metavar var a end metavar imply not0 metavar var b end metavar cut prop lemma remove double neg modus ponens not0 not0 metavar var a end metavar imply not0 metavar var b end metavar conclude metavar var a end metavar imply not0 metavar var b end metavar cut 1rule mp modus ponens metavar var a end metavar imply not0 metavar var b end metavar modus ponens metavar var a end metavar conclude not0 metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "

--------


----------

" [ math define statement of prop lemma to negated or as system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed not0 not0 metavar var a end metavar imply not0 not0 metavar var b end metavar infer not0 not0 metavar var a end metavar imply metavar var b end metavar end define end math ] "

" [ math define proof of prop lemma to negated or as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var a end metavar indeed all metavar var b end metavar indeed not0 not0 metavar var a end metavar imply not0 not0 metavar var b end metavar infer not0 metavar var a end metavar imply metavar var b end metavar infer prop lemma first conjunct modus ponens not0 not0 metavar var a end metavar imply not0 not0 metavar var b end metavar conclude not0 metavar var a end metavar cut prop lemma second conjunct modus ponens not0 not0 metavar var a end metavar imply not0 not0 metavar var b end metavar conclude not0 metavar var b end metavar cut prop lemma negate first disjunct modus ponens not0 metavar var a end metavar imply metavar var b end metavar modus ponens not0 metavar var a end metavar conclude metavar var b end metavar cut prop lemma from contradiction modus ponens metavar var b end metavar modus ponens not0 metavar var b end metavar conclude not0 not0 metavar var a end metavar imply metavar var b end metavar cut all metavar var a end metavar indeed all metavar var b end metavar indeed 1rule deduction modus ponens all metavar var a end metavar indeed all metavar var b end metavar indeed not0 not0 metavar var a end metavar imply not0 not0 metavar var b end metavar infer not0 metavar var a end metavar imply metavar var b end metavar infer not0 not0 metavar var a end metavar imply metavar var b end metavar conclude not0 not0 metavar var a end metavar imply not0 not0 metavar var b end metavar imply not0 metavar var a end metavar imply metavar var b end metavar imply not0 not0 metavar var a end metavar imply metavar var b end metavar cut not0 not0 metavar var a end metavar imply not0 not0 metavar var b end metavar infer 1rule mp modus ponens not0 not0 metavar var a end metavar imply not0 not0 metavar var b end metavar imply not0 metavar var a end metavar imply metavar var b end metavar imply not0 not0 metavar var a end metavar imply metavar var b end metavar modus ponens not0 not0 metavar var a end metavar imply not0 not0 metavar var b end metavar conclude not0 metavar var a end metavar imply metavar var b end metavar imply not0 not0 metavar var a end metavar imply metavar var b end metavar cut prop lemma imply negation modus ponens not0 metavar var a end metavar imply metavar var b end metavar imply not0 not0 metavar var a end metavar imply metavar var b end metavar conclude not0 not0 metavar var a end metavar imply metavar var b end metavar end quote state proof state cache var c end expand end define end math ] "




--------------------

" [ math define statement of 1rule nextXS(upperBound) as system Q infer all metavar var m end metavar indeed upperBound( 01//02 ** [ xs ; metavar var m end metavar ] ++ [ us ; metavar var m end metavar ] , setOfReals ) infer [ xs ; metavar var m end metavar + 1 ] == [ xs ; metavar var m end metavar ] end define , define proof of 1rule nextXS(upperBound) as rule tactic end define end math ] "

" [ math define statement of 1rule nextXS(noUpperBound) as system Q infer all metavar var m end metavar indeed not0 upperBound( 01//02 ** [ xs ; metavar var m end metavar ] ++ [ us ; metavar var m end metavar ] , setOfReals ) infer [ xs ; metavar var m end metavar + 1 ] == 01//02 ** [ xs ; metavar var m end metavar ] ++ [ us ; metavar var m end metavar ] end define , define proof of 1rule nextXS(noUpperBound) as rule tactic end define end math ] "

" [ math define statement of 1rule nextUS(upperBound) as system Q infer all metavar var m end metavar indeed upperBound( 01//02 ** [ xs ; metavar var m end metavar ] ++ [ us ; metavar var m end metavar ] , setOfReals ) infer [ us ; metavar var m end metavar + 1 ] == 01//02 ** [ xs ; metavar var m end metavar ] ++ [ us ; metavar var m end metavar ] end define , define proof of 1rule nextUS(upperBound) as rule tactic end define end math ] "

" [ math define statement of 1rule nextUS(noUpperBound) as system Q infer all metavar var m end metavar indeed not0 upperBound( 01//02 ** [ xs ; metavar var m end metavar ] ++ [ us ; metavar var m end metavar ] , setOfReals ) infer [ us ; metavar var m end metavar + 1 ] == [ us ; metavar var m end metavar ] end define , define proof of 1rule nextUS(noUpperBound) as rule tactic end define end math ] "

" [ math define statement of axiom US0 as system Q infer [ us ; 0 ] == [ xs ; 0 ] ++ R( 1f ) end define , define proof of axiom US0 as rule tactic end define end math ] "

" [ math define statement of 1rule expZero as system Q infer all metavar var m end metavar indeed all metavar var x end metavar indeed metavar var m end metavar = 0 infer metavar var x end metavar ^ metavar var m end metavar = 1 end define , define proof of 1rule expZero as rule tactic end define end math ] "

" [ math define statement of 1rule expPositive as system Q infer all metavar var m end metavar indeed all metavar var x end metavar indeed not0 0 <= metavar var m end metavar imply not0 not0 0 = metavar var m end metavar infer metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar + - 1 end define , define proof of 1rule expPositive as rule tactic end define end math ] "

--------------

" [ math define statement of 1rule base(1/2)Sum zero as system Q infer all metavar var m end metavar indeed all metavar var n end metavar indeed metavar var n end metavar = 0 infer base(1/2)Sum( metavar var m end metavar , metavar var n end metavar ) = 1/ 1 + 1 ^ metavar var m end metavar end define , define proof of 1rule base(1/2)Sum zero as rule tactic end define end math ] "

" [ math define statement of 1rule base(1/2)Sum positive as system Q infer all metavar var m end metavar indeed all metavar var n end metavar indeed not0 0 <= metavar var n end metavar imply not0 not0 0 = metavar var n end metavar infer base(1/2)Sum( metavar var m end metavar , metavar var n end metavar ) = 1/ 1 + 1 ^ metavar var m end metavar + metavar var n end metavar + base(1/2)Sum( metavar var m end metavar , metavar var n end metavar + - 1 ) end define , define proof of 1rule base(1/2)Sum positive as rule tactic end define end math ] "

------------

" [ math define statement of 1rule UStelescope zero as system Q infer all metavar var m end metavar indeed all metavar var n end metavar indeed metavar var n end metavar = 0 infer UStelescope( metavar var m end metavar , metavar var n end metavar ) = | [ us ; metavar var m end metavar ] + - [ us ; metavar var m end metavar + 1 ] | end define , define proof of 1rule UStelescope zero as rule tactic end define end math ] "

" [ math define statement of 1rule UStelescope positive as system Q infer all metavar var m end metavar indeed all metavar var n end metavar indeed not0 0 <= metavar var n end metavar imply not0 not0 0 = metavar var n end metavar infer UStelescope( metavar var m end metavar , metavar var n end metavar ) = | [ us ; metavar var m end metavar + metavar var n end metavar ] + - [ us ; metavar var m end metavar + metavar var n end metavar + 1 ] | + UStelescope( metavar var m end metavar , metavar var n end metavar + - 1 ) end define , define proof of 1rule UStelescope positive as rule tactic end define end math ] "


" [ math define macro of ( var x ) as lambda var t dot lambda var s dot lambda var c dot macro define four var t state var s cache var c definition quote macro define ( var x ) as parenthesis var x end parenthesis end define end quote end define end define end math ] "

----------


" [ math define statement of 1rule adhoc eqAddition(R) as system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var fz end metavar indeed R( metavar var fx end metavar ) = R( metavar var fy end metavar ) infer R( metavar var fx end metavar ) ++ R( metavar var fz end metavar ) = R( metavar var fy end metavar ) ++ R( metavar var fz end metavar ) end define , define proof of 1rule adhoc eqAddition(R) as rule tactic end define end math ] "

" [ math define statement of lemma plusCommutativity(R) as system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed R( metavar var fx end metavar ) ++ R( metavar var fy end metavar ) == R( metavar var fy end metavar ) ++ R( metavar var fx end metavar ) end define , define proof of lemma plusCommutativity(R) as rule tactic end define end math ] "


---------------

" [ math define statement of lemma plusAssociativity(R) as system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var fz end metavar indeed R( metavar var fx end metavar ) ++ R( metavar var fy end metavar ) ++ R( metavar var fz end metavar ) = R( metavar var fx end metavar ) ++ R( metavar var fy end metavar ) ++ R( metavar var fz end metavar ) end define , define proof of lemma plusAssociativity(R) as rule tactic end define end math ] "

" [ math define statement of lemma plusAssociativity(R)XX as system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var fz end metavar indeed R( metavar var fx end metavar +f metavar var fy end metavar +f metavar var fz end metavar ) == R( metavar var fx end metavar +f metavar var fy end metavar +f metavar var fz end metavar ) end define , define proof of lemma plusAssociativity(R)XX as rule tactic end define end math ] "

" [ math define statement of lemma plus0(R) as system Q infer all metavar var fx end metavar indeed R( metavar var fx end metavar ) ++ R( 0f ) == R( metavar var fx end metavar ) end define , define proof of lemma plus0(R) as rule tactic end define end math ] "

" [ math define statement of lemma negative(R) as system Q infer all metavar var m end metavar indeed all metavar var fx end metavar indeed R( metavar var fx end metavar ) ++ -- R( metavar var fx end metavar ) == R( 0f ) end define , define proof of lemma negative(R) as rule tactic end define end math ] "

" [ math define statement of lemma timesAssociativity(R) as system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var fz end metavar indeed R( metavar var fx end metavar ) ** R( metavar var fy end metavar ) ** R( metavar var fz end metavar ) == R( metavar var fx end metavar ) ** R( metavar var fy end metavar ) ** R( metavar var fz end metavar ) end define , define proof of lemma timesAssociativity(R) as rule tactic end define end math ] "

" [ math define statement of lemma times1(R) as system Q infer all metavar var fx end metavar indeed R( metavar var fx end metavar ) ** R( 1f ) == R( metavar var fx end metavar ) end define , define proof of lemma times1(R) as rule tactic end define end math ] "


" [ math var a end math ] "

venter-------




" [ flush left math define priority of kvanti as preassociative priority kvanti 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 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 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 1rule adhoc sameR equal priority lemma separation2formula(1) equal priority lemma separation2formula(2) equal priority axiom cauchy equal priority axiom plusF equal priority axiom reciprocalF equal priority 1rule from== equal priority 1rule to== equal priority 1rule fromInR equal priority lemma plusR(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 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 numericalF 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) end priority greater than preassociative priority x sub x end sub equal priority x intro x index x pyk x tex x end intro equal priority x intro x pyk x tex x end intro equal priority x intro x index x pyk x tex x name x end intro equal priority x intro x pyk x tex x name x end intro equal priority x prime equal priority x assoc x end assoc equal priority x set x to x end set equal priority x set multi x to x end set equal priority x bit nil equal priority x bit one equal priority binary equal priority x color x end color equal priority x color star x end color equal priority x raw head equal priority x raw tail equal priority x cardinal untag equal priority x head equal priority x tail equal priority x is singular equal priority x is cardinal equal priority x is data equal priority x is atomic equal priority x cardinal retract equal priority x tagged retract equal priority x boolean retract equal priority x ref equal priority x id equal priority x debug equal priority x root equal priority x zeroth equal priority x first equal priority x second equal priority x third equal priority x fourth equal priority x fifth equal priority x sixth equal priority x seventh equal priority x eighth equal priority x ninth equal priority x is error equal priority x is metavar equal priority x is metaclosed equal priority x is metaclosed star equal priority x hide end priority greater than preassociative priority unicode start of text x end unicode text equal priority unicode end of text equal priority text x end text equal priority text x plus x equal priority text x plus indent x equal priority unicode newline x equal priority unicode space x equal priority unicode exclamation mark x equal priority unicode quotation mark x equal priority unicode number sign x equal priority unicode dollar sign x equal priority unicode percent x equal priority unicode ampersand x equal priority unicode apostrophe x equal priority unicode left parenthesis x equal priority unicode right parenthesis x equal priority unicode asterisk x equal priority unicode plus sign x equal priority unicode comma x equal priority unicode hyphen x equal priority unicode period x equal priority unicode slash x equal priority unicode zero x equal priority unicode one x equal priority unicode two x equal priority unicode three x equal priority unicode four x equal priority unicode five x equal priority unicode six x equal priority unicode seven x equal priority unicode eight x equal priority unicode nine x equal priority unicode colon x equal priority unicode semicolon x equal priority unicode less than x equal priority unicode equal sign x equal priority unicode greater than x equal priority unicode question mark x equal priority unicode commercial at x equal priority unicode capital a x equal priority unicode capital b x equal priority unicode capital c x equal priority unicode capital d x equal priority unicode capital e x equal priority unicode capital f x equal priority unicode capital g x equal priority unicode capital h x equal priority unicode capital i x equal priority unicode capital j x equal priority unicode capital k x equal priority unicode capital l x equal priority unicode capital m x equal priority unicode capital n x equal priority unicode capital o x equal priority unicode capital p x equal priority unicode capital q x equal priority unicode capital r x equal priority unicode capital s x equal priority unicode capital t x equal priority unicode capital u x equal priority unicode capital v x equal priority unicode capital w x equal priority unicode capital x x equal priority unicode capital y x equal priority unicode capital z x equal priority unicode left bracket x equal priority unicode backslash x equal priority unicode right bracket x equal priority unicode circumflex x equal priority unicode underscore x equal priority unicode grave accent x equal priority unicode small a x equal priority unicode small b x equal priority unicode small c x equal priority unicode small d x equal priority unicode small e x equal priority unicode small f x equal priority unicode small g x equal priority unicode small h x equal priority unicode small i x equal priority unicode small j x equal priority unicode small k x equal priority unicode small l x equal priority unicode small m x equal priority unicode small n x equal priority unicode small o x equal priority unicode small p x equal priority unicode small q x equal priority unicode small r x equal priority unicode small s x equal priority unicode small t x equal priority unicode small u x equal priority unicode small v x equal priority unicode small w x equal priority unicode small x x equal priority unicode small y x equal priority unicode small z x equal priority unicode left brace x equal priority unicode vertical line x equal priority unicode right brace x equal priority unicode tilde x equal priority preassociative x greater than x equal priority postassociative x greater than x equal priority priority x equal x equal priority priority x end priority equal priority newline x equal priority macro newline x equal priority macro indent x end priority greater than preassociative priority x apply x equal priority x tagged apply x end priority greater than preassociative priority x ^ x end priority greater than preassociative priority x suc equal priority R( x ) equal priority --R( x ) equal priority 1/ x end priority greater than preassociative priority eq-system of x modulo x equal priority intersection x comma x end intersection equal priority [ x ; x ] end priority greater than preassociative priority union x end union equal priority binary-union x comma x end union equal priority power x end power end priority greater than preassociative priority zermelo singleton x end singleton equal priority stateExpand( x , x , x ) equal priority extractSeries( x ) equal priority setOfSeries( x ) equal priority --Macro( x ) equal priority expandList( x , x , x ) equal priority **Macro( x ) equal priority ++Macro( x ) equal priority <
\section{Pyk definitioner} \label{sec:pyk}

\begin{flushleft}
" [ math define pyk of lemma uniqueMember as text "lemma uniqueMember" end text end define linebreak define pyk of lemma uniqueMember(Type) as text "lemma uniqueMember(Type)" end text end define linebreak define pyk of lemma sameSeries as text "lemma sameSeries" end text end define linebreak define pyk of lemma a4 as text "lemma a4" end text end define linebreak define pyk of lemma sameMember as text "lemma sameMember" end text end define linebreak define pyk of 1rule Qclosed(Addition) as text "1rule Qclosed(Addition)" end text end define linebreak define pyk of 1rule Qclosed(Multiplication) as text "1rule Qclosed(Multiplication)" end text end define linebreak define pyk of 1rule fromCartProd(1) as text "1rule fromCartProd(1)" end text end define linebreak define pyk of 1rule fromCartProd(2) as text "1rule fromCartProd(2)" end text end define linebreak define pyk of constantRationalSeries( x ) as text "constantRationalSeries( "! )" end text end define linebreak define pyk of cartProd( x , x ) as text "cartProd( "! , "! )" end text end define linebreak define pyk of P( x ) as text "P( "! )" end text end define linebreak define pyk of binaryUnion( x , x ) as text "binaryUnion( "! , "! )" end text end define linebreak define pyk of setOfRationalSeries as text "setOfRationalSeries" end text end define linebreak define pyk of isSubset( x , x ) as text "isSubset( "! , "! )" end text end define linebreak define pyk of (p x , x ) as text "(p "! , "! )" end text end define linebreak define pyk of (s x ) as text "(s "! )" end text end define linebreak define pyk of cdots as text "cdots" end text end define linebreak define pyk of object-var as text "object-var" end text end define linebreak define pyk of ex-var as text "ex-var" end text end define linebreak define pyk of ph-var as text "ph-var" end text end define linebreak define pyk of vaerdi as text "vaerdi" end text end define linebreak define pyk of variabel as text "variabel" end text end define linebreak define pyk of op x end op as text "op "! end op" end text end define linebreak define pyk of op2 x comma x end op2 as text "op2 "! comma "! end op2" end text end define linebreak define pyk of define-equal x comma x end equal as text "define-equal "! comma "! end equal" end text end define linebreak define pyk of contains-empty x end empty as text "contains-empty "! end empty" end text end define linebreak define pyk of Nat( x ) as text "Nat( "! )" end text end define linebreak define pyk of 1deduction x conclude x end 1deduction as text "1deduction "! conclude "! end 1deduction" end text end define linebreak define pyk of 1deduction zero x conclude x end 1deduction as text "1deduction zero "! conclude "! end 1deduction" end text end define linebreak define pyk of 1deduction side x conclude x condition x end 1deduction as text "1deduction side "! conclude "! condition "! end 1deduction" end text end define linebreak define pyk of 1deduction one x conclude x condition x end 1deduction as text "1deduction one "! conclude "! condition "! end 1deduction" end text end define linebreak define pyk of 1deduction two x conclude x condition x end 1deduction as text "1deduction two "! conclude "! condition "! end 1deduction" end text end define linebreak define pyk of 1deduction three x conclude x condition x bound x end 1deduction as text "1deduction three "! conclude "! condition "! bound "! end 1deduction" end text end define linebreak define pyk of 1deduction four x conclude x condition x bound x end 1deduction as text "1deduction four "! conclude "! condition "! bound "! end 1deduction" end text end define linebreak define pyk of 1deduction four star x conclude x condition x bound x end 1deduction as text "1deduction four star "! conclude "! condition "! bound "! end 1deduction" end text end define linebreak define pyk of 1deduction five x condition x bound x end 1deduction as text "1deduction five "! condition "! bound "! end 1deduction" end text end define linebreak define pyk of 1deduction six x conclude x exception x bound x end 1deduction as text "1deduction six "! conclude "! exception "! bound "! end 1deduction" end text end define linebreak define pyk of 1deduction six star x conclude x exception x bound x end 1deduction as text "1deduction six star "! conclude "! exception "! bound "! end 1deduction" end text end define linebreak define pyk of 1deduction seven x end 1deduction as text "1deduction seven "! end 1deduction" end text end define linebreak define pyk of 1deduction eight x bound x end 1deduction as text "1deduction eight "! bound "! end 1deduction" end text end define linebreak define pyk of 1deduction eight star x bound x end 1deduction as text "1deduction eight star "! bound "! end 1deduction" end text end define linebreak define pyk of ex1 as text "ex1" end text end define linebreak define pyk of ex2 as text "ex2" end text end define linebreak define pyk of ex3 as text "ex3" end text end define linebreak define pyk of ex10 as text "ex10" end text end define linebreak define pyk of ex20 as text "ex20" end text end define linebreak define pyk of existential var x end var as text "existential var "! end var" end text end define linebreak define pyk of x is existential var as text ""! is existential var" end text end define linebreak define pyk of exist-sub x is x where x is x end sub as text "exist-sub "! is "! where "! is "! end sub" end text end define linebreak define pyk of exist-sub0 x is x where x is x end sub as text "exist-sub0 "! is "! where "! is "! end sub" end text end define linebreak define pyk of exist-sub1 x is x where x is x end sub as text "exist-sub1 "! is "! where "! is "! end sub" end text end define linebreak define pyk of exist-sub* x is x where x is x end sub as text "exist-sub* "! is "! where "! is "! end sub" end text end define linebreak define pyk of ph1 as text "ph1" end text end define linebreak define pyk of ph2 as text "ph2" end text end define linebreak define pyk of ph3 as text "ph3" end text end define linebreak define pyk of placeholder-var x end var as text "placeholder-var "! end var" end text end define linebreak define pyk of x is placeholder-var as text ""! is placeholder-var" end text end define linebreak define pyk of ph-sub x is x where x is x end sub as text "ph-sub "! is "! where "! is "! end sub" end text end define linebreak define pyk of ph-sub0 x is x where x is x end sub as text "ph-sub0 "! is "! where "! is "! end sub" end text end define linebreak define pyk of ph-sub1 x is x where x is x end sub as text "ph-sub1 "! is "! where "! is "! end sub" end text end define linebreak define pyk of ph-sub* x is x where x is x end sub as text "ph-sub* "! is "! where "! is "! end sub" end text end define linebreak define pyk of meta-sub x is x where x is x end sub as text "meta-sub "! is "! where "! is "! end sub" end text end define linebreak define pyk of meta-sub1 x is x where x is x end sub as text "meta-sub1 "! is "! where "! is "! end sub" end text end define linebreak define pyk of meta-sub* x is x where x is x end sub as text "meta-sub* "! is "! where "! is "! end sub" end text end define linebreak define pyk of var big set as text "var big set" end text end define linebreak define pyk of object big set as text "object big set" end text end define linebreak define pyk of meta big set as text "meta big set" end text end define linebreak define pyk of zermelo empty set as text "zermelo empty set" end text end define linebreak define pyk of system Q as text "system Q" end text end define linebreak define pyk of 1rule mp as text "1rule mp" end text end define linebreak define pyk of 1rule gen as text "1rule gen" end text end define linebreak define pyk of 1rule repetition as text "1rule repetition" end text end define linebreak define pyk of 1rule ad absurdum as text "1rule ad absurdum" end text end define linebreak define pyk of 1rule deduction as text "1rule deduction" end text end define linebreak define pyk of 1rule exist intro as text "1rule exist intro" end text end define linebreak define pyk of axiom extensionality as text "axiom extensionality" end text end define linebreak define pyk of axiom empty set as text "axiom empty set" end text end define linebreak define pyk of axiom pair definition as text "axiom pair definition" end text end define linebreak define pyk of axiom union definition as text "axiom union definition" end text end define linebreak define pyk of axiom power definition as text "axiom power definition" end text end define linebreak define pyk of axiom separation definition as text "axiom separation definition" end text end define linebreak define pyk of prop lemma add double neg as text "prop lemma add double neg" end text end define linebreak define pyk of prop lemma remove double neg as text "prop lemma remove double neg" end text end define linebreak define pyk of prop lemma and commutativity as text "prop lemma and commutativity" end text end define linebreak define pyk of prop lemma auto imply as text "prop lemma auto imply" end text end define linebreak define pyk of prop lemma contrapositive as text "prop lemma contrapositive" end text end define linebreak define pyk of prop lemma first conjunct as text "prop lemma first conjunct" end text end define linebreak define pyk of prop lemma second conjunct as text "prop lemma second conjunct" end text end define linebreak define pyk of prop lemma from contradiction as text "prop lemma from contradiction" end text end define linebreak define pyk of prop lemma from disjuncts as text "prop lemma from disjuncts" end text end define linebreak define pyk of prop lemma iff commutativity as text "prop lemma iff commutativity" end text end define linebreak define pyk of prop lemma iff first as text "prop lemma iff first" end text end define linebreak define pyk of prop lemma iff second as text "prop lemma iff second" end text end define linebreak define pyk of prop lemma imply transitivity as text "prop lemma imply transitivity" end text end define linebreak define pyk of prop lemma join conjuncts as text "prop lemma join conjuncts" end text end define linebreak define pyk of prop lemma mp2 as text "prop lemma mp2" end text end define linebreak define pyk of prop lemma mp3 as text "prop lemma mp3" end text end define linebreak define pyk of prop lemma mp4 as text "prop lemma mp4" end text end define linebreak define pyk of prop lemma mp5 as text "prop lemma mp5" end text end define linebreak define pyk of prop lemma mt as text "prop lemma mt" end text end define linebreak define pyk of prop lemma negative mt as text "prop lemma negative mt" end text end define linebreak define pyk of prop lemma technicality as text "prop lemma technicality" end text end define linebreak define pyk of prop lemma weakening as text "prop lemma weakening" end text end define linebreak define pyk of prop lemma weaken or first as text "prop lemma weaken or first" end text end define linebreak define pyk of prop lemma weaken or second as text "prop lemma weaken or second" end text end define linebreak define pyk of lemma formula2pair as text "lemma formula2pair" end text end define linebreak define pyk of lemma pair2formula as text "lemma pair2formula" end text end define linebreak define pyk of lemma formula2union as text "lemma formula2union" end text end define linebreak define pyk of lemma union2formula as text "lemma union2formula" end text end define linebreak define pyk of lemma formula2separation as text "lemma formula2separation" end text end define linebreak define pyk of lemma separation2formula as text "lemma separation2formula" end text end define linebreak define pyk of lemma formula2power as text "lemma formula2power" end text end define linebreak define pyk of lemma subset in power set as text "lemma subset in power set" end text end define linebreak define pyk of lemma power set is subset0 as text "lemma power set is subset0" end text end define linebreak define pyk of lemma power set is subset as text "lemma power set is subset" end text end define linebreak define pyk of lemma power set is subset0-switch as text "lemma power set is subset0-switch" end text end define linebreak define pyk of lemma power set is subset-switch as text "lemma power set is subset-switch" end text end define linebreak define pyk of lemma set equality suff condition as text "lemma set equality suff condition" end text end define linebreak define pyk of lemma set equality suff condition(t)0 as text "lemma set equality suff condition(t)0" end text end define linebreak define pyk of lemma set equality suff condition(t) as text "lemma set equality suff condition(t)" end text end define linebreak define pyk of lemma set equality skip quantifier as text "lemma set equality skip quantifier" end text end define linebreak define pyk of lemma set equality nec condition as text "lemma set equality nec condition" end text end define linebreak define pyk of lemma reflexivity0 as text "lemma reflexivity0" end text end define linebreak define pyk of lemma reflexivity as text "lemma reflexivity" end text end define linebreak define pyk of lemma symmetry0 as text "lemma symmetry0" end text end define linebreak define pyk of lemma symmetry as text "lemma symmetry" end text end define linebreak define pyk of lemma transitivity0 as text "lemma transitivity0" end text end define linebreak define pyk of lemma transitivity as text "lemma transitivity" end text end define linebreak define pyk of lemma er is reflexive as text "lemma er is reflexive" end text end define linebreak define pyk of lemma er is symmetric as text "lemma er is symmetric" end text end define linebreak define pyk of lemma er is transitive as text "lemma er is transitive" end text end define linebreak define pyk of lemma empty set is subset as text "lemma empty set is subset" end text end define linebreak define pyk of lemma member not empty0 as text "lemma member not empty0" end text end define linebreak define pyk of lemma member not empty as text "lemma member not empty" end text end define linebreak define pyk of lemma unique empty set0 as text "lemma unique empty set0" end text end define linebreak define pyk of lemma unique empty set as text "lemma unique empty set" end text end define linebreak define pyk of lemma ==Reflexivity as text "lemma ==Reflexivity" end text end define linebreak define pyk of lemma ==Symmetry as text "lemma ==Symmetry" end text end define linebreak define pyk of lemma ==Transitivity0 as text "lemma ==Transitivity0" end text end define linebreak define pyk of lemma ==Transitivity as text "lemma ==Transitivity" end text end define linebreak define pyk of lemma transfer ~is0 as text "lemma transfer ~is0" end text end define linebreak define pyk of lemma transfer ~is as text "lemma transfer ~is" end text end define linebreak define pyk of lemma pair subset0 as text "lemma pair subset0" end text end define linebreak define pyk of lemma pair subset1 as text "lemma pair subset1" end text end define linebreak define pyk of lemma pair subset as text "lemma pair subset" end text end define linebreak define pyk of lemma same pair as text "lemma same pair" end text end define linebreak define pyk of lemma same singleton as text "lemma same singleton" end text end define linebreak define pyk of lemma union subset as text "lemma union subset" end text end define linebreak define pyk of lemma same union as text "lemma same union" end text end define linebreak define pyk of lemma separation subset as text "lemma separation subset" end text end define linebreak define pyk of lemma same separation as text "lemma same separation" end text end define linebreak define pyk of lemma same binary union as text "lemma same binary union" end text end define linebreak define pyk of lemma intersection subset as text "lemma intersection subset" end text end define linebreak define pyk of lemma same intersection as text "lemma same intersection" end text end define linebreak define pyk of lemma auto member as text "lemma auto member" end text end define linebreak define pyk of lemma eq-system not empty0 as text "lemma eq-system not empty0" end text end define linebreak define pyk of lemma eq-system not empty as text "lemma eq-system not empty" end text end define linebreak define pyk of lemma eq subset0 as text "lemma eq subset0" end text end define linebreak define pyk of lemma eq subset as text "lemma eq subset" end text end define linebreak define pyk of lemma equivalence nec condition0 as text "lemma equivalence nec condition0" end text end define linebreak define pyk of lemma equivalence nec condition as text "lemma equivalence nec condition" end text end define linebreak define pyk of lemma none-equivalence nec condition0 as text "lemma none-equivalence nec condition0" end text end define linebreak define pyk of lemma none-equivalence nec condition1 as text "lemma none-equivalence nec condition1" end text end define linebreak define pyk of lemma none-equivalence nec condition as text "lemma none-equivalence nec condition" end text end define linebreak define pyk of lemma equivalence class is subset as text "lemma equivalence class is subset" end text end define linebreak define pyk of lemma equivalence classes are disjoint as text "lemma equivalence classes are disjoint" end text end define linebreak define pyk of lemma all disjoint as text "lemma all disjoint" end text end define linebreak define pyk of lemma all disjoint-imply as text "lemma all disjoint-imply" end text end define linebreak define pyk of lemma bs subset union(bs/r) as text "lemma bs subset union(bs/r)" end text end define linebreak define pyk of lemma union(bs/r) subset bs as text "lemma union(bs/r) subset bs" end text end define linebreak define pyk of lemma union(bs/r) is bs as text "lemma union(bs/r) is bs" end text end define linebreak define pyk of theorem eq-system is partition as text "theorem eq-system is partition" end text end define linebreak define pyk of var x1 as text "var x1" end text end define linebreak define pyk of var x2 as text "var x2" end text end define linebreak define pyk of var y1 as text "var y1" end text end define linebreak define pyk of var y2 as text "var y2" end text end define linebreak define pyk of var v1 as text "var v1" end text end define linebreak define pyk of var v2 as text "var v2" end text end define linebreak define pyk of var v3 as text "var v3" end text end define linebreak define pyk of var v4 as text "var v4" end text end define linebreak define pyk of var v2n as text "var v2n" end text end define linebreak define pyk of var m1 as text "var m1" end text end define linebreak define pyk of var m2 as text "var m2" end text end define linebreak define pyk of var n1 as text "var n1" end text end define linebreak define pyk of var n2 as text "var n2" end text end define linebreak define pyk of var n3 as text "var n3" end text end define linebreak define pyk of var ep as text "var ep" end text end define linebreak define pyk of var ep1 as text "var ep1" end text end define linebreak define pyk of var ep2 as text "var ep2" end text end define linebreak define pyk of var fep as text "var fep" end text end define linebreak define pyk of var fx as text "var fx" end text end define linebreak define pyk of var fy as text "var fy" end text end define linebreak define pyk of var fz as text "var fz" end text end define linebreak define pyk of var fu as text "var fu" end text end define linebreak define pyk of var fv as text "var fv" end text end define linebreak define pyk of var fw as text "var fw" end text end define linebreak define pyk of var rx as text "var rx" end text end define linebreak define pyk of var ry as text "var ry" end text end define linebreak define pyk of var rz as text "var rz" end text end define linebreak define pyk of var ru as text "var ru" end text end define linebreak define pyk of var sx as text "var sx" end text end define linebreak define pyk of var sx1 as text "var sx1" end text end define linebreak define pyk of var sy as text "var sy" end text end define linebreak define pyk of var sy1 as text "var sy1" end text end define linebreak define pyk of var sz as text "var sz" end text end define linebreak define pyk of var sz1 as text "var sz1" end text end define linebreak define pyk of var su as text "var su" end text end define linebreak define pyk of var su1 as text "var su1" end text end define linebreak define pyk of var fxs as text "var fxs" end text end define linebreak define pyk of var fys as text "var fys" end text end define linebreak define pyk of var crs1 as text "var crs1" end text end define linebreak define pyk of var f1 as text "var f1" end text end define linebreak define pyk of var f2 as text "var f2" end text end define linebreak define pyk of var f3 as text "var f3" end text end define linebreak define pyk of var f4 as text "var f4" end text end define linebreak define pyk of var op1 as text "var op1" end text end define linebreak define pyk of var op2 as text "var op2" end text end define linebreak define pyk of var r1 as text "var r1" end text end define linebreak define pyk of var s1 as text "var s1" end text end define linebreak define pyk of var s2 as text "var s2" end text end define linebreak define pyk of meta x1 as text "meta x1" end text end define linebreak define pyk of meta x2 as text "meta x2" end text end define linebreak define pyk of meta y1 as text "meta y1" end text end define linebreak define pyk of meta y2 as text "meta y2" end text end define linebreak define pyk of meta v1 as text "meta v1" end text end define linebreak define pyk of meta v2 as text "meta v2" end text end define linebreak define pyk of meta v3 as text "meta v3" end text end define linebreak define pyk of meta v4 as text "meta v4" end text end define linebreak define pyk of meta v2n as text "meta v2n" end text end define linebreak define pyk of meta m1 as text "meta m1" end text end define linebreak define pyk of meta m2 as text "meta m2" end text end define linebreak define pyk of meta n1 as text "meta n1" end text end define linebreak define pyk of meta n2 as text "meta n2" end text end define linebreak define pyk of meta n3 as text "meta n3" end text end define linebreak define pyk of meta ep as text "meta ep" end text end define linebreak define pyk of meta ep1 as text "meta ep1" end text end define linebreak define pyk of meta ep2 as text "meta ep2" end text end define linebreak define pyk of meta fx as text "meta fx" end text end define linebreak define pyk of meta fy as text "meta fy" end text end define linebreak define pyk of meta fz as text "meta fz" end text end define linebreak define pyk of meta fu as text "meta fu" end text end define linebreak define pyk of meta fv as text "meta fv" end text end define linebreak define pyk of meta fw as text "meta fw" end text end define linebreak define pyk of meta fep as text "meta fep" end text end define linebreak define pyk of meta rx as text "meta rx" end text end define linebreak define pyk of meta ry as text "meta ry" end text end define linebreak define pyk of meta rz as text "meta rz" end text end define linebreak define pyk of meta ru as text "meta ru" end text end define linebreak define pyk of meta sx as text "meta sx" end text end define linebreak define pyk of meta sx1 as text "meta sx1" end text end define linebreak define pyk of meta sy as text "meta sy" end text end define linebreak define pyk of meta sy1 as text "meta sy1" end text end define linebreak define pyk of meta sz as text "meta sz" end text end define linebreak define pyk of meta sz1 as text "meta sz1" end text end define linebreak define pyk of meta su as text "meta su" end text end define linebreak define pyk of meta su1 as text "meta su1" end text end define linebreak define pyk of meta fxs as text "meta fxs" end text end define linebreak define pyk of meta fys as text "meta fys" end text end define linebreak define pyk of meta f1 as text "meta f1" end text end define linebreak define pyk of meta f2 as text "meta f2" end text end define linebreak define pyk of meta f3 as text "meta f3" end text end define linebreak define pyk of meta f4 as text "meta f4" end text end define linebreak define pyk of meta op1 as text "meta op1" end text end define linebreak define pyk of meta op2 as text "meta op2" end text end define linebreak define pyk of meta r1 as text "meta r1" end text end define linebreak define pyk of meta s1 as text "meta s1" end text end define linebreak define pyk of meta s2 as text "meta s2" end text end define linebreak define pyk of object ep as text "object ep" end text end define linebreak define pyk of object crs1 as text "object crs1" end text end define linebreak define pyk of object f1 as text "object f1" end text end define linebreak define pyk of object f2 as text "object f2" end text end define linebreak define pyk of object f3 as text "object f3" end text end define linebreak define pyk of object f4 as text "object f4" end text end define linebreak define pyk of object n1 as text "object n1" end text end define linebreak define pyk of object n2 as text "object n2" end text end define linebreak define pyk of object op1 as text "object op1" end text end define linebreak define pyk of object op2 as text "object op2" end text end define linebreak define pyk of object r1 as text "object r1" end text end define linebreak define pyk of object s1 as text "object s1" end text end define linebreak define pyk of object s2 as text "object s2" end text end define linebreak define pyk of ph4 as text "ph4" end text end define linebreak define pyk of ph5 as text "ph5" end text end define linebreak define pyk of ph6 as text "ph6" end text end define linebreak define pyk of NAT as text "NAT" end text end define linebreak define pyk of RATIONAL_SERIES as text "RATIONAL_SERIES" end text end define linebreak define pyk of SERIES as text "SERIES" end text end define linebreak define pyk of setOfReals as text "setOfReals" end text end define linebreak define pyk of setOfFxs as text "setOfFxs" end text end define linebreak define pyk of N as text "N" end text end define linebreak define pyk of Q as text "Q" end text end define linebreak define pyk of X as text "X" end text end define linebreak define pyk of xs as text "xs" end text end define linebreak define pyk of xsF as text "xsF" end text end define linebreak define pyk of ysF as text "ysF" end text end define linebreak define pyk of us as text "us" end text end define linebreak define pyk of usF as text "usF" end text end define linebreak define pyk of 0 as text "0" end text end define linebreak define pyk of 1 as text "1" end text end define linebreak define pyk of (-1) as text "(-1)" end text end define linebreak define pyk of 2 as text "2" end text end define linebreak define pyk of 3 as text "3" end text end define linebreak define pyk of 1/2 as text "1/2" end text end define linebreak define pyk of 1/3 as text "1/3" end text end define linebreak define pyk of 2/3 as text "2/3" end text end define linebreak define pyk of 0f as text "0f" end text end define linebreak define pyk of 1f as text "1f" end text end define linebreak define pyk of 00 as text "00" end text end define linebreak define pyk of 01 as text "01" end text end define linebreak define pyk of (--01) as text "(--01)" end text end define linebreak define pyk of 02 as text "02" end text end define linebreak define pyk of 01//02 as text "01//02" end text end define linebreak define pyk of lemma plusAssociativity(R) as text "lemma plusAssociativity(R)" end text end define linebreak define pyk of lemma plusAssociativity(R)XX as text "lemma plusAssociativity(R)XX" end text end define linebreak define pyk of lemma plus0(R) as text "lemma plus0(R)" end text end define linebreak define pyk of lemma negative(R) as text "lemma negative(R)" end text end define linebreak define pyk of lemma times1(R) as text "lemma times1(R)" end text end define linebreak define pyk of lemma lessAddition(R) as text "lemma lessAddition(R)" end text end define linebreak define pyk of lemma plusCommutativity(R) as text "lemma plusCommutativity(R)" end text end define linebreak define pyk of lemma leqAntisymmetry(R) as text "lemma leqAntisymmetry(R)" end text end define linebreak define pyk of lemma leqTransitivity(R) as text "lemma leqTransitivity(R)" end text end define linebreak define pyk of lemma leqAddition(R) as text "lemma leqAddition(R)" end text end define linebreak define pyk of lemma distribution(R) as text "lemma distribution(R)" end text end define linebreak define pyk of axiom a4 as text "axiom a4" end text end define linebreak define pyk of axiom induction as text "axiom induction" end text end define linebreak define pyk of axiom equality as text "axiom equality" end text end define linebreak define pyk of axiom eqLeq as text "axiom eqLeq" end text end define linebreak define pyk of axiom eqAddition as text "axiom eqAddition" end text end define linebreak define pyk of axiom eqMultiplication as text "axiom eqMultiplication" end text end define linebreak define pyk of axiom QisClosed(reciprocal) as text "axiom QisClosed(reciprocal)" end text end define linebreak define pyk of lemma QisClosed(reciprocal) as text "lemma QisClosed(reciprocal)" end text end define linebreak define pyk of axiom QisClosed(negative) as text "axiom QisClosed(negative)" end text end define linebreak define pyk of lemma QisClosed(negative) as text "lemma QisClosed(negative)" end text end define linebreak define pyk of axiom leqReflexivity as text "axiom leqReflexivity" end text end define linebreak define pyk of axiom leqAntisymmetry as text "axiom leqAntisymmetry" end text end define linebreak define pyk of axiom leqTransitivity as text "axiom leqTransitivity" end text end define linebreak define pyk of axiom leqTotality as text "axiom leqTotality" end text end define linebreak define pyk of axiom leqAddition as text "axiom leqAddition" end text end define linebreak define pyk of axiom leqMultiplication as text "axiom leqMultiplication" end text end define linebreak define pyk of axiom plusAssociativity as text "axiom plusAssociativity" end text end define linebreak define pyk of axiom plusCommutativity as text "axiom plusCommutativity" end text end define linebreak define pyk of axiom negative as text "axiom negative" end text end define linebreak define pyk of axiom plus0 as text "axiom plus0" end text end define linebreak define pyk of axiom timesAssociativity as text "axiom timesAssociativity" end text end define linebreak define pyk of axiom timesCommutativity as text "axiom timesCommutativity" end text end define linebreak define pyk of axiom reciprocal as text "axiom reciprocal" end text end define linebreak define pyk of axiom times1 as text "axiom times1" end text end define linebreak define pyk of axiom distribution as text "axiom distribution" end text end define linebreak define pyk of axiom 0not1 as text "axiom 0not1" end text end define linebreak define pyk of lemma eqLeq(R) as text "lemma eqLeq(R)" end text end define linebreak define pyk of lemma timesAssociativity(R) as text "lemma timesAssociativity(R)" end text end define linebreak define pyk of lemma timesCommutativity(R) as text "lemma timesCommutativity(R)" end text end define linebreak define pyk of 1rule adhoc sameR as text "1rule adhoc sameR" end text end define linebreak define pyk of lemma separation2formula(1) as text "lemma separation2formula(1)" end text end define linebreak define pyk of lemma separation2formula(2) as text "lemma separation2formula(2)" end text end define linebreak define pyk of axiom cauchy as text "axiom cauchy" end text end define linebreak define pyk of axiom plusF as text "axiom plusF" end text end define linebreak define pyk of axiom reciprocalF as text "axiom reciprocalF" end text end define linebreak define pyk of 1rule from== as text "1rule from==" end text end define linebreak define pyk of 1rule to== as text "1rule to==" end text end define linebreak define pyk of 1rule fromInR as text "1rule fromInR" end text end define linebreak define pyk of lemma plusR(Sym) as text "lemma plusR(Sym)" end text end define linebreak define pyk of axiom reciprocalR as text "axiom reciprocalR" end text end define linebreak define pyk of 1rule lessMinus1(N) as text "1rule lessMinus1(N)" end text end define linebreak define pyk of axiom nonnegative(N) as text "axiom nonnegative(N)" end text end define linebreak define pyk of axiom US0 as text "axiom US0" end text end define linebreak define pyk of 1rule nextXS(upperBound) as text "1rule nextXS(upperBound)" end text end define linebreak define pyk of 1rule nextXS(noUpperBound) as text "1rule nextXS(noUpperBound)" end text end define linebreak define pyk of 1rule nextUS(upperBound) as text "1rule nextUS(upperBound)" end text end define linebreak define pyk of 1rule nextUS(noUpperBound) as text "1rule nextUS(noUpperBound)" end text end define linebreak define pyk of 1rule expZero as text "1rule expZero" end text end define linebreak define pyk of 1rule expPositive as text "1rule expPositive" end text end define linebreak define pyk of 1rule expZero(R) as text "1rule expZero(R)" end text end define linebreak define pyk of 1rule expPositive(R) as text "1rule expPositive(R)" end text end define linebreak define pyk of 1rule base(1/2)Sum zero as text "1rule base(1/2)Sum zero" end text end define linebreak define pyk of 1rule base(1/2)Sum positive as text "1rule base(1/2)Sum positive" end text end define linebreak define pyk of 1rule UStelescope zero as text "1rule UStelescope zero" end text end define linebreak define pyk of 1rule UStelescope positive as text "1rule UStelescope positive" end text end define linebreak define pyk of 1rule adhoc eqAddition(R) as text "1rule adhoc eqAddition(R)" end text end define linebreak define pyk of 1rule fromLimit as text "1rule fromLimit" end text end define linebreak define pyk of 1rule toUpperBound as text "1rule toUpperBound" end text end define linebreak define pyk of 1rule fromUpperBound as text "1rule fromUpperBound" end text end define linebreak define pyk of axiom USisUpperBound as text "axiom USisUpperBound" end text end define linebreak define pyk of axiom 0not1(R) as text "axiom 0not1(R)" end text end define linebreak define pyk of 1rule expUnbounded as text "1rule expUnbounded" end text end define linebreak define pyk of 1rule fromLeq(Advanced)(N) as text "1rule fromLeq(Advanced)(N)" end text end define linebreak define pyk of 1rule fromLeastUpperBound as text "1rule fromLeastUpperBound" end text end define linebreak define pyk of 1rule toLeastUpperBound as text "1rule toLeastUpperBound" end text end define linebreak define pyk of axiom XSisNotUpperBound as text "axiom XSisNotUpperBound" end text end define linebreak define pyk of axiom ysFGreater as text "axiom ysFGreater" end text end define linebreak define pyk of axiom ysFLess as text "axiom ysFLess" end text end define linebreak define pyk of 1rule smallInverse as text "1rule smallInverse" end text end define linebreak define pyk of axiom natType as text "axiom natType" end text end define linebreak define pyk of axiom rationalType as text "axiom rationalType" end text end define linebreak define pyk of axiom seriesType as text "axiom seriesType" end text end define linebreak define pyk of axiom max as text "axiom max" end text end define linebreak define pyk of axiom numerical as text "axiom numerical" end text end define linebreak define pyk of axiom numericalF as text "axiom numericalF" end text end define linebreak define pyk of axiom memberOfSeries as text "axiom memberOfSeries" end text end define linebreak define pyk of prop lemma doubly conditioned join conjuncts as text "prop lemma doubly conditioned join conjuncts" end text end define linebreak define pyk of prop lemma imply negation as text "prop lemma imply negation" end text end define linebreak define pyk of prop lemma tertium non datur as text "prop lemma tertium non datur" end text end define linebreak define pyk of prop lemma from negated imply as text "prop lemma from negated imply" end text end define linebreak define pyk of prop lemma to negated imply as text "prop lemma to negated imply" end text end define linebreak define pyk of prop lemma from negated double imply as text "prop lemma from negated double imply" end text end define linebreak define pyk of prop lemma from negated and as text "prop lemma from negated and" end text end define linebreak define pyk of prop lemma from negated or as text "prop lemma from negated or" end text end define linebreak define pyk of prop lemma to negated or as text "prop lemma to negated or" end text end define linebreak define pyk of prop lemma from negations as text "prop lemma from negations" end text end define linebreak define pyk of prop lemma from three disjuncts as text "prop lemma from three disjuncts" end text end define linebreak define pyk of prop lemma from two times two disjuncts as text "prop lemma from two times two disjuncts" end text end define linebreak define pyk of prop lemma negate first disjunct as text "prop lemma negate first disjunct" end text end define linebreak define pyk of prop lemma negate second disjunct as text "prop lemma negate second disjunct" end text end define linebreak define pyk of prop lemma expand disjuncts as text "prop lemma expand disjuncts" end text end define linebreak define pyk of lemma set equality nec condition(1) as text "lemma set equality nec condition(1)" end text end define linebreak define pyk of lemma set equality nec condition(2) as text "lemma set equality nec condition(2)" end text end define linebreak define pyk of lemma lessLeq(R) as text "lemma lessLeq(R)" end text end define linebreak define pyk of lemma memberOfSeries as text "lemma memberOfSeries" end text end define linebreak define pyk of lemma memberOfSeries(Type) as text "lemma memberOfSeries(Type)" end text end define linebreak define pyk of x ^ x as text ""! ^ "!" end text end define linebreak define pyk of R( x ) as text "R( "! )" end text end define linebreak define pyk of --R( x ) as text "--R( "! )" end text end define linebreak define pyk of 1/ x as text "1/ "!" end text end define linebreak define pyk of eq-system of x modulo x as text "eq-system of "! modulo "!" end text end define linebreak define pyk of intersection x comma x end intersection as text "intersection "! comma "! end intersection" end text end define linebreak define pyk of [ x ; x ] as text "[ "! ; "! ]" end text end define linebreak define pyk of union x end union as text "union "! end union" end text end define linebreak define pyk of binary-union x comma x end union as text "binary-union "! comma "! end union" end text end define linebreak define pyk of power x end power as text "power "! end power" end text end define linebreak define pyk of zermelo singleton x end singleton as text "zermelo singleton "! end singleton" end text end define linebreak define pyk of stateExpand( x , x , x ) as text "stateExpand( "! , "! , "! )" end text end define linebreak define pyk of extractSeries( x ) as text "extractSeries( "! )" end text end define linebreak define pyk of setOfSeries( x ) as text "setOfSeries( "! )" end text end define linebreak define pyk of --Macro( x ) as text "--Macro( "! )" end text end define linebreak define pyk of expandList( x , x , x ) as text "expandList( "! , "! , "! )" end text end define linebreak define pyk of **Macro( x ) as text "**Macro( "! )" end text end define linebreak define pyk of ++Macro( x ) as text "++Macro( "! )" end text end define linebreak define pyk of < \end{flushleft}

\newpage


\section{\TeX{} definitioner} \label{sec:tex}

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

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

\item " [ math define tex of cdots as text "(\cdots{})" end text end define end math ] "

\item " [ math define tex of object-var as text "\texttt{Objekt-var}" end text end define end math ] "

\item " [ math define tex of ex-var as text "\texttt{Ex-var}" end text end define end math ] "

\item " [ math define tex of ph-var as text "\texttt{Ph-var}" end text end define end math ] "

\item " [ math define tex of vaerdi as text "\texttt{V\ae{}rdi}" end text end define end math ] "

\item " [ math define tex of variabel as text "\texttt{Variabel}" end text end define end math ] "

\item " [ math define tex of op var x end op as text "Op(#1.
)" end text end define end math ] "

\item " [ math define tex of op2 var x comma var y end op2 as text "Op(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of define-equal var x comma var y end equal as text "#1.
\mathrel {\ddot {==}} #2." end text end define end math ] "

\item " [ math define tex of contains-empty var x end empty as text "ContainsEmpty(#1.
)" end text end define end math ] "

\item " [ math define tex of 1deduction var x conclude var y end 1deduction as text "
Dedu(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of 1deduction zero var x conclude var y end 1deduction as text "
Dedu_0(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of 1deduction side var x conclude var y condition var z end 1deduction as text "Dedu_{s}(#1.
,#2.
,#3.
)" end text end define end math ] "

\item " [ math define tex of 1deduction one var x conclude var y condition var z end 1deduction as text "
Dedu_1(#1.
,#2.
,#3.
)" end text end define end math ] "

\item " [ math define tex of 1deduction two var x conclude var y condition var z end 1deduction as text "
Dedu_2(#1.
,#2.
,#3.
)" end text end define end math ] "

\item " [ math define tex of 1deduction three var x conclude var y condition var z bound var u end 1deduction as text "
Dedu_3(#1.
,#2.
,#3.
,#4.
)" end text end define end math ] "

\item " [ math define tex of 1deduction four var x conclude var y condition var z bound var u end 1deduction as text "
Dedu_4(#1.
,#2.
,#3.
,#4.
)" end text end define end math ] "

\item " [ math define tex of 1deduction four star var x conclude var y condition var z bound var u end 1deduction as text "
Dedu_4^*(#1.
,#2.
,#3.
,#4.
)" end text end define end math ] "

\item " [ math define tex of 1deduction five var x condition var y bound var z end 1deduction as text "
Dedu_5(#1.
,#2.
,#3.
)" end text end define end math ] "

\item " [ math define tex of 1deduction six var p conclude var c exception var e bound var b end 1deduction as text "
Dedu_6(#1.
,#2.
,#3.
,#4.
)" end text end define end math ] "

\item " [ math define tex of 1deduction six star var p conclude var c exception var e bound var b end 1deduction as text "
Dedu_6^*(#1.
,#2.
,#3.
,#4.
)" end text end define end math ] "

\item " [ math define tex of 1deduction seven var p end 1deduction as text "
Dedu_7(#1.
)" end text end define end math ] "

\item " [ math define tex of 1deduction eight var p bound var b end 1deduction as text "
Dedu_8(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of 1deduction eight star var p bound var b end 1deduction as text "
Dedu_8^*(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of ex1 as text "Ex_{1}" end text end define end math ] "

\item " [ math define tex of ex2 as text "Ex_{2}" end text end define end math ] "

\item " [ math define tex of ex10 as text "Ex_{10}" end text end define end math ] "

\item " [ math define tex of ex20 as text "Ex_{20}" end text end define end math ] "

\item " [ math define tex of existential var var x end var as text "#1.
_{Ex}" end text end define end math ] "

\item " [ math define tex of var x is existential var as text "#1.
^{Ex}" end text end define end math ] "

\item " [ math define tex of exist-sub var x is var y where var z is var u end sub as text "\langle #1.
{\equiv} #2.
| #3.
{:==} #4.
\rangle_{Ex} " end text end define end math ] "

\item " [ math define tex of exist-sub0 var x is var y where var z is var u end sub as text "\langle #1.
{\equiv}^0 #2.
| #3.
{:==} #4.
\rangle_{Ex} " end text end define end math ] "

\item " [ math define tex of exist-sub1 var x is var y where var z is var u end sub as text "\langle #1.
{\equiv}^1 #2.
| #3.
{:==} #4.
\rangle_{Ex} " end text end define end math ] "

\item " [ math define tex of exist-sub* var x is var y where var z is var u end sub as text "\langle #1.
{\equiv}^* #2.
| #3.
{:==} #4.
\rangle_{Ex} " end text end define end math ] "


\item " [ math define tex of ph1 as text "ph_{1}" end text end define end math ] "

\item " [ math define tex of ph2 as text "ph_{2}" end text end define end math ] "

\item " [ math define tex of ph3 as text "ph_{3}" end text end define end math ] "

\item " [ math define tex of ph4 as text "ph_{4}" end text end define end math ] "

\item " [ math define tex of ph5 as text "ph_{5}" end text end define end math ] "

\item " [ math define tex of ph6 as text "ph_{6}" end text end define end math ] "

\item " [ math define tex of placeholder-var x end var as text "#1.
_{Ph} " end text end define end math ] "

\item " [ math define tex of var x is placeholder-var as text "#1.
^{Ph}" end text end define end math ] "

\item " [ math define tex of ph-sub var x is var y where var z is var u end sub as text "\langle #1.
{\equiv} #2.
| #3.
{:==} #4.
\rangle_{Ph} " end text end define end math ] "

\item " [ math define tex of ph-sub0 var x is var y where var z is var u end sub as text "\langle #1.
{\equiv}^0 #2.
| #3.
{:==} #4.
\rangle_{Ph} " end text end define end math ] "

\item " [ math define tex of ph-sub1 var x is var y where var z is var u end sub as text "\langle #1.
{\equiv}^1 #2.
| #3.
{:==} #4.
\rangle_{Ph} " end text end define end math ] "

\item " [ math define tex of ph-sub* var x is var y where var z is var u end sub as text "\langle #1.
{\equiv}^* #2.
| #3.
{:==} #4.
\rangle_{Ph} " end text end define end math ] "

\item " [ math define tex of var big set as text "\mathsf {bs}" end text end define end math ] "
\item " [ math define tex of object big set as text " \mathsf {OBS}" end text end define end math ] "


\item " [ math define tex of meta big set as text "{\cal BS}" end text end define end math ] "

\item " [ math define tex of zermelo empty set as text "\mathrm{\O}" end text end define end math ] "

\item " [ math define tex of system Q as text "SystemQ" end text end define end math ] "

\item " [ math define tex of 1rule mp as text "MP" end text end define end math ] "
\item " [ math define tex of 1rule gen as text "Gen" end text end define end math ] "
\item " [ math define tex of 1rule repetition as text "Repetition" end text end define end math ] "
\item " [ math define tex of 1rule ad absurdum as text "Neg" end text end define end math ] "
\item " [ math define tex of 1rule deduction as text "Ded" end text end define end math ] "
\item " [ math define tex of 1rule exist intro as text "ExistIntro" end text end define end math ] "



\item " [ math define tex of axiom extensionality as text "Extensionality" end text end define end math ] "
\item " [ math define tex of axiom empty set as text "\O{}def" end text end define end math ] "
\item " [ math define tex of axiom pair definition as text "PairDef" end text end define end math ] "
\item " [ math define tex of axiom union definition as text "UnionDef" end text end define end math ] "
\item " [ math define tex of axiom power definition as text "PowerDef" end text end define end math ] "
\item " [ math define tex of axiom separation definition as text "SeparationDef" end text end define end math ] "
\item " [ math define tex of prop lemma add double neg as text "AddDoubleNeg" end text end define end math ] "
\item " [ math define tex of prop lemma remove double neg as text "RemoveDoubleNeg" end text end define end math ] "
\item " [ math define tex of prop lemma and commutativity as text "AndCommutativity" end text end define end math ] "
\item " [ math define tex of prop lemma auto imply as text "AutoImply" end text end define end math ] "
\item " [ math define tex of prop lemma contrapositive as text "Contrapositive" end text end define end math ] "
\item " [ math define tex of prop lemma first conjunct as text "FirstConjunct" end text end define end math ] "
\item " [ math define tex of prop lemma second conjunct as text "SecondConjunct" end text end define end math ] "
\item " [ math define tex of prop lemma from contradiction as text "FromContradiction" end text end define end math ] "
\item " [ math define tex of prop lemma from disjuncts as text "FromDisjuncts" end text end define end math ] "
\item " [ math define tex of prop lemma iff commutativity as text "IffCommutativity" end text end define end math ] "
\item " [ math define tex of prop lemma iff first as text "IffFirst" end text end define end math ] "

\item " [ math define tex of prop lemma iff second as text "IffSecond" end text end define end math ] "
\item " [ math define tex of prop lemma imply transitivity as text "ImplyTransitivity" end text end define end math ] "



\item " [ math define tex of prop lemma join conjuncts as text "JoinConjuncts" end text end define end math ] "

\item " [ math define tex of prop lemma mp2 as text "MP2" end text end define end math ] "

\item " [ math define tex of prop lemma mp3 as text "MP3" end text end define end math ] "

\item " [ math define tex of prop lemma mp4 as text "MP4" end text end define end math ] "

\item " [ math define tex of prop lemma mp5 as text "MP5" end text end define end math ] "
\item " [ math define tex of prop lemma mt as text "MT" end text end define end math ] "

\item " [ math define tex of prop lemma negative mt as text "NegativeMT" end text end define end math ] "
\item " [ math define tex of prop lemma technicality as text "Technicality" end text end define end math ] "


\item " [ math define tex of prop lemma weakening as text "Weakening" end text end define end math ] "

\item " [ math define tex of prop lemma weaken or first as text "WeakenOr1" end text end define end math ] "

\item " [ math define tex of prop lemma weaken or second as text "WeakenOr2" end text end define end math ] "

\item " [ math define tex of lemma pair2formula as text "Pair2Formula" end text end define end math ] "

\item " [ math define tex of lemma formula2pair as text "Formula2Pair" end text end define end math ] "

\item " [ math define tex of lemma union2formula as text "Union2Formula" end text end define end math ] "

\item " [ math define tex of lemma formula2union as text "Formula2Union" end text end define end math ] "

\item " [ math define tex of lemma formula2power as text "Formula2Power" end text end define end math ] "

\item " [ math define tex of lemma separation2formula as text "Sep2Formula" end text end define end math ] "

\item " [ math define tex of lemma formula2separation as text "Formula2Sep" end text end define end math ] "

\item " [ math define tex of lemma subset in power set as text "SubsetInPower" end text end define end math ] "

\item " [ math define tex of lemma power set is subset0 as text "HelperPowerIsSub" end text end define end math ] "

\item " [ math define tex of lemma power set is subset as text "PowerIsSub" end text end define end math ] "

\item " [ math define tex of lemma power set is subset0-switch as text "(Switch)HelperPowerIsSub" end text end define end math ] "

\item " [ math define tex of lemma power set is subset-switch as text "(Switch)PowerIsSub" end text end define end math ] "

\item " [ math define tex of lemma set equality suff condition as text "ToSetEquality" end text end define end math ] "

\item " [ math define tex of lemma set equality suff condition(t)0 as text "HelperToSetEquality(t)" end text end define end math ] "

\item " [ math define tex of lemma set equality suff condition(t) as text "ToSetEquality(t)" end text end define end math ] "

\item " [ math define tex of lemma set equality skip quantifier as text "HelperFromSetEquality" end text end define end math ] "

\item " [ math define tex of lemma set equality nec condition as text "FromSetEquality" end text end define end math ] "

\item " [ math define tex of lemma reflexivity0 as text "HelperReflexivity" end text end define end math ] "

\item " [ math define tex of lemma reflexivity as text "Reflexivity" end text end define end math ] "

\item " [ math define tex of lemma symmetry0 as text "HelperSymmetry" end text end define end math ] "

\item " [ math define tex of lemma symmetry as text "Symmetry" end text end define end math ] "

\item " [ math define tex of lemma transitivity0 as text "HelperTransitivity" end text end define end math ] "

\item " [ math define tex of lemma transitivity as text "Transitivity" end text end define end math ] ",

\item " [ math define tex of lemma er is reflexive as text "ERisReflexive" end text end define end math ] "


\item " [ math define tex of lemma er is symmetric as text "ERisSymmetric" end text end define end math ] "

\item " [ math define tex of lemma er is transitive as text "ERisTransitive" end text end define end math ] "

\item " [ math define tex of lemma empty set is subset as text "\O{}isSubset" end text end define end math ] "

\item " [ math define tex of lemma member not empty0 as text "HelperMemberNot\O{}" end text end define end math ] "

\item " [ math define tex of lemma member not empty as text "MemberNot\O{}" end text end define end math ] "

\item " [ math define tex of lemma unique empty set0 as text "HelperUnique\O{}" end text end define end math ] "

\item " [ math define tex of lemma unique empty set as text "Unique\O{}" end text end define end math ] "

\item " [ math define tex of lemma ==Reflexivity as text "==\!{}Reflexivity" end text end define end math ] "

\item " [ math define tex of lemma ==Symmetry as text "==\!{}Symmetry" end text end define end math ] "

\item " [ math define tex of lemma ==Transitivity0 as text "Helper\!{}==\!{}Transitivity" end text end define end math ] "

\item " [ math define tex of lemma ==Transitivity as text "\!{}==\!{}Transitivity" end text end define end math ] "

\item " [ math define tex of lemma transfer ~is0 as text "HelperTransferNotEq" end text end define end math ] "

\item " [ math define tex of lemma transfer ~is as text "TransferNotEq" end text end define end math ] "

\item " [ math define tex of lemma pair subset0 as text "HelperPairSubset" end text end define end math ] "

\item " [ math define tex of lemma pair subset1 as text "Helper(2)PairSubset" end text end define end math ] "

\item " [ math define tex of lemma pair subset as text "PairSubset" end text end define end math ] "

\item " [ math define tex of lemma same pair as text "SamePair" end text end define end math ] "

\item " [ math define tex of lemma same singleton as text "SameSingleton" end text end define end math ] "


\item " [ math define tex of lemma union subset as text "UnionSubset" end text end define end math ] "

\item " [ math define tex of lemma same union as text "SameUnion" end text end define end math ] "



\item " [ math define tex of lemma separation subset as text "SeparationSubset" end text end define end math ] "

\item " [ math define tex of lemma same separation as text "SameSeparation" end text end define end math ] "

\item " [ math define tex of lemma same binary union as text "SameBinaryUnion" end text end define end math ] "

\item " [ math define tex of lemma intersection subset as text "IntersectionSubset" end text end define end math ] "

\item " [ math define tex of lemma same intersection as text "SameIntersection" end text end define end math ] "

\item " [ math define tex of lemma auto member as text "AutoMember" end text end define end math ] "

\item " [ math define tex of lemma eq-system not empty0 as text "HelperEqSysNot\O{}" end text end define end math ] "

\item " [ math define tex of lemma eq-system not empty as text "EqSysNot\O{}" end text end define end math ] "

\item " [ math define tex of lemma eq subset0 as text "HelperEqSubset" end text end define end math ] "

\item " [ math define tex of lemma eq subset as text "EqSubset" end text end define end math ] "

\item " [ math define tex of lemma equivalence nec condition as text "EqNecessary" end text end define end math ] "

\item " [ math define tex of lemma equivalence nec condition0 as text "HelperEqNecessary" end text end define end math ] "

\item " [ math define tex of lemma none-equivalence nec condition0 as text "HelperNoneEqNecessary" end text end define end math ] "

\item " [ math define tex of lemma none-equivalence nec condition1 as text "Helper(2)NoneEqNecessary" end text end define end math ] "

\item " [ math define tex of lemma none-equivalence nec condition as text "NoneEqNecessary" end text end define end math ] "

\item " [ math define tex of lemma equivalence class is subset as text "EqClassIsSubset" end text end define end math ] "

\item " [ math define tex of lemma equivalence classes are disjoint as text "EqClassesAreDisjoint" end text end define end math ] "


\item " [ math define tex of lemma all disjoint as text "AllDisjoint" end text end define end math ] "

\item " [ math define tex of lemma all disjoint-imply as text "AllDisjointImply" end text end define end math ] "

\item " [ math define tex of lemma bs subset union(bs/r) as text "BSsubset" end text end define end math ] "

\item " [ math define tex of lemma union(bs/r) subset bs as text "Union(BS/R)subset" end text end define end math ] "

\item " [ math define tex of lemma union(bs/r) is bs as text "UnionIdentity" end text end define end math ] "

\item " [ math define tex of theorem eq-system is partition as text "EqSysIsPartition" end text end define end math ] "

\item " [ math define tex of eq-system of var x modulo var y as text "#1.
/ #2." end text end define end math ] "

\item " [ math define tex of intersection var x comma var y end intersection as text "#1.
\cap #2." end text end define end math ] "

\item " [ math define tex of union var x end union as text "\cup #1." end text end define end math ] "

\item " [ math define tex of binary-union var x comma var y end union as text "#1.
\mathrel{\cup} #2." end text end define end math ] "

\item " [ math define tex of power var x end power as text "P(#1.
)" end text end define end math ] "

\item " [ math define tex of zermelo singleton var x end singleton as text "\{#1.
\}" end text end define end math ] "

\item " [ math define tex of zermelo pair var x comma var y end pair as text "\{#1.
,#2.
\}" end text end define end math ] "

\item " [ math define tex of zermelo ordered pair var x comma var y end pair as text "\langle #1.
,#2.
\rangle" end text end define end math ] ",

\item " [ math define tex of var x in0 var y as text "#1.
\mathrel{\in} #2." end text end define end math ] "

\item " [ math define tex of var x is related to var y under var z as text "#3.
(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of var r is reflexive relation in var x as text "ReflRel(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of var r is symmetric relation in var x as text "SymRel(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of var r is transitive relation in var x as text "TransRel(#1.
,#2.
)" end text end define end math ] "


\item " [ math define tex of var r is equivalence relation in var x as text "EqRel(#1.
,#2.
)" end text end define end math ] "


\item " [ math define tex of equivalence class of var x in var big set modulo var r as text "[#1.
\mathrel{\in} #2.
]_{#3.
}" end text end define end math ] "

\item " [ math define tex of var x is partition of var y as text "Partition(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of var x zermelo is var y as text "#1.
\!\mathrel{==}\! #2." end text end define end math ] "

\item " [ math define tex of var x is subset of var y as text "#1.
\mathrel{\subseteq} #2." end text end define end math ] "

\item " [ math define tex of not0 var x as text "\dot{\neg}\,(#1.
)n" end text end define end math ] "

\item " [ math define tex of var x zermelo ~in var y as text "#1.
\mathrel{\notin} #2." end text end define end math ] "

\item " [ math define tex of var x zermelo ~is var y as text "#1.
\mathrel{\neq} #2." end text end define end math ] "

\item " [ math define tex of var x and0 var y as text "#1.
\mathrel{\dot{\wedge}} #2." end text end define end math ] "

\item " [ math define tex of var x or0 var y as text "#1.
\mathrel{\dot{\vee}} #2." end text end define end math ] "

\item " [ math define tex of var x iff var y as text "#1.
\mathrel{\dot{\Leftrightarrow}} #2." end text end define end math ] "

\item " [ math define tex of the set of ph in var x such that var a end set as text " \{ ph \mathrel{\in} #1.
\mid #2.
\}" end text end define end math ] "







\item " [ math define tex of var x imply var y as text "(i#1.
\Rightarrow #2.
)i" end text end define end math ] "

\item " [ math define tex of Nat( var x ) as text "Nat(#1.
)" end text end define end math ] "

\item " [ math define tex of meta-sub var x is var y where var z is var u end sub as text "\langle #1.
{\equiv} #2.
| #3.
{:==} #4.
\rangle_{Me}" end text end define end math ] "

\item " [ math define tex of meta-sub1 var x is var y where var z is var u end sub as text "\langle #1.
{\equiv}^1 #2.
| #3.
{:==} #4.
\rangle_{Me} " end text end define end math ] "

\item " [ math define tex of meta-sub* var x is var y where var z is var u end sub as text "\langle #1.
{\equiv}^* #2.
| #3.
{:==} #4.
\rangle_{Me} " end text end define end math ] "

\item " [ math define tex of exist0 var x indeed var y as text "
\exists #1.
\colon #2." end text end define end math ] "

\item " [ math define tex of var x1 as text "(x1)" end text end define end math ] "

\item " [ math define tex of var x2 as text "(x2)" end text end define end math ] "

\item " [ math define tex of var y1 as text "(y1)" end text end define end math ] "

\item " [ math define tex of var y2 as text "(y2)" end text end define end math ] "

\item " [ math define tex of var v1 as text "(v1)" end text end define end math ] "

\item " [ math define tex of var v2 as text "(v2)" end text end define end math ] "

\item " [ math define tex of var v3 as text "(v3)" end text end define end math ] "

\item " [ math define tex of var v4 as text "(v4)" end text end define end math ] "

\item " [ math define tex of var v2n as text "(v2n)" end text end define end math ] "

\item " [ math define tex of var n1 as text "(n1)" end text end define end math ] "

\item " [ math define tex of var n2 as text "(n2)" end text end define end math ] "

\item " [ math define tex of var n3 as text "(n3)" end text end define end math ] "

\item " [ math define tex of var m1 as text "(m1)" end text end define end math ] "

\item " [ math define tex of var m2 as text "(m2)" end text end define end math ] "

\item " [ math define tex of var ep as text "(\epsilon)" end text end define end math ] "

\item " [ math define tex of var ep1 as text "(\epsilon)_{1}" end text end define end math ] "

\item " [ math define tex of var ep2 as text "(\epsilon 2)" end text end define end math ] "

\item " [ math define tex of var fx as text "(fx)" end text end define end math ] "

\item " [ math define tex of var fy as text "(fy)" end text end define end math ] "

\item " [ math define tex of var fz as text "(fz)" end text end define end math ] "

\item " [ math define tex of var fu as text "(fu)" end text end define end math ] "

\item " [ math define tex of var fv as text "(fv)" end text end define end math ] "

\item " [ math define tex of var fw as text "(fw)" end text end define end math ] "

\item " [ math define tex of var fep as text "(fep)" end text end define end math ] "

\item " [ math define tex of var rx as text "(rx)" end text end define end math ] "

\item " [ math define tex of var ry as text "(ry)" end text end define end math ] "

\item " [ math define tex of var rz as text "(rz)" end text end define end math ] "

\item " [ math define tex of var ru as text "(ru)" end text end define end math ] "

\item " [ math define tex of var sx as text "(sx)" end text end define end math ] "

\item " [ math define tex of var sx1 as text "(sx1)" end text end define end math ] "

\item " [ math define tex of var sy as text "(sy)" end text end define end math ] "

\item " [ math define tex of var sy1 as text "(sy1)" end text end define end math ] "

\item " [ math define tex of var sz as text "(sz)" end text end define end math ] "

\item " [ math define tex of var sz1 as text "(sz1)" end text end define end math ] "

\item " [ math define tex of var su as text "(su)" end text end define end math ] "

\item " [ math define tex of var su1 as text "(su1)" end text end define end math ] "

\item " [ math define tex of var fxs as text "(fxs)" end text end define end math ] "

\item " [ math define tex of var fys as text "(fys)" end text end define end math ] "

\item " [ math define tex of var crs1 as text "(crs1)" end text end define end math ] "

\item " [ math define tex of var f1 as text "(f1)" end text end define end math ] "

\item " [ math define tex of var f2 as text "(f2)" end text end define end math ] "

\item " [ math define tex of var f3 as text "(f3)" end text end define end math ] "

\item " [ math define tex of var f4 as text "(f4)" end text end define end math ] "

\item " [ math define tex of var op1 as text "(op1)" end text end define end math ] "

\item " [ math define tex of var op2 as text "(op2)" end text end define end math ] "

\item " [ math define tex of var r1 as text "(r1)" end text end define end math ] "

\item " [ math define tex of var s1 as text "(s1)" end text end define end math ] "

\item " [ math define tex of var s2 as text "(s2)" end text end define end math ] "

\item " [ math define tex of meta x1 as text "X_{1}" end text end define end math ] "

\item " [ math define tex of meta x2 as text "X_{2}" end text end define end math ] "

\item " [ math define tex of meta y1 as text "Y_{1}" end text end define end math ] "

\item " [ math define tex of meta y2 as text "Y_{2}" end text end define end math ] "

\item " [ math define tex of meta v1 as text "V_{1}" end text end define end math ] "

\item " [ math define tex of meta v2 as text "V_{2}" end text end define end math ] "

\item " [ math define tex of meta v3 as text "V_{3}" end text end define end math ] "

\item " [ math define tex of meta v4 as text "V_{4}" end text end define end math ] "

\item " [ math define tex of meta v2n as text "V_{2n}" end text end define end math ] "

\item " [ math define tex of meta ep as text "\epsilon" end text end define end math ] "

\item " [ math define tex of meta m1 as text "M_{1}" end text end define end math ] "

\item " [ math define tex of meta m2 as text "M_{2}" end text end define end math ] "

\item " [ math define tex of meta n1 as text "N_{1} " end text end define end math ] "

\item " [ math define tex of meta n2 as text "N_{2} " end text end define end math ] "

\item " [ math define tex of meta n3 as text "N_{3} " end text end define end math ] "

\item " [ math define tex of meta ep1 as text "\epsilon 1" end text end define end math ] "

\item " [ math define tex of meta ep2 as text "\epsilon 2" end text end define end math ] "

\item " [ math define tex of meta fx as text "FX" end text end define end math ] "

\item " [ math define tex of meta fy as text "FY" end text end define end math ] "

\item " [ math define tex of meta fz as text "FZ" end text end define end math ] "

\item " [ math define tex of meta fu as text "FU" end text end define end math ] "

\item " [ math define tex of meta fv as text "FV" end text end define end math ] "

\item " [ math define tex of meta fw as text "FW" end text end define end math ] "

\item " [ math define tex of meta fep as text "FEP" end text end define end math ] "

\item " [ math define tex of meta rx as text "RX" end text end define end math ] "

\item " [ math define tex of meta ry as text "RY" end text end define end math ] "

\item " [ math define tex of meta rz as text "RZ" end text end define end math ] "

\item " [ math define tex of meta ru as text "RU" end text end define end math ] "

\item " [ math define tex of meta sx as text "(SX)" end text end define end math ] "

\item " [ math define tex of meta sx1 as text "(SX1)" end text end define end math ] "

\item " [ math define tex of meta sy as text "(SY)" end text end define end math ] "

\item " [ math define tex of meta sy1 as text "(SY1)" end text end define end math ] "

\item " [ math define tex of meta sz as text "(SZ)" end text end define end math ] "

\item " [ math define tex of meta sz1 as text "(SZ1)" end text end define end math ] "

\item " [ math define tex of meta su as text "(SU)" end text end define end math ] "

\item " [ math define tex of meta su1 as text "(SU1)" end text end define end math ] "

\item " [ math define tex of meta fxs as text "FXS" end text end define end math ] "

\item " [ math define tex of meta fys as text "FYS" end text end define end math ] "

\item " [ math define tex of meta f1 as text "(F1)" end text end define end math ] "

\item " [ math define tex of meta f2 as text "(F2)" end text end define end math ] "

\item " [ math define tex of meta f3 as text "(F3)" end text end define end math ] "

\item " [ math define tex of meta f4 as text "(F4)" end text end define end math ] "

\item " [ math define tex of meta op1 as text "(OP1)" end text end define end math ] "

\item " [ math define tex of meta op2 as text "(OP2)" end text end define end math ] "

\item " [ math define tex of meta r1 as text "(R1)" end text end define end math ] "

\item " [ math define tex of meta s1 as text "(S1)" end text end define end math ] "

\item " [ math define tex of meta s2 as text "(S2)" end text end define end math ] "

\item " [ math define tex of object ep as text "(EPob)" end text end define end math ] "

\item " [ math define tex of object crs1 as text "(CRS1ob)" end text end define end math ] "

\item " [ math define tex of object f1 as text "(F1ob)" end text end define end math ] "

\item " [ math define tex of object f2 as text "(F2ob)" end text end define end math ] "

\item " [ math define tex of object f3 as text "(F3ob)" end text end define end math ] "

\item " [ math define tex of object f4 as text "(F4ob)" end text end define end math ] "

\item " [ math define tex of object n1 as text "(N1ob)" end text end define end math ] "

\item " [ math define tex of object n2 as text "(N2ob)" end text end define end math ] "

\item " [ math define tex of object op1 as text "(OP1ob)" end text end define end math ] "

\item " [ math define tex of object op2 as text "(OP2ob)" end text end define end math ] "

\item " [ math define tex of object r1 as text "(R1ob)" end text end define end math ] "

\item " [ math define tex of object s1 as text "(S1ob)" end text end define end math ] "

\item " [ math define tex of object s2 as text "(S2ob)" end text end define end math ] "






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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\item " [ math define tex of (-1) as text "(-1)" end text end define end math ] "

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

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

\item " [ math define tex of 1/2 as text "1/2" end text end define end math ] "

\item " [ math define tex of 1/3 as text "1/3" end text end define end math ] "

\item " [ math define tex of 2/3 as text "2/3" end text end define end math ] "

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

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

\item " [ math define tex of (--01) as text "(--01)" end text end define end math ] "

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

\item " [ math define tex of 01//02 as text "01//02" end text end define end math ] "

\item " [ math define tex of var x = var y as text "#1.
= #2." end text end define end math ] "

\item " [ math define tex of var x != var y as text "#1.
\neq #2." end text end define end math ] "

\item " [ math define tex of var x < var y as text "#1.
< #2." end text end define end math ] "

\item " [ math define tex of var x <= var y as text "#1.
<= #2." end text end define end math ] "

\item " [ math define tex of var x <_{f}#2." end text end define end math ] "

\item " [ math define tex of var x <=f var y as text "#1.
\leq_{f}#2." end text end define end math ] "

\item " [ math define tex of var x sameF var y as text "SF(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of var x == var y as text "#1.
== #2." end text end define end math ] "

\item " [ math define tex of var x !!== var y as text "#1.
!!== #2." end text end define end math ] "

\item " [ math define tex of var x << var y as text "#1.
<< #2." end text end define end math ] "

\item " [ math define tex of var x <<== var y as text "#1.
<<== #2." end text end define end math ] "

\item " [ math define tex of [ var x ; var y ] as text "#1.
[#2.
]" end text end define end math ] "

\item " [ math define tex of - var x as text "(-u#1.
)" end text end define end math ] "

\item " [ math define tex of -f var x as text "-_{f}#1." end text end define end math ] "

\item " [ math define tex of -- var x as text "(--#1.
)" end text end define end math ] "

\item " [ math define tex of 1f/ var x as text "1f/#1." end text end define end math ] "

\item " [ math define tex of 01// var x as text "01//temp#1." end text end define end math ] "

\item " [ math define tex of var x + var y as text "(#1.
+#2.
)" end text end define end math ] "

\item " [ math define tex of var x - var y as text "(#1.
-#2.
)" end text end define end math ] "

\item " [ math define tex of var fx +f var fy as text "#1.
+_{f}#2." end text end define end math ] "

\item " [ math define tex of var fx -f var fy as text "#1.
-_{f}#2." end text end define end math ] "

\item " [ math define tex of var fx *f var fy as text "#1.
*_{f}#2." end text end define end math ] "

\item " [ math define tex of var x ++ var y as text "#1.
++#2." end text end define end math ] "

\item " [ math define tex of R( var fx ) -- R( var fy ) as text "R(#1.
) -- R(#2.
)" end text end define end math ] "

\item " [ math define tex of var x * var y as text "(#1.
*#2.
)" end text end define end math ] "

\item " [ math define tex of var x ** var y as text "#1.
**#2." end text end define end math ] "

\item " [ math define tex of var x ^ var y as text " #1.
(exp) #2." end text end define end math ] "

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

\item " [ math define tex of 1/ var x as text "rec#1." end text end define end math ] "

\item " [ math define tex of | var x | as text "|#1.
|" end text end define end math ] "

\item " [ math define tex of stateExpand( var t , var s , var c ) as text "StateExpand(#1.
,#2.
,#3.
)" end text end define end math ] "

\item " [ math define tex of extractSeries( var t ) as text "extractSeries(#1.
)" end text end define end math ] "

\item " [ math define tex of |f var x | as text "|f#1.
|" end text end define end math ] "

\item " [ math define tex of |r var x | as text "|r#1.
|" end text end define end math ] "

\item " [ math define tex of setOfSeries( var x ) as text "SetOfSeries(#1.
)" end text end define end math ] "

\item " [ math define tex of expandList( var x , var y , var z ) as text "ExpandList(#1.
,#2.
,#3.
)" end text end define end math ] "

\item " [ math define tex of **Macro( var x ) as text "**Macro(#1.
)" end text end define end math ] "

\item " [ math define tex of ++Macro( var x ) as text "++Macro(#1.
)" end text end define end math ] "

\item " [ math define tex of --Macro( var x ) as text "--Macro(#1.
)" end text end define end math ] "

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

\item " [ math define tex of ||Macro( var x ) as text "||Macro(#1.
)" end text end define end math ] "

\item " [ math define tex of 01//Macro( var x ) as text "01//Macro(#1.
)" end text end define end math ] "



\item " [ math define tex of max( var x , var y ) as text "Max(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of maxR( var x , var y ) as text "Max(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of limit( var x , var y ) as text "Limit(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of U( var x ) as text "Union(#1.
)" end text end define end math ] "

\item " [ math define tex of if( var x , var y , var z ) as text "if(#1.
,#2.
,#3.
)" end text end define end math ] "

\item " [ math define tex of isOrderedPair( var x , var y , var z ) as text "IsOrderedPair(#1.
,#2.
,#3.
)" end text end define end math ] "

\item " [ math define tex of isRelation( var x , var y , var z ) as text "IsRelation(#1.
,#2.
,#3.
)" end text end define end math ] "

\item " [ math define tex of isFunction( var x , var y , var z ) as text "isFunction(#1.
,#2.
,#3.
)" end text end define end math ] "

\item " [ math define tex of typeNat( var x ) as text "TypeNat(#1.
)" end text end define end math ] "

\item " [ math define tex of typeNat0( var x ) as text "TypeNat0(#1.
)" end text end define end math ] "

\item " [ math define tex of typeRational( var x ) as text "TypeRational(#1.
)" end text end define end math ] "

\item " [ math define tex of typeRational0( var x ) as text "TypeRational0(#1.
)" end text end define end math ] "

\item " [ math define tex of typeSeries( var x , var y ) as text "TypeSeries(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of typeSeries0( var x , var y ) as text "Typeseries0(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of upperBound( var x , var y ) as text "UB(#1.
, #2.
)" end text end define end math ] "

\item " [ math define tex of leastUpperBound( var x , var y ) as text "LUB(#1.
, #2.
)" end text end define end math ] "

\item " [ math define tex of base(1/2)Sum( var x , var y ) as text "BS(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of UStelescope( var x , var y ) as text "UStelescope(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of ( var x ) as text "(#1.
)" end text end define end math ] "

\item " [ math define tex of R( var x ) as text "R(#1.
)" end text end define end math ] "

\item " [ math define tex of --R( var x ) as text "--R(#1.
)" end text end define end math ] "

\item " [ math define tex of isSeries( var x , var y ) as text "IsSeries(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of isNatural( var x , var y ) as text "IsNatural(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of (o var x , var y ) as text "OrderedPair(#1.
,#2.
)" end text end define end math ] "


\item " [ math define tex of axiom leqAntisymmetry as text "leqAntisymmetryAxiom" end text end define end math ] "

\item " [ math define tex of axiom leqTransitivity as text "leqTransitivityAxiom" end text end define end math ] "

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

\item " [ math define tex of axiom leqAddition as text "leqAdditionAxiom" end text end define end math ] "

\item " [ math define tex of axiom leqMultiplication as text "leqMultiplicationAxiom" end text end define end math ] "

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

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

\item " [ math define tex of axiom negative as text "Negative" end text end define end math ] "

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

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

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

\item " [ math define tex of axiom reciprocal as text "ReciprocalAxiom" end text end define end math ] "

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

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

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

\item " [ math define tex of axiom negative as text "Negative" end text end define end math ] "

\item " [ math define tex of axiom distribution as text "Distribution" end text end define end math ] "

\item " [ math define tex of axiom 0not1 as text "0not1" end text end define end math ] "

\item " [ math define tex of axiom a4 as text "A4(Axiom)" end text end define end math ] "

\item " [ math define tex of axiom induction as text "InductionAxiom" end text end define end math ] "

\item " [ math define tex of axiom equality as text "EqualityAxiom" end text end define end math ] "

\item " [ math define tex of axiom eqLeq as text "EqLeqAxiom" end text end define end math ] "

\item " [ math define tex of axiom eqAddition as text "EqAdditionAxiom" end text end define end math ] "

\item " [ math define tex of axiom eqMultiplication as text "EqMultiplicationAxiom" end text end define end math ] "

\item " [ math define tex of lemma set equality nec condition(1) as text "SENC1" end text end define end math ] "

\item " [ math define tex of lemma set equality nec condition(2) as text "SENC2" end text end define end math ] "

\item " [ math define tex of axiom cauchy as text "Cauchy" end text end define end math ] "

\item " [ math define tex of axiom plusF as text "PlusF" end text end define end math ] "

\item " [ math define tex of axiom reciprocalF as text "ReciprocalF" end text end define end math ] "

\item " [ math define tex of 1rule from== as text "From==" end text end define end math ] "

\item " [ math define tex of 1rule to== as text "To==" end text end define end math ] "


\item " [ math define tex of 1rule fromInR as text "FromInR" end text end define end math ] "

\item " [ math define tex of axiom reciprocalR as text "ReciprocalR(Axiom)" end text end define end math ] "

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

\item " [ math define tex of 1rule nextXS(upperBound) as text "NextXS(UpperBound)" end text end define end math ] "

\item " [ math define tex of 1rule nextXS(noUpperBound) as text "NextXS(NoUpperBound)" end text end define end math ] "

\item " [ math define tex of 1rule nextUS(upperBound) as text "NextUS(UpperBound)" end text end define end math ] "

\item " [ math define tex of 1rule nextUS(noUpperBound) as text "NextUS(NoUpperBound)" end text end define end math ] "

\item " [ math define tex of 1rule expZero as text "ExpZero" end text end define end math ] "

\item " [ math define tex of 1rule expPositive as text "ExpPositive" end text end define end math ] "

\item " [ math define tex of 1rule expZero(R) as text "ExpZero(R)" end text end define end math ] "

\item " [ math define tex of 1rule expPositive(R) as text "ExpPositive(R)" end text end define end math ] "

\item " [ math define tex of 1rule lessMinus1(N) as text "LessMinus1(N)" end text end define end math ] "

\item " [ math define tex of axiom nonnegative(N) as text "Nonnegative(N)" end text end define end math ] "

\item " [ math define tex of 1rule base(1/2)Sum zero as text "BSzero" end text end define end math ] "

\item " [ math define tex of 1rule base(1/2)Sum positive as text "BSpositive" end text end define end math ] "

\item " [ math define tex of 1rule UStelescope zero as text "UStelescope(Zero)" end text end define end math ] "

\item " [ math define tex of 1rule UStelescope positive as text "UStelescope(Positive)" end text end define end math ] "

\item " [ math define tex of 1rule adhoc eqAddition(R) as text "EqAddition(R)" end text end define end math ] "

\item " [ math define tex of 1rule fromLimit as text "FromLimit" end text end define end math ] "

\item " [ math define tex of 1rule toUpperBound as text "ToUpperBound" end text end define end math ] "

\item " [ math define tex of 1rule fromUpperBound as text "FromUpperBound" end text end define end math ] "

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

\item " [ math define tex of axiom 0not1(R) as text "0not1(R)" end text end define end math ] "

\item " [ math define tex of 1rule expUnbounded as text "ExpUnbounded(R)" end text end define end math ] "

\item " [ math define tex of 1rule fromLeq(Advanced)(N) as text "FromLeq(Advanced)(N)" end text end define end math ] "

\item " [ math define tex of 1rule fromLeastUpperBound as text "FromLeastUpperBound" end text end define end math ] "

\item " [ math define tex of 1rule toLeastUpperBound as text "ToLeastUpperBound" end text end define end math ] "

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

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

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

\item " [ math define tex of 1rule smallInverse as text "SmallInverse" end text end define end math ] "

\item " [ math define tex of axiom memberOfSeries as text "MemberOfSeries(Imply)" end text end define end math ] "

\item " [ math define tex of axiom natType as text "NatType" end text end define end math ] "

\item " [ math define tex of axiom rationalType as text "RationalType" end text end define end math ] "

\item " [ math define tex of axiom seriesType as text "SeriesType" end text end define end math ] "


\item " [ math define tex of prop lemma doubly conditioned join conjuncts as text "JoinConjuncts(2conditions)" end text end define end math ] "

\item " [ math define tex of prop lemma tertium non datur as text "TND" end text end define end math ] "

\item " [ math define tex of prop lemma from negated imply as text "FromNegatedImply" end text end define end math ] "

\item " [ math define tex of prop lemma to negated imply as text "ToNegatedImply" end text end define end math ] "

\item " [ math define tex of prop lemma from negated double imply as text "FromNegated(2*Imply)" end text end define end math ] "

\item " [ math define tex of prop lemma from negated and as text "FromNegatedAnd" end text end define end math ] "

\item " [ math define tex of prop lemma from negated or as text "FromNegatedOr" end text end define end math ] "

\item " [ math define tex of prop lemma to negated or as text "ToNegatedOr" end text end define end math ] "

\item " [ math define tex of prop lemma from negations as text "FromNegations" end text end define end math ] "

\item " [ math define tex of prop lemma from three disjuncts as text "From3Disjuncts" end text end define end math ] "

\item " [ math define tex of prop lemma negate first disjunct as text "NegateDisjunct1" end text end define end math ] "

\item " [ math define tex of prop lemma negate second disjunct as text "NegateDisjunct2" end text end define end math ] "

\item " [ math define tex of prop lemma expand disjuncts as text "ExpandDisjuncts" end text end define end math ] "

\item " [ math define tex of prop lemma from two times two disjuncts as text "From2*2Disjuncts" end text end define end math ] "







\item " [ math define tex of lemma plusR(Sym) as text "PlusR(Sym)" end text end define end math ] "

\item " [ math define tex of lemma lessLeq(R) as text "LessLeq(R)" end text end define end math ] "


\item " [ math define tex of lemma leqAntisymmetry(R) as text "LeqAntisymmetry(R)" end text end define end math ] "

\item " [ math define tex of lemma leqTransitivity(R) as text "LeqTransitivity(R)" end text end define end math ] "

\item " [ math define tex of lemma plus0(R) as text "Plus0(R)" end text end define end math ] "


\item " [ math define tex of lemma lessAddition(R) as text "lessAddition(R)" end text end define end math ] "




\item " [ math define tex of lemma leqAddition(R) as text "leqAddition(R)" end text end define end math ] "

\item " [ math define tex of lemma plusAssociativity(R)XX as text "PlusAssociativity(R)XX" end text end define end math ] "

\item " [ math define tex of lemma plusAssociativity(R) as text "PlusAssociativity(R)" end text end define end math ] "

\item " [ math define tex of lemma negative(R) as text "Negative(R)" end text end define end math ] "

\item " [ math define tex of lemma plusCommutativity(R) as text "PlusCommutativity(R)" end text end define end math ] "



\item " [ math define tex of lemma times1(R) as text "Times1(R)" end text end define end math ] "

\item " [ math define tex of lemma timesAssociativity(R) as text "TimesAssociativity(R)" end text end define end math ] "




\item " [ math define tex of lemma timesCommutativity(R) as text "TimesCommutativity(R)" end text end define end math ] "

\item " [ math define tex of lemma distribution(R) as text "Distribution(R)" end text end define end math ] "

\item " [ math define tex of exist var x indeed var y as text "(AARRGGHH!-exist-bug!)" end text end define end math ] "

\item " [ math define tex of constantRationalSeries( var x ) as text "constantRationalSeries(#1.
)" end text end define end math ] "

\item " [ math define tex of P( var x ) as text "Power(#1.
)" end text end define end math ] "

\item " [ math define tex of cartProd( var x , var y ) as text "cartProd(#1.
)" end text end define end math ] "

\item " [ math define tex of binaryUnion( var x , var y ) as text "binaryUnion(#1.
,#2.
)" end text end define end math ] "

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

\item " [ math define tex of lemma memberOfSeries as text "MemberOfSeries" end text end define end math ] "

\item " [ math define tex of isSubset( var x , var y ) as text "IsSubset(#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of lemma memberOfSeries(Type) as text "memberOfSeries(Type)" end text end define end math ] "

\item " [ math define tex of lemma uniqueMember as text "UniqueMember" end text end define end math ] "

\item " [ math define tex of lemma uniqueMember(Type) as text "UniqueMember(Type)" end text end define end math ] "

\item " [ math define tex of lemma sameSeries as text "SameSeries" end text end define end math ] "

\item " [ math define tex of lemma a4 as text "A4" end text end define end math ] "

\item " [ math define tex of (s var x ) as text "(s#1.
)" end text end define end math ] "

\item " [ math define tex of (p var x , var y ) as text "(p#1.
,#2.
)" end text end define end math ] "

\item " [ math define tex of lemma sameMember as text "SameMember" end text end define end math ] "

\item " [ math define tex of 1rule Qclosed(Addition) as text "Qclosed(Addition)" end text end define end math ] "

\item " [ math define tex of 1rule Qclosed(Multiplication) as text "Qclosed(Multiplication)" end text end define end math ] "

\item " [ math define tex of 1rule fromCartProd(1) as text "FromCartProd(1)" end text end define end math ] "

\item " [ math define tex of 1rule fromCartProd(1) as text "FromCartProd(1)" end text end define end math ] "


\item " [ math define tex of axiom max as text "Max" end text end define end math ] "

\item " [ math define tex of axiom numerical as text "Numerical" end text end define end math ] "

\item " [ math define tex of axiom numericalF as text "NumericalF" end text end define end math ] "

\item " [ math define tex of lemma separation2formula(1) as text "Separation2formula(1)" end text end define end math ] "

\item " [ math define tex of lemma separation2formula(2) as text "Separation2formula(2)" end text end define end math ] "

\item " [ math define tex of axiom QisClosed(reciprocal) as text "QisClosed(Reciprocal)(Imply)" end text end define end math ] "

\item " [ math define tex of lemma QisClosed(reciprocal) as text "QisClosed(Reciprocal)" end text end define end math ] "

\item " [ math define tex of axiom QisClosed(negative) as text "QisClosed(Negative)(Imply)" end text end define end math ] "

\item " [ math define tex of lemma QisClosed(negative) as text "QisClosed(Negative)" end text end define end math ] "

\item " [ math define tex of 1rule adhoc sameR as text "(Adgic)SameR" end text end define end math ] "

\end{list}


\end{document}

End of file
latex page
latex page
dvipdfm page"