eisenstein_fubini_column_count_witness_retarget

Exact expanded PA statement

forall p q hs ht bs cs bt ct i k n. (forall erc_row_fubini_total_retarget_outer. (exists erc_lt_gap_fubini_total_retarget_outer_bound. erc_lt_gap_fubini_total_retarget_outer_bound + S (erc_row_fubini_total_retarget_outer) = k) -> exists erc_count_fubini_total_retarget_outer. ((((exists ff_h_erc_fubini_total_retarget_outer_decoded. ff_h_erc_fubini_total_retarget_outer_decoded + S (erc_count_fubini_total_retarget_outer) = S ((S (erc_row_fubini_total_retarget_outer)) * ct)) /\ exists ff_q_erc_fubini_total_retarget_outer_decoded. bt = ff_q_erc_fubini_total_retarget_outer_decoded * S ((S (erc_row_fubini_total_retarget_outer)) * ct) + (erc_count_fubini_total_retarget_outer))) /\ (exists erc_row_code_fubini_total_retarget_outer_witness erc_row_scale_fubini_total_retarget_outer_witness. ((forall eri_column_erc_fubini_total_retarget_outer_witness_row. (exists eri_gap_erc_fubini_total_retarget_outer_witness_row_bound. eri_gap_erc_fubini_total_retarget_outer_witness_row_bound + S (eri_column_erc_fubini_total_retarget_outer_witness_row) = ht) -> exists eri_bit_erc_fubini_total_retarget_outer_witness_row. ((((exists ff_h_eri_erc_fubini_total_retarget_outer_witness_row_decoded. ff_h_eri_erc_fubini_total_retarget_outer_witness_row_decoded + S (eri_bit_erc_fubini_total_retarget_outer_witness_row) = S ((S (eri_column_erc_fubini_total_retarget_outer_witness_row)) * erc_row_scale_fubini_total_retarget_outer_witness)) /\ exists ff_q_eri_erc_fubini_total_retarget_outer_witness_row_decoded. erc_row_code_fubini_total_retarget_outer_witness = ff_q_eri_erc_fubini_total_retarget_outer_witness_row_decoded * S ((S (eri_column_erc_fubini_total_retarget_outer_witness_row)) * erc_row_scale_fubini_total_retarget_outer_witness) + (eri_bit_erc_fubini_total_retarget_outer_witness_row))) /\ (((eri_bit_erc_fubini_total_retarget_outer_witness_row = 0 /\ ((exists eri_gap_erc_fubini_total_retarget_outer_witness_row_choice_left. eri_gap_erc_fubini_total_retarget_outer_witness_row_choice_left + S (p * S erc_row_fubini_total_retarget_outer) = q * S eri_column_erc_fubini_total_retarget_outer_witness_row) /\ ~(exists eri_gap_erc_fubini_total_retarget_outer_witness_row_choice_right. eri_gap_erc_fubini_total_retarget_outer_witness_row_choice_right + S (q * S eri_column_erc_fubini_total_retarget_outer_witness_row) = p * S erc_row_fubini_total_retarget_outer))) \/ (eri_bit_erc_fubini_total_retarget_outer_witness_row = 1 /\ ((exists eri_gap_erc_fubini_total_retarget_outer_witness_row_choice_right. eri_gap_erc_fubini_total_retarget_outer_witness_row_choice_right + S (q * S eri_column_erc_fubini_total_retarget_outer_witness_row) = p * S erc_row_fubini_total_retarget_outer) /\ ~(exists eri_gap_erc_fubini_total_retarget_outer_witness_row_choice_left. eri_gap_erc_fubini_total_retarget_outer_witness_row_choice_left + S (p * S erc_row_fubini_total_retarget_outer) = q * S eri_column_erc_fubini_total_retarget_outer_witness_row))))))) /\ (((exists ff_u_erc_fubini_total_retarget_outer_witness_count_sum ff_v_erc_fubini_total_retarget_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_retarget_outer_witness_count_sum_start. ff_h_erc_fubini_total_retarget_outer_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_total_retarget_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_retarget_outer_witness_count_sum_start. ff_u_erc_fubini_total_retarget_outer_witness_count_sum = ff_q_erc_fubini_total_retarget_outer_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_total_retarget_outer_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_total_retarget_outer_witness_count_sum_terminal. ff_h_erc_fubini_total_retarget_outer_witness_count_sum_terminal + S (erc_count_fubini_total_retarget_outer) = S ((S (ht)) * ff_v_erc_fubini_total_retarget_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_retarget_outer_witness_count_sum_terminal. ff_u_erc_fubini_total_retarget_outer_witness_count_sum = ff_q_erc_fubini_total_retarget_outer_witness_count_sum_terminal * S ((S (ht)) * ff_v_erc_fubini_total_retarget_outer_witness_count_sum) + (erc_count_fubini_total_retarget_outer))) /\ forall ff_i_erc_fubini_total_retarget_outer_witness_count_sum. (exists ff_lt_erc_fubini_total_retarget_outer_witness_count_sum_bound. ff_lt_erc_fubini_total_retarget_outer_witness_count_sum_bound + S ff_i_erc_fubini_total_retarget_outer_witness_count_sum = ht) -> exists ff_a_erc_fubini_total_retarget_outer_witness_count_sum ff_r_erc_fubini_total_retarget_outer_witness_count_sum ff_s_erc_fubini_total_retarget_outer_witness_count_sum. ((((exists ff_h_erc_fubini_total_retarget_outer_witness_count_sum_summand. ff_h_erc_fubini_total_retarget_outer_witness_count_sum_summand + S (ff_a_erc_fubini_total_retarget_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_retarget_outer_witness_count_sum)) * erc_row_scale_fubini_total_retarget_outer_witness)) /\ exists ff_q_erc_fubini_total_retarget_outer_witness_count_sum_summand. erc_row_code_fubini_total_retarget_outer_witness = ff_q_erc_fubini_total_retarget_outer_witness_count_sum_summand * S ((S (ff_i_erc_fubini_total_retarget_outer_witness_count_sum)) * erc_row_scale_fubini_total_retarget_outer_witness) + (ff_a_erc_fubini_total_retarget_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_retarget_outer_witness_count_sum_partial. ff_h_erc_fubini_total_retarget_outer_witness_count_sum_partial + S (ff_r_erc_fubini_total_retarget_outer_witness_count_sum) = S ((S (ff_i_erc_fubini_total_retarget_outer_witness_count_sum)) * ff_v_erc_fubini_total_retarget_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_retarget_outer_witness_count_sum_partial. ff_u_erc_fubini_total_retarget_outer_witness_count_sum = ff_q_erc_fubini_total_retarget_outer_witness_count_sum_partial * S ((S (ff_i_erc_fubini_total_retarget_outer_witness_count_sum)) * ff_v_erc_fubini_total_retarget_outer_witness_count_sum) + (ff_r_erc_fubini_total_retarget_outer_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_total_retarget_outer_witness_count_sum_successor. ff_h_erc_fubini_total_retarget_outer_witness_count_sum_successor + S (ff_s_erc_fubini_total_retarget_outer_witness_count_sum) = S ((S (S ff_i_erc_fubini_total_retarget_outer_witness_count_sum)) * ff_v_erc_fubini_total_retarget_outer_witness_count_sum)) /\ exists ff_q_erc_fubini_total_retarget_outer_witness_count_sum_successor. ff_u_erc_fubini_total_retarget_outer_witness_count_sum = ff_q_erc_fubini_total_retarget_outer_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_total_retarget_outer_witness_count_sum)) * ff_v_erc_fubini_total_retarget_outer_witness_count_sum) + (ff_s_erc_fubini_total_retarget_outer_witness_count_sum))) /\ ff_s_erc_fubini_total_retarget_outer_witness_count_sum = ff_r_erc_fubini_total_retarget_outer_witness_count_sum + ff_a_erc_fubini_total_retarget_outer_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_total_retarget_outer_witness_count_bits. (exists ff_lt_erc_fubini_total_retarget_outer_witness_count_bits_bound. ff_lt_erc_fubini_total_retarget_outer_witness_count_bits_bound + S ff_i_erc_fubini_total_retarget_outer_witness_count_bits = ht) -> exists ff_bit_erc_fubini_total_retarget_outer_witness_count_bits. ((((exists ff_h_erc_fubini_total_retarget_outer_witness_count_bits_decoded. ff_h_erc_fubini_total_retarget_outer_witness_count_bits_decoded + S (ff_bit_erc_fubini_total_retarget_outer_witness_count_bits) = S ((S (ff_i_erc_fubini_total_retarget_outer_witness_count_bits)) * erc_row_scale_fubini_total_retarget_outer_witness)) /\ exists ff_q_erc_fubini_total_retarget_outer_witness_count_bits_decoded. erc_row_code_fubini_total_retarget_outer_witness = ff_q_erc_fubini_total_retarget_outer_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_total_retarget_outer_witness_count_bits)) * erc_row_scale_fubini_total_retarget_outer_witness) + (ff_bit_erc_fubini_total_retarget_outer_witness_count_bits))) /\ (ff_bit_erc_fubini_total_retarget_outer_witness_count_bits = 0 \/ ff_bit_erc_fubini_total_retarget_outer_witness_count_bits = 1))))))))) -> (exists edt_lt_gap_fubini_total_source_fixed_bound. edt_lt_gap_fubini_total_source_fixed_bound + S (i) = hs) -> (exists edt_lt_gap_fubini_total_target_fixed_bound. edt_lt_gap_fubini_total_target_fixed_bound + S (i) = ht) -> (exists eft_column_code_fubini_total_retarget_source eft_column_scale_fubini_total_retarget_source. ((forall etc_row_index_eft_fubini_total_retarget_source_column. (exists edt_lt_gap_eft_fubini_total_retarget_source_column_bound. edt_lt_gap_eft_fubini_total_retarget_source_column_bound + S (etc_row_index_eft_fubini_total_retarget_source_column) = k) -> exists etc_bit_eft_fubini_total_retarget_source_column. ((((exists ff_h_etc_eft_fubini_total_retarget_source_column_decoded. ff_h_etc_eft_fubini_total_retarget_source_column_decoded + S (etc_bit_eft_fubini_total_retarget_source_column) = S ((S (etc_row_index_eft_fubini_total_retarget_source_column)) * eft_column_scale_fubini_total_retarget_source)) /\ exists ff_q_etc_eft_fubini_total_retarget_source_column_decoded. eft_column_code_fubini_total_retarget_source = ff_q_etc_eft_fubini_total_retarget_source_column_decoded * S ((S (etc_row_index_eft_fubini_total_retarget_source_column)) * eft_column_scale_fubini_total_retarget_source) + (etc_bit_eft_fubini_total_retarget_source_column))) /\ (exists etc_count_eft_fubini_total_retarget_source_column_witness etc_row_code_eft_fubini_total_retarget_source_column_witness etc_row_scale_eft_fubini_total_retarget_source_column_witness. ((((((exists ff_h_etc_eft_fubini_total_retarget_source_column_witness_outer_entry. ff_h_etc_eft_fubini_total_retarget_source_column_witness_outer_entry + S (etc_count_eft_fubini_total_retarget_source_column_witness) = S ((S (etc_row_index_eft_fubini_total_retarget_source_column)) * cs)) /\ exists ff_q_etc_eft_fubini_total_retarget_source_column_witness_outer_entry. bs = ff_q_etc_eft_fubini_total_retarget_source_column_witness_outer_entry * S ((S (etc_row_index_eft_fubini_total_retarget_source_column)) * cs) + (etc_count_eft_fubini_total_retarget_source_column_witness))) /\ (forall eri_column_etc_eft_fubini_total_retarget_source_column_witness_row. (exists eri_gap_etc_eft_fubini_total_retarget_source_column_witness_row_bound. eri_gap_etc_eft_fubini_total_retarget_source_column_witness_row_bound + S (eri_column_etc_eft_fubini_total_retarget_source_column_witness_row) = hs) -> exists eri_bit_etc_eft_fubini_total_retarget_source_column_witness_row. ((((exists ff_h_eri_etc_eft_fubini_total_retarget_source_column_witness_row_decoded. ff_h_eri_etc_eft_fubini_total_retarget_source_column_witness_row_decoded + S (eri_bit_etc_eft_fubini_total_retarget_source_column_witness_row) = S ((S (eri_column_etc_eft_fubini_total_retarget_source_column_witness_row)) * etc_row_scale_eft_fubini_total_retarget_source_column_witness)) /\ exists ff_q_eri_etc_eft_fubini_total_retarget_source_column_witness_row_decoded. etc_row_code_eft_fubini_total_retarget_source_column_witness = ff_q_eri_etc_eft_fubini_total_retarget_source_column_witness_row_decoded * S ((S (eri_column_etc_eft_fubini_total_retarget_source_column_witness_row)) * etc_row_scale_eft_fubini_total_retarget_source_column_witness) + (eri_bit_etc_eft_fubini_total_retarget_source_column_witness_row))) /\ (((eri_bit_etc_eft_fubini_total_retarget_source_column_witness_row = 0 /\ ((exists eri_gap_etc_eft_fubini_total_retarget_source_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_retarget_source_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_retarget_source_column) = q * S eri_column_etc_eft_fubini_total_retarget_source_column_witness_row) /\ ~(exists eri_gap_etc_eft_fubini_total_retarget_source_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_retarget_source_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_retarget_source_column_witness_row) = p * S etc_row_index_eft_fubini_total_retarget_source_column))) \/ (eri_bit_etc_eft_fubini_total_retarget_source_column_witness_row = 1 /\ ((exists eri_gap_etc_eft_fubini_total_retarget_source_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_retarget_source_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_retarget_source_column_witness_row) = p * S etc_row_index_eft_fubini_total_retarget_source_column) /\ ~(exists eri_gap_etc_eft_fubini_total_retarget_source_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_retarget_source_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_retarget_source_column) = q * S eri_column_etc_eft_fubini_total_retarget_source_column_witness_row)))))))) /\ (((exists ff_u_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum ff_v_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_start. ff_h_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_start. ff_u_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_terminal. ff_h_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_terminal + S (etc_count_eft_fubini_total_retarget_source_column_witness) = S ((S (hs)) * ff_v_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_terminal. ff_u_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_terminal * S ((S (hs)) * ff_v_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum) + (etc_count_eft_fubini_total_retarget_source_column_witness))) /\ forall ff_i_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum. (exists ff_lt_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_bound. ff_lt_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_bound + S ff_i_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum = hs) -> exists ff_a_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum ff_r_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum ff_s_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_summand. ff_h_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_summand + S (ff_a_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_retarget_source_column_witness)) /\ exists ff_q_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_summand. etc_row_code_eft_fubini_total_retarget_source_column_witness = ff_q_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_retarget_source_column_witness) + (ff_a_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_partial. ff_h_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_partial + S (ff_r_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_partial. ff_u_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum) + (ff_r_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_successor. ff_h_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_successor + S (ff_s_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum) = S ((S (S ff_i_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_successor. ff_u_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum) + (ff_s_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum))) /\ ff_s_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum = ff_r_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum + ff_a_etc_eft_fubini_total_retarget_source_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_eft_fubini_total_retarget_source_column_witness_count_relation_bits. (exists ff_lt_etc_eft_fubini_total_retarget_source_column_witness_count_relation_bits_bound. ff_lt_etc_eft_fubini_total_retarget_source_column_witness_count_relation_bits_bound + S ff_i_etc_eft_fubini_total_retarget_source_column_witness_count_relation_bits = hs) -> exists ff_bit_etc_eft_fubini_total_retarget_source_column_witness_count_relation_bits. ((((exists ff_h_etc_eft_fubini_total_retarget_source_column_witness_count_relation_bits_decoded. ff_h_etc_eft_fubini_total_retarget_source_column_witness_count_relation_bits_decoded + S (ff_bit_etc_eft_fubini_total_retarget_source_column_witness_count_relation_bits) = S ((S (ff_i_etc_eft_fubini_total_retarget_source_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_retarget_source_column_witness)) /\ exists ff_q_etc_eft_fubini_total_retarget_source_column_witness_count_relation_bits_decoded. etc_row_code_eft_fubini_total_retarget_source_column_witness = ff_q_etc_eft_fubini_total_retarget_source_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_eft_fubini_total_retarget_source_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_retarget_source_column_witness) + (ff_bit_etc_eft_fubini_total_retarget_source_column_witness_count_relation_bits))) /\ (ff_bit_etc_eft_fubini_total_retarget_source_column_witness_count_relation_bits = 0 \/ ff_bit_etc_eft_fubini_total_retarget_source_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_eft_fubini_total_retarget_source_column_witness_inner_entry. ff_h_etc_eft_fubini_total_retarget_source_column_witness_inner_entry + S (etc_bit_eft_fubini_total_retarget_source_column) = S ((S (i)) * etc_row_scale_eft_fubini_total_retarget_source_column_witness)) /\ exists ff_q_etc_eft_fubini_total_retarget_source_column_witness_inner_entry. etc_row_code_eft_fubini_total_retarget_source_column_witness = ff_q_etc_eft_fubini_total_retarget_source_column_witness_inner_entry * S ((S (i)) * etc_row_scale_eft_fubini_total_retarget_source_column_witness) + (etc_bit_eft_fubini_total_retarget_source_column))))))) /\ (((exists ff_u_eft_fubini_total_retarget_source_count_sum ff_v_eft_fubini_total_retarget_source_count_sum. ((((exists ff_h_eft_fubini_total_retarget_source_count_sum_start. ff_h_eft_fubini_total_retarget_source_count_sum_start + S (0) = S ((S (0)) * ff_v_eft_fubini_total_retarget_source_count_sum)) /\ exists ff_q_eft_fubini_total_retarget_source_count_sum_start. ff_u_eft_fubini_total_retarget_source_count_sum = ff_q_eft_fubini_total_retarget_source_count_sum_start * S ((S (0)) * ff_v_eft_fubini_total_retarget_source_count_sum) + (0))) /\ ((((exists ff_h_eft_fubini_total_retarget_source_count_sum_terminal. ff_h_eft_fubini_total_retarget_source_count_sum_terminal + S (n) = S ((S (k)) * ff_v_eft_fubini_total_retarget_source_count_sum)) /\ exists ff_q_eft_fubini_total_retarget_source_count_sum_terminal. ff_u_eft_fubini_total_retarget_source_count_sum = ff_q_eft_fubini_total_retarget_source_count_sum_terminal * S ((S (k)) * ff_v_eft_fubini_total_retarget_source_count_sum) + (n))) /\ forall ff_i_eft_fubini_total_retarget_source_count_sum. (exists ff_lt_eft_fubini_total_retarget_source_count_sum_bound. ff_lt_eft_fubini_total_retarget_source_count_sum_bound + S ff_i_eft_fubini_total_retarget_source_count_sum = k) -> exists ff_a_eft_fubini_total_retarget_source_count_sum ff_r_eft_fubini_total_retarget_source_count_sum ff_s_eft_fubini_total_retarget_source_count_sum. ((((exists ff_h_eft_fubini_total_retarget_source_count_sum_summand. ff_h_eft_fubini_total_retarget_source_count_sum_summand + S (ff_a_eft_fubini_total_retarget_source_count_sum) = S ((S (ff_i_eft_fubini_total_retarget_source_count_sum)) * eft_column_scale_fubini_total_retarget_source)) /\ exists ff_q_eft_fubini_total_retarget_source_count_sum_summand. eft_column_code_fubini_total_retarget_source = ff_q_eft_fubini_total_retarget_source_count_sum_summand * S ((S (ff_i_eft_fubini_total_retarget_source_count_sum)) * eft_column_scale_fubini_total_retarget_source) + (ff_a_eft_fubini_total_retarget_source_count_sum))) /\ ((((exists ff_h_eft_fubini_total_retarget_source_count_sum_partial. ff_h_eft_fubini_total_retarget_source_count_sum_partial + S (ff_r_eft_fubini_total_retarget_source_count_sum) = S ((S (ff_i_eft_fubini_total_retarget_source_count_sum)) * ff_v_eft_fubini_total_retarget_source_count_sum)) /\ exists ff_q_eft_fubini_total_retarget_source_count_sum_partial. ff_u_eft_fubini_total_retarget_source_count_sum = ff_q_eft_fubini_total_retarget_source_count_sum_partial * S ((S (ff_i_eft_fubini_total_retarget_source_count_sum)) * ff_v_eft_fubini_total_retarget_source_count_sum) + (ff_r_eft_fubini_total_retarget_source_count_sum))) /\ ((((exists ff_h_eft_fubini_total_retarget_source_count_sum_successor. ff_h_eft_fubini_total_retarget_source_count_sum_successor + S (ff_s_eft_fubini_total_retarget_source_count_sum) = S ((S (S ff_i_eft_fubini_total_retarget_source_count_sum)) * ff_v_eft_fubini_total_retarget_source_count_sum)) /\ exists ff_q_eft_fubini_total_retarget_source_count_sum_successor. ff_u_eft_fubini_total_retarget_source_count_sum = ff_q_eft_fubini_total_retarget_source_count_sum_successor * S ((S (S ff_i_eft_fubini_total_retarget_source_count_sum)) * ff_v_eft_fubini_total_retarget_source_count_sum) + (ff_s_eft_fubini_total_retarget_source_count_sum))) /\ ff_s_eft_fubini_total_retarget_source_count_sum = ff_r_eft_fubini_total_retarget_source_count_sum + ff_a_eft_fubini_total_retarget_source_count_sum)))))) /\ (forall ff_i_eft_fubini_total_retarget_source_count_bits. (exists ff_lt_eft_fubini_total_retarget_source_count_bits_bound. ff_lt_eft_fubini_total_retarget_source_count_bits_bound + S ff_i_eft_fubini_total_retarget_source_count_bits = k) -> exists ff_bit_eft_fubini_total_retarget_source_count_bits. ((((exists ff_h_eft_fubini_total_retarget_source_count_bits_decoded. ff_h_eft_fubini_total_retarget_source_count_bits_decoded + S (ff_bit_eft_fubini_total_retarget_source_count_bits) = S ((S (ff_i_eft_fubini_total_retarget_source_count_bits)) * eft_column_scale_fubini_total_retarget_source)) /\ exists ff_q_eft_fubini_total_retarget_source_count_bits_decoded. eft_column_code_fubini_total_retarget_source = ff_q_eft_fubini_total_retarget_source_count_bits_decoded * S ((S (ff_i_eft_fubini_total_retarget_source_count_bits)) * eft_column_scale_fubini_total_retarget_source) + (ff_bit_eft_fubini_total_retarget_source_count_bits))) /\ (ff_bit_eft_fubini_total_retarget_source_count_bits = 0 \/ ff_bit_eft_fubini_total_retarget_source_count_bits = 1))))))) -> (exists eft_column_code_fubini_total_retarget_target eft_column_scale_fubini_total_retarget_target. ((forall etc_row_index_eft_fubini_total_retarget_target_column. (exists edt_lt_gap_eft_fubini_total_retarget_target_column_bound. edt_lt_gap_eft_fubini_total_retarget_target_column_bound + S (etc_row_index_eft_fubini_total_retarget_target_column) = k) -> exists etc_bit_eft_fubini_total_retarget_target_column. ((((exists ff_h_etc_eft_fubini_total_retarget_target_column_decoded. ff_h_etc_eft_fubini_total_retarget_target_column_decoded + S (etc_bit_eft_fubini_total_retarget_target_column) = S ((S (etc_row_index_eft_fubini_total_retarget_target_column)) * eft_column_scale_fubini_total_retarget_target)) /\ exists ff_q_etc_eft_fubini_total_retarget_target_column_decoded. eft_column_code_fubini_total_retarget_target = ff_q_etc_eft_fubini_total_retarget_target_column_decoded * S ((S (etc_row_index_eft_fubini_total_retarget_target_column)) * eft_column_scale_fubini_total_retarget_target) + (etc_bit_eft_fubini_total_retarget_target_column))) /\ (exists etc_count_eft_fubini_total_retarget_target_column_witness etc_row_code_eft_fubini_total_retarget_target_column_witness etc_row_scale_eft_fubini_total_retarget_target_column_witness. ((((((exists ff_h_etc_eft_fubini_total_retarget_target_column_witness_outer_entry. ff_h_etc_eft_fubini_total_retarget_target_column_witness_outer_entry + S (etc_count_eft_fubini_total_retarget_target_column_witness) = S ((S (etc_row_index_eft_fubini_total_retarget_target_column)) * ct)) /\ exists ff_q_etc_eft_fubini_total_retarget_target_column_witness_outer_entry. bt = ff_q_etc_eft_fubini_total_retarget_target_column_witness_outer_entry * S ((S (etc_row_index_eft_fubini_total_retarget_target_column)) * ct) + (etc_count_eft_fubini_total_retarget_target_column_witness))) /\ (forall eri_column_etc_eft_fubini_total_retarget_target_column_witness_row. (exists eri_gap_etc_eft_fubini_total_retarget_target_column_witness_row_bound. eri_gap_etc_eft_fubini_total_retarget_target_column_witness_row_bound + S (eri_column_etc_eft_fubini_total_retarget_target_column_witness_row) = ht) -> exists eri_bit_etc_eft_fubini_total_retarget_target_column_witness_row. ((((exists ff_h_eri_etc_eft_fubini_total_retarget_target_column_witness_row_decoded. ff_h_eri_etc_eft_fubini_total_retarget_target_column_witness_row_decoded + S (eri_bit_etc_eft_fubini_total_retarget_target_column_witness_row) = S ((S (eri_column_etc_eft_fubini_total_retarget_target_column_witness_row)) * etc_row_scale_eft_fubini_total_retarget_target_column_witness)) /\ exists ff_q_eri_etc_eft_fubini_total_retarget_target_column_witness_row_decoded. etc_row_code_eft_fubini_total_retarget_target_column_witness = ff_q_eri_etc_eft_fubini_total_retarget_target_column_witness_row_decoded * S ((S (eri_column_etc_eft_fubini_total_retarget_target_column_witness_row)) * etc_row_scale_eft_fubini_total_retarget_target_column_witness) + (eri_bit_etc_eft_fubini_total_retarget_target_column_witness_row))) /\ (((eri_bit_etc_eft_fubini_total_retarget_target_column_witness_row = 0 /\ ((exists eri_gap_etc_eft_fubini_total_retarget_target_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_retarget_target_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_retarget_target_column) = q * S eri_column_etc_eft_fubini_total_retarget_target_column_witness_row) /\ ~(exists eri_gap_etc_eft_fubini_total_retarget_target_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_retarget_target_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_retarget_target_column_witness_row) = p * S etc_row_index_eft_fubini_total_retarget_target_column))) \/ (eri_bit_etc_eft_fubini_total_retarget_target_column_witness_row = 1 /\ ((exists eri_gap_etc_eft_fubini_total_retarget_target_column_witness_row_choice_right. eri_gap_etc_eft_fubini_total_retarget_target_column_witness_row_choice_right + S (q * S eri_column_etc_eft_fubini_total_retarget_target_column_witness_row) = p * S etc_row_index_eft_fubini_total_retarget_target_column) /\ ~(exists eri_gap_etc_eft_fubini_total_retarget_target_column_witness_row_choice_left. eri_gap_etc_eft_fubini_total_retarget_target_column_witness_row_choice_left + S (p * S etc_row_index_eft_fubini_total_retarget_target_column) = q * S eri_column_etc_eft_fubini_total_retarget_target_column_witness_row)))))))) /\ (((exists ff_u_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum ff_v_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_start. ff_h_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_start. ff_u_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_terminal. ff_h_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_terminal + S (etc_count_eft_fubini_total_retarget_target_column_witness) = S ((S (ht)) * ff_v_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_terminal. ff_u_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_terminal * S ((S (ht)) * ff_v_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum) + (etc_count_eft_fubini_total_retarget_target_column_witness))) /\ forall ff_i_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum. (exists ff_lt_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_bound. ff_lt_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_bound + S ff_i_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum = ht) -> exists ff_a_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum ff_r_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum ff_s_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum. ((((exists ff_h_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_summand. ff_h_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_summand + S (ff_a_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_retarget_target_column_witness)) /\ exists ff_q_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_summand. etc_row_code_eft_fubini_total_retarget_target_column_witness = ff_q_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum)) * etc_row_scale_eft_fubini_total_retarget_target_column_witness) + (ff_a_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_partial. ff_h_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_partial + S (ff_r_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum) = S ((S (ff_i_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_partial. ff_u_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum) + (ff_r_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_successor. ff_h_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_successor + S (ff_s_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum) = S ((S (S ff_i_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum)) /\ exists ff_q_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_successor. ff_u_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum = ff_q_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum)) * ff_v_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum) + (ff_s_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum))) /\ ff_s_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum = ff_r_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum + ff_a_etc_eft_fubini_total_retarget_target_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_eft_fubini_total_retarget_target_column_witness_count_relation_bits. (exists ff_lt_etc_eft_fubini_total_retarget_target_column_witness_count_relation_bits_bound. ff_lt_etc_eft_fubini_total_retarget_target_column_witness_count_relation_bits_bound + S ff_i_etc_eft_fubini_total_retarget_target_column_witness_count_relation_bits = ht) -> exists ff_bit_etc_eft_fubini_total_retarget_target_column_witness_count_relation_bits. ((((exists ff_h_etc_eft_fubini_total_retarget_target_column_witness_count_relation_bits_decoded. ff_h_etc_eft_fubini_total_retarget_target_column_witness_count_relation_bits_decoded + S (ff_bit_etc_eft_fubini_total_retarget_target_column_witness_count_relation_bits) = S ((S (ff_i_etc_eft_fubini_total_retarget_target_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_retarget_target_column_witness)) /\ exists ff_q_etc_eft_fubini_total_retarget_target_column_witness_count_relation_bits_decoded. etc_row_code_eft_fubini_total_retarget_target_column_witness = ff_q_etc_eft_fubini_total_retarget_target_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_eft_fubini_total_retarget_target_column_witness_count_relation_bits)) * etc_row_scale_eft_fubini_total_retarget_target_column_witness) + (ff_bit_etc_eft_fubini_total_retarget_target_column_witness_count_relation_bits))) /\ (ff_bit_etc_eft_fubini_total_retarget_target_column_witness_count_relation_bits = 0 \/ ff_bit_etc_eft_fubini_total_retarget_target_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_eft_fubini_total_retarget_target_column_witness_inner_entry. ff_h_etc_eft_fubini_total_retarget_target_column_witness_inner_entry + S (etc_bit_eft_fubini_total_retarget_target_column) = S ((S (i)) * etc_row_scale_eft_fubini_total_retarget_target_column_witness)) /\ exists ff_q_etc_eft_fubini_total_retarget_target_column_witness_inner_entry. etc_row_code_eft_fubini_total_retarget_target_column_witness = ff_q_etc_eft_fubini_total_retarget_target_column_witness_inner_entry * S ((S (i)) * etc_row_scale_eft_fubini_total_retarget_target_column_witness) + (etc_bit_eft_fubini_total_retarget_target_column))))))) /\ (((exists ff_u_eft_fubini_total_retarget_target_count_sum ff_v_eft_fubini_total_retarget_target_count_sum. ((((exists ff_h_eft_fubini_total_retarget_target_count_sum_start. ff_h_eft_fubini_total_retarget_target_count_sum_start + S (0) = S ((S (0)) * ff_v_eft_fubini_total_retarget_target_count_sum)) /\ exists ff_q_eft_fubini_total_retarget_target_count_sum_start. ff_u_eft_fubini_total_retarget_target_count_sum = ff_q_eft_fubini_total_retarget_target_count_sum_start * S ((S (0)) * ff_v_eft_fubini_total_retarget_target_count_sum) + (0))) /\ ((((exists ff_h_eft_fubini_total_retarget_target_count_sum_terminal. ff_h_eft_fubini_total_retarget_target_count_sum_terminal + S (n) = S ((S (k)) * ff_v_eft_fubini_total_retarget_target_count_sum)) /\ exists ff_q_eft_fubini_total_retarget_target_count_sum_terminal. ff_u_eft_fubini_total_retarget_target_count_sum = ff_q_eft_fubini_total_retarget_target_count_sum_terminal * S ((S (k)) * ff_v_eft_fubini_total_retarget_target_count_sum) + (n))) /\ forall ff_i_eft_fubini_total_retarget_target_count_sum. (exists ff_lt_eft_fubini_total_retarget_target_count_sum_bound. ff_lt_eft_fubini_total_retarget_target_count_sum_bound + S ff_i_eft_fubini_total_retarget_target_count_sum = k) -> exists ff_a_eft_fubini_total_retarget_target_count_sum ff_r_eft_fubini_total_retarget_target_count_sum ff_s_eft_fubini_total_retarget_target_count_sum. ((((exists ff_h_eft_fubini_total_retarget_target_count_sum_summand. ff_h_eft_fubini_total_retarget_target_count_sum_summand + S (ff_a_eft_fubini_total_retarget_target_count_sum) = S ((S (ff_i_eft_fubini_total_retarget_target_count_sum)) * eft_column_scale_fubini_total_retarget_target)) /\ exists ff_q_eft_fubini_total_retarget_target_count_sum_summand. eft_column_code_fubini_total_retarget_target = ff_q_eft_fubini_total_retarget_target_count_sum_summand * S ((S (ff_i_eft_fubini_total_retarget_target_count_sum)) * eft_column_scale_fubini_total_retarget_target) + (ff_a_eft_fubini_total_retarget_target_count_sum))) /\ ((((exists ff_h_eft_fubini_total_retarget_target_count_sum_partial. ff_h_eft_fubini_total_retarget_target_count_sum_partial + S (ff_r_eft_fubini_total_retarget_target_count_sum) = S ((S (ff_i_eft_fubini_total_retarget_target_count_sum)) * ff_v_eft_fubini_total_retarget_target_count_sum)) /\ exists ff_q_eft_fubini_total_retarget_target_count_sum_partial. ff_u_eft_fubini_total_retarget_target_count_sum = ff_q_eft_fubini_total_retarget_target_count_sum_partial * S ((S (ff_i_eft_fubini_total_retarget_target_count_sum)) * ff_v_eft_fubini_total_retarget_target_count_sum) + (ff_r_eft_fubini_total_retarget_target_count_sum))) /\ ((((exists ff_h_eft_fubini_total_retarget_target_count_sum_successor. ff_h_eft_fubini_total_retarget_target_count_sum_successor + S (ff_s_eft_fubini_total_retarget_target_count_sum) = S ((S (S ff_i_eft_fubini_total_retarget_target_count_sum)) * ff_v_eft_fubini_total_retarget_target_count_sum)) /\ exists ff_q_eft_fubini_total_retarget_target_count_sum_successor. ff_u_eft_fubini_total_retarget_target_count_sum = ff_q_eft_fubini_total_retarget_target_count_sum_successor * S ((S (S ff_i_eft_fubini_total_retarget_target_count_sum)) * ff_v_eft_fubini_total_retarget_target_count_sum) + (ff_s_eft_fubini_total_retarget_target_count_sum))) /\ ff_s_eft_fubini_total_retarget_target_count_sum = ff_r_eft_fubini_total_retarget_target_count_sum + ff_a_eft_fubini_total_retarget_target_count_sum)))))) /\ (forall ff_i_eft_fubini_total_retarget_target_count_bits. (exists ff_lt_eft_fubini_total_retarget_target_count_bits_bound. ff_lt_eft_fubini_total_retarget_target_count_bits_bound + S ff_i_eft_fubini_total_retarget_target_count_bits = k) -> exists ff_bit_eft_fubini_total_retarget_target_count_bits. ((((exists ff_h_eft_fubini_total_retarget_target_count_bits_decoded. ff_h_eft_fubini_total_retarget_target_count_bits_decoded + S (ff_bit_eft_fubini_total_retarget_target_count_bits) = S ((S (ff_i_eft_fubini_total_retarget_target_count_bits)) * eft_column_scale_fubini_total_retarget_target)) /\ exists ff_q_eft_fubini_total_retarget_target_count_bits_decoded. eft_column_code_fubini_total_retarget_target = ff_q_eft_fubini_total_retarget_target_count_bits_decoded * S ((S (ff_i_eft_fubini_total_retarget_target_count_bits)) * eft_column_scale_fubini_total_retarget_target) + (ff_bit_eft_fubini_total_retarget_target_count_bits))) /\ (ff_bit_eft_fubini_total_retarget_target_count_bits = 0 \/ ff_bit_eft_fubini_total_retarget_target_count_bits = 1)))))))