Logiweb dictionary of sup2

Up Help

0 0 sup2 1 0 LeqTotality(R) 2 0 PositiveToLeft(Eq) 3 0 ExpZero(Exact) 4 0 SameExp(Base) 5 0 SameExp(Indu) 6 0 SameExp 7 0 (1/2)(x + y) − x = (1/2)(y − x) 8 0 y − (1/2)(x + y) = (1/2)(y − x) 9 0 BSzero(Exact) 10 0 SameBS(2)(Base) 11 0 SameBS(2)(Indu) 12 0 SameBS(2) 13 0 NegativeToLeft(Less)(1term) 14 0 BS(+1) 15 0 BSbound(Exact)(Base) 16 0 BSbound(Exact)(Indu) 17 0 BSbound(Exact) 18 0 BSbound 19 0 UStelescope(Zero)(Exact) 20 0 SameTelescope(2)(Base) 21 0 SameTelescope(2)(Indu) 22 0 SameTelescope(2) 23 0 Exp(+1) 24 0 PositiveBase(Base) 25 0 PositiveBase(Indu) 26 0 PositiveBase 27 0 TelescopeNumerical(Base) 28 0 TelescopeNumerical(Indu)

29 0 TelescopeNumerical 30 0 (+1)IsPositive(N) 31 0 DistributionOut(Minus) 32 0 PositiveToRight(Eq)(1term) 33 0 SameSeries(NumDiff) 34 0 ToNegatedDoubleImply 35 0 AddNegatedAll 36 0 (A)to( E )(Imply) 37 0 (E)to( A )(Imply) 38 0 (E )to( A)(Imply) 39 0 ToNegatedAEA 40 0 Three2threeTerms(R) 41 0 LessNeq(F)(Helper) 42 0 LessNeq(F) 43 0 LessNeq(R) 44 0 x = x + (y − y)(R) 45 0 x = x + y − y(R) 46 0 SubtractEquations(R) 47 0 NeqAddition(R) 48 0 PositiveToRight(Less)(R) 49 0 PositiveToRight(Less)(1term)(R) 50 0 LeqNeqLess(R) 51 0 SubLeqLeft(R) 52 0 ToLeq(Advanced)(R) 53 0 LeqLessTransitivity(R) 54 0 NegativeToLeft(Eq)(R) 55 0 NegativeToRight(Less)(R) 56 0 !! == Symmetry 57 0 SwitchTerms(x <= y − z) 58 0 Plus0Left(R) 59 0 PositiveToRight(Eq)(R) 60 0 EqAdditionLeft(R) 61 0 Three2twoTerms(R) 62 0 To!! == 63 0 PositiveToRight(Less)(1term) 64 0 (A )to( E) 65 0 NegativeToRight(Eq)(R) 66 0 NegativeToRight(Eq)(1term)(R) 67 0 DoubleMinus(R) 68 0 UniqueNegative(R) 69 0 SubtractEquationsLeft(R) 70 0 EqNegated(R) 71 0 NeqNegated(R) 72 0 −0 = 0(R) 73 0 NegativeNegated(R) 74 0 FromLeqGeq(R) 75 0 0 <= |x|(R) 76 0 PositiveNegated(R) 77 0 AddEquations(R) 78 0 Times(−1)(R) 79 0 Times(−1)Left(R) 80 0 −x − y = −(x + y)(R) 81 0 LessTotality(R) 82 0 SameNumerical(R) 83 0 MinusNegated(R) 84 0 PositiveNumerical(R) 85 0 SignNumerical(+)(R) 86 0 NonnegativeNumerical(R) 87 0 NegativeNumerical(R) 88 0 LeqNegated(R) 89 0 LessNegated(R) 90 0 SubLeqRight(R) 91 0 FromLess(R) 92 0 DistributionOut(R) 93 0 x ∗ 0 + x = x(R) 94 0 x ∗ 0 = 0(R)(fff) 95 0 SignNumerical(R) 96 0 NumericalDifference(R)

