Logiweb dictionary of sup

Up Help

0 0 sup 1 0 To!! == 2 0 ToNegatedDoubleImply 3 0 ToNegatedAnd(1) 4 0 AddNegatedAll 5 0 (A)to( E )(Imply) 6 0 (E)to( A )(Imply) 7 0 (E )to( A)(Imply) 8 0 ToNegatedAEA 9 0 UniqueNegative 10 0 DoubleMinus 11 0 MinusNegated 12 0 eqReflexivity 13 0 eqSymmetry 14 0 eqTransitivity 15 0 eqTransitivity4 16 0 eqTransitivity5 17 0 eqTransitivity6 18 0 AddEquations 19 0 SubtractEquations 20 0 SubtractEquationsLeft 21 0 MultiplyEquations 22 0 EqNegated 23 0 PositiveToRight(Eq) 24 0 PositiveToLeft(Eq) 25 0 PositiveToLeft(Eq)(1term) 26 0 NegativeToLeft(Eq) 27 0 NonreciprocalToRight(Eq)(1term) 28 0 DistributionOut(Minus)

29 0 PositiveToRight(Eq)(1term) 30 0 SameSeries(NumDiff) 31 0 PlusAssociativity(4terms) 32 0 LessNeq 33 0 NeqSymmetry 34 0 NeqNegated 35 0 SubNeqRight 36 0 SubNeqLeft 37 0 NegativeToRight(Neq)(1term) 38 0 NeqAddition 39 0 NeqMultiplication 40 0 NonzeroProduct(2) 41 0 SwitchTerms(x <= y − z) 42 0 NegativeToLeft(Less)(1term) 43 0 (+1)IsPositive(N) 44 0 (1/2)(x + y) − x = (1/2)(y − x) 45 0 y − (1/2)(x + y) = (1/2)(y − x) 46 0 ExpZero(Exact) 47 0 SameExp(Base) 48 0 SameExp(Indu) 49 0 SameExp 50 0 Exp(+1) 51 0 PositiveBase(Base) 52 0 PositiveBase(Indu) 53 0 PositiveBase 54 0 BSzero(Exact) 55 0 SameBS(2)(Base) 56 0 SameBS(2)(Indu) 57 0 SameBS(2) 58 0 BS(+1) 59 0 BSbound(Exact)(Base) 60 0 BSbound(Exact)(Indu) 61 0 BSbound(Exact) 62 0 BSbound 63 0 UStelescope(Zero)(Exact) 64 0 SameTelescope(2)(Base) 65 0 SameTelescope(2)(Indu) 66 0 SameTelescope(2) 67 0 UStelescope(+1) 68 0 TelescopeNumerical(Base) 69 0 TelescopeNumerical(Indu) 70 0 TelescopeNumerical 71 0 TelescopeBound(Base) 72 0 TelescopeBound(Indu) 73 0 TelescopeBound 74 0 LessNeq(F)(Helper) 75 0 LessNeq(F) 76 0 LessNeq(R) 77 0 IntervalSize(Base) 78 0 IntervalSize(Indu) 79 0 IntervalSize 80 0 XS < US

81 0 lemma USdecreasing(+1)

82 0 CloseUS 83 0 CloseUS(n + 1) 84 0 AllNegated(Imply) 85 0 ExistNegated(Imply) 86 0 IntroExist(Helper) 87 0 IntroExist 88 0 ExistMP 89 0 ExistMP2 90 0 TwiceExistMP 91 0 TwiceExistMP2 92 0 EAE − MP 93 0 AddAll 94 0 AddExist(Helper1) 95 0 AddExist(Helper2) 96 0 AddExist 97 0 AddExist(SimpleAnt) 98 0 AddExist(Simple) 99 0 AddEAE 100 0 AEA − negated 101 0 EEA − negated 102 0 Induction 103 0 leqAntisymmetry 104 0 leqTransitivity 105 0 leqAddition 106 0 leqMultiplication 107 0 Reciprocal 108 0 Equality 109 0 eqLeq 110 0 eqAddition 111 0 eqMultiplication 112 0 LeqMultiplicationLeft 113 0 LeqLessEq 114 0 LessLeq 115 0 FromLeqGeq 116 0 subLeqRight 117 0 subLeqLeft 118 0 Leq + 1 119 0 PositiveToRight(Leq) 120 0 PositiveToRight(Leq)(1term)

