"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 expansion ] "
(*** MAKROER BEGYNDER ***)
" [ math macro define ph1 as placeholder-var var a end var end define end math ] "
" [ math macro define ph2 as placeholder-var var b end var end define end math ] "
" [ math macro define ph3 as placeholder-var var c end var end define end math ] "
" [ math macro define ph4 as placeholder-var var d end var end define end math ] "
" [ math macro define ph5 as placeholder-var var e end var end define end math ] "
" [ math macro define ph6 as placeholder-var var f end var end define end math ] "
" [ math macro define var x and0 var y as not0 parenthesis var x imply not0 var y end parenthesis end define end math ] "
" [ math macro define var x or0 var y as not0 var x imply var y end define end math ] "
" [ math 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 math ] "
" [ math macro define var x zermelo ~is var y as not0 var x zermelo is var y end define end math ] "
" [ math macro define var x zermelo ~in var y as not0 var x in0 var y end define end math ] "
" [ math 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 math ] "
" [ math macro define zermelo singleton var x end singleton as zermelo pair var x comma var x end pair end define end math ] "
" [ math 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 math ] "
" [ math 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 math ] "
" [ math 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 math ] "
" [ math 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 math ] "
" [ math 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 math ] "
" [ math 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 math ] "
" [ math 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 math ] "
\display{" [ math 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 math ] "}
" [ math macro define meta big set as metavar var big set end metavar end define end math ] "
" [ math macro define object big set as object var var big set end var end define end math ] "
\display{
" [ math 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 math ] "
}
\display{
" [ math 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 math ] "
}
\display{
" [ math 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 math ] "
}
(*** EKSISTENS-VARIABLE ***)
\display{" [ math value define 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 macro define ex1 as existential var var a end var end define end math ] "
}
" [ math macro define ex2 as existential var var b end var end define end math ] "
" [ math macro define ex10 as existential var var j end var end define end math ] "
" [ math macro define ex20 as existential var var t end var end define end math ] "
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math 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 math ] "
\item " [ math value define 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 value define 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 open if var b term root equal quote for all var u indeed var v end quote then false else newline open if var b is existential var and var b term equal var x then var a term equal var t else newline var a term root equal var b macro and exist-sub* var a tail is var b tail where var x is var t end sub end define end math ] "
\item " [ math value define 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 exist-sub1 var a head is var b head where var x is var t end sub macro and exist-sub* var a tail is var b tail where var x is var t end sub end if end define end math ] "
\end{list}
(*** AKSIOMATISK SYSTEM ***)
" [ math theory system Q end theory end math ] "
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math in theory system Q rule 1rule mp says for all terms meta a comma meta b indeed meta a imply meta b infer meta a infer meta b end rule end math ] "
\item " [ math in theory system Q rule 1rule gen says for all terms meta x comma meta a indeed meta a infer for all meta x indeed meta a end rule end math ] "
\item " [ math in theory system Q rule 1rule repetition says for all terms meta a indeed meta a infer meta a end rule end math ] "
\item " [ math in theory system Q rule 1rule ad absurdum says for all terms meta a comma meta b indeed not0 meta b imply meta a infer not0 meta b imply not0 meta a infer meta b end rule end math ] "
\item " [ math in theory system Q rule 1rule deduction says for all terms meta a comma meta b indeed meta a infer meta b end rule end math ] "
\item " [ math in theory system Q rule 1rule exist intro says for all terms meta x comma meta t comma meta a comma meta b indeed exist-sub meta a is meta b where meta x is meta t end sub endorse meta a infer meta b end rule end math ] "
\item " [ math in theory system Q rule axiom extensionality says for all terms meta x comma meta y indeed meta x zermelo is meta y iff for all object s indeed parenthesis object s in0 meta x iff object s in0 meta y end parenthesis end rule end math ] "
\item " [ math in theory system Q rule axiom empty set says for all terms meta s indeed not0 meta s in0 zermelo empty set end rule end math ] "
\item " [ math in theory system Q rule axiom pair definition says for all terms meta s comma meta x comma meta y indeed meta s in0 zermelo pair meta x comma meta y end pair iff meta s zermelo is meta x or0 meta s zermelo is meta y end rule end math ] "
\item " [ math in theory system Q rule axiom union definition says for all terms meta s comma meta x indeed meta s in0 union meta x end union iff parenthesis meta s in0 ex10 and0 ex10 in0 meta x end parenthesis end rule end math ] "
\item " [ math in theory system Q rule axiom power definition says for all terms meta s comma meta x indeed meta s in0 power meta x end power iff for all object s indeed parenthesis object s in0 meta s imply object s in0 meta x end parenthesis end rule end math ] "
\item " [ math in theory system Q rule axiom separation definition says for all terms meta a comma meta b comma meta p comma meta x comma meta z indeed meta p is placeholder-var and ph-sub meta b is meta a where meta p is meta z end sub endorse macro newline meta z in0 the set of ph in meta x such that meta a end set iff meta z in0 meta x and0 meta b end rule end math ] "
\end{list}
\appendix
------------- RRRRRRRRRRRRRRR -------------
(*** import fra A.M. ***)
" [ math in theory system Q rule lemma timesCommutativity(R) says for all terms meta fx comma meta fy indeed R( meta fx ) ** R( meta fy ) == R( meta fy ) ** R( meta fx ) end rule end math ] "
(*** aksiomer ***)
" [ math in theory system Q rule axiom leqReflexivity says for all terms meta x indeed meta x <= meta x end rule end math ] "
" [ math in theory system Q rule axiom leqAntisymmetry says for all terms meta x comma meta y indeed meta x <= meta y imply meta y <= meta x imply meta x = meta y end rule end math ] "
" [ math in theory system Q rule axiom leqTransitivity says for all terms meta x comma meta y comma meta z indeed meta x <= meta y imply meta y <= meta z imply meta x <= meta z end rule end math ] "
" [ math in theory system Q rule axiom leqTotality says for all terms meta x comma meta y indeed meta x <= meta y or0 meta y <= meta x end rule end math ] "
" [ math in theory system Q rule axiom leqAddition says for all terms meta x comma meta y comma meta z indeed meta x <= meta y imply meta x + meta z <= meta y + meta z end rule end math ] "
" [ math in theory system Q rule axiom leqMultiplication says for all terms meta x comma meta y comma meta z indeed 0 <= meta z imply meta x <= meta y imply meta x * meta z <= meta y * meta z end rule end math ] "
" [ math in theory system Q rule axiom plusAssociativity says for all terms meta x comma meta y comma meta z indeed parenthesis meta x + meta y end parenthesis + meta z = meta x + parenthesis meta y + meta z end parenthesis end rule end math ] "
" [ math in theory system Q rule axiom plusCommutativity says for all terms meta x comma meta y indeed meta x + meta y = meta y + meta x end rule end math ] "
" [ math in theory system Q rule axiom negative says for all terms meta x indeed meta x + parenthesis - meta x end parenthesis = 0 end rule end math ] "
" [ math in theory system Q rule axiom plus0 says for all terms meta x indeed meta x + 0 = meta x end rule end math ] "
" [ math in theory system Q rule axiom timesAssociativity says for all terms meta x comma meta y comma meta z indeed parenthesis meta x * meta y end parenthesis * meta z = meta x * parenthesis meta y * meta z end parenthesis end rule end math ] "
" [ math in theory system Q rule axiom timesCommutativity says for all terms meta x comma meta y indeed meta x * meta y = meta y * meta x end rule end math ] "
" [ math in theory system Q rule axiom reciprocal says for all terms meta x indeed meta x != 0 imply meta x * 1/ meta x = 1 end rule end math ] "
" [ math in theory system Q rule axiom times1 says for all terms meta x indeed meta x * 1 = meta x end rule end math ] "
" [ math in theory system Q rule axiom distribution says for all terms meta x comma meta y comma meta z indeed meta x * parenthesis meta y + meta z end parenthesis = parenthesis meta x * meta y end parenthesis + parenthesis meta x * meta z end parenthesis end rule end math ] "
" [ math in theory system Q rule axiom 0not1 says 0 != 1 end rule end math ] "
" [ math in theory system Q rule axiom equality says for all terms meta x comma meta y comma meta z indeed meta x = meta y imply meta x = meta z imply meta y = meta z end rule end math ] "
" [ math in theory system Q rule axiom eqLeq says for all terms meta x comma meta y indeed meta x = meta y imply meta x <= meta y end rule end math ] "
" [ math in theory system Q rule axiom eqAddition says for all terms meta x comma meta y comma meta z indeed meta x = meta y imply meta x + meta z = meta y + meta z end rule end math ] "
" [ math in theory system Q rule axiom eqMultiplication says for all terms meta x comma meta y comma meta z indeed meta x = meta y imply meta x * meta z = meta y * meta z end rule end math ] "
" [ math in theory system Q rule axiom a4 says for all terms meta x comma meta v1 comma meta a comma meta b indeed meta-sub meta a is meta b where meta v1 is meta x end sub endorse for all meta v1 indeed meta b imply meta a end rule end math ] "
(*** XX snydeaksiomer ***)
" [ math in theory system Q rule lemma ==Reflexivity says for all terms meta rx indeed meta rx == meta rx end rule end math ] "
" [ math in theory system Q rule lemma ==Symmetry says for all terms meta rx comma meta ry indeed meta rx == meta ry infer meta ry == meta rx end rule end math ] "
" [ math in theory system Q rule lemma ==Transitivity says for all terms meta rx comma meta ry comma meta rz indeed meta rx == meta ry infer meta ry == meta rz infer meta rx == meta rz end rule end math ] "
XX ikke 100procent identisk med originalen fra equivalence-relations
" [ math in theory system Q rule lemma set equality nec condition(1) says for all terms meta fx comma meta rx comma meta ry indeed meta rx == meta ry infer meta fx in0 meta rx infer meta fx in0 meta ry end rule end math ] "
XX boer bevises ud fra nummer 1
" [ math in theory system Q rule lemma set equality nec condition(2) says for all terms meta fx comma meta rx comma meta ry indeed meta rx == meta ry infer meta fx in0 meta ry infer meta fx in0 meta rx end rule end math ] "
" [ math in theory system Q rule axiom plusF says for all terms meta m comma meta fx comma meta fy indeed [ meta fx +f meta fy ; meta m ] = [ meta fx ; meta m ] + [ meta fy ; meta m ] end rule end math ] "
" [ math in theory system Q rule 1rule from== says for all terms meta fx comma meta fy indeed R( meta fx ) == R( meta fy ) infer meta fx sameF meta fy end rule end math ] "
" [ math in theory system Q rule 1rule to== says for all terms meta fx comma meta fy indeed meta fx sameF meta fy infer R( meta fx ) == R( meta fy ) end rule end math ] "
" [ math in theory system Q rule 1rule fromInR says for all terms meta fx comma meta fy indeed meta fx in0 R( meta fy ) infer meta fx sameF meta fy end rule end math ] "
(*** makroer ***)
KVANTI
" [ math macro define meta m1 as metavar var m1 end metavar end define end math ] "
" [ math macro define meta m2 as metavar var m2 end metavar end define end math ] "
" [ math macro define meta n1 as metavar var n1 end metavar end define end math ] "
" [ math macro define meta n2 as metavar var n2 end metavar end define end math ] "
" [ math macro define meta n3 as metavar var n3 end metavar end define end math ] "
" [ math macro define meta ep as metavar var ep end metavar end define end math ] "
" [ math macro define meta ep1 as metavar var ep1 end metavar end define end math ] "
" [ math macro define meta ep2 as metavar var ep2 end metavar end define end math ] "
" [ math macro define meta x1 as metavar var x1 end metavar end define end math ] "
" [ math macro define meta x2 as metavar var x2 end metavar end define end math ] "
" [ math macro define meta y1 as metavar var y1 end metavar end define end math ] "
" [ math macro define meta y2 as metavar var y2 end metavar end define end math ] "
" [ math macro define meta v1 as metavar var v1 end metavar end define end math ] "
" [ math macro define meta v2 as metavar var v2 end metavar end define end math ] "
" [ math macro define meta v3 as metavar var v3 end metavar end define end math ] "
" [ math macro define meta v4 as metavar var v4 end metavar end define end math ] "
" [ math macro define meta v2n as metavar var v2n end metavar end define end math ] "
" [ math macro define meta fx as metavar var fx end metavar end define end math ] "
" [ math macro define meta fy as metavar var fy end metavar end define end math ] "
" [ math macro define meta fz as metavar var fz end metavar end define end math ] "
" [ math macro define meta fu as metavar var fu end metavar end define end math ] "
" [ math macro define meta fv as metavar var fv end metavar end define end math ] "
" [ math macro define meta fw as metavar var fw end metavar end define end math ] "
" [ math macro define meta fep as metavar var fep end metavar end define end math ] "
" [ math macro define meta rx as metavar var rx end metavar end define end math ] "
" [ math macro define meta ry as metavar var ry end metavar end define end math ] "
" [ math macro define meta rz as metavar var rz end metavar end define end math ] "
" [ math macro define meta ru as metavar var ru end metavar end define end math ] "
" [ math macro define meta sx as metavar var sx end metavar end define end math ] "
" [ math macro define meta sx1 as metavar var sx1 end metavar end define end math ] "
" [ math macro define meta sy as metavar var sy end metavar end define end math ] "
" [ math macro define meta sy1 as metavar var sy1 end metavar end define end math ] "
" [ math macro define meta sz as metavar var sz end metavar end define end math ] "
" [ math macro define meta sz1 as metavar var sz1 end metavar end define end math ] "
" [ math macro define meta su as metavar var su end metavar end define end math ] "
" [ math macro define meta su1 as metavar var su1 end metavar end define end math ] "
" [ math macro define meta fxs as metavar var fxs end metavar end define end math ] "
" [ math macro define meta fys as metavar var fys end metavar end define end math ] "
" [ math macro define meta f1 as metavar var f1 end metavar end define end math ] "
" [ math macro define meta f2 as metavar var f2 end metavar end define end math ] "
" [ math macro define meta f3 as metavar var f3 end metavar end define end math ] "
" [ math macro define meta f4 as metavar var f4 end metavar end define end math ] "
" [ math macro define meta op1 as metavar var op1 end metavar end define end math ] "
" [ math macro define meta op2 as metavar var op2 end metavar end define end math ] "
" [ math macro define meta r1 as metavar var r1 end metavar end define end math ] "
" [ math macro define meta s1 as metavar var s1 end metavar end define end math ] "
" [ math macro define meta s2 as metavar var s2 end metavar end define end math ] "
" [ math macro define object ep as object var var ep end var end define end math ] "
" [ math macro define object crs1 as object var var crs1 end var end define end math ] "
" [ math macro define object f1 as object var var f1 end var end define end math ] "
" [ math macro define object f2 as object var var f2 end var end define end math ] "
" [ math macro define object f3 as object var var f3 end var end define end math ] "
" [ math macro define object f4 as object var var f4 end var end define end math ] "
" [ math macro define object n1 as object var var n1 end var end define end math ] "
" [ math macro define object n2 as object var var n2 end var end define end math ] "
" [ math macro define object op1 as object var var op1 end var end define end math ] "
" [ math macro define object op2 as object var var op2 end var end define end math ] "
" [ math macro define object r1 as object var var r1 end var end define end math ] "
" [ math macro define object s1 as object var var s1 end var end define end math ] "
" [ math macro define object s2 as object var var s2 end var end define end math ] "
" [ math macro define var fx <=f var fy as var fx
" [ math macro define ex3 as existential var var c end var end define end math ] "
" [ math macro define exist0 var v1 indeed var a as not0 for all var v1 indeed not0 var a end define end math ] "
" [ math macro define var x <<== var y as var x << var y or0 var x == var y end define end math ] "
" [ math macro define (-1) as - 1 end define end math ] "
" [ math macro define 2 as 1 + 1 end define end math ] "
" [ math macro define 3 as 2 + 1 end define end math ] "
" [ math macro define 1/2 as 1/ 2 end define end math ] "
" [ math macro define 1/3 as 1/ 3 end define end math ] "
" [ math macro define 2/3 as 2 * 1/3 end define end math ] "
" [ math macro define var x < var y as var x <= var y and0 var x != var y end define end math ] "
" [ math macro define var x != var y as not0 var x = var y end define end math ] "
" [ math macro define var x - var y as var x + - var y end define end math ] "
" [ math macro define 00 as R( 0f ) end define end math ] "
" [ math macro define 01 as R( 1f ) end define end math ] "
" [ math macro define var x !!== var y as not0 var x == var y end define end math ] "
(*** REGELLEMMAER ***)
(*** UDSAGNSLOGIK ***)
" [ math in theory system Q lemma prop lemma to negated imply says for all terms meta a comma meta b indeed meta a infer not0 meta b infer not0 parenthesis meta a imply meta b end parenthesis end lemma end math ] "
" [ math system Q proof of prop lemma to negated imply reads block any term meta a comma meta b end line line ell a premise meta a end line line ell b premise not0 meta b end line line ell c premise not0 not0 parenthesis meta a imply meta b end parenthesis end line line ell d because prop lemma remove double neg modus ponens ell c indeed meta a imply meta b end line line ell e because 1rule mp modus ponens ell d modus ponens ell a indeed meta b end line because prop lemma from contradiction modus ponens ell e modus ponens ell b indeed not0 parenthesis meta a imply meta b end parenthesis end line line ell f end block any term meta a comma meta b end line line ell g because 1rule deduction modus ponens ell f indeed meta a imply not0 meta b imply not0 not0 parenthesis meta a imply meta b end parenthesis imply not0 parenthesis meta a imply meta b end parenthesis end line line ell h premise meta a end line line ell i premise not0 meta b end line line ell j because prop lemma mp2 modus ponens ell g modus ponens ell h modus ponens ell i indeed not0 not0 parenthesis meta a imply meta b end parenthesis imply not0 parenthesis meta a imply meta b end parenthesis end line line ell k because prop lemma auto imply indeed not0 not0 parenthesis meta a imply meta b end parenthesis imply not0 not0 parenthesis meta a imply meta b end parenthesis end line because 1rule ad absurdum modus ponens ell j modus ponens ell k indeed not0 parenthesis meta a imply meta b end parenthesis qed end math ] "
" [ math in theory system Q lemma prop lemma tertium non datur says for all terms meta a indeed meta a or0 not0 meta a end lemma end math ] "
" [ math system Q proof of prop lemma tertium non datur reads any term meta a end line line ell a because prop lemma auto imply indeed not0 meta a imply not0 meta a end line because 1rule repetition modus ponens ell a indeed meta a or0 not0 meta a qed end math ] "
" [ math in theory system Q lemma prop lemma from negations says for all terms meta a comma meta b indeed meta a imply meta b infer not0 meta a imply meta b infer meta b end lemma end math ] "
" [ math system Q proof of prop lemma from negations reads any term meta a comma meta b end line line ell a premise meta a imply meta b end line line ell b premise not0 meta a imply meta b end line line ell c because prop lemma tertium non datur indeed meta a or0 not0 meta a end line because prop lemma from disjuncts modus ponens ell c modus ponens ell a modus ponens ell b indeed meta b qed end math ] "
" [ math in theory system Q lemma prop lemma imply negation says for all terms meta a indeed meta a imply not0 meta a infer not0 meta a end lemma end math ] "
" [ math system Q proof of prop lemma imply negation reads any term meta a end line line ell a premise meta a imply not0 meta a end line line ell b because prop lemma auto imply indeed not0 meta a imply not0 meta a end line line ell c because prop lemma tertium non datur indeed meta a or0 not0 meta a end line because prop lemma from disjuncts modus ponens ell c modus ponens ell a modus ponens ell b indeed not0 meta a qed end math ] "
" [ math in theory system Q lemma prop lemma from three disjuncts says for all terms meta a comma meta b comma meta c comma meta d indeed meta a or0 meta b or0 meta c infer meta a imply meta d infer meta b imply meta d infer meta c imply meta d infer meta d end lemma end math ] "
" [ math system Q proof of prop lemma from three disjuncts reads block any term meta a comma meta b comma meta c comma meta d end line line ell big a premise meta a or0 meta b or0 meta c end line line ell big b premise meta b imply meta d end line line ell big c premise meta c imply meta d end line line ell big d premise not0 meta a end line line ell big e because 1rule repetition modus ponens ell big a indeed not0 meta a imply parenthesis meta b or0 meta c end parenthesis end line line ell big f because 1rule mp modus ponens ell big e modus ponens ell big d indeed meta b or0 meta c end line because prop lemma from disjuncts modus ponens ell big f modus ponens ell big b modus ponens ell big c indeed meta d end line line ell big g end block any term meta a comma meta b comma meta c comma meta d end line line ell a because 1rule deduction modus ponens ell big g indeed meta a or0 meta b or0 meta c imply parenthesis meta b imply meta d end parenthesis imply parenthesis meta c imply meta d end parenthesis imply not0 meta a imply meta d end line line ell b because prop lemma auto imply indeed parenthesis meta a imply meta d end parenthesis imply meta a imply meta d end line line ell c premise meta a or0 meta b or0 meta c end line line ell d premise meta a imply meta d end line line ell e premise meta b imply meta d end line line ell f premise meta c imply meta d end line line ell g because prop lemma mp3 modus ponens ell a modus ponens ell c modus ponens ell e modus ponens ell f indeed not0 meta a imply meta d end line line ell h because 1rule mp modus ponens ell b modus ponens ell d indeed meta a imply meta d end line because prop lemma from negations modus ponens ell h modus ponens ell g indeed meta d qed end math ] "
" [ math in theory system Q lemma prop lemma negate first disjunct says for all terms meta a comma meta b indeed meta a or0 meta b infer not0 meta a infer meta b end lemma end math ] "
" [ math system Q proof of prop lemma negate first disjunct reads any term meta a comma meta b end line line ell a premise meta a or0 meta b end line line ell b premise not0 meta a end line line ell c because 1rule repetition modus ponens ell a indeed not0 meta a imply meta b end line because 1rule mp modus ponens ell c modus ponens ell b indeed meta b qed end math ] "
" [ math in theory system Q lemma prop lemma negate second disjunct says for all terms meta a comma meta b indeed meta a or0 meta b infer not0 meta b infer meta a end lemma end math ] "
" [ math system Q proof of prop lemma negate second disjunct reads any term meta a comma meta b end line line ell a premise meta a or0 meta b end line line ell b premise not0 meta b end line line ell c because 1rule repetition modus ponens ell a indeed not0 meta a imply meta b end line because prop lemma negative mt modus ponens ell c modus ponens ell b indeed meta a qed end math ] "
(***)
" [ math in theory system Q lemma prop lemma expand disjuncts says for all terms meta a comma meta b comma meta c comma meta d indeed meta a or0 meta b infer meta c or0 meta d infer meta b or0 meta d or0 parenthesis meta a and0 meta c end parenthesis end lemma end math ] "
" [ math system Q proof of prop lemma expand disjuncts reads block any term meta a comma meta b comma meta c comma meta d end line line ell a premise meta a or0 meta b end line line ell b premise meta c or0 meta d end line line ell c premise not0 meta b end line line ell d premise not0 meta d end line line ell e because prop lemma negate second disjunct modus ponens ell a modus ponens ell c indeed meta a end line line ell f because prop lemma negate second disjunct modus ponens ell b modus ponens ell d indeed meta c end line because prop lemma join conjuncts modus ponens ell e modus ponens ell f indeed meta a and0 meta c end line line ell g end block any term meta a comma meta b comma meta c comma meta d end line line ell h because 1rule deduction modus ponens ell g indeed meta a or0 meta b imply meta c or0 meta d imply not0 meta b imply not0 meta d imply meta a and0 meta c end line line ell i premise meta a or0 meta b end line line ell j premise meta c or0 meta d end line line ell k because prop lemma mp2 modus ponens ell h modus ponens ell i modus ponens ell j indeed not0 meta b imply not0 meta d imply meta a and0 meta c end line because 1rule repetition modus ponens ell k indeed meta b or0 meta d or0 parenthesis meta a and0 meta c end parenthesis qed end math ] "
" [ math in theory system Q lemma prop lemma from two times two disjuncts says for all terms meta a comma meta b comma meta c comma meta d comma meta e indeed meta a or0 meta b infer meta c or0 meta d infer meta a imply meta c imply meta e infer meta a imply meta d imply meta e infer meta b imply meta c imply meta e infer meta b imply meta d imply meta e infer meta e end lemma end math ] "
" [ math system Q proof of prop lemma from two times two disjuncts reads block any term meta a comma meta b comma meta c comma meta d comma meta e end line line ell a premise meta c or0 meta d end line line ell b premise meta a imply meta c imply meta e end line line ell c premise meta a imply meta d imply meta e end line line ell d premise meta a end line line ell e because 1rule mp modus ponens ell b modus ponens ell d indeed meta c imply meta e end line line ell f because 1rule mp modus ponens ell c modus ponens ell d indeed meta d imply meta e end line because prop lemma from disjuncts modus ponens ell a modus ponens ell e modus ponens ell f indeed meta e end line line ell g end block block any term meta a comma meta b comma meta c comma meta d comma meta e end line line ell big a premise meta a or0 meta b end line line ell big b premise meta c or0 meta d end line line ell big c premise meta b imply meta c imply meta e end line line ell big d premise meta b imply meta d imply meta e end line line ell big e premise not0 meta a end line line ell big f because prop lemma negate first disjunct modus ponens ell big a modus ponens ell big e indeed meta b end line line ell big g because 1rule mp modus ponens ell big c modus ponens ell big f indeed meta c imply meta e end line line ell big h because 1rule mp modus ponens ell big d modus ponens ell big f indeed meta d imply meta e end line because prop lemma from disjuncts modus ponens ell big b modus ponens ell big g modus ponens ell big h indeed meta e end line line ell big i end block any term meta a comma meta b comma meta c comma meta d comma meta e end line line ell h because 1rule deduction modus ponens ell g indeed meta c or0 meta d imply parenthesis meta a imply meta c imply meta e end parenthesis imply parenthesis meta a imply meta d imply meta e end parenthesis imply meta a imply meta e end line line ell i because 1rule deduction modus ponens ell big i indeed meta a or0 meta b imply meta c or0 meta d imply parenthesis meta b imply meta c imply meta e end parenthesis imply parenthesis meta b imply meta d imply meta e end parenthesis imply not0 meta a imply meta e end line line ell j premise meta a or0 meta b end line line ell k premise meta c or0 meta d end line line ell l premise meta a imply meta c imply meta e end line line ell m premise meta a imply meta d imply meta e end line line ell n premise meta b imply meta c imply meta e end line line ell o premise meta b imply meta d imply meta e end line line ell p because prop lemma mp3 modus ponens ell h modus ponens ell k modus ponens ell l modus ponens ell m indeed meta a imply meta e end line line ell q because prop lemma mp4 modus ponens ell i modus ponens ell j modus ponens ell k modus ponens ell n modus ponens ell o indeed not0 meta a imply meta e end line because prop lemma from negations modus ponens ell p modus ponens ell q indeed meta e qed end math ] "
(*** SAME-F ***)
XX-am
(*** R-AFDELINGEN ***)
XX-am
(*******************)
" [ math in theory system Q lemma prop lemma from negated imply says for all terms meta a comma meta b indeed not0 parenthesis meta a imply meta b end parenthesis infer meta a and0 not0 meta b end lemma end math ] "
" [ math system Q proof of prop lemma from negated imply reads block any term meta a comma meta b end line line ell a premise meta a imply not0 not0 meta b end line line ell b premise meta a end line line ell c because 1rule mp modus ponens ell a modus ponens ell b indeed not0 not0 meta b end line because prop lemma remove double neg modus ponens ell c indeed meta b end line line ell big a end block any term meta a comma meta b end line line ell a because 1rule deduction modus ponens ell big a indeed parenthesis meta a imply not0 not0 meta b end parenthesis imply parenthesis meta a imply meta b end parenthesis end line line ell b premise not0 parenthesis meta a imply meta b end parenthesis end line line ell c because prop lemma mt modus ponens ell a modus ponens ell b indeed not0 parenthesis meta a imply not0 not0 meta b end parenthesis end line because 1rule repetition modus ponens ell c indeed meta a and0 not0 meta b qed end math ] "
(***)
" [ math in theory system Q lemma prop lemma from negated double imply says for all terms meta a comma meta b comma meta c indeed not0 parenthesis meta a imply meta b imply meta c end parenthesis infer meta a and0 meta b and0 not0 meta c end lemma end math ] "
" [ math system Q proof of prop lemma from negated double imply reads any term meta a comma meta b comma meta c end line line ell a premise not0 parenthesis meta a imply meta b imply meta c end parenthesis end line line ell b because prop lemma from negated imply modus ponens ell a indeed meta a and0 not0 parenthesis meta b imply meta c end parenthesis end line line ell c because prop lemma first conjunct modus ponens ell b indeed meta a end line line ell d because prop lemma second conjunct modus ponens ell b indeed not0 parenthesis meta b imply meta c end parenthesis end line line ell e because prop lemma from negated imply modus ponens ell d indeed meta b and0 not0 meta c end line line ell f because prop lemma first conjunct modus ponens ell e indeed meta b end line line ell g because prop lemma second conjunct modus ponens ell e indeed not0 meta c end line line ell h because prop lemma join conjuncts modus ponens ell c modus ponens ell f indeed meta a and0 meta b end line because prop lemma join conjuncts modus ponens ell h modus ponens ell g indeed meta a and0 meta b and0 not0 meta c qed end math ] "
" [ math in theory system Q lemma prop lemma from negated or says for all terms meta a comma meta b indeed not0 parenthesis meta a or0 meta b end parenthesis infer not0 meta a and0 not0 meta b end lemma end math ] "
" [ math system Q proof of prop lemma from negated or reads any term meta a comma meta b end line line ell a premise not0 parenthesis meta a or0 meta b end parenthesis end line line ell b because 1rule repetition modus ponens ell a indeed not0 parenthesis not0 meta a imply meta b end parenthesis end line because prop lemma from negated imply modus ponens ell b indeed not0 meta a and0 not0 meta b qed end math ] "
" [ math in theory system Q rule axiom induction says for all terms meta v1 comma meta a comma meta b comma meta c indeed meta-sub meta b is meta a where meta v1 is 0 end sub endorse meta-sub meta c is meta a where meta v1 is meta v1 + 1 end sub endorse meta b imply for all meta v1 indeed parenthesis meta a imply meta c end parenthesis imply for all meta v1 indeed meta a end rule end math ] "
" [ math in theory system Q rule 1rule lessMinus1(N) says for all terms meta m comma meta n indeed Nat( meta m ) endorse Nat( meta n ) endorse meta m < meta n + 1 infer meta m <= meta n end rule end math ] "
" [ math in theory system Q rule axiom nonnegative(N) says for all terms meta m indeed Nat( meta m ) endorse 0 <= meta m end rule end math ] "
--------------
" [ math in theory system Q rule axiom cauchy says for all terms meta v1 comma meta v2 comma meta n comma meta ep comma meta fx indeed for all meta ep indeed exist0 meta n indeed for all meta v1 comma meta v2 indeed parenthesis 0 < meta ep imply meta n <= meta v1 imply meta n <= meta v2 imply | [ meta fx ; meta v1 ] - [ meta fx ; meta v2 ] | < meta ep end parenthesis end rule end math ] "
-------------
--------------
" [ math in theory system Q lemma prop lemma doubly conditioned join conjuncts says for all terms meta a comma meta b comma meta c comma meta d indeed meta a imply meta b imply meta c infer meta a imply meta b imply meta d infer meta a imply meta b imply meta c and0 meta d end lemma end math ] "
" [ math system Q proof of prop lemma doubly conditioned join conjuncts reads block any term meta a comma meta b comma meta c comma meta d end line line ell a premise meta a imply meta b imply meta c end line line ell b premise meta a imply meta b imply meta d end line line ell c premise meta a end line line ell d premise meta b end line line ell e because prop lemma mp2 modus ponens ell a modus ponens ell c modus ponens ell d indeed meta c end line line ell f because prop lemma mp2 modus ponens ell b modus ponens ell c modus ponens ell d indeed meta d end line because prop lemma join conjuncts modus ponens ell e modus ponens ell f indeed meta c and0 meta d end line line ell big a end block any term meta a comma meta b comma meta c comma meta d end line line ell a because 1rule deduction modus ponens ell big a indeed parenthesis meta a imply meta b imply meta c end parenthesis imply parenthesis meta a imply meta b imply meta d end parenthesis imply meta a imply meta b imply meta c and0 meta d end line line ell b premise meta a imply meta b imply meta c end line line ell c premise meta a imply meta b imply meta d end line because prop lemma mp2 modus ponens ell a modus ponens ell b modus ponens ell c indeed meta a imply meta b imply meta c and0 meta d qed end math ] "
----------------
" [ math in theory system Q lemma prop lemma from negated and says for all terms meta a comma meta b indeed not0 parenthesis meta a and0 meta b end parenthesis infer meta a infer not0 meta b end lemma end math ] "
" [ math system Q proof of prop lemma from negated and reads any term meta a comma meta b end line line ell a premise not0 parenthesis meta a and0 meta b end parenthesis end line line ell b premise meta a end line line ell c because 1rule repetition modus ponens ell a indeed not0 not0 parenthesis meta a imply not0 meta b end parenthesis end line line ell d because prop lemma remove double neg modus ponens ell c indeed meta a imply not0 meta b end line because 1rule mp modus ponens ell d modus ponens ell b indeed not0 meta b qed end math ] "
--------
----------
" [ math in theory system Q lemma prop lemma to negated or says for all terms meta a comma meta b indeed not0 meta a and0 not0 meta b infer not0 parenthesis meta a or0 meta b end parenthesis end lemma end math ] "
" [ math system Q proof of prop lemma to negated or reads block any term meta a comma meta b end line line ell a premise not0 meta a and0 not0 meta b end line line ell b premise meta a or0 meta b end line line ell c because prop lemma first conjunct modus ponens ell a indeed not0 meta a end line line ell d because prop lemma second conjunct modus ponens ell a indeed not0 meta b end line line ell e because prop lemma negate first disjunct modus ponens ell b modus ponens ell c indeed meta b end line because prop lemma from contradiction modus ponens ell e modus ponens ell d indeed not0 parenthesis meta a or0 meta b end parenthesis end line line ell big a end block any term meta a comma meta b end line line ell a because 1rule deduction modus ponens ell big a indeed not0 meta a and0 not0 meta b imply meta a or0 meta b imply not0 parenthesis meta a or0 meta b end parenthesis end line line ell b premise not0 meta a and0 not0 meta b end line line ell c because 1rule mp modus ponens ell a modus ponens ell b indeed meta a or0 meta b imply not0 parenthesis meta a or0 meta b end parenthesis end line because prop lemma imply negation modus ponens ell c indeed not0 parenthesis meta a or0 meta b end parenthesis qed end math ] "
--------------------
" [ math in theory system Q rule 1rule nextXS(upperBound) says for all terms meta m indeed upperBound( 01//02 ** parenthesis [ xs ; meta m ] ++ [ us ; meta m ] end parenthesis , setOfReals ) infer [ xs ; meta m + 1 ] == [ xs ; meta m ] end rule end math ] "
" [ math in theory system Q rule 1rule nextXS(noUpperBound) says for all terms meta m indeed not0 upperBound( 01//02 ** ( [ xs ; meta m ] ++ [ us ; meta m ] ) , setOfReals ) infer [ xs ; meta m + 1 ] == 01//02 ** parenthesis [ xs ; meta m ] ++ [ us ; meta m ] end parenthesis end rule end math ] "
" [ math in theory system Q rule 1rule nextUS(upperBound) says for all terms meta m indeed upperBound( 01//02 ** parenthesis [ xs ; meta m ] ++ [ us ; meta m ] end parenthesis , setOfReals ) infer [ us ; meta m + 1 ] == 01//02 ** parenthesis [ xs ; meta m ] ++ [ us ; meta m ] end parenthesis end rule end math ] "
" [ math in theory system Q rule 1rule nextUS(noUpperBound) says for all terms meta m indeed not0 upperBound( 01//02 ** ( [ xs ; meta m ] ++ [ us ; meta m ] ) , setOfReals ) infer [ us ; meta m + 1 ] == [ us ; meta m ] end rule end math ] "
" [ math in theory system Q rule axiom US0 says [ us ; 0 ] == [ xs ; 0 ] ++ 01 end rule end math ] "
" [ math in theory system Q rule 1rule expZero says for all terms meta m comma meta x indeed meta m = 0 infer meta x ^ meta m = 1 end rule end math ] "
" [ math in theory system Q rule 1rule expPositive says for all terms meta m comma meta x indeed 0 < meta m infer meta x ^ meta m = meta x * meta x ^ parenthesis meta m - 1 end parenthesis end rule end math ] "
--------------
" [ math in theory system Q rule 1rule base(1/2)Sum zero says for all terms meta m comma meta n indeed meta n = 0 infer base(1/2)Sum( meta m , meta n ) = 1/2 ^ meta m end rule end math ] "
" [ math in theory system Q rule 1rule base(1/2)Sum positive says for all terms meta m comma meta n indeed 0 < meta n infer base(1/2)Sum( meta m , meta n ) = 1/2 ^ parenthesis meta m + meta n end parenthesis + base(1/2)Sum( meta m , meta n - 1 ) end rule end math ] "
------------
" [ math in theory system Q rule 1rule UStelescope zero says for all terms meta m comma meta n indeed meta n = 0 infer UStelescope( meta m , meta n ) = | [ us ; meta m ] - [ us ; meta m + 1 ] | end rule end math ] "
" [ math in theory system Q rule 1rule UStelescope positive says for all terms meta m comma meta n indeed 0 < meta n infer UStelescope( meta m , meta n ) = | [ us ; meta m + meta n ] - [ us ; meta m + ( meta n + 1 ) ] | + UStelescope( meta m , meta n - 1 ) end rule end math ] "
" [ math macro define ( var x ) as parenthesis var x end parenthesis end define end math ] "
----------
" [ math in theory system Q rule 1rule adhoc eqAddition(R) says for all terms meta fx comma meta fy comma meta fz indeed R( meta fx ) = R( meta fy ) infer R( meta fx ) ++ R( meta fz ) = R( meta fy ) ++ R( meta fz ) end rule end math ] "
" [ math in theory system Q rule lemma plusCommutativity(R) says for all terms meta fx comma meta fy indeed R( meta fx ) ++ R( meta fy ) == R( meta fy ) ++ R( meta fx ) end rule end math ] "
---------------
" [ math in theory system Q rule lemma plusAssociativity(R) says for all terms meta fx comma meta fy comma meta fz indeed R( meta fx ) ++ R( meta fy ) ++ R( meta fz ) = R( meta fx ) ++ ( R( meta fy ) ++ R( meta fz ) ) end rule end math ] "
" [ math in theory system Q rule lemma plusAssociativity(R)XX says for all terms meta fx comma meta fy comma meta fz indeed R( meta fx +f meta fy +f meta fz ) == R( meta fx +f ( meta fy +f meta fz ) ) end rule end math ] "
" [ math in theory system Q rule lemma plus0(R) says for all terms meta fx indeed R( meta fx ) ++ 00 == R( meta fx ) end rule end math ] "
" [ math in theory system Q rule lemma negative(R) says for all terms meta m comma meta fx indeed R( meta fx ) ++ -- R( meta fx ) == 00 end rule end math ] "
" [ math in theory system Q rule lemma timesAssociativity(R) says for all terms meta fx comma meta fy comma meta fz indeed R( meta fx ) ** R( meta fy ) ** R( meta fz ) == R( meta fx ) ** ( R( meta fy ) ** R( meta fz ) ) end rule end math ] "
" [ math in theory system Q rule lemma times1(R) says for all terms meta fx indeed R( meta fx ) ** 01 == R( meta fx ) end rule end math ] "
" [ math var a end math ] "
venter-------
" [ flush left math priority table 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 protect 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 <
\newpage
\section{\TeX{} definitioner} \label{sec:tex}
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math tex define kvanti as "kvanti" end define end math ] "
\item " [ math tex define cdots as "(\cdots{})" end define end math ] "
\item " [ math tex define object-var as "\texttt{Objekt-var}" end define end math ] "
\item " [ math tex define ex-var as "\texttt{Ex-var}" end define end math ] "
\item " [ math tex define ph-var as "\texttt{Ph-var}" end define end math ] "
\item " [ math tex define vaerdi as "\texttt{V\ae{}rdi}" end define end math ] "
\item " [ math tex define variabel as "\texttt{Variabel}" end define end math ] "
\item " [ math tex define op var x end op as "Op(#1.
)" end define end math ] "
\item " [ math tex define op2 var x comma var y end op2 as "Op(#1.
,#2.
)" end define end math ] "
\item " [ math tex define define-equal var x comma var y end equal as "#1.
\mathrel {\ddot {==}} #2." end define end math ] "
\item " [ math tex define contains-empty var x end empty as "ContainsEmpty(#1.
)" end define end math ] "
\item " [ math tex define 1deduction var x conclude var y end 1deduction as "
Dedu(#1.
,#2.
)" end define end math ] "
\item " [ math tex define 1deduction zero var x conclude var y end 1deduction as "
Dedu_0(#1.
,#2.
)" end define end math ] "
\item " [ math tex define 1deduction side var x conclude var y condition var z end 1deduction as "Dedu_{s}(#1.
,#2.
,#3.
)" end define end math ] "
\item " [ math tex define 1deduction one var x conclude var y condition var z end 1deduction as "
Dedu_1(#1.
,#2.
,#3.
)" end define end math ] "
\item " [ math tex define 1deduction two var x conclude var y condition var z end 1deduction as "
Dedu_2(#1.
,#2.
,#3.
)" end define end math ] "
\item " [ math tex define 1deduction three var x conclude var y condition var z bound var u end 1deduction as "
Dedu_3(#1.
,#2.
,#3.
,#4.
)" end define end math ] "
\item " [ math tex define 1deduction four var x conclude var y condition var z bound var u end 1deduction as "
Dedu_4(#1.
,#2.
,#3.
,#4.
)" end define end math ] "
\item " [ math tex define 1deduction four star var x conclude var y condition var z bound var u end 1deduction as "
Dedu_4^*(#1.
,#2.
,#3.
,#4.
)" end define end math ] "
\item " [ math tex define 1deduction five var x condition var y bound var z end 1deduction as "
Dedu_5(#1.
,#2.
,#3.
)" end define end math ] "
\item " [ math tex define 1deduction six var p conclude var c exception var e bound var b end 1deduction as "
Dedu_6(#1.
,#2.
,#3.
,#4.
)" end define end math ] "
\item " [ math tex define 1deduction six star var p conclude var c exception var e bound var b end 1deduction as "
Dedu_6^*(#1.
,#2.
,#3.
,#4.
)" end define end math ] "
\item " [ math tex define 1deduction seven var p end 1deduction as "
Dedu_7(#1.
)" end define end math ] "
\item " [ math tex define 1deduction eight var p bound var b end 1deduction as "
Dedu_8(#1.
,#2.
)" end define end math ] "
\item " [ math tex define 1deduction eight star var p bound var b end 1deduction as "
Dedu_8^*(#1.
,#2.
)" end define end math ] "
\item " [ math tex define ex1 as "Ex_{1}" end define end math ] "
\item " [ math tex define ex2 as "Ex_{2}" end define end math ] "
\item " [ math tex define ex10 as "Ex_{10}" end define end math ] "
\item " [ math tex define ex20 as "Ex_{20}" end define end math ] "
\item " [ math tex define existential var var x end var as "#1.
_{Ex}" end define end math ] "
\item " [ math tex define var x is existential var as "#1.
^{Ex}" end define end math ] "
\item " [ math tex define exist-sub var x is var y where var z is var u end sub as "\langle #1.
{\equiv} #2.
| #3.
{:==} #4.
\rangle_{Ex} " end define end math ] "
\item " [ math tex define exist-sub0 var x is var y where var z is var u end sub as "\langle #1.
{\equiv}^0 #2.
| #3.
{:==} #4.
\rangle_{Ex} " end define end math ] "
\item " [ math tex define exist-sub1 var x is var y where var z is var u end sub as "\langle #1.
{\equiv}^1 #2.
| #3.
{:==} #4.
\rangle_{Ex} " end define end math ] "
\item " [ math tex define exist-sub* var x is var y where var z is var u end sub as "\langle #1.
{\equiv}^* #2.
| #3.
{:==} #4.
\rangle_{Ex} " end define end math ] "
\item " [ math tex define ph1 as "ph_{1}" end define end math ] "
\item " [ math tex define ph2 as "ph_{2}" end define end math ] "
\item " [ math tex define ph3 as "ph_{3}" end define end math ] "
\item " [ math tex define ph4 as "ph_{4}" end define end math ] "
\item " [ math tex define ph5 as "ph_{5}" end define end math ] "
\item " [ math tex define ph6 as "ph_{6}" end define end math ] "
\item " [ math tex define placeholder-var x end var as "#1.
_{Ph} " end define end math ] "
\item " [ math tex define var x is placeholder-var as "#1.
^{Ph}" end define end math ] "
\item " [ math tex define ph-sub var x is var y where var z is var u end sub as "\langle #1.
{\equiv} #2.
| #3.
{:==} #4.
\rangle_{Ph} " end define end math ] "
\item " [ math tex define ph-sub0 var x is var y where var z is var u end sub as "\langle #1.
{\equiv}^0 #2.
| #3.
{:==} #4.
\rangle_{Ph} " end define end math ] "
\item " [ math tex define ph-sub1 var x is var y where var z is var u end sub as "\langle #1.
{\equiv}^1 #2.
| #3.
{:==} #4.
\rangle_{Ph} " end define end math ] "
\item " [ math tex define ph-sub* var x is var y where var z is var u end sub as "\langle #1.
{\equiv}^* #2.
| #3.
{:==} #4.
\rangle_{Ph} " end define end math ] "
\item " [ math tex define var big set as "\mathsf {bs}" end define end math ] "
\item " [ math tex define object big set as " \mathsf {OBS}" end define end math ] "
\item " [ math tex define meta big set as "{\cal BS}" end define end math ] "
\item " [ math tex define zermelo empty set as "\mathrm{\O}" end define end math ] "
\item " [ math tex define system Q as "SystemQ" end define end math ] "
\item " [ math tex define 1rule mp as "MP" end define end math ] "
\item " [ math tex define 1rule gen as "Gen" end define end math ] "
\item " [ math tex define 1rule repetition as "Repetition" end define end math ] "
\item " [ math tex define 1rule ad absurdum as "Neg" end define end math ] "
\item " [ math tex define 1rule deduction as "Ded" end define end math ] "
\item " [ math tex define 1rule exist intro as "ExistIntro" end define end math ] "
\item " [ math tex define axiom extensionality as "Extensionality" end define end math ] "
\item " [ math tex define axiom empty set as "\O{}def" end define end math ] "
\item " [ math tex define axiom pair definition as "PairDef" end define end math ] "
\item " [ math tex define axiom union definition as "UnionDef" end define end math ] "
\item " [ math tex define axiom power definition as "PowerDef" end define end math ] "
\item " [ math tex define axiom separation definition as "SeparationDef" end define end math ] "
\item " [ math tex define prop lemma add double neg as "AddDoubleNeg" end define end math ] "
\item " [ math tex define prop lemma remove double neg as "RemoveDoubleNeg" end define end math ] "
\item " [ math tex define prop lemma and commutativity as "AndCommutativity" end define end math ] "
\item " [ math tex define prop lemma auto imply as "AutoImply" end define end math ] "
\item " [ math tex define prop lemma contrapositive as "Contrapositive" end define end math ] "
\item " [ math tex define prop lemma first conjunct as "FirstConjunct" end define end math ] "
\item " [ math tex define prop lemma second conjunct as "SecondConjunct" end define end math ] "
\item " [ math tex define prop lemma from contradiction as "FromContradiction" end define end math ] "
\item " [ math tex define prop lemma from disjuncts as "FromDisjuncts" end define end math ] "
\item " [ math tex define prop lemma iff commutativity as "IffCommutativity" end define end math ] "
\item " [ math tex define prop lemma iff first as "IffFirst" end define end math ] "
\item " [ math tex define prop lemma iff second as "IffSecond" end define end math ] "
\item " [ math tex define prop lemma imply transitivity as "ImplyTransitivity" end define end math ] "
\item " [ math tex define prop lemma join conjuncts as "JoinConjuncts" end define end math ] "
\item " [ math tex define prop lemma mp2 as "MP2" end define end math ] "
\item " [ math tex define prop lemma mp3 as "MP3" end define end math ] "
\item " [ math tex define prop lemma mp4 as "MP4" end define end math ] "
\item " [ math tex define prop lemma mp5 as "MP5" end define end math ] "
\item " [ math tex define prop lemma mt as "MT" end define end math ] "
\item " [ math tex define prop lemma negative mt as "NegativeMT" end define end math ] "
\item " [ math tex define prop lemma technicality as "Technicality" end define end math ] "
\item " [ math tex define prop lemma weakening as "Weakening" end define end math ] "
\item " [ math tex define prop lemma weaken or first as "WeakenOr1" end define end math ] "
\item " [ math tex define prop lemma weaken or second as "WeakenOr2" end define end math ] "
\item " [ math tex define lemma pair2formula as "Pair2Formula" end define end math ] "
\item " [ math tex define lemma formula2pair as "Formula2Pair" end define end math ] "
\item " [ math tex define lemma union2formula as "Union2Formula" end define end math ] "
\item " [ math tex define lemma formula2union as "Formula2Union" end define end math ] "
\item " [ math tex define lemma formula2power as "Formula2Power" end define end math ] "
\item " [ math tex define lemma separation2formula as "Sep2Formula" end define end math ] "
\item " [ math tex define lemma formula2separation as "Formula2Sep" end define end math ] "
\item " [ math tex define lemma subset in power set as "SubsetInPower" end define end math ] "
\item " [ math tex define lemma power set is subset0 as "HelperPowerIsSub" end define end math ] "
\item " [ math tex define lemma power set is subset as "PowerIsSub" end define end math ] "
\item " [ math tex define lemma power set is subset0-switch as "(Switch)HelperPowerIsSub" end define end math ] "
\item " [ math tex define lemma power set is subset-switch as "(Switch)PowerIsSub" end define end math ] "
\item " [ math tex define lemma set equality suff condition as "ToSetEquality" end define end math ] "
\item " [ math tex define lemma set equality suff condition(t)0 as "HelperToSetEquality(t)" end define end math ] "
\item " [ math tex define lemma set equality suff condition(t) as "ToSetEquality(t)" end define end math ] "
\item " [ math tex define lemma set equality skip quantifier as "HelperFromSetEquality" end define end math ] "
\item " [ math tex define lemma set equality nec condition as "FromSetEquality" end define end math ] "
\item " [ math tex define lemma reflexivity0 as "HelperReflexivity" end define end math ] "
\item " [ math tex define lemma reflexivity as "Reflexivity" end define end math ] "
\item " [ math tex define lemma symmetry0 as "HelperSymmetry" end define end math ] "
\item " [ math tex define lemma symmetry as "Symmetry" end define end math ] "
\item " [ math tex define lemma transitivity0 as "HelperTransitivity" end define end math ] "
\item " [ math tex define lemma transitivity as "Transitivity" end define end math ] ",
\item " [ math tex define lemma er is reflexive as "ERisReflexive" end define end math ] "
\item " [ math tex define lemma er is symmetric as "ERisSymmetric" end define end math ] "
\item " [ math tex define lemma er is transitive as "ERisTransitive" end define end math ] "
\item " [ math tex define lemma empty set is subset as "\O{}isSubset" end define end math ] "
\item " [ math tex define lemma member not empty0 as "HelperMemberNot\O{}" end define end math ] "
\item " [ math tex define lemma member not empty as "MemberNot\O{}" end define end math ] "
\item " [ math tex define lemma unique empty set0 as "HelperUnique\O{}" end define end math ] "
\item " [ math tex define lemma unique empty set as "Unique\O{}" end define end math ] "
\item " [ math tex define lemma ==Reflexivity as "==\!{}Reflexivity" end define end math ] "
\item " [ math tex define lemma ==Symmetry as "==\!{}Symmetry" end define end math ] "
\item " [ math tex define lemma ==Transitivity0 as "Helper\!{}==\!{}Transitivity" end define end math ] "
\item " [ math tex define lemma ==Transitivity as "\!{}==\!{}Transitivity" end define end math ] "
\item " [ math tex define lemma transfer ~is0 as "HelperTransferNotEq" end define end math ] "
\item " [ math tex define lemma transfer ~is as "TransferNotEq" end define end math ] "
\item " [ math tex define lemma pair subset0 as "HelperPairSubset" end define end math ] "
\item " [ math tex define lemma pair subset1 as "Helper(2)PairSubset" end define end math ] "
\item " [ math tex define lemma pair subset as "PairSubset" end define end math ] "
\item " [ math tex define lemma same pair as "SamePair" end define end math ] "
\item " [ math tex define lemma same singleton as "SameSingleton" end define end math ] "
\item " [ math tex define lemma union subset as "UnionSubset" end define end math ] "
\item " [ math tex define lemma same union as "SameUnion" end define end math ] "
\item " [ math tex define lemma separation subset as "SeparationSubset" end define end math ] "
\item " [ math tex define lemma same separation as "SameSeparation" end define end math ] "
\item " [ math tex define lemma same binary union as "SameBinaryUnion" end define end math ] "
\item " [ math tex define lemma intersection subset as "IntersectionSubset" end define end math ] "
\item " [ math tex define lemma same intersection as "SameIntersection" end define end math ] "
\item " [ math tex define lemma auto member as "AutoMember" end define end math ] "
\item " [ math tex define lemma eq-system not empty0 as "HelperEqSysNot\O{}" end define end math ] "
\item " [ math tex define lemma eq-system not empty as "EqSysNot\O{}" end define end math ] "
\item " [ math tex define lemma eq subset0 as "HelperEqSubset" end define end math ] "
\item " [ math tex define lemma eq subset as "EqSubset" end define end math ] "
\item " [ math tex define lemma equivalence nec condition as "EqNecessary" end define end math ] "
\item " [ math tex define lemma equivalence nec condition0 as "HelperEqNecessary" end define end math ] "
\item " [ math tex define lemma none-equivalence nec condition0 as "HelperNoneEqNecessary" end define end math ] "
\item " [ math tex define lemma none-equivalence nec condition1 as "Helper(2)NoneEqNecessary" end define end math ] "
\item " [ math tex define lemma none-equivalence nec condition as "NoneEqNecessary" end define end math ] "
\item " [ math tex define lemma equivalence class is subset as "EqClassIsSubset" end define end math ] "
\item " [ math tex define lemma equivalence classes are disjoint as "EqClassesAreDisjoint" end define end math ] "
\item " [ math tex define lemma all disjoint as "AllDisjoint" end define end math ] "
\item " [ math tex define lemma all disjoint-imply as "AllDisjointImply" end define end math ] "
\item " [ math tex define lemma bs subset union(bs/r) as "BSsubset" end define end math ] "
\item " [ math tex define lemma union(bs/r) subset bs as "Union(BS/R)subset" end define end math ] "
\item " [ math tex define lemma union(bs/r) is bs as "UnionIdentity" end define end math ] "
\item " [ math tex define theorem eq-system is partition as "EqSysIsPartition" end define end math ] "
\item " [ math tex define eq-system of var x modulo var y as "#1.
/ #2." end define end math ] "
\item " [ math tex define intersection var x comma var y end intersection as "#1.
\cap #2." end define end math ] "
\item " [ math tex define union var x end union as "\cup #1." end define end math ] "
\item " [ math tex define binary-union var x comma var y end union as "#1.
\mathrel{\cup} #2." end define end math ] "
\item " [ math tex define power var x end power as "P(#1.
)" end define end math ] "
\item " [ math tex define zermelo singleton var x end singleton as "\{#1.
\}" end define end math ] "
\item " [ math tex define zermelo pair var x comma var y end pair as "\{#1.
,#2.
\}" end define end math ] "
\item " [ math tex define zermelo ordered pair var x comma var y end pair as "\langle #1.
,#2.
\rangle" end define end math ] ",
\item " [ math tex define var x in0 var y as "#1.
\mathrel{\in} #2." end define end math ] "
\item " [ math tex define var x is related to var y under var z as "#3.
(#1.
,#2.
)" end define end math ] "
\item " [ math tex define var r is reflexive relation in var x as "ReflRel(#1.
,#2.
)" end define end math ] "
\item " [ math tex define var r is symmetric relation in var x as "SymRel(#1.
,#2.
)" end define end math ] "
\item " [ math tex define var r is transitive relation in var x as "TransRel(#1.
,#2.
)" end define end math ] "
\item " [ math tex define var r is equivalence relation in var x as "EqRel(#1.
,#2.
)" end define end math ] "
\item " [ math tex define equivalence class of var x in var big set modulo var r as "[#1.
\mathrel{\in} #2.
]_{#3.
}" end define end math ] "
\item " [ math tex define var x is partition of var y as "Partition(#1.
,#2.
)" end define end math ] "
\item " [ math tex define var x zermelo is var y as "#1.
\!\mathrel{==}\! #2." end define end math ] "
\item " [ math tex define var x is subset of var y as "#1.
\mathrel{\subseteq} #2." end define end math ] "
\item " [ math tex define not0 var x as "\dot{\neg}\,(#1.
)n" end define end math ] "
\item " [ math tex define var x zermelo ~in var y as "#1.
\mathrel{\notin} #2." end define end math ] "
\item " [ math tex define var x zermelo ~is var y as "#1.
\mathrel{\neq} #2." end define end math ] "
\item " [ math tex define var x and0 var y as "#1.
\mathrel{\dot{\wedge}} #2." end define end math ] "
\item " [ math tex define var x or0 var y as "#1.
\mathrel{\dot{\vee}} #2." end define end math ] "
\item " [ math tex define var x iff var y as "#1.
\mathrel{\dot{\Leftrightarrow}} #2." end define end math ] "
\item " [ math tex define the set of ph in var x such that var a end set as " \{ ph \mathrel{\in} #1.
\mid #2.
\}" end define end math ] "
\item " [ math tex define var x imply var y as "(i#1.
\Rightarrow #2.
)i" end define end math ] "
\item " [ math tex define Nat( var x ) as "Nat(#1.
)" end define end math ] "
\item " [ math tex define meta-sub var x is var y where var z is var u end sub as "\langle #1.
{\equiv} #2.
| #3.
{:==} #4.
\rangle_{Me}" end define end math ] "
\item " [ math tex define meta-sub1 var x is var y where var z is var u end sub as "\langle #1.
{\equiv}^1 #2.
| #3.
{:==} #4.
\rangle_{Me} " end define end math ] "
\item " [ math tex define meta-sub* var x is var y where var z is var u end sub as "\langle #1.
{\equiv}^* #2.
| #3.
{:==} #4.
\rangle_{Me} " end define end math ] "
\item " [ math tex define exist0 var x indeed var y as "
\exists #1.
\colon #2." end define end math ] "
\item " [ math tex define var x1 as "(x1)" end define end math ] "
\item " [ math tex define var x2 as "(x2)" end define end math ] "
\item " [ math tex define var y1 as "(y1)" end define end math ] "
\item " [ math tex define var y2 as "(y2)" end define end math ] "
\item " [ math tex define var v1 as "(v1)" end define end math ] "
\item " [ math tex define var v2 as "(v2)" end define end math ] "
\item " [ math tex define var v3 as "(v3)" end define end math ] "
\item " [ math tex define var v4 as "(v4)" end define end math ] "
\item " [ math tex define var v2n as "(v2n)" end define end math ] "
\item " [ math tex define var n1 as "(n1)" end define end math ] "
\item " [ math tex define var n2 as "(n2)" end define end math ] "
\item " [ math tex define var n3 as "(n3)" end define end math ] "
\item " [ math tex define var m1 as "(m1)" end define end math ] "
\item " [ math tex define var m2 as "(m2)" end define end math ] "
\item " [ math tex define var ep as "(\epsilon)" end define end math ] "
\item " [ math tex define var ep1 as "(\epsilon)_{1}" end define end math ] "
\item " [ math tex define var ep2 as "(\epsilon 2)" end define end math ] "
\item " [ math tex define var fx as "(fx)" end define end math ] "
\item " [ math tex define var fy as "(fy)" end define end math ] "
\item " [ math tex define var fz as "(fz)" end define end math ] "
\item " [ math tex define var fu as "(fu)" end define end math ] "
\item " [ math tex define var fv as "(fv)" end define end math ] "
\item " [ math tex define var fw as "(fw)" end define end math ] "
\item " [ math tex define var fep as "(fep)" end define end math ] "
\item " [ math tex define var rx as "(rx)" end define end math ] "
\item " [ math tex define var ry as "(ry)" end define end math ] "
\item " [ math tex define var rz as "(rz)" end define end math ] "
\item " [ math tex define var ru as "(ru)" end define end math ] "
\item " [ math tex define var sx as "(sx)" end define end math ] "
\item " [ math tex define var sx1 as "(sx1)" end define end math ] "
\item " [ math tex define var sy as "(sy)" end define end math ] "
\item " [ math tex define var sy1 as "(sy1)" end define end math ] "
\item " [ math tex define var sz as "(sz)" end define end math ] "
\item " [ math tex define var sz1 as "(sz1)" end define end math ] "
\item " [ math tex define var su as "(su)" end define end math ] "
\item " [ math tex define var su1 as "(su1)" end define end math ] "
\item " [ math tex define var fxs as "(fxs)" end define end math ] "
\item " [ math tex define var fys as "(fys)" end define end math ] "
\item " [ math tex define var crs1 as "(crs1)" end define end math ] "
\item " [ math tex define var f1 as "(f1)" end define end math ] "
\item " [ math tex define var f2 as "(f2)" end define end math ] "
\item " [ math tex define var f3 as "(f3)" end define end math ] "
\item " [ math tex define var f4 as "(f4)" end define end math ] "
\item " [ math tex define var op1 as "(op1)" end define end math ] "
\item " [ math tex define var op2 as "(op2)" end define end math ] "
\item " [ math tex define var r1 as "(r1)" end define end math ] "
\item " [ math tex define var s1 as "(s1)" end define end math ] "
\item " [ math tex define var s2 as "(s2)" end define end math ] "
\item " [ math tex define meta x1 as "X_{1}" end define end math ] "
\item " [ math tex define meta x2 as "X_{2}" end define end math ] "
\item " [ math tex define meta y1 as "Y_{1}" end define end math ] "
\item " [ math tex define meta y2 as "Y_{2}" end define end math ] "
\item " [ math tex define meta v1 as "V_{1}" end define end math ] "
\item " [ math tex define meta v2 as "V_{2}" end define end math ] "
\item " [ math tex define meta v3 as "V_{3}" end define end math ] "
\item " [ math tex define meta v4 as "V_{4}" end define end math ] "
\item " [ math tex define meta v2n as "V_{2n}" end define end math ] "
\item " [ math tex define meta ep as "\epsilon" end define end math ] "
\item " [ math tex define meta m1 as "M_{1}" end define end math ] "
\item " [ math tex define meta m2 as "M_{2}" end define end math ] "
\item " [ math tex define meta n1 as "N_{1} " end define end math ] "
\item " [ math tex define meta n2 as "N_{2} " end define end math ] "
\item " [ math tex define meta n3 as "N_{3} " end define end math ] "
\item " [ math tex define meta ep1 as "\epsilon 1" end define end math ] "
\item " [ math tex define meta ep2 as "\epsilon 2" end define end math ] "
\item " [ math tex define meta fx as "FX" end define end math ] "
\item " [ math tex define meta fy as "FY" end define end math ] "
\item " [ math tex define meta fz as "FZ" end define end math ] "
\item " [ math tex define meta fu as "FU" end define end math ] "
\item " [ math tex define meta fv as "FV" end define end math ] "
\item " [ math tex define meta fw as "FW" end define end math ] "
\item " [ math tex define meta fep as "FEP" end define end math ] "
\item " [ math tex define meta rx as "RX" end define end math ] "
\item " [ math tex define meta ry as "RY" end define end math ] "
\item " [ math tex define meta rz as "RZ" end define end math ] "
\item " [ math tex define meta ru as "RU" end define end math ] "
\item " [ math tex define meta sx as "(SX)" end define end math ] "
\item " [ math tex define meta sx1 as "(SX1)" end define end math ] "
\item " [ math tex define meta sy as "(SY)" end define end math ] "
\item " [ math tex define meta sy1 as "(SY1)" end define end math ] "
\item " [ math tex define meta sz as "(SZ)" end define end math ] "
\item " [ math tex define meta sz1 as "(SZ1)" end define end math ] "
\item " [ math tex define meta su as "(SU)" end define end math ] "
\item " [ math tex define meta su1 as "(SU1)" end define end math ] "
\item " [ math tex define meta fxs as "FXS" end define end math ] "
\item " [ math tex define meta fys as "FYS" end define end math ] "
\item " [ math tex define meta f1 as "(F1)" end define end math ] "
\item " [ math tex define meta f2 as "(F2)" end define end math ] "
\item " [ math tex define meta f3 as "(F3)" end define end math ] "
\item " [ math tex define meta f4 as "(F4)" end define end math ] "
\item " [ math tex define meta op1 as "(OP1)" end define end math ] "
\item " [ math tex define meta op2 as "(OP2)" end define end math ] "
\item " [ math tex define meta r1 as "(R1)" end define end math ] "
\item " [ math tex define meta s1 as "(S1)" end define end math ] "
\item " [ math tex define meta s2 as "(S2)" end define end math ] "
\item " [ math tex define object ep as "(EPob)" end define end math ] "
\item " [ math tex define object crs1 as "(CRS1ob)" end define end math ] "
\item " [ math tex define object f1 as "(F1ob)" end define end math ] "
\item " [ math tex define object f2 as "(F2ob)" end define end math ] "
\item " [ math tex define object f3 as "(F3ob)" end define end math ] "
\item " [ math tex define object f4 as "(F4ob)" end define end math ] "
\item " [ math tex define object n1 as "(N1ob)" end define end math ] "
\item " [ math tex define object n2 as "(N2ob)" end define end math ] "
\item " [ math tex define object op1 as "(OP1ob)" end define end math ] "
\item " [ math tex define object op2 as "(OP2ob)" end define end math ] "
\item " [ math tex define object r1 as "(R1ob)" end define end math ] "
\item " [ math tex define object s1 as "(S1ob)" end define end math ] "
\item " [ math tex define object s2 as "(S2ob)" end define end math ] "
\item " [ math tex define ex3 as "Ex3" end define end math ] "
\item " [ math tex define NAT as "NAT" end define end math ] "
\item " [ math tex define RATIONAL_SERIES as "RATIONAL_SERIES" end define end math ] "
\item " [ math tex define SERIES as "SERIES" end define end math ] "
\item " [ math tex define setOfReals as "SetOfReals" end define end math ] "
\item " [ math tex define setOfFxs as "SetOfFxs" end define end math ] "
\item " [ math tex define N as "N" end define end math ] "
\item " [ math tex define Q as "Q" end define end math ] "
\item " [ math tex define X as "X" end define end math ] "
\item " [ math tex define xs as "xs" end define end math ] "
\item " [ math tex define xsF as "xaF" end define end math ] "
\item " [ math tex define ysF as "ysF" end define end math ] "
\item " [ math tex define us as "us" end define end math ] "
\item " [ math tex define usF as "usFoelge" end define end math ] "
\item " [ math tex define 0 as "0" end define end math ] "
\item " [ math tex define 1 as "1" end define end math ] "
\item " [ math tex define (-1) as "(-1)" end define end math ] "
\item " [ math tex define 2 as "2" end define end math ] "
\item " [ math tex define 3 as "3" end define end math ] "
\item " [ math tex define 1/2 as "1/2" end define end math ] "
\item " [ math tex define 1/3 as "1/3" end define end math ] "
\item " [ math tex define 2/3 as "2/3" end define end math ] "
\item " [ math tex define 0f as "0f" end define end math ] "
\item " [ math tex define 00 as "00" end define end math ] "
\item " [ math tex define (--01) as "(--01)" end define end math ] "
\item " [ math tex define 02 as "02" end define end math ] "
\item " [ math tex define 01//02 as "01//02" end define end math ] "
\item " [ math tex define var x = var y as "#1.
= #2." end define end math ] "
\item " [ math tex define var x != var y as "#1.
\neq #2." end define end math ] "
\item " [ math tex define var x < var y as "#1.
< #2." end define end math ] "
\item " [ math tex define var x <= var y as "#1.
<= #2." end define end math ] "
\item " [ math tex define var x
\item " [ math tex define var x <=f var y as "#1.
\leq_{f}#2." end define end math ] "
\item " [ math tex define var x sameF var y as "SF(#1.
,#2.
)" end define end math ] "
\item " [ math tex define var x == var y as "#1.
== #2." end define end math ] "
\item " [ math tex define var x !!== var y as "#1.
!!== #2." end define end math ] "
\item " [ math tex define var x << var y as "#1.
<< #2." end define end math ] "
\item " [ math tex define var x <<== var y as "#1.
<<== #2." end define end math ] "
\item " [ math tex define [ var x ; var y ] as "#1.
[#2.
]" end define end math ] "
\item " [ math tex define - var x as "(-u#1.
)" end define end math ] "
\item " [ math tex define -f var x as "-_{f}#1." end define end math ] "
\item " [ math tex define -- var x as "(--#1.
)" end define end math ] "
\item " [ math tex define 1f/ var x as "1f/#1." end define end math ] "
\item " [ math tex define 01// var x as "01//temp#1." end define end math ] "
\item " [ math tex define var x + var y as "(#1.
+#2.
)" end define end math ] "
\item " [ math tex define var x - var y as "(#1.
-#2.
)" end define end math ] "
\item " [ math tex define var fx +f var fy as "#1.
+_{f}#2." end define end math ] "
\item " [ math tex define var fx -f var fy as "#1.
-_{f}#2." end define end math ] "
\item " [ math tex define var fx *f var fy as "#1.
*_{f}#2." end define end math ] "
\item " [ math tex define var x ++ var y as "#1.
++#2." end define end math ] "
\item " [ math tex define R( var fx ) -- R( var fy ) as "R(#1.
) -- R(#2.
)" end define end math ] "
\item " [ math tex define var x * var y as "(#1.
*#2.
)" end define end math ] "
\item " [ math tex define var x ** var y as "#1.
**#2." end define end math ] "
\item " [ math tex define var x ^ var y as " #1.
(exp) #2." end define end math ] "
\item " [ math tex define axiom leqReflexivity as "leqReflexivity" end define end math ] "
\item " [ math tex define 1/ var x as "rec#1." end define end math ] "
\item " [ math tex define | var x | as "|#1.
|" end define end math ] "
\item " [ math tex define stateExpand( var t , var s , var c ) as "StateExpand(#1.
,#2.
,#3.
)" end define end math ] "
\item " [ math tex define extractSeries( var t ) as "extractSeries(#1.
)" end define end math ] "
\item " [ math tex define |f var x | as "|f#1.
|" end define end math ] "
\item " [ math tex define |r var x | as "|r#1.
|" end define end math ] "
\item " [ math tex define setOfSeries( var x ) as "SetOfSeries(#1.
)" end define end math ] "
\item " [ math tex define expandList( var x , var y , var z ) as "ExpandList(#1.
,#2.
,#3.
)" end define end math ] "
\item " [ math tex define **Macro( var x ) as "**Macro(#1.
)" end define end math ] "
\item " [ math tex define ++Macro( var x ) as "++Macro(#1.
)" end define end math ] "
\item " [ math tex define --Macro( var x ) as "--Macro(#1.
)" end define end math ] "
\item " [ math tex define <
\item " [ math tex define ||Macro( var x ) as "||Macro(#1.
)" end define end math ] "
\item " [ math tex define 01//Macro( var x ) as "01//Macro(#1.
)" end define end math ] "
\item " [ math tex define max( var x , var y ) as "Max(#1.
,#2.
)" end define end math ] "
\item " [ math tex define maxR( var x , var y ) as "Max(#1.
,#2.
)" end define end math ] "
\item " [ math tex define limit( var x , var y ) as "Limit(#1.
,#2.
)" end define end math ] "
\item " [ math tex define U( var x ) as "Union(#1.
)" end define end math ] "
\item " [ math tex define if( var x , var y , var z ) as "if(#1.
,#2.
,#3.
)" end define end math ] "
\item " [ math tex define isOrderedPair( var x , var y , var z ) as "IsOrderedPair(#1.
,#2.
,#3.
)" end define end math ] "
\item " [ math tex define isRelation( var x , var y , var z ) as "IsRelation(#1.
,#2.
,#3.
)" end define end math ] "
\item " [ math tex define isFunction( var x , var y , var z ) as "isFunction(#1.
,#2.
,#3.
)" end define end math ] "
\item " [ math tex define typeNat( var x ) as "TypeNat(#1.
)" end define end math ] "
\item " [ math tex define typeNat0( var x ) as "TypeNat0(#1.
)" end define end math ] "
\item " [ math tex define typeRational( var x ) as "TypeRational(#1.
)" end define end math ] "
\item " [ math tex define typeRational0( var x ) as "TypeRational0(#1.
)" end define end math ] "
\item " [ math tex define typeSeries( var x , var y ) as "TypeSeries(#1.
,#2.
)" end define end math ] "
\item " [ math tex define typeSeries0( var x , var y ) as "Typeseries0(#1.
,#2.
)" end define end math ] "
\item " [ math tex define upperBound( var x , var y ) as "UB(#1.
, #2.
)" end define end math ] "
\item " [ math tex define leastUpperBound( var x , var y ) as "LUB(#1.
, #2.
)" end define end math ] "
\item " [ math tex define base(1/2)Sum( var x , var y ) as "BS(#1.
,#2.
)" end define end math ] "
\item " [ math tex define UStelescope( var x , var y ) as "UStelescope(#1.
,#2.
)" end define end math ] "
\item " [ math tex define ( var x ) as "(#1.
)" end define end math ] "
\item " [ math tex define R( var x ) as "R(#1.
)" end define end math ] "
\item " [ math tex define --R( var x ) as "--R(#1.
)" end define end math ] "
\item " [ math tex define isSeries( var x , var y ) as "IsSeries(#1.
,#2.
)" end define end math ] "
\item " [ math tex define isNatural( var x , var y ) as "IsNatural(#1.
,#2.
)" end define end math ] "
\item " [ math tex define (o var x , var y ) as "OrderedPair(#1.
,#2.
)" end define end math ] "
\item " [ math tex define axiom leqAntisymmetry as "leqAntisymmetryAxiom" end define end math ] "
\item " [ math tex define axiom leqTransitivity as "leqTransitivityAxiom" end define end math ] "
\item " [ math tex define axiom leqTotality as "leqTotality" end define end math ] "
\item " [ math tex define axiom leqAddition as "leqAdditionAxiom" end define end math ] "
\item " [ math tex define axiom leqMultiplication as "leqMultiplicationAxiom" end define end math ] "
\item " [ math tex define axiom plusAssociativity as "plusAssociativity" end define end math ] "
\item " [ math tex define axiom plusCommutativity as "plusCommutativity" end define end math ] "
\item " [ math tex define axiom negative as "Negative" end define end math ] "
\item " [ math tex define axiom plus0 as "plus0" end define end math ] "
\item " [ math tex define axiom timesAssociativity as "timesAssociativity" end define end math ] "
\item " [ math tex define axiom timesCommutativity as "timesCommutativity" end define end math ] "
\item " [ math tex define axiom reciprocal as "ReciprocalAxiom" end define end math ] "
\item " [ math tex define axiom times1 as "times1" end define end math ] "
\item " [ math tex define axiom plusAssociativity as "plusAssociativity" end define end math ] "
\item " [ math tex define axiom plusCommutativity as "plusCommutativity" end define end math ] "
\item " [ math tex define axiom negative as "Negative" end define end math ] "
\item " [ math tex define axiom distribution as "Distribution" end define end math ] "
\item " [ math tex define axiom 0not1 as "0not1" end define end math ] "
\item " [ math tex define axiom a4 as "A4(Axiom)" end define end math ] "
\item " [ math tex define axiom induction as "InductionAxiom" end define end math ] "
\item " [ math tex define axiom equality as "EqualityAxiom" end define end math ] "
\item " [ math tex define axiom eqLeq as "EqLeqAxiom" end define end math ] "
\item " [ math tex define axiom eqAddition as "EqAdditionAxiom" end define end math ] "
\item " [ math tex define axiom eqMultiplication as "EqMultiplicationAxiom" end define end math ] "
\item " [ math tex define lemma set equality nec condition(1) as "SENC1" end define end math ] "
\item " [ math tex define lemma set equality nec condition(2) as "SENC2" end define end math ] "
\item " [ math tex define axiom cauchy as "Cauchy" end define end math ] "
\item " [ math tex define axiom plusF as "PlusF" end define end math ] "
\item " [ math tex define axiom reciprocalF as "ReciprocalF" end define end math ] "
\item " [ math tex define 1rule from== as "From==" end define end math ] "
\item " [ math tex define 1rule to== as "To==" end define end math ] "
\item " [ math tex define 1rule fromInR as "FromInR" end define end math ] "
\item " [ math tex define axiom reciprocalR as "ReciprocalR(Axiom)" end define end math ] "
\item " [ math tex define axiom US0 as "US0" end define end math ] "
\item " [ math tex define 1rule nextXS(upperBound) as "NextXS(UpperBound)" end define end math ] "
\item " [ math tex define 1rule nextXS(noUpperBound) as "NextXS(NoUpperBound)" end define end math ] "
\item " [ math tex define 1rule nextUS(upperBound) as "NextUS(UpperBound)" end define end math ] "
\item " [ math tex define 1rule nextUS(noUpperBound) as "NextUS(NoUpperBound)" end define end math ] "
\item " [ math tex define 1rule expZero as "ExpZero" end define end math ] "
\item " [ math tex define 1rule expPositive as "ExpPositive" end define end math ] "
\item " [ math tex define 1rule expZero(R) as "ExpZero(R)" end define end math ] "
\item " [ math tex define 1rule expPositive(R) as "ExpPositive(R)" end define end math ] "
\item " [ math tex define 1rule lessMinus1(N) as "LessMinus1(N)" end define end math ] "
\item " [ math tex define axiom nonnegative(N) as "Nonnegative(N)" end define end math ] "
\item " [ math tex define 1rule base(1/2)Sum zero as "BSzero" end define end math ] "
\item " [ math tex define 1rule base(1/2)Sum positive as "BSpositive" end define end math ] "
\item " [ math tex define 1rule UStelescope zero as "UStelescope(Zero)" end define end math ] "
\item " [ math tex define 1rule UStelescope positive as "UStelescope(Positive)" end define end math ] "
\item " [ math tex define 1rule adhoc eqAddition(R) as "EqAddition(R)" end define end math ] "
\item " [ math tex define 1rule fromLimit as "FromLimit" end define end math ] "
\item " [ math tex define 1rule toUpperBound as "ToUpperBound" end define end math ] "
\item " [ math tex define 1rule fromUpperBound as "FromUpperBound" end define end math ] "
\item " [ math tex define axiom USisUpperBound as "USisUpperBound" end define end math ] "
\item " [ math tex define axiom 0not1(R) as "0not1(R)" end define end math ] "
\item " [ math tex define 1rule expUnbounded as "ExpUnbounded(R)" end define end math ] "
\item " [ math tex define 1rule fromLeq(Advanced)(N) as "FromLeq(Advanced)(N)" end define end math ] "
\item " [ math tex define 1rule fromLeastUpperBound as "FromLeastUpperBound" end define end math ] "
\item " [ math tex define 1rule toLeastUpperBound as "ToLeastUpperBound" end define end math ] "
\item " [ math tex define axiom XSisNotUpperBound as "XSisNotUpperBound" end define end math ] "
\item " [ math tex define axiom ysFGreater as "ysFGreater" end define end math ] "
\item " [ math tex define axiom ysFLess as "ysFLess" end define end math ] "
\item " [ math tex define 1rule smallInverse as "SmallInverse" end define end math ] "
\item " [ math tex define axiom memberOfSeries as "MemberOfSeries(Imply)" end define end math ] "
\item " [ math tex define axiom natType as "NatType" end define end math ] "
\item " [ math tex define axiom rationalType as "RationalType" end define end math ] "
\item " [ math tex define axiom seriesType as "SeriesType" end define end math ] "
\item " [ math tex define prop lemma doubly conditioned join conjuncts as "JoinConjuncts(2conditions)" end define end math ] "
\item " [ math tex define prop lemma tertium non datur as "TND" end define end math ] "
\item " [ math tex define prop lemma from negated imply as "FromNegatedImply" end define end math ] "
\item " [ math tex define prop lemma to negated imply as "ToNegatedImply" end define end math ] "
\item " [ math tex define prop lemma from negated double imply as "FromNegated(2*Imply)" end define end math ] "
\item " [ math tex define prop lemma from negated and as "FromNegatedAnd" end define end math ] "
\item " [ math tex define prop lemma from negated or as "FromNegatedOr" end define end math ] "
\item " [ math tex define prop lemma to negated or as "ToNegatedOr" end define end math ] "
\item " [ math tex define prop lemma from negations as "FromNegations" end define end math ] "
\item " [ math tex define prop lemma from three disjuncts as "From3Disjuncts" end define end math ] "
\item " [ math tex define prop lemma negate first disjunct as "NegateDisjunct1" end define end math ] "
\item " [ math tex define prop lemma negate second disjunct as "NegateDisjunct2" end define end math ] "
\item " [ math tex define prop lemma expand disjuncts as "ExpandDisjuncts" end define end math ] "
\item " [ math tex define prop lemma from two times two disjuncts as "From2*2Disjuncts" end define end math ] "
\item " [ math tex define lemma plusR(Sym) as "PlusR(Sym)" end define end math ] "
\item " [ math tex define lemma lessLeq(R) as "LessLeq(R)" end define end math ] "
\item " [ math tex define lemma leqAntisymmetry(R) as "LeqAntisymmetry(R)" end define end math ] "
\item " [ math tex define lemma leqTransitivity(R) as "LeqTransitivity(R)" end define end math ] "
\item " [ math tex define lemma plus0(R) as "Plus0(R)" end define end math ] "
\item " [ math tex define lemma lessAddition(R) as "lessAddition(R)" end define end math ] "
\item " [ math tex define lemma leqAddition(R) as "leqAddition(R)" end define end math ] "
\item " [ math tex define lemma plusAssociativity(R)XX as "PlusAssociativity(R)XX" end define end math ] "
\item " [ math tex define lemma plusAssociativity(R) as "PlusAssociativity(R)" end define end math ] "
\item " [ math tex define lemma negative(R) as "Negative(R)" end define end math ] "
\item " [ math tex define lemma plusCommutativity(R) as "PlusCommutativity(R)" end define end math ] "
\item " [ math tex define lemma times1(R) as "Times1(R)" end define end math ] "
\item " [ math tex define lemma timesAssociativity(R) as "TimesAssociativity(R)" end define end math ] "
\item " [ math tex define lemma timesCommutativity(R) as "TimesCommutativity(R)" end define end math ] "
\item " [ math tex define lemma distribution(R) as "Distribution(R)" end define end math ] "
\item " [ math tex define exist var x indeed var y as "(AARRGGHH!-exist-bug!)" end define end math ] "
\item " [ math tex define constantRationalSeries( var x ) as "constantRationalSeries(#1.
)" end define end math ] "
\item " [ math tex define P( var x ) as "Power(#1.
)" end define end math ] "
\item " [ math tex define cartProd( var x , var y ) as "cartProd(#1.
)" end define end math ] "
\item " [ math tex define binaryUnion( var x , var y ) as "binaryUnion(#1.
,#2.
)" end define end math ] "
\item " [ math tex define setOfRationalSeries as "SetOfRationalSeries" end define end math ] "
\item " [ math tex define lemma memberOfSeries as "MemberOfSeries" end define end math ] "
\item " [ math tex define isSubset( var x , var y ) as "IsSubset(#1.
,#2.
)" end define end math ] "
\item " [ math tex define lemma memberOfSeries(Type) as "memberOfSeries(Type)" end define end math ] "
\item " [ math tex define lemma uniqueMember as "UniqueMember" end define end math ] "
\item " [ math tex define lemma uniqueMember(Type) as "UniqueMember(Type)" end define end math ] "
\item " [ math tex define lemma sameSeries as "SameSeries" end define end math ] "
\item " [ math tex define lemma a4 as "A4" end define end math ] "
\item " [ math tex define (s var x ) as "(s#1.
)" end define end math ] "
\item " [ math tex define (p var x , var y ) as "(p#1.
,#2.
)" end define end math ] "
\item " [ math tex define lemma sameMember as "SameMember" end define end math ] "
\item " [ math tex define 1rule Qclosed(Addition) as "Qclosed(Addition)" end define end math ] "
\item " [ math tex define 1rule Qclosed(Multiplication) as "Qclosed(Multiplication)" end define end math ] "
\item " [ math tex define 1rule fromCartProd(1) as "FromCartProd(1)" end define end math ] "
\item " [ math tex define 1rule fromCartProd(1) as "FromCartProd(1)" end define end math ] "
\item " [ math tex define axiom max as "Max" end define end math ] "
\item " [ math tex define axiom numerical as "Numerical" end define end math ] "
\item " [ math tex define axiom numericalF as "NumericalF" end define end math ] "
\item " [ math tex define lemma separation2formula(1) as "Separation2formula(1)" end define end math ] "
\item " [ math tex define lemma separation2formula(2) as "Separation2formula(2)" end define end math ] "
\item " [ math tex define axiom QisClosed(reciprocal) as "QisClosed(Reciprocal)(Imply)" end define end math ] "
\item " [ math tex define lemma QisClosed(reciprocal) as "QisClosed(Reciprocal)" end define end math ] "
\item " [ math tex define axiom QisClosed(negative) as "QisClosed(Negative)(Imply)" end define end math ] "
\item " [ math tex define lemma QisClosed(negative) as "QisClosed(Negative)" end define end math ] "
\item " [ math tex define 1rule adhoc sameR as "(Adgic)SameR" end define end math ] "
\end{list}
\end{document}
End of file
latex page
latex page
dvipdfm page"
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,