Logiweb dictionary of kvanti

Up Help

0 0 kvanti 1 0 UniqueMember 2 0 UniqueMember(Type) 3 0 SameSeries 4 0 A4 5 0 SameMember 6 0 Qclosed(Addition) 7 0 Qclosed(Multiplication) 8 0 FromCartProd(1)

9 0 1rule fromCartProd(2)

10 1 constantRationalSeries(∗) 11 2 cartProd(∗) 12 1 Power(∗) 13 2 binaryUnion(∗, ∗) 14 0 SetOfRationalSeries 15 2 IsSubset(∗, ∗) 16 2 (p∗, ∗) 17 1 (s∗) 18 0 (⋯)

19 0 Objekt-var
20 0 Ex-var
21 0 Ph-var
22 0 Værdi
23 0 Variabel

24 1 Op(∗) 25 2 Op(∗, ∗) 26 2 ∗ ¨ == ∗ 27 1 ContainsEmpty(∗) 28 1 Nat(∗)

29 2 Dedu(∗, ∗) 30 2 Dedu_{0}(∗, ∗) 31 3 Dedu_{s}(∗, ∗, ∗) 32 3 Dedu_{1}(∗, ∗, ∗) 33 3 Dedu_{2}(∗, ∗, ∗) 34 4 Dedu_{3}(∗, ∗, ∗, ∗) 35 4 Dedu_{4}(∗, ∗, ∗, ∗) 36 4 Dedu_{4}^{∗}(∗, ∗, ∗, ∗) 37 3 Dedu_{5}(∗, ∗, ∗) 38 4 Dedu_{6}(∗, ∗, ∗, ∗) 39 4 Dedu_{6}^{∗}(∗, ∗, ∗, ∗) 40 1 Dedu_{7}(∗) 41 2 Dedu_{8}(∗, ∗) 42 2 Dedu_{8}^{∗}(∗, ∗) 43 0 Ex_{1} 44 0 Ex_{2} 45 0 Ex3 46 0 Ex_{10} 47 0 Ex_{20} 48 1 ∗_{Ex} 49 1 ∗^{Ex} 50 4 ⟨∗≡ ∗ | ∗:==∗⟩_{Ex} 51 4 ⟨∗≡^{0} ∗ | ∗:==∗⟩_{Ex} 52 4 ⟨∗≡^{1} ∗ | ∗:==∗⟩_{Ex} 53 4 ⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Ex} 54 0 ph_{1} 55 0 ph_{2} 56 0 ph_{3} 57 1 ∗_{Ph} 58 1 ∗^{Ph} 59 4 ⟨∗≡ ∗ | ∗:==∗⟩_{Ph} 60 4 ⟨∗≡^{0} ∗ | ∗:==∗⟩_{Ph} 61 4 ⟨∗≡^{1} ∗ | ∗:==∗⟩_{Ph} 62 4 ⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Ph} 63 4 ⟨∗≡ ∗ | ∗:==∗⟩_{Me} 64 4 ⟨∗≡^{1} ∗ | ∗:==∗⟩_{Me} 65 4 ⟨∗≡^{∗} ∗ | ∗:==∗⟩_{Me}

66 0 bs
67 0 OBS
68 0 BS

