eisenstein_transposed_column_prefix_exists

Proof neighborhood

Direct dependencies

Direct dependents

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

1. 0001intro p
2. 0002intro q
3. 0003intro h
4. 0004intro bb
5. 0005intro bc
6. 0006intro i
7. 0007induction k
8. 0008intro hchoices
9. 0009exists 0
10. 0010exists 0
11. 0011intro j
12. 0012intro hj
13. 0013exfalso
14. 0014cases hj
15. 0015have hsj : S j = 0
16. 0016specialize add_eq_zero_right x
17. 0017specialize add_eq_zero_right (S j)
18. 0018apply add_eq_zero_right
19. 0019exact hj_witness
20. 0020specialize succ_ne_zero j
21. 0021apply succ_ne_zero
22. 0022exact hsj
23. 0023intro hchoices
24. 0024have hprevious_choices : forall etc_row_index_transposed_column_exists_previous_choices. (exists edt_lt_gap_transposed_column_exists_previous_choices_bound. edt_lt_gap_transposed_column_exists_previous_choices_bound + S (etc_row_index_transposed_column_exists_previous_choices) = k) -> exists etc_bit_transposed_column_exists_previous_choices. (exists etc_count_transposed_column_exists_previous_choices_witness etc_row_code_transposed_column_exists_previous_choices_witness etc_row_scale_transposed_column_exists_previous_choices_witness. ((((((exists ff_h_etc_transposed_column_exists_previous_choices_witness_outer_entry. ff_h_etc_transposed_column_exists_previous_choices_witness_outer_entry + S (etc_count_transposed_column_exists_previous_choices_witness) = S ((S (etc_row_index_transposed_column_exists_previous_choices)) * bc)) /\ exists ff_q_etc_transposed_column_exists_previous_choices_witness_outer_entry. bb = ff_q_etc_transposed_column_exists_previous_choices_witness_outer_entry * S ((S (etc_row_index_transposed_column_exists_previous_choices)) * bc) + (etc_count_transposed_column_exists_previous_choices_witness))) /\ (forall eri_column_etc_transposed_column_exists_previous_choices_witness_row. (exists eri_gap_etc_transposed_column_exists_previous_choices_witness_row_bound. eri_gap_etc_transposed_column_exists_previous_choices_witness_row_bound + S (eri_column_etc_transposed_column_exists_previous_choices_witness_row) = h) -> exists eri_bit_etc_transposed_column_exists_previous_choices_witness_row. ((((exists ff_h_eri_etc_transposed_column_exists_previous_choices_witness_row_decoded. ff_h_eri_etc_transposed_column_exists_previous_choices_witness_row_decoded + S (eri_bit_etc_transposed_column_exists_previous_choices_witness_row) = S ((S (eri_column_etc_transposed_column_exists_previous_choices_witness_row)) * etc_row_scale_transposed_column_exists_previous_choices_witness)) /\ exists ff_q_eri_etc_transposed_column_exists_previous_choices_witness_row_decoded. etc_row_code_transposed_column_exists_previous_choices_witness = ff_q_eri_etc_transposed_column_exists_previous_choices_witness_row_decoded * S ((S (eri_column_etc_transposed_column_exists_previous_choices_witness_row)) * etc_row_scale_transposed_column_exists_previous_choices_witness) + (eri_bit_etc_transposed_column_exists_previous_choices_witness_row))) /\ (((eri_bit_etc_transposed_column_exists_previous_choices_witness_row = 0 /\ ((exists eri_gap_etc_transposed_column_exists_previous_choices_witness_row_choice_left. eri_gap_etc_transposed_column_exists_previous_choices_witness_row_choice_left + S (p * S etc_row_index_transposed_column_exists_previous_choices) = q * S eri_column_etc_transposed_column_exists_previous_choices_witness_row) /\ ~(exists eri_gap_etc_transposed_column_exists_previous_choices_witness_row_choice_right. eri_gap_etc_transposed_column_exists_previous_choices_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_exists_previous_choices_witness_row) = p * S etc_row_index_transposed_column_exists_previous_choices))) \/ (eri_bit_etc_transposed_column_exists_previous_choices_witness_row = 1 /\ ((exists eri_gap_etc_transposed_column_exists_previous_choices_witness_row_choice_right. eri_gap_etc_transposed_column_exists_previous_choices_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_exists_previous_choices_witness_row) = p * S etc_row_index_transposed_column_exists_previous_choices) /\ ~(exists eri_gap_etc_transposed_column_exists_previous_choices_witness_row_choice_left. eri_gap_etc_transposed_column_exists_previous_choices_witness_row_choice_left + S (p * S etc_row_index_transposed_column_exists_previous_choices) = q * S eri_column_etc_transposed_column_exists_previous_choices_witness_row)))))))) /\ (((exists ff_u_etc_transposed_column_exists_previous_choices_witness_count_relation_sum ff_v_etc_transposed_column_exists_previous_choices_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_start. ff_h_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_transposed_column_exists_previous_choices_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_start. ff_u_etc_transposed_column_exists_previous_choices_witness_count_relation_sum = ff_q_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_transposed_column_exists_previous_choices_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_terminal. ff_h_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_terminal + S (etc_count_transposed_column_exists_previous_choices_witness) = S ((S (h)) * ff_v_etc_transposed_column_exists_previous_choices_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_terminal. ff_u_etc_transposed_column_exists_previous_choices_witness_count_relation_sum = ff_q_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_transposed_column_exists_previous_choices_witness_count_relation_sum) + (etc_count_transposed_column_exists_previous_choices_witness))) /\ forall ff_i_etc_transposed_column_exists_previous_choices_witness_count_relation_sum. (exists ff_lt_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_bound. ff_lt_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_bound + S ff_i_etc_transposed_column_exists_previous_choices_witness_count_relation_sum = h) -> exists ff_a_etc_transposed_column_exists_previous_choices_witness_count_relation_sum ff_r_etc_transposed_column_exists_previous_choices_witness_count_relation_sum ff_s_etc_transposed_column_exists_previous_choices_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_summand. ff_h_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_summand + S (ff_a_etc_transposed_column_exists_previous_choices_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_exists_previous_choices_witness_count_relation_sum)) * etc_row_scale_transposed_column_exists_previous_choices_witness)) /\ exists ff_q_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_summand. etc_row_code_transposed_column_exists_previous_choices_witness = ff_q_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_summand * S ((S (ff_i_etc_transposed_column_exists_previous_choices_witness_count_relation_sum)) * etc_row_scale_transposed_column_exists_previous_choices_witness) + (ff_a_etc_transposed_column_exists_previous_choices_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_partial. ff_h_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_partial + S (ff_r_etc_transposed_column_exists_previous_choices_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_exists_previous_choices_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_previous_choices_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_partial. ff_u_etc_transposed_column_exists_previous_choices_witness_count_relation_sum = ff_q_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_partial * S ((S (ff_i_etc_transposed_column_exists_previous_choices_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_previous_choices_witness_count_relation_sum) + (ff_r_etc_transposed_column_exists_previous_choices_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_successor. ff_h_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_successor + S (ff_s_etc_transposed_column_exists_previous_choices_witness_count_relation_sum) = S ((S (S ff_i_etc_transposed_column_exists_previous_choices_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_previous_choices_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_successor. ff_u_etc_transposed_column_exists_previous_choices_witness_count_relation_sum = ff_q_etc_transposed_column_exists_previous_choices_witness_count_relation_sum_successor * S ((S (S ff_i_etc_transposed_column_exists_previous_choices_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_previous_choices_witness_count_relation_sum) + (ff_s_etc_transposed_column_exists_previous_choices_witness_count_relation_sum))) /\ ff_s_etc_transposed_column_exists_previous_choices_witness_count_relation_sum = ff_r_etc_transposed_column_exists_previous_choices_witness_count_relation_sum + ff_a_etc_transposed_column_exists_previous_choices_witness_count_relation_sum)))))) /\ (forall ff_i_etc_transposed_column_exists_previous_choices_witness_count_relation_bits. (exists ff_lt_etc_transposed_column_exists_previous_choices_witness_count_relation_bits_bound. ff_lt_etc_transposed_column_exists_previous_choices_witness_count_relation_bits_bound + S ff_i_etc_transposed_column_exists_previous_choices_witness_count_relation_bits = h) -> exists ff_bit_etc_transposed_column_exists_previous_choices_witness_count_relation_bits. ((((exists ff_h_etc_transposed_column_exists_previous_choices_witness_count_relation_bits_decoded. ff_h_etc_transposed_column_exists_previous_choices_witness_count_relation_bits_decoded + S (ff_bit_etc_transposed_column_exists_previous_choices_witness_count_relation_bits) = S ((S (ff_i_etc_transposed_column_exists_previous_choices_witness_count_relation_bits)) * etc_row_scale_transposed_column_exists_previous_choices_witness)) /\ exists ff_q_etc_transposed_column_exists_previous_choices_witness_count_relation_bits_decoded. etc_row_code_transposed_column_exists_previous_choices_witness = ff_q_etc_transposed_column_exists_previous_choices_witness_count_relation_bits_decoded * S ((S (ff_i_etc_transposed_column_exists_previous_choices_witness_count_relation_bits)) * etc_row_scale_transposed_column_exists_previous_choices_witness) + (ff_bit_etc_transposed_column_exists_previous_choices_witness_count_relation_bits))) /\ (ff_bit_etc_transposed_column_exists_previous_choices_witness_count_relation_bits = 0 \/ ff_bit_etc_transposed_column_exists_previous_choices_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_transposed_column_exists_previous_choices_witness_inner_entry. ff_h_etc_transposed_column_exists_previous_choices_witness_inner_entry + S (etc_bit_transposed_column_exists_previous_choices) = S ((S (i)) * etc_row_scale_transposed_column_exists_previous_choices_witness)) /\ exists ff_q_etc_transposed_column_exists_previous_choices_witness_inner_entry. etc_row_code_transposed_column_exists_previous_choices_witness = ff_q_etc_transposed_column_exists_previous_choices_witness_inner_entry * S ((S (i)) * etc_row_scale_transposed_column_exists_previous_choices_witness) + (etc_bit_transposed_column_exists_previous_choices)))))
25. 0025intro j
26. 0026intro hj
27. 0027specialize hchoices j
28. 0028apply hchoices
29. 0029specialize le_succ (S j)
30. 0030specialize le_succ k
31. 0031apply le_succ
32. 0032exact hj
33. 0033have hprevious : exists z e. (forall etc_row_index_transposed_column_exists_previous_prefix. (exists edt_lt_gap_transposed_column_exists_previous_prefix_bound. edt_lt_gap_transposed_column_exists_previous_prefix_bound + S (etc_row_index_transposed_column_exists_previous_prefix) = k) -> exists etc_bit_transposed_column_exists_previous_prefix. ((((exists ff_h_etc_transposed_column_exists_previous_prefix_decoded. ff_h_etc_transposed_column_exists_previous_prefix_decoded + S (etc_bit_transposed_column_exists_previous_prefix) = S ((S (etc_row_index_transposed_column_exists_previous_prefix)) * e)) /\ exists ff_q_etc_transposed_column_exists_previous_prefix_decoded. z = ff_q_etc_transposed_column_exists_previous_prefix_decoded * S ((S (etc_row_index_transposed_column_exists_previous_prefix)) * e) + (etc_bit_transposed_column_exists_previous_prefix))) /\ (exists etc_count_transposed_column_exists_previous_prefix_witness etc_row_code_transposed_column_exists_previous_prefix_witness etc_row_scale_transposed_column_exists_previous_prefix_witness. ((((((exists ff_h_etc_transposed_column_exists_previous_prefix_witness_outer_entry. ff_h_etc_transposed_column_exists_previous_prefix_witness_outer_entry + S (etc_count_transposed_column_exists_previous_prefix_witness) = S ((S (etc_row_index_transposed_column_exists_previous_prefix)) * bc)) /\ exists ff_q_etc_transposed_column_exists_previous_prefix_witness_outer_entry. bb = ff_q_etc_transposed_column_exists_previous_prefix_witness_outer_entry * S ((S (etc_row_index_transposed_column_exists_previous_prefix)) * bc) + (etc_count_transposed_column_exists_previous_prefix_witness))) /\ (forall eri_column_etc_transposed_column_exists_previous_prefix_witness_row. (exists eri_gap_etc_transposed_column_exists_previous_prefix_witness_row_bound. eri_gap_etc_transposed_column_exists_previous_prefix_witness_row_bound + S (eri_column_etc_transposed_column_exists_previous_prefix_witness_row) = h) -> exists eri_bit_etc_transposed_column_exists_previous_prefix_witness_row. ((((exists ff_h_eri_etc_transposed_column_exists_previous_prefix_witness_row_decoded. ff_h_eri_etc_transposed_column_exists_previous_prefix_witness_row_decoded + S (eri_bit_etc_transposed_column_exists_previous_prefix_witness_row) = S ((S (eri_column_etc_transposed_column_exists_previous_prefix_witness_row)) * etc_row_scale_transposed_column_exists_previous_prefix_witness)) /\ exists ff_q_eri_etc_transposed_column_exists_previous_prefix_witness_row_decoded. etc_row_code_transposed_column_exists_previous_prefix_witness = ff_q_eri_etc_transposed_column_exists_previous_prefix_witness_row_decoded * S ((S (eri_column_etc_transposed_column_exists_previous_prefix_witness_row)) * etc_row_scale_transposed_column_exists_previous_prefix_witness) + (eri_bit_etc_transposed_column_exists_previous_prefix_witness_row))) /\ (((eri_bit_etc_transposed_column_exists_previous_prefix_witness_row = 0 /\ ((exists eri_gap_etc_transposed_column_exists_previous_prefix_witness_row_choice_left. eri_gap_etc_transposed_column_exists_previous_prefix_witness_row_choice_left + S (p * S etc_row_index_transposed_column_exists_previous_prefix) = q * S eri_column_etc_transposed_column_exists_previous_prefix_witness_row) /\ ~(exists eri_gap_etc_transposed_column_exists_previous_prefix_witness_row_choice_right. eri_gap_etc_transposed_column_exists_previous_prefix_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_exists_previous_prefix_witness_row) = p * S etc_row_index_transposed_column_exists_previous_prefix))) \/ (eri_bit_etc_transposed_column_exists_previous_prefix_witness_row = 1 /\ ((exists eri_gap_etc_transposed_column_exists_previous_prefix_witness_row_choice_right. eri_gap_etc_transposed_column_exists_previous_prefix_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_exists_previous_prefix_witness_row) = p * S etc_row_index_transposed_column_exists_previous_prefix) /\ ~(exists eri_gap_etc_transposed_column_exists_previous_prefix_witness_row_choice_left. eri_gap_etc_transposed_column_exists_previous_prefix_witness_row_choice_left + S (p * S etc_row_index_transposed_column_exists_previous_prefix) = q * S eri_column_etc_transposed_column_exists_previous_prefix_witness_row)))))))) /\ (((exists ff_u_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum ff_v_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_start. ff_h_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_start. ff_u_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum = ff_q_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_terminal. ff_h_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_terminal + S (etc_count_transposed_column_exists_previous_prefix_witness) = S ((S (h)) * ff_v_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_terminal. ff_u_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum = ff_q_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum) + (etc_count_transposed_column_exists_previous_prefix_witness))) /\ forall ff_i_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum. (exists ff_lt_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_bound. ff_lt_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_bound + S ff_i_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum = h) -> exists ff_a_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum ff_r_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum ff_s_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_summand. ff_h_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_summand + S (ff_a_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum)) * etc_row_scale_transposed_column_exists_previous_prefix_witness)) /\ exists ff_q_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_summand. etc_row_code_transposed_column_exists_previous_prefix_witness = ff_q_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_summand * S ((S (ff_i_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum)) * etc_row_scale_transposed_column_exists_previous_prefix_witness) + (ff_a_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_partial. ff_h_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_partial + S (ff_r_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_partial. ff_u_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum = ff_q_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_partial * S ((S (ff_i_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum) + (ff_r_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_successor. ff_h_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_successor + S (ff_s_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum) = S ((S (S ff_i_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_successor. ff_u_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum = ff_q_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum_successor * S ((S (S ff_i_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum) + (ff_s_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum))) /\ ff_s_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum = ff_r_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum + ff_a_etc_transposed_column_exists_previous_prefix_witness_count_relation_sum)))))) /\ (forall ff_i_etc_transposed_column_exists_previous_prefix_witness_count_relation_bits. (exists ff_lt_etc_transposed_column_exists_previous_prefix_witness_count_relation_bits_bound. ff_lt_etc_transposed_column_exists_previous_prefix_witness_count_relation_bits_bound + S ff_i_etc_transposed_column_exists_previous_prefix_witness_count_relation_bits = h) -> exists ff_bit_etc_transposed_column_exists_previous_prefix_witness_count_relation_bits. ((((exists ff_h_etc_transposed_column_exists_previous_prefix_witness_count_relation_bits_decoded. ff_h_etc_transposed_column_exists_previous_prefix_witness_count_relation_bits_decoded + S (ff_bit_etc_transposed_column_exists_previous_prefix_witness_count_relation_bits) = S ((S (ff_i_etc_transposed_column_exists_previous_prefix_witness_count_relation_bits)) * etc_row_scale_transposed_column_exists_previous_prefix_witness)) /\ exists ff_q_etc_transposed_column_exists_previous_prefix_witness_count_relation_bits_decoded. etc_row_code_transposed_column_exists_previous_prefix_witness = ff_q_etc_transposed_column_exists_previous_prefix_witness_count_relation_bits_decoded * S ((S (ff_i_etc_transposed_column_exists_previous_prefix_witness_count_relation_bits)) * etc_row_scale_transposed_column_exists_previous_prefix_witness) + (ff_bit_etc_transposed_column_exists_previous_prefix_witness_count_relation_bits))) /\ (ff_bit_etc_transposed_column_exists_previous_prefix_witness_count_relation_bits = 0 \/ ff_bit_etc_transposed_column_exists_previous_prefix_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_transposed_column_exists_previous_prefix_witness_inner_entry. ff_h_etc_transposed_column_exists_previous_prefix_witness_inner_entry + S (etc_bit_transposed_column_exists_previous_prefix) = S ((S (i)) * etc_row_scale_transposed_column_exists_previous_prefix_witness)) /\ exists ff_q_etc_transposed_column_exists_previous_prefix_witness_inner_entry. etc_row_code_transposed_column_exists_previous_prefix_witness = ff_q_etc_transposed_column_exists_previous_prefix_witness_inner_entry * S ((S (i)) * etc_row_scale_transposed_column_exists_previous_prefix_witness) + (etc_bit_transposed_column_exists_previous_prefix)))))))
34. 0034apply IH
35. 0035exact hprevious_choices
36. 0036cases hprevious
37. 0037cases hprevious_witness
38. 0038have hlast : exists d. (exists etc_count_transposed_column_exists_last etc_row_code_transposed_column_exists_last etc_row_scale_transposed_column_exists_last. ((((((exists ff_h_etc_transposed_column_exists_last_outer_entry. ff_h_etc_transposed_column_exists_last_outer_entry + S (etc_count_transposed_column_exists_last) = S ((S (k)) * bc)) /\ exists ff_q_etc_transposed_column_exists_last_outer_entry. bb = ff_q_etc_transposed_column_exists_last_outer_entry * S ((S (k)) * bc) + (etc_count_transposed_column_exists_last))) /\ (forall eri_column_etc_transposed_column_exists_last_row. (exists eri_gap_etc_transposed_column_exists_last_row_bound. eri_gap_etc_transposed_column_exists_last_row_bound + S (eri_column_etc_transposed_column_exists_last_row) = h) -> exists eri_bit_etc_transposed_column_exists_last_row. ((((exists ff_h_eri_etc_transposed_column_exists_last_row_decoded. ff_h_eri_etc_transposed_column_exists_last_row_decoded + S (eri_bit_etc_transposed_column_exists_last_row) = S ((S (eri_column_etc_transposed_column_exists_last_row)) * etc_row_scale_transposed_column_exists_last)) /\ exists ff_q_eri_etc_transposed_column_exists_last_row_decoded. etc_row_code_transposed_column_exists_last = ff_q_eri_etc_transposed_column_exists_last_row_decoded * S ((S (eri_column_etc_transposed_column_exists_last_row)) * etc_row_scale_transposed_column_exists_last) + (eri_bit_etc_transposed_column_exists_last_row))) /\ (((eri_bit_etc_transposed_column_exists_last_row = 0 /\ ((exists eri_gap_etc_transposed_column_exists_last_row_choice_left. eri_gap_etc_transposed_column_exists_last_row_choice_left + S (p * S k) = q * S eri_column_etc_transposed_column_exists_last_row) /\ ~(exists eri_gap_etc_transposed_column_exists_last_row_choice_right. eri_gap_etc_transposed_column_exists_last_row_choice_right + S (q * S eri_column_etc_transposed_column_exists_last_row) = p * S k))) \/ (eri_bit_etc_transposed_column_exists_last_row = 1 /\ ((exists eri_gap_etc_transposed_column_exists_last_row_choice_right. eri_gap_etc_transposed_column_exists_last_row_choice_right + S (q * S eri_column_etc_transposed_column_exists_last_row) = p * S k) /\ ~(exists eri_gap_etc_transposed_column_exists_last_row_choice_left. eri_gap_etc_transposed_column_exists_last_row_choice_left + S (p * S k) = q * S eri_column_etc_transposed_column_exists_last_row)))))))) /\ (((exists ff_u_etc_transposed_column_exists_last_count_relation_sum ff_v_etc_transposed_column_exists_last_count_relation_sum. ((((exists ff_h_etc_transposed_column_exists_last_count_relation_sum_start. ff_h_etc_transposed_column_exists_last_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_transposed_column_exists_last_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_last_count_relation_sum_start. ff_u_etc_transposed_column_exists_last_count_relation_sum = ff_q_etc_transposed_column_exists_last_count_relation_sum_start * S ((S (0)) * ff_v_etc_transposed_column_exists_last_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_transposed_column_exists_last_count_relation_sum_terminal. ff_h_etc_transposed_column_exists_last_count_relation_sum_terminal + S (etc_count_transposed_column_exists_last) = S ((S (h)) * ff_v_etc_transposed_column_exists_last_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_last_count_relation_sum_terminal. ff_u_etc_transposed_column_exists_last_count_relation_sum = ff_q_etc_transposed_column_exists_last_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_transposed_column_exists_last_count_relation_sum) + (etc_count_transposed_column_exists_last))) /\ forall ff_i_etc_transposed_column_exists_last_count_relation_sum. (exists ff_lt_etc_transposed_column_exists_last_count_relation_sum_bound. ff_lt_etc_transposed_column_exists_last_count_relation_sum_bound + S ff_i_etc_transposed_column_exists_last_count_relation_sum = h) -> exists ff_a_etc_transposed_column_exists_last_count_relation_sum ff_r_etc_transposed_column_exists_last_count_relation_sum ff_s_etc_transposed_column_exists_last_count_relation_sum. ((((exists ff_h_etc_transposed_column_exists_last_count_relation_sum_summand. ff_h_etc_transposed_column_exists_last_count_relation_sum_summand + S (ff_a_etc_transposed_column_exists_last_count_relation_sum) = S ((S (ff_i_etc_transposed_column_exists_last_count_relation_sum)) * etc_row_scale_transposed_column_exists_last)) /\ exists ff_q_etc_transposed_column_exists_last_count_relation_sum_summand. etc_row_code_transposed_column_exists_last = ff_q_etc_transposed_column_exists_last_count_relation_sum_summand * S ((S (ff_i_etc_transposed_column_exists_last_count_relation_sum)) * etc_row_scale_transposed_column_exists_last) + (ff_a_etc_transposed_column_exists_last_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_exists_last_count_relation_sum_partial. ff_h_etc_transposed_column_exists_last_count_relation_sum_partial + S (ff_r_etc_transposed_column_exists_last_count_relation_sum) = S ((S (ff_i_etc_transposed_column_exists_last_count_relation_sum)) * ff_v_etc_transposed_column_exists_last_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_last_count_relation_sum_partial. ff_u_etc_transposed_column_exists_last_count_relation_sum = ff_q_etc_transposed_column_exists_last_count_relation_sum_partial * S ((S (ff_i_etc_transposed_column_exists_last_count_relation_sum)) * ff_v_etc_transposed_column_exists_last_count_relation_sum) + (ff_r_etc_transposed_column_exists_last_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_exists_last_count_relation_sum_successor. ff_h_etc_transposed_column_exists_last_count_relation_sum_successor + S (ff_s_etc_transposed_column_exists_last_count_relation_sum) = S ((S (S ff_i_etc_transposed_column_exists_last_count_relation_sum)) * ff_v_etc_transposed_column_exists_last_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_last_count_relation_sum_successor. ff_u_etc_transposed_column_exists_last_count_relation_sum = ff_q_etc_transposed_column_exists_last_count_relation_sum_successor * S ((S (S ff_i_etc_transposed_column_exists_last_count_relation_sum)) * ff_v_etc_transposed_column_exists_last_count_relation_sum) + (ff_s_etc_transposed_column_exists_last_count_relation_sum))) /\ ff_s_etc_transposed_column_exists_last_count_relation_sum = ff_r_etc_transposed_column_exists_last_count_relation_sum + ff_a_etc_transposed_column_exists_last_count_relation_sum)))))) /\ (forall ff_i_etc_transposed_column_exists_last_count_relation_bits. (exists ff_lt_etc_transposed_column_exists_last_count_relation_bits_bound. ff_lt_etc_transposed_column_exists_last_count_relation_bits_bound + S ff_i_etc_transposed_column_exists_last_count_relation_bits = h) -> exists ff_bit_etc_transposed_column_exists_last_count_relation_bits. ((((exists ff_h_etc_transposed_column_exists_last_count_relation_bits_decoded. ff_h_etc_transposed_column_exists_last_count_relation_bits_decoded + S (ff_bit_etc_transposed_column_exists_last_count_relation_bits) = S ((S (ff_i_etc_transposed_column_exists_last_count_relation_bits)) * etc_row_scale_transposed_column_exists_last)) /\ exists ff_q_etc_transposed_column_exists_last_count_relation_bits_decoded. etc_row_code_transposed_column_exists_last = ff_q_etc_transposed_column_exists_last_count_relation_bits_decoded * S ((S (ff_i_etc_transposed_column_exists_last_count_relation_bits)) * etc_row_scale_transposed_column_exists_last) + (ff_bit_etc_transposed_column_exists_last_count_relation_bits))) /\ (ff_bit_etc_transposed_column_exists_last_count_relation_bits = 0 \/ ff_bit_etc_transposed_column_exists_last_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_transposed_column_exists_last_inner_entry. ff_h_etc_transposed_column_exists_last_inner_entry + S (d) = S ((S (i)) * etc_row_scale_transposed_column_exists_last)) /\ exists ff_q_etc_transposed_column_exists_last_inner_entry. etc_row_code_transposed_column_exists_last = ff_q_etc_transposed_column_exists_last_inner_entry * S ((S (i)) * etc_row_scale_transposed_column_exists_last) + (d)))))
39. 0039specialize hchoices k
40. 0040apply hchoices
41. 0041specialize le_refl (S k)
42. 0042exact le_refl
43. 0043have hnext : exists z e. (forall etc_row_index_transposed_column_exists_successor. (exists edt_lt_gap_transposed_column_exists_successor_bound. edt_lt_gap_transposed_column_exists_successor_bound + S (etc_row_index_transposed_column_exists_successor) = S k) -> exists etc_bit_transposed_column_exists_successor. ((((exists ff_h_etc_transposed_column_exists_successor_decoded. ff_h_etc_transposed_column_exists_successor_decoded + S (etc_bit_transposed_column_exists_successor) = S ((S (etc_row_index_transposed_column_exists_successor)) * e)) /\ exists ff_q_etc_transposed_column_exists_successor_decoded. z = ff_q_etc_transposed_column_exists_successor_decoded * S ((S (etc_row_index_transposed_column_exists_successor)) * e) + (etc_bit_transposed_column_exists_successor))) /\ (exists etc_count_transposed_column_exists_successor_witness etc_row_code_transposed_column_exists_successor_witness etc_row_scale_transposed_column_exists_successor_witness. ((((((exists ff_h_etc_transposed_column_exists_successor_witness_outer_entry. ff_h_etc_transposed_column_exists_successor_witness_outer_entry + S (etc_count_transposed_column_exists_successor_witness) = S ((S (etc_row_index_transposed_column_exists_successor)) * bc)) /\ exists ff_q_etc_transposed_column_exists_successor_witness_outer_entry. bb = ff_q_etc_transposed_column_exists_successor_witness_outer_entry * S ((S (etc_row_index_transposed_column_exists_successor)) * bc) + (etc_count_transposed_column_exists_successor_witness))) /\ (forall eri_column_etc_transposed_column_exists_successor_witness_row. (exists eri_gap_etc_transposed_column_exists_successor_witness_row_bound. eri_gap_etc_transposed_column_exists_successor_witness_row_bound + S (eri_column_etc_transposed_column_exists_successor_witness_row) = h) -> exists eri_bit_etc_transposed_column_exists_successor_witness_row. ((((exists ff_h_eri_etc_transposed_column_exists_successor_witness_row_decoded. ff_h_eri_etc_transposed_column_exists_successor_witness_row_decoded + S (eri_bit_etc_transposed_column_exists_successor_witness_row) = S ((S (eri_column_etc_transposed_column_exists_successor_witness_row)) * etc_row_scale_transposed_column_exists_successor_witness)) /\ exists ff_q_eri_etc_transposed_column_exists_successor_witness_row_decoded. etc_row_code_transposed_column_exists_successor_witness = ff_q_eri_etc_transposed_column_exists_successor_witness_row_decoded * S ((S (eri_column_etc_transposed_column_exists_successor_witness_row)) * etc_row_scale_transposed_column_exists_successor_witness) + (eri_bit_etc_transposed_column_exists_successor_witness_row))) /\ (((eri_bit_etc_transposed_column_exists_successor_witness_row = 0 /\ ((exists eri_gap_etc_transposed_column_exists_successor_witness_row_choice_left. eri_gap_etc_transposed_column_exists_successor_witness_row_choice_left + S (p * S etc_row_index_transposed_column_exists_successor) = q * S eri_column_etc_transposed_column_exists_successor_witness_row) /\ ~(exists eri_gap_etc_transposed_column_exists_successor_witness_row_choice_right. eri_gap_etc_transposed_column_exists_successor_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_exists_successor_witness_row) = p * S etc_row_index_transposed_column_exists_successor))) \/ (eri_bit_etc_transposed_column_exists_successor_witness_row = 1 /\ ((exists eri_gap_etc_transposed_column_exists_successor_witness_row_choice_right. eri_gap_etc_transposed_column_exists_successor_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_exists_successor_witness_row) = p * S etc_row_index_transposed_column_exists_successor) /\ ~(exists eri_gap_etc_transposed_column_exists_successor_witness_row_choice_left. eri_gap_etc_transposed_column_exists_successor_witness_row_choice_left + S (p * S etc_row_index_transposed_column_exists_successor) = q * S eri_column_etc_transposed_column_exists_successor_witness_row)))))))) /\ (((exists ff_u_etc_transposed_column_exists_successor_witness_count_relation_sum ff_v_etc_transposed_column_exists_successor_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_exists_successor_witness_count_relation_sum_start. ff_h_etc_transposed_column_exists_successor_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_transposed_column_exists_successor_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_successor_witness_count_relation_sum_start. ff_u_etc_transposed_column_exists_successor_witness_count_relation_sum = ff_q_etc_transposed_column_exists_successor_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_transposed_column_exists_successor_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_transposed_column_exists_successor_witness_count_relation_sum_terminal. ff_h_etc_transposed_column_exists_successor_witness_count_relation_sum_terminal + S (etc_count_transposed_column_exists_successor_witness) = S ((S (h)) * ff_v_etc_transposed_column_exists_successor_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_successor_witness_count_relation_sum_terminal. ff_u_etc_transposed_column_exists_successor_witness_count_relation_sum = ff_q_etc_transposed_column_exists_successor_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_transposed_column_exists_successor_witness_count_relation_sum) + (etc_count_transposed_column_exists_successor_witness))) /\ forall ff_i_etc_transposed_column_exists_successor_witness_count_relation_sum. (exists ff_lt_etc_transposed_column_exists_successor_witness_count_relation_sum_bound. ff_lt_etc_transposed_column_exists_successor_witness_count_relation_sum_bound + S ff_i_etc_transposed_column_exists_successor_witness_count_relation_sum = h) -> exists ff_a_etc_transposed_column_exists_successor_witness_count_relation_sum ff_r_etc_transposed_column_exists_successor_witness_count_relation_sum ff_s_etc_transposed_column_exists_successor_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_exists_successor_witness_count_relation_sum_summand. ff_h_etc_transposed_column_exists_successor_witness_count_relation_sum_summand + S (ff_a_etc_transposed_column_exists_successor_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_exists_successor_witness_count_relation_sum)) * etc_row_scale_transposed_column_exists_successor_witness)) /\ exists ff_q_etc_transposed_column_exists_successor_witness_count_relation_sum_summand. etc_row_code_transposed_column_exists_successor_witness = ff_q_etc_transposed_column_exists_successor_witness_count_relation_sum_summand * S ((S (ff_i_etc_transposed_column_exists_successor_witness_count_relation_sum)) * etc_row_scale_transposed_column_exists_successor_witness) + (ff_a_etc_transposed_column_exists_successor_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_exists_successor_witness_count_relation_sum_partial. ff_h_etc_transposed_column_exists_successor_witness_count_relation_sum_partial + S (ff_r_etc_transposed_column_exists_successor_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_exists_successor_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_successor_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_successor_witness_count_relation_sum_partial. ff_u_etc_transposed_column_exists_successor_witness_count_relation_sum = ff_q_etc_transposed_column_exists_successor_witness_count_relation_sum_partial * S ((S (ff_i_etc_transposed_column_exists_successor_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_successor_witness_count_relation_sum) + (ff_r_etc_transposed_column_exists_successor_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_exists_successor_witness_count_relation_sum_successor. ff_h_etc_transposed_column_exists_successor_witness_count_relation_sum_successor + S (ff_s_etc_transposed_column_exists_successor_witness_count_relation_sum) = S ((S (S ff_i_etc_transposed_column_exists_successor_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_successor_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_successor_witness_count_relation_sum_successor. ff_u_etc_transposed_column_exists_successor_witness_count_relation_sum = ff_q_etc_transposed_column_exists_successor_witness_count_relation_sum_successor * S ((S (S ff_i_etc_transposed_column_exists_successor_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_successor_witness_count_relation_sum) + (ff_s_etc_transposed_column_exists_successor_witness_count_relation_sum))) /\ ff_s_etc_transposed_column_exists_successor_witness_count_relation_sum = ff_r_etc_transposed_column_exists_successor_witness_count_relation_sum + ff_a_etc_transposed_column_exists_successor_witness_count_relation_sum)))))) /\ (forall ff_i_etc_transposed_column_exists_successor_witness_count_relation_bits. (exists ff_lt_etc_transposed_column_exists_successor_witness_count_relation_bits_bound. ff_lt_etc_transposed_column_exists_successor_witness_count_relation_bits_bound + S ff_i_etc_transposed_column_exists_successor_witness_count_relation_bits = h) -> exists ff_bit_etc_transposed_column_exists_successor_witness_count_relation_bits. ((((exists ff_h_etc_transposed_column_exists_successor_witness_count_relation_bits_decoded. ff_h_etc_transposed_column_exists_successor_witness_count_relation_bits_decoded + S (ff_bit_etc_transposed_column_exists_successor_witness_count_relation_bits) = S ((S (ff_i_etc_transposed_column_exists_successor_witness_count_relation_bits)) * etc_row_scale_transposed_column_exists_successor_witness)) /\ exists ff_q_etc_transposed_column_exists_successor_witness_count_relation_bits_decoded. etc_row_code_transposed_column_exists_successor_witness = ff_q_etc_transposed_column_exists_successor_witness_count_relation_bits_decoded * S ((S (ff_i_etc_transposed_column_exists_successor_witness_count_relation_bits)) * etc_row_scale_transposed_column_exists_successor_witness) + (ff_bit_etc_transposed_column_exists_successor_witness_count_relation_bits))) /\ (ff_bit_etc_transposed_column_exists_successor_witness_count_relation_bits = 0 \/ ff_bit_etc_transposed_column_exists_successor_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_transposed_column_exists_successor_witness_inner_entry. ff_h_etc_transposed_column_exists_successor_witness_inner_entry + S (etc_bit_transposed_column_exists_successor) = S ((S (i)) * etc_row_scale_transposed_column_exists_successor_witness)) /\ exists ff_q_etc_transposed_column_exists_successor_witness_inner_entry. etc_row_code_transposed_column_exists_successor_witness = ff_q_etc_transposed_column_exists_successor_witness_inner_entry * S ((S (i)) * etc_row_scale_transposed_column_exists_successor_witness) + (etc_bit_transposed_column_exists_successor)))))))
44. 0044specialize eisenstein_transposed_column_prefix_extend p
45. 0045specialize eisenstein_transposed_column_prefix_extend q
46. 0046specialize eisenstein_transposed_column_prefix_extend h
47. 0047specialize eisenstein_transposed_column_prefix_extend bb
48. 0048specialize eisenstein_transposed_column_prefix_extend bc
49. 0049specialize eisenstein_transposed_column_prefix_extend i
50. 0050specialize eisenstein_transposed_column_prefix_extend x
51. 0051specialize eisenstein_transposed_column_prefix_extend x1
52. 0052specialize eisenstein_transposed_column_prefix_extend k
53. 0053apply eisenstein_transposed_column_prefix_extend
54. 0054exact hprevious_witness_witness
55. 0055exact hlast
56. 0056exact hnext