eisenstein_transposed_decoded_cell_bits_complementary

Exact expanded PA statement

forall p q h k i j rb rc cb cc a d. (forall eri_column_transpose_row. (exists eri_gap_transpose_row_bound. eri_gap_transpose_row_bound + S (eri_column_transpose_row) = k) -> exists eri_bit_transpose_row. ((((exists ff_h_eri_transpose_row_decoded. ff_h_eri_transpose_row_decoded + S (eri_bit_transpose_row) = S ((S (eri_column_transpose_row)) * rc)) /\ exists ff_q_eri_transpose_row_decoded. rb = ff_q_eri_transpose_row_decoded * S ((S (eri_column_transpose_row)) * rc) + (eri_bit_transpose_row))) /\ (((eri_bit_transpose_row = 0 /\ ((exists eri_gap_transpose_row_choice_left. eri_gap_transpose_row_choice_left + S (q * S i) = p * S eri_column_transpose_row) /\ ~(exists eri_gap_transpose_row_choice_right. eri_gap_transpose_row_choice_right + S (p * S eri_column_transpose_row) = q * S i))) \/ (eri_bit_transpose_row = 1 /\ ((exists eri_gap_transpose_row_choice_right. eri_gap_transpose_row_choice_right + S (p * S eri_column_transpose_row) = q * S i) /\ ~(exists eri_gap_transpose_row_choice_left. eri_gap_transpose_row_choice_left + S (q * S i) = p * S eri_column_transpose_row))))))) -> (forall eri_column_transpose_column. (exists eri_gap_transpose_column_bound. eri_gap_transpose_column_bound + S (eri_column_transpose_column) = h) -> exists eri_bit_transpose_column. ((((exists ff_h_eri_transpose_column_decoded. ff_h_eri_transpose_column_decoded + S (eri_bit_transpose_column) = S ((S (eri_column_transpose_column)) * cc)) /\ exists ff_q_eri_transpose_column_decoded. cb = ff_q_eri_transpose_column_decoded * S ((S (eri_column_transpose_column)) * cc) + (eri_bit_transpose_column))) /\ (((eri_bit_transpose_column = 0 /\ ((exists eri_gap_transpose_column_choice_left. eri_gap_transpose_column_choice_left + S (p * S j) = q * S eri_column_transpose_column) /\ ~(exists eri_gap_transpose_column_choice_right. eri_gap_transpose_column_choice_right + S (q * S eri_column_transpose_column) = p * S j))) \/ (eri_bit_transpose_column = 1 /\ ((exists eri_gap_transpose_column_choice_right. eri_gap_transpose_column_choice_right + S (q * S eri_column_transpose_column) = p * S j) /\ ~(exists eri_gap_transpose_column_choice_left. eri_gap_transpose_column_choice_left + S (p * S j) = q * S eri_column_transpose_column))))))) -> (exists gap. gap + S j = k) -> (exists gap. gap + S i = h) -> (((exists ff_h_transpose_row_entry. ff_h_transpose_row_entry + S (a) = S ((S (j)) * rc)) /\ exists ff_q_transpose_row_entry. rb = ff_q_transpose_row_entry * S ((S (j)) * rc) + (a))) -> (((exists ff_h_transpose_column_entry. ff_h_transpose_column_entry + S (d) = S ((S (i)) * cc)) /\ exists ff_q_transpose_column_entry. cb = ff_q_transpose_column_entry * S ((S (i)) * cc) + (d))) -> ((a = 0 /\ d = 1) \/ (a = 1 /\ d = 0))