"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 ] "
SUPSUPSUPSUPSUPSUPSUPSUPSUPSUPSUPSUPSUPSUPSUP
" [ math in theory system Q lemma prop lemma to negated double imply says for all terms meta a comma meta b comma meta c indeed meta a infer meta b infer not0 meta c infer not0 ( meta a imply meta b imply meta c ) end lemma end math ] "
" [ math system Q proof of prop lemma to negated double imply reads block any term meta a comma meta b comma meta c end line line ell a premise meta a end line line ell b premise meta b end line line ell c premise not0 meta c end line line ell d premise meta a imply meta b imply meta c end line line ell e because prop lemma mp2 modus ponens ell d modus ponens ell a modus ponens ell b indeed meta c end line because prop lemma from contradiction modus ponens ell e modus ponens ell c indeed not0 ( meta a imply meta b imply meta c ) end line line ell big a end block any term meta a comma meta b comma meta c end line line ell a because 1rule deduction modus ponens ell big a indeed meta a imply meta b imply not0 meta c imply ( meta a imply meta b imply meta c ) imply not0 ( meta a imply meta b imply meta c ) end line line ell b premise meta a end line line ell c premise meta b end line line ell d premise not0 meta c end line line ell e because prop lemma mp3 modus ponens ell a modus ponens ell b modus ponens ell c modus ponens ell d indeed ( meta a imply meta b imply meta c ) imply not0 ( meta a imply meta b imply meta c ) end line because prop lemma imply negation modus ponens ell e indeed not0 ( meta a imply meta b imply meta c ) qed end math ] "
" [ math in theory system Q lemma prop lemma from negated and (imply) says for all terms meta a comma meta b indeed not0 ( meta a and0 meta b ) imply meta a imply not0 meta b end lemma end math ] "
" [ math system Q proof of prop lemma from negated and (imply) reads block any term meta a comma meta b end line line ell a premise not0 ( meta a and0 meta b ) end line line ell b premise meta a end line because prop lemma from negated and modus ponens ell a modus ponens ell b indeed not0 meta b end line line ell big a end block any term meta a comma meta b end line because 1rule deduction modus ponens ell big a indeed not0 ( meta a and0 meta b ) imply meta a imply not0 meta b qed end math ] "
" [ math in theory system Q lemma prop lemma remove double neg (consequent) says for all terms meta a comma meta b indeed meta a imply not0 not0 meta b infer meta a imply meta b end lemma end math ] "
" [ math system Q proof of prop lemma remove double neg (consequent) 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 ( meta a imply not0 not0 meta b ) imply meta a imply meta b end line line ell b premise meta a imply not0 not0 meta b end line because 1rule mp modus ponens ell a modus ponens ell b indeed meta a imply meta b qed end math ] "
" [ math in theory system Q lemma pred lemma (A)to(~E~)(Imply) says for all terms meta v1 comma meta a indeed for all meta v1 indeed meta a imply not0 exist0 meta v1 indeed not0 meta a end lemma end math ] "
" [ math system Q proof of pred lemma (A)to(~E~)(Imply) reads block any term meta v1 comma meta a end line line ell a premise for all meta v1 indeed meta a end line line ell b because lemma a4 at meta v1 modus ponens ell a indeed meta a end line line ell c because prop lemma add double neg modus ponens ell b indeed not0 not0 meta a end line line ell d because 1rule gen modus ponens ell c indeed for all meta v1 indeed not0 not0 meta a end line line ell e because prop lemma add double neg modus ponens ell d indeed not0 not0 for all meta v1 indeed not0 not0 meta a end line because 1rule repetition modus ponens ell e indeed not0 exist0 meta v1 indeed not0 meta a end line line ell big a end block any term meta v1 comma meta a end line because 1rule deduction modus ponens ell big a indeed for all meta v1 indeed meta a imply not0 exist0 meta v1 indeed not0 meta a qed end math ] "
" [ math in theory system Q lemma pred lemma (E)to(~A~)(Imply) says for all terms meta v1 comma meta a indeed exist0 meta v1 indeed meta a imply not0 for all meta v1 indeed not0 meta a end lemma end math ] "
" [ math system Q proof of pred lemma (E)to(~A~)(Imply) reads any term meta v1 comma meta a end line line ell a because prop lemma auto imply indeed not0 for all meta v1 indeed not0 meta a imply not0 for all meta v1 indeed not0 meta a end line because 1rule repetition modus ponens ell a indeed exist0 meta v1 indeed meta a imply not0 for all meta v1 indeed not0 meta a qed end math ] "
" [ math in theory system Q lemma pred lemma (E~)to(~A)(Imply) says for all terms meta v1 comma meta a indeed exist0 meta v1 indeed not0 meta a imply not0 for all meta v1 indeed meta a end lemma end math ] "
" [ math system Q proof of pred lemma (E~)to(~A)(Imply) reads block any term meta v1 comma meta a end line line ell a premise exist0 meta v1 indeed not0 meta a end line line ell b because prop lemma add double neg modus ponens ell a indeed not0 not0 exist0 meta v1 indeed not0 meta a end line line ell c because pred lemma (A)to(~E~)(Imply) indeed for all meta v1 indeed meta a imply not0 exist0 meta v1 indeed not0 meta a end line because prop lemma mt modus ponens ell c modus ponens ell b indeed not0 for all meta v1 indeed meta a end line line ell big a end block any term meta v1 comma meta a end line because 1rule deduction modus ponens ell big a indeed exist0 meta v1 indeed not0 meta a imply not0 for all meta v1 indeed meta a qed end math ] "
" [ math in theory system Q lemma pred lemma addNegatedAll says for all terms meta v1 comma meta a comma meta b indeed meta b imply meta a infer not0 for all meta v1 indeed meta a imply not0 for all meta v1 indeed meta b end lemma end math ] "
" [ math system Q proof of pred lemma addNegatedAll reads any term meta v1 comma meta a comma meta b end line line ell a premise meta b imply meta a end line line ell b because pred lemma addAll modus ponens ell a indeed for all meta v1 indeed meta b imply for all meta v1 indeed meta a end line because prop lemma contrapositive modus ponens ell b indeed not0 for all meta v1 indeed meta a imply not0 for all meta v1 indeed meta b qed end math ] "
" [ math in theory system Q lemma pred lemma toNegatedAEA says for all terms meta v1 comma meta v2 comma meta v3 comma meta a indeed exist0 meta v1 indeed for all meta v2 indeed exist0 meta v3 indeed not0 meta a infer not0 for all meta v1 indeed exist0 meta v2 indeed for all meta v3 indeed meta a end lemma end math ] "
" [ math system Q proof of pred lemma toNegatedAEA reads any term meta v1 comma meta v2 comma meta v3 comma meta a end line line ell big a premise exist0 meta v1 indeed for all meta v2 indeed exist0 meta v3 indeed not0 meta a end line line ell a because pred lemma (E~)to(~A)(Imply) indeed exist0 meta v3 indeed not0 meta a imply not0 for all meta v3 indeed meta a end line line ell b because pred lemma addNegatedAll modus ponens ell a indeed not0 for all meta v2 indeed not0 for all meta v3 indeed meta a imply not0 for all meta v2 indeed exist0 meta v3 indeed not0 meta a end line line ell c because pred lemma (E)to(~A~)(Imply) indeed exist0 meta v2 indeed for all meta v3 indeed meta a imply not0 for all meta v2 indeed not0 for all meta v3 indeed meta a end line line ell d because prop lemma imply transitivity modus ponens ell c modus ponens ell b indeed exist0 meta v2 indeed for all meta v3 indeed meta a imply not0 for all meta v2 indeed exist0 meta v3 indeed not0 meta a end line line ell e because pred lemma addNegatedAll modus ponens ell d indeed not0 for all meta v1 indeed not0 for all meta v2 indeed exist0 meta v3 indeed not0 meta a imply not0 for all meta v1 indeed exist0 meta v2 indeed for all meta v3 indeed meta a end line line ell f because pred lemma (E)to(~A~)(Imply) indeed exist0 meta v1 indeed for all meta v2 indeed exist0 meta v3 indeed not0 meta a imply not0 for all meta v1 indeed not0 for all meta v2 indeed exist0 meta v3 indeed not0 meta a end line line ell g because prop lemma imply transitivity modus ponens ell f modus ponens ell e indeed exist0 meta v1 indeed for all meta v2 indeed exist0 meta v3 indeed not0 meta a imply not0 for all meta v1 indeed exist0 meta v2 indeed for all meta v3 indeed meta a end line because 1rule mp modus ponens ell g modus ponens ell big a indeed not0 for all meta v1 indeed exist0 meta v2 indeed for all meta v3 indeed meta a qed end math ] "
" [ math in theory system Q lemma pred lemma (A~)to(~E) says for all terms meta v1 comma meta a indeed for all meta v1 indeed not0 meta a infer not0 exist0 meta v1 indeed meta a end lemma end math ] "
" [ math system Q proof of pred lemma (A~)to(~E) reads any term meta v1 comma meta a end line line ell a premise for all meta v1 indeed not0 meta a end line line ell b because prop lemma add double neg modus ponens ell a indeed not0 not0 for all meta v1 indeed not0 meta a end line because 1rule repetition modus ponens ell b indeed not0 exist0 meta v1 indeed meta a qed end math ] "
" [ math in theory system Q lemma pred lemma exist mp3 says for all terms meta v1 comma meta v2 comma meta v3 comma meta a comma meta b comma meta c comma meta d indeed meta a imply meta b imply meta c imply meta d infer exist0 meta v1 indeed meta a infer exist0 meta v2 indeed meta b infer exist0 meta v3 indeed meta c infer meta d end lemma end math ] "
" [ math system Q proof of pred lemma exist mp3 reads any term meta v1 comma meta v2 comma meta v3 comma 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 imply meta d end line line ell b premise exist0 meta v1 indeed meta a end line line ell c premise exist0 meta v2 indeed meta b end line line ell d premise exist0 meta v3 indeed meta c end line line ell e because pred lemma exist mp2 modus ponens ell a modus ponens ell b modus ponens ell c indeed meta c imply meta d end line because pred lemma exist mp modus ponens ell e modus ponens ell d indeed meta d qed end math ] "
" [ math in theory system Q lemma lemma positiveToLeft(Eq) says for all terms meta x comma meta y comma meta z indeed meta x = meta y + meta z infer meta x - meta z = meta y end lemma end math ] "
" [ math system Q proof of lemma positiveToLeft(Eq) reads any term meta x comma meta y comma meta z end line line ell a premise meta x = meta y + meta z end line line ell b because lemma eqAddition modus ponens ell a indeed meta x - meta z = meta y + meta z - meta z end line line ell c because lemma x=x+y-y indeed meta y = meta y + meta z - meta z end line line ell d because lemma eqSymmetry modus ponens ell c indeed meta y + meta z - meta z = meta y end line because lemma eqTransitivity modus ponens ell b modus ponens ell d indeed meta x - meta z = meta y qed end math ] "
--------
" [ math in theory system Q lemma lemma expZero exact says for all terms meta x indeed meta x ^ 0 = 1 end lemma end math ] "
" [ math system Q proof of lemma expZero exact reads any term meta x end line line ell a because lemma eqReflexivity indeed 0 = 0 end line because 1rule expZero modus ponens ell a indeed meta x ^ 0 = 1 qed end math ] "
" [ math in theory system Q lemma lemma +1IsPositive(N) says for all terms meta m indeed Nat( meta m ) endorse 0 < meta m + 1 end lemma end math ] "
" [ math system Q proof of lemma +1IsPositive(N) reads any term meta m end line line ell a side condition Nat( meta m ) end line line ell b because axiom nonnegative(N) modus probans ell a indeed 0 <= meta m end line because lemma leqPlus1 modus ponens ell b indeed 0 < meta m + 1 qed end math ] "
" [ math in theory system Q lemma lemma sameExp base says for all terms meta n comma meta x indeed for all meta n indeed parenthesis 0 = meta n imply meta x ^ 0 = meta x ^ meta n end parenthesis end lemma end math ] "
" [ math system Q proof of lemma sameExp base reads block any term meta n comma meta x end line line ell a premise 0 = meta n end line line ell b because lemma expZero exact indeed meta x ^ 0 = 1 end line line ell c because lemma eqSymmetry modus ponens ell a indeed meta n = 0 end line line ell d because 1rule expZero modus ponens ell c indeed meta x ^ meta n = 1 end line line ell e because lemma eqSymmetry modus ponens ell d indeed 1 = meta x ^ meta n end line because lemma eqTransitivity modus ponens ell b modus ponens ell e indeed meta x ^ 0 = meta x ^ meta n end line line ell big a end block any term meta n comma meta x end line line ell a because 1rule deduction modus ponens ell big a indeed 0 = meta n imply meta x ^ 0 = meta x ^ meta n end line because 1rule gen modus ponens ell a indeed for all meta n indeed parenthesis 0 = meta n imply meta x ^ 0 = meta x ^ meta n end parenthesis qed end math ] "
" [ math in theory system Q lemma lemma sameExp indu says for all terms meta m comma meta n comma meta x indeed for all meta n indeed parenthesis meta m = meta n imply meta x ^ meta m = meta x ^ meta n end parenthesis imply for all meta n indeed parenthesis meta m + 1 = meta n imply meta x ^ parenthesis meta m + 1 end parenthesis = meta x ^ meta n end parenthesis end lemma end math ] "
" [ math system Q proof of lemma sameExp indu reads block any term meta m comma meta n comma meta x end line block any term meta m comma meta n comma meta x end line line ell a premise for all meta n indeed parenthesis meta m = meta n imply meta x ^ meta m = meta x ^ meta n end parenthesis end line line ell b premise meta m + 1 = meta n end line line ell c because lemma +1IsPositive(N) indeed 0 < meta m + 1 end line line ell f because 1rule expPositive modus ponens ell c indeed meta x ^ parenthesis meta m + 1 end parenthesis = meta x * meta x ^ parenthesis meta m + 1 - 1 end parenthesis end line line ell g because lemma x=x+y-y indeed meta m = meta m + 1 - 1 end line line ell h because lemma a4 at meta m + 1 - 1 modus ponens ell a indeed meta m = meta m + 1 - 1 imply meta x ^ meta m = meta x ^ parenthesis meta m + 1 - 1 end parenthesis end line line ell i because 1rule mp modus ponens ell h modus ponens ell g indeed meta x ^ meta m = meta x ^ parenthesis meta m + 1 - 1 end parenthesis end line line ell j because lemma eqSymmetry modus ponens ell i indeed meta x ^ parenthesis meta m + 1 - 1 end parenthesis = meta x ^ meta m end line line ell k because lemma eqMultiplicationLeft modus ponens ell j indeed meta x * meta x ^ parenthesis meta m + 1 - 1 end parenthesis = meta x * meta x ^ meta m end line line ell l because lemma a4 at meta n - 1 modus ponens ell a indeed meta m = meta n - 1 imply meta x ^ meta m = meta x ^ parenthesis meta n - 1 end parenthesis end line line ell m because lemma positiveToRight(Eq) modus ponens ell b indeed meta m = meta n - 1 end line line ell o because 1rule mp modus ponens ell l modus ponens ell m indeed meta x ^ meta m = meta x ^ parenthesis meta n - 1 end parenthesis end line line ell p because lemma eqMultiplicationLeft modus ponens ell o indeed meta x * meta x ^ meta m = meta x * meta x ^ parenthesis meta n - 1 end parenthesis end line line ell q because lemma subLessRight modus ponens ell b modus ponens ell c indeed 0 < meta n end line line ell r because 1rule expPositive modus ponens ell q indeed meta x ^ meta n = meta x * meta x ^ parenthesis meta n - 1 end parenthesis end line line ell s because lemma eqSymmetry modus ponens ell r indeed meta x * meta x ^ parenthesis meta n - 1 end parenthesis = meta x ^ meta n end line because lemma eqTransitivity5 modus ponens ell f modus ponens ell k modus ponens ell p modus ponens ell s indeed meta x ^ parenthesis meta m + 1 end parenthesis = meta x ^ meta n end line line ell big a end block line ell a because 1rule deduction modus ponens ell big a indeed for all meta n indeed parenthesis meta m = meta n imply meta x ^ meta m = meta x ^ meta n end parenthesis imply meta m + 1 = meta n imply meta x ^ parenthesis meta m + 1 end parenthesis = meta x ^ meta n end line line ell b premise for all meta n indeed parenthesis meta m = meta n imply meta x ^ meta m = meta x ^ meta n end parenthesis end line line ell c because 1rule mp modus ponens ell a modus ponens ell b indeed meta m + 1 = meta n imply meta x ^ parenthesis meta m + 1 end parenthesis = meta x ^ meta n end line because 1rule gen modus ponens ell c indeed for all meta n indeed parenthesis meta m + 1 = meta n imply meta x ^ parenthesis meta m + 1 end parenthesis = meta x ^ meta n end parenthesis end line line ell big b end block any term meta m comma meta n comma meta x end line because 1rule deduction modus ponens ell big b indeed for all meta n indeed parenthesis meta m = meta n imply meta x ^ meta m = meta x ^ meta n end parenthesis imply for all meta n indeed parenthesis meta m + 1 = meta n imply meta x ^ parenthesis meta m + 1 end parenthesis = meta x ^ meta n end parenthesis qed end math ] "
" [ math in theory system Q lemma lemma sameExp says for all terms meta m comma meta n comma meta x indeed meta m = meta n infer meta x ^ meta m = meta x ^ meta n end lemma end math ] "
" [ math system Q proof of lemma sameExp reads any term meta m comma meta n comma meta x end line line ell big a premise meta m = meta n end line line ell a because lemma sameExp base indeed for all meta n indeed parenthesis 0 = meta n imply meta x ^ 0 = meta x ^ meta n end parenthesis end line line ell b because lemma sameExp indu indeed for all meta n indeed parenthesis meta m = meta n imply meta x ^ meta m = meta x ^ meta n end parenthesis imply for all meta n indeed parenthesis meta m + 1 = meta n imply meta x ^ parenthesis meta m + 1 end parenthesis = meta x ^ meta n end parenthesis end line line ell c because lemma induction modus ponens ell a modus ponens ell b indeed for all meta n indeed parenthesis meta m = meta n imply meta x ^ meta m = meta x ^ meta n end parenthesis end line line ell d because lemma a4 at meta n modus ponens ell c indeed meta m = meta n imply meta x ^ meta m = meta x ^ meta n end line because 1rule mp modus ponens ell d modus ponens ell big a indeed meta x ^ meta m = meta x ^ meta n qed end math ] "
------------
" [ math in theory system Q lemma lemma exp(+1) says for all terms meta m comma meta x indeed meta x ^ parenthesis meta m + 1 end parenthesis = meta x * meta x ^ meta m end lemma end math ] "
" [ math system Q proof of lemma exp(+1) reads any term meta m comma meta x end line line ell a because lemma +1IsPositive(N) indeed 0 < meta m + 1 end line line ell b because 1rule expPositive modus ponens ell a indeed meta x ^ parenthesis meta m + 1 end parenthesis = meta x * meta x ^ parenthesis meta m + 1 - 1 end parenthesis end line line ell c because lemma x=x+y-y indeed meta m = meta m + 1 - 1 end line line ell d because lemma sameExp modus ponens ell c indeed meta x ^ meta m = meta x ^ parenthesis meta m + 1 - 1 end parenthesis end line line ell e because lemma eqMultiplicationLeft modus ponens ell d indeed meta x * meta x ^ meta m = meta x * meta x ^ parenthesis meta m + 1 - 1 end parenthesis end line line ell f because lemma eqSymmetry modus ponens ell e indeed meta x * meta x ^ parenthesis meta m + 1 - 1 end parenthesis = meta x * meta x ^ meta m end line because lemma eqTransitivity modus ponens ell b modus ponens ell f indeed meta x ^ parenthesis meta m + 1 end parenthesis = meta x * meta x ^ meta m qed end math ] "
" [ math in theory system Q lemma lemma distributionOut(Minus) says for all terms meta x comma meta y comma meta z indeed meta x * meta y - meta x * meta z = meta x * parenthesis meta y - meta z end parenthesis end lemma end math ] "
" [ math system Q proof of lemma distributionOut(Minus) reads any term meta x comma meta y comma meta z end line line ell a because lemma times(-1)Left indeed (-1) * parenthesis meta x * meta z end parenthesis = - parenthesis meta x * meta z end parenthesis end line line ell b because lemma eqSymmetry modus ponens ell a indeed - parenthesis meta x * meta z end parenthesis = (-1) * parenthesis meta x * meta z end parenthesis end line line ell c because axiom timesCommutativity indeed (-1) * parenthesis meta x * meta z end parenthesis = meta x * meta z * (-1) end line line ell d because axiom timesAssociativity indeed meta x * meta z * (-1) = meta x * parenthesis meta z * (-1) end parenthesis end line line ell e because lemma times(-1) indeed meta z * (-1) = - meta z end line line ell f because lemma eqMultiplicationLeft modus ponens ell e indeed meta x * parenthesis meta z * (-1) end parenthesis = meta x * parenthesis - meta z end parenthesis end line line ell g because lemma eqTransitivity5 modus ponens ell b modus ponens ell c modus ponens ell d modus ponens ell f indeed - parenthesis meta x * meta z end parenthesis = meta x * parenthesis - meta z end parenthesis end line line ell h because lemma eqAdditionLeft modus ponens ell g indeed meta x * meta y - meta x * meta z = meta x * meta y + meta x * parenthesis - meta z end parenthesis end line line ell i because lemma distributionOut indeed meta x * meta y + meta x * parenthesis - meta z end parenthesis = meta x * parenthesis meta y - meta z end parenthesis end line because lemma eqTransitivity modus ponens ell h modus ponens ell i indeed meta x * meta y - meta x * meta z = meta x * parenthesis meta y - meta z end parenthesis qed end math ] "
" [ math in theory system Q lemma lemma (1/2)(x+y)-x=(1/2)(y-x) says for all terms meta x comma meta y indeed 1/2 * parenthesis meta x + meta y end parenthesis - meta x = 1/2 * parenthesis meta y - meta x end parenthesis end lemma end math ] "
" [ math system Q proof of lemma (1/2)(x+y)-x=(1/2)(y-x) reads any term meta x comma meta y end line line ell a because axiom distribution indeed 1/2 * parenthesis meta x + meta y end parenthesis = 1/2 * meta x + 1/2 * meta y end line line ell b because lemma eqAddition modus ponens ell a indeed 1/2 * parenthesis meta x + meta y end parenthesis - meta x = 1/2 * meta x + 1/2 * meta y - meta x end line line ell c because axiom plusCommutativity indeed 1/2 * meta x + 1/2 * meta y = 1/2 * meta y + 1/2 * meta x end line line ell d because lemma eqAddition modus ponens ell c indeed 1/2 * meta x + 1/2 * meta y - meta x = 1/2 * meta y + 1/2 * meta x - meta x end line line ell big a because axiom plusAssociativity indeed 1/2 * meta y + 1/2 * meta x - meta x = 1/2 * meta y + parenthesis 1/2 * meta x - meta x end parenthesis end line line ell e because lemma (1/2)x+(1/2)x=x indeed 1/2 * meta x + 1/2 * meta x = meta x end line line ell f because lemma positiveToRight(Eq) modus ponens ell e indeed 1/2 * meta x = meta x - 1/2 * meta x end line line ell g because lemma eqNegated modus ponens ell f indeed - parenthesis 1/2 * meta x end parenthesis = - parenthesis meta x - 1/2 * meta x end parenthesis end line line ell h because lemma minusNegated indeed - parenthesis meta x - 1/2 * meta x end parenthesis = 1/2 * meta x - meta x end line line ell i because lemma eqTransitivity modus ponens ell g modus ponens ell h indeed - parenthesis 1/2 * meta x end parenthesis = 1/2 * meta x - meta x end line line ell j because lemma eqSymmetry modus ponens ell i indeed 1/2 * meta x - meta x = - parenthesis 1/2 * meta x end parenthesis end line line ell k because lemma eqAdditionLeft modus ponens ell j indeed 1/2 * meta y + parenthesis 1/2 * meta x - meta x end parenthesis = 1/2 * meta y - 1/2 * meta x end line line ell l because lemma distributionOut(Minus) indeed 1/2 * meta y - 1/2 * meta x = 1/2 * parenthesis meta y - meta x end parenthesis end line because lemma eqTransitivity6 modus ponens ell b modus ponens ell d modus ponens ell big a modus ponens ell k modus ponens ell l indeed 1/2 * parenthesis meta x + meta y end parenthesis - meta x = 1/2 * parenthesis meta y - meta x end parenthesis qed end math ] "
" [ math in theory system Q lemma lemma y-(1/2)(x+y)=(1/2)(y-x) says for all terms meta x comma meta y indeed meta y - 1/2 * parenthesis meta x + meta y end parenthesis = 1/2 * parenthesis meta y - meta x end parenthesis end lemma end math ] "
" [ math system Q proof of lemma y-(1/2)(x+y)=(1/2)(y-x) reads any term meta x comma meta y end line line ell a because axiom distribution indeed 1/2 * parenthesis meta x + meta y end parenthesis = 1/2 * meta x + 1/2 * meta y end line line ell b because lemma eqNegated modus ponens ell a indeed - parenthesis 1/2 * parenthesis meta x + meta y end parenthesis end parenthesis = - parenthesis 1/2 * meta x + 1/2 * meta y end parenthesis end line line ell c because lemma eqAdditionLeft modus ponens ell b indeed meta y - 1/2 * parenthesis meta x + meta y end parenthesis = meta y - parenthesis 1/2 * meta x + 1/2 * meta y end parenthesis end line line ell d because axiom plusCommutativity indeed 1/2 * meta x + 1/2 * meta y = 1/2 * meta y + 1/2 * meta x end line line ell e because lemma eqNegated modus ponens ell d indeed - parenthesis 1/2 * meta x + 1/2 * meta y end parenthesis = - parenthesis 1/2 * meta y + 1/2 * meta x end parenthesis end line line ell f because lemma -x-y=-(x+y) indeed - parenthesis 1/2 * meta y end parenthesis - 1/2 * meta x = - parenthesis 1/2 * meta y + 1/2 * meta x end parenthesis end line line ell g because lemma eqSymmetry modus ponens ell f indeed - parenthesis 1/2 * meta y + 1/2 * meta x end parenthesis = - parenthesis 1/2 * meta y end parenthesis - 1/2 * meta x end line line ell h because lemma eqTransitivity modus ponens ell e modus ponens ell g indeed - parenthesis 1/2 * meta x + 1/2 * meta y end parenthesis = - parenthesis 1/2 * meta y end parenthesis - 1/2 * meta x end line line ell i because lemma eqAdditionLeft modus ponens ell h indeed meta y - parenthesis 1/2 * meta x + 1/2 * meta y end parenthesis = meta y + parenthesis - parenthesis 1/2 * meta y end parenthesis - 1/2 * meta x end parenthesis end line line ell big i because axiom plusAssociativity indeed meta y - 1/2 * meta y - 1/2 * meta x = meta y + parenthesis - parenthesis 1/2 * meta y end parenthesis - 1/2 * meta x end parenthesis end line line ell big j because lemma eqSymmetry modus ponens ell big i indeed meta y + parenthesis - parenthesis 1/2 * meta y end parenthesis - 1/2 * meta x end parenthesis = meta y - 1/2 * meta y - 1/2 * meta x end line line ell j because lemma (1/2)x+(1/2)x=x indeed 1/2 * meta y + 1/2 * meta y = meta y end line line ell k because lemma positiveToRight(Eq) modus ponens ell j indeed 1/2 * meta y = meta y - 1/2 * meta y end line line ell l because lemma eqSymmetry modus ponens ell k indeed meta y - 1/2 * meta y = 1/2 * meta y end line line ell m because lemma eqAddition modus ponens ell l indeed meta y - 1/2 * meta y - 1/2 * meta x = 1/2 * meta y - 1/2 * meta x end line line ell n because lemma distributionOut(Minus) indeed 1/2 * meta y - 1/2 * meta x = 1/2 * parenthesis meta y - meta x end parenthesis end line because lemma eqTransitivity6 modus ponens ell c modus ponens ell i modus ponens ell big j modus ponens ell m modus ponens ell n indeed meta y - 1/2 * parenthesis meta x + meta y end parenthesis = 1/2 * parenthesis meta y - meta x end parenthesis qed end math ] "
--------------
" [ math in theory system Q lemma lemma positiveBase base says for all terms meta x indeed 0 < meta x ^ 0 end lemma end math ] "
" [ math system Q proof of lemma positiveBase base reads any term meta x end line line ell a because lemma expZero exact indeed meta x ^ 0 = 1 end line line ell b because lemma eqSymmetry modus ponens ell a indeed 1 = meta x ^ 0 end line line ell c because lemma 0<1 indeed 0 < 1 end line because lemma subLessRight modus ponens ell b modus ponens ell c indeed 0 < meta x ^ 0 qed end math ] "
" [ math in theory system Q lemma lemma positiveBase indu says for all terms meta m comma meta x indeed 0 < meta x infer 0 < meta x ^ meta m imply 0 < meta x ^ parenthesis meta m + 1 end parenthesis end lemma end math ] "
" [ math system Q proof of lemma positiveBase indu reads block any term meta m comma meta x end line line ell a premise 0 < meta x end line line ell b premise 0 < meta x ^ meta m end line line ell c because lemma exp(+1) indeed meta x ^ parenthesis meta m + 1 end parenthesis = meta x * meta x ^ meta m end line line ell d because lemma eqSymmetry modus ponens ell c indeed meta x * meta x ^ meta m = meta x ^ parenthesis meta m + 1 end parenthesis end line line ell e because lemma positiveFactors modus ponens ell a modus ponens ell b indeed 0 < meta x * meta x ^ meta m end line because lemma subLessRight modus ponens ell d modus ponens ell e indeed 0 < meta x ^ parenthesis meta m + 1 end parenthesis end line line ell big a end block any term meta m comma meta x end line line ell a because 1rule deduction modus ponens ell big a indeed 0 < meta x imply 0 < meta x ^ meta m imply 0 < meta x ^ parenthesis meta m + 1 end parenthesis end line line ell b premise 0 < meta x end line because 1rule mp modus ponens ell a modus ponens ell b indeed 0 < meta x ^ meta m imply 0 < meta x ^ parenthesis meta m + 1 end parenthesis qed end math ] "
" [ math in theory system Q lemma lemma positiveBase says for all terms meta m comma meta x indeed 0 < meta x infer 0 < meta x ^ meta m end lemma end math ] "
" [ math system Q proof of lemma positiveBase reads any term meta m comma meta x end line line ell a premise 0 < meta x end line line ell b because lemma positiveBase base indeed 0 < meta x ^ 0 end line line ell c because lemma positiveBase indu modus ponens ell a indeed 0 < meta x ^ meta m imply 0 < meta x ^ parenthesis meta m + 1 end parenthesis end line because lemma induction modus ponens ell b modus ponens ell c indeed 0 < meta x ^ meta m qed end math ] "
" [ math in theory system Q lemma lemma positiveToRight(Eq)(1 term) says for all terms meta x comma meta y indeed meta x = meta y infer 0 = meta y - meta x end lemma end math ] "
" [ math system Q proof of lemma positiveToRight(Eq)(1 term) reads any term meta x comma meta y end line line ell a premise meta x = meta y end line line ell b because lemma eqSymmetry modus ponens ell a indeed meta y = meta x end line line ell c because lemma positiveToLeft(Eq)(1 term) modus ponens ell b indeed meta y - meta x = 0 end line because lemma eqSymmetry modus ponens ell c indeed 0 = meta y - meta x qed end math ] "
---------
" [ math in theory system Q lemma lemma base(1/2)Sum zero exact says for all terms meta m indeed base(1/2)Sum( meta m , 0 ) = 1/2 ^ meta m end lemma end math ] "
" [ math system Q proof of lemma base(1/2)Sum zero exact reads any term meta m end line line ell a because lemma eqReflexivity indeed 0 = 0 end line because 1rule base(1/2)Sum zero modus ponens ell a indeed base(1/2)Sum( meta m , 0 ) = 1/2 ^ meta m qed end math ] "
" [ math in theory system Q lemma lemma sameBase(1/2)Sum second base says for all terms meta m comma meta n2 indeed for all meta n2 indeed parenthesis 0 = meta n2 imply base(1/2)Sum( meta m , 0 ) = base(1/2)Sum( meta m , meta n2 ) end parenthesis end lemma end math ] "
" [ math system Q proof of lemma sameBase(1/2)Sum second base reads block any term meta m comma meta n2 end line line ell a premise 0 = meta n2 end line line ell b because lemma eqSymmetry modus ponens ell a indeed meta n2 = 0 end line line ell c because 1rule base(1/2)Sum zero modus ponens ell b indeed base(1/2)Sum( meta m , meta n2 ) = 1/2 ^ parenthesis meta m end parenthesis end line line ell d because lemma eqSymmetry modus ponens ell c indeed 1/2 ^ parenthesis meta m end parenthesis = base(1/2)Sum( meta m , meta n2 ) end line line ell e because lemma base(1/2)Sum zero exact indeed base(1/2)Sum( meta m , 0 ) = 1/2 ^ parenthesis meta m end parenthesis end line because lemma eqTransitivity modus ponens ell e modus ponens ell d indeed base(1/2)Sum( meta m , 0 ) = base(1/2)Sum( meta m , meta n2 ) end line line ell big a end block any term meta m comma meta n2 end line line ell a because 1rule deduction modus ponens ell big a indeed 0 = meta n2 imply base(1/2)Sum( meta m , 0 ) = base(1/2)Sum( meta m , meta n2 ) end line because 1rule gen modus ponens ell a indeed for all meta n2 indeed parenthesis 0 = meta n2 imply base(1/2)Sum( meta m , 0 ) = base(1/2)Sum( meta m , meta n2 ) end parenthesis qed end math ] "
" [ math in theory system Q lemma lemma sameBase(1/2)Sum second indu says for all terms meta m comma meta n1 comma meta n2 indeed for all meta n2 indeed parenthesis meta n1 = meta n2 imply base(1/2)Sum( meta m , meta n1 ) = base(1/2)Sum( meta m , meta n2 ) end parenthesis imply for all meta n2 indeed parenthesis meta n1 + 1 = meta n2 imply base(1/2)Sum( meta m , meta n1 + 1 ) = base(1/2)Sum( meta m , meta n2 ) end parenthesis end lemma end math ] "
" [ math system Q proof of lemma sameBase(1/2)Sum second indu reads block any term meta m comma meta n1 comma meta n2 end line block any term meta m comma meta n1 comma meta n2 end line line ell a premise for all meta n2 indeed parenthesis meta n1 = meta n2 imply base(1/2)Sum( meta m , meta n1 ) = base(1/2)Sum( meta m , meta n2 ) end parenthesis end line line ell b premise meta n1 + 1 = meta n2 end line line ell c because lemma +1IsPositive(N) indeed 0 < meta n1 + 1 end line line ell d because 1rule base(1/2)Sum positive modus ponens ell c indeed base(1/2)Sum( meta m , meta n1 + 1 ) = 1/2 ^ parenthesis meta m + parenthesis meta n1 + 1 end parenthesis end parenthesis + base(1/2)Sum( meta m , meta n1 + 1 - 1 ) end line line ell e because lemma x=x+y-y indeed meta n1 = meta n1 + 1 - 1 end line line ell f because lemma a4 at meta n1 + 1 - 1 modus ponens ell a indeed meta n1 = meta n1 + 1 - 1 imply base(1/2)Sum( meta m , meta n1 ) = base(1/2)Sum( meta m , meta n1 + 1 - 1 ) end line line ell g because 1rule mp modus ponens ell f modus ponens ell e indeed base(1/2)Sum( meta m , meta n1 ) = base(1/2)Sum( meta m , meta n1 + 1 - 1 ) end line line ell h because lemma eqSymmetry modus ponens ell g indeed base(1/2)Sum( meta m , meta n1 + 1 - 1 ) = base(1/2)Sum( meta m , meta n1 ) end line line ell i because lemma eqAdditionLeft modus ponens ell h indeed 1/2 ^ parenthesis meta m + parenthesis meta n1 + 1 end parenthesis end parenthesis + base(1/2)Sum( meta m , meta n1 + 1 - 1 ) = 1/2 ^ parenthesis meta m + parenthesis meta n1 + 1 end parenthesis end parenthesis + base(1/2)Sum( meta m , meta n1 ) end line line ell j because lemma positiveToRight(Eq) modus ponens ell b indeed meta n1 = meta n2 - 1 end line line ell k because lemma a4 at meta n2 - 1 modus ponens ell a indeed meta n1 = meta n2 - 1 imply base(1/2)Sum( meta m , meta n1 ) = base(1/2)Sum( meta m , meta n2 - 1 ) end line line ell l because 1rule mp modus ponens ell k modus ponens ell j indeed base(1/2)Sum( meta m , meta n1 ) = base(1/2)Sum( meta m , meta n2 - 1 ) end line line ell m because lemma eqAdditionLeft modus ponens ell l indeed 1/2 ^ parenthesis meta m + parenthesis meta n1 + 1 end parenthesis end parenthesis + base(1/2)Sum( meta m , meta n1 ) = 1/2 ^ parenthesis meta m + parenthesis meta n1 + 1 end parenthesis end parenthesis + base(1/2)Sum( meta m , meta n2 - 1 ) end line line ell n because lemma eqAdditionLeft modus ponens ell b indeed meta m + parenthesis meta n1 + 1 end parenthesis = meta m + meta n2 end line line ell o because lemma sameExp modus ponens ell n indeed 1/2 ^ parenthesis meta m + parenthesis meta n1 + 1 end parenthesis end parenthesis = 1/2 ^ parenthesis meta m + meta n2 end parenthesis end line line ell p because lemma eqAddition modus ponens ell o indeed 1/2 ^ parenthesis meta m + parenthesis meta n1 + 1 end parenthesis end parenthesis + base(1/2)Sum( meta m , meta n2 - 1 ) = 1/2 ^ parenthesis meta m + meta n2 end parenthesis + base(1/2)Sum( meta m , meta n2 - 1 ) end line line ell q because lemma subLessRight modus ponens ell b modus ponens ell c indeed 0 < meta n2 end line line ell r because 1rule base(1/2)Sum positive modus ponens ell q indeed base(1/2)Sum( meta m , meta n2 ) = 1/2 ^ parenthesis meta m + meta n2 end parenthesis + base(1/2)Sum( meta m , meta n2 - 1 ) end line line ell s because lemma eqSymmetry modus ponens ell r indeed 1/2 ^ parenthesis meta m + meta n2 end parenthesis + base(1/2)Sum( meta m , meta n2 - 1 ) = base(1/2)Sum( meta m , meta n2 ) end line because lemma eqTransitivity6 modus ponens ell d modus ponens ell i modus ponens ell m modus ponens ell p modus ponens ell s indeed base(1/2)Sum( meta m , meta n1 + 1 ) = base(1/2)Sum( meta m , meta n2 ) end line line ell big a end block line ell a because 1rule deduction modus ponens ell big a indeed for all meta n2 indeed parenthesis meta n1 = meta n2 imply base(1/2)Sum( meta m , meta n1 ) = base(1/2)Sum( meta m , meta n2 ) end parenthesis imply meta n1 + 1 = meta n2 imply base(1/2)Sum( meta m , meta n1 + 1 ) = base(1/2)Sum( meta m , meta n2 ) end line line ell b premise for all meta n2 indeed parenthesis meta n1 = meta n2 imply base(1/2)Sum( meta m , meta n1 ) = base(1/2)Sum( meta m , meta n2 ) end parenthesis end line line ell c because 1rule mp modus ponens ell a modus ponens ell b indeed meta n1 + 1 = meta n2 imply base(1/2)Sum( meta m , meta n1 + 1 ) = base(1/2)Sum( meta m , meta n2 ) end line because 1rule gen modus ponens ell c indeed for all meta n2 indeed parenthesis meta n1 + 1 = meta n2 imply base(1/2)Sum( meta m , meta n1 + 1 ) = base(1/2)Sum( meta m , meta n2 ) end parenthesis end line line ell big b end block any term meta m comma meta n1 comma meta n2 end line because 1rule deduction modus ponens ell big b indeed for all meta n2 indeed parenthesis meta n1 = meta n2 imply base(1/2)Sum( meta m , meta n1 ) = base(1/2)Sum( meta m , meta n2 ) end parenthesis imply for all meta n2 indeed parenthesis meta n1 + 1 = meta n2 imply base(1/2)Sum( meta m , meta n1 + 1 ) = base(1/2)Sum( meta m , meta n2 ) end parenthesis qed end math ] "
" [ math in theory system Q lemma lemma sameBase(1/2)Sum second says for all terms meta m comma meta n1 comma meta n2 indeed meta n1 = meta n2 infer base(1/2)Sum( meta m , meta n1 ) = base(1/2)Sum( meta m , meta n2 ) end lemma end math ] "
" [ math system Q proof of lemma sameBase(1/2)Sum second reads any term meta m comma meta n1 comma meta n2 end line line ell a premise meta n1 = meta n2 end line line ell b because lemma sameBase(1/2)Sum second base indeed for all meta n2 indeed parenthesis 0 = meta n2 imply base(1/2)Sum( meta m , 0 ) = base(1/2)Sum( meta m , meta n2 ) end parenthesis end line line ell c because lemma sameBase(1/2)Sum second indu indeed for all meta n2 indeed parenthesis meta n1 = meta n2 imply base(1/2)Sum( meta m , meta n1 ) = base(1/2)Sum( meta m , meta n2 ) end parenthesis imply for all meta n2 indeed parenthesis meta n1 + 1 = meta n2 imply base(1/2)Sum( meta m , meta n1 + 1 ) = base(1/2)Sum( meta m , meta n2 ) end parenthesis end line line ell d because lemma induction modus ponens ell b modus ponens ell c indeed for all meta n2 indeed parenthesis meta n1 = meta n2 imply base(1/2)Sum( meta m , meta n1 ) = base(1/2)Sum( meta m , meta n2 ) end parenthesis end line line ell e because lemma a4 at meta n2 modus ponens ell d indeed meta n1 = meta n2 imply base(1/2)Sum( meta m , meta n1 ) = base(1/2)Sum( meta m , meta n2 ) end line because 1rule mp modus ponens ell e modus ponens ell a indeed base(1/2)Sum( meta m , meta n1 ) = base(1/2)Sum( meta m , meta n2 ) qed end math ] "
--------------
" [ math in theory system Q lemma lemma negativeToLeft(Less)(1 term) says for all terms meta x comma meta y indeed 0 < meta x - meta y infer meta y < meta x end lemma end math ] "
" [ math system Q proof of lemma negativeToLeft(Less)(1 term) reads any term meta x comma meta y end line line ell a premise 0 < meta x - meta y end line line ell b because lemma lessAddition modus ponens ell a indeed 0 + meta y < meta x - meta y + meta y end line line ell c because lemma plus0Left indeed 0 + meta y = meta y end line line ell d because lemma subLessLeft modus ponens ell c modus ponens ell b indeed meta y < meta x - meta y + meta y end line line ell e because lemma three2threeTerms indeed meta x - meta y + meta y = meta x + meta y - meta y end line line ell f because lemma x=x+y-y indeed meta x = meta x + meta y - meta y end line line ell g because lemma eqSymmetry modus ponens ell f indeed meta x + meta y - meta y = meta x end line line ell h because lemma eqTransitivity modus ponens ell e modus ponens ell g indeed meta x - meta y + meta y = meta x end line because lemma subLessRight modus ponens ell h modus ponens ell d indeed meta y < meta x qed end math ] "
" [ math in theory system Q lemma lemma base(1/2)Sum(+1) says for all terms meta m comma meta n indeed base(1/2)Sum( meta m , meta n + 1 ) = 1/2 ^ parenthesis meta m + meta n + 1 end parenthesis + base(1/2)Sum( meta m , meta n ) end lemma end math ] "
" [ math system Q proof of lemma base(1/2)Sum(+1) reads any term meta m comma meta n end line line ell a because lemma +1IsPositive(N) indeed 0 < meta n + 1 end line line ell b because 1rule base(1/2)Sum positive modus ponens ell a indeed base(1/2)Sum( meta m , meta n + 1 ) = 1/2 ^ parenthesis meta m + parenthesis meta n + 1 end parenthesis end parenthesis + base(1/2)Sum( meta m , meta n + 1 - 1 ) end line line ell f because axiom plusAssociativity indeed meta m + meta n + 1 = meta m + parenthesis meta n + 1 end parenthesis end line line ell g because lemma sameExp modus ponens ell f indeed 1/2 ^ parenthesis meta m + meta n + 1 end parenthesis = 1/2 ^ parenthesis meta m + parenthesis meta n + 1 end parenthesis end parenthesis end line line ell h because lemma eqSymmetry modus ponens ell g indeed 1/2 ^ parenthesis meta m + parenthesis meta n + 1 end parenthesis end parenthesis = 1/2 ^ parenthesis meta m + meta n + 1 end parenthesis end line line ell c because lemma x=x+y-y indeed meta n = meta n + 1 - 1 end line line ell d because lemma sameBase(1/2)Sum second modus ponens ell c indeed base(1/2)Sum( meta m , meta n ) = base(1/2)Sum( meta m , meta n + 1 - 1 ) end line line ell e because lemma eqSymmetry modus ponens ell d indeed base(1/2)Sum( meta m , meta n + 1 - 1 ) = base(1/2)Sum( meta m , meta n ) end line line ell i because lemma addEquations modus ponens ell h modus ponens ell e indeed 1/2 ^ parenthesis meta m + parenthesis meta n + 1 end parenthesis end parenthesis + base(1/2)Sum( meta m , meta n + 1 - 1 ) = 1/2 ^ parenthesis meta m + meta n + 1 end parenthesis + base(1/2)Sum( meta m , meta n ) end line because lemma eqTransitivity modus ponens ell b modus ponens ell i indeed base(1/2)Sum( meta m , meta n + 1 ) = 1/2 ^ parenthesis meta m + meta n + 1 end parenthesis + base(1/2)Sum( meta m , meta n ) qed end math ] "
" [ math in theory system Q lemma lemma base(1/2)Sum exact bound base says for all terms meta m indeed base(1/2)Sum( meta m + 1 , 0 ) + 1/2 ^ parenthesis meta m + 1 + 0 end parenthesis = 1/2 ^ meta m end lemma end math ] "
" [ math system Q proof of lemma base(1/2)Sum exact bound base reads any term meta m end line line ell a because lemma base(1/2)Sum zero exact indeed base(1/2)Sum( meta m + 1 , 0 ) = 1/2 ^ parenthesis meta m + 1 end parenthesis end line line ell b because lemma exp(+1) indeed 1/2 ^ parenthesis meta m + 1 end parenthesis = 1/2 * 1/2 ^ meta m end line line ell c because lemma eqTransitivity modus ponens ell a modus ponens ell b indeed base(1/2)Sum( meta m + 1 , 0 ) = 1/2 * 1/2 ^ meta m end line line ell d because axiom plus0 indeed meta m + 1 + 0 = meta m + 1 end line line ell e because lemma sameExp modus ponens ell d indeed 1/2 ^ parenthesis meta m + 1 + 0 end parenthesis = 1/2 ^ parenthesis meta m + 1 end parenthesis end line line ell f because lemma eqTransitivity modus ponens ell e modus ponens ell b indeed 1/2 ^ parenthesis meta m + 1 + 0 end parenthesis = 1/2 * 1/2 ^ meta m end line line ell g because lemma addEquations modus ponens ell c modus ponens ell f indeed base(1/2)Sum( meta m + 1 , 0 ) + 1/2 ^ parenthesis meta m + 1 + 0 end parenthesis = 1/2 * 1/2 ^ meta m + 1/2 * 1/2 ^ meta m end line line ell h because lemma (1/2)x+(1/2)x=x indeed 1/2 * 1/2 ^ meta m + 1/2 * 1/2 ^ meta m = 1/2 ^ meta m end line because lemma eqTransitivity modus ponens ell g modus ponens ell h indeed base(1/2)Sum( meta m + 1 , 0 ) + 1/2 ^ parenthesis meta m + 1 + 0 end parenthesis = 1/2 ^ meta m qed end math ] "
" [ math in theory system Q lemma lemma base(1/2)Sum exact bound indu says for all terms meta m comma meta n indeed base(1/2)Sum( meta m + 1 , meta n ) + 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis = 1/2 ^ meta m imply base(1/2)Sum( meta m + 1 , meta n + 1 ) + 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis = 1/2 ^ meta m end lemma end math ] "
" [ math system Q proof of lemma base(1/2)Sum exact bound indu reads block any term meta m comma meta n end line line ell a premise base(1/2)Sum( meta m + 1 , meta n ) + 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis = 1/2 ^ meta m end line line ell b because lemma base(1/2)Sum(+1) indeed base(1/2)Sum( meta m + 1 , meta n + 1 ) = 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis + base(1/2)Sum( meta m + 1 , meta n ) end line line ell c because lemma eqAddition modus ponens ell b indeed base(1/2)Sum( meta m + 1 , meta n + 1 ) + 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis = 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis + base(1/2)Sum( meta m + 1 , meta n ) + 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis end line line ell d because axiom plusCommutativity indeed 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis + base(1/2)Sum( meta m + 1 , meta n ) = base(1/2)Sum( meta m + 1 , meta n ) + 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis end line line ell e because lemma eqAddition modus ponens ell d indeed 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis + base(1/2)Sum( meta m + 1 , meta n ) + 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis = base(1/2)Sum( meta m + 1 , meta n ) + 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis + 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis end line line ell f because lemma exp(+1) indeed 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis = 1/2 * 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis end line line ell g because lemma addEquations modus ponens ell f modus ponens ell f indeed 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis + 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis = 1/2 * 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis + 1/2 * 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis end line line ell h because lemma (1/2)x+(1/2)x=x indeed 1/2 * 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis + 1/2 * 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis = 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis end line line ell i because lemma eqTransitivity modus ponens ell g modus ponens ell h indeed 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis + 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis = 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis end line line ell j because lemma three2twoTerms modus ponens ell i indeed base(1/2)Sum( meta m + 1 , meta n ) + 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis + 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis = base(1/2)Sum( meta m + 1 , meta n ) + 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis end line because lemma eqTransitivity5 modus ponens ell c modus ponens ell e modus ponens ell j modus ponens ell a indeed base(1/2)Sum( meta m + 1 , meta n + 1 ) + 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis = 1/2 ^ meta m end line line ell big a end block any term meta m comma meta n end line because 1rule deduction modus ponens ell big a indeed base(1/2)Sum( meta m + 1 , meta n ) + 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis = 1/2 ^ meta m imply base(1/2)Sum( meta m + 1 , meta n + 1 ) + 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis = 1/2 ^ meta m qed end math ] "
" [ math in theory system Q lemma lemma base(1/2)Sum exact bound says for all terms meta m comma meta n indeed base(1/2)Sum( meta m + 1 , meta n ) + 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis = 1/2 ^ meta m end lemma end math ] "
" [ math system Q proof of lemma base(1/2)Sum exact bound reads any term meta m comma meta n end line line ell a because lemma base(1/2)Sum exact bound base indeed base(1/2)Sum( meta m + 1 , 0 ) + 1/2 ^ parenthesis meta m + 1 + 0 end parenthesis = 1/2 ^ meta m end line line ell b because lemma base(1/2)Sum exact bound indu indeed base(1/2)Sum( meta m + 1 , meta n ) + 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis = 1/2 ^ meta m imply base(1/2)Sum( meta m + 1 , meta n + 1 ) + 1/2 ^ parenthesis meta m + 1 + meta n + 1 end parenthesis = 1/2 ^ meta m end line because lemma induction modus ponens ell a modus ponens ell b indeed base(1/2)Sum( meta m + 1 , meta n ) + 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis = 1/2 ^ meta m qed end math ] "
" [ math in theory system Q lemma lemma base(1/2)Sum bound says for all terms meta m comma meta n indeed base(1/2)Sum( meta m + 1 , meta n ) < 1/2 ^ meta m end lemma end math ] "
" [ math system Q proof of lemma base(1/2)Sum bound reads any term meta m comma meta n end line line ell a because lemma base(1/2)Sum exact bound indeed base(1/2)Sum( meta m + 1 , meta n ) + 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis = 1/2 ^ meta m end line line ell b because axiom plusCommutativity indeed 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis + base(1/2)Sum( meta m + 1 , meta n ) = base(1/2)Sum( meta m + 1 , meta n ) + 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis end line line ell c because lemma eqTransitivity modus ponens ell b modus ponens ell a indeed 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis + base(1/2)Sum( meta m + 1 , meta n ) = 1/2 ^ meta m end line line ell d because lemma positiveToRight(Eq) modus ponens ell c indeed 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis = 1/2 ^ meta m - base(1/2)Sum( meta m + 1 , meta n ) end line line ell e because lemma 0<1/2 indeed 0 < 1/2 end line line ell f because lemma positiveBase modus ponens ell e indeed 0 < 1/2 ^ parenthesis meta m + 1 + meta n end parenthesis end line line ell g because lemma subLessRight modus ponens ell d modus ponens ell f indeed 0 < 1/2 ^ meta m - base(1/2)Sum( meta m + 1 , meta n ) end line because lemma negativeToLeft(Less)(1 term) modus ponens ell g indeed base(1/2)Sum( meta m + 1 , meta n ) < 1/2 ^ meta m qed end math ] "
---------
" [ math in theory system Q lemma lemma sameSeries(NumDiff) says for all terms meta fx comma meta fy comma meta o comma meta p comma meta n1 comma meta n2 indeed meta o = meta p infer meta n1 = meta n2 infer | [ meta fx ; meta o ] - [ meta fy ; meta n1 ] | = | [ meta fx ; meta p ] - [ meta fy ; meta n2 ] | end lemma end math ] "
" [ math system Q proof of lemma sameSeries(NumDiff) reads any term meta fx comma meta fy comma meta o comma meta p comma meta n1 comma meta n2 end line line ell a premise meta o = meta p end line line ell b premise meta n1 = meta n2 end line line ell c because lemma sameSeries modus ponens ell a indeed [ meta fx ; meta o ] = [ meta fx ; meta p ] end line line ell d because lemma sameSeries modus ponens ell b indeed [ meta fy ; meta n1 ] = [ meta fy ; meta n2 ] end line line ell e because lemma eqNegated modus ponens ell d indeed - [ meta fy ; meta n1 ] = - [ meta fy ; meta n2 ] end line line ell f because lemma addEquations modus ponens ell c modus ponens ell e indeed [ meta fx ; meta o ] - [ meta fy ; meta n1 ] = [ meta fx ; meta p ] - [ meta fy ; meta n2 ] end line because lemma sameNumerical modus ponens ell f indeed | [ meta fx ; meta o ] - [ meta fy ; meta n1 ] | = | [ meta fx ; meta p ] - [ meta fy ; meta n2 ] | qed end math ] "
" [ math in theory system Q lemma lemma UStelescope zero exact says for all terms meta m indeed UStelescope( meta m , 0 ) = | [ us ; meta m ] - [ us ; meta m + 1 ] | end lemma end math ] "
" [ math system Q proof of lemma UStelescope zero exact reads any term meta m end line line ell a because lemma eqReflexivity indeed 0 = 0 end line because 1rule UStelescope zero modus ponens ell a indeed UStelescope( meta m , 0 ) = | [ us ; meta m ] - [ us ; meta m + 1 ] | qed end math ] "
" [ math in theory system Q lemma lemma sameTelescope second base says for all terms meta m comma meta n2 indeed for all meta n2 indeed ( 0 = meta n2 imply UStelescope( meta m , 0 ) = UStelescope( meta m , meta n2 ) ) end lemma end math ] "
" [ math system Q proof of lemma sameTelescope second base reads block any term meta m comma meta n2 end line line ell a premise 0 = meta n2 end line line ell b because lemma eqSymmetry modus ponens ell a indeed meta n2 = 0 end line line ell c because 1rule UStelescope zero modus ponens ell b indeed UStelescope( meta m , meta n2 ) = | [ us ; meta m ] - [ us ; meta m + 1 ] | end line line ell d because lemma eqSymmetry modus ponens ell c indeed | [ us ; meta m ] - [ us ; meta m + 1 ] | = UStelescope( meta m , meta n2 ) end line line ell e because lemma UStelescope zero exact indeed UStelescope( meta m , 0 ) = | [ us ; meta m ] - [ us ; meta m + 1 ] | end line because lemma eqTransitivity modus ponens ell e modus ponens ell d indeed UStelescope( meta m , 0 ) = UStelescope( meta m , meta n2 ) end line line ell big a end block any term meta m comma meta n2 end line line ell a because 1rule deduction modus ponens ell big a indeed 0 = meta n2 imply UStelescope( meta m , 0 ) = UStelescope( meta m , meta n2 ) end line because 1rule gen modus ponens ell a indeed for all meta n2 indeed ( 0 = meta n2 imply UStelescope( meta m , 0 ) = UStelescope( meta m , meta n2 ) ) qed end math ] "
" [ math in theory system Q lemma lemma sameTelescope second indu says for all terms meta m comma meta n1 comma meta n2 indeed for all meta n2 indeed ( meta n1 = meta n2 imply UStelescope( meta m , meta n1 ) = UStelescope( meta m , meta n2 ) ) imply for all meta n2 indeed ( meta n1 + 1 = meta n2 imply UStelescope( meta m , meta n1 + 1 ) = UStelescope( meta m , meta n2 ) ) end lemma end math ] "
" [ math system Q proof of lemma sameTelescope second indu reads block any term meta m comma meta n1 comma meta n2 end line block any term meta m comma meta n1 comma meta n2 end line line ell a premise for all meta n2 indeed ( meta n1 = meta n2 imply UStelescope( meta m , meta n1 ) = UStelescope( meta m , meta n2 ) ) end line line ell b premise meta n1 + 1 = meta n2 end line line ell c because lemma +1IsPositive(N) indeed 0 < meta n1 + 1 end line line ell d because 1rule UStelescope positive modus ponens ell c indeed UStelescope( meta m , meta n1 + 1 ) = | [ us ; meta m + ( meta n1 + 1 ) ] - [ us ; meta m + ( meta n1 + 1 + 1 ) ] | + UStelescope( meta m , meta n1 + 1 - 1 ) end line line ell e because lemma x=x+y-y indeed meta n1 = meta n1 + 1 - 1 end line line ell f because lemma a4 at meta n1 + 1 - 1 modus ponens ell a indeed meta n1 = meta n1 + 1 - 1 imply UStelescope( meta m , meta n1 ) = UStelescope( meta m , meta n1 + 1 - 1 ) end line line ell g because 1rule mp modus ponens ell f modus ponens ell e indeed UStelescope( meta m , meta n1 ) = UStelescope( meta m , meta n1 + 1 - 1 ) end line line ell h because lemma eqSymmetry modus ponens ell g indeed UStelescope( meta m , meta n1 + 1 - 1 ) = UStelescope( meta m , meta n1 ) end line line ell i because lemma positiveToRight(Eq) modus ponens ell b indeed meta n1 = meta n2 - 1 end line line ell j because lemma a4 at meta n2 - 1 modus ponens ell a indeed meta n1 = meta n2 - 1 imply UStelescope( meta m , meta n1 ) = UStelescope( meta m , meta n2 - 1 ) end line line ell k because 1rule mp modus ponens ell j modus ponens ell i indeed UStelescope( meta m , meta n1 ) = UStelescope( meta m , meta n2 - 1 ) end line line ell l because lemma eqTransitivity modus ponens ell h modus ponens ell k indeed UStelescope( meta m , meta n1 + 1 - 1 ) = UStelescope( meta m , meta n2 - 1 ) end line line ell m because lemma eqAdditionLeft modus ponens ell b indeed meta m + ( meta n1 + 1 ) = meta m + meta n2 end line line ell big m because lemma eqAddition modus ponens ell b indeed meta n1 + 1 + 1 = meta n2 + 1 end line line ell n because lemma eqAdditionLeft modus ponens ell big m indeed meta m + ( meta n1 + 1 + 1 ) = meta m + ( meta n2 + 1 ) end line line ell o because lemma sameSeries(NumDiff) modus ponens ell m modus ponens ell n indeed | [ us ; meta m + ( meta n1 + 1 ) ] - [ us ; meta m + ( meta n1 + 1 + 1 ) ] | = | [ us ; meta m + meta n2 ] - [ us ; meta m + ( meta n2 + 1 ) ] | end line line ell p because lemma addEquations modus ponens ell o modus ponens ell l indeed | [ us ; meta m + ( meta n1 + 1 ) ] - [ us ; meta m + ( meta n1 + 1 + 1 ) ] | + UStelescope( meta m , meta n1 + 1 - 1 ) = | [ us ; meta m + meta n2 ] - [ us ; meta m + ( meta n2 + 1 ) ] | + UStelescope( meta m , meta n2 - 1 ) end line line ell q because lemma subLessRight modus ponens ell b modus ponens ell c indeed 0 < meta n2 end line line ell r because 1rule UStelescope positive modus ponens ell q indeed UStelescope( meta m , meta n2 ) = | [ us ; meta m + meta n2 ] - [ us ; meta m + ( meta n2 + 1 ) ] | + UStelescope( meta m , meta n2 - 1 ) end line line ell s because lemma eqSymmetry modus ponens ell r indeed | [ us ; meta m + meta n2 ] - [ us ; meta m + ( meta n2 + 1 ) ] | + UStelescope( meta m , meta n2 - 1 ) = UStelescope( meta m , meta n2 ) end line because lemma eqTransitivity4 modus ponens ell d modus ponens ell p modus ponens ell s indeed UStelescope( meta m , meta n1 + 1 ) = UStelescope( meta m , meta n2 ) end line line ell big a end block line ell a because 1rule deduction modus ponens ell big a indeed for all meta n2 indeed ( meta n1 = meta n2 imply UStelescope( meta m , meta n1 ) = UStelescope( meta m , meta n2 ) ) imply meta n1 + 1 = meta n2 imply UStelescope( meta m , meta n1 + 1 ) = UStelescope( meta m , meta n2 ) end line line ell b premise for all meta n2 indeed ( meta n1 = meta n2 imply UStelescope( meta m , meta n1 ) = UStelescope( meta m , meta n2 ) ) end line line ell c because 1rule mp modus ponens ell a modus ponens ell b indeed meta n1 + 1 = meta n2 imply UStelescope( meta m , meta n1 + 1 ) = UStelescope( meta m , meta n2 ) end line because 1rule gen modus ponens ell c indeed for all meta n2 indeed ( meta n1 + 1 = meta n2 imply UStelescope( meta m , meta n1 + 1 ) = UStelescope( meta m , meta n2 ) ) end line line ell big b end block any term meta m comma meta n1 comma meta n2 end line because 1rule deduction modus ponens ell big b indeed for all meta n2 indeed ( meta n1 = meta n2 imply UStelescope( meta m , meta n1 ) = UStelescope( meta m , meta n2 ) ) imply for all meta n2 indeed ( meta n1 + 1 = meta n2 imply UStelescope( meta m , meta n1 + 1 ) = UStelescope( meta m , meta n2 ) ) qed end math ] "
" [ math in theory system Q lemma lemma sameTelescope second says for all terms meta m comma meta n1 comma meta n2 indeed meta n1 = meta n2 infer UStelescope( meta m , meta n1 ) = UStelescope( meta m , meta n2 ) end lemma end math ] "
" [ math system Q proof of lemma sameTelescope second reads any term meta m comma meta n1 comma meta n2 end line line ell big a premise meta n1 = meta n2 end line line ell a because lemma sameTelescope second base indeed for all meta n2 indeed ( 0 = meta n2 imply UStelescope( meta m , 0 ) = UStelescope( meta m , meta n2 ) ) end line line ell b because lemma sameTelescope second indu indeed for all meta n2 indeed ( meta n1 = meta n2 imply UStelescope( meta m , meta n1 ) = UStelescope( meta m , meta n2 ) ) imply for all meta n2 indeed ( meta n1 + 1 = meta n2 imply UStelescope( meta m , meta n1 + 1 ) = UStelescope( meta m , meta n2 ) ) end line line ell c because lemma induction modus ponens ell a modus ponens ell b indeed for all meta n2 indeed ( meta n1 = meta n2 imply UStelescope( meta m , meta n1 ) = UStelescope( meta m , meta n2 ) ) end line line ell d because lemma a4 at meta n2 modus ponens ell c indeed meta n1 = meta n2 imply UStelescope( meta m , meta n1 ) = UStelescope( meta m , meta n2 ) end line because 1rule mp modus ponens ell d modus ponens ell big a indeed UStelescope( meta m , meta n1 ) = UStelescope( meta m , meta n2 ) qed end math ] "
" [ math in theory system Q lemma lemma telescopeNumerical base says for all terms meta m indeed | [ us ; meta m ] - [ us ; meta m + ( 0 + 1 ) ] | <= UStelescope( meta m , 0 ) end lemma end math ] "
" [ math system Q proof of lemma telescopeNumerical base reads any term meta m end line line ell a because lemma eqReflexivity indeed 0 = 0 end line line ell b because 1rule UStelescope zero modus ponens ell a indeed UStelescope( meta m , 0 ) = | [ us ; meta m ] - [ us ; meta m + 1 ] | end line line ell c because lemma eqReflexivity indeed meta m = meta m end line line ell d because lemma plus0Left indeed 0 + 1 = 1 end line line ell e because lemma eqAdditionLeft modus ponens ell d indeed meta m + ( 0 + 1 ) = meta m + 1 end line line ell f because lemma eqSymmetry modus ponens ell e indeed meta m + 1 = meta m + ( 0 + 1 ) end line line ell g because lemma sameSeries(NumDiff) modus ponens ell c modus ponens ell f indeed | [ us ; meta m ] - [ us ; meta m + 1 ] | = | [ us ; meta m ] - [ us ; meta m + ( 0 + 1 ) ] | end line line ell h because lemma eqTransitivity modus ponens ell b modus ponens ell g indeed UStelescope( meta m , 0 ) = | [ us ; meta m ] - [ us ; meta m + ( 0 + 1 ) ] | end line line ell i because lemma eqSymmetry modus ponens ell h indeed | [ us ; meta m ] - [ us ; meta m + ( 0 + 1 ) ] | = UStelescope( meta m , 0 ) end line because lemma eqLeq modus ponens ell i indeed | [ us ; meta m ] - [ us ; meta m + ( 0 + 1 ) ] | <= UStelescope( meta m , 0 ) qed end math ] "
" [ math in theory system Q lemma lemma telescopeNumerical indu says for all terms meta m comma meta n indeed | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 ) ] | <= UStelescope( meta m , meta n ) imply | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | <= UStelescope( meta m , meta n + 1 ) end lemma end math ] "
" [ math system Q proof of lemma telescopeNumerical indu reads block any term meta m comma meta n end line line ell a premise | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 ) ] | <= UStelescope( meta m , meta n ) end line line ell b because lemma +1IsPositive(N) indeed 0 < meta n + 1 end line line ell c because 1rule UStelescope positive modus ponens ell b indeed UStelescope( meta m , meta n + 1 ) = | [ us ; meta m + ( meta n + 1 ) ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | + UStelescope( meta m , meta n + 1 - 1 ) end line line ell d because lemma x=x+y-y indeed meta n = meta n + 1 - 1 end line line ell big d because lemma eqSymmetry modus ponens ell d indeed meta n + 1 - 1 = meta n end line line ell e because lemma sameTelescope second modus ponens ell big d indeed UStelescope( meta m , meta n + 1 - 1 ) = UStelescope( meta m , meta n ) end line line ell f because lemma eqAdditionLeft modus ponens ell e indeed | [ us ; meta m + ( meta n + 1 ) ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | + UStelescope( meta m , meta n + 1 - 1 ) = | [ us ; meta m + ( meta n + 1 ) ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | + UStelescope( meta m , meta n ) end line line ell g because lemma eqTransitivity modus ponens ell c modus ponens ell f indeed UStelescope( meta m , meta n + 1 ) = | [ us ; meta m + ( meta n + 1 ) ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | + UStelescope( meta m , meta n ) end line line ell h because lemma eqSymmetry modus ponens ell g indeed | [ us ; meta m + ( meta n + 1 ) ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | + UStelescope( meta m , meta n ) = UStelescope( meta m , meta n + 1 ) end line line ell i because lemma leqAdditionLeft modus ponens ell a indeed | [ us ; meta m + ( meta n + 1 ) ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | + | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 ) ] | <= | [ us ; meta m + ( meta n + 1 ) ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | + UStelescope( meta m , meta n ) end line line ell j because lemma subLeqRight modus ponens ell h modus ponens ell i indeed | [ us ; meta m + ( meta n + 1 ) ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | + | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 ) ] | <= UStelescope( meta m , meta n + 1 ) end line line ell k because axiom plusCommutativity indeed | [ us ; meta m + ( meta n + 1 ) ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | + | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 ) ] | = | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 ) ] | + | [ us ; meta m + ( meta n + 1 ) ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | end line line ell l because lemma subLeqLeft modus ponens ell k modus ponens ell j indeed | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 ) ] | + | [ us ; meta m + ( meta n + 1 ) ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | <= UStelescope( meta m , meta n + 1 ) end line line ell m because lemma insertMiddleTerm(Numerical) indeed | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | <= | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 ) ] | + | [ us ; meta m + ( meta n + 1 ) ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | end line because lemma leqTransitivity modus ponens ell m modus ponens ell l indeed | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | <= UStelescope( meta m , meta n + 1 ) end line line ell big a end block any term meta m comma meta n end line because 1rule deduction modus ponens ell big a indeed | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 ) ] | <= UStelescope( meta m , meta n ) imply | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | <= UStelescope( meta m , meta n + 1 ) qed end math ] "
" [ math in theory system Q lemma lemma telescopeNumerical says for all terms meta m comma meta n indeed | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 ) ] | <= UStelescope( meta m , meta n ) end lemma end math ] "
" [ math system Q proof of lemma telescopeNumerical reads any term meta m comma meta n end line line ell a because lemma telescopeNumerical base indeed | [ us ; meta m ] - [ us ; meta m + ( 0 + 1 ) ] | <= UStelescope( meta m , 0 ) end line line ell b because lemma telescopeNumerical indu indeed | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 ) ] | <= UStelescope( meta m , meta n ) imply | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 + 1 ) ] | <= UStelescope( meta m , meta n + 1 ) end line because lemma induction modus ponens ell a modus ponens ell b indeed | [ us ; meta m ] - [ us ; meta m + ( meta n + 1 ) ] | <= UStelescope( meta m , meta n ) qed end math ] "
---------------(21.10.06)
" [ math in theory system Q lemma lemma eqAdditionLeft(R) says for all terms meta fx comma meta fy comma meta fz indeed R( meta fx ) == R( meta fy ) infer R( meta fz ) ++ R( meta fx ) == R( meta fz ) ++ R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma eqAdditionLeft(R) reads any term meta fx comma meta fy comma meta fz end line line ell a premise R( meta fx ) == R( meta fy ) end line line ell b because 1rule adhoc eqAddition(R) modus ponens ell a indeed R( meta fx ) ++ R( meta fz ) == R( meta fy ) ++ R( meta fz ) end line line ell c because lemma plusCommutativity(R) indeed R( meta fz ) ++ R( meta fx ) == R( meta fx ) ++ R( meta fz ) end line line ell d because lemma plusCommutativity(R) indeed R( meta fy ) ++ R( meta fz ) == R( meta fz ) ++ R( meta fy ) end line because lemma eqTransitivity4 modus ponens ell c modus ponens ell b modus ponens ell d indeed R( meta fz ) ++ R( meta fx ) == R( meta fz ) ++ R( meta fy ) qed end math ] "
" [ math in theory system Q lemma lemma x=x+(y-y)(R) says for all terms meta fx comma meta fy indeed R( meta fx ) = R( meta fx ) ++ ( R( meta fy ) ++ -- R( meta fy ) ) end lemma end math ] "
" [ math system Q proof of lemma x=x+(y-y)(R) reads any term meta fx comma meta fy end line line ell a because lemma plus0(R) indeed R( meta fx ) ++ 00 == R( meta fx ) end line line ell b because lemma ==Symmetry modus ponens ell a indeed R( meta fx ) == R( meta fx ) ++ 00 end line line ell c because lemma negative(R) indeed R( meta fy ) ++ -- R( meta fy ) == 00 end line line ell d because lemma ==Symmetry modus ponens ell c indeed 00 == R( meta fy ) ++ -- R( meta fy ) end line line ell e because lemma eqAdditionLeft(R) modus ponens ell d indeed R( meta fx ) ++ 00 == R( meta fx ) ++ ( R( meta fy ) ++ -- R( meta fy ) ) end line because lemma eqTransitivity modus ponens ell b modus ponens ell e indeed R( meta fx ) == R( meta fx ) ++ ( R( meta fy ) ++ -- R( meta fy ) ) qed end math ] "
" [ math in theory system Q lemma lemma x=x+y-y(R) says for all terms meta fx comma meta fy indeed R( meta fx ) = R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma x=x+y-y(R) reads any term meta fx comma meta fy end line line ell a because lemma x=x+(y-y)(R) indeed R( meta fx ) == R( meta fx ) ++ ( R( meta fy ) ++ -- R( meta fy ) ) end line line ell b because lemma plusAssociativity(R) indeed R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) == R( meta fx ) ++ ( R( meta fy ) ++ -- R( meta fy ) ) end line line ell c because lemma ==Symmetry modus ponens ell b indeed R( meta fx ) ++ ( R( meta fy ) ++ -- R( meta fy ) ) == R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) end line because lemma eqTransitivity modus ponens ell a modus ponens ell c indeed R( meta fx ) == R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) qed end math ] "
----------(22.10.06)
" [ math in theory system Q lemma lemma three2twoTerms(R) says for all terms meta fx comma meta fy comma meta fz comma meta fu indeed R( meta fy ) ++ R( meta fz ) == R( meta fu ) infer R( meta fx ) ++ R( meta fy ) ++ R( meta fz ) == R( meta fx ) ++ R( meta fu ) end lemma end math ] "
" [ math system Q proof of lemma three2twoTerms(R) reads any term meta fx comma meta fy comma meta fz comma meta fu end line line ell a premise R( meta fy ) ++ R( meta fz ) == R( meta fu ) end line line ell b because lemma eqAdditionLeft(R) modus ponens ell a indeed R( meta fx ) ++ ( R( meta fy ) ++ R( meta fz ) ) == R( meta fx ) ++ R( meta fu ) end line line ell c because lemma plusAssociativity(R) indeed R( meta fx ) ++ R( meta fy ) ++ R( meta fz ) == R( meta fx ) ++ ( R( meta fy ) ++ R( meta fz ) ) end line because lemma eqTransitivity modus ponens ell c modus ponens ell b indeed R( meta fx ) ++ R( meta fy ) ++ R( meta fz ) == R( meta fx ) ++ R( meta fu ) qed end math ] "
" [ math in theory system Q lemma lemma positiveToRight(Less)(R) says for all terms meta fx comma meta fy comma meta fz indeed R( meta fx ) ++ R( meta fy ) << R( meta fz ) infer R( meta fx ) << R( meta fz ) ++ -- R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma positiveToRight(Less)(R) reads any term meta fx comma meta fy comma meta fz end line line ell a premise R( meta fx ) ++ R( meta fy ) << R( meta fz ) end line line ell b because lemma lessAddition(R) modus ponens ell a indeed R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) << R( meta fz ) ++ -- R( meta fy ) end line line ell c because lemma x=x+y-y(R) indeed R( meta fx ) == R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) end line line ell d because lemma ==Symmetry modus ponens ell c indeed R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) == R( meta fx ) end line because lemma subLessLeft(R) modus ponens ell d modus ponens ell b indeed R( meta fx ) << R( meta fz ) ++ -- R( meta fy ) qed end math ] "
" [ math in theory system Q lemma lemma three2threeTerms(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 fz ) ++ R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma three2threeTerms(R) reads any term meta fx comma meta fy comma meta fz end line line ell a because lemma plusCommutativity(R) indeed R( meta fy ) ++ R( meta fz ) == R( meta fz ) ++ R( meta fy ) end line line ell b because lemma three2twoTerms(R) modus ponens ell a indeed R( meta fx ) ++ R( meta fy ) ++ R( meta fz ) == R( meta fx ) ++ ( R( meta fz ) ++ R( meta fy ) ) end line line ell c because lemma plusAssociativity(R) indeed R( meta fx ) ++ R( meta fz ) ++ R( meta fy ) == R( meta fx ) ++ ( R( meta fz ) ++ R( meta fy ) ) end line line ell d because lemma ==Symmetry modus ponens ell c indeed R( meta fx ) ++ ( R( meta fz ) ++ R( meta fy ) ) == R( meta fx ) ++ R( meta fz ) ++ R( meta fy ) end line because lemma eqTransitivity modus ponens ell b modus ponens ell d indeed R( meta fx ) ++ R( meta fy ) ++ R( meta fz ) == R( meta fx ) ++ R( meta fz ) ++ R( meta fy ) qed end math ] "
--------(22.10.06)
" [ math in theory system Q lemma lemma plus0Left(R) says for all terms meta fx indeed 00 ++ R( meta fx ) == R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma plus0Left(R) reads any term meta fx end line line ell a because lemma plus0(R) indeed R( meta fx ) ++ 00 == R( meta fx ) end line line ell b because lemma plusCommutativity(R) indeed 00 ++ R( meta fx ) == R( meta fx ) ++ 00 end line because lemma eqTransitivity modus ponens ell b modus ponens ell a indeed 00 ++ R( meta fx ) == R( meta fx ) qed end math ] "
" [ math in theory system Q lemma lemma positiveToRight(Eq)(R) says for all terms meta fx comma meta fy comma meta fz indeed R( meta fx ) ++ R( meta fy ) == R( meta fz ) infer R( meta fx ) == R( meta fz ) ++ -- R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma positiveToRight(Eq)(R) reads any term meta fx comma meta fy comma meta fz end line line ell a premise R( meta fx ) ++ R( meta fy ) == R( meta fz ) end line line ell b because 1rule adhoc eqAddition(R) modus ponens ell a indeed R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) == R( meta fz ) ++ -- R( meta fy ) end line line ell c because lemma x=x+y-y(R) indeed R( meta fx ) == R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) end line because lemma eqTransitivity modus ponens ell c modus ponens ell b indeed R( meta fx ) == R( meta fz ) ++ -- R( meta fy ) qed end math ] "
" [ math in theory system Q lemma lemma subtractEquations(R) says for all terms meta fx comma meta fy comma meta fz comma meta fu indeed R( meta fx ) ++ R( meta fz ) == R( meta fy ) ++ R( meta fu ) infer R( meta fz ) == R( meta fu ) infer R( meta fx ) == R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma subtractEquations(R) reads any term meta fx comma meta fy comma meta fz comma meta fu end line line ell b premise R( meta fx ) ++ R( meta fz ) == R( meta fy ) ++ R( meta fu ) end line line ell a premise R( meta fz ) == R( meta fu ) end line line ell c because 1rule adhoc eqAddition(R) modus ponens ell b indeed R( meta fx ) ++ R( meta fz ) ++ -- R( meta fz ) == R( meta fy ) ++ R( meta fu ) ++ -- R( meta fz ) end line line ell d because lemma plus0Left(R) indeed 00 ++ R( meta fz ) == R( meta fz ) end line line ell e because lemma eqTransitivity modus ponens ell d modus ponens ell a indeed 00 ++ R( meta fz ) == R( meta fu ) end line line ell f because lemma positiveToRight(Eq)(R) modus ponens ell e indeed 00 == R( meta fu ) ++ -- R( meta fz ) end line line ell g because lemma ==Symmetry modus ponens ell f indeed R( meta fu ) ++ -- R( meta fz ) == 00 end line line ell h because lemma eqAdditionLeft(R) modus ponens ell g indeed R( meta fy ) ++ ( R( meta fu ) ++ -- R( meta fz ) ) == R( meta fy ) ++ 00 end line line ell i because lemma plusAssociativity(R) indeed R( meta fy ) ++ R( meta fu ) ++ -- R( meta fz ) == R( meta fy ) ++ ( R( meta fu ) ++ -- R( meta fz ) ) end line line ell j because lemma plus0(R) indeed R( meta fy ) ++ 00 == R( meta fy ) end line line ell k because lemma eqTransitivity4 modus ponens ell i modus ponens ell h modus ponens ell j indeed R( meta fy ) ++ R( meta fu ) ++ -- R( meta fz ) == R( meta fy ) end line line ell m because lemma x=x+y-y(R) indeed R( meta fx ) == R( meta fx ) ++ R( meta fz ) ++ -- R( meta fz ) end line because lemma eqTransitivity4 modus ponens ell m modus ponens ell c modus ponens ell k indeed R( meta fx ) == R( meta fy ) qed end math ] "
" [ math in theory system Q lemma lemma neqAddition(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 lemma end math ] "
" [ math system Q proof of lemma neqAddition(R) reads block any term meta fx comma meta fy comma meta fz end line line ell big a premise R( meta fx ) != R( meta fy ) end line line ell big b premise R( meta fx ) ++ R( meta fz ) == R( meta fy ) ++ R( meta fz ) end line line ell big c because lemma ==Reflexivity indeed R( meta fz ) == R( meta fz ) end line line ell big d because lemma subtractEquations(R) modus ponens ell big b modus ponens ell big c indeed R( meta fx ) == R( meta fy ) end line because prop lemma from contradiction modus ponens ell big d modus ponens ell big a indeed R( meta fx ) ++ R( meta fz ) != R( meta fy ) ++ R( meta fz ) end line line ell big e end block any term meta fx comma meta fy comma meta fz end line line ell a because 1rule deduction modus ponens ell big e indeed R( meta fx ) != R( meta fy ) imply R( meta fx ) ++ R( meta fz ) == R( meta fy ) ++ R( meta fz ) imply R( meta fx ) ++ R( meta fz ) != R( meta fy ) ++ R( meta fz ) end line line ell b premise R( meta fx ) != R( meta fy ) end line line ell c because 1rule mp modus ponens ell a modus ponens ell b indeed R( meta fx ) ++ R( meta fz ) == R( meta fy ) ++ R( meta fz ) imply R( meta fx ) ++ R( meta fz ) != R( meta fy ) ++ R( meta fz ) end line because prop lemma imply negation modus ponens ell c indeed R( meta fx ) ++ R( meta fz ) != R( meta fy ) ++ R( meta fz ) qed end math ] "
-----------(22.10.06)
" [ math in theory system Q lemma lemma positiveToRight(Less)(1 term)(R) says for all terms meta fx comma meta fy indeed R( meta fx ) << R( meta fy ) infer 00 << R( meta fy ) ++ -- R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma positiveToRight(Less)(1 term)(R) reads any term meta fx comma meta fy end line line ell a premise R( meta fx ) << R( meta fy ) end line line ell b because lemma plus0Left(R) indeed 00 ++ R( meta fx ) == R( meta fx ) end line line ell c because lemma ==Symmetry modus ponens ell b indeed R( meta fx ) == 00 ++ R( meta fx ) end line line ell d because lemma subLessLeft(R) modus ponens ell c modus ponens ell a indeed 00 ++ R( meta fx ) << R( meta fy ) end line because lemma positiveToRight(Less)(R) modus ponens ell d indeed 00 << R( meta fy ) ++ -- R( meta fx ) qed end math ] "
-----------(22.10.06)
" [ math in theory system Q lemma lemma to!!== says for all terms meta m comma meta n comma meta ep comma meta fx comma meta fy indeed not0 meta fx sameF meta fy infer R( meta fx ) !!== R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma to!!== reads block any term meta m comma meta n comma meta ep comma meta fx comma meta fy end line line ell a premise R( meta fx ) == R( meta fy ) end line because 1rule from== modus ponens ell a indeed meta fx sameF meta fy end line line ell big a end block any term meta m comma meta n comma meta ep comma meta fx comma meta fy end line line ell a because 1rule deduction modus ponens ell big a indeed R( meta fx ) == R( meta fy ) imply meta fx sameF meta fy end line line ell b premise not0 meta fx sameF meta fy end line because prop lemma mt modus ponens ell a modus ponens ell b indeed R( meta fx ) !!== R( meta fy ) qed end math ] "
" [ math in theory system Q lemma lemma switchTerms(x<=y-z) says for all terms meta x comma meta y comma meta z indeed meta x <= meta y - meta z infer meta z <= meta y - meta x end lemma end math ] "
" [ math system Q proof of lemma switchTerms(x<=y-z) reads any term meta x comma meta y comma meta z end line line ell a premise meta x <= meta y - meta z end line line ell b because lemma negativeToLeft(Leq) modus ponens ell a indeed meta x + meta z <= meta y end line line ell c because axiom plusCommutativity indeed meta x + meta z = meta z + meta x end line line ell d because lemma subLeqLeft modus ponens ell c modus ponens ell b indeed meta z + meta x <= meta y end line because lemma positiveToRight(Leq) modus ponens ell d indeed meta z <= meta y - meta x qed end math ] "
" [ math in theory system Q lemma lemma lessNeq(F) helper says for all terms meta m comma meta n comma meta ep comma meta fx comma meta fy indeed for all meta m indeed 0 < meta ep and0 ( meta n <= meta m imply [ meta fx ; meta m ] <= [ meta fy ; meta m ] - meta ep ) imply not0 ( 0 < meta ep imply meta n <= meta n imply | [ meta fx ; meta n ] - [ meta fy ; meta n ] | < meta ep ) end lemma end math ] "
" [ math system Q proof of lemma lessNeq(F) helper reads block any term meta m comma meta n comma meta ep comma meta fx comma meta fy end line line ell a premise for all meta m indeed 0 < meta ep and0 ( meta n <= meta m imply [ meta fx ; meta m ] <= [ meta fy ; meta m ] - meta ep ) end line line ell b because lemma a4 at meta n modus ponens ell a indeed 0 < meta ep and0 ( meta n <= meta n imply [ meta fx ; meta n ] <= [ meta fy ; meta n ] - meta ep ) end line line ell c because prop lemma first conjunct modus ponens ell b indeed 0 < meta ep end line line ell d because prop lemma second conjunct modus ponens ell b indeed meta n <= meta n imply [ meta fx ; meta n ] <= [ meta fy ; meta n ] - meta ep end line line ell e because axiom leqReflexivity indeed meta n <= meta n end line line ell f because 1rule mp modus ponens ell d modus ponens ell e indeed [ meta fx ; meta n ] <= [ meta fy ; meta n ] - meta ep end line line ell g because lemma switchTerms(x<=y-z) modus ponens ell f indeed meta ep <= [ meta fy ; meta n ] - [ meta fx ; meta n ] end line line ell h because lemma x<=|x| indeed [ meta fy ; meta n ] - [ meta fx ; meta n ] <= | [ meta fy ; meta n ] - [ meta fx ; meta n ] | end line line ell i because lemma leqTransitivity modus ponens ell g modus ponens ell h indeed meta ep <= | [ meta fy ; meta n ] - [ meta fx ; meta n ] | end line line ell j because lemma numericalDifference indeed | [ meta fy ; meta n ] - [ meta fx ; meta n ] | = | [ meta fx ; meta n ] - [ meta fy ; meta n ] | end line line ell k because lemma subLeqRight modus ponens ell j modus ponens ell i indeed meta ep <= | [ meta fx ; meta n ] - [ meta fy ; meta n ] | end line line ell l because lemma toNotLess modus ponens ell k indeed not0 | [ meta fx ; meta n ] - [ meta fy ; meta n ] | < meta ep end line because prop lemma to negated double imply modus ponens ell c modus ponens ell e modus ponens ell l indeed not0 ( 0 < meta ep imply meta n <= meta n imply | [ meta fx ; meta n ] - [ meta fy ; meta n ] | < meta ep ) end line line ell big a end block any term meta m comma meta n comma meta ep comma meta fx comma meta fy end line because 1rule deduction modus ponens ell big a indeed for all meta m indeed 0 < meta ep and0 ( meta n <= meta m imply [ meta fx ; meta m ] <= [ meta fy ; meta m ] - meta ep ) imply not0 ( 0 < meta ep imply meta n <= meta n imply | [ meta fx ; meta n ] - [ meta fy ; meta n ] | < meta ep ) qed end math ] "
" [ math in theory system Q lemma lemma lessNeq(F) says for all terms meta m comma meta n comma meta ep comma meta fx comma meta fy indeed meta fx
" [ math system Q proof of lemma lessNeq(F) reads any term meta m comma meta n comma meta ep comma meta fx comma meta fy end line line ell a premise meta fx
" [ math in theory system Q lemma lemma lessNeq(R) says for all terms meta fx comma meta fy indeed R( meta fx ) << R( meta fy ) infer R( meta fx ) !!== R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma lessNeq(R) reads any term meta fx comma meta fy end line line ell a premise R( meta fx ) << R( meta fy ) end line line ell b because 1rule repetition modus ponens ell a indeed meta fx
" [ math in theory system Q lemma lemma positiveToRight(Less)(1 term) says for all terms meta x comma meta y indeed meta x < meta y infer 0 < meta y - meta x end lemma end math ] "
" [ math system Q proof of lemma positiveToRight(Less)(1 term) reads any term meta x comma meta y end line line ell a premise meta x < meta y end line line ell b because lemma plus0Left indeed 0 + meta x = meta x end line line ell c because lemma eqSymmetry modus ponens ell b indeed meta x = 0 + meta x end line line ell d because lemma subLessLeft modus ponens ell c modus ponens ell a indeed 0 + meta x < meta y end line because lemma positiveToRight(Less) modus ponens ell d indeed 0 < meta y - meta x qed end math ] "
" [ math in theory system Q lemma lemma toLeq(Advanced)(R) says for all terms meta fep comma meta fx comma meta fy indeed 00 << R( meta fep ) imply R( meta fx ) ++ R( meta fep ) != R( meta fy ) infer R( meta fy ) <<== R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma toLeq(Advanced)(R) reads block any term meta fep comma meta fx comma meta fy end line line ell a premise R( meta fx ) << R( meta fy ) end line line ell b because lemma positiveToRight(Less)(1 term)(R) modus ponens ell a indeed 00 << R( meta fy ) ++ -- R( meta fx ) end line line ell c because lemma plusCommutativity(R) indeed R( meta fx ) ++ ( R( meta fy ) ++ -- R( meta fx ) ) = R( meta fy ) ++ -- R( meta fx ) ++ R( meta fx ) end line line ell d because lemma three2threeTerms(R) indeed R( meta fy ) ++ -- R( meta fx ) ++ R( meta fx ) = R( meta fy ) ++ R( meta fx ) ++ -- R( meta fx ) end line line ell e because lemma x=x+y-y(R) indeed R( meta fy ) = R( meta fy ) ++ R( meta fx ) ++ -- R( meta fx ) end line line ell f because lemma ==Symmetry modus ponens ell e indeed R( meta fy ) ++ R( meta fx ) ++ -- R( meta fx ) == R( meta fy ) end line line ell g because lemma eqTransitivity4 modus ponens ell c modus ponens ell d modus ponens ell f indeed R( meta fx ) ++ ( R( meta fy ) ++ -- R( meta fx ) ) == R( meta fy ) end line line ell h because prop lemma join conjuncts modus ponens ell b modus ponens ell g indeed 00 << R( meta fy ) ++ -- R( meta fx ) and0 R( meta fx ) ++ ( R( meta fy ) ++ -- R( meta fx ) ) = R( meta fy ) end line because pred lemma intro exist at R( meta fy ) ++ -- R( meta fx ) modus ponens ell h indeed exist0 meta fep indeed 00 << R( meta fep ) and0 R( meta fx ) ++ R( meta fep ) == R( meta fy ) end line line ell big a end block any term meta fep comma meta fx comma meta fy end line line ell a because 1rule deduction modus ponens ell big a indeed R( meta fx ) << R( meta fy ) imply exist0 meta fep indeed 00 << R( meta fep ) and0 R( meta fx ) ++ R( meta fep ) == R( meta fy ) end line line ell b premise 00 << R( meta fep ) imply R( meta fx ) ++ R( meta fep ) !!== R( meta fy ) end line line ell c because prop lemma to negated and modus ponens ell b indeed not0 ( 00 << R( meta fep ) and0 R( meta fx ) ++ R( meta fep ) == R( meta fy ) ) end line line ell d because 1rule gen modus ponens ell c indeed for all meta fep indeed not0 ( 00 << R( meta fep ) and0 R( meta fx ) ++ R( meta fep ) == R( meta fy ) ) end line line ell e because pred lemma (A~)to(~E) modus ponens ell d indeed not0 exist0 meta fep indeed 00 << R( meta fep ) and0 R( meta fx ) ++ R( meta fep ) == R( meta fy ) end line line ell f because prop lemma mt modus ponens ell a modus ponens ell e indeed not0 R( meta fx ) << R( meta fy ) end line because lemma fromNotLess(R) modus ponens ell f indeed R( meta fy ) <<== R( meta fx ) qed end math ] "
--------(23.10.06)
" [ math in theory system Q lemma lemma leqNeqLess(R) says for all terms meta fx comma meta fy indeed R( meta fx ) <<== R( meta fy ) infer R( meta fx ) !!== R( meta fy ) infer R( meta fx ) << R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma leqNeqLess(R) reads block any term meta fx comma meta fy end line line ell a premise R( meta fx ) <<== R( meta fy ) end line line ell b premise R( meta fx ) !!== R( meta fy ) end line line ell c premise R( meta fy ) <<== R( meta fx ) end line line ell d because lemma leqAntisymmetry(R) modus ponens ell a modus ponens ell c indeed R( meta fx ) == R( meta fy ) end line because prop lemma from contradiction modus ponens ell d modus ponens ell b indeed not0 R( meta fy ) <<== R( meta fx ) end line line ell big a end block any term meta fx comma meta fy end line line ell a because 1rule deduction modus ponens ell big a indeed R( meta fx ) <<== R( meta fy ) imply R( meta fx ) !!== R( meta fy ) imply R( meta fy ) <<== R( meta fx ) imply not0 R( meta fy ) <<== R( meta fx ) end line line ell b premise R( meta fx ) <<== R( meta fy ) end line line ell c premise R( meta fx ) !!== R( meta fy ) end line line ell d because prop lemma mp2 modus ponens ell a modus ponens ell b modus ponens ell c indeed R( meta fy ) <<== R( meta fx ) imply not0 R( meta fy ) <<== R( meta fx ) end line line ell e because prop lemma imply negation modus ponens ell d indeed not0 R( meta fy ) <<== R( meta fx ) end line because lemma toLess(R) modus ponens ell e indeed R( meta fx ) << R( meta fy ) qed end math ] "
" [ math in theory system Q lemma lemma subLeqLeft(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 ) infer R( meta fy ) <<== R( meta fz ) end lemma end math ] "
" [ math system Q proof of lemma subLeqLeft(R) reads any term meta fx comma meta fy comma meta fz end line line ell a premise R( meta fx ) == R( meta fy ) end line line ell b premise R( meta fx ) <<== R( meta fz ) end line line ell c because lemma ==Symmetry modus ponens ell a indeed R( meta fy ) == R( meta fx ) end line line ell d because lemma eqLeq(R) modus ponens ell c indeed R( meta fy ) <<== R( meta fx ) end line because lemma leqTransitivity(R) modus ponens ell d modus ponens ell b indeed R( meta fy ) <<== R( meta fz ) qed end math ] "
" [ math in theory system Q lemma lemma leqLessTransitivity(R) says for all terms meta fx comma meta fy comma meta fz indeed R( meta fx ) <<== R( meta fy ) infer R( meta fy ) << R( meta fz ) infer R( meta fx ) << R( meta fz ) end lemma end math ] "
" [ math system Q proof of lemma leqLessTransitivity(R) reads block any term meta fx comma meta fy comma meta fz end line line ell a premise R( meta fx ) <<== R( meta fy ) end line line ell b premise R( meta fy ) << R( meta fz ) end line line ell big a premise R( meta fx ) == R( meta fz ) end line line ell c because lemma lessLeq(R) modus ponens ell b indeed R( meta fy ) <<== R( meta fz ) end line line ell d because lemma lessNeq(R) modus ponens ell b indeed R( meta fy ) !!== R( meta fz ) end line line ell f because lemma subLeqLeft(R) modus ponens ell big a modus ponens ell a indeed R( meta fz ) <<== R( meta fy ) end line line ell g because lemma leqAntisymmetry(R) modus ponens ell c modus ponens ell f indeed R( meta fy ) == R( meta fz ) end line because prop lemma from contradiction modus ponens ell g modus ponens ell d indeed R( meta fx ) !!== R( meta fz ) end line line ell h end block any term meta fx comma meta fy comma meta fz end line line ell i because 1rule deduction modus ponens ell h indeed R( meta fx ) <<== R( meta fy ) imply R( meta fy ) << R( meta fz ) imply R( meta fx ) == R( meta fz ) imply R( meta fx ) !!== R( meta fz ) end line line ell j premise R( meta fx ) <<== R( meta fy ) end line line ell k premise R( meta fy ) << R( meta fz ) end line line ell l because prop lemma mp2 modus ponens ell i modus ponens ell j modus ponens ell k indeed R( meta fx ) == R( meta fz ) imply R( meta fx ) !!== R( meta fz ) end line line ell m because prop lemma imply negation modus ponens ell l indeed R( meta fx ) !!== R( meta fz ) end line line ell o because lemma lessLeq(R) modus ponens ell k indeed R( meta fy ) <<== R( meta fz ) end line line ell q because lemma leqTransitivity(R) modus ponens ell j modus ponens ell o indeed R( meta fx ) <<== R( meta fz ) end line because lemma leqNeqLess(R) modus ponens ell q modus ponens ell m indeed R( meta fx ) << R( meta fz ) qed end math ] "
-----------(23.10.06)
" [ math in theory system Q lemma lemma negativeToLeft(Eq)(R) says for all terms meta fx comma meta fy comma meta fz indeed R( meta fx ) == R( meta fy ) ++ -- R( meta fz ) infer R( meta fx ) ++ R( meta fz ) == R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma negativeToLeft(Eq)(R) reads any term meta fx comma meta fy comma meta fz end line line ell a premise R( meta fx ) == R( meta fy ) ++ -- R( meta fz ) end line line ell b because 1rule adhoc eqAddition(R) modus ponens ell a indeed R( meta fx ) ++ R( meta fz ) == R( meta fy ) ++ -- R( meta fz ) ++ R( meta fz ) end line line ell c because lemma three2threeTerms(R) indeed R( meta fy ) ++ -- R( meta fz ) ++ R( meta fz ) == R( meta fy ) ++ R( meta fz ) ++ -- R( meta fz ) end line line ell d because lemma x=x+y-y(R) indeed R( meta fy ) == R( meta fy ) ++ R( meta fz ) ++ -- R( meta fz ) end line line ell e because lemma ==Symmetry modus ponens ell d indeed R( meta fy ) ++ R( meta fz ) ++ -- R( meta fz ) == R( meta fy ) end line because lemma eqTransitivity4 modus ponens ell b modus ponens ell c modus ponens ell e indeed R( meta fx ) ++ R( meta fz ) == R( meta fy ) qed end math ] "
" [ math in theory system Q lemma lemma negativeToRight(Less)(R) says for all terms meta fx comma meta fy comma meta fz indeed R( meta fx ) ++ -- R( meta fy ) << R( meta fz ) infer R( meta fx ) << R( meta fz ) ++ R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma negativeToRight(Less)(R) reads any term meta fx comma meta fy comma meta fz end line line ell a premise R( meta fx ) ++ -- R( meta fy ) << R( meta fz ) end line line ell b because lemma lessAddition(R) modus ponens ell a indeed R( meta fx ) ++ -- R( meta fy ) ++ R( meta fy ) << R( meta fz ) ++ R( meta fy ) end line line ell c because lemma three2threeTerms(R) indeed R( meta fx ) ++ -- R( meta fy ) ++ R( meta fy ) == R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) end line line ell d because lemma x=x+y-y(R) indeed R( meta fx ) == R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) end line line ell e because lemma ==Symmetry modus ponens ell d indeed R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) == R( meta fx ) end line line ell f because lemma eqTransitivity modus ponens ell c modus ponens ell e indeed R( meta fx ) ++ -- R( meta fy ) ++ R( meta fy ) == R( meta fx ) end line because lemma subLessLeft(R) modus ponens ell f modus ponens ell b indeed R( meta fx ) << R( meta fz ) ++ R( meta fy ) qed end math ] "
" [ math in theory system Q lemma lemma !!==Symmetry says for all terms meta fx comma meta fy indeed R( meta fx ) !!== R( meta fy ) infer R( meta fy ) !!== R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma !!==Symmetry reads block any term meta fx comma meta fy end line line ell a premise R( meta fy ) == R( meta fx ) end line because lemma ==Symmetry modus ponens ell a indeed R( meta fx ) == R( meta fy ) end line line ell b end block any term meta fx comma meta fy end line line ell c because 1rule deduction modus ponens ell b indeed R( meta fy ) == R( meta fx ) imply R( meta fx ) == R( meta fy ) end line line ell d premise R( meta fx ) !!== R( meta fy ) end line because prop lemma mt modus ponens ell c modus ponens ell d indeed R( meta fy ) !!== R( meta fx ) qed end math ] "
-------------(23.10.06)
" [ math in theory system Q lemma lemma negativeToRight(Eq)(R) says for all terms meta fx comma meta fy comma meta fz indeed R( meta fx ) ++ -- R( meta fy ) == R( meta fz ) infer R( meta fx ) == R( meta fz ) ++ R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma negativeToRight(Eq)(R) reads any term meta fx comma meta fy comma meta fz end line line ell a premise R( meta fx ) ++ -- R( meta fy ) == R( meta fz ) end line line ell b because 1rule adhoc eqAddition(R) modus ponens ell a indeed R( meta fx ) ++ -- R( meta fy ) ++ R( meta fy ) == R( meta fz ) ++ R( meta fy ) end line line ell c because lemma x=x+y-y(R) indeed R( meta fx ) == R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) end line line ell e because lemma three2threeTerms(R) indeed R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) == R( meta fx ) ++ -- R( meta fy ) ++ R( meta fy ) end line because lemma eqTransitivity4 modus ponens ell c modus ponens ell e modus ponens ell b indeed R( meta fx ) == R( meta fz ) ++ R( meta fy ) qed end math ] "
" [ math in theory system Q lemma lemma negativeToRight(Eq)(1 term)(R) says for all terms meta fx comma meta fy indeed R( meta fx ) ++ -- R( meta fy ) == 00 infer R( meta fx ) == R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma negativeToRight(Eq)(1 term)(R) reads any term meta fx comma meta fy end line line ell a premise R( meta fx ) ++ -- R( meta fy ) == 00 end line line ell b because lemma negativeToRight(Eq)(R) modus ponens ell a indeed R( meta fx ) == 00 ++ R( meta fy ) end line line ell c because lemma plus0Left(R) indeed 00 ++ R( meta fy ) == R( meta fy ) end line because lemma eqTransitivity modus ponens ell b modus ponens ell c indeed R( meta fx ) == R( meta fy ) qed end math ] "
" [ math in theory system Q lemma lemma doubleMinus(R) says for all terms meta fx indeed -- -- R( meta fx ) == R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma doubleMinus(R) reads any term meta fx end line line ell a because lemma negative(R) indeed -- R( meta fx ) ++ -- -- R( meta fx ) == 00 end line line ell b because lemma plusCommutativity(R) indeed -- R( meta fx ) ++ -- -- R( meta fx ) == -- -- R( meta fx ) ++ -- R( meta fx ) end line line ell c because lemma ==Symmetry modus ponens ell b indeed -- -- R( meta fx ) ++ -- R( meta fx ) == -- R( meta fx ) ++ -- -- R( meta fx ) end line line ell d because lemma eqTransitivity modus ponens ell c modus ponens ell a indeed -- -- R( meta fx ) ++ -- R( meta fx ) == 00 end line because lemma negativeToRight(Eq)(1 term)(R) modus ponens ell d indeed -- -- R( meta fx ) == R( meta fx ) qed end math ] "
" [ math in theory system Q lemma lemma uniqueNegative(R) says for all terms meta fx comma meta fy comma meta fz indeed R( meta fx ) ++ R( meta fy ) == 00 infer R( meta fx ) ++ R( meta fz ) == 00 infer R( meta fy ) == R( meta fz ) end lemma end math ] "
" [ math system Q proof of lemma uniqueNegative(R) reads any term meta fx comma meta fy comma meta fz end line line ell a premise R( meta fx ) ++ R( meta fy ) == 00 end line line ell b premise R( meta fx ) ++ R( meta fz ) == 00 end line line ell c because lemma plusCommutativity(R) indeed R( meta fy ) ++ R( meta fx ) == R( meta fx ) ++ R( meta fy ) end line line ell d because lemma eqTransitivity modus ponens ell c modus ponens ell a indeed R( meta fy ) ++ R( meta fx ) == 00 end line line ell e because lemma positiveToRight(Eq)(R) modus ponens ell d indeed R( meta fy ) == 00 ++ -- R( meta fx ) end line line ell f because lemma plusCommutativity(R) indeed R( meta fz ) ++ R( meta fx ) == R( meta fx ) ++ R( meta fz ) end line line ell g because lemma eqTransitivity modus ponens ell f modus ponens ell b indeed R( meta fz ) ++ R( meta fx ) == 00 end line line ell h because lemma positiveToRight(Eq)(R) modus ponens ell g indeed R( meta fz ) == 00 ++ -- R( meta fx ) end line line ell i because lemma ==Symmetry modus ponens ell h indeed 00 ++ -- R( meta fx ) == R( meta fz ) end line because lemma eqTransitivity modus ponens ell e modus ponens ell i indeed R( meta fy ) == R( meta fz ) qed end math ] "
" [ math in theory system Q lemma lemma subtractEquationsLeft(R) says for all terms meta fx comma meta fy comma meta fz comma meta fu indeed R( meta fx ) ++ R( meta fz ) == R( meta fy ) ++ R( meta fu ) infer R( meta fx ) == R( meta fy ) infer R( meta fz ) == R( meta fu ) end lemma end math ] "
" [ math system Q proof of lemma subtractEquationsLeft(R) reads any term meta fx comma meta fy comma meta fz comma meta fu end line line ell b premise R( meta fx ) ++ R( meta fz ) == R( meta fy ) ++ R( meta fu ) end line line ell a premise R( meta fx ) == R( meta fy ) end line line ell c because lemma plusCommutativity(R) indeed R( meta fz ) ++ R( meta fx ) == R( meta fx ) ++ R( meta fz ) end line line ell d because lemma plusCommutativity(R) indeed R( meta fy ) ++ R( meta fu ) == R( meta fu ) ++ R( meta fy ) end line line ell e because lemma eqTransitivity4 modus ponens ell c modus ponens ell b modus ponens ell d indeed R( meta fz ) ++ R( meta fx ) == R( meta fu ) ++ R( meta fy ) end line because lemma subtractEquations(R) modus ponens ell e modus ponens ell a indeed R( meta fz ) == R( meta fu ) qed end math ] "
" [ math in theory system Q lemma lemma eqNegated(R) says for all terms meta fx comma meta fy indeed R( meta fx ) == R( meta fy ) infer -- R( meta fx ) == -- R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma eqNegated(R) reads any term meta fx comma meta fy end line line ell a premise R( meta fx ) == R( meta fy ) end line line ell b because lemma negative(R) indeed R( meta fx ) ++ -- R( meta fx ) == 00 end line line ell c because lemma negative(R) indeed R( meta fy ) ++ -- R( meta fy ) == 00 end line line ell d because lemma ==Symmetry modus ponens ell c indeed 00 == R( meta fy ) ++ -- R( meta fy ) end line line ell e because lemma eqTransitivity modus ponens ell b modus ponens ell d indeed R( meta fx ) ++ -- R( meta fx ) == R( meta fy ) ++ -- R( meta fy ) end line because lemma subtractEquationsLeft(R) modus ponens ell e modus ponens ell a indeed -- R( meta fx ) == -- R( meta fy ) qed end math ] "
" [ math in theory system Q lemma lemma neqNegated(R) says for all terms meta fx comma meta fy indeed R( meta fx ) !!== R( meta fy ) infer -- R( meta fx ) !!== -- R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma neqNegated(R) reads block any term meta fx comma meta fy end line line ell big a premise R( meta fx ) !!== R( meta fy ) end line line ell big b premise -- R( meta fx ) == -- R( meta fy ) end line line ell big c because lemma eqNegated(R) modus ponens ell big b indeed -- -- R( meta fx ) == -- -- R( meta fy ) end line line ell big d because lemma doubleMinus(R) indeed -- -- R( meta fx ) == R( meta fx ) end line line ell big e because lemma ==Symmetry modus ponens ell big d indeed R( meta fx ) == -- -- R( meta fx ) end line line ell big f because lemma doubleMinus(R) indeed -- -- R( meta fy ) == R( meta fy ) end line line ell big g because lemma eqTransitivity4 modus ponens ell big e modus ponens ell big c modus ponens ell big f indeed R( meta fx ) == R( meta fy ) end line because prop lemma from contradiction modus ponens ell big g modus ponens ell big a indeed -- R( meta fx ) !!== -- R( meta fy ) end line line ell big h end block any term meta fx comma meta fy end line line ell a because 1rule deduction modus ponens ell big h indeed R( meta fx ) !!== R( meta fy ) imply -- R( meta fx ) == -- R( meta fy ) imply not0 -- R( meta fx ) == -- R( meta fy ) end line line ell b premise R( meta fx ) !!== R( meta fy ) end line line ell c because 1rule mp modus ponens ell a modus ponens ell b indeed -- R( meta fx ) == -- R( meta fy ) imply not0 -- R( meta fx ) == -- R( meta fy ) end line because prop lemma imply negation modus ponens ell c indeed not0 -- R( meta fx ) == -- R( meta fy ) qed end math ] "
-----------(23.10.06)
" [ math in theory system Q lemma lemma subLeqRight(R) says for all terms meta fx comma meta fy comma meta fz indeed R( meta fx ) == R( meta fy ) infer R( meta fz ) <<== R( meta fx ) infer R( meta fz ) <<== R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma subLeqRight(R) reads any term meta fx comma meta fy comma meta fz end line line ell a premise R( meta fx ) == R( meta fy ) end line line ell b premise R( meta fz ) <<== R( meta fx ) end line line ell c because lemma eqLeq(R) modus ponens ell a indeed R( meta fx ) <<== R( meta fy ) end line because lemma leqTransitivity(R) modus ponens ell b modus ponens ell c indeed R( meta fz ) <<== R( meta fy ) qed end math ] "
" [ math in theory system Q lemma lemma leqNegated(R) says for all terms meta fx comma meta fy indeed R( meta fx ) <<== R( meta fy ) infer -- R( meta fy ) <<== -- R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma leqNegated(R) reads any term meta fx comma meta fy end line line ell a premise R( meta fx ) <<== R( meta fy ) end line line ell b because lemma leqAddition(R) modus ponens ell a indeed R( meta fx ) ++ -- R( meta fx ) <<== R( meta fy ) ++ -- R( meta fx ) end line line ell c because lemma negative(R) indeed R( meta fx ) ++ -- R( meta fx ) == 00 end line line ell d because lemma subLeqLeft(R) modus ponens ell c modus ponens ell b indeed 00 <<== R( meta fy ) ++ -- R( meta fx ) end line line ell e because lemma plusCommutativity(R) indeed R( meta fy ) ++ -- R( meta fx ) == -- R( meta fx ) ++ R( meta fy ) end line line ell f because lemma subLeqRight(R) modus ponens ell e modus ponens ell d indeed 00 <<== -- R( meta fx ) ++ R( meta fy ) end line line ell g because lemma leqAddition(R) modus ponens ell f indeed 00 ++ -- R( meta fy ) <<== -- R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) end line line ell h because lemma plus0Left(R) indeed 00 ++ -- R( meta fy ) == -- R( meta fy ) end line line ell i because lemma x=x+y-y(R) indeed -- R( meta fx ) == -- R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) end line line ell j because lemma ==Symmetry modus ponens ell i indeed -- R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) == -- R( meta fx ) end line line ell k because lemma subLeqLeft(R) modus ponens ell h modus ponens ell g indeed -- R( meta fy ) <<== -- R( meta fx ) ++ R( meta fy ) ++ -- R( meta fy ) end line because lemma subLeqRight(R) modus ponens ell j modus ponens ell k indeed -- R( meta fy ) <<== -- R( meta fx ) qed end math ] "
" [ math in theory system Q lemma lemma lessNegated(R) says for all terms meta fx comma meta fy indeed R( meta fx ) << R( meta fy ) infer -- R( meta fy ) << -- R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma lessNegated(R) reads any term meta fx comma meta fy end line line ell a premise R( meta fx ) << R( meta fy ) end line line ell b because lemma lessLeq(R) modus ponens ell a indeed R( meta fx ) <<== R( meta fy ) end line line ell c because lemma leqNegated(R) modus ponens ell b indeed -- R( meta fy ) <<== -- R( meta fx ) end line line ell d because lemma lessNeq(R) modus ponens ell a indeed R( meta fx ) !!== R( meta fy ) end line line ell e because lemma neqNegated(R) modus ponens ell d indeed -- R( meta fx ) !!== -- R( meta fy ) end line line ell f because lemma !!==Symmetry modus ponens ell e indeed -- R( meta fy ) !!== -- R( meta fx ) end line because lemma leqNeqLess(R) modus ponens ell c modus ponens ell f indeed -- R( meta fy ) << -- R( meta fx ) qed end math ] "
" [ math in theory system Q lemma lemma -0=0(R) says -- 00 == 00 end lemma end math ] "
" [ math system Q proof of lemma -0=0(R) reads line ell a because lemma negative(R) indeed 00 ++ -- 00 == 00 end line line ell b because lemma plus0(R) indeed 00 ++ 00 == 00 end line because lemma uniqueNegative(R) modus ponens ell a modus ponens ell b indeed -- 00 == 00 qed end math ] "
" [ math in theory system Q lemma lemma negativeNegated(R) says for all terms meta fx indeed R( meta fx ) << 00 infer 00 << -- R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma negativeNegated(R) reads any term meta fx end line line ell a premise R( meta fx ) << 00 end line line ell b because lemma lessNegated(R) modus ponens ell a indeed -- 00 << -- R( meta fx ) end line line ell c because lemma -0=0(R) indeed -- 00 == 00 end line because lemma subLessLeft(R) modus ponens ell c modus ponens ell b indeed 00 << -- R( meta fx ) qed end math ] "
" [ math in theory system Q lemma lemma leqTotality(R) says for all terms meta fx comma meta fy indeed R( meta fx ) <<== R( meta fy ) or0 R( meta fy ) <<== R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma leqTotality(R) reads block any term meta fx comma meta fy end line line ell a premise not0 R( meta fx ) <<== R( meta fy ) end line line ell b because lemma toLess(R) modus ponens ell a indeed R( meta fy ) << R( meta fx ) end line because lemma lessLeq(R) modus ponens ell b indeed R( meta fy ) <<== R( meta fx ) end line line ell big a end block any term meta fx comma meta fy end line line ell a because 1rule deduction modus ponens ell big a indeed not0 R( meta fx ) <<== R( meta fy ) imply R( meta fy ) <<== R( meta fx ) end line because 1rule repetition modus ponens ell a indeed R( meta fx ) <<== R( meta fy ) or0 R( meta fy ) <<== R( meta fx ) qed end math ] "
" [ math in theory system Q lemma lemma from leqGeq(R) says for all terms meta a comma meta fx comma meta fy indeed R( meta fx ) <<== R( meta fy ) imply meta a infer R( meta fy ) <<== R( meta fx ) imply meta a infer meta a end lemma end math ] "
" [ math system Q proof of lemma from leqGeq(R) reads any term meta a comma meta fx comma meta fy end line line ell a premise R( meta fx ) <<== R( meta fy ) imply meta a end line line ell b premise R( meta fy ) <<== R( meta fx ) imply meta a end line line ell c because lemma leqTotality(R) indeed R( meta fx ) <<== R( meta fy ) or0 R( meta fy ) <<== R( meta fx ) end line because prop lemma from disjuncts modus ponens ell c modus ponens ell a modus ponens ell b indeed meta a qed end math ] "
--------(24.10.06)
" [ math in theory system Q lemma lemma fromLess(R) says for all terms meta fx comma meta fy indeed R( meta fx ) << R( meta fy ) infer not0 R( meta fy ) <<== R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma fromLess(R) reads block any term meta fx comma meta fy end line line ell a premise R( meta fx ) << R( meta fy ) end line line ell b premise R( meta fy ) <<== R( meta fx ) end line line ell c because lemma lessLeq(R) modus ponens ell a indeed R( meta fx ) <<== R( meta fy ) end line line ell d because lemma leqAntisymmetry(R) modus ponens ell c modus ponens ell b indeed R( meta fx ) == R( meta fy ) end line line ell e because lemma lessNeq(R) modus ponens ell a indeed R( meta fx ) !!== R( meta fy ) end line because prop lemma from contradiction modus ponens ell d modus ponens ell e indeed not0 R( meta fy ) <<== R( meta fx ) end line line ell big a end block any term meta fx comma meta fy end line line ell a because 1rule deduction modus ponens ell big a indeed R( meta fx ) << R( meta fy ) imply R( meta fy ) <<== R( meta fx ) imply not0 R( meta fy ) <<== R( meta fx ) end line line ell b premise R( meta fx ) << R( meta fy ) end line line ell c because 1rule mp modus ponens ell a modus ponens ell b indeed R( meta fy ) <<== R( meta fx ) imply not0 R( meta fy ) <<== R( meta fx ) end line because prop lemma imply negation modus ponens ell c indeed not0 R( meta fy ) <<== R( meta fx ) qed end math ] "
" [ math in theory system Q lemma lemma from<<== says for all terms meta fx comma meta fy indeed R( meta fx ) <<== R( meta fy ) infer meta fx <=f meta fy end lemma end math ] "
" [ math system Q proof of lemma from<<== reads any term meta fx comma meta fy end line line ell a premise R( meta fx ) <<== R( meta fy ) end line line ell b because 1rule repetition modus ponens ell a indeed R( meta fx ) << R( meta fy ) or0 R( meta fx ) = R( meta fy ) end line line ell c because 1rule repetition modus ponens ell b indeed meta fx
" [ math in theory system Q lemma lemma nonnegativeNumerical(F) says for all terms meta fx indeed 0f <=f meta fx infer |f meta fx | = meta fx end lemma end math ] "
" [ math system Q proof of lemma nonnegativeNumerical(F) reads any term meta fx end line line ell a premise 0f <=f meta fx end line line ell b because axiom numericalF indeed ( 0f <=f meta fx imply |f meta fx | = meta fx ) and0 ( not0 0f <=f meta fx imply |f meta fx | = -f meta fx ) end line line ell c because prop lemma first conjunct modus ponens ell b indeed 0f <=f meta fx imply |f meta fx | = meta fx end line because 1rule mp modus ponens ell c modus ponens ell a indeed |f meta fx | = meta fx qed end math ] "
" [ math in theory system Q lemma lemma nonnegativeNumerical(R) says for all terms meta fx indeed 00 <<== R( meta fx ) infer |r R( meta fx ) | = R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma nonnegativeNumerical(R) reads any term meta fx end line line ell a premise 00 <<== R( meta fx ) end line line ell b because lemma from<<== modus ponens ell a indeed 0f <=f meta fx end line line ell c because lemma nonnegativeNumerical(F) modus ponens ell b indeed |f meta fx | = meta fx end line line ell d because 1rule adhoc sameR modus ponens ell c indeed R( |f meta fx | ) = R( meta fx ) end line because 1rule repetition modus ponens ell d indeed |r R( meta fx ) | = R( meta fx ) qed end math ] "
" [ math in theory system Q lemma lemma to<<== says for all terms meta fx comma meta fy indeed meta fx <=f meta fy infer R( meta fx ) <<== R( meta fy ) end lemma end math ] "
" [ math system Q proof of lemma to<<== reads any term meta fx comma meta fy end line line ell a premise meta fx <=f meta fy end line line ell b because 1rule repetition modus ponens ell a indeed meta fx
" [ math in theory system Q lemma lemma negativeNumerical(F) says for all terms meta fx indeed not0 0f <=f meta fx infer |f meta fx | = -f meta fx end lemma end math ] "
" [ math system Q proof of lemma negativeNumerical(F) reads any term meta fx end line line ell a premise not0 0f <=f meta fx end line line ell b because axiom numericalF indeed ( 0f <=f meta fx imply |f meta fx | = meta fx ) and0 ( not0 0f <=f meta fx imply |f meta fx | = -f meta fx ) end line line ell c because prop lemma second conjunct modus ponens ell b indeed not0 0f <=f meta fx imply |f meta fx | = -f meta fx end line because 1rule mp modus ponens ell c modus ponens ell a indeed |f meta fx | = -f meta fx qed end math ] "
" [ math in theory system Q lemma lemma negativeNumerical(R) says for all terms meta fx indeed R( meta fx ) << 00 infer |r R( meta fx ) | == -- R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma negativeNumerical(R) reads block any term meta fx end line line ell a premise R( meta fx ) << 00 end line line ell b premise 0f <=f meta fx end line line ell c because lemma fromLess(R) modus ponens ell a indeed not0 00 <<== R( meta fx ) end line line ell d because lemma to<<== modus ponens ell b indeed 00 <<== R( meta fx ) end line because prop lemma from contradiction modus ponens ell d modus ponens ell c indeed not0 0f <=f meta fx end line line ell big a end block any term meta fx end line line ell a because 1rule deduction modus ponens ell big a indeed R( meta fx ) << 00 imply 0f <=f meta fx imply not0 0f <=f meta fx end line line ell b premise R( meta fx ) << 00 end line line ell c because 1rule mp modus ponens ell a modus ponens ell b indeed 0f <=f meta fx imply not0 0f <=f meta fx end line line ell d because prop lemma imply negation modus ponens ell c indeed not0 0f <=f meta fx end line line ell e because lemma negativeNumerical(F) indeed |f meta fx | = -f meta fx end line line ell f because 1rule adhoc sameR modus ponens ell e indeed R( |f meta fx | ) = R( -f meta fx ) end line because 1rule repetition modus ponens ell f indeed |r R( meta fx ) | = -- R( meta fx ) qed end math ] "
" [ math in theory system Q lemma lemma 0<=|x|(R) says for all terms meta fx indeed 00 <<== |r R( meta fx ) | end lemma end math ] "
" [ math system Q proof of lemma 0<=|x|(R) reads block any term meta fx end line line ell a premise 00 <<== R( meta fx ) end line line ell b because lemma nonnegativeNumerical(R) modus ponens ell a indeed |r R( meta fx ) | == R( meta fx ) end line line ell c because lemma ==Symmetry modus ponens ell b indeed R( meta fx ) == |r R( meta fx ) | end line because lemma subLeqRight(R) modus ponens ell c modus ponens ell a indeed 00 <<== |r R( meta fx ) | end line line ell d end block block any term meta fx end line line ell e premise not0 00 <<== R( meta fx ) end line line ell f because lemma toLess(R) modus ponens ell e indeed R( meta fx ) << 00 end line line ell g because lemma negativeNumerical(R) modus ponens ell f indeed |r R( meta fx ) | == -- R( meta fx ) end line line ell h because lemma ==Symmetry modus ponens ell g indeed -- R( meta fx ) == |r R( meta fx ) | end line line ell i because lemma negativeNegated(R) modus ponens ell f indeed 00 << -- R( meta fx ) end line line ell j because lemma lessLeq(R) modus ponens ell i indeed 00 <<== -- R( meta fx ) end line because lemma subLeqRight(R) modus ponens ell h modus ponens ell j indeed 00 <<== |r R( meta fx ) | end line line ell k end block any term meta fx end line line ell l because 1rule deduction modus ponens ell d indeed 00 <<== R( meta fx ) imply 00 <<== |r R( meta fx ) | end line line ell m because 1rule deduction modus ponens ell k indeed not0 00 <<== R( meta fx ) imply 00 <<== |r R( meta fx ) | end line because prop lemma from negations modus ponens ell l modus ponens ell m indeed 00 <<== |r R( meta fx ) | qed end math ] "
-----------(24.10.06)
" [ math in theory system Q lemma lemma positiveNegated(R) says for all terms meta fx indeed 00 << R( meta fx ) infer -- R( meta fx ) << 00 end lemma end math ] "
" [ math system Q proof of lemma positiveNegated(R) reads any term meta fx end line line ell a premise 00 << R( meta fx ) end line line ell b because lemma lessNegated(R) modus ponens ell a indeed -- R( meta fx ) << -- 00 end line line ell c because lemma -0=0(R) indeed -- 00 == 00 end line because lemma subLessRight(R) modus ponens ell c modus ponens ell b indeed -- R( meta fx ) << 00 qed end math ] "
" [ math in theory system Q lemma lemma addEquations(R) says for all terms meta fx comma meta fy comma meta fz comma meta fu indeed R( meta fx ) == R( meta fy ) infer R( meta fz ) == R( meta fu ) infer R( meta fx ) ++ R( meta fz ) == R( meta fy ) ++ R( meta fu ) end lemma end math ] "
" [ math system Q proof of lemma addEquations(R) reads any term meta fx comma meta fy comma meta fz comma meta fu end line line ell a premise R( meta fx ) == R( meta fy ) end line line ell b premise R( meta fz ) == R( meta fu ) end line line ell c because 1rule adhoc eqAddition(R) modus ponens ell a indeed R( meta fx ) ++ R( meta fz ) == R( meta fy ) ++ R( meta fz ) end line line ell d because lemma eqAdditionLeft(R) modus ponens ell b indeed R( meta fy ) ++ R( meta fz ) == R( meta fy ) ++ R( meta fu ) end line because lemma eqTransitivity modus ponens ell c modus ponens ell d indeed R( meta fx ) ++ R( meta fz ) == R( meta fy ) ++ R( meta fu ) qed end math ] "
" [ math in theory system Q lemma lemma distributionOut(R) says for all terms meta fx comma meta fy comma meta fz indeed R( meta fx ) ** R( meta fy ) ++ R( meta fx ) ** R( meta fz ) == R( meta fx ) ** ( R( meta fy ) ++ R( meta fz ) ) end lemma end math ] "
" [ math system Q proof of lemma distributionOut(R) reads any term meta fx comma meta fy comma meta fz end line line ell a because lemma distribution(R) indeed R( meta fx ) ** ( R( meta fy ) ++ R( meta fz ) ) == R( meta fx ) ** R( meta fy ) ++ R( meta fx ) ** R( meta fz ) end line because lemma ==Symmetry modus ponens ell a indeed R( meta fx ) ** R( meta fy ) ++ R( meta fx ) ** R( meta fz ) == R( meta fx ) ** ( R( meta fy ) ++ R( meta fz ) ) qed end math ] "
" [ math in theory system Q lemma lemma x*0+x=x(R) says for all terms meta fx indeed R( meta fx ) ** 00 ++ R( meta fx ) == R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma x*0+x=x(R) reads any term meta fx end line line ell big a because lemma times1(R) indeed R( meta fx ) ** 01 == R( meta fx ) end line line ell a because lemma ==Symmetry modus ponens ell big a indeed R( meta fx ) == R( meta fx ) ** 01 end line line ell b because lemma eqAdditionLeft(R) modus ponens ell a indeed R( meta fx ) ** 00 ++ R( meta fx ) == R( meta fx ) ** 00 ++ R( meta fx ) ** 01 end line line ell c because lemma distribution(R) indeed R( meta fx ) ** ( 00 ++ 01 ) == R( meta fx ) ** 00 ++ R( meta fx ) ** 01 end line line ell d because lemma ==Symmetry modus ponens ell c indeed R( meta fx ) ** 00 ++ R( meta fx ) ** 01 == R( meta fx ) ** ( 00 ++ 01 ) end line line ell e because lemma plus0Left(R) indeed 00 ++ 01 == 01 end line line ell f because lemma eqMultiplicationLeft(R) modus ponens ell e indeed R( meta fx ) ** ( 00 ++ 01 ) == R( meta fx ) ** 01 end line because lemma eqTransitivity5 modus ponens ell b modus ponens ell d modus ponens ell f modus ponens ell big a indeed R( meta fx ) ** 00 ++ R( meta fx ) == R( meta fx ) qed end math ] "
--------(24.10.06)
" [ math in theory system Q lemma lemma x*0=0(R)fff says for all terms meta fx indeed R( meta fx ) ** 00 == 00 end lemma end math ] "
" [ math system Q proof of lemma x*0=0(R)fff reads any term meta fx end line line ell a because lemma x=x+(y-y)(R) indeed R( meta fx ) ** 00 == R( meta fx ) ** 00 ++ ( R( meta fx ) ++ -- R( meta fx ) ) end line line ell b because lemma plusAssociativity(R) indeed R( meta fx ) ** 00 ++ R( meta fx ) ++ -- R( meta fx ) == R( meta fx ) ** 00 ++ ( R( meta fx ) ++ -- R( meta fx ) ) end line line ell c because lemma ==Symmetry modus ponens ell b indeed R( meta fx ) ** 00 ++ ( R( meta fx ) ++ -- R( meta fx ) ) == R( meta fx ) ** 00 ++ R( meta fx ) ++ -- R( meta fx ) end line line ell d because lemma x*0+x=x(R) indeed R( meta fx ) ** 00 ++ R( meta fx ) == R( meta fx ) end line line ell e because 1rule adhoc eqAddition(R) modus ponens ell d indeed R( meta fx ) ** 00 ++ R( meta fx ) ++ -- R( meta fx ) == R( meta fx ) ++ -- R( meta fx ) end line line ell f because lemma negative(R) indeed R( meta fx ) ++ -- R( meta fx ) == 00 end line because lemma eqTransitivity5 modus ponens ell a modus ponens ell c modus ponens ell e modus ponens ell f indeed R( meta fx ) ** 00 == 00 qed end math ] "
" [ math in theory system Q lemma lemma times(-1)(R) says for all terms meta fx indeed R( meta fx ) ** (--01) == -- R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma times(-1)(R) reads any term meta fx end line line ell a because lemma negative(R) indeed 01 ++ (--01) == 00 end line line ell b because lemma plusCommutativity(R) indeed (--01) ++ 01 == 01 ++ (--01) end line line ell c because lemma eqTransitivity modus ponens ell b modus ponens ell a indeed (--01) ++ 01 == 00 end line line ell d because lemma eqMultiplicationLeft(R) modus ponens ell c indeed R( meta fx ) ** ( (--01) ++ 01 ) == R( meta fx ) ** 00 end line line ell e because lemma x*0=0(R)fff indeed R( meta fx ) ** 00 == 00 end line line ell f because lemma eqTransitivity modus ponens ell d modus ponens ell e indeed R( meta fx ) ** ( (--01) ++ 01 ) == 00 end line line ell g because lemma distribution(R) indeed R( meta fx ) ** ( (--01) ++ 01 ) == R( meta fx ) ** (--01) ++ R( meta fx ) ** 01 end line line ell h because lemma ==Symmetry modus ponens ell g indeed R( meta fx ) ** (--01) ++ R( meta fx ) ** 01 == R( meta fx ) ** ( (--01) ++ 01 ) end line line ell i because lemma eqTransitivity modus ponens ell h modus ponens ell f indeed R( meta fx ) ** (--01) ++ R( meta fx ) ** 01 == 00 end line line ell j because lemma positiveToRight(Eq)(R) modus ponens ell i indeed R( meta fx ) ** (--01) == 00 ++ -- ( R( meta fx ) ** 01 ) end line line ell k because lemma plus0Left(R) indeed 00 ++ -- ( R( meta fx ) ** 01 ) == -- ( R( meta fx ) ** 01 ) end line line ell m because lemma eqTransitivity modus ponens ell j modus ponens ell k indeed R( meta fx ) ** (--01) == -- ( R( meta fx ) ** 01 ) end line line ell n because lemma times1(R) indeed R( meta fx ) ** 01 == R( meta fx ) end line line ell o because lemma eqNegated(R) modus ponens ell n indeed -- ( R( meta fx ) ** 01 ) == -- R( meta fx ) end line because lemma eqTransitivity modus ponens ell m modus ponens ell o indeed R( meta fx ) ** (--01) == -- R( meta fx ) qed end math ] "
" [ math in theory system Q lemma lemma times(-1)Left(R) says for all terms meta fx indeed (--01) ** R( meta fx ) == -- R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma times(-1)Left(R) reads any term meta fx end line line ell a because lemma times(-1)(R) indeed R( meta fx ) ** (--01) == -- R( meta fx ) end line line ell b because lemma timesCommutativity(R) indeed (--01) ** R( meta fx ) == R( meta fx ) ** (--01) end line because lemma eqTransitivity modus ponens ell b modus ponens ell a indeed (--01) ** R( meta fx ) == -- R( meta fx ) qed end math ] "
(************)
" [ math in theory system Q lemma lemma -x-y=-(x+y)(R) says for all terms meta fx comma meta fy indeed -- R( meta fx ) ++ -- R( meta fy ) == -- ( R( meta fx ) ++ R( meta fy ) ) end lemma end math ] "
" [ math system Q proof of lemma -x-y=-(x+y)(R) reads any term meta fx comma meta fy end line line ell a because lemma times(-1)Left(R) indeed (--01) ** R( meta fx ) == -- R( meta fx ) end line line ell b because lemma times(-1)Left(R) indeed (--01) ** R( meta fy ) == -- R( meta fy ) end line line ell c because lemma addEquations(R) modus ponens ell a modus ponens ell b indeed (--01) ** R( meta fx ) ++ (--01) ** R( meta fy ) == -- R( meta fx ) ++ -- R( meta fy ) end line line ell d because lemma ==Symmetry modus ponens ell c indeed -- R( meta fx ) ++ -- R( meta fy ) == (--01) ** R( meta fx ) ++ (--01) ** R( meta fy ) end line line ell e because lemma distributionOut(R) indeed (--01) ** R( meta fx ) ++ (--01) ** R( meta fy ) == (--01) ** ( R( meta fx ) ++ R( meta fy ) ) end line line ell f because lemma times(-1)Left(R) indeed (--01) ** ( R( meta fx ) ++ R( meta fy ) ) == -- ( R( meta fx ) ++ R( meta fy ) ) end line because lemma eqTransitivity4 modus ponens ell d modus ponens ell e modus ponens ell f indeed -- R( meta fx ) ++ -- R( meta fy ) == -- ( R( meta fx ) ++ R( meta fy ) ) qed end math ] "
" [ math in theory system Q lemma lemma lessTotality(R) says for all terms meta fx comma meta fy indeed R( meta fx ) << R( meta fy ) or0 R( meta fx ) == R( meta fy ) or0 R( meta fy ) << R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma lessTotality(R) reads block any term meta fx comma meta fy end line line ell a premise not0 R( meta fx ) << R( meta fy ) end line line ell b premise R( meta fx ) !!== R( meta fy ) end line line ell c because lemma fromNotLess(R) modus ponens ell a indeed R( meta fy ) <<== R( meta fx ) end line line ell d because lemma !!==Symmetry modus ponens ell b indeed R( meta fy ) !!== R( meta fx ) end line because lemma leqNeqLess(R) modus ponens ell c modus ponens ell d indeed R( meta fy ) << R( meta fx ) end line line ell e end block any term meta fx comma meta fy end line line ell f because 1rule deduction modus ponens ell e indeed not0 R( meta fx ) << R( meta fy ) imply R( meta fx ) !!== R( meta fy ) imply R( meta fy ) << R( meta fx ) end line because 1rule repetition modus ponens ell f indeed R( meta fx ) << R( meta fy ) or0 R( meta fx ) == R( meta fy ) or0 R( meta fy ) << R( meta fx ) qed end math ] "
" [ math in theory system Q lemma lemma sameNumerical(R) says for all terms meta fx comma meta fy indeed R( meta fx ) == R( meta fy ) infer |r R( meta fx ) | == |r R( meta fy ) | end lemma end math ] "
" [ math system Q proof of lemma sameNumerical(R) reads block any term meta fx comma meta fy end line line ell big a premise 00 <<== R( meta fx ) end line line ell big b premise R( meta fx ) == R( meta fy ) end line line ell big c because lemma nonnegativeNumerical(R) modus ponens ell big a indeed |r R( meta fx ) | == R( meta fx ) end line line ell big d because lemma subLeqRight(R) modus ponens ell big b modus ponens ell big a indeed 00 <<== R( meta fy ) end line line ell big e because lemma nonnegativeNumerical(R) modus ponens ell big d indeed |r R( meta fy ) | == R( meta fy ) end line line ell big f because lemma ==Symmetry modus ponens ell big e indeed R( meta fy ) == |r R( meta fy ) | end line because lemma eqTransitivity4 modus ponens ell big c modus ponens ell big b modus ponens ell big f indeed |r R( meta fx ) | == |r R( meta fy ) | end line line ell big g end block block any term meta fx comma meta fy end line line ell d premise not0 00 <<== R( meta fx ) end line line ell e premise R( meta fx ) == R( meta fy ) end line line ell f because lemma toLess(R) modus ponens ell d indeed R( meta fx ) << 00 end line line ell g because lemma negativeNumerical(R) modus ponens ell f indeed |r R( meta fx ) | == -- R( meta fx ) end line line ell h because lemma subLessLeft(R) modus ponens ell e modus ponens ell f indeed R( meta fy ) << 00 end line line ell i because lemma negativeNumerical(R) modus ponens ell h indeed |r R( meta fy ) | == -- R( meta fy ) end line line ell j because lemma ==Symmetry modus ponens ell i indeed -- R( meta fy ) == |r R( meta fy ) | end line line ell k because lemma eqNegated(R) modus ponens ell e indeed -- R( meta fx ) == -- R( meta fy ) end line because lemma eqTransitivity4 modus ponens ell g modus ponens ell k modus ponens ell j indeed |r R( meta fx ) | == |r R( meta fy ) | end line line ell l end block any term meta fx comma meta fy end line line ell m premise R( meta fx ) == R( meta fy ) end line line ell n because 1rule deduction modus ponens ell big g indeed 00 <<== R( meta fx ) imply R( meta fx ) == R( meta fy ) imply |r R( meta fx ) | == |r R( meta fy ) | end line line ell o because 1rule deduction modus ponens ell l indeed not0 00 <<== R( meta fx ) imply R( meta fx ) == R( meta fy ) imply |r R( meta fx ) | == |r R( meta fy ) | end line line ell p because prop lemma from negations modus ponens ell n modus ponens ell o indeed R( meta fx ) == R( meta fy ) imply |r R( meta fx ) | == |r R( meta fy ) | end line because 1rule mp modus ponens ell p modus ponens ell m indeed |r R( meta fx ) | == |r R( meta fy ) | qed end math ] "
" [ math in theory system Q lemma lemma minusNegated(R) says for all terms meta fx comma meta fy indeed -- ( R( meta fx ) ++ -- R( meta fy ) ) == R( meta fy ) ++ -- R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma minusNegated(R) reads any term meta fx comma meta fy end line line ell a because lemma doubleMinus(R) indeed -- -- R( meta fy ) == R( meta fy ) end line line ell b because 1rule adhoc eqAddition(R) modus ponens ell a indeed -- -- R( meta fy ) ++ -- R( meta fx ) == R( meta fy ) ++ -- R( meta fx ) end line line ell c because lemma ==Symmetry modus ponens ell b indeed R( meta fy ) ++ -- R( meta fx ) == -- -- R( meta fy ) ++ -- R( meta fx ) end line line ell d because lemma -x-y=-(x+y)(R) indeed -- -- R( meta fy ) ++ -- R( meta fx ) == -- ( -- R( meta fy ) ++ R( meta fx ) ) end line line ell e because lemma plusCommutativity(R) indeed -- R( meta fy ) ++ R( meta fx ) == R( meta fx ) ++ -- R( meta fy ) end line line ell f because lemma eqNegated(R) modus ponens ell e indeed -- ( -- R( meta fy ) ++ R( meta fx ) ) == -- ( R( meta fx ) ++ -- R( meta fy ) ) end line line ell g because lemma eqTransitivity4 modus ponens ell c modus ponens ell d modus ponens ell f indeed R( meta fy ) ++ -- R( meta fx ) == -- ( R( meta fx ) ++ -- R( meta fy ) ) end line because lemma ==Symmetry modus ponens ell g indeed -- ( R( meta fx ) ++ -- R( meta fy ) ) == R( meta fy ) ++ -- R( meta fx ) qed end math ] "
-----------(24.10.06)
" [ math in theory system Q lemma lemma positiveNumerical(R) says for all terms meta fx indeed 00 << R( meta fx ) infer |r R( meta fx ) | == R( meta fx ) end lemma end math ] "
" [ math system Q proof of lemma positiveNumerical(R) reads any term meta fx end line line ell a premise 00 << R( meta fx ) end line line ell b because lemma lessLeq(R) modus ponens ell a indeed 00 <<== R( meta fx ) end line because lemma nonnegativeNumerical(R) modus ponens ell b indeed |r R( meta fx ) | == R( meta fx ) qed end math ] "
" [ math in theory system Q lemma lemma signNumerical(+)(R) says for all terms meta fx indeed 00 << R( meta fx ) infer |r R( meta fx ) | == |r -- R( meta fx ) | end lemma end math ] "
" [ math system Q proof of lemma signNumerical(+)(R) reads any term meta fx end line line ell a premise 00 << R( meta fx ) end line line ell b because lemma positiveNumerical(R) modus ponens ell a indeed |r R( meta fx ) | == R( meta fx ) end line line ell c because lemma positiveNegated(R) modus ponens ell a indeed -- R( meta fx ) << 00 end line line ell d because lemma negativeNumerical(R) modus ponens ell c indeed |r -- R( meta fx ) | == -- -- R( meta fx ) end line line ell e because lemma doubleMinus(R) indeed -- -- R( meta fx ) == R( meta fx ) end line line ell f because lemma eqTransitivity modus ponens ell d modus ponens ell e indeed |r -- R( meta fx ) | == R( meta fx ) end line line ell g because lemma ==Symmetry modus ponens ell f indeed R( meta fx ) == |r -- R( meta fx ) | end line because lemma eqTransitivity modus ponens ell b modus ponens ell g indeed |r R( meta fx ) | == |r -- R( meta fx ) | qed end math ] "
" [ math in theory system Q lemma lemma signNumerical(R) says for all terms meta fx indeed |r R( meta fx ) | == |r -- R( meta fx ) | end lemma end math ] "
" [ math system Q proof of lemma signNumerical(R) reads block any term meta fx end line line ell a premise R( meta fx ) << 00 end line line ell b because lemma negativeNegated(R) modus ponens ell a indeed 00 << -- R( meta fx ) end line line ell c because lemma signNumerical(+)(R) modus ponens ell b indeed |r -- R( meta fx ) | == |r -- -- R( meta fx ) | end line line ell d because lemma doubleMinus(R) indeed -- -- R( meta fx ) == R( meta fx ) end line line ell e because lemma sameNumerical(R) modus ponens ell d indeed |r -- -- R( meta fx ) | == |r R( meta fx ) | end line line ell f because lemma eqTransitivity modus ponens ell c modus ponens ell e indeed |r -- R( meta fx ) | == |r R( meta fx ) | end line because lemma ==Symmetry modus ponens ell f indeed |r R( meta fx ) | == |r -- R( meta fx ) | end line line ell big a end block block any term meta fx end line line ell a premise R( meta fx ) == 00 end line line ell b because lemma eqNegated(R) modus ponens ell a indeed -- R( meta fx ) == -- 00 end line line ell c because lemma -0=0(R) indeed -- 00 == 00 end line line ell d because lemma ==Symmetry modus ponens ell a indeed 00 == R( meta fx ) end line line ell e because lemma eqTransitivity4 modus ponens ell b modus ponens ell c modus ponens ell d indeed -- R( meta fx ) == R( meta fx ) end line line ell f because lemma ==Symmetry modus ponens ell e indeed R( meta fx ) == -- R( meta fx ) end line because lemma sameNumerical(R) modus ponens ell f indeed |r R( meta fx ) | == |r -- R( meta fx ) | end line line ell big b end block block any term meta fx end line line ell a premise 00 << R( meta fx ) end line because lemma signNumerical(+)(R) modus ponens ell a indeed |r R( meta fx ) | == |r -- R( meta fx ) | end line line ell big c end block any term meta fx end line line ell big d because 1rule deduction modus ponens ell big a indeed R( meta fx ) << 00 imply |r R( meta fx ) | == |r -- R( meta fx ) | end line line ell big e because 1rule deduction modus ponens ell big b indeed R( meta fx ) == 00 imply |r R( meta fx ) | == |r -- R( meta fx ) | end line line ell big f because 1rule deduction modus ponens ell big c indeed 00 << R( meta fx ) imply |r R( meta fx ) | == |r -- R( meta fx ) | end line line ell big g because lemma lessTotality(R) indeed R( meta fx ) << 00 or0 R( meta fx ) == 00 or0 00 << R( meta fx ) end line because prop lemma from three disjuncts modus ponens ell big g modus ponens ell big d modus ponens ell big e modus ponens ell big f indeed |r R( meta fx ) | == |r -- R( meta fx ) | qed end math ] "
" [ math in theory system Q lemma lemma numericalDifference(R) says for all terms meta fx comma meta fy indeed |r R( meta fx ) ++ -- R( meta fy ) | == |r R( meta fy ) ++ -- R( meta fx ) | end lemma end math ] "
" [ math system Q proof of lemma numericalDifference(R) reads any term meta fx comma meta fy end line line ell a because lemma signNumerical(R) indeed |r R( meta fx ) ++ -- R( meta fy ) | == |r -- ( R( meta fx ) ++ -- R( meta fy ) ) | end line line ell b because lemma minusNegated(R) indeed -- ( R( meta fx ) ++ -- R( meta fy ) ) == R( meta fy ) ++ -- R( meta fx ) end line line ell c because lemma sameNumerical(R) modus ponens ell b indeed |r -- ( R( meta fx ) ++ -- R( meta fy ) ) | == |r R( meta fy ) ++ -- R( meta fx ) | end line because lemma eqTransitivity modus ponens ell a modus ponens ell c indeed |r R( meta fx ) ++ -- R( meta fy ) | == |r R( meta fy ) ++ -- R( meta fx ) | qed end math ] "
--------(25.10.06)
" [ math in theory system Q lemma lemma x<=|x|(R) says for all terms meta fx indeed R( meta fx ) <<== |r R( meta fx ) | end lemma end math ] "
" [ math system Q proof of lemma x<=|x|(R) reads block any term meta fx end line line ell a premise 00 <<== R( meta fx ) end line line ell b because lemma nonnegativeNumerical(R) indeed |r R( meta fx ) | == R( meta fx ) end line line ell c because lemma ==Symmetry modus ponens ell b indeed R( meta fx ) == |r R( meta fx ) | end line because lemma eqLeq(R) modus ponens ell c indeed R( meta fx ) <<== |r R( meta fx ) | end line line ell big a end block block any term meta fx end line line ell a premise R( meta fx ) <<== 00 end line line ell b because lemma 0<=|x|(R) indeed 00 <<== |r R( meta fx ) | end line because lemma leqTransitivity(R) modus ponens ell a modus ponens ell b indeed R( meta fx ) <<== |r R( meta fx ) | end line line ell big b end block any term meta fx end line line ell a because 1rule deduction modus ponens ell big a indeed 00 <<== R( meta fx ) imply R( meta fx ) <<== |r R( meta fx ) | end line line ell b because 1rule deduction modus ponens ell big b indeed R( meta fx ) <<== 00 imply R( meta fx ) <<== |r R( meta fx ) | end line because lemma from leqGeq(R) modus ponens ell a modus ponens ell b indeed R( meta fx ) <<== |r R( meta fx ) | qed end math ] "
" [ math var a end math ] "
venter----
\appendix
" [ flush left math priority table preassociative priority sup2 equal priority base equal priority bracket x end bracket equal priority big bracket x end bracket equal priority math x end math equal priority flush left x end left equal priority var x equal priority var y equal priority var z equal priority proclaim x as x end proclaim equal priority define x of x as x end define equal priority pyk equal priority tex equal priority tex name equal priority priority equal priority x equal priority true equal priority if x then x else x end if equal priority introduce x of x as x end introduce equal priority value equal priority claim equal priority bottom equal priority function f of x end function equal priority identity x end identity equal priority false equal priority untagged zero equal priority untagged one equal priority untagged two equal priority untagged three equal priority untagged four equal priority untagged five equal priority untagged six equal priority untagged seven equal priority untagged eight equal priority untagged nine equal priority zero equal priority one equal priority two equal priority three equal priority four equal priority five equal priority six equal priority seven equal priority eight equal priority nine equal priority var a equal priority var b equal priority var c equal priority var d equal priority var e equal priority var f equal priority var g equal priority var h equal priority var i equal priority var j equal priority var k equal priority var l equal priority var m equal priority var n equal priority var o equal priority var p equal priority var q equal priority var r equal priority var s equal priority var t equal priority var u equal priority var v equal priority var w equal priority tagged parenthesis x end tagged equal priority tagged if x then x else x end if equal priority array x is x end array equal priority left equal priority center equal priority right equal priority empty equal priority substitute x set x to x end substitute equal priority map tag x end tag equal priority raw map untag x end untag equal priority map untag x end untag equal priority normalizing untag x end untag equal priority apply x to x end apply equal priority apply one x to x end apply equal priority identifier x end identifier equal priority identifier one x plus id x end identifier equal priority array plus x and x end plus equal priority array remove x array x level x end remove equal priority array put x value x array x level x end put equal priority array add x value x index x value x level x end add equal priority bit x of x end bit equal priority bit one x of x end bit equal priority example rack equal priority vector hook equal priority bibliography hook equal priority dictionary hook equal priority body hook equal priority codex hook equal priority expansion hook equal priority code hook equal priority cache hook equal priority diagnose hook equal priority pyk aspect equal priority tex aspect equal priority texname aspect equal priority value aspect equal priority message aspect equal priority macro aspect equal priority definition aspect equal priority unpack aspect equal priority claim aspect equal priority priority aspect equal priority lambda identifier equal priority apply identifier equal priority true identifier equal priority if identifier equal priority quote identifier equal priority proclaim identifier equal priority define identifier equal priority introduce identifier equal priority hide identifier equal priority pre identifier equal priority post identifier equal priority eval x stack x cache x end eval equal priority eval two x ref x id x stack x cache x end eval equal priority eval three x function x stack x cache x end eval equal priority eval four x arguments x stack x cache x end eval equal priority lookup x stack x default x end lookup equal priority abstract x term x stack x cache x end abstract equal priority quote x end quote equal priority expand x state x cache x end expand equal priority expand two x definition x state x cache x end expand equal priority expand list x state x cache x end expand equal priority macro equal priority macro state equal priority zip x with x end zip equal priority assoc one x address x index x end assoc equal priority protect x end protect equal priority self equal priority macro define x as x end define equal priority value define x as x end define equal priority intro define x as x end define equal priority pyk define x as x end define equal priority tex define x as x end define equal priority tex name define x as x end define equal priority priority table x end table equal priority macro define one equal priority macro define two x end define equal priority macro define three x end define equal priority macro define four x state x cache x definition x end define equal priority state expand x state x cache x end expand equal priority quote expand x term x stack x end expand equal priority quote expand two x term x stack x end expand equal priority quote expand three x term x stack x value x end expand equal priority quote expand star x term x stack x end expand equal priority parenthesis x end parenthesis equal priority big parenthesis x end parenthesis equal priority display x end display equal priority statement x end statement equal priority spying test x end test equal priority false spying test x end test equal priority aspect x subcodex x end aspect equal priority aspect x term x cache x end aspect equal priority tuple x end tuple equal priority tuple one x end tuple equal priority tuple two x end tuple equal priority let two x apply x end let equal priority let one x apply x end let equal priority claim define x as x end define equal priority checker equal priority check x cache x end check equal priority check two x cache x def x end check equal priority check three x cache x def x end check equal priority check list x cache x end check equal priority check list two x cache x value x end check equal priority test x end test equal priority false test x end test equal priority raw test x end test equal priority message equal priority message define x as x end define equal priority the statement aspect equal priority statement equal priority statement define x as x end define equal priority example axiom equal priority example scheme equal priority example rule equal priority absurdity equal priority contraexample equal priority example theory primed equal priority example lemma equal priority metavar x end metavar equal priority meta a equal priority meta b equal priority meta c equal priority meta d equal priority meta e equal priority meta f equal priority meta g equal priority meta h equal priority meta i equal priority meta j equal priority meta k equal priority meta l equal priority meta m equal priority meta n equal priority meta o equal priority meta p equal priority meta q equal priority meta r equal priority meta s equal priority meta t equal priority meta u equal priority meta v equal priority meta w equal priority meta x equal priority meta y equal priority meta z equal priority sub x set x to x end sub equal priority sub star x set x to x end sub equal priority the empty set equal priority example remainder equal priority make visible x end visible equal priority intro x index x pyk x tex x end intro equal priority intro x pyk x tex x end intro equal priority error x term x end error equal priority error two x term x end error equal priority proof x term x cache x end proof equal priority proof two x term x end proof equal priority sequent eval x term x end eval equal priority seqeval init x term x end eval equal priority seqeval modus x term x end eval equal priority seqeval modus one x term x sequent x end eval equal priority seqeval verify x term x end eval equal priority seqeval verify one x term x sequent x end eval equal priority sequent eval plus x term x end eval equal priority seqeval plus one x term x sequent x end eval equal priority seqeval minus x term x end eval equal priority seqeval minus one x term x sequent x end eval equal priority seqeval deref x term x end eval equal priority seqeval deref one x term x sequent x end eval equal priority seqeval deref two x term x sequent x def x end eval equal priority seqeval at x term x end eval equal priority seqeval at one x term x sequent x end eval equal priority seqeval infer x term x end eval equal priority seqeval infer one x term x premise x sequent x end eval equal priority seqeval endorse x term x end eval equal priority seqeval endorse one x term x side x sequent x end eval equal priority seqeval est x term x end eval equal priority seqeval est one x term x name x sequent x end eval equal priority seqeval est two x term x name x sequent x def x end eval equal priority seqeval all x term x end eval equal priority seqeval all one x term x variable x sequent x end eval equal priority seqeval cut x term x end eval equal priority seqeval cut one x term x forerunner x end eval equal priority seqeval cut two x term x forerunner x sequent x end eval equal priority computably true x end true equal priority claims x cache x ref x end claims equal priority claims two x cache x ref x end claims equal priority the proof aspect equal priority proof equal priority lemma x says x end lemma equal priority proof of x reads x end proof equal priority in theory x lemma x says x end lemma equal priority in theory x antilemma x says x end antilemma equal priority in theory x rule x says x end rule equal priority in theory x antirule x says x end antirule equal priority verifier equal priority verify one x end verify equal priority verify two x proofs x end verify equal priority verify three x ref x sequents x diagnose x end verify equal priority verify four x premises x end verify equal priority verify five x ref x array x sequents x end verify equal priority verify six x ref x list x sequents x end verify equal priority verify seven x ref x id x sequents x end verify equal priority cut x and x end cut equal priority head x end head equal priority tail x end tail equal priority rule one x theory x end rule equal priority rule x subcodex x end rule equal priority rule tactic equal priority plus x and x end plus equal priority theory x end theory equal priority theory two x cache x end theory equal priority theory three x name x end theory equal priority theory four x name x sum x end theory equal priority example axiom lemma primed equal priority example scheme lemma primed equal priority example rule lemma primed equal priority contraexample lemma primed equal priority example axiom lemma equal priority example scheme lemma equal priority example rule lemma equal priority contraexample lemma equal priority example theory equal priority ragged right equal priority ragged right expansion equal priority parameter term x stack x seed x end parameter equal priority parameter term star x stack x seed x end parameter equal priority instantiate x with x end instantiate equal priority instantiate star x with x end instantiate equal priority occur x in x substitution x end occur equal priority occur star x in x substitution x end occur equal priority unify x with x substitution x end unify equal priority unify star x with x substitution x end unify equal priority unify two x with x substitution x end unify equal priority ell a equal priority ell b equal priority ell c equal priority ell d equal priority ell e equal priority ell f equal priority ell g equal priority ell h equal priority ell i equal priority ell j equal priority ell k equal priority ell l equal priority ell m equal priority ell n equal priority ell o equal priority ell p equal priority ell q equal priority ell r equal priority ell s equal priority ell t equal priority ell u equal priority ell v equal priority ell w equal priority ell x equal priority ell y equal priority ell z equal priority ell big a equal priority ell big b equal priority ell big c equal priority ell big d equal priority ell big e equal priority ell big f equal priority ell big g equal priority ell big h equal priority ell big i equal priority ell big j equal priority ell big k equal priority ell big l equal priority ell big m equal priority ell big n equal priority ell big o equal priority ell big p equal priority ell big q equal priority ell big r equal priority ell big s equal priority ell big t equal priority ell big u equal priority ell big v equal priority ell big w equal priority ell big x equal priority ell big y equal priority ell big z equal priority ell dummy equal priority sequent reflexivity equal priority tactic reflexivity equal priority sequent commutativity equal priority tactic commutativity equal priority the tactic aspect equal priority tactic equal priority tactic define x as x end define equal priority proof expand x state x cache x end expand equal priority proof expand list x state x cache x end expand equal priority proof state equal priority conclude one x cache x end conclude equal priority conclude two x proves x cache x end conclude equal priority conclude three x proves x lemma x substitution x end conclude equal priority conclude four x lemma x end conclude equal priority check equal priority general macro define x as x end define equal priority make root visible x end visible equal priority sequent example axiom equal priority sequent example rule equal priority sequent example contradiction equal priority sequent example theory equal priority sequent example lemma equal priority set x end set equal priority object var x end var equal priority object a equal priority object b equal priority object c equal priority object d equal priority object e equal priority object f equal priority object g equal priority object h equal priority object i equal priority object j equal priority object k equal priority object l equal priority object m equal priority object n equal priority object o equal priority object p equal priority object q equal priority object r equal priority object s equal priority object t equal priority object u equal priority object v equal priority object w equal priority object x equal priority object y equal priority object z equal priority sub x is x where x is x end sub equal priority sub zero x is x where x is x end sub equal priority sub one x is x where x is x end sub equal priority sub star x is x where x is x end sub equal priority deduction x conclude x end deduction equal priority deduction zero x conclude x end deduction equal priority deduction one x conclude x condition x end deduction equal priority deduction two x conclude x condition x end deduction equal priority deduction three x conclude x condition x bound x end deduction equal priority deduction four x conclude x condition x bound x end deduction equal priority deduction four star x conclude x condition x bound x end deduction equal priority deduction five x condition x bound x end deduction equal priority deduction six x conclude x exception x bound x end deduction equal priority deduction six star x conclude x exception x bound x end deduction equal priority deduction seven x end deduction equal priority deduction eight x bound x end deduction equal priority deduction eight star x bound x end deduction equal priority system s equal priority double negation equal priority rule mp equal priority rule gen equal priority deduction equal priority axiom s one equal priority axiom s two equal priority axiom s three equal priority axiom s four equal priority axiom s five equal priority axiom s six equal priority axiom s seven equal priority axiom s eight equal priority axiom s nine equal priority repetition equal priority lemma a one equal priority lemma a two equal priority lemma a four equal priority lemma a five equal priority prop three two a equal priority prop three two b equal priority prop three two c equal priority prop three two d equal priority prop three two e one equal priority prop three two e two equal priority prop three two e equal priority prop three two f one equal priority prop three two f two equal priority prop three two f equal priority prop three two g one equal priority prop three two g two equal priority prop three two g equal priority prop three two h one equal priority prop three two h two equal priority prop three two h equal priority block one x state x cache x end block equal priority block two x end block equal priority kvanti equal priority lemma uniqueMember equal priority lemma uniqueMember(Type) equal priority lemma sameSeries equal priority lemma a4 equal priority lemma sameMember equal priority 1rule Qclosed(Addition) equal priority 1rule Qclosed(Multiplication) equal priority 1rule fromCartProd(1) equal priority 1rule fromCartProd(2) equal priority constantRationalSeries( x ) equal priority cartProd( x , x ) equal priority P( x ) equal priority binaryUnion( x , x ) equal priority setOfRationalSeries equal priority isSubset( x , x ) equal priority (p x , x ) equal priority (s x ) equal priority cdots equal priority object-var equal priority ex-var equal priority ph-var equal priority vaerdi equal priority variabel equal priority op x end op equal priority op2 x comma x end op2 equal priority define-equal x comma x end equal equal priority contains-empty x end empty equal priority Nat( x ) equal priority 1deduction x conclude x end 1deduction equal priority 1deduction zero x conclude x end 1deduction equal priority 1deduction side x conclude x condition x end 1deduction equal priority 1deduction one x conclude x condition x end 1deduction equal priority 1deduction two x conclude x condition x end 1deduction equal priority 1deduction three x conclude x condition x bound x end 1deduction equal priority 1deduction four x conclude x condition x bound x end 1deduction equal priority 1deduction four star x conclude x condition x bound x end 1deduction equal priority 1deduction five x condition x bound x end 1deduction equal priority 1deduction six x conclude x exception x bound x end 1deduction equal priority 1deduction six star x conclude x exception x bound x end 1deduction equal priority 1deduction seven x end 1deduction equal priority 1deduction eight x bound x end 1deduction equal priority 1deduction eight star x bound x end 1deduction equal priority ex1 equal priority ex2 equal priority ex3 equal priority ex10 equal priority ex20 equal priority existential var x end var equal priority x is existential var equal priority exist-sub x is x where x is x end sub equal priority exist-sub0 x is x where x is x end sub equal priority exist-sub1 x is x where x is x end sub equal priority exist-sub* x is x where x is x end sub equal priority ph1 equal priority ph2 equal priority ph3 equal priority placeholder-var x end var equal priority x is placeholder-var equal priority ph-sub x is x where x is x end sub equal priority ph-sub0 x is x where x is x end sub equal priority ph-sub1 x is x where x is x end sub equal priority ph-sub* x is x where x is x end sub equal priority meta-sub x is x where x is x end sub equal priority meta-sub1 x is x where x is x end sub equal priority meta-sub* x is x where x is x end sub equal priority var big set equal priority object big set equal priority meta big set equal priority zermelo empty set equal priority system Q equal priority 1rule mp equal priority 1rule gen equal priority 1rule repetition equal priority 1rule ad absurdum equal priority 1rule deduction equal priority 1rule exist intro equal priority axiom extensionality equal priority axiom empty set equal priority axiom pair definition equal priority axiom union definition equal priority axiom power definition equal priority axiom separation definition equal priority prop lemma add double neg equal priority prop lemma remove double neg equal priority prop lemma and commutativity equal priority prop lemma auto imply equal priority prop lemma contrapositive equal priority prop lemma first conjunct equal priority prop lemma second conjunct equal priority prop lemma from contradiction equal priority prop lemma from disjuncts equal priority prop lemma iff commutativity equal priority prop lemma iff first equal priority prop lemma iff second equal priority prop lemma imply transitivity equal priority prop lemma join conjuncts equal priority prop lemma mp2 equal priority prop lemma mp3 equal priority prop lemma mp4 equal priority prop lemma mp5 equal priority prop lemma mt equal priority prop lemma negative mt equal priority prop lemma technicality equal priority prop lemma weakening equal priority prop lemma weaken or first equal priority prop lemma weaken or second equal priority lemma formula2pair equal priority lemma pair2formula equal priority lemma formula2union equal priority lemma union2formula equal priority lemma formula2separation equal priority lemma separation2formula equal priority lemma formula2power equal priority lemma subset in power set equal priority lemma power set is subset0 equal priority lemma power set is subset equal priority lemma power set is subset0-switch equal priority lemma power set is subset-switch equal priority lemma set equality suff condition equal priority lemma set equality suff condition(t)0 equal priority lemma set equality suff condition(t) equal priority lemma set equality skip quantifier equal priority lemma set equality nec condition equal priority lemma reflexivity0 equal priority lemma reflexivity equal priority lemma symmetry0 equal priority lemma symmetry equal priority lemma transitivity0 equal priority lemma transitivity equal priority lemma er is reflexive equal priority lemma er is symmetric equal priority lemma er is transitive equal priority lemma empty set is subset equal priority lemma member not empty0 equal priority lemma member not empty equal priority lemma unique empty set0 equal priority lemma unique empty set equal priority lemma ==Reflexivity equal priority lemma ==Symmetry equal priority lemma ==Transitivity0 equal priority lemma ==Transitivity equal priority lemma transfer ~is0 equal priority lemma transfer ~is equal priority lemma pair subset0 equal priority lemma pair subset1 equal priority lemma pair subset equal priority lemma same pair equal priority lemma same singleton equal priority lemma union subset equal priority lemma same union equal priority lemma separation subset equal priority lemma same separation equal priority lemma same binary union equal priority lemma intersection subset equal priority lemma same intersection equal priority lemma auto member equal priority lemma eq-system not empty0 equal priority lemma eq-system not empty equal priority lemma eq subset0 equal priority lemma eq subset equal priority lemma equivalence nec condition0 equal priority lemma equivalence nec condition equal priority lemma none-equivalence nec condition0 equal priority lemma none-equivalence nec condition1 equal priority lemma none-equivalence nec condition equal priority lemma equivalence class is subset equal priority lemma equivalence classes are disjoint equal priority lemma all disjoint equal priority lemma all disjoint-imply equal priority lemma bs subset union(bs/r) equal priority lemma union(bs/r) subset bs equal priority lemma union(bs/r) is bs equal priority theorem eq-system is partition equal priority var x1 equal priority var x2 equal priority var y1 equal priority var y2 equal priority var v1 equal priority var v2 equal priority var v3 equal priority var v4 equal priority var v2n equal priority var m1 equal priority var m2 equal priority var n1 equal priority var n2 equal priority var n3 equal priority var ep equal priority var ep1 equal priority var ep2 equal priority var fep equal priority var fx equal priority var fy equal priority var fz equal priority var fu equal priority var fv equal priority var fw equal priority var rx equal priority var ry equal priority var rz equal priority var ru equal priority var sx equal priority var sx1 equal priority var sy equal priority var sy1 equal priority var sz equal priority var sz1 equal priority var su equal priority var su1 equal priority var fxs equal priority var fys equal priority var crs1 equal priority var f1 equal priority var f2 equal priority var f3 equal priority var f4 equal priority var op1 equal priority var op2 equal priority var r1 equal priority var s1 equal priority var s2 equal priority meta x1 equal priority meta x2 equal priority meta y1 equal priority meta y2 equal priority meta v1 equal priority meta v2 equal priority meta v3 equal priority meta v4 equal priority meta v2n equal priority meta m1 equal priority meta m2 equal priority meta n1 equal priority meta n2 equal priority meta n3 equal priority meta ep equal priority meta ep1 equal priority meta ep2 equal priority meta fx equal priority meta fy equal priority meta fz equal priority meta fu equal priority meta fv equal priority meta fw equal priority meta fep equal priority meta rx equal priority meta ry equal priority meta rz equal priority meta ru equal priority meta sx equal priority meta sx1 equal priority meta sy equal priority meta sy1 equal priority meta sz equal priority meta sz1 equal priority meta su equal priority meta su1 equal priority meta fxs equal priority meta fys equal priority meta f1 equal priority meta f2 equal priority meta f3 equal priority meta f4 equal priority meta op1 equal priority meta op2 equal priority meta r1 equal priority meta s1 equal priority meta s2 equal priority object ep equal priority object crs1 equal priority object f1 equal priority object f2 equal priority object f3 equal priority object f4 equal priority object n1 equal priority object n2 equal priority object op1 equal priority object op2 equal priority object r1 equal priority object s1 equal priority object s2 equal priority ph4 equal priority ph5 equal priority ph6 equal priority NAT equal priority RATIONAL_SERIES equal priority SERIES equal priority setOfReals equal priority setOfFxs equal priority N equal priority Q equal priority X equal priority xs equal priority xsF equal priority ysF equal priority us equal priority usF equal priority 0 equal priority 1 equal priority (-1) equal priority 2 equal priority 3 equal priority 1/2 equal priority 1/3 equal priority 2/3 equal priority 0f equal priority 1f equal priority 00 equal priority 01 equal priority (--01) equal priority 02 equal priority 01//02 equal priority lemma 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) equal priority sup equal priority prop lemma to negated and(1) equal priority lemma uniqueNegative equal priority lemma doubleMinus equal priority lemma minusNegated equal priority lemma eqReflexivity equal priority lemma eqSymmetry equal priority lemma eqTransitivity equal priority lemma eqTransitivity4 equal priority lemma eqTransitivity5 equal priority lemma eqTransitivity6 equal priority lemma addEquations equal priority lemma subtractEquations equal priority lemma subtractEquationsLeft equal priority lemma multiplyEquations equal priority lemma eqNegated equal priority lemma positiveToRight(Eq) equal priority lemma positiveToLeft(Eq)(1 term) equal priority lemma negativeToLeft(Eq) equal priority lemma nonreciprocalToRight(Eq)(1 term) equal priority lemma plusAssociativity(4 terms) equal priority lemma lessNeq equal priority lemma neqSymmetry equal priority lemma neqNegated equal priority lemma subNeqRight equal priority lemma subNeqLeft equal priority lemma negativeToRight(Neq)(1 term) equal priority lemma neqAddition equal priority lemma neqMultiplication equal priority lemma nonzeroProduct(2) equal priority lemma UStelescope(+1) equal priority lemma telescopeBound base equal priority lemma telescopeBound indu equal priority lemma telescopeBound equal priority lemma intervalSize base equal priority lemma intervalSize indu equal priority lemma intervalSize equal priority lemma XSlessUS equal priority lemma USdecreasing(+1) equal priority lemma closeUS equal priority lemma closeUS(n+1) equal priority pred lemma allNegated(Imply) equal priority pred lemma existNegated(Imply) equal priority pred lemma intro exist helper equal priority pred lemma intro exist equal priority pred lemma exist mp equal priority pred lemma exist mp2 equal priority pred lemma 2exist mp equal priority pred lemma 2exist mp2 equal priority pred lemma EAE mp equal priority pred lemma addAll equal priority pred lemma addExist helper1 equal priority pred lemma addExist helper2 equal priority pred lemma addExist equal priority pred lemma addExist(SimpleAnt) equal priority pred lemma addExist(Simple) equal priority pred lemma addEAE equal priority pred lemma AEAnegated equal priority pred lemma EEAnegated equal priority lemma induction equal priority lemma leqAntisymmetry equal priority lemma leqTransitivity equal priority lemma leqAddition equal priority lemma leqMultiplication equal priority lemma reciprocal equal priority lemma equality equal priority lemma eqLeq equal priority lemma eqAddition equal priority lemma eqMultiplication equal priority lemma leqMultiplicationLeft equal priority lemma leqLessEq equal priority lemma lessLeq equal priority lemma from leqGeq equal priority lemma subLeqRight equal priority lemma subLeqLeft equal priority lemma leqPlus1 equal priority lemma positiveToRight(Leq) equal priority lemma positiveToRight(Leq)(1 term) equal priority lemma negativeToRight(Leq) equal priority lemma positiveToLeft(Leq) equal priority lemma negativeToLeft(Leq) equal priority lemma negativeToLeft(Leq)(1 term) equal priority lemma leqAdditionLeft equal priority lemma leqSubtraction equal priority lemma leqSubtractionLeft equal priority lemma thirdGeq equal priority lemma leqNegated equal priority lemma addEquations(Leq) equal priority lemma multiplyEquations(Leq) equal priority lemma thirdGeqSeries equal priority lemma leqNeqLess equal priority lemma fromLess equal priority lemma toLess equal priority lemma fromNotLess equal priority lemma toNotLess equal priority lemma negativeLessPositive equal priority lemma leqLessTransitivity equal priority lemma lessLeqTransitivity equal priority lemma lessTransitivity equal priority lemma lessTotality equal priority lemma subLessRight equal priority lemma subLessLeft equal priority lemma switchTerms(x
\section{Pyk definitioner} \label{sec:pyk}
\begin{flushleft}
" [ math protect define pyk of lemma leqTotality(R) as text "lemma leqTotality(R)" end text end define linebreak define pyk of lemma positiveToLeft(Eq) as text "lemma positiveToLeft(Eq)" end text end define linebreak define pyk of lemma expZero exact as text "lemma expZero exact" end text end define linebreak define pyk of lemma sameExp base as text "lemma sameExp base" end text end define linebreak define pyk of lemma sameExp indu as text "lemma sameExp indu" end text end define linebreak define pyk of lemma sameExp as text "lemma sameExp" end text end define linebreak define pyk of lemma (1/2)(x+y)-x=(1/2)(y-x) as text "lemma (1/2)(x+y)-x=(1/2)(y-x)" end text end define linebreak define pyk of lemma y-(1/2)(x+y)=(1/2)(y-x) as text "lemma y-(1/2)(x+y)=(1/2)(y-x)" end text end define linebreak define pyk of lemma base(1/2)Sum zero exact as text "lemma base(1/2)Sum zero exact" end text end define linebreak define pyk of lemma sameBase(1/2)Sum second base as text "lemma sameBase(1/2)Sum second base" end text end define linebreak define pyk of lemma sameBase(1/2)Sum second indu as text "lemma sameBase(1/2)Sum second indu" end text end define linebreak define pyk of lemma sameBase(1/2)Sum second as text "lemma sameBase(1/2)Sum second" end text end define linebreak define pyk of lemma negativeToLeft(Less)(1 term) as text "lemma negativeToLeft(Less)(1 term)" end text end define linebreak define pyk of lemma base(1/2)Sum(+1) as text "lemma base(1/2)Sum(+1)" end text end define linebreak define pyk of lemma base(1/2)Sum exact bound base as text "lemma base(1/2)Sum exact bound base" end text end define linebreak define pyk of lemma base(1/2)Sum exact bound indu as text "lemma base(1/2)Sum exact bound indu" end text end define linebreak define pyk of lemma base(1/2)Sum exact bound as text "lemma base(1/2)Sum exact bound" end text end define linebreak define pyk of lemma base(1/2)Sum bound as text "lemma base(1/2)Sum bound" end text end define linebreak define pyk of lemma UStelescope zero exact as text "lemma UStelescope zero exact" end text end define linebreak define pyk of lemma sameTelescope second base as text "lemma sameTelescope second base" end text end define linebreak define pyk of lemma sameTelescope second indu as text "lemma sameTelescope second indu" end text end define linebreak define pyk of lemma sameTelescope second as text "lemma sameTelescope second" end text end define linebreak define pyk of lemma exp(+1) as text "lemma exp(+1)" end text end define linebreak define pyk of lemma positiveBase base as text "lemma positiveBase base" end text end define linebreak define pyk of lemma positiveBase indu as text "lemma positiveBase indu" end text end define linebreak define pyk of lemma positiveBase as text "lemma positiveBase" end text end define linebreak define pyk of lemma telescopeNumerical base as text "lemma telescopeNumerical base" end text end define linebreak define pyk of lemma telescopeNumerical indu as text "lemma telescopeNumerical indu" end text end define linebreak define pyk of lemma telescopeNumerical as text "lemma telescopeNumerical" end text end define linebreak define pyk of lemma +1IsPositive(N) as text "lemma +1IsPositive(N)" end text end define linebreak define pyk of lemma distributionOut(Minus) as text "lemma distributionOut(Minus)" end text end define linebreak define pyk of lemma positiveToRight(Eq)(1 term) as text "lemma positiveToRight(Eq)(1 term)" end text end define linebreak define pyk of lemma sameSeries(NumDiff) as text "lemma sameSeries(NumDiff)" end text end define linebreak define pyk of prop lemma to negated double imply as text "prop lemma to negated double imply" end text end define linebreak define pyk of pred lemma addNegatedAll as text "pred lemma addNegatedAll" end text end define linebreak define pyk of pred lemma (A)to(~E~)(Imply) as text "pred lemma (A)to(~E~)(Imply)" end text end define linebreak define pyk of pred lemma (E)to(~A~)(Imply) as text "pred lemma (E)to(~A~)(Imply)" end text end define linebreak define pyk of pred lemma (E~)to(~A)(Imply) as text "pred lemma (E~)to(~A)(Imply)" end text end define linebreak define pyk of pred lemma toNegatedAEA as text "pred lemma toNegatedAEA" end text end define linebreak define pyk of lemma three2threeTerms(R) as text "lemma three2threeTerms(R)" end text end define linebreak define pyk of lemma lessNeq(F) helper as text "lemma lessNeq(F) helper" end text end define linebreak define pyk of lemma lessNeq(F) as text "lemma lessNeq(F)" end text end define linebreak define pyk of lemma lessNeq(R) as text "lemma lessNeq(R)" end text end define linebreak define pyk of lemma x=x+(y-y)(R) as text "lemma x=x+(y-y)(R)" end text end define linebreak define pyk of lemma x=x+y-y(R) as text "lemma x=x+y-y(R)" end text end define linebreak define pyk of lemma subtractEquations(R) as text "lemma subtractEquations(R)" end text end define linebreak define pyk of lemma neqAddition(R) as text "lemma neqAddition(R)" end text end define linebreak define pyk of lemma positiveToRight(Less)(R) as text "lemma positiveToRight(Less)(R)" end text end define linebreak define pyk of lemma positiveToRight(Less)(1 term)(R) as text "lemma positiveToRight(Less)(1 term)(R)" end text end define linebreak define pyk of lemma leqNeqLess(R) as text "lemma leqNeqLess(R)" end text end define linebreak define pyk of lemma subLeqLeft(R) as text "lemma subLeqLeft(R)" end text end define linebreak define pyk of lemma toLeq(Advanced)(R) as text "lemma toLeq(Advanced)(R)" end text end define linebreak define pyk of lemma leqLessTransitivity(R) as text "lemma leqLessTransitivity(R)" end text end define linebreak define pyk of lemma negativeToLeft(Eq)(R) as text "lemma negativeToLeft(Eq)(R)" end text end define linebreak define pyk of lemma negativeToRight(Less)(R) as text "lemma negativeToRight(Less)(R)" end text end define linebreak define pyk of lemma !!==Symmetry as text "lemma !!==Symmetry" end text end define linebreak define pyk of lemma switchTerms(x<=y-z) as text "lemma switchTerms(x<=y-z)" end text end define linebreak define pyk of lemma plus0Left(R) as text "lemma plus0Left(R)" end text end define linebreak define pyk of lemma positiveToRight(Eq)(R) as text "lemma positiveToRight(Eq)(R)" end text end define linebreak define pyk of lemma eqAdditionLeft(R) as text "lemma eqAdditionLeft(R)" end text end define linebreak define pyk of lemma three2twoTerms(R) as text "lemma three2twoTerms(R)" end text end define linebreak define pyk of lemma to!!== as text "lemma to!!==" end text end define linebreak define pyk of lemma positiveToRight(Less)(1 term) as text "lemma positiveToRight(Less)(1 term)" end text end define linebreak define pyk of pred lemma (A~)to(~E) as text "pred lemma (A~)to(~E)" end text end define linebreak define pyk of lemma negativeToRight(Eq)(R) as text "lemma negativeToRight(Eq)(R)" end text end define linebreak define pyk of lemma negativeToRight(Eq)(1 term)(R) as text "lemma negativeToRight(Eq)(1 term)(R)" end text end define linebreak define pyk of lemma doubleMinus(R) as text "lemma doubleMinus(R)" end text end define linebreak define pyk of lemma uniqueNegative(R) as text "lemma uniqueNegative(R)" end text end define linebreak define pyk of lemma subtractEquationsLeft(R) as text "lemma subtractEquationsLeft(R)" end text end define linebreak define pyk of lemma eqNegated(R) as text "lemma eqNegated(R)" end text end define linebreak define pyk of lemma neqNegated(R) as text "lemma neqNegated(R)" end text end define linebreak define pyk of lemma -0=0(R) as text "lemma -0=0(R)" end text end define linebreak define pyk of lemma negativeNegated(R) as text "lemma negativeNegated(R)" end text end define linebreak define pyk of lemma from leqGeq(R) as text "lemma from leqGeq(R)" end text end define linebreak define pyk of lemma 0<=|x|(R) as text "lemma 0<=|x|(R)" end text end define linebreak define pyk of lemma positiveNegated(R) as text "lemma positiveNegated(R)" end text end define linebreak define pyk of lemma addEquations(R) as text "lemma addEquations(R)" end text end define linebreak define pyk of lemma times(-1)(R) as text "lemma times(-1)(R)" end text end define linebreak define pyk of lemma times(-1)Left(R) as text "lemma times(-1)Left(R)" end text end define linebreak define pyk of lemma -x-y=-(x+y)(R) as text "lemma -x-y=-(x+y)(R)" end text end define linebreak define pyk of lemma lessTotality(R) as text "lemma lessTotality(R)" end text end define linebreak define pyk of lemma sameNumerical(R) as text "lemma sameNumerical(R)" end text end define linebreak define pyk of lemma minusNegated(R) as text "lemma minusNegated(R)" end text end define linebreak define pyk of lemma positiveNumerical(R) as text "lemma positiveNumerical(R)" end text end define linebreak define pyk of lemma signNumerical(+)(R) as text "lemma signNumerical(+)(R)" end text end define linebreak define pyk of lemma nonnegativeNumerical(R) as text "lemma nonnegativeNumerical(R)" end text end define linebreak define pyk of lemma negativeNumerical(R) as text "lemma negativeNumerical(R)" end text end define linebreak define pyk of lemma leqNegated(R) as text "lemma leqNegated(R)" end text end define linebreak define pyk of lemma lessNegated(R) as text "lemma lessNegated(R)" end text end define linebreak define pyk of lemma subLeqRight(R) as text "lemma subLeqRight(R)" end text end define linebreak define pyk of lemma fromLess(R) as text "lemma fromLess(R)" end text end define linebreak define pyk of lemma distributionOut(R) as text "lemma distributionOut(R)" end text end define linebreak define pyk of lemma x*0+x=x(R) as text "lemma x*0+x=x(R)" end text end define linebreak define pyk of lemma x*0=0(R)fff as text "lemma x*0=0(R)fff" end text end define linebreak define pyk of lemma signNumerical(R) as text "lemma signNumerical(R)" end text end define linebreak define pyk of lemma numericalDifference(R) as text "lemma numericalDifference(R)" end text end define linebreak define pyk of lemma x<=|x|(R) as text "lemma x<=|x|(R)" end text end define linebreak define pyk of lemma USlimitIsUpperBound helper as text "lemma USlimitIsUpperBound helper" end text end define linebreak define pyk of lemma USlimitIsUpperBound as text "lemma USlimitIsUpperBound" end text end define linebreak define pyk of lemma (-1)*(-1)+(-1)*1=0(R) as text "lemma (-1)*(-1)+(-1)*1=0(R)" end text end define linebreak define pyk of lemma (-1)*(-1)=1(R) as text "lemma (-1)*(-1)=1(R)" end text end define linebreak define pyk of lemma 0<1Helper(R) as text "lemma 0<1Helper(R)" end text end define linebreak define pyk of lemma 0<1(R) as text "lemma 0<1(R)" end text end define linebreak define pyk of lemma expZero exact(R) as text "lemma expZero exact(R)" end text end define linebreak define pyk of lemma positiveBase(R) base as text "lemma positiveBase(R) base" end text end define linebreak define pyk of lemma three2twoFactors(R) as text "lemma three2twoFactors(R)" end text end define linebreak define pyk of lemma x=x*y*(1/y)(R) as text "lemma x=x*y*(1/y)(R)" end text end define linebreak define pyk of lemma neqMultiplication(R) as text "lemma neqMultiplication(R)" end text end define linebreak define pyk of lemma lessTransitivity(R) as text "lemma lessTransitivity(R)" end text end define linebreak define pyk of lemma 0<2(R) as text "lemma 0<2(R)" end text end define linebreak define pyk of lemma sameExp(R) base as text "lemma sameExp(R) base" end text end define linebreak define pyk of lemma sameExp(R) indu as text "lemma sameExp(R) indu" end text end define linebreak define pyk of lemma sameExp(R) as text "lemma sameExp(R)" end text end define linebreak define pyk of lemma subNeqLeft(R) as text "lemma subNeqLeft(R)" end text end define linebreak define pyk of lemma subNeqRight(R) as text "lemma subNeqRight(R)" end text end define linebreak define pyk of lemma nonzeroFactors(R) as text "lemma nonzeroFactors(R)" end text end define linebreak define pyk of lemma nonnegativeFactors(R) as text "lemma nonnegativeFactors(R)" end text end define linebreak define pyk of lemma positiveFactors(R) as text "lemma positiveFactors(R)" end text end define linebreak define pyk of lemma lessDivision(R) as text "lemma lessDivision(R)" end text end define linebreak define pyk of lemma 0<1/2(R) as text "lemma 0<1/2(R)" end text end define linebreak define pyk of lemma positiveToRight(Eq)(1 term)(R) as text "lemma positiveToRight(Eq)(1 term)(R)" end text end define linebreak define pyk of lemma exp(+1)(R) as text "lemma exp(+1)(R)" end text end define linebreak define pyk of lemma positiveBase(R) indu as text "lemma positiveBase(R) indu" end text end define linebreak define pyk of lemma positiveBase(R) as text "lemma positiveBase(R)" end text end define linebreak define pyk of lemma -x*y=-(x*y)(R) as text "lemma -x*y=-(x*y)(R)" end text end define linebreak define pyk of lemma positiveToLeft(Eq)(R) as text "lemma positiveToLeft(Eq)(R)" end text end define linebreak define pyk of lemma times1Left(R) as text "lemma times1Left(R)" end text end define linebreak define pyk of lemma x+x=2*x(R) as text "lemma x+x=2*x(R)" end text end define linebreak define pyk of lemma (1/2)x+(1/2)x=x(R) as text "lemma (1/2)x+(1/2)x=x(R)" end text end define linebreak define pyk of lemma distributionOut(Minus)(R) as text "lemma distributionOut(Minus)(R)" end text end define linebreak define pyk of lemma (1/2)(x+y)-x=(1/2)(y-x)(R) as text "lemma (1/2)(x+y)-x=(1/2)(y-x)(R)" end text end define linebreak define pyk of lemma intervalSize(R) base as text "lemma intervalSize(R) base" end text end define linebreak define pyk of lemma lessMultiplicationLeft(R) as text "lemma lessMultiplicationLeft(R)" end text end define linebreak define pyk of lemma negativeToLeft(Less)(R) as text "lemma negativeToLeft(Less)(R)" end text end define linebreak define pyk of lemma negativeToLeft(Less)(1 term)(R) as text "lemma negativeToLeft(Less)(1 term)(R)" end text end define linebreak define pyk of lemma y-(1/2)(x+y)=(1/2)(y-x)(R) as text "lemma y-(1/2)(x+y)=(1/2)(y-x)(R)" end text end define linebreak define pyk of lemma intervalSize(R) indu as text "lemma intervalSize(R) indu" end text end define linebreak define pyk of lemma intervalSize(R) as text "lemma intervalSize(R)" end text end define linebreak define pyk of lemma XSlessUS(R) as text "lemma XSlessUS(R)" end text end define linebreak define pyk of lemma USdecreasing(+1)(R) as text "lemma USdecreasing(+1)(R)" end text end define linebreak define pyk of lemma expUnbounded base as text "lemma expUnbounded base" end text end define linebreak define pyk of lemma expUnbounded indu as text "lemma expUnbounded indu" end text end define linebreak define pyk of lemma expUnbounded as text "lemma expUnbounded" end text end define linebreak define pyk of lemma 1<=x+1(N) as text "lemma 1<=x+1(N)" end text end define linebreak define pyk of lemma expNonzero base as text "lemma expNonzero base" end text end define linebreak define pyk of lemma expNonzero indu as text "lemma expNonzero indu" end text end define linebreak define pyk of lemma expNonzero as text "lemma expNonzero" end text end define linebreak define pyk of lemma expNonzero(2) as text "lemma expNonzero(2)" end text end define linebreak define pyk of lemma halfBase base as text "lemma halfBase base" end text end define linebreak define pyk of lemma halfBase indu as text "lemma halfBase indu" end text end define linebreak define pyk of lemma multiplyEquations(R) as text "lemma multiplyEquations(R)" end text end define linebreak define pyk of lemma nonreciprocalToRight(Eq)(1 term)(R) as text "lemma nonreciprocalToRight(Eq)(1 term)(R)" end text end define linebreak define pyk of lemma positiveNonzero(R) as text "lemma positiveNonzero(R)" end text end define linebreak define pyk of lemma nonzeroProduct(2)(R) as text "lemma nonzeroProduct(2)(R)" end text end define linebreak define pyk of lemma halfBase as text "lemma halfBase" end text end define linebreak define pyk of lemma three2threeFactors(R) as text "lemma three2threeFactors(R)" end text end define linebreak define pyk of lemma x*y=zBackwards(R) as text "lemma x*y=zBackwards(R)" end text end define linebreak define pyk of lemma positiveInverted(R) as text "lemma positiveInverted(R)" end text end define linebreak define pyk of lemma reciprocalToRight(Less)(R) as text "lemma reciprocalToRight(Less)(R)" end text end define linebreak define pyk of lemma reciprocalToRight(Less)(1 term)(R) as text "lemma reciprocalToRight(Less)(1 term)(R)" end text end define linebreak define pyk of lemma nonreciprocalToLeft(Less)(R) as text "lemma nonreciprocalToLeft(Less)(R)" end text end define linebreak define pyk of lemma 1
\newpage
\begin{list}{}{
\setlength{\leftmargin}{0em}
\setlength{\itemindent}{0em}
\setlength{\itemsep}{1ex}}
\item " [ math tex define sup2 as "sup2" end define end math ] "
\item " [ math tex define lemma leqTotality(R) as "LeqTotality(R)" end define end math ] "
\item " [ math tex define lemma positiveToLeft(Eq) as "PositiveToLeft(Eq)" end define end math ] "
\item " [ math tex define lemma expZero exact as "ExpZero(Exact) " end define end math ] "
\item " [ math tex define lemma +1IsPositive(N) as "(+1)IsPositive(N)" end define end math ] "
\item " [ math tex define lemma sameExp base as "SameExp(Base)" end define end math ] "
\item " [ math tex define lemma sameExp indu as "SameExp(Indu)" end define end math ] "
\item " [ math tex define lemma sameExp as "SameExp" end define end math ] "
\item " [ math tex define lemma exp(+1) as "Exp(+1)" end define end math ] "
\item " [ math tex define lemma distributionOut(Minus) as "DistributionOut(Minus)" end define end math ] "
\item " [ math tex define lemma (1/2)(x+y)-x=(1/2)(y-x) as "(1/2)(x+y)-x=(1/2)(y-x)" end define end math ] "
\item " [ math tex define lemma y-(1/2)(x+y)=(1/2)(y-x) as "y-(1/2)(x+y)=(1/2)(y-x)" end define end math ] "
\item " [ math tex define lemma positiveBase base as "PositiveBase(Base)" end define end math ] "
\item " [ math tex define lemma positiveBase indu as "PositiveBase(Indu)" end define end math ] "
\item " [ math tex define lemma positiveBase as "PositiveBase" end define end math ] "
\item " [ math tex define lemma positiveToRight(Eq)(1 term) as "PositiveToRight(Eq)(1 term)" end define end math ] "
\item " [ math tex define lemma base(1/2)Sum zero exact as "BSzero(Exact)" end define end math ] "
\item " [ math tex define lemma sameBase(1/2)Sum second base as "SameBS(2)(Base)" end define end math ] "
\item " [ math tex define lemma sameBase(1/2)Sum second indu as "SameBS(2)(Indu)" end define end math ] "
\item " [ math tex define lemma sameBase(1/2)Sum second as "SameBS(2)" end define end math ] "
\item " [ math tex define lemma negativeToLeft(Less)(1 term) as "NegativeToLeft(Less)(1 term)" end define end math ] "
\item " [ math tex define lemma base(1/2)Sum(+1) as "BS(+1)" end define end math ] "
\item " [ math tex define lemma base(1/2)Sum exact bound base as "BSbound(Exact)(Base)" end define end math ] "
\item " [ math tex define lemma base(1/2)Sum exact bound indu as "BSbound(Exact)(Indu)" end define end math ] "
\item " [ math tex define lemma base(1/2)Sum exact bound as "BSbound(Exact)" end define end math ] "
\item " [ math tex define lemma base(1/2)Sum bound as "BSbound" end define end math ] "
\item " [ math tex define lemma sameSeries(NumDiff) as "SameSeries(NumDiff)" end define end math ] "
\item " [ math tex define lemma UStelescope zero exact as "UStelescope(Zero)(Exact)" end define end math ] "
\item " [ math tex define lemma sameTelescope second base as "SameTelescope(2)(Base)" end define end math ] "
\item " [ math tex define lemma sameTelescope second indu as "SameTelescope(2)(Indu)" end define end math ] "
\item " [ math tex define lemma sameTelescope second as "SameTelescope(2)" end define end math ] "
\item " [ math tex define lemma telescopeNumerical base as "TelescopeNumerical(Base)" end define end math ] "
\item " [ math tex define lemma telescopeNumerical indu as "TelescopeNumerical(Indu)" end define end math ] "
\item " [ math tex define lemma telescopeNumerical as "TelescopeNumerical" end define end math ] "
\item " [ math tex define prop lemma to negated double imply as "ToNegatedDoubleImply" end define end math ] "
\item " [ math tex define lemma eqAdditionLeft(R) as "EqAdditionLeft(R)" end define end math ] "
\item " [ math tex define lemma x=x+(y-y)(R) as "x=x+(y-y)(R)" end define end math ] "
\item " [ math tex define lemma x=x+y-y(R) as "x=x+y-y(R)" end define end math ] "
\item " [ math tex define lemma three2twoTerms(R) as "Three2twoTerms(R)" end define end math ] "
\item " [ math tex define lemma positiveToRight(Less)(R) as "PositiveToRight(Less)(R)" end define end math ] "
\item " [ math tex define lemma three2threeTerms(R) as "Three2threeTerms(R)" end define end math ] "
\item " [ math tex define lemma plus0Left(R) as "Plus0Left(R)" end define end math ] "
\item " [ math tex define lemma positiveToRight(Eq)(R) as "PositiveToRight(Eq)(R)" end define end math ] "
\item " [ math tex define lemma subtractEquations(R) as "SubtractEquations(R)" end define end math ] "
\item " [ math tex define lemma neqAddition(R) as "NeqAddition(R)" end define end math ] "
\item " [ math tex define lemma positiveToRight(Less)(R) as "PositiveToRight(Less)(R)" end define end math ] "
\item " [ math tex define lemma positiveToRight(Less)(1 term)(R) as "PositiveToRight(Less)(1 term)(R)" end define end math ] "
\item " [ math tex define lemma to!!== as "To!!==" end define end math ] "
\item " [ math tex define lemma switchTerms(x<=y-z) as "SwitchTerms(x<=y-z)" end define end math ] "
\item " [ math tex define pred lemma (A)to(~E~)(Imply) as "(A)to(~E~)(Imply)" end define end math ] "
\item " [ math tex define pred lemma (E)to(~A~)(Imply) as "(E)to(~A~)(Imply)" end define end math ] "
\item " [ math tex define pred lemma (E~)to(~A)(Imply) as "(E~)to(~A)(Imply)" end define end math ] "
\item " [ math tex define pred lemma addNegatedAll as "AddNegatedAll" end define end math ] "
\item " [ math tex define pred lemma toNegatedAEA as "ToNegatedAEA " end define end math ] "
\item " [ math tex define lemma lessNeq(F) helper as "LessNeq(F)(Helper)" end define end math ] "
\item " [ math tex define lemma lessNeq(F) as "LessNeq(F)" end define end math ] "
\item " [ math tex define lemma lessNeq(R) as "LessNeq(R)" end define end math ] "
\item " [ math tex define lemma positiveToRight(Less)(1 term) as "PositiveToRight(Less)(1 term)" end define end math ] "
\item " [ math tex define pred lemma (A~)to(~E) as "(A~)to(~E)" end define end math ] "
\item " [ math tex define lemma toLeq(Advanced)(R) as "ToLeq(Advanced)(R)" end define end math ] "
\item " [ math tex define lemma leqNeqLess(R) as "LeqNeqLess(R)" end define end math ] "
\item " [ math tex define lemma subLeqLeft(R) as "SubLeqLeft(R)" end define end math ] "
\item " [ math tex define lemma leqLessTransitivity(R) as "LeqLessTransitivity(R)" end define end math ] "
\item " [ math tex define lemma negativeToLeft(Eq)(R) as "NegativeToLeft(Eq)(R)" end define end math ] "
\item " [ math tex define lemma negativeToRight(Less)(R) as "NegativeToRight(Less)(R)" end define end math ] "
\item " [ math tex define lemma !!==Symmetry as "!!==Symmetry" end define end math ] "
\item " [ math tex define lemma negativeToRight(Eq)(R) as "NegativeToRight(Eq)(R)" end define end math ] "
\item " [ math tex define lemma negativeToRight(Eq)(1 term)(R) as "NegativeToRight(Eq)(1 term)(R)" end define end math ] "
\item " [ math tex define lemma doubleMinus(R) as "DoubleMinus(R)" end define end math ] "
\item " [ math tex define lemma uniqueNegative(R) as "UniqueNegative(R)" end define end math ] "
\item " [ math tex define lemma subtractEquationsLeft(R) as "SubtractEquationsLeft(R)" end define end math ] "
\item " [ math tex define lemma eqNegated(R) as "EqNegated(R)" end define end math ] "
\item " [ math tex define lemma neqNegated(R) as "NeqNegated(R)" end define end math ] "
\item " [ math tex define lemma subLeqRight(R) as "SubLeqRight(R)" end define end math ] "
\item " [ math tex define lemma leqNegated(R) as "LeqNegated(R)" end define end math ] "
\item " [ math tex define lemma lessNegated(R) as "LessNegated(R)" end define end math ] "
\item " [ math tex define lemma -0=0(R) as "-0=0(R)" end define end math ] "
\item " [ math tex define lemma negativeNegated(R) as "NegativeNegated(R)" end define end math ] "
\item " [ math tex define lemma from leqGeq(R) as "FromLeqGeq(R)" end define end math ] "
\item " [ math tex define lemma fromLess(R) as "FromLess(R)" end define end math ] "
\item " [ math tex define lemma nonnegativeNumerical(R) as "NonnegativeNumerical(R)" end define end math ] "
\item " [ math tex define lemma negativeNumerical(R) as "NegativeNumerical(R)" end define end math ] "
\item " [ math tex define lemma 0<=|x|(R) as "0<=|x|(R)" end define end math ] "
\item " [ math tex define lemma positiveNegated(R) as "PositiveNegated(R)" end define end math ] "
\item " [ math tex define lemma addEquations(R) as "AddEquations(R)" end define end math ] "
\item " [ math tex define lemma distributionOut(R) as "DistributionOut(R)" end define end math ] "
\item " [ math tex define lemma x*0+x=x(R) as "x*0+x=x(R)" end define end math ] "
\item " [ math tex define lemma x*0=0(R)fff as "x*0=0(R)(fff)" end define end math ] "
\item " [ math tex define lemma times(-1)(R) as "Times(-1)(R)" end define end math ] "
\item " [ math tex define lemma times(-1)Left(R) as "Times(-1)Left(R)" end define end math ] "
\item " [ math tex define lemma -x-y=-(x+y)(R) as "-x-y=-(x+y)(R)" end define end math ] "
\item " [ math tex define lemma lessTotality(R) as "LessTotality(R)" end define end math ] "
\item " [ math tex define lemma sameNumerical(R) as "SameNumerical(R)" end define end math ] "
\item " [ math tex define lemma minusNegated(R) as "MinusNegated(R)" end define end math ] "
\item " [ math tex define lemma positiveNumerical(R) as "PositiveNumerical(R)" end define end math ] "
\item " [ math tex define lemma signNumerical(+)(R) as "SignNumerical(+)(R)" end define end math ] "
\item " [ math tex define lemma signNumerical(R) as "SignNumerical(R)" end define end math ] "
\item " [ math tex define lemma numericalDifference(R) as "NumericalDifference(R)" end define end math ] "
\item " [ math tex define lemma x<=|x|(R) as "x<=|x|(R)" end define end math ] "
\item " [ math tex define lemma USlimitIsUpperBound helper as "USlimitIsUpperBound(Helper)" end define end math ] "
\item " [ math tex define lemma USlimitIsUpperBound as "USlimitIsUpperBound" end define end math ] "
\item " [ math tex define lemma (-1)*(-1)+(-1)*1=0(R) as "(-1)*(-1)+(-1)*1=0(R)" end define end math ] "
\item " [ math tex define lemma (-1)*(-1)=1(R) as "(-1)*(-1)=1(R)" end define end math ] "
\item " [ math tex define lemma 0<1Helper(R) as "0<1Helper(R)" end define end math ] "
\item " [ math tex define lemma 0<1(R) as "0<1(R)" end define end math ] "
\item " [ math tex define lemma expZero exact(R) as "ExpZero(Exact)(R)" end define end math ] "
\item " [ math tex define lemma positiveBase(R) base as "PositiveBase(R)(Base)" end define end math ] "
\item " [ math tex define lemma three2twoFactors(R) as "Three2twoFactors(R)" end define end math ] "
\item " [ math tex define lemma x=x*y*(1/y)(R) as "x=x*y*(1/y)(R)" end define end math ] "
\item " [ math tex define lemma neqMultiplication(R) as "NeqMultiplication(R)" end define end math ] "
\item " [ math tex define lemma lessTransitivity(R) as "LessTransitivity(R)" end define end math ] "
\item " [ math tex define lemma 0<2(R) as "0<2(R)" end define end math ] "
\item " [ math tex define lemma sameExp(R) base as "SameExp(R)(Base)" end define end math ] "
\item " [ math tex define lemma sameExp(R) indu as "SameExp(R)(Indu)" end define end math ] "
\item " [ math tex define lemma sameExp(R) as "SameExp(R)" end define end math ] "
\item " [ math tex define lemma subNeqLeft(R) as "SubNeqLeft(R)" end define end math ] "
\item " [ math tex define lemma subNeqRight(R) as "SubNeqRight(R)" end define end math ] "
\item " [ math tex define lemma nonzeroFactors(R) as "NonzeroFactors(R)" end define end math ] "
\item " [ math tex define lemma nonnegativeFactors(R) as "NonnegativeFactors(R)" end define end math ] "
\item " [ math tex define lemma positiveFactors(R) as "PositiveFactors(R)" end define end math ] "
\item " [ math tex define lemma lessDivision(R) as "LessDivision(R)" end define end math ] "
\item " [ math tex define lemma 0<1/2(R) as "0<1/2(R)" end define end math ] "
\item " [ math tex define lemma positiveToRight(Eq)(1 term)(R) as "PositiveToRight(Eq)(1 term)(R)" end define end math ] "
\item " [ math tex define lemma exp(+1)(R) as "Exp(+1)(R)" end define end math ] "
\item " [ math tex define lemma positiveBase(R) indu as "PositiveBase(R)(Indu)" end define end math ] "
\item " [ math tex define lemma positiveBase(R) as "PositiveBase(R)" end define end math ] "
\item " [ math tex define lemma -x*y=-(x*y)(R) as "-x*y=-(x*y)(R)" end define end math ] "
\item " [ math tex define lemma positiveToLeft(Eq)(R) as "PositiveToLeft(Eq)(R)" end define end math ] "
\item " [ math tex define lemma times1Left(R) as "Times1Left(R)" end define end math ] "
\item " [ math tex define lemma x+x=2*x(R) as "x+x=2*x(R)" end define end math ] "
\item " [ math tex define lemma (1/2)x+(1/2)x=x(R) as "(1/2)x+(1/2)x=x(R)" end define end math ] "
\item " [ math tex define lemma distributionOut(Minus)(R) as "DistributionOut(Minus)(R)" end define end math ] "
\item " [ math tex define lemma (1/2)(x+y)-x=(1/2)(y-x)(R) as "(1/2)(x+y)-x=(1/2)(y-x)(R)" end define end math ] "
\item " [ math tex define lemma intervalSize(R) base as "IntervalSize(R)(Base)" end define end math ] "
\item " [ math tex define lemma lessMultiplicationLeft(R) as "LessMultiplicationLeft(R)" end define end math ] "
\item " [ math tex define lemma negativeToLeft(Less)(R) as "NegativeToLeft(Less)(R)" end define end math ] "
\item " [ math tex define lemma negativeToLeft(Less)(1 term)(R) as "NegativeToLeft(Less)(1 term)(R)" end define end math ] "
\item " [ math tex define lemma y-(1/2)(x+y)=(1/2)(y-x)(R) as "y-(1/2)(x+y)=(1/2)(y-x)(R)" end define end math ] "
\item " [ math tex define lemma intervalSize(R) indu as "IntervalSize(R)(Indu)" end define end math ] "
\item " [ math tex define lemma intervalSize(R) as "IntervalSize(R)" end define end math ] "
\item " [ math tex define lemma XSlessUS(R) as "XSlessUS(R)" end define end math ] "
\item " [ math tex define lemma USdecreasing(+1)(R) as "USdecreasing(+1)(R)" end define end math ] "
\item " [ math tex define lemma 1<=x+1(N) as "1<=x+1(N)" end define end math ] "
\item " [ math tex define lemma expUnbounded base as "ExpUnbounded(Base)" end define end math ] "
\item " [ math tex define lemma expUnbounded indu as "ExpUnbounded(Indu)" end define end math ] "
\item " [ math tex define lemma expUnbounded as "ExpUnbounded" end define end math ] "
\item " [ math tex define lemma nonzeroProduct(2)(R) as "NonzeroProduct(2)(R)" end define end math ] "
\item " [ math tex define lemma positiveNonzero(R) as "PositiveNonzero(R)" end define end math ] "
\item " [ math tex define lemma nonreciprocalToRight(Eq)(1 term)(R) as "NonreciprocalToRight(Eq)(1 term)(R)" end define end math ] "
\item " [ math tex define lemma expNonzero base as "ExpNonzero(Base)" end define end math ] "
\item " [ math tex define lemma expNonzero indu as "ExpNonzero(Indu)" end define end math ] "
\item " [ math tex define lemma expNonzero as "ExpNonzero" end define end math ] "
\item " [ math tex define lemma multiplyEquations(R) as "MultiplyEquations(R)" end define end math ] "
\item " [ math tex define lemma expNonzero(2) as "ExpNonzero(2)" end define end math ] "
\item " [ math tex define lemma halfBase base as "HalfBase(Base)" end define end math ] "
\item " [ math tex define lemma halfBase indu as "HalfBase(Indu)" end define end math ] "
\item " [ math tex define lemma halfBase as "HalfBase" end define end math ] "
\item " [ math tex define lemma three2threeFactors(R) as "Three2threeFactors(R)" end define end math ] "
\item " [ math tex define lemma x*y=zBackwards(R) as "x*y=zBackwards(R)" end define end math ] "
\item " [ math tex define lemma positiveInverted(R) as "PositiveInverted(R)" end define end math ] "
\item " [ math tex define lemma reciprocalToRight(Less)(R) as "ReciprocalToRight(Less)(R)" end define end math ] "
\item " [ math tex define lemma reciprocalToRight(Less)(1 term)(R) as "ReciprocalToRight(Less)(1 term)(R)" end define end math ] "
\item " [ math tex define lemma nonreciprocalToLeft(Less)(R) as "NonreciprocalToLeft(Less)(R)" end define end math ] "
\item " [ math tex define lemma 1
\item " [ math tex define lemma switchFactors(1/x
\item " [ math tex define lemma intervalSize(anyPositive) as "IntervalSize(anyPositive)" end define end math ] "
\item " [ math tex define lemma USdecreasing(+n) base as "USdecreasing(+n)(Base)" end define end math ] "
\item " [ math tex define lemma USdecreasing(+n) indu as "USdecreasing(+n)(Indu)" end define end math ] "
\item " [ math tex define lemma USdecreasing(+n) as "USdecreasing(+n)" end define end math ] "
\item " [ math tex define lemma USdecreasing as "USdecreasing" end define end math ] "
\item " [ math tex define lemma leqAdditionLeft(R) as "LeqAdditionLeft(R)" end define end math ] "
\item " [ math tex define lemma toNotLess(R) as "ToNotLess(R)" end define end math ] "
\item " [ math tex define lemma limitOfUSIsLeq as "LimitOfUSIsLeq" end define end math ] "
\item " [ math tex define lemma subtractEquations(Less)(R) as "SubtractEquations(Less)(R)" end define end math ] "
\item " [ math tex define lemma subtractEquationsLeft(Less)(R) as "SubtractEquationsLeft(Less)(R)" end define end math ] "
\item " [ math tex define lemma lessNegated(Negative)(R) as "LessNegated(Negative)(R)" end define end math ] "
\item " [ math tex define prop lemma from negated and (imply) as "FromNegatedAnd(Imply)" end define end math ] "
\item " [ math tex define prop lemma remove double neg (consequent) as "RemoveDoubleNeg(Consequent)" end define end math ] "
\item " [ math tex define lemma fromNotUpperBound as "FromNotUpperBound" end define end math ] "
\item " [ math tex define lemma leqNUB as "LeqNUB" end define end math ] "
\item " [ math tex define lemma USlimitIsLeastUpperBound helper as "USlimitIsLeastUpperBound(Helper)" end define end math ] "
\item " [ math tex define lemma USlimitIsLeastUpperBound as "USlimitIsLeastUpperBound" end define end math ] "
\item " [ math tex define pred lemma exist mp3 as "ExistMP3" end define end math ] "
\item " [ math tex define lemma greaterPositive(N) as "GreaterPositive(N)" end define end math ] "
\item " [ math tex define lemma ysFClose helper as "ysFClose(Helper)" end define end math ] "
\item " [ math tex define lemma ysFClose as "ysFClose" end define end math ] "
\item " [ math tex define lemma ysFCauchy helper as "ysFCauchy(Helper)" end define end math ] "
\item " [ math tex define lemma ysFCauchy as "ysFCauchy" end define end math ] "
\item " [ math tex define lemma from<<== as "from<<==" end define end math ] "
\item " [ math tex define lemma nonnegativeNumerical(F) as "NonnegativeNumerical(F)" end define end math ] "
\item " [ math tex define lemma to<<== as "to<<==" end define end math ] "
\item " [ math tex define lemma negativeNumerical(F) as "NegativeNumerical(F)" 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,