N/M := Fr_to_Ra([N,0],[M,0]) Ra_abs(Q) := if Ra_is_nonneg(Q) then Q else Ra_Rev(Q) end ifThe following list of statements gives some basic facts about these operations. In particular, they imply that the operation which associates the value Ra_abs(a *Ra_MINUS b) with every pair a, b of rational numbers can be viewed as a 'distance' function:

Theorem A: P in Ra *imp (EXISTS l in Z, m in Z | m /= 0 & l/m = P) Theorem B: ({J,K,M,N} *incin Z-{0} & L in Z & N *incin M & K /= L & K /= M) *imp (L/M in Ra & J/M *Ra_LE J/N & N/K *Ra_LE M/K & K/N /= L/N & J/K /= J/M & Ra_0 *Ra_LE L/M & (Ra_0 = L/M *eq L = 0) & 1/K *Ra_PLUS 1/K = 2/K & 1/(2 *TIMES K) *Ra_PLUS 1/(2 *TIMES K) = 1/K) Theorem C: (P in Ra & Q in Ra & R in Ra) *imp (P *Ra_LE Ra_abs(P) & Ra_abs(Ra_abs(P)) = Ra_abs(P) & (Ra_abs(P) = Ra_0 *eq P = Ra_0) & Ra_abs(Ra_Rev(P)) = Ra_abs(P) & Ra_abs(P *Ra_PLUS Q) *Ra_LE Ra_abs(P) *Ra_PLUS Ra_abs(Q) & Ra_abs(Ra_abs(P) *Ra_MINUS Ra_abs(Q)) *Ra_LE Ra_abs(P *Ra_MINUS Q) & Ra_abs(Q *Ra_MINUS Q) = Ra_0 & Ra_abs(P *Ra_MINUS Q) = Ra_abs(Q *Ra_MINUS P) & Ra_abs(P *Ra_MINUS Q) *Ra_LE Ra_abs(P *Ra_MINUS R) *Ra_PLUS Ra_abs(R *Ra_MINUS Q) & Ra_abs(Q) *Ra_MINUS Ra_abs(Ra_abs(P) *Ra_MINUS Ra_abs(Q)) *Ra_LE Ra_abs(P)) Theorem D: Ra_abs(P *Ra_TIMES Q) = Ra_abs(P) *Ra_TIMES Ra_abs(Q) * Theorem E: Q in Ra *imp (EXISTS m in Z | Q *Ra_LT (m/1)) * Theorem F: (P in Ra & J in Z & J /= 0 & (FORALL k in Z | k /= 0 *imp Ra_abs(P) *Ra_LT (J/k))) *imp P = Ra_0An infinite sequence s

Def a: regular_maps := {s: s *incin Z *PROD Ra | Z = domain(s) & (FORALL p in s, q in s | Ra_abs(cdr(p) *Ra_MINUS cdr(q)) *Ra_LE (1/next(car(p))) *Ra_PLUS (1/next(car(q))))} Theorem G: Q in Ra *imp {[n,Q]: n in Z} in regular_mapsIn using regular sequences to represent real numbers, we regard two regular sequences s,t as being 'the same' (in the sense of representing the same real number) if, for all N, their corresponding components s

Def b: Same_regmap(S,T) :*eq (FORALL p in S, q in T | car(p) = car(q) *imp Ra_abs(cdr(p) *Ra_MINUS cdr(q)) *Ra_LE (2/next(car(p))))The following theorem is used to derive the fact that the 'Same_regmap' relationship is transitive and hence is an equivalence relation. It states that if s and t are equivalent regular sequences, then for each positive integer k there is an m such that for all N greater than or equal to m, the corresponding components s

* Theorem H: S in regular_maps & T in regular_maps *imp (Same_regmap(S,T) *eq (FORALL k in Z | k /= 0 *imp (EXISTS m in Z | (FORALL p in S, q in T | m *incin car(p) & car(p) = car(q) *imp Ra_abs(cdr(p) *Ra_MINUS cdr(q)) *Ra_LE (1/k))))) Theorem H': S in regular_maps & T in regular_maps & R in regular_maps *imp Same_regmap(S,S) & (Same_regmap(T,R) & Same_regmap(R,S) *imp Same_regmap(S,T))The following auxiliary theories ease derivation of the reflexivity of Same_regmap, and give us a convenient way of obtaining a regular sequence from a regular map.

THEORY shifted_regmap(s,f,m) s in regular_maps (FORALL n in Z | f(n) in Z & n *incin f(n)) ==>(t) t = {[k,cdr(p)]: k in Z, p in s | car(p)=f(k)} Same_regmap(t,s) Svm(s) *imp Svm(t) END shifted_regmap THEORY regmap_to_seq(t) t in regular_maps ==>(s) -- s = {[n,arb({cdr(p):p in t|car(p) = n})]: n in Z} s in regular_maps Svm(s) Same_regmap(t,s) END regmap_to_seqWe are now ready to define real numbers via application of the THEORY equivalence_classes, which also gives a natural embedding of the rational numbers into the reals.