121 0 lemma negativeToRight(Leq)

122 0 PositiveToLeft(Leq) 123 0 negativeToLeft(Leq) 124 0 negativeToLeft(Leq)(1term) 125 0 LeqAdditionLeft 126 0 leqSubtraction 127 0 leqSubtractionLeft 128 0 thirdGeq 129 0 LeqNegated 130 0 AddEquations(Leq)

131 0 MultiplyEquations(Leq) 132 0 ThirdGeqSeries 133 0 LeqNeqLess 134 0 FromLess 135 0 ToLess 136 0 fromNotLess 137 0 toNotLess 138 0 NegativeLessPositive 139 0 leqLessTransitivity 140 0 LessLeqTransitivity 141 0 LessTransitivity 142 0 LessTotality 143 0 SubLessRight 144 0 SubLessLeft 145 0 SwitchTerms(x < y − z) 146 0 SwitchTerms(x − y < z) 147 0 LessAddition 148 0 LessAdditionLeft 149 0 LessMultiplication 150 0 LessMultiplicationLeft 151 0 LessDivision 152 0 PositiveToRight(Less) 153 0 PositiveToLeft(Less) 154 0 NegativeToLeft(Less) 155 0 NegativeToRight(Less) 156 0 AddEquations(Less) 157 0 AddEquations(LeqLess) 158 0 reciprocalToLeft(Less) 159 0 LessNegated 160 0 PositiveNonzero 161 0 PositiveNegated 162 0 NonpositiveNegated 163 0 NegativeNegated 164 0 NonnegativeNegated 165 0 PositiveHalved 166 0 PositiveInverted 167 0 NonnegativeNumerical 168 0 NegativeNumerical 169 0 PositiveNumerical

170 0 lemma nonpositiveNumerical

171 0 |0| = 0 172 0 0 <= |x| 173 0 x <= |x| 174 0 FromPositiveNumerical 175 0 SameNumerical 176 0 SignNumerical(+) 177 0 SignNumerical 178 0 ToNumericalLess 179 0 FromNumericalGreater 180 0 NumericalDifference 181 0 NumericalDifferenceLess(Helper) 182 0 NumericalDifferenceLess 183 0 SplitNumericalSumHelper 184 0 splitNumericalSum(++) 185 0 splitNumericalSum(−−) 186 0 splitNumericalSum(+ − small) 187 0 splitNumericalSum(+ − big) 188 0 splitNumericalSum(+−) 189 0 splitNumericalSum(−+) 190 0 splitNumericalSum 191 0 SplitNumericalProduct(++) 192 0 SplitNumericalProduct(+−) 193 0 SplitNumericalProduct 194 0 insertMiddleTerm(Numerical) 195 0 insertTwoMiddleTerms(Numerical) 196 0 Three2twoTerms 197 0 Three2threeTerms 198 0 Three2twoFactors 199 0 Three2threeFactors 200 0 Times(−1) 201 0 Times(−1)Left 202 0 MaxLeq(1) 203 0 MaxLeq(2) 204 0 LessThanMax 205 0 x + y = zBackwards 206 0 x ∗ y = zBackwards 207 0 x = x + (y − y) 208 0 x = x + y − y 209 0 x = x ∗ y ∗ (1/y) 210 0 insertMiddleTerm(Sum) 211 0 insertTwoMiddleTerms(Sum) 212 0 insertMiddleTerm(Difference) 213 0 x ∗ 0 + x = x 214 0 x ∗ 0 = 0 215 0 NonnegativeFactors 216 0 NonzeroFactors 217 0 PositiveFactors 218 0 PlusTimesMinus 219 0 MinusTimesMinus 220 0 (−1) ∗ (−1) + (−1) ∗ 1 = 0 221 0 (−1) ∗ (−1) = 1 222 0 0 < 1Helper 223 0 0 < 1 224 0 0 < 2 225 0 0 < 3 226 0 0 < 1/2 227 0 0 < 1/3 228 0 TwoWholes 229 0 ThreeWholes 230 0 TwoHalves 231 0 ThreeThirds 232 0 −x − y = −(x + y)

