Function balanced_approach 

pub fn balanced_approach(width: u32, jam: u64, backlog: u64) -> String

A queue with a starting backlog and service that exceeds arrivals: it only ever drains, so it provably never reaches jam — for all reachable states (k-induction).