Logiweb dictionary of sup

Up Help

0 0 sup 1 0 ToNegatedAnd(1) 2 0 UniqueNegative 3 0 DoubleMinus 4 0 MinusNegated 5 0 eqReflexivity 6 0 eqSymmetry 7 0 eqTransitivity 8 0 eqTransitivity4 9 0 eqTransitivity5 10 0 eqTransitivity6 11 0 AddEquations 12 0 SubtractEquations 13 0 SubtractEquationsLeft 14 0 MultiplyEquations 15 0 EqNegated 16 0 PositiveToRight(Eq) 17 0 PositiveToLeft(Eq)(1term) 18 0 NegativeToLeft(Eq) 19 0 NonreciprocalToRight(Eq)(1term) 20 0 PlusAssociativity(4terms) 21 0 LessNeq 22 0 NeqSymmetry 23 0 NeqNegated 24 0 SubNeqRight 25 0 SubNeqLeft 26 0 NegativeToRight(Neq)(1term) 27 0 NeqAddition 28 0 NeqMultiplication 29 0 NonzeroProduct(2) 30 0 UStelescope(+1) 31 0 TelescopeBound(Base) 32 0 TelescopeBound(Indu) 33 0 TelescopeBound 34 0 IntervalSize(Base) 35 0 IntervalSize(Indu) 36 0 IntervalSize 37 0 XS < US

38 0 lemma USdecreasing(+1)

39 0 CloseUS 40 0 CloseUS(n + 1) 41 0 AllNegated(Imply) 42 0 ExistNegated(Imply) 43 0 IntroExist(Helper) 44 0 IntroExist 45 0 ExistMP 46 0 ExistMP2 47 0 TwiceExistMP 48 0 TwiceExistMP2 49 0 EAE − MP 50 0 AddAll 51 0 AddExist(Helper1) 52 0 AddExist(Helper2) 53 0 AddExist 54 0 AddExist(SimpleAnt) 55 0 AddExist(Simple) 56 0 AddEAE 57 0 AEA − negated 58 0 EEA − negated 59 0 Induction 60 0 leqAntisymmetry 61 0 leqTransitivity 62 0 leqAddition 63 0 leqMultiplication 64 0 Reciprocal 65 0 Equality 66 0 eqLeq 67 0 eqAddition 68 0 eqMultiplication 69 0 LeqMultiplicationLeft 70 0 LeqLessEq 71 0 LessLeq 72 0 FromLeqGeq 73 0 subLeqRight 74 0 subLeqLeft 75 0 Leq + 1 76 0 PositiveToRight(Leq) 77 0 PositiveToRight(Leq)(1term)

78 0 lemma negativeToRight(Leq)

79 0 PositiveToLeft(Leq) 80 0 negativeToLeft(Leq) 81 0 negativeToLeft(Leq)(1term) 82 0 LeqAdditionLeft 83 0 leqSubtraction 84 0 leqSubtractionLeft 85 0 thirdGeq 86 0 LeqNegated 87 0 AddEquations(Leq) 88 0 MultiplyEquations(Leq) 89 0 ThirdGeqSeries 90 0 LeqNeqLess 91 0 FromLess 92 0 ToLess 93 0 fromNotLess 94 0 toNotLess 95 0 NegativeLessPositive 96 0 leqLessTransitivity 97 0 LessLeqTransitivity 98 0 LessTransitivity 99 0 LessTotality 100 0 SubLessRight 101 0 SubLessLeft 102 0 SwitchTerms(x < y − z) 103 0 SwitchTerms(x − y < z) 104 0 LessAddition 105 0 LessAdditionLeft 106 0 LessMultiplication 107 0 LessMultiplicationLeft 108 0 LessDivision 109 0 PositiveToRight(Less) 110 0 PositiveToLeft(Less) 111 0 NegativeToLeft(Less) 112 0 NegativeToRight(Less) 113 0 AddEquations(Less) 114 0 AddEquations(LeqLess) 115 0 reciprocalToLeft(Less) 116 0 LessNegated 117 0 PositiveNonzero 118 0 PositiveNegated 119 0 NonpositiveNegated 120 0 NegativeNegated 121 0 NonnegativeNegated 122 0 PositiveHalved 123 0 PositiveInverted 124 0 NonnegativeNumerical 125 0 NegativeNumerical 126 0 PositiveNumerical