233 0 −x ∗ y = −(x ∗ y) 234 0 −0 = 0 235 0 SFsymmetry 236 0 SFtransitivity 237 0 f2R(Plus) 238 0 f2R(Times) 239 0 << TransitivityHelper(Q) 240 0 << Transitivity 241 0 <<== Reflexivity 242 0 <<== AntisymmetryHelper(Q) 243 0 FromNot < f(Weak)(Helper) 244 0 FromNot < f(Weak) 245 0 FromNot < f(Strong)(Helper2) 246 0 FromNot < f(Strong)(Helper) 247 0 FromNot < f(Strong) 248 0 fromNotSameF(Strongest)(Helper2) 249 0 fromNotSameF(Strongest)(Helper) 250 0 fromNotSameF(Strongest) 251 0 ToLess(F)(Helper) 252 0 ToLess(F) 253 0 FromNot << 254 0 ToLess(R) 255 0 LeqTotality(R) 256 0 FromNotSameF(Weak)(Helper) 257 0 FromNotSameF(Weak) 258 0 FromNotLess(F) 259 0 == Addition 260 0 == AdditionLeft 261 0 Fpart − Bounded(Base) 262 0 Fpart − Bounded(InduHelper) 263 0 Fpart − Bounded(Indu) 264 0 Fpart − Bounded 265 0 F − Bounded(Helper) 266 0 F − Bounded 267 0 SameFmultiplication(Helper) 268 0 SameFmultiplication 269 0 EqMultiplication(R) 270 0 EqMultiplicationLeft(R) 271 0 x ∗ 0 = 0(F) 272 0 x ∗ 0 = 0(R) 273 0 LessMultiplication(F)(Helper2) 274 0 LessMultiplication(F)(Helper) 275 0 LessMultiplication(F) 276 0 LessMultiplication(R) 277 0 LeqMultiplication(R) 278 0 PlusAssociativity(F) 279 0 Plus0(F) 280 0 PlusCommutativity(F) 281 0 TimesAssociativity(F) 282 0 Times1f 283 0 Cauchy(2)(Helper) 284 0 Cauchy(2) 285 0 ReciprocalFnonzero 286 0 ReciprocalFnynonzero 287 0 (Eventually = f)2sameF(Helper) 288 0 (Eventually = f)2sameF 289 0 FromNotSameF(Strong)(Helper2) 290 0 FromNotSameF(Strong)(Helper) 291 0 FromNotSameF(Strong) 292 0 SameFreciprocal(Helper) 293 0 SameFreciprocal 294 0 From!! == 295 0 Reciprocal(R) 296 0 TimesCommutativity(F) 297 0 Distribution(F) 298 0 FromMax(1) 299 0 FromMax(2) 300 0 ToNegatedAnd 301 0 PositiveToRight(Less)(1term) 302 0 (A )to( E)

303 0 lemma ==Transitivity4

304 0 Plus0Left(R) 305 0 x = x + (y − y)(R) 306 0 x = x + y − y(R) 307 0 PositiveToRight(Eq)(R) 308 0 SubtractEquations(R) 309 0 NeqAddition(R) 310 0 EqAdditionLeft(R) 311 0 Three2twoTerms(R) 312 0 PositiveToRight(Less)(R) 313 0 Three2threeTerms(R) 314 0 PositiveToRight(Less)(1term)(R) 315 0 ToLeq(Advanced)(R) 316 0 LeqNeqLess(R) 317 0 SubLeqLeft(R) 318 0 LeqLessTransitivity(R) 319 0 NegativeToLeft(Eq)(R) 320 0 NegativeToRight(Less)(R) 321 0 !! == Symmetry 322 0 NegativeToRight(Eq)(R) 323 0 NegativeToRight(Eq)(1term)(R) 324 0 DoubleMinus(R) 325 0 UniqueNegative(R) 326 0 SubtractEquationsLeft(R) 327 0 EqNegated(R) 328 0 NeqNegated(R) 329 0 LeqNegated(R) 330 0 LessNegated(R) 331 0 −0 = 0(R) 332 0 NegativeNegated(R) 333 0 FromLeqGeq(R) 334 0 SubLeqRight(R)

