| Name | Conclusion | Link |
|---|---|---|
| probability_1 | random_geometric = random_geometric_loop 0 | link to proof |
| probability_2 | random_bits = random_vector random_bit | link to proof |
| probability_3 | !r. mk_random (dest_random r) = r | link to proof |
| probability_4 | !s. dest_random (mk_random s) = s | link to proof |
| probability_5 | !b. ?r. random_bit r <=> b | link to proof |
| probability_6 | !r. random_bit r <=> shd (dest_random r) | link to proof |
| probability_7 | !n r. LENGTH (random_bits n r) = n | link to proof |
| probability_8 | !f r. random_vector f 0 r = [] | link to proof |
| probability_9 | !r1 r2. ?r. split_random r = r1,r2 | link to proof |
| probability_10 | !f n r. LENGTH (random_vector f n r) = n | link to proof |
| probability_11 | !n l. LENGTH l = n ==> (?r. random_bits n r = l) | link to proof |
| probability_12 | !f n l. ONTO f /\ LENGTH l = n ==> (?r. random_vector f n r = l) | link to proof |
| probability_13 | !r. split_random r = (let s1,s2 = ssplit (dest_random r) in mk_random s1,mk_random s2) | link to proof |
| probability_14 | !f r. random_geometric_list f r = (let r1,r2 = split_random r in random_vector f (random_geometric r1) r2) | link to proof |
| probability_15 | !n r. random_geometric_loop n r = (let r1,r2 = split_random r in if random_bit r1 then n else random_geometric_loop (SUC n) r2) | link to proof |
| probability_16 | !n r. random_geometric_loop n r = (let r1,r2 = split_random r in if random_bit r1 then n else random_geometric_loop (n + 1) r2) | link to proof |
| probability_17 | !f r n. random_vector f (SUC n) r = (let r1,r2 = split_random r in CONS (f r1) (random_vector f n r2)) | link to proof |
| probability_18 | !f n r. random_vector f n r = (if n = 0 then [] else let r1,r2 = split_random r in CONS (f r1) (random_vector f (n - 1) r2)) | link to proof |