APPLY(Re,Seq_to_Re) equivalence_classes(P(x,y)->Same_regmap(x,y), s->regular_maps) ==> (FORALL x in regular_maps | Seq_to_Re(x) in Re) (FORALL x in Re | arb(x) in regular_maps & Seq_to_Re(arb(x)) = x) (FORALL x in regular_maps | (FORALL y in regular_maps | (Same_regmap(x,y) *eq (Seq_to_Re(x) = Seq_to_Re(y))))) (FORALL x in regular_maps | Same_regmap(x,arb(Seq_to_Re(x)))) Def c: [Rational-to-Real conversion] Ra_to_Re(Q) := Seq_to_Re({[n,Q]: n in Z}) Def d: [Real 0] R_0 := Ra_to_Re(Ra_0) Def e: [Real 1] R_1 := Ra_to_Re(Ra_1)To introduce the algebraic operations on the set Re of reals we need an auxiliary bound for the terms of a regular sequence s of rational numbers. We define the 'canonical' bound of such an s to be the least integer m which is at least 2 greater than the absolute value of the first component of s. It follows easily that m is greater than the absolute value of s

Def f: canon_bound(S) := arb({m: m in Z | (EXISTS p in S | car(p) = 0 & Ra_abs(cdr(p)) *Ra_PLUS (2/1) *Ra_LT (m/1))}) * Theorem K: S in regular_maps & P in S *imp Ra_abs(cdr(P)) *Ra_LT (canon_bound(S)/1)The arithmetic operations on real numbers x,y are now defined in terms of their rational approximations x

Def g: [Real Sum] def(X *R_PLUS Y) := Seq_to_Re( {[n,cdr(p) *Ra_PLUS cdr(q)]: n in Z, p in arb(X), q in arb(Y) | next(n *PLUS n) = car(p) & car(p) = car(q)}) Def h: [Real Negative] R_Rev(X) := Seq_to_Re( {[car(p),Ra_Rev(cdr(p))]: p in arb(X)}) Def j: [Real Subtraction] def(X *R_MINUS Y) := X *Ra_PLUS R_Rev(Y) Def k: [Real Multiplication] def(X *R_TIMES Y) := Seq_to_Re( {[n,cdr(p) *Ra_TIMES cdr(q)]: n in Z, p in arb(X), q in arb(Y) | 2 *TIMES ((canon_bound(X)+canon_bound(Y)) *TIMES next(n)) = next(car(p)) & car(p) = car(q)}) Def m: [Absolute value, i.e. the larger of X and R_Rev(X)] abs(X) := Seq_to_Re({[car(p),Ra_abs(cdr(p))]: p in arb(X)}) Def n: R_is_nonneg(X) :*eq abs(X)=X Def p: Z_aux(S) := arb({m: m in Z | m /= 0 & (FORALL p in S | m *Ra_LE next(car(p)) *imp (1/m) *Ra_LE Ra_abs(cdr(p)))}) Def q: [Real Reciprocal] R_Recip(X) := Seq_to_Re( {[n, Recip(cdr(p))]: n in Z, p in arb(X), m in Z | m = Z_aux(arb(X)) & next(car(p)) = (n+m) *TIMES (m *TIMES m)}) Def r: [Real Quotient] def(X *R_OVER Y) := X *R_TIMES R_Recip(Y)Here, for example, Definition q states that in order to get the reciprocal of a real number X, one must consider a regular sequence s

It is important to show that the above operations produce real numbers when their operands are reals, and that the results of the arithmetic operations do not depend on the way in which one chooses a representative sequence from each of the equivalence classes representing reals. For example, for real addition, we need to know that

* Theorem M: S in regular_maps & T in regular_maps *imp {[n,cdr(p) *Ra_PLUS cdr(q)]: n in Z, p in S, q in T | next(n *PLUS n) = car(p) & car(p) = car(q)} in regular_maps * Theorem N: X in Re & Y in Re *imp X *R_PLUS Y in Re * Theorem P: SAnalogously, for the real reciprocal operation, we need to know that_{1}in regular_maps & S_{2}in regular_maps & T_{1}in regular_maps & T_{2}in regular_maps & Same_regmap(S_{1},S_{2}) & Same_regmap(T_{1},T_{2}) *imp Same_regmap({[n,Ra_abs(cdr(p)) *Ra_PLUS Ra_abs(cdr(q))]: n in Z, p in S_{1}, q in T_{1}| next(n *PLUS n) = car(p) & car(p) = car(q)}, {[n,Ra_abs(cdr(p)) *Ra_PLUS Ra_abs(cdr(q))]: n in Z, p in S_{2}, q in T_{2}| next(n *PLUS n) = car(p) & car(p) = car(q)})