69 0 Ø 70 0 SystemQ 71 0 MP 72 0 Gen 73 0 Repetition 74 0 Neg 75 0 Ded 76 0 ExistIntro 77 0 Extensionality 78 0 Ødef 79 0 PairDef 80 0 UnionDef 81 0 PowerDef 82 0 SeparationDef 83 0 AddDoubleNeg 84 0 RemoveDoubleNeg 85 0 AndCommutativity 86 0 AutoImply 87 0 Contrapositive 88 0 FirstConjunct 89 0 SecondConjunct 90 0 FromContradiction 91 0 FromDisjuncts 92 0 IffCommutativity 93 0 IffFirst 94 0 IffSecond 95 0 ImplyTransitivity 96 0 JoinConjuncts 97 0 MP2 98 0 MP3 99 0 MP4 100 0 MP5 101 0 MT 102 0 NegativeMT 103 0 Technicality 104 0 Weakening 105 0 WeakenOr1 106 0 WeakenOr2 107 0 Formula2Pair 108 0 Pair2Formula 109 0 Formula2Union 110 0 Union2Formula 111 0 Formula2Sep 112 0 Sep2Formula 113 0 Formula2Power 114 0 SubsetInPower 115 0 HelperPowerIsSub 116 0 PowerIsSub 117 0 (Switch)HelperPowerIsSub 118 0 (Switch)PowerIsSub 119 0 ToSetEquality 120 0 HelperToSetEquality(t) 121 0 ToSetEquality(t) 122 0 HelperFromSetEquality 123 0 FromSetEquality 124 0 HelperReflexivity 125 0 Reflexivity 126 0 HelperSymmetry 127 0 Symmetry 128 0 HelperTransitivity 129 0 Transitivity 130 0 ERisReflexive 131 0 ERisSymmetric 132 0 ERisTransitive 133 0 ØisSubset 134 0 HelperMemberNotØ 135 0 MemberNotØ 136 0 HelperUniqueØ 137 0 UniqueØ 138 0 ==Reflexivity 139 0 ==Symmetry 140 0 Helper==Transitivity 141 0 ==Transitivity 142 0 HelperTransferNotEq 143 0 TransferNotEq 144 0 HelperPairSubset 145 0 Helper(2)PairSubset 146 0 PairSubset 147 0 SamePair 148 0 SameSingleton 149 0 UnionSubset 150 0 SameUnion 151 0 SeparationSubset 152 0 SameSeparation 153 0 SameBinaryUnion 154 0 IntersectionSubset 155 0 SameIntersection 156 0 AutoMember 157 0 HelperEqSysNotØ 158 0 EqSysNotØ 159 0 HelperEqSubset 160 0 EqSubset 161 0 HelperEqNecessary 162 0 EqNecessary 163 0 HelperNoneEqNecessary 164 0 Helper(2)NoneEqNecessary 165 0 NoneEqNecessary 166 0 EqClassIsSubset 167 0 EqClassesAreDisjoint 168 0 AllDisjoint 169 0 AllDisjointImply 170 0 BSsubset 171 0 Union(BS/R)subset 172 0 UnionIdentity 173 0 EqSysIsPartition 174 0 (x1) 175 0 (x2) 176 0 (y1) 177 0 (y2) 178 0 (v1) 179 0 (v2) 180 0 (v3) 181 0 (v4) 182 0 (v2n) 183 0 (m1) 184 0 (m2) 185 0 (n1) 186 0 (n2) 187 0 (n3) 188 0 (ϵ) 189 0 (ϵ)_{1} 190 0 (ϵ2) 191 0 (fep) 192 0 (fx) 193 0 (fy) 194 0 (fz) 195 0 (fu) 196 0 (fv) 197 0 (fw) 198 0 (rx)

199 0 (ry) 200 0 (rz) 201 0 (ru) 202 0 (sx) 203 0 (sx1) 204 0 (sy) 205 0 (sy1) 206 0 (sz) 207 0 (sz1) 208 0 (su) 209 0 (su1) 210 0 (fxs) 211 0 (fys) 212 0 (crs1) 213 0 (f1) 214 0 (f2) 215 0 (f3) 216 0 (f4) 217 0 (op1) 218 0 (op2) 219 0 (r1) 220 0 (s1) 221 0 (s2) 222 0 X_{1} 223 0 X_{2} 224 0 Y_{1} 225 0 Y_{2} 226 0 V_{1} 227 0 V_{2} 228 0 V_{3} 229 0 V_{4} 230 0 V_{2n} 231 0 M_{1} 232 0 M_{2} 233 0 N_{1} 234 0 N_{2} 235 0 N_{3} 236 0 ϵ 237 0 ϵ1 238 0 ϵ2 239 0 FX 240 0 FY 241 0 FZ 242 0 FU 243 0 FV 244 0 FW 245 0 FEP 246 0 RX 247 0 RY 248 0 RZ 249 0 RU 250 0 (SX) 251 0 (SX1) 252 0 (SY) 253 0 (SY1) 254 0 (SZ) 255 0 (SZ1) 256 0 (SU) 257 0 (SU1) 258 0 FXS 259 0 FYS 260 0 (F1) 261 0 (F2) 262 0 (F3) 263 0 (F4) 264 0 (OP1) 265 0 (OP2) 266 0 (R1)

