Logiweb dictionary of am

Up Help

0 0 am 1 0 (⋯)

 2 0 Objekt-var
 3 0 Ex-var
 4 0 Ph-var
 5 0 Værdi
 6 0 Variabel

7 1 Op(∗) 8 2 Op(∗, ∗) 9 2 ∗ ¨ == ∗ 10 1 ContainsEmpty(∗) 11 2 Dedu(∗, ∗) 12 2 Dedu_{0}(∗, ∗) 13 3 Dedu_{s}(∗, ∗, ∗) 14 3 Dedu_{1}(∗, ∗, ∗) 15 3 Dedu_{2}(∗, ∗, ∗) 16 4 Dedu_{3}(∗, ∗, ∗, ∗) 17 4 Dedu_{4}(∗, ∗, ∗, ∗) 18 4 Dedu_{4}^{∗}(∗, ∗, ∗, ∗) 19 3 Dedu_{5}(∗, ∗, ∗) 20 4 Dedu_{6}(∗, ∗, ∗, ∗) 21 4 Dedu_{6}^{∗}(∗, ∗, ∗, ∗) 22 1 Dedu_{7}(∗) 23 2 Dedu_{8}(∗, ∗) 24 2 Dedu_{8}^{∗}(∗, ∗) 25 0 Ex_{1} 26 0 Ex_{2} 27 0 Ex3 28 0 Ex_{10} 29 0 Ex_{20} 30 1 ∗_{Ex} 31 1 ∗^{Ex} 32 4 ⟨∗≡ ∗ | ∗:==∗⟩_{Ex} 33 4 ⟨∗≡^{0} ∗ | ∗:==∗⟩_{Ex} 34 4 ⟨∗≡^{1} ∗ | ∗:==∗⟩_{Ex} 35 4 ⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Ex} 36 0 ph_{1} 37 0 ph_{2} 38 0 ph_{3} 39 1 ∗_{Ph} 40 1 ∗^{Ph} 41 4 ⟨∗≡ ∗ | ∗:==∗⟩_{Ph} 42 4 ⟨∗≡^{0} ∗ | ∗:==∗⟩_{Ph} 43 4 ⟨∗≡^{1} ∗ | ∗:==∗⟩_{Ph} 44 4 ⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Ph}

45 0 bs
46 0 OBS
47 0 BS

48 0 Ø 49 0 ZFsub 50 0 MP 51 0 Gen 52 0 Repetition 53 0 Neg 54 0 Ded 55 0 ExistIntro 56 0 Extensionality 57 0 Ødef 58 0 PairDef 59 0 UnionDef 60 0 PowerDef 61 0 SeparationDef 62 0 AddDoubleNeg 63 0 RemoveDoubleNeg 64 0 AndCommutativity 65 0 AutoImply 66 0 Contrapositive 67 0 FirstConjunct 68 0 SecondConjunct 69 0 FromContradiction 70 0 FromDisjuncts 71 0 IffCommutativity 72 0 IffFirst 73 0 IffSecond 74 0 ImplyTransitivity 75 0 JoinConjuncts 76 0 MP2 77 0 MP3 78 0 MP4 79 0 MP5 80 0 MT 81 0 NegativeMT 82 0 Technicality 83 0 Weakening 84 0 WeakenOr1 85 0 WeakenOr2 86 0 Formula2Pair 87 0 Pair2Formula 88 0 Formula2Union 89 0 Union2Formula 90 0 Formula2Sep 91 0 Sep2Formula 92 0 SubsetInPower 93 0 HelperPowerIsSub 94 0 PowerIsSub 95 0 (Switch)HelperPowerIsSub 96 0 (Switch)PowerIsSub 97 0 ToSetEquality 98 0 HelperToSetEquality(t) 99 0 ToSetEquality(t) 100 0 HelperFromSetEquality 101 0 FromSetEquality 102 0 HelperReflexivity 103 0 Reflexivity 104 0 HelperSymmetry 105 0 Symmetry 106 0 HelperTransitivity 107 0 Transitivity 108 0 ERisReflexive 109 0 ERisSymmetric 110 0 ERisTransitive 111 0 ØisSubset 112 0 HelperMemberNotØ 113 0 MemberNotØ 114 0 HelperUniqueØ 115 0 UniqueØ 116 0 ==Reflexivity 117 0 ==Symmetry 118 0 Helper==Transitivity 119 0 ==Transitivity 120 0 HelperTransferNotEq 121 0 TransferNotEq 122 0 HelperPairSubset 123 0 Helper(2)PairSubset 124 0 PairSubset 125 0 SamePair 126 0 SameSingleton 127 0 UnionSubset 128 0 SameUnion 129 0 SeparationSubset 130 0 SameSeparation 131 0 SameBinaryUnion 132 0 IntersectionSubset 133 0 SameIntersection 134 0 AutoMember 135 0 HelperEqSysNotØ 136 0 EqSysNotØ 137 0 HelperEqSubset 138 0 EqSubset 139 0 HelperEqNecessary 140 0 EqNecessary 141 0 HelperNoneEqNecessary 142 0 Helper(2)NoneEqNecessary 143 0 NoneEqNecessary 144 0 EqClassIsSubset 145 0 EqClassesAreDisjoint 146 0 AllDisjoint 147 0 AllDisjointImply 148 0 BSsubset 149 0 Union(BS/R)subset 150 0 UnionIdentity 151 0 EqSysIsPartition 152 0 (ϵ) 153 0 (fx) 154 0 (fy) 155 0 (fz) 156 0 (fv)