* Theorem M': S in regular_maps & not(Same_regmap(S,{[n,Ra_0]: n in Z})) *imp (EXISTS m in Z | m /= 0 & (FORALL p in S | m *Ra_LE next(car(p)) *imp (1/m) *Ra_LE Ra_abs(cdr(p)))) * Theorem M'': S in regular_maps & M in Z & M /= 0 & (FORALL p in S | M *Ra_LE next(car(p)) *imp (1/M) *Ra_LE Ra_abs(cdr(p))) *imp {[n, Recip(cdr(p))]: n in Z, p in S | next(car(p)) = (n+M) *TIMES (M *TIMES M)} in regular_maps Theorem N': X in Re & X /= R_0 *imp R_Recip(X) in Re * Theorem P': S in regular_maps & MWe also need to derive the algebraic properties of the basic operations on reals from the definitions given above, e.g._{1}in Z & M_{2}in Z & M_{1}/= 0 & M_{2}/= 0 & (FORALL p in S | M_{1}*Ra_LE next(car(p)) *imp (1/M_{1}*Ra_LE Ra_abs(cdr(p)))) & (FORALL p in S | M_{2}*Ra_LE next(car(p)) *imp (1/M_{2}*Ra_LE Ra_abs(cdr(p)))) *imp Same_regmap({[n, Recip(cdr(p))]: n in Z, p in S | next(car(p)) = (n+M_{1}) *TIMES (M_{1}*TIMES M_{1})}, {[n, Recip(cdr(p))]: n in Z, p in S | next(car(p)) = (n+M_{2}) *TIMES (M_{2}*TIMES M_{2})})

Theorem Q: X in Re & Y in Re & W in Re *imp X *R_PLUS Y = Y *R_PLUS X & W *R_PLUS (X *R_PLUS Y) = (W *R_PLUS X) *R_PLUS Y & X *R_PLUS R_0 = X & X *R_PLUS R_Rev(X) = R_0 & X *R_TIMES Y = Y *R_TIMES X & R_1 *R_TIMES X = X & X *R_TIMES R_1 = X & (X /= R_0 *imp (X *R_TIMES Y=R_1 *eq Y=R_Recip(X)))There are important connections between rational and real numbers, such as the fact that Ra is 'order dense' in Re. The following definitions and theorems define the ordering of reals and state this fact.

Def s: [Real Maximum] def(X *R_MAX Y) := Seq_to_Re({[car(p), if cdr(p) *Ra_LE cdr(q) then cdr(q) else cdr(p) end if]: p in arb(X), q in arb(Y) | car(p) = car(q)}) Def t: [Real Ordering] def(X *R_LE Y) :*eq (X *R_MAX Y) = Y Def u: [Real Ordering] def(X *R_LT Y) :*eq (X *R_MAX Y) /= X Theorem R: X in Re & [N,Y] in arb(X) *imp abs(X *R_MINUS Ra_to_Re(Y)) *R_LE Ra_to_Re(1/N) Theorem S: X in Re & Y in Re *imp (EXISTS r in Ra | X *R_LT Ra_to_Re(r) & Ra_to_Re(r) *R_LT Y)Another important connection between real and rational numbers lies in Dedekind cuts, which are the nonnull sets d of rational numbers, bounded above, such that every rational not in d is larger than any rational in d. (If we added the requirement that to any x in d there must correspond a larger rational y in d, then we could establish a one-to-one correspondence between Dedekind cuts and real numbers; but this is of no concern to us here.) Below we specify this notion formally, and define a function translating Dedekind cuts into real numbers, and then define the operation which determines the least upper bound of any nonnull set of real numbers bounded above:

Def v: dedekind_cuts := {d: d *incin Ra | 0 /= d & d /= Ra & (FORALL x in d, y in Ra | y *Ra_LT x *imp y in d)} Def w: [Cut-to-Real conversion] Dedek_to_Re(D):= Seq_to_Re({ [n, arb(D) *Ra_PLUS arb({(h/next(n)) : h in Z | arb(D) *Ra_PLUS (next(h)/next(n)) notin D})]: n in Z}) * Theorem T: D in dedekind_cuts *imp Dedek_to_Re(D) in Re Def x: [Least Upper Bound] Re_LUB(I) := Dedek_to_Re( Un({q: q in Ra| (EXISTS x in I| Ra_to_Re(q) *R_LT x)})) * Theorem U: I in Re & I /= 0 & (EXISTS y in Re | (FORALL x in I | x *R_LE y)) *imp Re_LUB(I) in Re & (FORALL y in Re | Re_LUB(I) *R_LT y *eq (FORALL x in I | x *R_LE y))====================== Proof sketches ==================================

Proof of Theorem C: The many theses of this theorem are obvious consequences of the fact that the quadruple (Ra, *Ra_PLUS, Ra_0, Ra_is_nonneg) constitutes an ordered Abelian group within which the operation *Ra_MINUS behaves as the inverse of *Ra_PLUS. Otter experiments deducing Theorem C from this fact are documented here. QED

Proof of Theorem H: Assuming that Theorem H is false, we are led to consider s,t such which fall into the following two cases:

Case 1:

Same_regmap(s,t) & k in Z & k /= 0 & not(EXISTS m in Z | (FORALL p in s, q in t | m *incin car(p) & car(p) = car(q) *imp Ra_abs(cdr(p) *Ra_MINUS cdr(q)) *Ra_LE (1/k)))However, since in this case we have

(FORALL p in s, q in t | car(p) = car(q) *imp Ra_abs(cdr(p) *Ra_MINUS cdr(q)) *Ra_LE (2/next(car(p))))by the definition of Same_regmap, we can take m = 2 *TIMES k and then replace 2/next(car(p)) by 1/k inside

(FORALL p in s, q in t | m *incin car(p) & car(p) = car(q) *imp Ra_abs(cdr(p) *Ra_MINUS cdr(q)) *Ra_LE (2/next(car(p))))because m *incin car(p) implies the following *Ra_LE-chain:

