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 |