157 0 var fv

158 0 (rx) 159 0 (ry) 160 0 (rz) 161 0 (ru) 162 0 ϵ 163 0 FX 164 0 FY 165 0 FZ 166 0 FU 167 0 FV 168 0 RX 169 0 RY 170 0 RZ 171 0 RU 172 0 0 173 0 1 174 0 (−1) 175 0 2 176 0 1/2 177 0 0f

178 0 1f

179 0 00

180 0 01

181 0 leqReflexivity 182 0 leqAntisymmetryAxiom 183 0 leqTransitivityAxiom 184 0 leqTotality 185 0 leqAdditionAxiom 186 0 leqMultiplicationAxiom 187 0 plusAssociativity 188 0 plusCommutativity 189 0 Negative 190 0 plus0 191 0 timesAssociativity 192 0 timesCommutativity 193 0 ReciprocalAxiom 194 0 times1 195 0 Distribution 196 0 0not1 197 0 equalityAxiom 198 0 eqLeqAxiom 199 0 eqAdditionAxiom 200 0 eqMultiplicationAxiom 201 0 SENC1 202 0 SENC2 203 0 IfThenElse(T) 204 0 IfThenElse(F) 205 0 From = f 206 0 To = f 207 0 From < f 208 0 To < f 209 0 PlusF 210 0 TimesF 211 0 MinusF 212 0 0f 213 0 1f 214 0 FromSF 215 0 ToSF 216 0 To == XX 217 0 From == 218 0 To == 219 0 From << XX 220 0 From << (1) 221 0 From << (2) 222 0 to << XX 223 0 From << 224 0 To << 225 0 FromInR 226 0 PlusR 227 0 TimesR 228 0 leqAntisymmetry 229 0 leqTransitivity 230 0 leqAddition 231 0 leqMultiplication 232 0 Reciprocal 233 0 Equality 234 0 eqLeq 235 0 eqAddition 236 0 eqMultiplication 237 0 ToNegatedImply 238 0 TND 239 0 ImplyNegation 240 0 FromNegations 241 0 From3Disjuncts 242 0 From2 ∗ 2Disjuncts 243 0 NegateDisjunct1 244 0 NegateDisjunct2 245 0 ExpandDisjuncts 246 0 eqReflexivity 247 0 eqSymmetry 248 0 eqTransitivity 249 0 eqTransitivity4 250 0 eqTransitivity5 251 0 eqTransitivity6 252 0 plus0Left 253 0 times1Left

254 0 lemma eqAdditionLeft

255 0 EqMultiplicationLeft 256 0 DistributionOut 257 0 Three2twoTerms 258 0 Three2threeTerms 259 0 Three2threeFactors 260 0 AddEquations 261 0 SubtractEquations 262 0 SubtractEquationsLeft 263 0 EqNegated 264 0 PositiveToRight(Eq) 265 0 PositiveToLeft(Eq)(1term) 266 0 NegativeToLeft(Eq)

267 0 LessNeq 268 0 NeqSymmetry 269 0 NeqNegated 270 0 SubNeqRight 271 0 SubNeqLeft 272 0 NeqAddition 273 0 NeqMultiplication 274 0 UniqueNegative 275 0 DoubleMinus 276 0 LeqLessEq 277 0 LessLeq 278 0 FromLeqGeq 279 0 subLeqRight 280 0 subLeqLeft 281 0 Leq + 1 282 0 PositiveToRight(Leq) 283 0 PositiveToRight(Leq)(1term) 284 0 negativeToLeft(Leq) 285 0 LeqAdditionLeft 286 0 leqSubtraction 287 0 leqSubtractionLeft 288 0 thirdGeq 289 0 LeqNegated 290 0 AddEquations(Leq) 291 0 ThirdGeqSeries 292 0 LeqNeqLess 293 0 FromLess 294 0 ToLess 295 0 fromNotLess 296 0 toNotLess 297 0 NegativeLessPositive 298 0 leqLessTransitivity 299 0 LessLeqTransitivity 300 0 LessTransitivity 301 0 LessTotality 302 0 SubLessRight 303 0 SubLessLeft 304 0 LessAddition 305 0 LessAdditionLeft 306 0 LessMultiplication 307 0 LessMultiplicationLeft 308 0 LessDivision 309 0 AddEquations(Less) 310 0 LessNegated 311 0 PositiveNegated 312 0 NonpositiveNegated 313 0 NegativeNegated 314 0 NonnegativeNegated 315 0 PositiveHalved 316 0 NonnegativeNumerical 317 0 NegativeNumerical 318 0 PositiveNumerical