97 0 x <= |x|(R) 98 0 USlimitIsUpperBound(Helper) 99 0 USlimitIsUpperBound 100 0 (−1) ∗ (−1) + (−1) ∗ 1 = 0(R) 101 0 (−1) ∗ (−1) = 1(R) 102 0 0 < 1Helper(R) 103 0 0 < 1(R) 104 0 ExpZero(Exact)(R) 105 0 PositiveBase(R)(Base) 106 0 Three2twoFactors(R) 107 0 x = x ∗ y ∗ (1/y)(R) 108 0 NeqMultiplication(R) 109 0 LessTransitivity(R) 110 0 0 < 2(R) 111 0 SameExp(R)(Base) 112 0 SameExp(R)(Indu) 113 0 SameExp(R) 114 0 SubNeqLeft(R) 115 0 SubNeqRight(R) 116 0 NonzeroFactors(R) 117 0 NonnegativeFactors(R) 118 0 PositiveFactors(R) 119 0 LessDivision(R) 120 0 0 < 1/2(R) 121 0 PositiveToRight(Eq)(1term)(R) 122 0 Exp(+1)(R) 123 0 PositiveBase(R)(Indu) 124 0 PositiveBase(R) 125 0 −x ∗ y = −(x ∗ y)(R) 126 0 PositiveToLeft(Eq)(R) 127 0 Times1Left(R) 128 0 x + x = 2 ∗ x(R) 129 0 (1/2)x + (1/2)x = x(R) 130 0 DistributionOut(Minus)(R)

131 0 (1/2)(x + y) − x = (1/2)(y − x)(R) 132 0 IntervalSize(R)(Base) 133 0 LessMultiplicationLeft(R) 134 0 NegativeToLeft(Less)(R) 135 0 NegativeToLeft(Less)(1term)(R) 136 0 y − (1/2)(x + y) = (1/2)(y − x)(R) 137 0 IntervalSize(R)(Indu) 138 0 IntervalSize(R) 139 0 XSlessUS(R) 140 0 USdecreasing(+1)(R) 141 0 ExpUnbounded(Base) 142 0 ExpUnbounded(Indu) 143 0 ExpUnbounded 144 0 1 <= x + 1(N) 145 0 ExpNonzero(Base) 146 0 ExpNonzero(Indu) 147 0 ExpNonzero 148 0 ExpNonzero(2) 149 0 HalfBase(Base) 150 0 HalfBase(Indu) 151 0 MultiplyEquations(R) 152 0 NonreciprocalToRight(Eq)(1term)(R) 153 0 PositiveNonzero(R) 154 0 NonzeroProduct(2)(R) 155 0 HalfBase 156 0 Three2threeFactors(R) 157 0 x ∗ y = zBackwards(R) 158 0 PositiveInverted(R) 159 0 ReciprocalToRight(Less)(R) 160 0 ReciprocalToRight(Less)(1term)(R) 161 0 NonreciprocalToLeft(Less)(R) 162 0 1 < x ∗ y(R) 163 0 SwitchFactors(1/x < y)(R) 164 0 SmallHalving 165 0 IntervalSize(anyPositive) 166 0 USdecreasing(+n)(Base) 167 0 USdecreasing(+n)(Indu) 168 0 USdecreasing(+n) 169 0 USdecreasing 170 0 LeqAdditionLeft(R) 171 0 ToNotLess(R) 172 0 LimitOfUSIsLeq 173 0 SubtractEquations(Less)(R) 174 0 SubtractEquationsLeft(Less)(R) 175 0 LessNegated(Negative)(R) 176 0 FromNegatedAnd(Imply) 177 0 RemoveDoubleNeg(Consequent) 178 0 FromNotUpperBound 179 0 LeqNUB 180 0 USlimitIsLeastUpperBound(Helper) 181 0 USlimitIsLeastUpperBound 182 0 ExistMP3 183 0 GreaterPositive(N) 184 0 ysFClose(Helper) 185 0 ysFClose 186 0 ysFCauchy(Helper) 187 0 ysFCauchy 188 0 from <<== 189 0 to <<== 190 0 NonnegativeNumerical(F) 191 0 NegativeNumerical(F)

192 0 tester1
193 0 tester2
194 0 tester3
195 0 tester4
196 0 tester5
197 0 tester6

The pyk compiler, version 0.grue.20060417+ by Klaus Grue GRD-2006-12-29.UTC:10:12:14.905583 = MJD-54098.TAI:10:12:47.905583 = LGT-4674103967905583e-6