335 0 FromLess(R) 336 0 NonnegativeNumerical(R) 337 0 NegativeNumerical(R) 338 0 0 <= |x|(R) 339 0 PositiveNegated(R) 340 0 AddEquations(R) 341 0 DistributionOut(R) 342 0 == Transitivity5 343 0 x ∗ 0 + x = x(R) 344 0 x ∗ 0 = 0(R)(fff) 345 0 Times(−1)(R) 346 0 Times(−1)Left(R) 347 0 −x − y = −(x + y)(R) 348 0 LessTotality(R) 349 0 PositiveNumerical(R) 350 0 SignNumerical(+)(R) 351 0 SameNumerical(R) 352 0 MinusNegated(R) 353 0 SignNumerical(R) 354 0 NumericalDifference(R) 355 0 x <= |x|(R) 356 0 USlimitIsUpperBound(Helper) 357 0 USlimitIsUpperBound 358 0 (−1) ∗ (−1) + (−1) ∗ 1 = 0(R) 359 0 (−1) ∗ (−1) = 1(R) 360 0 0 < 1Helper(R) 361 0 0 < 1(R) 362 0 ExpZero(Exact)(R) 363 0 PositiveBase(R)(Base) 364 0 Three2twoFactors(R) 365 0 x = x ∗ y ∗ (1/y)(R) 366 0 NeqMultiplication(R) 367 0 LessTransitivity(R) 368 0 0 < 2(R)

369 0 SameExp(R)(Base) 370 0 SameExp(R)(Indu) 371 0 SameExp(R) 372 0 SubNeqLeft(R) 373 0 SubNeqRight(R) 374 0 NonzeroFactors(R) 375 0 NonnegativeFactors(R) 376 0 PositiveFactors(R) 377 0 LessDivision(R) 378 0 0 < 1/2(R) 379 0 PositiveToRight(Eq)(1term)(R) 380 0 Exp(+1)(R) 381 0 PositiveBase(R)(Indu) 382 0 PositiveBase(R) 383 0 −x ∗ y = −(x ∗ y)(R) 384 0 PositiveToLeft(Eq)(R) 385 0 Times1Left(R) 386 0 == Transitivity6 387 0 x + x = 2 ∗ x(R) 388 0 (1/2)x + (1/2)x = x(R) 389 0 DistributionOut(Minus)(R) 390 0 (1/2)(x + y) − x = (1/2)(y − x)(R) 391 0 IntervalSize(R)(Base) 392 0 LessMultiplicationLeft(R) 393 0 NegativeToLeft(Less)(R) 394 0 NegativeToLeft(Less)(1term)(R) 395 0 y − (1/2)(x + y) = (1/2)(y − x)(R) 396 0 IntervalSize(R)(Indu) 397 0 IntervalSize(R) 398 0 XSlessUS(R) 399 0 USdecreasing(+1)(R) 400 0 ExpUnbounded(Base) 401 0 ExpUnbounded(Indu) 402 0 ExpUnbounded 403 0 1 <= x + 1(N) 404 0 NonzeroProduct(2)(R) 405 0 PositiveNonzero(R) 406 0 NonreciprocalToRight(Eq)(1term)(R) 407 0 ExpNonzero(Base) 408 0 ExpNonzero(Indu) 409 0 ExpNonzero 410 0 ExpNonzero(2) 411 0 MultiplyEquations(R) 412 0 HalfBase(Base) 413 0 HalfBase(Indu) 414 0 HalfBase 415 0 Three2threeFactors(R) 416 0 x ∗ y = zBackwards(R) 417 0 PositiveInverted(R) 418 0 ReciprocalToRight(Less)(R) 419 0 ReciprocalToRight(Less)(1term)(R) 420 0 NonreciprocalToLeft(Less)(R) 421 0 1 < x ∗ y(R) 422 0 SwitchFactors(1/x < y)(R) 423 0 SmallHalving 424 0 IntervalSize(anyPositive) 425 0 USdecreasing(+n)(Base) 426 0 USdecreasing(+n)(Indu) 427 0 USdecreasing(+n) 428 0 USdecreasing 429 0 LeqAdditionLeft(R) 430 0 ToNotLess(R) 431 0 LimitOfUSIsLeq 432 0 SubtractEquations(Less)(R) 433 0 SubtractEquationsLeft(Less)(R) 434 0 LessNegated(Negative)(R) 435 0 FromNegatedAnd(Imply) 436 0 RemoveDoubleNeg(Consequent)

