[[[[[
   Show that a real r is Solovay random
   iff it is Martin-Lof random.

   An effective covering A_k of k is a function
   of k that enumerates bit strings s,
   which are the initial bits of the covered
   reals.  We assume that no s in A_k is a
   proper prefix or extension of another.
   Thus the measure of the cover A_k of k is
   exactly Sum_{s in A_k} of 2^{-|s|},
   where |s| is the length of the bit string s.
]]]]]

[First part: not M-L random ===> not Solovay random] 

[
This is immediate.  We are given coverings A_k such
that real r is in A_k for all k and the measure of A_k <= 2^{-k}.
It follows immediately that r is in infinitely many of the
A_k and the sum of the measure of A_k summed over all k converges.
Thus r is not Solovay random.
]

[Second part: not Solovay random ===> not M-L random] 

[
Suppose that a real r is in infinitely many of the 
coverings A_n and that Sum_k mu A_n <= 2^c.
Consider B_k defined as the set of all reals that are
in at least 2^{k+c} of the A_n.
Then r is in all of the B_k and the measure of 
B_k is <= 2^{-k}, so r is not Martin-Lof random.

Now let's program this!

Instead, I'll program B_k which is the set of all reals
that are in at least k of the A_n.
The proof then results from considering B_{2^{k+c}} .

The main function has two parameters, the stage n, and
the number of times something has to be repeated to
be taken into account.  At stage n, with number 
of repeats r, we look at A_0 through A_n for time n,
and put into our condensed result cover only subintervals
that are covered at least r times.

The key auxiliary function given n generates A_0 through A_n for time n,
then expands all intervals to the same max length and counts how
many times each is repeated.  Then it is easy to select those that
are covered the requisite number of times.

First step is to run A_0 through A_n for time n and append the results.
Then we get the max length and do a binary tree walk.  We start with
s and see if it's a prefix of at least r things.
If so, s will be in our result, and we backtrack.
If not, if s has max length, we stop recursion.
Otherwise, we look at s0 and at s1.
And we start with s = nil.
This gives our covering at stage n,
then we have to eliminate overlaps to
get our final result.
]