2/next(car(p)) *Ra_LE 2/next(m) & 2/next(m) = 2/next(2 *TIMES k) & 2/next(2 *TIMES k) *Ra_LT 2/(2 *TIMES k) & 2/(2 *TIMES k) = 1/kThis leads to a contradiction.

Case 2:

s in regular_maps & t in regular_maps & not(Same_regmap(s,t)) & (FORALL k in Z | k /= 0 *imp (EXISTS m in Z | (FORALL p in s, q in t | m *incin car(p) & car(p) = car(q) *imp Ra_abs(cdr(p) *Ra_MINUS cdr(q)) *Ra_LE (1/k))))We can obtain a contradiction in this case by using the last part of the assumption, namely

(FORALL k in Z | k /= 0 *imp (EXISTS m in Z | (FORALL d in s, b in t | m *incin car(d) & car(d) = car(b) *imp Ra_abs(cdr(d) *Ra_MINUS cdr(b)) *Ra_LE (1/k))))to derive

K in Z & K /= 0 & P in s & Q in t & car(P) = car(Q) *imp Ra_abs(cdr(P) *Ra_MINUS cdr(Q)) *Ra_LT (2/next(car(P))) *Ra_PLUS (3/K)).It follows readily from this that

P in s & Q in t & car(P) = car(Q) *imp Ra_abs(cdr(P) *Ra_MINUS cdr(Q)) *Ra_LE 2/next(car(P))which conflicts with not(Same_regmap(s,t))). It remains to find a contradiction between

(FORALL k in Z | k /= 0 *imp (EXISTS m in Z | (FORALL d in s, b in t | m *incin car(d) & car(d) = car(b) *imp Ra_abs(cdr(d) *Ra_MINUS cdr(b)) *Ra_LE (1/k))))and

k in Z & k /= 0 & p in s & q in t & car(p) = car(q) & Ra_abs(cdr(p) *Ra_MINUS cdr(q)) *Ra_GE (2/next(car(p))) *Ra_PLUS (3/k))under the assumption that s in regular_maps & t in regular_maps & d in s & b in t. But these assumptions let us find an m for which

