List of theorems referencing the symbol CDR

(10) Theorem 8: [cdr of pair] cdr([X,Y]) = Y
(11) Theorem 9: [Ordered pair property] (car([X,Y]) = X) & (cdr([X,Y]) = Y)
(12) Theorem 10: [Ordered pair property, 2] [X,Y] = [car([X,Y]),cdr([X,Y])]
(13) Theorem 11: [Pair reconstruction lemma] (U = [A,B]) •imp (U = [car(U),cdr(U)])
(39) Theorem 26: [Maps are mapformers] Is_map(F) •eq (F •incin {[car(x),cdr(x)]: x in F})
(72) Theorem 51: [Map members are pairs] (Is_map(F) •imp ((X in F) •imp (X = [car(X),cdr(X)]))) & ((FORALL x in F | x = [car(x),cdr(x)]) •imp Is_map(F))
(82) Theorem 61: [Range membership lemma] (X in F) •imp (cdr(X) in range(F))
(104) Theorem 74: [Map image formula] (Svm(F) & (X in F)) •imp (F~[car(X)] = cdr(X))
(106) Theorem 76: [Map members are pairs, 2] (Is_map(F) & (U in F)) •imp (U = [car(U),cdr(U)])
(174) Theorem 135: [Members of Cartesian products] (X in (S •PROD T)) •imp ((car(X) in S) & (cdr(X) in T))
(378) Theorem 327: [Form of a shifted sequence] ((M in Za) & (domain(F) •incin Za)) •imp (shifted_seq(F,M) = {[car(x) •MINUS M,cdr(x)]: x in F | car(x) incs M})
(379) Theorem 328: [Properties of finite and shifted finite sequences] ((F in Fin_seqs(S)) & (G in Fin_seqs(S))) •imp (Svm({[car(x) •PLUS #F, cdr(x)]: x in G}) & (domain(F) * domain({[car(x) •PLUS #F, cdr(x)]: x in G}) = 0))
(426) Theorem product_order_2: [The second component of any member of a Cartesian product of ordinals is an ordinal] (X in o1 •PROD o2) •imp Ord(cdr(X))
(427) Theorem product_order_3: [The maximum of the components of any member of a Cartesian product of ordinals is an ordinal] (X in o1 •PROD o2) •imp Ord(car(X) + cdr(X))
(436) Theorem 343: (Ord(O1) & Ord(O2)) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (range(f) = (O1 •PROD O2)) & (FORALL x in domain(f), y in domain(f) | (x in y) •eq (((car(f~[x]) + cdr(f~[x])) in (car(f~[y]) + cdr(f~[y]))) or (((car(f~[x]) + cdr(f~[x])) = (car(f~[y]) + cdr(f~[y]))) & (car(f~[x]) in car(f~[y]))) or (((car(f~[x]) + cdr(f~[x])) = (car(f~[y]) + cdr(f~[y]))) & (car(f~[x]) = car(f~[y])) & (cdr(f~[x]) in cdr(f~[y]))))))
(445) Theorem 352: [The signed integers as integer pairs with one component equal to 0] (N in Si) •imp ((N = [car(N),cdr(N)]) & (car(N) = 0 or cdr(N) = 0) & (car(N) in Za) & (cdr(N) in Za) & (Red(N) = N) & (car(N) * cdr(N) = 0))
(446) Theorem 353: [Signed integers as integer pairs, 2] (N in Si) •imp ((N = [car(N),0] or N = [0,cdr(N)]) & (car(N) = 0 or cdr(N) = 0) & (car(N) in Za) & (cdr(N) in Za) & (Red(N) = N) & (car(N) * cdr(N) = 0))
(517) Theorem sigma_theory2: [Summation of singleton map is range element] (cdr(X) in s) •imp (sigma_thryvar({X}) = cdr(X))
(518) Theorem sigma_theory4: [Removal of single element from domain of a sum] ((C in F) & Finite(F) & (range(F) •incin s)) •imp (sigma_thryvar(F) = pluz(sigma_thryvar(F - {C}),cdr(C)))
(533) Theorem linear_order_12: (FORALL f | (Finite(f) & (range(f) •incin next(s0))) •imp (min_over_thryvar(f) in next(s0))) & (FORALL x | (cdr(x) in next(s0)) •imp (min_over_thryvar({x}) = cdr(x))) & (FORALL f,t | (Finite(f) & Is_map(f) & (range(f) •incin next(s0))) •imp (min_over_thryvar(f) = smaller_thryvar(min_over_thryvar(f •ON (domain(f) * t)),min_over_thryvar(f •ON (domain(f) - t))))) & (FORALL c,f | ((c in f) & Finite(f) & (range(f) •incin next(s0))) •imp (min_over_thryvar(f) = smaller_thryvar(min_over_thryvar(f - {c}),cdr(c))))
(564) Theorem 414: [Fractions are pairs of signed integers with non-zero denominator] (X in Fr) •eq ((X = [car(X),cdr(X)]) & (car(X) in Si) & (cdr(X) in Si) & (cdr(X) /= [0,0]))
(566) Theorem 416: [Rational numbers are classes of pairs of signed integers] (N in Ra) •imp ((arb(N) in Fr) & (arb(N) = [car(arb(N)),cdr(arb(N))]) & (car(arb(N)) in Si) & (cdr(arb(N)) in Si) & (cdr(arb(N)) /= [0,0]))
(567) Theorem 417: [Fractions are equivalent if their cross-products are equal] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & (W in Fr) & (Z in Fr) & Same_frac(W,Z)) •imp Same_frac([(car(X) •S_TIMES cdr(W)) •S_PLUS (car(W) •S_TIMES cdr(X)),cdr(X) •S_TIMES cdr(W)], [(car(Y) •S_TIMES cdr(Z)) •S_PLUS (car(Z) •S_TIMES cdr(Y)),cdr(Y) •S_TIMES cdr(Z)])
(568) Theorem 418: [If two pair of fractions are equivalent, their formal sums are also equivalent] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & (W in Fr) & (Z in Fr) & Same_frac(W,Z)) •imp (Fr_to_Ra([(car(X) •S_TIMES cdr(W)) •S_PLUS (car(W) •S_TIMES cdr(X)),cdr(X) •S_TIMES cdr(W)]) = Fr_to_Ra([(car(Y) •S_TIMES cdr(Z)) •S_PLUS (car(Z) •S_TIMES cdr(Y)),cdr(Y) •S_TIMES cdr(Z)]))
(568+) Theorem 419: [If two pairs of fractions are equivalent, their formal products are also equivalent] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & (W in Fr) & (Z in Fr) & Same_frac(W,Z)) •imp Same_frac([car(X) •S_TIMES car(W),cdr(X) •S_TIMES cdr(W)],[car(Y) •S_TIMES car(Z),cdr(Y) •S_TIMES cdr(Z)])
(569) Theorem 420: [If two pairs of fractions are equivalent, their formal sums define the same rational number] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & (W in Fr) & (Z in Fr) & Same_frac(W,Z)) •imp (Fr_to_Ra([car(X) •S_TIMES car(W),cdr(X) •S_TIMES cdr(W)]) = Fr_to_Ra([car(Y) •S_TIMES car(Z),cdr(Y) •S_TIMES cdr(Z)]))
(570) Theorem 421: [The sum of a rational number and a formal fraction can be expressed as a sum of formal fractions] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp (X •Ra_PLUS Fr_to_Ra([Y,Z]) = Fr_to_Ra([(car(arb(X)) •S_TIMES Z) •S_PLUS (cdr(arb(X)) •S_TIMES Y),(cdr(arb(X)) •S_TIMES Z)]))
(571) Theorem 422: [The product of a rational number and a formal fraction can be expressed as a product of formal fractions] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp (X •Ra_TIMES Fr_to_Ra([Y,Z]) = Fr_to_Ra([car(arb(X)) •S_TIMES Y,cdr(arb(X)) •S_TIMES Z]))
(572) Theorem 423: [Reversing both the numerator and denominator of a formal fraction does not change the rational it represents] (X in Fr) •imp Same_frac(X,[S_Rev(car(X)),S_Rev(cdr(X))])
(573) Theorem 424: [?] ((X in Fr) & (Y in Fr) & Same_frac(X,Y) & is_nonneg(cdr(X)) & is_nonneg(cdr(Y))) •imp ((is_nonneg(car(X)) or car(X) = [0,0]) •eq (is_nonneg(car(Y)) or car(Y) = [0,0]))
(574) Theorem 425: [The sign of the product of the numerator and denominator of a fraction defines the sign of the rational number which it represents] ((X in Fr) & (Y in Fr) & Same_frac(X,Y)) •imp (is_nonneg(car(X) •S_TIMES cdr(X)) •eq is_nonneg(car(Y) •S_TIMES cdr(Y)))
(575) Theorem 426: [?] (X in Fr) •imp (Fr_is_nonneg(X) •eq Fr_is_nonneg([S_Rev(car(X)),S_Rev(cdr(X))]))
(578) Theorem 429: [?] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp (Fr_to_Ra([Y,Z]) •Ra_PLUS X = Fr_to_Ra([(car(arb(X)) •S_TIMES Z) •S_PLUS (cdr(arb(X)) •S_TIMES Y),(cdr(arb(X)) •S_TIMES Z)]))
(580) Theorem 432: [?] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp ((Fr_to_Ra([Y,Z]) •Ra_TIMES X) = Fr_to_Ra([car(arb(X)) •S_TIMES Y,cdr(arb(X)) •S_TIMES Z]))
(900) Theorem 745: (R_SIGMA(0) = R_0) & (FORALL x in OM | (cdr(x) in Re) •imp (R_SIGMA({x}) = cdr(x))) & (FORALL f in OM | (Finite(f) & (range(f) •incin Re)) •imp (R_SIGMA(f) in Re)) & (FORALL f in OM, c in f | (Finite(f) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA(f - {c}) •R_PLUS cdr(c))) & (FORALL f in OM | (Finite(f) & Is_map(f) & (range(f) •incin Re)) •imp (FORALL t | R_SIGMA(f) = R_SIGMA(f •ON (domain(f) * t)) •R_PLUS R_SIGMA(f •ON (domain(f) - t)))) & (FORALL f in OM, g | (Finite(f) & Svm(f) & Svm(g) & (domain(f) = domain(g)) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA({[y,R_SIGMA(f •ON (g •INV_IM {y}))]: y in range(g)}))) & (FORALL f in OM, g | (Finite(f) & Svm(f) & one_1_map(g) & (domain(f) = domain(g)) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA({[y,f~[inv(g)~[y]]]: y in range(g)})))
(901) Theorem 746: (R_SIGMA(0) = R_0) & ((cdr(X) in Re) •imp (R_SIGMA({X}) = cdr(X))) & ((Finite(F) & (range(F) •incin Re)) •imp (R_SIGMA(F) in Re)) & ((Finite(F) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA(F - {c}) •R_PLUS cdr(c))) & ((Finite(F) & Is_map(F) & (range(F) •incin Re)) •imp R_SIGMA(F) = R_SIGMA(F •ON (domain(F) * T)) •R_PLUS R_SIGMA(F •ON (domain(F) - T))) & ((Finite(F) & Svm(F) & Svm(G) & (domain(F) = domain(G)) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA({[y,R_SIGMA(F •ON (G •INV_IM {y}))]: y in range(G)}))) & ((Finite(F) & Svm(F) & one_1_map(G) & (domain(F) = domain(G)) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA({[y,F~[inv(G)~[y]]]: y in range(G)})))
(914) Theorem 759: (BoundedClosedRe(S) & (S •incin Un({OI(car(ends),cdr(ends)): ends in T})) & (FORALL ends in T | ends in (Re •PROD Re))) •imp (EXISTS T1 | (T1 •incin T) & Finite(T1) & (S •incin Un({OI(car(ends),cdr(ends)): ends in T1})))
(926) Theorem 804: (M in Cm) •eq ((M = [car(M),cdr(M)]) & (car(M) in Re) & (cdr(M) in Re))
(947) Theorem real_sigma0: (FORALL f | (Finite(f) & (range(f) •incin Re)) •imp (Sig(f) in Re)) & (FORALL x | (cdr(x) in Re) •imp (Sig({x}) = cdr(x))) & (FORALL f,t | (Finite(f) & Is_map(f) & (range(f) •incin Re)) •imp (Sig(f) = (Sig(f •ON (domain(f) * t)) •R_PLUS Sig(f •ON (domain(f) - t)))))