beta_sum_transport_prefix

Exact expanded PA statement

forall b c z e l n. (exists ff_u_transport_source ff_v_transport_source. ((((exists ff_h_transport_source_start. ff_h_transport_source_start + S (0) = S ((S (0)) * ff_v_transport_source)) /\ exists ff_q_transport_source_start. ff_u_transport_source = ff_q_transport_source_start * S ((S (0)) * ff_v_transport_source) + (0))) /\ ((((exists ff_h_transport_source_terminal. ff_h_transport_source_terminal + S (n) = S ((S (l)) * ff_v_transport_source)) /\ exists ff_q_transport_source_terminal. ff_u_transport_source = ff_q_transport_source_terminal * S ((S (l)) * ff_v_transport_source) + (n))) /\ forall ff_i_transport_source. (exists ff_lt_transport_source_bound. ff_lt_transport_source_bound + S ff_i_transport_source = l) -> exists ff_a_transport_source ff_r_transport_source ff_s_transport_source. ((((exists ff_h_transport_source_summand. ff_h_transport_source_summand + S (ff_a_transport_source) = S ((S (ff_i_transport_source)) * c)) /\ exists ff_q_transport_source_summand. b = ff_q_transport_source_summand * S ((S (ff_i_transport_source)) * c) + (ff_a_transport_source))) /\ ((((exists ff_h_transport_source_partial. ff_h_transport_source_partial + S (ff_r_transport_source) = S ((S (ff_i_transport_source)) * ff_v_transport_source)) /\ exists ff_q_transport_source_partial. ff_u_transport_source = ff_q_transport_source_partial * S ((S (ff_i_transport_source)) * ff_v_transport_source) + (ff_r_transport_source))) /\ ((((exists ff_h_transport_source_successor. ff_h_transport_source_successor + S (ff_s_transport_source) = S ((S (S ff_i_transport_source)) * ff_v_transport_source)) /\ exists ff_q_transport_source_successor. ff_u_transport_source = ff_q_transport_source_successor * S ((S (S ff_i_transport_source)) * ff_v_transport_source) + (ff_s_transport_source))) /\ ff_s_transport_source = ff_r_transport_source + ff_a_transport_source)))))) -> (forall i a. (exists h. h + S i = l) -> (((exists ff_h_transport_source_entry. ff_h_transport_source_entry + S (a) = S ((S (i)) * c)) /\ exists ff_q_transport_source_entry. b = ff_q_transport_source_entry * S ((S (i)) * c) + (a))) -> (((exists ff_h_transport_target_entry. ff_h_transport_target_entry + S (a) = S ((S (i)) * e)) /\ exists ff_q_transport_target_entry. z = ff_q_transport_target_entry * S ((S (i)) * e) + (a)))) -> (exists ff_u_transport_target ff_v_transport_target. ((((exists ff_h_transport_target_start. ff_h_transport_target_start + S (0) = S ((S (0)) * ff_v_transport_target)) /\ exists ff_q_transport_target_start. ff_u_transport_target = ff_q_transport_target_start * S ((S (0)) * ff_v_transport_target) + (0))) /\ ((((exists ff_h_transport_target_terminal. ff_h_transport_target_terminal + S (n) = S ((S (l)) * ff_v_transport_target)) /\ exists ff_q_transport_target_terminal. ff_u_transport_target = ff_q_transport_target_terminal * S ((S (l)) * ff_v_transport_target) + (n))) /\ forall ff_i_transport_target. (exists ff_lt_transport_target_bound. ff_lt_transport_target_bound + S ff_i_transport_target = l) -> exists ff_a_transport_target ff_r_transport_target ff_s_transport_target. ((((exists ff_h_transport_target_summand. ff_h_transport_target_summand + S (ff_a_transport_target) = S ((S (ff_i_transport_target)) * e)) /\ exists ff_q_transport_target_summand. z = ff_q_transport_target_summand * S ((S (ff_i_transport_target)) * e) + (ff_a_transport_target))) /\ ((((exists ff_h_transport_target_partial. ff_h_transport_target_partial + S (ff_r_transport_target) = S ((S (ff_i_transport_target)) * ff_v_transport_target)) /\ exists ff_q_transport_target_partial. ff_u_transport_target = ff_q_transport_target_partial * S ((S (ff_i_transport_target)) * ff_v_transport_target) + (ff_r_transport_target))) /\ ((((exists ff_h_transport_target_successor. ff_h_transport_target_successor + S (ff_s_transport_target) = S ((S (S ff_i_transport_target)) * ff_v_transport_target)) /\ exists ff_q_transport_target_successor. ff_u_transport_target = ff_q_transport_target_successor * S ((S (S ff_i_transport_target)) * ff_v_transport_target) + (ff_s_transport_target))) /\ ff_s_transport_target = ff_r_transport_target + ff_a_transport_target))))))