127 0 lemma nonpositiveNumerical

128 0 |0| = 0 129 0 0 <= |x| 130 0 x <= |x| 131 0 FromPositiveNumerical 132 0 SameNumerical 133 0 SignNumerical(+) 134 0 SignNumerical 135 0 ToNumericalLess 136 0 FromNumericalGreater 137 0 NumericalDifference 138 0 NumericalDifferenceLess(Helper) 139 0 NumericalDifferenceLess 140 0 SplitNumericalSumHelper 141 0 splitNumericalSum(++) 142 0 splitNumericalSum(−−) 143 0 splitNumericalSum(+ − small) 144 0 splitNumericalSum(+ − big) 145 0 splitNumericalSum(+−) 146 0 splitNumericalSum(−+) 147 0 splitNumericalSum 148 0 SplitNumericalProduct(++) 149 0 SplitNumericalProduct(+−) 150 0 SplitNumericalProduct 151 0 insertMiddleTerm(Numerical) 152 0 insertTwoMiddleTerms(Numerical) 153 0 Three2twoTerms 154 0 Three2threeTerms 155 0 Three2twoFactors 156 0 Three2threeFactors 157 0 Times(−1) 158 0 Times(−1)Left 159 0 MaxLeq(1) 160 0 MaxLeq(2) 161 0 LessThanMax 162 0 x + y = zBackwards 163 0 x ∗ y = zBackwards 164 0 x = x + (y − y)

165 0 x = x + y − y 166 0 x = x ∗ y ∗ (1/y) 167 0 insertMiddleTerm(Sum) 168 0 insertTwoMiddleTerms(Sum) 169 0 insertMiddleTerm(Difference) 170 0 x ∗ 0 + x = x 171 0 x ∗ 0 = 0 172 0 NonnegativeFactors 173 0 NonzeroFactors 174 0 PositiveFactors 175 0 PlusTimesMinus 176 0 MinusTimesMinus 177 0 (−1) ∗ (−1) + (−1) ∗ 1 = 0 178 0 (−1) ∗ (−1) = 1 179 0 0 < 1Helper 180 0 0 < 1 181 0 0 < 2 182 0 0 < 3 183 0 0 < 1/2 184 0 0 < 1/3 185 0 TwoWholes 186 0 ThreeWholes 187 0 TwoHalves 188 0 ThreeThirds 189 0 −x − y = −(x + y) 190 0 −x ∗ y = −(x ∗ y) 191 0 −0 = 0 192 0 SFsymmetry 193 0 SFtransitivity 194 0 f2R(Plus) 195 0 f2R(Times) 196 0 << TransitivityHelper(Q) 197 0 << Transitivity 198 0 <<== Reflexivity 199 0 <<== AntisymmetryHelper(Q) 200 0 FromNot < f(Weak)(Helper) 201 0 FromNot < f(Weak) 202 0 FromNot < f(Strong)(Helper2) 203 0 FromNot < f(Strong)(Helper) 204 0 FromNot < f(Strong) 205 0 fromNotSameF(Strongest)(Helper2) 206 0 fromNotSameF(Strongest)(Helper) 207 0 fromNotSameF(Strongest) 208 0 ToLess(F)(Helper) 209 0 ToLess(F) 210 0 FromNot << 211 0 ToLess(R) 212 0 FromNotSameF(Weak)(Helper) 213 0 FromNotSameF(Weak) 214 0 FromNotLess(F) 215 0 == Addition 216 0 == AdditionLeft 217 0 Fpart − Bounded(Base) 218 0 Fpart − Bounded(InduHelper) 219 0 Fpart − Bounded(Indu) 220 0 Fpart − Bounded 221 0 F − Bounded(Helper) 222 0 F − Bounded 223 0 SameFmultiplication(Helper) 224 0 SameFmultiplication 225 0 EqMultiplication(R) 226 0 EqMultiplicationLeft(R) 227 0 x ∗ 0 = 0(F) 228 0 x ∗ 0 = 0(R) 229 0 LessMultiplication(F)(Helper2) 230 0 LessMultiplication(F)(Helper) 231 0 LessMultiplication(F) 232 0 LessMultiplication(R)