319 0 lemma nonpositiveNumerical

320 0 |0| = 0 321 0 0 <= |x| 322 0 SameNumerical 323 0 SignNumerical(+) 324 0 SignNumerical 325 0 NumericalDifference 326 0 SplitNumericalSumHelper 327 0 splitNumericalSum(++) 328 0 splitNumericalSum(−−) 329 0 splitNumericalSum(+ − small) 330 0 splitNumericalSum(+ − big) 331 0 splitNumericalSum(+−) 332 0 splitNumericalSum(−+) 333 0 splitNumericalSum 334 0 insertMiddleTerm(Numerical)

335 0 x + y = zBackwards 336 0 x ∗ y = zBackwards 337 0 x = x + (y − y) 338 0 x = x + y − y

339 0

340 0 insertMiddleTerm(Sum) 341 0 insertMiddleTerm(Difference) 342 0 x ∗ 0 + x = x 343 0 x ∗ 0 = 0 344 0 (−1) ∗ (−1) + (−1) ∗ 1 = 0 345 0 (−1) ∗ (−1) = 1 346 0 0 < 1Helper 347 0 0 < 1 348 0 0 < 2 349 0 0 < 1/2 350 0 TwoWholes 351 0 TwoHalves 352 0 −x − y = −(x + y) 353 0 MinusNegated 354 0 Times(−1) 355 0 Times(−1)Left 356 0 −0 = 0 357 0 SFsymmetry 358 0 SFtransitivity 359 0 = fToSameF 360 0 PlusF(Sym) 361 0 TimesF(Sym) 362 0 f2R(Plus) 363 0 f2R(Times) 364 0 PlusR(Sym) 365 0 TimesR(Sym) 366 0 LessLeq(R) 367 0 eqLeq(R) 368 0 SubLessRight(R)

369 0 SubLessLeft(R) 370 0 << TransitivityHelper(Q) 371 0 << Transitivity 372 0 <<== Reflexivity 373 0 <<== AntisymmetryHelper(Q) 374 0 <<== Antisymmetry 375 0 <<== Transitivity 376 0 Plus0f 377 0 Plus00 378 0 == Addition 379 0 == AdditionLeft 380 0 << Addition 381 0 <<== Addition 382 0 PlusAssociativity(F) 383 0 PlusAssociativity(R) 384 0 Negative(R) 385 0 PlusCommutativity(F) 386 0 PlusCommutativity(R) 387 0 TimesAssociativity(F) 388 0 TimesAssociativity(R) 389 0 Times1f 390 0 Times01 391 0 TimesCommutativity(F) 392 0 TimesCommutativity(R) 393 0 Distribution(F) 394 0 Distribution(R) 395 1 R(∗) 396 1 − − R(∗) 397 1 rec∗ 398 2 ∗/∗ 399 2 ∗ ∩ ∗ 400 2 ∗[∗] 401 1 ∪∗ 402 2 ∗ ∪ ∗ 403 1 P(∗) 404 1 {∗} 405 2 {∗, ∗} 406 2 ⟨∗, ∗⟩ 407 1 −∗ 408 1 −_{f}∗ 409 2 ∗ ∈ ∗ 410 3 ∗(∗, ∗) 411 2 ReflRel(∗, ∗) 412 2 SymRel(∗, ∗) 413 2 TransRel(∗, ∗) 414 2 EqRel(∗, ∗) 415 3 [∗ ∈ ∗]_{∗} 416 2 Partition(∗, ∗) 417 2 ∗ ∗ ∗ 418 2 ∗ ∗_{f} ∗ 419 2 ∗ ∗ ∗∗ 420 2 ∗ + ∗ 421 2 ∗ − ∗ 422 2 ∗ +_{f} ∗ 423 2 ∗ −_{f} ∗ 424 2 ∗ + +∗ 425 2 R(∗) − −R(∗) 426 1 | ∗ | 427 3 if(∗, ∗, ∗) 428 2 ∗ = ∗ 429 2 ∗ ≠ ∗ 430 2 ∗ <= ∗ 431 2 ∗ < ∗ 432 2 ∗ =_{f} ∗ 433 2 ∗ <_{f} ∗ 434 2 SF(∗, ∗) 435 2 ∗ == ∗ 436 2 ∗ << ∗ 437 2 ∗ <<== ∗ 438 2 ∗==∗ 439 2 ∗ ⊆ ∗ 440 1 ˙¬ ∗ 441 2 ∗ ∉ ∗ 442 2 ∗ ≠ ∗ 443 2 ∗ ˙∧ ∗ 444 2 ∗ ˙∨ ∗ 445 2 ∗ ˙⇔ ∗ 446 2 {ph ∈ ∗ | ∗}

The pyk compiler, version 0.grue.20060417+ by Klaus Grue GRD-2006-09-15.UTC:09:33:20.992497 = MJD-53993.TAI:09:33:53.992497 = LGT-4665029633992497e-6