Defining real numbers using Bishop's 'regular' Cauchy sequences. In preparation for definition of the real numbers and real arithmetic we introduce the usual fractional notation and absolute value operation for rational numbers: 
  N/M := Fr_to_Ra([N,0],[M,0])
  Ra_abs(Q) := if Ra_is_nonneg(Q) then Q else Ra_Rev(Q) end if
The 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_0
An infinite sequence s1,s2,...,sN,... of rational numbers is said to be regular if its N-th component and its M-th component differ (in absolute value) by at most 1/N + 1/M for all pairs N, M of positive integers. The formal definition given below looks slightly more complicated than this because we number sequence components starting with 0 instead of with 1. On the other hand, we find it unnecessary to impose single valuedness; this is why our first definition introduces 'regular_maps' instead of 'regular_seqs'. An example of a regular sequence is one whose components are all equal. Note also that the sequence {[n,2/next(n)]: n in Z} is not regular, because e.g. Ra_abs(2/1-2/4) = 6/4 *Ra_GT 5/4 = 1/1 *Ra_PLUS 1/4. 
  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_maps
In 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 sN, tN differ by 2/N at most. Taking our 'numbering from 0' unit into account once more, we define: 
  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 sN and tN of s and t differ at most by 1/k. 
* 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_seq
We 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 sN for all N: 
  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 xN,yN (more precisely, arb(x)N and arb(y)N). 
  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 s1,s2,...,sN,... in X, determine the least positive integer m satisfying (1/m) *Ra_LE Ra_abs(si) for all i greater than or equal to m, and then construct the regular sequence t whose first m components t1,t2,...,tm all equal Recip(sm *TIMES m *TIMES m) and whose subsequent components tN with m in N are defined as tN=Recip(sN *TIMES m *TIMES m): the desired reciprocal Y of X will be the real number to which t belongs.

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: S1 in regular_maps & S2 in regular_maps
       & T1 in regular_maps & T2 in regular_maps
       & Same_regmap(S1,S2) & Same_regmap(T1,T2)
    *imp
       Same_regmap({[n,Ra_abs(cdr(p)) *Ra_PLUS Ra_abs(cdr(q))]:
           n in Z, p in S1, q in T1
           | 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 S2, q in T2
           | next(n *PLUS n) = car(p) & car(p) = car(q)})
Analogously, for the real reciprocal operation, we need to know that 
* 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
       & M1 in Z & M2 in Z & M1 /= 0 & M2 /= 0
       & (FORALL p in S | M1 *Ra_LE next(car(p)) 
           *imp (1/M1 *Ra_LE Ra_abs(cdr(p))))
       & (FORALL p in S | M2 *Ra_LE next(car(p)) 
           *imp (1/M2 *Ra_LE Ra_abs(cdr(p)))) 
    *imp
       Same_regmap({[n, Recip(cdr(p))]: n in Z, p in S
           | next(car(p)) = (n+M1) *TIMES (M1 *TIMES M1)},
                      {[n, Recip(cdr(p))]: n in Z, p in S
           | next(car(p)) = (n+M2) *TIMES (M2 *TIMES M2)})
We also need to derive the algebraic properties of the basic operations on reals from the definitions given above, e.g. 
  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/k
This 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 m
we 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))/1
This 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_maps
so 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_maps
which 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 Re
follows 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 sn is a rational number.
If i and j are natural numbers, let r be the smaller number between si+(1/next(i)) and sj+(1/next(j)), neither of which belongs to d. Then we have si *Ra_LT r and sj *Ra_LT r, because d is downward closed and si, sj belong to d. Therefore, we have the following *Ra_LE-chain:
  Ra_abs(si *Ra_MINUS sj) *Ra_LE
    Ra_abs(si *Ra_MINUS r) *Ra_PLUS Ra_abs(r *Ra_MINUS sj)
  & Ra_abs(si *Ra_MINUS r) *Ra_PLUS Ra_abs(r *Ra_MINUS sj) =
    (r *Ra_MINUS si) *Ra_PLUS (r *Ra_MINUS sj)
  & (r *Ra_MINUS si) *Ra_PLUS (r *Ra_MINUS sj) *Ra_LE
    ((si *Ra_PLUS (1/next(i))) *Ra_MINUS si) *Ra_PLUS 
      (sj *Ra_PLUS (1/next(j))) *Ra_MINUS sj)
  & ((si *Ra_PLUS (1/next(i))) *Ra_MINUS si) *Ra_PLUS 
      (sj *Ra_PLUS (1/next(j))) *Ra_MINUS sj)=
        (1/next(i)) *Ra_PLUS (1/next(i))
completing the proof that the sequence is regular, QED

Proof of Theorem U: TO BE SUPPLIED, QED