beta_range_transport_entry

Exact expanded PA statement

forall b c z d a l. (forall ff_i_transport_l. (exists ff_lt_transport_l_bound. ff_lt_transport_l_bound + S ff_i_transport_l = l) -> (((exists ff_h_transport_l_decoded. ff_h_transport_l_decoded + S (a + ff_i_transport_l) = S ((S (ff_i_transport_l)) * c)) /\ exists ff_q_transport_l_decoded. b = ff_q_transport_l_decoded * S ((S (ff_i_transport_l)) * c) + (a + ff_i_transport_l)))) -> (forall ff_i_transport_r. (exists ff_lt_transport_r_bound. ff_lt_transport_r_bound + S ff_i_transport_r = l) -> (((exists ff_h_transport_r_decoded. ff_h_transport_r_decoded + S (a + ff_i_transport_r) = S ((S (ff_i_transport_r)) * d)) /\ exists ff_q_transport_r_decoded. z = ff_q_transport_r_decoded * S ((S (ff_i_transport_r)) * d) + (a + ff_i_transport_r)))) -> forall i x. (exists h. h + S i = l) -> (((exists ff_h_range_transport_x. ff_h_range_transport_x + S (x) = S ((S (i)) * c)) /\ exists ff_q_range_transport_x. b = ff_q_range_transport_x * S ((S (i)) * c) + (x))) -> (((exists ff_h_range_transport_y. ff_h_range_transport_y + S (x) = S ((S (i)) * d)) /\ exists ff_q_range_transport_y. z = ff_q_range_transport_y * S ((S (i)) * d) + (x)))