267 0 (S1) 268 0 (S2) 269 0 (EPob) 270 0 (CRS1ob) 271 0 (F1ob) 272 0 (F2ob) 273 0 (F3ob) 274 0 (F4ob) 275 0 (N1ob) 276 0 (N2ob) 277 0 (OP1ob) 278 0 (OP2ob) 279 0 (R1ob) 280 0 (S1ob) 281 0 (S2ob) 282 0 ph_{4} 283 0 ph_{5} 284 0 ph_{6} 285 0 NAT 286 0 RATIONAL_{S}ERIES 287 0 SERIES 288 0 SetOfReals 289 0 SetOfFxs 290 0 N 291 0 Q 292 0 X 293 0 xs 294 0 xaF 295 0 ysF 296 0 us 297 0 usFoelge 298 0 0 299 0 1 300 0 (−1)

301 0 2 302 0 3 303 0 1/2 304 0 1/3 305 0 2/3 306 0 0f

307 0 1f

308 0 00

309 0 01

310 0 (− − 01) 311 0 02 312 0 01//02 313 0 PlusAssociativity(R) 314 0 PlusAssociativity(R)XX 315 0 Plus0(R) 316 0 Negative(R) 317 0 Times1(R) 318 0 lessAddition(R) 319 0 PlusCommutativity(R) 320 0 LeqAntisymmetry(R) 321 0 LeqTransitivity(R) 322 0 leqAddition(R) 323 0 Distribution(R) 324 0 A4(Axiom) 325 0 InductionAxiom 326 0 EqualityAxiom 327 0 EqLeqAxiom 328 0 EqAdditionAxiom 329 0 EqMultiplicationAxiom 330 0 QisClosed(Reciprocal)(Imply) 331 0 QisClosed(Reciprocal) 332 0 QisClosed(Negative)(Imply) 333 0 QisClosed(Negative) 334 0 leqReflexivity 335 0 leqAntisymmetryAxiom 336 0 leqTransitivityAxiom 337 0 leqTotality 338 0 leqAdditionAxiom 339 0 leqMultiplicationAxiom 340 0 plusAssociativity 341 0 plusCommutativity 342 0 Negative 343 0 plus0 344 0 timesAssociativity 345 0 timesCommutativity 346 0 ReciprocalAxiom 347 0 times1 348 0 Distribution 349 0 0not1

350 0 lemma eqLeq(R)

351 0 TimesAssociativity(R) 352 0 TimesCommutativity(R) 353 0 (Adgic)SameR 354 0 Separation2formula(1) 355 0 Separation2formula(2) 356 0 Cauchy 357 0 PlusF 358 0 ReciprocalF 359 0 From == 360 0 To == 361 0 FromInR 362 0 PlusR(Sym) 363 0 ReciprocalR(Axiom) 364 0 LessMinus1(N) 365 0 Nonnegative(N) 366 0 US0 367 0 NextXS(UpperBound) 368 0 NextXS(NoUpperBound)

369 0 NextUS(UpperBound) 370 0 NextUS(NoUpperBound) 371 0 ExpZero 372 0 ExpPositive 373 0 ExpZero(R) 374 0 ExpPositive(R) 375 0 BSzero 376 0 BSpositive 377 0 UStelescope(Zero) 378 0 UStelescope(Positive) 379 0 EqAddition(R) 380 0 FromLimit 381 0 ToUpperBound 382 0 FromUpperBound 383 0 USisUpperBound 384 0 0not1(R) 385 0 ExpUnbounded(R) 386 0 FromLeq(Advanced)(N) 387 0 FromLeastUpperBound 388 0 ToLeastUpperBound 389 0 XSisNotUpperBound 390 0 ysFGreater 391 0 ysFLess 392 0 SmallInverse 393 0 NatType 394 0 RationalType 395 0 SeriesType 396 0 Max 397 0 Numerical 398 0 NumericalF 399 0 MemberOfSeries(Imply) 400 0 JoinConjuncts(2conditions)

401 0 prop lemma imply negation

