eisenstein_transposed_column_pointwise_complement

forall p q h k i rb rc bb bc z e j a d. (forall eri_column_transposed_column_original_row. (exists eri_gap_transposed_column_original_row_bound. eri_gap_transposed_column_original_row_bound + S (eri_column_transposed_column_original_row) = k) -> exists eri_bit_transposed_column_original_row. ((((exists ff_h_eri_transposed_column_original_row_decoded. ff_h_eri_transposed_column_original_row_decoded + S (eri_bit_transposed_column_original_row) = S ((S (eri_column_transposed_column_original_row)) * rc)) /\ exists ff_q_eri_transposed_column_original_row_decoded. rb = ff_q_eri_transposed_column_original_row_decoded * S ((S (eri_column_transposed_column_original_row)) * rc) + (eri_bit_transposed_column_original_row))) /\ (((eri_bit_transposed_column_original_row = 0 /\ ((exists eri_gap_transposed_column_original_row_choice_left. eri_gap_transposed_column_original_row_choice_left + S (q * S i) = p * S eri_column_transposed_column_original_row) /\ ~(exists eri_gap_transposed_column_original_row_choice_right. eri_gap_transposed_column_original_row_choice_right + S (p * S eri_column_transposed_column_original_row) = q * S i))) \/ (eri_bit_transposed_column_original_row = 1 /\ ((exists eri_gap_transposed_column_original_row_choice_right. eri_gap_transposed_column_original_row_choice_right + S (p * S eri_column_transposed_column_original_row) = q * S i) /\ ~(exists eri_gap_transposed_column_original_row_choice_left. eri_gap_transposed_column_original_row_choice_left + S (q * S i) = p * S eri_column_transposed_column_original_row))))))) -> (forall etc_row_index_transposed_column_semantic_prefix. (exists edt_lt_gap_transposed_column_semantic_prefix_bound. edt_lt_gap_transposed_column_semantic_prefix_bound + S (etc_row_index_transposed_column_semantic_prefix) = k) -> exists etc_bit_transposed_column_semantic_prefix. ((((exists ff_h_etc_transposed_column_semantic_prefix_decoded. ff_h_etc_transposed_column_semantic_prefix_decoded + S (etc_bit_transposed_column_semantic_prefix) = S ((S (etc_row_index_transposed_column_semantic_prefix)) * e)) /\ exists ff_q_etc_transposed_column_semantic_prefix_decoded. z = ff_q_etc_transposed_column_semantic_prefix_decoded * S ((S (etc_row_index_transposed_column_semantic_prefix)) * e) + (etc_bit_transposed_column_semantic_prefix))) /\ (exists etc_count_transposed_column_semantic_prefix_witness etc_row_code_transposed_column_semantic_prefix_witness etc_row_scale_transposed_column_semantic_prefix_witness. ((((((exists ff_h_etc_transposed_column_semantic_prefix_witness_outer_entry. ff_h_etc_transposed_column_semantic_prefix_witness_outer_entry + S (etc_count_transposed_column_semantic_prefix_witness) = S ((S (etc_row_index_transposed_column_semantic_prefix)) * bc)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_outer_entry. bb = ff_q_etc_transposed_column_semantic_prefix_witness_outer_entry * S ((S (etc_row_index_transposed_column_semantic_prefix)) * bc) + (etc_count_transposed_column_semantic_prefix_witness))) /\ (forall eri_column_etc_transposed_column_semantic_prefix_witness_row. (exists eri_gap_etc_transposed_column_semantic_prefix_witness_row_bound. eri_gap_etc_transposed_column_semantic_prefix_witness_row_bound + S (eri_column_etc_transposed_column_semantic_prefix_witness_row) = h) -> exists eri_bit_etc_transposed_column_semantic_prefix_witness_row. ((((exists ff_h_eri_etc_transposed_column_semantic_prefix_witness_row_decoded. ff_h_eri_etc_transposed_column_semantic_prefix_witness_row_decoded + S (eri_bit_etc_transposed_column_semantic_prefix_witness_row) = S ((S (eri_column_etc_transposed_column_semantic_prefix_witness_row)) * etc_row_scale_transposed_column_semantic_prefix_witness)) /\ exists ff_q_eri_etc_transposed_column_semantic_prefix_witness_row_decoded. etc_row_code_transposed_column_semantic_prefix_witness = ff_q_eri_etc_transposed_column_semantic_prefix_witness_row_decoded * S ((S (eri_column_etc_transposed_column_semantic_prefix_witness_row)) * etc_row_scale_transposed_column_semantic_prefix_witness) + (eri_bit_etc_transposed_column_semantic_prefix_witness_row))) /\ (((eri_bit_etc_transposed_column_semantic_prefix_witness_row = 0 /\ ((exists eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_left. eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_left + S (p * S etc_row_index_transposed_column_semantic_prefix) = q * S eri_column_etc_transposed_column_semantic_prefix_witness_row) /\ ~(exists eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_right. eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_semantic_prefix_witness_row) = p * S etc_row_index_transposed_column_semantic_prefix))) \/ (eri_bit_etc_transposed_column_semantic_prefix_witness_row = 1 /\ ((exists eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_right. eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_semantic_prefix_witness_row) = p * S etc_row_index_transposed_column_semantic_prefix) /\ ~(exists eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_left. eri_gap_etc_transposed_column_semantic_prefix_witness_row_choice_left + S (p * S etc_row_index_transposed_column_semantic_prefix) = q * S eri_column_etc_transposed_column_semantic_prefix_witness_row)))))))) /\ (((exists ff_u_etc_transposed_column_semantic_prefix_witness_count_relation_sum ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_start. ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_start. ff_u_etc_transposed_column_semantic_prefix_witness_count_relation_sum = ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_terminal. ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_terminal + S (etc_count_transposed_column_semantic_prefix_witness) = S ((S (h)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_terminal. ff_u_etc_transposed_column_semantic_prefix_witness_count_relation_sum = ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum) + (etc_count_transposed_column_semantic_prefix_witness))) /\ forall ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum. (exists ff_lt_etc_transposed_column_semantic_prefix_witness_count_relation_sum_bound. ff_lt_etc_transposed_column_semantic_prefix_witness_count_relation_sum_bound + S ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum = h) -> exists ff_a_etc_transposed_column_semantic_prefix_witness_count_relation_sum ff_r_etc_transposed_column_semantic_prefix_witness_count_relation_sum ff_s_etc_transposed_column_semantic_prefix_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_summand. ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_summand + S (ff_a_etc_transposed_column_semantic_prefix_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) * etc_row_scale_transposed_column_semantic_prefix_witness)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_summand. etc_row_code_transposed_column_semantic_prefix_witness = ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_summand * S ((S (ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) * etc_row_scale_transposed_column_semantic_prefix_witness) + (ff_a_etc_transposed_column_semantic_prefix_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_partial. ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_partial + S (ff_r_etc_transposed_column_semantic_prefix_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_partial. ff_u_etc_transposed_column_semantic_prefix_witness_count_relation_sum = ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_partial * S ((S (ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum) + (ff_r_etc_transposed_column_semantic_prefix_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_successor. ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_sum_successor + S (ff_s_etc_transposed_column_semantic_prefix_witness_count_relation_sum) = S ((S (S ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_successor. ff_u_etc_transposed_column_semantic_prefix_witness_count_relation_sum = ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_sum_successor * S ((S (S ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_sum)) * ff_v_etc_transposed_column_semantic_prefix_witness_count_relation_sum) + (ff_s_etc_transposed_column_semantic_prefix_witness_count_relation_sum))) /\ ff_s_etc_transposed_column_semantic_prefix_witness_count_relation_sum = ff_r_etc_transposed_column_semantic_prefix_witness_count_relation_sum + ff_a_etc_transposed_column_semantic_prefix_witness_count_relation_sum)))))) /\ (forall ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_bits. (exists ff_lt_etc_transposed_column_semantic_prefix_witness_count_relation_bits_bound. ff_lt_etc_transposed_column_semantic_prefix_witness_count_relation_bits_bound + S ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_bits = h) -> exists ff_bit_etc_transposed_column_semantic_prefix_witness_count_relation_bits. ((((exists ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_bits_decoded. ff_h_etc_transposed_column_semantic_prefix_witness_count_relation_bits_decoded + S (ff_bit_etc_transposed_column_semantic_prefix_witness_count_relation_bits) = S ((S (ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_bits)) * etc_row_scale_transposed_column_semantic_prefix_witness)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_bits_decoded. etc_row_code_transposed_column_semantic_prefix_witness = ff_q_etc_transposed_column_semantic_prefix_witness_count_relation_bits_decoded * S ((S (ff_i_etc_transposed_column_semantic_prefix_witness_count_relation_bits)) * etc_row_scale_transposed_column_semantic_prefix_witness) + (ff_bit_etc_transposed_column_semantic_prefix_witness_count_relation_bits))) /\ (ff_bit_etc_transposed_column_semantic_prefix_witness_count_relation_bits = 0 \/ ff_bit_etc_transposed_column_semantic_prefix_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_transposed_column_semantic_prefix_witness_inner_entry. ff_h_etc_transposed_column_semantic_prefix_witness_inner_entry + S (etc_bit_transposed_column_semantic_prefix) = S ((S (i)) * etc_row_scale_transposed_column_semantic_prefix_witness)) /\ exists ff_q_etc_transposed_column_semantic_prefix_witness_inner_entry. etc_row_code_transposed_column_semantic_prefix_witness = ff_q_etc_transposed_column_semantic_prefix_witness_inner_entry * S ((S (i)) * etc_row_scale_transposed_column_semantic_prefix_witness) + (etc_bit_transposed_column_semantic_prefix))))))) -> (exists edt_lt_gap_transposed_column_fixed_bound. edt_lt_gap_transposed_column_fixed_bound + S (i) = h) -> (exists edt_lt_gap_transposed_column_pointwise_bound. edt_lt_gap_transposed_column_pointwise_bound + S (j) = k) -> (((exists ff_h_transposed_column_row_entry. ff_h_transposed_column_row_entry + S (a) = S ((S (j)) * rc)) /\ exists ff_q_transposed_column_row_entry. rb = ff_q_transposed_column_row_entry * S ((S (j)) * rc) + (a))) -> (((exists ff_h_transposed_column_column_entry. ff_h_transposed_column_column_entry + S (d) = S ((S (j)) * e)) /\ exists ff_q_transposed_column_column_entry. z = ff_q_transposed_column_column_entry * S ((S (j)) * e) + (d))) -> ((a = 0 /\ d = 1) \/ (a = 1 /\ d = 0))