PAGE sup BIBLIOGRAPHY "base" nani keta kute sena seku kuka kute tuti teke tati tetu sise sinu seku kuna tetu kisu kune nane tise kike kesi seku kana sasu sane kika sunu nasa natu, "check" nani tusi nese tutu kena kane sine setu siti kene keni tite tena sasi sasa site sutu sane nita nini nasi kana sane suka sane sasu kika sunu nasa natu, "kvanti" nani kuku seka sesi situ tasi kiti kisa naki nata sike kisu nenu suna tisu tase nuse kenu kusa teta nune kuta suku kaka saku keka suse sutu nasa natu PREASSOCIATIVE ""; RR, KVANTI (linie 23...) "base" bracket " end bracket "check" general macro define " as " end define "kvanti" cdots ""; REGELLEMMAER "" lemma to!!== ""; UDSAGNSLOGIK "" prop lemma to negated double imply "" prop lemma to negated and(1) ""; PRAEDIKATLOGK "" pred lemma addNegatedAll "" pred lemma (A)to(~E~)(Imply) "" pred lemma (E)to(~A~)(Imply) "" pred lemma (E~)to(~A)(Imply) "" pred lemma toNegatedAEA ""; MINUS "" lemma uniqueNegative "" lemma doubleMinus "" lemma minusNegated ""; EQ "" lemma eqReflexivity "" lemma eqSymmetry "" lemma eqTransitivity "" lemma eqTransitivity4 "" lemma eqTransitivity5 "" lemma eqTransitivity6 "" lemma addEquations "" lemma subtractEquations "" lemma subtractEquationsLeft "" lemma multiplyEquations "" lemma eqNegated "" lemma positiveToRight(Eq) "" lemma positiveToLeft(Eq) "" lemma positiveToLeft(Eq)(1 term) "" lemma negativeToLeft(Eq) "" lemma nonreciprocalToRight(Eq)(1 term) "" lemma distributionOut(Minus) "" lemma positiveToRight(Eq)(1 term) "" lemma sameSeries(NumDiff) "" lemma plusAssociativity(4 terms) ""; NEQ "" lemma lessNeq "" lemma neqSymmetry "" lemma neqNegated "" lemma subNeqRight "" lemma subNeqLeft "" lemma negativeToRight(Neq)(1 term) "" lemma neqAddition "" lemma neqMultiplication "" lemma nonzeroProduct(2) ""; LEQ "" lemma switchTerms(x<=y-z) ""; LESS "" lemma negativeToLeft(Less)(1 term) ""; NATURLIGE TAL "" lemma +1IsPositive(N) ""; REGNESTYKKER "" lemma (1/2)(x+y)-x=(1/2)(y-x) "" lemma y-(1/2)(x+y)=(1/2)(y-x) ""; EXP "" lemma expZero exact "" lemma sameExp base "" lemma sameExp indu "" lemma sameExp "" lemma exp(+1) "" lemma positiveBase base "" lemma positiveBase indu "" lemma positiveBase ""; BASE(1/2)SUM "" lemma base(1/2)Sum zero exact "" lemma sameBase(1/2)Sum second base "" lemma sameBase(1/2)Sum second indu "" lemma sameBase(1/2)Sum second "" lemma base(1/2)Sum(+1) "" lemma base(1/2)Sum exact bound base "" lemma base(1/2)Sum exact bound indu "" lemma base(1/2)Sum exact bound "" lemma base(1/2)Sum bound ""; TELESCOPE "" lemma UStelescope zero exact "" lemma sameTelescope second base "" lemma sameTelescope second indu "" lemma sameTelescope second "" lemma UStelescope(+1) "" lemma telescopeNumerical base "" lemma telescopeNumerical indu "" lemma telescopeNumerical "" lemma telescopeBound base "" lemma telescopeBound indu "" lemma telescopeBound ""; F/R "" lemma lessNeq(F) helper "" lemma lessNeq(F) "" lemma lessNeq(R) ""; SUP "" lemma intervalSize base "" lemma intervalSize indu "" lemma intervalSize "" lemma XSlessUS "" lemma USdecreasing(+1) "" lemma closeUS "" lemma closeUS(n+1) ""; PRAEXXDIKATLOGIK "" pred lemma allNegated(Imply) "" pred lemma existNegated(Imply) "" pred lemma intro exist helper "" pred lemma intro exist "" pred lemma exist mp "" pred lemma exist mp2 "" pred lemma 2exist mp "" pred lemma 2exist mp2 "" pred lemma EAE mp "" pred lemma addAll "" pred lemma addExist helper1 "" pred lemma addExist helper2 "" pred lemma addExist "" pred lemma addExist(SimpleAnt) "" pred lemma addExist(Simple) "" pred lemma addEAE "" pred lemma AEAnegated "" pred lemma EEAnegated ""; REGELLEMMAER "" lemma induction "" lemma leqAntisymmetry "" lemma leqTransitivity "" lemma leqAddition "" lemma leqMultiplication "" lemma reciprocal "" lemma equality "" lemma eqLeq "" lemma eqAddition "" lemma eqMultiplication ""; LEQ "" lemma leqMultiplicationLeft "" lemma leqLessEq "" lemma lessLeq "" lemma from leqGeq "" lemma subLeqRight "" lemma subLeqLeft "" lemma leqPlus1 "" lemma positiveToRight(Leq) "" lemma positiveToRight(Leq)(1 term) "" lemma negativeToRight(Leq) "" lemma positiveToLeft(Leq) "" lemma negativeToLeft(Leq) "" lemma negativeToLeft(Leq)(1 term) "" lemma leqAdditionLeft "" lemma leqSubtraction "" lemma leqSubtractionLeft "" lemma thirdGeq "" lemma leqNegated "" lemma addEquations(Leq) "" lemma multiplyEquations(Leq) "" lemma thirdGeqSeries ""; LESS "" lemma leqNeqLess "" lemma fromLess "" lemma toLess "" lemma fromNotLess "" lemma toNotLess "" lemma negativeLessPositive "" lemma leqLessTransitivity "" lemma lessLeqTransitivity "" lemma lessTransitivity "" lemma lessTotality "" lemma subLessRight "" lemma subLessLeft "" lemma switchTerms(x