402 0 TND 403 0 FromNegatedImply 404 0 ToNegatedImply 405 0 FromNegated(2 ∗ Imply) 406 0 FromNegatedAnd 407 0 FromNegatedOr 408 0 ToNegatedOr 409 0 FromNegations 410 0 From3Disjuncts 411 0 From2 ∗ 2Disjuncts 412 0 NegateDisjunct1 413 0 NegateDisjunct2 414 0 ExpandDisjuncts 415 0 SENC1 416 0 SENC2 417 0 LessLeq(R) 418 0 MemberOfSeries 419 0 memberOfSeries(Type) 420 2 ∗(exp)∗ 421 1 R(∗) 422 1 − − R(∗) 423 1 rec∗ 424 2 ∗/∗ 425 2 ∗ ∩ ∗ 426 2 ∗[∗] 427 1 ∪∗ 428 2 ∗ ∪ ∗ 429 1 P(∗) 430 1 {∗} 431 3 StateExpand(∗, ∗, ∗) 432 1 extractSeries(∗) 433 1 SetOfSeries(∗) 434 1 − − Macro(∗) 435 3 ExpandList(∗, ∗, ∗) 436 1 ∗ ∗ Macro(∗)

437 1 + + Macro(∗) 438 1 << Macro(∗) 439 1 ||Macro(∗) 440 1 01//Macro(∗) 441 2 UB(∗, ∗) 442 2 LUB(∗, ∗) 443 2 BS(∗, ∗) 444 2 UStelescope(∗, ∗) 445 1 (∗) 446 1 |f ∗ | 447 1 |r ∗ | 448 2 Limit(∗, ∗) 449 1 Union(∗) 450 3 IsOrderedPair(∗, ∗, ∗) 451 3 IsRelation(∗, ∗, ∗) 452 3 isFunction(∗, ∗, ∗) 453 2 IsSeries(∗, ∗) 454 1 IsNatural(∗, ∗) 455 2 OrderedPair(∗, ∗) 456 1 TypeNat(∗) 457 1 TypeNat0(∗) 458 1 TypeRational(∗) 459 1 TypeRational0(∗) 460 2 TypeSeries(∗, ∗) 461 2 Typeseries0(∗, ∗) 462 2 {∗, ∗} 463 2 ⟨∗, ∗⟩ 464 1 (−u∗) 465 1 −_{f}∗ 466 1 (− − ∗) 467 1 1f/∗ 468 1 01//temp∗ 469 3 ∗(∗, ∗) 470 2 ReflRel(∗, ∗)

471 2 SymRel(∗, ∗) 472 2 TransRel(∗, ∗) 473 2 EqRel(∗, ∗) 474 3 [∗ ∈ ∗]_{∗} 475 2 Partition(∗, ∗) 476 2 (∗ ∗ ∗) 477 2 ∗ ∗_{f} ∗ 478 2 ∗ ∗ ∗∗ 479 2 (∗ + ∗) 480 2 (∗ − ∗) 481 2 ∗ +_{f} ∗ 482 2 ∗ −_{f} ∗ 483 2 ∗ + +∗ 484 2 R(∗) − −R(∗) 485 2 ∗ ∈ ∗ 486 1 | ∗ | 487 3 if(∗, ∗, ∗) 488 2 Max(∗, ∗) 489 2 Max(∗, ∗) 490 2 ∗ = ∗ 491 2 ∗ ≠ ∗ 492 2 ∗ <= ∗ 493 2 ∗ < ∗ 494 2 ∗ <_{f} ∗ 495 2 ∗ ≤_{f} ∗ 496 2 SF(∗, ∗) 497 2 ∗ == ∗ 498 2 ∗!! == ∗ 499 2 ∗ << ∗ 500 2 ∗ <<== ∗ 501 2 ∗==∗ 502 2 ∗ ⊆ ∗ 503 1 ˙¬ (∗)n 504 2 ∗ ∉ ∗ 505 2 ∗ ≠ ∗ 506 2 ∗ ˙∧ ∗ 507 2 ∗ ˙∨ ∗ 508 2 ∃∗: ∗ 509 2 ∗ ˙⇔ ∗ 510 2 {ph ∈ ∗ | ∗}

The pyk compiler, version 0.grue.20060417+ by Klaus Grue GRD-2006-12-15.UTC:00:19:10.164930 = MJD-54084.TAI:00:19:43.164930 = LGT-4672858783164930e-6