437 0 FromNotUpperBound 438 0 DistributionOut 439 0 DistributionOutLeft 440 0 DistributionLeft 441 0 LeqNUB 442 0 USlimitIsLeastUpperBound(Helper) 443 0 USlimitIsLeastUpperBound 444 0 FromNotLess(R) 445 0 ExistMP3 446 0 GreaterPositive(N) 447 0 ysFClose(Helper) 448 0 ysFClose 449 0 ysFCauchy(Helper) 450 0 ysFCauchy 451 0 CartProdIsRelation 452 0 FromSubset 453 0 SubsetIsRelation 454 0 ToSeries 455 0 FromSeries 456 0 SeriesSubsetCP 457 0 ValueType 458 0 RemoveOr 459 0 FromSingleton 460 0 InPair(1) 461 0 InPair(2) 462 0 SameMember(2) 463 0 ToBinaryUnion(1) 464 0 ToBinaryUnion(2) 465 0 FromOrderedPair(TwoLevels) 466 0 ToCartProd(Helper) 467 0 ToCartProd 468 0 NonreciprocalToRight(Eq) 469 0 NonreciprocalToLeft(Eq)(1term) 470 0 SameReciprocal 471 0 CPseparationIsRelation 472 0 OrderedPairEquality 473 0 ReciprocalIsFunction 474 0 ReciprocalIsTotal 475 0 ReciprocalIsRationalSeries 476 0 CrsIsRelation 477 0 CrsIsFunction 478 0 CrsIsTotal 479 0 CrsIsSeries 480 0 CrsLookup 481 0 0f 482 0 1f 483 0 ToSingleton 484 0 FromSameSingleton 485 0 SingletonmembersEqual 486 0 UnequalsNotInSingleton 487 0 NonsingletonmembersUnequal 488 0 FromOrderedPair 489 0 FromOrderedPair(1) 490 0 FromOrderedPair(2) 491 0 FromCartProd 492 0 FromCartProd(1) 493 0 FromCartProd(2) 494 0 sameOrderedPair 495 0 InSeriesHelper 496 0 InSeries 497 0 To = f(Subset)(Helper) 498 0 To = f(Subset) 499 0 To = f 500 0 productIsFunction 501 0 productIsTotal 502 0 ProductIsRationalSeries 503 0 TimesF 504 0 −x + (1/2)x = −(1/2)x 505 0 PositiveTripled 506 0 PositiveDividedBy3 507 0 |x − x| = 0 508 0 1 < 2 509 0 1/3 < 2/3 510 0 (1/3)x + (1/3)x = (2/3)x 511 0 (2/3)x + (1/3)x = x 512 0 −x + (2/3)x = −(1/3)x 513 0 −(1/3)x − (1/3)x = −(2/3)x 514 0 −x + (1/3)x = −(2/3)x 515 0 PreserveLessGreater 516 0 ClosetolessIsLess 517 0 SubLessLeft(F) 518 0 SubLessLeft(R) 519 0 ClosetogreaterIsGreater 520 0 SubLessRight(F) 521 0 SubLessRight(R) 522 0 Tester1 523 0 Tester2 524 0 Tester3 525 0 Tester4 526 0 Tester5 527 0 Tester6

The pyk compiler, version 0.grue.20060417+ by Klaus Grue GRD-2006-12-08.UTC:16:16:16.345569 = MJD-54077.TAI:16:16:49.345569 = LGT-4672311409345569e-6