233 0 LeqMultiplication(R) 234 0 PlusAssociativity(F) 235 0 Plus0(F) 236 0 PlusCommutativity(F) 237 0 TimesAssociativity(F) 238 0 Times1f 239 0 Cauchy(2)(Helper) 240 0 Cauchy(2) 241 0 ReciprocalFnonzero 242 0 (Eventually = f)2sameF(Helper) 243 0 (Eventually = f)2sameF 244 0 FromNotSameF(Strong)(Helper2) 245 0 FromNotSameF(Strong)(Helper) 246 0 FromNotSameF(Strong) 247 0 SameFreciprocal(Helper) 248 0 SameFreciprocal 249 0 From!! == 250 0 Reciprocal(R) 251 0 TimesCommutativity(F) 252 0 Distribution(F) 253 0 FromMax(1) 254 0 FromMax(2) 255 0 ToNegatedAnd 256 0 DistributionOut 257 0 DistributionOutLeft 258 0 DistributionLeft 259 0 FromNotLess(R) 260 0 CartProdIsRelation 261 0 FromSubset 262 0 SubsetIsRelation 263 0 ToSeries 264 0 FromSeries 265 0 SeriesSubsetCP 266 0 ValueType 267 0 RemoveOr 268 0 FromSingleton 269 0 InPair(1) 270 0 InPair(2) 271 0 SameMember(2) 272 0 ToBinaryUnion(1) 273 0 ToBinaryUnion(2) 274 0 FromOrderedPair(TwoLevels) 275 0 ToCartProd(Helper) 276 0 ToCartProd 277 0 NonreciprocalToRight(Eq) 278 0 NonreciprocalToLeft(Eq)(1term) 279 0 SameReciprocal 280 0 CPseparationIsRelation 281 0 OrderedPairEquality 282 0 ReciprocalIsFunction 283 0 ReciprocalIsTotal 284 0 ReciprocalIsRationalSeries 285 0 CrsIsRelation 286 0 CrsIsFunction 287 0 CrsIsTotal 288 0 CrsIsSeries 289 0 CrsLookup 290 0 0f 291 0 1f 292 0 ToSingleton 293 0 FromSameSingleton 294 0 SingletonmembersEqual 295 0 UnequalsNotInSingleton 296 0 NonsingletonmembersUnequal 297 0 FromOrderedPair 298 0 FromOrderedPair(1) 299 0 FromOrderedPair(2) 300 0 FromCartProd 301 0 FromCartProd(1) 302 0 FromCartProd(2) 303 0 sameOrderedPair 304 0 InSeriesHelper 305 0 InSeries 306 0 To = f(Subset)(Helper) 307 0 To = f(Subset) 308 0 To = f 309 0 productIsFunction 310 0 productIsTotal 311 0 ProductIsRationalSeries 312 0 TimesF 313 0 −x + (1/2)x = −(1/2)x 314 0 PositiveTripled 315 0 PositiveDividedBy3 316 0 |x − x| = 0 317 0 1 < 2 318 0 1/3 < 2/3 319 0 (1/3)x + (1/3)x = (2/3)x 320 0 (2/3)x + (1/3)x = x 321 0 −x + (2/3)x = −(1/3)x 322 0 −(1/3)x − (1/3)x = −(2/3)x 323 0 −x + (1/3)x = −(2/3)x 324 0 PreserveLessGreater 325 0 ClosetolessIsLess 326 0 SubLessLeft(F) 327 0 SubLessLeft(R) 328 0 ClosetogreaterIsGreater 329 0 SubLessRight(F) 330 0 SubLessRight(R) 331 0 plus0Left 332 0 times1Left 333 0 EqAdditionLeft 334 0 EqMultiplicationLeft 335 0 PlusF(Sym) 336 0 TimesF(Sym) 337 0 SameSeries(Gen) 338 0 EqualsSameF 339 0 LeqReflexivity(R) 340 0 Tester1 341 0 Tester2 342 0 Tester3 343 0 Tester4 344 0 Tester5 345 0 Tester6

The pyk compiler, version 0.grue.20060417+ by Klaus Grue GRD-2006-12-29.UTC:09:42:35.018035 = MJD-54098.TAI:09:43:08.018035 = LGT-4674102188018035e-6