[ 
 Test case: A_n is defined to be the set of
 all natural numbers greater than n,
 where k is represented as k 1's followed by a 0.
 Then measure of A_n is 2^{-n-1}, and
 1=10 is in one of the A_n, 2=110 is in two of them,
 3=1110 is in three of them, etc.

 I.e., 1=10 is only in A_0,
       2=110 is only in A_0 & A_1,
       3=1110 is only in A_0 A_1 & A_2, etc.

 In this case the total measure of the A_n is 
 1/2 + 1/4 + 1/8 + ... = 1.
 For the proof in general, all we know is that
 this total measure converges to a finite sum, not 1.
]
define (A n) [displays infinite set 1^k 0, k > n] 
  let (loop k)
      cons display 
         append base10-to-2 - ^ 2 k 1 [2^k - 1 = k 1's]
            cons 0 nil [followed by a 0 bit]
      (loop + k 1)
  (loop + n 1) 

[now put together in one list stage n of A_0 through A_n]
define (sum n)
   let (loop k sum)
      if > k n sum
      (loop + k 1 
            append caddr try n cons cons "' cons A nil cons k nil nil
                   sum)
   (loop 0 nil)

[
 (count x y) 
 Now count how many times something x is contained in / 
 is an extension of an element of y
]
define (count x y) 
   if atom y 0
   if (is-prefix-of? car y x) + 1 (count x cdr y)
   (count x cdr y)

define (is-prefix-of? x y) [is bit string x a prefix of bit string y?]
   if atom x  true
   if atom y  false
   if = car x car y (is-prefix-of? cdr x cdr y)
   false

[get maximum length of a list of bit strings]
define (max-length list) 
   if atom list   0
   let len1 length car list
   let len2 (max-length cdr list)
   if > len1 len2   
      [then] len1 
      [else] len2 

[
 Now we get what (sum n) covers with multiplicity >= k.
 The measure of the multiplicity k covering will
 be bounded by the finite total measure (here 1) divided by k.
]

define (exceeds-count n k)
   let sum-n (sum n)
   let max-length-sum-n (max-length sum-n)
   (look-at nil)

[
 This routine has free parameters sum-n, max-length-sum-n, k.
 It gets us the MINIMAL multiplicity >= k covering for (sum n)!
]
define (look-at x) [produces strings x covered with multiplicity >= k in (sum n)]
   if = length x max-length-sum-n
      let n (count x sum-n)
      if >= n k cons x nil [found an interval x that is covered >= k times]
                nil  [didn't find an interval x that is covered >= k times]
   [otherwise break x into subintervals]
   let x0 append x cons 0 nil
   let x1 append x cons 1 nil
   let v  append (look-at x0)
                 (look-at x1)
   [consolidate subintervals?]
   if = v cons x0 cons x1 nil [yes!] cons x nil
          [no, leave covering as is] v

[
 Now we put this all together into B_k, which is
 the limit as n goes to infinity of (exceeds-count n k),
 k fixed, n --> infinity.

 I.e., B_k is what A_0, A_1, A_2, ... covers with
 multiplicity >= k.

 Thus the measure of B_k will be bounded by the
 total measure of the A_n (if it exists) divided by k.

 The main problem is to avoid overlaps in B_k,
 which we do using a completely general algorithm.
]

[list of intervals in covering so far]
[used to avoid overlapping intervals in covering]
define intervals ()

define (process-all x) [process list of intervals x]
   if atom x  intervals
   let intervals append (process car x) intervals
   (process-all cdr x)

define (process interval) [process individual interval]
   if (new-interval-covered-by-previous-one? interval intervals) 
      [then don't need to repeat it]
      nil
   let holes (new-interval-covers-previous-ones interval intervals)
   if atom holes
      [then interval is fine as is]
      [output it with display!]
      cons display interval nil 
   [get max granularity needed]
   let max (max-length holes) 
   [convert everything to same granularity]
   let holes (extend-all holes max)
   [and remove overlap]
   [subtract will output residue with display]
   (subtract (extend interval max) holes)

[returns true/false]
define (new-interval-covered-by-previous-one? interval intervals)
   if atom intervals  false
   if (is-prefix-of? car intervals interval)  true
   (new-interval-covered-by-previous-one? interval cdr intervals)

[returns set of previous intervals covered by this one]
define (new-interval-covers-previous-ones interval intervals)
   if atom intervals  nil
   if (is-prefix-of? interval car intervals)
      [then] cons car intervals (new-interval-covers-previous-ones interval cdr intervals)
      [else]                    (new-interval-covers-previous-ones interval cdr intervals)
   
[produce set of all extensions of a given bit string to a given length]
[(assumed >= to its current length)]
define (extend bit-string len)
   if = len length bit-string   
      [has correct length; return singleton set]
      cons bit-string nil
   append (extend append bit-string cons 0 nil len)
          (extend append bit-string cons 1 nil len)

[extend all the bit strings in a given list to the same length]
define (extend-all list len)
   if atom list   nil
   append (extend     car list len)
          (extend-all cdr list len)

[subtract set of intervals y from set of intervals x]
[output residue with display!]
define (subtract x y)
   if atom x   nil    
   if (is-in? car x y)
   [then]                    (subtract cdr x y)
   [else] cons display car x (subtract cdr x y)

define (is-in? x l) [is x an element of list l?]
   if atom l     false
   if = x car l  true
   (is-in? x cdr l)

[
 Put it all together---Here is cover B_k,
 which is what is covered by A_0, A_1, A_2, ...
 with multiplicity >= k, and therefore has
 measure bounded by the total measure of the A_n
 divided by k.
 Supposing that this total measure is <= 2^c
 and considering B_{2^{k+c}}, 
 we see that if a real r is in infinitely many of
 the A_n, then it will be in all of the 
 B_{2^{k+c}}, each of which has measure <= 1/2^k.
 Hence if a real r is not Solovay random,
 it follows that it will not be M-L random.
 Here we write the code for B_k, not for
 B_{2^{k+c}}.
]
define (B k)
   let intervals nil
   let (stage n)
      if = n 6 stop! [to stop test run---remove if real thing]
      let exceed-count (exceeds-count n k)
      let intervals (process-all exceed-count) 
      (stage + 1 n)
   [go!!!!!]
   (stage 0)

[k = multiplicity = repeated/covered 2 or more times in the A_n]
(B 2)