321 (coin) Repeatedly flip a coin until you get a head. Prove that it takes n flips with probability 2–n . With an appropriate definition of R , the program is
R ⇐ t:=t+1. ifrand2thenokelseRfi
§ Starting with the right side, using 1/2 for rand 2 and (tʹ′>t) × 2t–tʹ′ for R :
t:= t+1. if 1/2 then tʹ′=t else (tʹ′>t) × 2t–tʹ′ fi
= if 1/2 then tʹ′=t+1 else (tʹ′>t+1) × 2t+1–tʹ′ fi
= (tʹ′=t+1) / 2 + (tʹ′>t+1) × 2t+1–tʹ′ / 2 = (tʹ′=t+1) × 2t–tʹ′ + (tʹ′>t+1) × 2t–tʹ′
= (tʹ′>t) × 2t–tʹ′ =R
substitution law replace if