(FORALL d in s, b in t | m *incin car(d) & car(d) = car(b) *imp Ra_abs(cdr(d) *Ra_MINUS cdr(b)) *Ra_LE (1/k).Then, using the regularity of s,t, and choosing d,s such that

d in s & b in t & car(d) = car(b) & car(b) = k *PLUS mwe can write the following *Ra_LT-chain.

Ra_abs(cdr(p) *Ra_MINUS cdr(q)) *Ra_LE Ra_abs(cdr(p) *Ra_MINUS cdr(d)) *Ra_PLUS (Ra_abs(cdr(d) *Ra_MINUS cdr(b) *Ra_PLUS Ra_abs(cdr(b) *Ra_MINUS cdr(q)))) & Ra_abs(cdr(p) *Ra_MINUS cdr(d)) *Ra_PLUS (Ra_abs(cdr(d) *Ra_MINUS cdr(b) *Ra_PLUS Ra_abs(cdr(b) *Ra_MINUS cdr(q)))) *Ra_LE ((1/next(car(p)) *Ra_PLUS (1/next(car(d)))) *Ra_PLUS ((1/k) *Ra_PLUS ((1/next(car(p)) *Ra_PLUS (1/next(car(d))))))) & ((1/next(car(p)) *Ra_PLUS (1/next(car(d)))) *Ra_PLUS ((1/k) *Ra_PLUS ((1/next(car(p)) *Ra_PLUS (1/next(car(d))))))) *Ra_LT ((2/next(car(p))) *Ra_PLUS (3/k))From this we get

Ra_abs(cdr(p) *Ra_MINUS cdr(q)) *Ra_LT ((2/next(car(p))) *Ra_PLUS (3/k))conflicting with a fact derived earlier, QED

Proofs pertaining to the THEORY shifted_regmap. Obviously t is a map, because it consists of pairs; moreover,
domain(t) *incin Z. Also, Z *incin domain(t): in fact, for any k in Z, the pair [n,cdr(p)] will
belong to t for any element p of s whose first component is f(k) (since f(k) is in Z, one such p is guaranteed to exist).
If s is single valued, then t is single valued too: in fact, since there is only one p in s such that
car(p)=f(k), there will be only one pair [k,cdr(p)] in t for each k in Z.

Now make the absurd hypothesis that

b in t & d in t & Ra_abs(cdr(b) *Ra_MINUS cdr(d)) *Ra_GT (1/next(car(b))) *Ra_PLUS (1/next(car(d))).Then it follows from b in t, d in t that [f(car(b)),cdr(b)] and [f(car(d)),cdr(d)] are in s; hence (taking the inclusions car(b) *incin f(car(b)) and car(d) *incin f(car(d)) into account) we get the following *Ra_LE-chain

Ra_abs(cdr(b) *Ra_MINUS cdr(d)) = Ra_abs(cdr([f(car(b),cdr(b)]) *Ra_MINUS cdr([f(car(d)),cdr(d)])) & Ra_abs(cdr([f(car(b),cdr(b)]) *Ra_MINUS cdr([f(car(d)),cdr(d)])) *Ra_LE ((1/next(f(car(b))) *Ra_PLUS (1/next(f(car(d))))) & ((1/next(f(car(b))) *Ra_PLUS (1/next(f(car(d))))) *Ra_LE ((1/next(car(b)) *Ra_PLUS (1/next(car(d)))))which contradicts the absurd hypothesis. This leads to the conclusion that t is in regular_maps.

Now make the absurd hypothesis that

p in s & d in t & car(p)=car(d) & Ra_abs(cdr(p) *Ra_MINUS cdr(d)) *Ra_GT (2/next(car(p))).Then [f(car(d)),cdr(d)] is in s, and hence we get

Ra_abs(cdr(p) *Ra_MINUS cdr(d)) = Ra_abs(cdr(p) *Ra_MINUS cdr([f(car(d)),cdr(d)]) & Ra_abs(cdr(p) *Ra_MINUS cdr([f(car(d)),cdr(d)]) *Ra_LE ((1/next(car(p)) *Ra_PLUS (1/next(f(car(d))))) & ((1/next(car(p)) *Ra_PLUS (1/next(f(car(d))))) *Ra_LE ((1/next(car(p)) *Ra_PLUS (1/next(car(p))) & ((1/next(car(p)) *Ra_PLUS (1/next(car(p))) = (2/next(car(p)),conflicting with the absurd hypothesis again. This leads to the conclusion that Same_regmap(s,t). QED

Proof of Theorem K: Assuming the opposite, let s,q be such that

s in regular_maps & q in s & (canon_bound(s)/1) *Ra_LE Ra_abs(cdr(q))implying cdr(q) in Ra. The Archimedean property of rational numbers (Theorem E) lets us to show using the fact that s in regular_maps that

canon_bound(s) in Z & p in s & car(p) = 0 & Ra_abs(cdr(p)) *Ra_PLUS (2/1) *Ra_LT (canon_bound(s)/1)holds for a suitable p, and hence that cdr(p) in Ra and (canon_bound(s)/1) in Ra. Using the definition of regular_maps again, we have also

(FORALL q in s | Ra_abs(cdr(p) *Ra_MINUS cdr(q)) *Ra_LE (1/1) *Ra_PLUS 1/next(car(q)))whence

Ra_abs(cdr(p) *Ra_MINUS cdr(q)) *Ra_LE (2/1))follows. By instantiating P as p and Q as q in the *Ra_LE-chain

Ra_abs(cdr(Q)) *Ra_MINUS Ra_abs(cdr(P)) *Ra_LE Ra_abs(Ra_abs(cdr(Q)) *Ra_MINUS Ra_abs(cdr(P))) & Ra_abs(Ra_abs(cdr(Q)) *Ra_MINUS Ra_abs(cdr(P))) *Ra_LE Ra_abs(cdr(Q) *Ra_MINUS cdr(P)) & Ra_abs(cdr(Q) *Ra_MINUS cdr(P)) = Ra_abs(cdr(P) *Ra_MINUS cdr(Q))we get Ra_abs(cdr(q)) *Ra_MINUS Ra_abs(cdr(p)), and hence

Ra_abs(cdr(q)) *Ra_LE Ra_abs(cdr(p)) *Ra_PLUS Ra_abs(cdr(p) *Ra_MINUS cdr(q)) & Ra_abs(cdr(p)) *Ra_PLUS Ra_abs(cdr(p) *Ra_MINUS cdr(q)) *Ra_LE Ra_abs(cdr(p)) *Ra_PLUS (2/1) & Ra_abs(cdr(p)) *Ra_PLUS (2/1) *Ra_LT (canon_bound(s)/1) *Ra_PLUS (2/1).This leads to

Ra_abs(cdr(q)) *Ra_LT (canon_bound(s)/1)and hence to a contradiction, QED

Proof of Theorem M: Assuming S in regular_maps and T in regular_maps, we must show that

{[n,cdr(p) *Ra_PLUS cdr(q)]: n in Z, p in S, q in T | next(n *PLUS n) = car(p) & car(p) = car(q)}is a regular map. After showing that this is a map with domain Z, we are left with the task of obtaining a contradiction from

s in regular_maps & t in regular_maps & m in Z & n in Z & b in s & p in s & d in t & q in t & next(m *Ra_PLUS m) = car(b) & car(b) = car(d) & next(n *Ra_PLUS n) = car(p) & car(p) = car(q) & Ra_abs((cdr(b) *Ra_PLUS cdr(d)) *Ra_MINUS (cdr(p) *Ra_PLUS cdr(q))) *Ra_GT ((1/next(m)) *Ra_PLUS (1/next(n)))These last statements let us write the following *Ra_LE-chain:

Ra_abs((cdr(b) *Ra_PLUS cdr(d)) *Ra_MINUS (cdr(p) *Ra_PLUS cdr(q))) = Ra_abs((cdr(b) *Ra_MINUS cdr(p)) *Ra_PLUS (cdr(d) *Ra_MINUS cdr(q))) & Ra_abs((cdr(b) *Ra_MINUS cdr(p)) *Ra_PLUS (cdr(d) *Ra_MINUS cdr(q))) *Ra_LE Ra_abs((cdr(b) *Ra_MINUS cdr(p))) *Ra_PLUS Ra_abs((cdr(d) *Ra_MINUS cdr(q))) & Ra_abs((cdr(b) *Ra_MINUS cdr(p))) *Ra_PLUS Ra_abs((cdr(d) *Ra_MINUS cdr(q))) *Ra_LE ((1/next(next(m *PLUS m))) *Ra_PLUS (1/next(next(n *PLUS n)))) *Ra_PLUS ((1/next(next(m *PLUS m))) *Ra_PLUS (1/next(next(n *PLUS n)))) & ((1/next(next(m *PLUS m))) *Ra_PLUS (1/next(next(n *PLUS n)))) *Ra_PLUS ((1/next(next(m *PLUS m))) *Ra_PLUS (1/next(next(n *PLUS n)))) = (1/next(m)) *Ra_PLUS (1/next(n))whence

Ra_abs((cdr(b) *Ra_PLUS cdr(d)) *Ra_MINUS (cdr(p) *Ra_PLUS cdr(q))) *Ra_LE ((1/next(m)) *Ra_PLUS (1/next(n)))follows. QED

Proofs of statements analogous to Theorem M about real subtraction, multiplication, and the absolute value operation are obtained just as easily. For instance, for multiplication one proves that

{[n,cdr(p) *Ra_TIMES cdr(q)]: n in Z, p in S, q in T | 2 *TIMES ((canon_bound(S)+canon_bound(T)) *TIMES (next(n))) = next(car(p)) & car(p) = car(q)}is a regular map if S and T are regular maps by deriving a contradiction from

s in regular_maps & t in regular_maps & m in Z & n in Z & b in s & p in s & d in t & q in t & 2 *TIMES (c *TIMES next(m)) = next(car(b)) & car(b) = car(d) & 2 *TIMES (c *TIMES next(n)) = next(car(p)) & car(p) = car(q) & Ra_abs((cdr(b) *Ra_TIMES cdr(d)) *Ra_MINUS (cdr(p) *Ra_TIMES cdr(q))) *Ra_GT ((1/next(m)) *Ra_PLUS (1/next(n)))where

c := (canon_bound(s)+canon_bound(t))/1This is done using the following *Ra_LE-chain.

Ra_abs((cdr(b) *Ra_TIMES cdr(d)) *Ra_MINUS (cdr(p) *Ra_TIMES cdr(q))) = Ra_abs(((cdr(b) *Ra_TIMES cdr(d)) *Ra_MINUS (cdr(b) *Ra_TIMES cdr(q))) *Ra_PLUS ((cdr(b) *Ra_TIMES cdr(q)) *Ra_MINUS (cdr(p) *Ra_MINUS cdr(q)))) & Ra_abs(((cdr(b) *Ra_TIMES cdr(d)) *Ra_MINUS (cdr(b) *Ra_TIMES cdr(q))) *Ra_PLUS ((cdr(b) *Ra_TIMES cdr(q)) *Ra_MINUS (cdr(p) *Ra_MINUS cdr(q)))) = Ra_abs((cdr(b) *Ra_TIMES (cdr(d) *Ra_MINUS cdr(q))) *Ra_PLUS (cdr(q) *Ra_TIMES (cdr(b) *Ra_MINUS cdr(p)))) & Ra_abs((cdr(b) *Ra_TIMES (cdr(d) *Ra_MINUS cdr(q))) *Ra_PLUS (cdr(q) *Ra_TIMES (cdr(b) *Ra_MINUS cdr(p)))) *Ra_LE Ra_abs((cdr(b) *Ra_TIMES (cdr(d) *Ra_MINUS cdr(q)))) *Ra_PLUS Ra_abs((cdr(q) *Ra_TIMES (cdr(b) *Ra_MINUS cdr(p)))) & Ra_abs((cdr(b) *Ra_TIMES (cdr(d) *Ra_MINUS cdr(q)))) *Ra_PLUS Ra_abs((cdr(q) *Ra_TIMES (cdr(b) *Ra_MINUS cdr(p)))) = (Ra_abs((cdr(b)) *Ra_TIMES Ra_abs((cdr(d) *Ra_MINUS cdr(q))))) *Ra_PLUS (Ra_abs((cdr(q)) *Ra_TIMES Ra_abs((cdr(b) *Ra_MINUS cdr(p))))) & (Ra_abs((cdr(b)) *Ra_TIMES Ra_abs((cdr(d) *Ra_MINUS cdr(q))))) *Ra_PLUS (Ra_abs((cdr(q)) *Ra_TIMES Ra_abs((cdr(b) *Ra_MINUS cdr(p))))) *Ra_LE (c *Ra_TIMES ((1/next(car(d))) *Ra_PLUS (1/next(car(q))))) *Ra_PLUS (c *Ra_TIMES ((1/next(car(b))) *Ra_PLUS (1/next(car(p))))) & (c *Ra_TIMES ((1/next(car(d))) *Ra_PLUS (1/next(car(q))))) *Ra_PLUS (c *Ra_TIMES ((1/next(car(b))) *Ra_PLUS (1/next(car(p))))) = (2 *TIMES c) *Ra_TIMES ((1/(2 *TIMES (c *TIMES next(m)))) *Ra_PLUS (1/(2 *TIMES (c *TIMES next(n))))) & (2 *TIMES c) *Ra_TIMES ((1/(2 *TIMES (c *TIMES next(m)))) *Ra_PLUS (1/(2 *TIMES (c *TIMES next(n))))) = (1/next(m)) *Ra_PLUS (1/next(n))QED

Proof of Theorem N: This theorem is an obvious corollary of Theorem M, because

arb(X) in regular_maps & arb(Y) in regular_mapsso that

{[n,cdr(p) *Ra_PLUS cdr(q)]: n in Z, p in arb(X), q in arb(Y) | car(p) = car(q) & car(p) = next(n *PLUS n)} in regular_mapswhich yields X *R_PLUS Y in Re, since

Seq_to_Re({[n,cdr(p) *Ra_PLUS cdr(q)]: n in Z, p in arb(X), q in arb(Y) | car(p) = car(q) & car(p) = next(n *PLUS n)}) in Refollows from the assumptions X in Re, Y in Re, in view of the definition of Re and of Seq_to_Re. QED

Proof of Theorem P: Assuming the contrary, we would have

s1 in regular_maps & s2 in regular_maps & t1 in regular_maps & t2 in regular_maps & Same_regmap(s1,s2) & Same_regmap(t1,t2) & n in Z & p1 in s1 & p2 in s2 & q1 in t1 & q2 in t2 & next(n *PLUS n)=car(p1) & car(p1)=car(q1) & next(n *PLUS n)=car(p2) & car(p2)=car(q2) & (2/next(n)) *Ra_LT Ra_abs((cdr(p1) *Ra_PLUS cdr(q1)) *Ra_MINUS (cdr(p2) *Ra_PLUS cdr(q2)))But on the other hand, these imply the *Ra_LE-chain

Ra_abs((cdr(p1) *Ra_PLUS cdr(q1)) *Ra_MINUS (cdr(p2) *Ra_PLUS cdr(q2))) = Ra_abs((cdr(p1) *Ra_MINUS cdr(p2)) *Ra_PLUS (cdr(q1) *Ra_MINUS cdr(q2))) & Ra_abs((cdr(p1) *Ra_MINUS cdr(p2)) *Ra_PLUS (cdr(q1) *Ra_MINUS cdr(q2))) *Ra_LE Ra_abs(cdr(p1) *Ra_MINUS cdr(p2)) *Ra_PLUS Ra_abs(cdr(q1) *Ra_MINUS cdr(q2)) & Ra_abs(cdr(p1) *Ra_MINUS cdr(p2)) *Ra_PLUS Ra_abs(cdr(q1) *Ra_MINUS cdr(q2)) *Ra_LE (2/next(next(n *PLUS n))) *Ra_PLUS (2/next(next(n *PLUS n))) & (2/next(next(n *PLUS n))) *Ra_PLUS (2/next(next(n *PLUS n))) *Ra_LE (2/next(n))whose fourth conjunct ensues from Same_regmap(s1,s2)&Same_regmap(t1,t2) and which implies Ra_abs((cdr(p1) *Ra_PLUS cdr(q1)) *Ra_MINUS (cdr(p2) *Ra_PLUS cdr(q2))) *Ra_LE (2/next(n)), leading to a contradiction, QED

Proof of Theorems M': Let us make the absurd hypothesis that

s in regular_maps & not(Same_regmap(s,{[n,Ra_0]: n in Z})) & (FORALL m in Z | m /= 0 *imp (EXISTS p in s | m *Ra_LE next(car(p)) & Ra_abs(cdr(p)) *Ra_LT (1/m)))It follows from the assumption not(Same_regmap(s,{[n,Ra_0]: n in Z})) that (2/next(car(q)) *Ra_LT Ra_abs(cdr(q)) holds for some q in s; therefore we readily get (1/next(car(q)) *Ra_LT Ra_abs(cdr(q)), whence

Ra_abs(cdr(q)) *Ra_MINUS (1/next(car(q))) /= Ra_0 & Ra_abs(cdr(q)) *Ra_MINUS (1/next(car(q))) = Ra_abs( Ra_abs(cdr(q)) *Ra_MINUS (1/next(car(q))))follows; and hence we get, thanks to Theorem F, the existence of an m in Z such that

m /= 0, (3/m) *Ra_LE Ra_abs(cdr(q)) *Ra_MINUS (1/next(car(q))), (1/m) *Ra_LT Ra_abs(cdr(q)) *Ra_MINUS (1/next(car(q))) *Ra_MINUS (1/m)follow. For all p in s such that m *Ra_LE next(car(p)), we hence have the following *Ra_LE-chain

(1/m) *Ra_LT Ra_abs(cdr(q)) *Ra_MINUS (1/next(car(q))) *Ra_MINUS (1/m) & Ra_abs(cdr(q)) *Ra_MINUS (1/next(car(q))) *Ra_MINUS (1/m) *Ra_LE Ra_abs(cdr(q)) *Ra_MINUS (1/next(car(q))) *Ra_MINUS (1/next(car(p))) & Ra_abs(cdr(q)) *Ra_MINUS (1/next(car(q))) *Ra_MINUS (1/next(car(p))) *Ra_LE Ra_abs(cdr(q)) *Ra_MINUS Ra_abs(Ra_abs(cdr(p)) *Ra_MINUS Ra_abs(cdr(q)))) & Ra_abs(cdr(q)) *Ra_MINUS Ra_abs(Ra_abs(cdr(p)) *Ra_MINUS Ra_abs(cdr(q)))) *Ra_LE Ra_abs(cdr(p))which implies (1/m) *Ra_LE Ra_abs(cdr(p)), leading to a contradiction. QED

Proofs of Theorems M'', P': TO BE SUPPLIED, QED

Sketch of the proof of Theorem Q: Proof of the algebraic properties of the elementary operations on reals is easy if we note that to determine the value of an arithmetic operation on real operands, we can use any regular sequence in the equivalence class of arb(X) in place of each operand X. For example, even though arb(R_0) may not equal {[n,Ra_0]: n in Z}, we can nevertheless prove that X *R_PLUS R_0 = X holds for all real numbers X by showing that

S in regular_maps *imp Same_regmap({[n,cdr(p) *Ra_PLUS Ra_0]: n in Z, p in S | next(n *PLUS n) = car(p)},S).This follows readily as an application of the THEORY shifted_regmap. Similarly, to prove the associativity law (W *R_PLUS X) *R_PLUS Y=W *R_PLUS (X *R_PLUS Y) for all W,X,Y in Re, making the absurd hypothesis that w,x,y in Re satisfy (w *R_PLUS x) *R_PLUS y /= w *R_PLUS (x *R_PLUS y), we can easily reach a contradiction by choosing (with the aid of the theories 'shifted_regmap' and 'regmap_to_seq') maps r,s,t,r1,t1 so that

Svm(r1) & Svm(r) & Svm(s) & Svm(t) & Svm(t1) & r1 in regular_maps & Same_regmap(r,r1) & r in regular_maps & Same_regmap(arb(w),r) & s in regular_maps & Same_regmap(arb(x),s) & t in regular_maps & Same_regmap(arb(y),t) & t1 in regular_maps & Same_regmap(t,t1) & r1 = {[n,cdr(p)]: n in Z, p in r | next(car(p))=(4 *TIMES next(n))} & t1 = {[n,cdr(p)]: n in Z, p in t | next(car(p))=(4 *TIMES next(n))}and by showing that

(FORALL n in Z, p in r, q in s, d1 in t1, p1 in r1, d in t | car(p1) = next(n *PLUS n) & car(d1) = next(n *PLUS n) & next(car(p)) = (4 *TIMES next(n)) & next(car(q)) = (4 *TIMES next(n)) & next(car(d)) = (4 *TIMES next(n)) *imp (cdr(p) *Ra_PLUS cdr(q)) *Ra_PLUS cdr(d1) = cdr(p1) *Ra_PLUS (cdr(q) *Ra_PLUS cdr(d))whence

Same_regmap({[n,(cdr(p) *Ra_PLUS cdr(q))*Ra_PLUS cdr(d1)]: n in Z, p in r, q in s, d1 in t | next(n *PLUS n)=car(d1) & (4 *TIMES next(n))=next(car(p)) & car(p)=car(q)}, ,{[n,cdr(p1) *Ra_PLUS (cdr(q)*Ra_PLUS cdr(d))]: n in Z, p1 in r, q in s, d in t | next(n *PLUS n)=car(p1) & (4 *TIMES next(n))=next(car(q)) & car(q)=car(d)})and therefore (w *R_PLUS x) *R_PLUS y=w *R_PLUS (x *R_PLUS y), follows, QED

Proof of Theorem T: The thesis amounts to the assertion that if we assume d to be a Dedekind cut then it follows that the sequence

{[n, arb(d) *Ra_PLUS arb({(h/next(n)) : h in Z | arb(d) *Ra_PLUS (next(h)/next(n)) notin d}]: n in Z}is regular. Putting g=arb(d), we have g in d since d/=0. For all n, the minimum h for which g *Ra_PLUS (next(h)/next(n)) does not belong to d is such that g *Ra_PLUS (h/next(n)) belongs to d (this is obvious, as just noted, if h=0); hence s

If i and j are natural numbers, let r be the smaller number between s

Ra_abs(scompleting the proof that the sequence is regular, QED_{i}*Ra_MINUS s_{j}) *Ra_LE Ra_abs(s_{i}*Ra_MINUS r) *Ra_PLUS Ra_abs(r *Ra_MINUS s_{j}) & Ra_abs(s_{i}*Ra_MINUS r) *Ra_PLUS Ra_abs(r *Ra_MINUS s_{j}) = (r *Ra_MINUS s_{i}) *Ra_PLUS (r *Ra_MINUS s_{j}) & (r *Ra_MINUS s_{i}) *Ra_PLUS (r *Ra_MINUS s_{j}) *Ra_LE ((s_{i}*Ra_PLUS (1/next(i))) *Ra_MINUS s_{i}) *Ra_PLUS (s_{j}*Ra_PLUS (1/next(j))) *Ra_MINUS s_{j}) & ((s_{i}*Ra_PLUS (1/next(i))) *Ra_MINUS s_{i}) *Ra_PLUS (s_{j}*Ra_PLUS (1/next(j))) *Ra_MINUS s_{j})= (1/next(i)) *Ra_PLUS (1/next(i))

Proof of Theorem U: TO BE SUPPLIED, QED