eisenstein_transposed_column_count_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 k
5. 0005intro ab
6. 0006intro ac
7. 0007intro bb
8. 0008intro bc
9. 0009induction l
10. 0010intro hchoices
11. 0011exists 0
12. 0012exists 0
13. 0013intro i
14. 0014intro hi
15. 0015exfalso
16. 0016cases hi
17. 0017have hsi : S i = 0
18. 0018specialize add_eq_zero_right x
19. 0019specialize add_eq_zero_right (S i)
20. 0020apply add_eq_zero_right
21. 0021exact hi_witness
22. 0022specialize succ_ne_zero i
23. 0023apply succ_ne_zero
24. 0024exact hsi
25. 0025intro hchoices
26. 0026have hprevious : forall etcc_row_index_column_count_exists_previous_choices. (exists edt_lt_gap_column_count_exists_previous_choices_bound. edt_lt_gap_column_count_exists_previous_choices_bound + S (etcc_row_index_column_count_exists_previous_choices) = l) -> exists etcc_count_column_count_exists_previous_choices. (exists etcc_row_count_column_count_exists_previous_choices_witness etcc_column_code_column_count_exists_previous_choices_witness etcc_column_scale_column_count_exists_previous_choices_witness. ((((((exists ff_h_etcc_column_count_exists_previous_choices_witness_first_entry. ff_h_etcc_column_count_exists_previous_choices_witness_first_entry + S (etcc_row_count_column_count_exists_previous_choices_witness) = S ((S (etcc_row_index_column_count_exists_previous_choices)) * ac)) /\ exists ff_q_etcc_column_count_exists_previous_choices_witness_first_entry. ab = ff_q_etcc_column_count_exists_previous_choices_witness_first_entry * S ((S (etcc_row_index_column_count_exists_previous_choices)) * ac) + (etcc_row_count_column_count_exists_previous_choices_witness))) /\ (exists erc_row_code_etcc_column_count_exists_previous_choices_witness_row_semantics erc_row_scale_etcc_column_count_exists_previous_choices_witness_row_semantics. ((forall eri_column_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row. (exists eri_gap_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row_bound. eri_gap_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row_bound + S (eri_column_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row) = k) -> exists eri_bit_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row. ((((exists ff_h_eri_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row_decoded. ff_h_eri_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row_decoded + S (eri_bit_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row) = S ((S (eri_column_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row)) * erc_row_scale_etcc_column_count_exists_previous_choices_witness_row_semantics)) /\ exists ff_q_eri_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row_decoded. erc_row_code_etcc_column_count_exists_previous_choices_witness_row_semantics = ff_q_eri_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row_decoded * S ((S (eri_column_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row)) * erc_row_scale_etcc_column_count_exists_previous_choices_witness_row_semantics) + (eri_bit_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row))) /\ (((eri_bit_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row = 0 /\ ((exists eri_gap_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row_choice_left. eri_gap_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row_choice_left + S (q * S etcc_row_index_column_count_exists_previous_choices) = p * S eri_column_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row) /\ ~(exists eri_gap_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row_choice_right. eri_gap_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row) = q * S etcc_row_index_column_count_exists_previous_choices))) \/ (eri_bit_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row = 1 /\ ((exists eri_gap_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row_choice_right. eri_gap_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row) = q * S etcc_row_index_column_count_exists_previous_choices) /\ ~(exists eri_gap_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row_choice_left. eri_gap_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row_choice_left + S (q * S etcc_row_index_column_count_exists_previous_choices) = p * S eri_column_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_row))))))) /\ (((exists ff_u_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum ff_v_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum. ((((exists ff_h_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_start. ff_h_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_start. ff_u_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_start * S ((S (0)) * ff_v_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum) + (0))) /\ ((((exists ff_h_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_terminal. ff_h_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_terminal + S (etcc_row_count_column_count_exists_previous_choices_witness) = S ((S (k)) * ff_v_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_terminal. ff_u_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_terminal * S ((S (k)) * ff_v_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum) + (etcc_row_count_column_count_exists_previous_choices_witness))) /\ forall ff_i_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum. (exists ff_lt_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_bound. ff_lt_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_bound + S ff_i_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum = k) -> exists ff_a_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum ff_r_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum ff_s_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum. ((((exists ff_h_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_summand. ff_h_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_summand + S (ff_a_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum)) * erc_row_scale_etcc_column_count_exists_previous_choices_witness_row_semantics)) /\ exists ff_q_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_summand. erc_row_code_etcc_column_count_exists_previous_choices_witness_row_semantics = ff_q_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_summand * S ((S (ff_i_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum)) * erc_row_scale_etcc_column_count_exists_previous_choices_witness_row_semantics) + (ff_a_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_partial. ff_h_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_partial + S (ff_r_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_partial. ff_u_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_partial * S ((S (ff_i_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum) + (ff_r_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_successor. ff_h_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_successor + S (ff_s_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum) = S ((S (S ff_i_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_successor. ff_u_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum_successor * S ((S (S ff_i_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum) + (ff_s_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum))) /\ ff_s_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum = ff_r_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum + ff_a_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_sum)))))) /\ (forall ff_i_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_bits. (exists ff_lt_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_bits_bound. ff_lt_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_bits_bound + S ff_i_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_bits = k) -> exists ff_bit_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_bits. ((((exists ff_h_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_bits_decoded. ff_h_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_bits_decoded + S (ff_bit_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_bits) = S ((S (ff_i_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_bits)) * erc_row_scale_etcc_column_count_exists_previous_choices_witness_row_semantics)) /\ exists ff_q_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_bits_decoded. erc_row_code_etcc_column_count_exists_previous_choices_witness_row_semantics = ff_q_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_bits_decoded * S ((S (ff_i_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_bits)) * erc_row_scale_etcc_column_count_exists_previous_choices_witness_row_semantics) + (ff_bit_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_bits))) /\ (ff_bit_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_bits = 0 \/ ff_bit_erc_etcc_column_count_exists_previous_choices_witness_row_semantics_count_bits = 1)))))))) /\ (forall etc_row_index_etcc_column_count_exists_previous_choices_witness_column. (exists edt_lt_gap_etcc_column_count_exists_previous_choices_witness_column_bound. edt_lt_gap_etcc_column_count_exists_previous_choices_witness_column_bound + S (etc_row_index_etcc_column_count_exists_previous_choices_witness_column) = k) -> exists etc_bit_etcc_column_count_exists_previous_choices_witness_column. ((((exists ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_decoded. ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_decoded + S (etc_bit_etcc_column_count_exists_previous_choices_witness_column) = S ((S (etc_row_index_etcc_column_count_exists_previous_choices_witness_column)) * etcc_column_scale_column_count_exists_previous_choices_witness)) /\ exists ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_decoded. etcc_column_code_column_count_exists_previous_choices_witness = ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_decoded * S ((S (etc_row_index_etcc_column_count_exists_previous_choices_witness_column)) * etcc_column_scale_column_count_exists_previous_choices_witness) + (etc_bit_etcc_column_count_exists_previous_choices_witness_column))) /\ (exists etc_count_etcc_column_count_exists_previous_choices_witness_column_witness etc_row_code_etcc_column_count_exists_previous_choices_witness_column_witness etc_row_scale_etcc_column_count_exists_previous_choices_witness_column_witness. ((((((exists ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_outer_entry. ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_outer_entry + S (etc_count_etcc_column_count_exists_previous_choices_witness_column_witness) = S ((S (etc_row_index_etcc_column_count_exists_previous_choices_witness_column)) * bc)) /\ exists ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_outer_entry. bb = ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_outer_entry * S ((S (etc_row_index_etcc_column_count_exists_previous_choices_witness_column)) * bc) + (etc_count_etcc_column_count_exists_previous_choices_witness_column_witness))) /\ (forall eri_column_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row. (exists eri_gap_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row_bound. eri_gap_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row_bound + S (eri_column_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row) = h) -> exists eri_bit_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row. ((((exists ff_h_eri_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row_decoded. ff_h_eri_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row_decoded + S (eri_bit_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row) = S ((S (eri_column_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row)) * etc_row_scale_etcc_column_count_exists_previous_choices_witness_column_witness)) /\ exists ff_q_eri_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row_decoded. etc_row_code_etcc_column_count_exists_previous_choices_witness_column_witness = ff_q_eri_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row_decoded * S ((S (eri_column_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row)) * etc_row_scale_etcc_column_count_exists_previous_choices_witness_column_witness) + (eri_bit_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row))) /\ (((eri_bit_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row = 0 /\ ((exists eri_gap_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row_choice_left. eri_gap_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row_choice_left + S (p * S etc_row_index_etcc_column_count_exists_previous_choices_witness_column) = q * S eri_column_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row) /\ ~(exists eri_gap_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row_choice_right. eri_gap_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row) = p * S etc_row_index_etcc_column_count_exists_previous_choices_witness_column))) \/ (eri_bit_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row = 1 /\ ((exists eri_gap_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row_choice_right. eri_gap_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row) = p * S etc_row_index_etcc_column_count_exists_previous_choices_witness_column) /\ ~(exists eri_gap_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row_choice_left. eri_gap_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row_choice_left + S (p * S etc_row_index_etcc_column_count_exists_previous_choices_witness_column) = q * S eri_column_etc_etcc_column_count_exists_previous_choices_witness_column_witness_row)))))))) /\ (((exists ff_u_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum ff_v_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_start. ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_start. ff_u_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_terminal. ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_terminal + S (etc_count_etcc_column_count_exists_previous_choices_witness_column_witness) = S ((S (h)) * ff_v_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_terminal. ff_u_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum) + (etc_count_etcc_column_count_exists_previous_choices_witness_column_witness))) /\ forall ff_i_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum. (exists ff_lt_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_bound. ff_lt_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_bound + S ff_i_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum = h) -> exists ff_a_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum ff_r_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum ff_s_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_summand. ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_summand + S (ff_a_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum)) * etc_row_scale_etcc_column_count_exists_previous_choices_witness_column_witness)) /\ exists ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_summand. etc_row_code_etcc_column_count_exists_previous_choices_witness_column_witness = ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum)) * etc_row_scale_etcc_column_count_exists_previous_choices_witness_column_witness) + (ff_a_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_partial. ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_partial + S (ff_r_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_partial. ff_u_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum) + (ff_r_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_successor. ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_successor + S (ff_s_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum) = S ((S (S ff_i_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_successor. ff_u_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum) + (ff_s_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum))) /\ ff_s_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum = ff_r_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum + ff_a_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_bits. (exists ff_lt_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_bits_bound. ff_lt_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_bits_bound + S ff_i_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_bits = h) -> exists ff_bit_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_bits. ((((exists ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_bits_decoded. ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_bits_decoded + S (ff_bit_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_bits) = S ((S (ff_i_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_bits)) * etc_row_scale_etcc_column_count_exists_previous_choices_witness_column_witness)) /\ exists ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_bits_decoded. etc_row_code_etcc_column_count_exists_previous_choices_witness_column_witness = ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_bits)) * etc_row_scale_etcc_column_count_exists_previous_choices_witness_column_witness) + (ff_bit_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_bits))) /\ (ff_bit_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_bits = 0 \/ ff_bit_etc_etcc_column_count_exists_previous_choices_witness_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_inner_entry. ff_h_etc_etcc_column_count_exists_previous_choices_witness_column_witness_inner_entry + S (etc_bit_etcc_column_count_exists_previous_choices_witness_column) = S ((S (etcc_row_index_column_count_exists_previous_choices)) * etc_row_scale_etcc_column_count_exists_previous_choices_witness_column_witness)) /\ exists ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_inner_entry. etc_row_code_etcc_column_count_exists_previous_choices_witness_column_witness = ff_q_etc_etcc_column_count_exists_previous_choices_witness_column_witness_inner_entry * S ((S (etcc_row_index_column_count_exists_previous_choices)) * etc_row_scale_etcc_column_count_exists_previous_choices_witness_column_witness) + (etc_bit_etcc_column_count_exists_previous_choices_witness_column)))))))) /\ ((((exists ff_u_etcc_column_count_exists_previous_choices_witness_column_count_sum ff_v_etcc_column_count_exists_previous_choices_witness_column_count_sum. ((((exists ff_h_etcc_column_count_exists_previous_choices_witness_column_count_sum_start. ff_h_etcc_column_count_exists_previous_choices_witness_column_count_sum_start + S (0) = S ((S (0)) * ff_v_etcc_column_count_exists_previous_choices_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_previous_choices_witness_column_count_sum_start. ff_u_etcc_column_count_exists_previous_choices_witness_column_count_sum = ff_q_etcc_column_count_exists_previous_choices_witness_column_count_sum_start * S ((S (0)) * ff_v_etcc_column_count_exists_previous_choices_witness_column_count_sum) + (0))) /\ ((((exists ff_h_etcc_column_count_exists_previous_choices_witness_column_count_sum_terminal. ff_h_etcc_column_count_exists_previous_choices_witness_column_count_sum_terminal + S (etcc_count_column_count_exists_previous_choices) = S ((S (k)) * ff_v_etcc_column_count_exists_previous_choices_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_previous_choices_witness_column_count_sum_terminal. ff_u_etcc_column_count_exists_previous_choices_witness_column_count_sum = ff_q_etcc_column_count_exists_previous_choices_witness_column_count_sum_terminal * S ((S (k)) * ff_v_etcc_column_count_exists_previous_choices_witness_column_count_sum) + (etcc_count_column_count_exists_previous_choices))) /\ forall ff_i_etcc_column_count_exists_previous_choices_witness_column_count_sum. (exists ff_lt_etcc_column_count_exists_previous_choices_witness_column_count_sum_bound. ff_lt_etcc_column_count_exists_previous_choices_witness_column_count_sum_bound + S ff_i_etcc_column_count_exists_previous_choices_witness_column_count_sum = k) -> exists ff_a_etcc_column_count_exists_previous_choices_witness_column_count_sum ff_r_etcc_column_count_exists_previous_choices_witness_column_count_sum ff_s_etcc_column_count_exists_previous_choices_witness_column_count_sum. ((((exists ff_h_etcc_column_count_exists_previous_choices_witness_column_count_sum_summand. ff_h_etcc_column_count_exists_previous_choices_witness_column_count_sum_summand + S (ff_a_etcc_column_count_exists_previous_choices_witness_column_count_sum) = S ((S (ff_i_etcc_column_count_exists_previous_choices_witness_column_count_sum)) * etcc_column_scale_column_count_exists_previous_choices_witness)) /\ exists ff_q_etcc_column_count_exists_previous_choices_witness_column_count_sum_summand. etcc_column_code_column_count_exists_previous_choices_witness = ff_q_etcc_column_count_exists_previous_choices_witness_column_count_sum_summand * S ((S (ff_i_etcc_column_count_exists_previous_choices_witness_column_count_sum)) * etcc_column_scale_column_count_exists_previous_choices_witness) + (ff_a_etcc_column_count_exists_previous_choices_witness_column_count_sum))) /\ ((((exists ff_h_etcc_column_count_exists_previous_choices_witness_column_count_sum_partial. ff_h_etcc_column_count_exists_previous_choices_witness_column_count_sum_partial + S (ff_r_etcc_column_count_exists_previous_choices_witness_column_count_sum) = S ((S (ff_i_etcc_column_count_exists_previous_choices_witness_column_count_sum)) * ff_v_etcc_column_count_exists_previous_choices_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_previous_choices_witness_column_count_sum_partial. ff_u_etcc_column_count_exists_previous_choices_witness_column_count_sum = ff_q_etcc_column_count_exists_previous_choices_witness_column_count_sum_partial * S ((S (ff_i_etcc_column_count_exists_previous_choices_witness_column_count_sum)) * ff_v_etcc_column_count_exists_previous_choices_witness_column_count_sum) + (ff_r_etcc_column_count_exists_previous_choices_witness_column_count_sum))) /\ ((((exists ff_h_etcc_column_count_exists_previous_choices_witness_column_count_sum_successor. ff_h_etcc_column_count_exists_previous_choices_witness_column_count_sum_successor + S (ff_s_etcc_column_count_exists_previous_choices_witness_column_count_sum) = S ((S (S ff_i_etcc_column_count_exists_previous_choices_witness_column_count_sum)) * ff_v_etcc_column_count_exists_previous_choices_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_previous_choices_witness_column_count_sum_successor. ff_u_etcc_column_count_exists_previous_choices_witness_column_count_sum = ff_q_etcc_column_count_exists_previous_choices_witness_column_count_sum_successor * S ((S (S ff_i_etcc_column_count_exists_previous_choices_witness_column_count_sum)) * ff_v_etcc_column_count_exists_previous_choices_witness_column_count_sum) + (ff_s_etcc_column_count_exists_previous_choices_witness_column_count_sum))) /\ ff_s_etcc_column_count_exists_previous_choices_witness_column_count_sum = ff_r_etcc_column_count_exists_previous_choices_witness_column_count_sum + ff_a_etcc_column_count_exists_previous_choices_witness_column_count_sum)))))) /\ (forall ff_i_etcc_column_count_exists_previous_choices_witness_column_count_bits. (exists ff_lt_etcc_column_count_exists_previous_choices_witness_column_count_bits_bound. ff_lt_etcc_column_count_exists_previous_choices_witness_column_count_bits_bound + S ff_i_etcc_column_count_exists_previous_choices_witness_column_count_bits = k) -> exists ff_bit_etcc_column_count_exists_previous_choices_witness_column_count_bits. ((((exists ff_h_etcc_column_count_exists_previous_choices_witness_column_count_bits_decoded. ff_h_etcc_column_count_exists_previous_choices_witness_column_count_bits_decoded + S (ff_bit_etcc_column_count_exists_previous_choices_witness_column_count_bits) = S ((S (ff_i_etcc_column_count_exists_previous_choices_witness_column_count_bits)) * etcc_column_scale_column_count_exists_previous_choices_witness)) /\ exists ff_q_etcc_column_count_exists_previous_choices_witness_column_count_bits_decoded. etcc_column_code_column_count_exists_previous_choices_witness = ff_q_etcc_column_count_exists_previous_choices_witness_column_count_bits_decoded * S ((S (ff_i_etcc_column_count_exists_previous_choices_witness_column_count_bits)) * etcc_column_scale_column_count_exists_previous_choices_witness) + (ff_bit_etcc_column_count_exists_previous_choices_witness_column_count_bits))) /\ (ff_bit_etcc_column_count_exists_previous_choices_witness_column_count_bits = 0 \/ ff_bit_etcc_column_count_exists_previous_choices_witness_column_count_bits = 1))))) /\ etcc_row_count_column_count_exists_previous_choices_witness + etcc_count_column_count_exists_previous_choices = k)))
27. 0027intro i
28. 0028intro hi
29. 0029specialize hchoices i
30. 0030apply hchoices
31. 0031specialize le_succ (S i)
32. 0032specialize le_succ l
33. 0033apply le_succ
34. 0034exact hi
35. 0035have hprefix : exists db dc. (forall etcc_row_index_column_count_exists_previous_prefix. (exists edt_lt_gap_column_count_exists_previous_prefix_bound. edt_lt_gap_column_count_exists_previous_prefix_bound + S (etcc_row_index_column_count_exists_previous_prefix) = l) -> exists etcc_count_column_count_exists_previous_prefix. ((((exists ff_h_etcc_column_count_exists_previous_prefix_decoded. ff_h_etcc_column_count_exists_previous_prefix_decoded + S (etcc_count_column_count_exists_previous_prefix) = S ((S (etcc_row_index_column_count_exists_previous_prefix)) * dc)) /\ exists ff_q_etcc_column_count_exists_previous_prefix_decoded. db = ff_q_etcc_column_count_exists_previous_prefix_decoded * S ((S (etcc_row_index_column_count_exists_previous_prefix)) * dc) + (etcc_count_column_count_exists_previous_prefix))) /\ (exists etcc_row_count_column_count_exists_previous_prefix_witness etcc_column_code_column_count_exists_previous_prefix_witness etcc_column_scale_column_count_exists_previous_prefix_witness. ((((((exists ff_h_etcc_column_count_exists_previous_prefix_witness_first_entry. ff_h_etcc_column_count_exists_previous_prefix_witness_first_entry + S (etcc_row_count_column_count_exists_previous_prefix_witness) = S ((S (etcc_row_index_column_count_exists_previous_prefix)) * ac)) /\ exists ff_q_etcc_column_count_exists_previous_prefix_witness_first_entry. ab = ff_q_etcc_column_count_exists_previous_prefix_witness_first_entry * S ((S (etcc_row_index_column_count_exists_previous_prefix)) * ac) + (etcc_row_count_column_count_exists_previous_prefix_witness))) /\ (exists erc_row_code_etcc_column_count_exists_previous_prefix_witness_row_semantics erc_row_scale_etcc_column_count_exists_previous_prefix_witness_row_semantics. ((forall eri_column_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row. (exists eri_gap_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row_bound. eri_gap_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row_bound + S (eri_column_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row) = k) -> exists eri_bit_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row. ((((exists ff_h_eri_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row_decoded. ff_h_eri_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row_decoded + S (eri_bit_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row) = S ((S (eri_column_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row)) * erc_row_scale_etcc_column_count_exists_previous_prefix_witness_row_semantics)) /\ exists ff_q_eri_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row_decoded. erc_row_code_etcc_column_count_exists_previous_prefix_witness_row_semantics = ff_q_eri_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row_decoded * S ((S (eri_column_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row)) * erc_row_scale_etcc_column_count_exists_previous_prefix_witness_row_semantics) + (eri_bit_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row))) /\ (((eri_bit_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row = 0 /\ ((exists eri_gap_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row_choice_left. eri_gap_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row_choice_left + S (q * S etcc_row_index_column_count_exists_previous_prefix) = p * S eri_column_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row) /\ ~(exists eri_gap_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row_choice_right. eri_gap_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row) = q * S etcc_row_index_column_count_exists_previous_prefix))) \/ (eri_bit_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row = 1 /\ ((exists eri_gap_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row_choice_right. eri_gap_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row) = q * S etcc_row_index_column_count_exists_previous_prefix) /\ ~(exists eri_gap_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row_choice_left. eri_gap_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row_choice_left + S (q * S etcc_row_index_column_count_exists_previous_prefix) = p * S eri_column_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_row))))))) /\ (((exists ff_u_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum ff_v_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum. ((((exists ff_h_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_start. ff_h_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_start. ff_u_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_start * S ((S (0)) * ff_v_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum) + (0))) /\ ((((exists ff_h_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_terminal. ff_h_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_terminal + S (etcc_row_count_column_count_exists_previous_prefix_witness) = S ((S (k)) * ff_v_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_terminal. ff_u_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_terminal * S ((S (k)) * ff_v_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum) + (etcc_row_count_column_count_exists_previous_prefix_witness))) /\ forall ff_i_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum. (exists ff_lt_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_bound. ff_lt_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_bound + S ff_i_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum = k) -> exists ff_a_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum ff_r_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum ff_s_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum. ((((exists ff_h_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_summand. ff_h_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_summand + S (ff_a_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum)) * erc_row_scale_etcc_column_count_exists_previous_prefix_witness_row_semantics)) /\ exists ff_q_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_summand. erc_row_code_etcc_column_count_exists_previous_prefix_witness_row_semantics = ff_q_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_summand * S ((S (ff_i_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum)) * erc_row_scale_etcc_column_count_exists_previous_prefix_witness_row_semantics) + (ff_a_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_partial. ff_h_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_partial + S (ff_r_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_partial. ff_u_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_partial * S ((S (ff_i_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum) + (ff_r_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_successor. ff_h_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_successor + S (ff_s_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum) = S ((S (S ff_i_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_successor. ff_u_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum_successor * S ((S (S ff_i_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum) + (ff_s_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum))) /\ ff_s_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum = ff_r_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum + ff_a_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_sum)))))) /\ (forall ff_i_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_bits. (exists ff_lt_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_bits_bound. ff_lt_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_bits_bound + S ff_i_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_bits = k) -> exists ff_bit_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_bits. ((((exists ff_h_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_bits_decoded. ff_h_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_bits_decoded + S (ff_bit_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_bits) = S ((S (ff_i_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_bits)) * erc_row_scale_etcc_column_count_exists_previous_prefix_witness_row_semantics)) /\ exists ff_q_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_bits_decoded. erc_row_code_etcc_column_count_exists_previous_prefix_witness_row_semantics = ff_q_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_bits_decoded * S ((S (ff_i_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_bits)) * erc_row_scale_etcc_column_count_exists_previous_prefix_witness_row_semantics) + (ff_bit_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_bits))) /\ (ff_bit_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_bits = 0 \/ ff_bit_erc_etcc_column_count_exists_previous_prefix_witness_row_semantics_count_bits = 1)))))))) /\ (forall etc_row_index_etcc_column_count_exists_previous_prefix_witness_column. (exists edt_lt_gap_etcc_column_count_exists_previous_prefix_witness_column_bound. edt_lt_gap_etcc_column_count_exists_previous_prefix_witness_column_bound + S (etc_row_index_etcc_column_count_exists_previous_prefix_witness_column) = k) -> exists etc_bit_etcc_column_count_exists_previous_prefix_witness_column. ((((exists ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_decoded. ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_decoded + S (etc_bit_etcc_column_count_exists_previous_prefix_witness_column) = S ((S (etc_row_index_etcc_column_count_exists_previous_prefix_witness_column)) * etcc_column_scale_column_count_exists_previous_prefix_witness)) /\ exists ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_decoded. etcc_column_code_column_count_exists_previous_prefix_witness = ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_decoded * S ((S (etc_row_index_etcc_column_count_exists_previous_prefix_witness_column)) * etcc_column_scale_column_count_exists_previous_prefix_witness) + (etc_bit_etcc_column_count_exists_previous_prefix_witness_column))) /\ (exists etc_count_etcc_column_count_exists_previous_prefix_witness_column_witness etc_row_code_etcc_column_count_exists_previous_prefix_witness_column_witness etc_row_scale_etcc_column_count_exists_previous_prefix_witness_column_witness. ((((((exists ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_outer_entry. ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_outer_entry + S (etc_count_etcc_column_count_exists_previous_prefix_witness_column_witness) = S ((S (etc_row_index_etcc_column_count_exists_previous_prefix_witness_column)) * bc)) /\ exists ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_outer_entry. bb = ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_outer_entry * S ((S (etc_row_index_etcc_column_count_exists_previous_prefix_witness_column)) * bc) + (etc_count_etcc_column_count_exists_previous_prefix_witness_column_witness))) /\ (forall eri_column_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row. (exists eri_gap_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row_bound. eri_gap_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row_bound + S (eri_column_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row) = h) -> exists eri_bit_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row. ((((exists ff_h_eri_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row_decoded. ff_h_eri_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row_decoded + S (eri_bit_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row) = S ((S (eri_column_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row)) * etc_row_scale_etcc_column_count_exists_previous_prefix_witness_column_witness)) /\ exists ff_q_eri_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row_decoded. etc_row_code_etcc_column_count_exists_previous_prefix_witness_column_witness = ff_q_eri_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row_decoded * S ((S (eri_column_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row)) * etc_row_scale_etcc_column_count_exists_previous_prefix_witness_column_witness) + (eri_bit_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row))) /\ (((eri_bit_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row = 0 /\ ((exists eri_gap_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row_choice_left. eri_gap_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row_choice_left + S (p * S etc_row_index_etcc_column_count_exists_previous_prefix_witness_column) = q * S eri_column_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row) /\ ~(exists eri_gap_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row_choice_right. eri_gap_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row) = p * S etc_row_index_etcc_column_count_exists_previous_prefix_witness_column))) \/ (eri_bit_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row = 1 /\ ((exists eri_gap_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row_choice_right. eri_gap_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row) = p * S etc_row_index_etcc_column_count_exists_previous_prefix_witness_column) /\ ~(exists eri_gap_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row_choice_left. eri_gap_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row_choice_left + S (p * S etc_row_index_etcc_column_count_exists_previous_prefix_witness_column) = q * S eri_column_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_row)))))))) /\ (((exists ff_u_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum ff_v_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_start. ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_start. ff_u_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_terminal. ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_terminal + S (etc_count_etcc_column_count_exists_previous_prefix_witness_column_witness) = S ((S (h)) * ff_v_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_terminal. ff_u_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum) + (etc_count_etcc_column_count_exists_previous_prefix_witness_column_witness))) /\ forall ff_i_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum. (exists ff_lt_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_bound. ff_lt_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_bound + S ff_i_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum = h) -> exists ff_a_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum ff_r_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum ff_s_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_summand. ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_summand + S (ff_a_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum)) * etc_row_scale_etcc_column_count_exists_previous_prefix_witness_column_witness)) /\ exists ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_summand. etc_row_code_etcc_column_count_exists_previous_prefix_witness_column_witness = ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum)) * etc_row_scale_etcc_column_count_exists_previous_prefix_witness_column_witness) + (ff_a_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_partial. ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_partial + S (ff_r_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_partial. ff_u_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum) + (ff_r_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_successor. ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_successor + S (ff_s_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum) = S ((S (S ff_i_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_successor. ff_u_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum) + (ff_s_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum))) /\ ff_s_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum = ff_r_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum + ff_a_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_bits. (exists ff_lt_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_bits_bound. ff_lt_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_bits_bound + S ff_i_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_bits = h) -> exists ff_bit_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_bits. ((((exists ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_bits_decoded. ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_bits_decoded + S (ff_bit_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_bits) = S ((S (ff_i_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_bits)) * etc_row_scale_etcc_column_count_exists_previous_prefix_witness_column_witness)) /\ exists ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_bits_decoded. etc_row_code_etcc_column_count_exists_previous_prefix_witness_column_witness = ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_bits)) * etc_row_scale_etcc_column_count_exists_previous_prefix_witness_column_witness) + (ff_bit_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_bits))) /\ (ff_bit_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_bits = 0 \/ ff_bit_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_inner_entry. ff_h_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_inner_entry + S (etc_bit_etcc_column_count_exists_previous_prefix_witness_column) = S ((S (etcc_row_index_column_count_exists_previous_prefix)) * etc_row_scale_etcc_column_count_exists_previous_prefix_witness_column_witness)) /\ exists ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_inner_entry. etc_row_code_etcc_column_count_exists_previous_prefix_witness_column_witness = ff_q_etc_etcc_column_count_exists_previous_prefix_witness_column_witness_inner_entry * S ((S (etcc_row_index_column_count_exists_previous_prefix)) * etc_row_scale_etcc_column_count_exists_previous_prefix_witness_column_witness) + (etc_bit_etcc_column_count_exists_previous_prefix_witness_column)))))))) /\ ((((exists ff_u_etcc_column_count_exists_previous_prefix_witness_column_count_sum ff_v_etcc_column_count_exists_previous_prefix_witness_column_count_sum. ((((exists ff_h_etcc_column_count_exists_previous_prefix_witness_column_count_sum_start. ff_h_etcc_column_count_exists_previous_prefix_witness_column_count_sum_start + S (0) = S ((S (0)) * ff_v_etcc_column_count_exists_previous_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_previous_prefix_witness_column_count_sum_start. ff_u_etcc_column_count_exists_previous_prefix_witness_column_count_sum = ff_q_etcc_column_count_exists_previous_prefix_witness_column_count_sum_start * S ((S (0)) * ff_v_etcc_column_count_exists_previous_prefix_witness_column_count_sum) + (0))) /\ ((((exists ff_h_etcc_column_count_exists_previous_prefix_witness_column_count_sum_terminal. ff_h_etcc_column_count_exists_previous_prefix_witness_column_count_sum_terminal + S (etcc_count_column_count_exists_previous_prefix) = S ((S (k)) * ff_v_etcc_column_count_exists_previous_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_previous_prefix_witness_column_count_sum_terminal. ff_u_etcc_column_count_exists_previous_prefix_witness_column_count_sum = ff_q_etcc_column_count_exists_previous_prefix_witness_column_count_sum_terminal * S ((S (k)) * ff_v_etcc_column_count_exists_previous_prefix_witness_column_count_sum) + (etcc_count_column_count_exists_previous_prefix))) /\ forall ff_i_etcc_column_count_exists_previous_prefix_witness_column_count_sum. (exists ff_lt_etcc_column_count_exists_previous_prefix_witness_column_count_sum_bound. ff_lt_etcc_column_count_exists_previous_prefix_witness_column_count_sum_bound + S ff_i_etcc_column_count_exists_previous_prefix_witness_column_count_sum = k) -> exists ff_a_etcc_column_count_exists_previous_prefix_witness_column_count_sum ff_r_etcc_column_count_exists_previous_prefix_witness_column_count_sum ff_s_etcc_column_count_exists_previous_prefix_witness_column_count_sum. ((((exists ff_h_etcc_column_count_exists_previous_prefix_witness_column_count_sum_summand. ff_h_etcc_column_count_exists_previous_prefix_witness_column_count_sum_summand + S (ff_a_etcc_column_count_exists_previous_prefix_witness_column_count_sum) = S ((S (ff_i_etcc_column_count_exists_previous_prefix_witness_column_count_sum)) * etcc_column_scale_column_count_exists_previous_prefix_witness)) /\ exists ff_q_etcc_column_count_exists_previous_prefix_witness_column_count_sum_summand. etcc_column_code_column_count_exists_previous_prefix_witness = ff_q_etcc_column_count_exists_previous_prefix_witness_column_count_sum_summand * S ((S (ff_i_etcc_column_count_exists_previous_prefix_witness_column_count_sum)) * etcc_column_scale_column_count_exists_previous_prefix_witness) + (ff_a_etcc_column_count_exists_previous_prefix_witness_column_count_sum))) /\ ((((exists ff_h_etcc_column_count_exists_previous_prefix_witness_column_count_sum_partial. ff_h_etcc_column_count_exists_previous_prefix_witness_column_count_sum_partial + S (ff_r_etcc_column_count_exists_previous_prefix_witness_column_count_sum) = S ((S (ff_i_etcc_column_count_exists_previous_prefix_witness_column_count_sum)) * ff_v_etcc_column_count_exists_previous_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_previous_prefix_witness_column_count_sum_partial. ff_u_etcc_column_count_exists_previous_prefix_witness_column_count_sum = ff_q_etcc_column_count_exists_previous_prefix_witness_column_count_sum_partial * S ((S (ff_i_etcc_column_count_exists_previous_prefix_witness_column_count_sum)) * ff_v_etcc_column_count_exists_previous_prefix_witness_column_count_sum) + (ff_r_etcc_column_count_exists_previous_prefix_witness_column_count_sum))) /\ ((((exists ff_h_etcc_column_count_exists_previous_prefix_witness_column_count_sum_successor. ff_h_etcc_column_count_exists_previous_prefix_witness_column_count_sum_successor + S (ff_s_etcc_column_count_exists_previous_prefix_witness_column_count_sum) = S ((S (S ff_i_etcc_column_count_exists_previous_prefix_witness_column_count_sum)) * ff_v_etcc_column_count_exists_previous_prefix_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_previous_prefix_witness_column_count_sum_successor. ff_u_etcc_column_count_exists_previous_prefix_witness_column_count_sum = ff_q_etcc_column_count_exists_previous_prefix_witness_column_count_sum_successor * S ((S (S ff_i_etcc_column_count_exists_previous_prefix_witness_column_count_sum)) * ff_v_etcc_column_count_exists_previous_prefix_witness_column_count_sum) + (ff_s_etcc_column_count_exists_previous_prefix_witness_column_count_sum))) /\ ff_s_etcc_column_count_exists_previous_prefix_witness_column_count_sum = ff_r_etcc_column_count_exists_previous_prefix_witness_column_count_sum + ff_a_etcc_column_count_exists_previous_prefix_witness_column_count_sum)))))) /\ (forall ff_i_etcc_column_count_exists_previous_prefix_witness_column_count_bits. (exists ff_lt_etcc_column_count_exists_previous_prefix_witness_column_count_bits_bound. ff_lt_etcc_column_count_exists_previous_prefix_witness_column_count_bits_bound + S ff_i_etcc_column_count_exists_previous_prefix_witness_column_count_bits = k) -> exists ff_bit_etcc_column_count_exists_previous_prefix_witness_column_count_bits. ((((exists ff_h_etcc_column_count_exists_previous_prefix_witness_column_count_bits_decoded. ff_h_etcc_column_count_exists_previous_prefix_witness_column_count_bits_decoded + S (ff_bit_etcc_column_count_exists_previous_prefix_witness_column_count_bits) = S ((S (ff_i_etcc_column_count_exists_previous_prefix_witness_column_count_bits)) * etcc_column_scale_column_count_exists_previous_prefix_witness)) /\ exists ff_q_etcc_column_count_exists_previous_prefix_witness_column_count_bits_decoded. etcc_column_code_column_count_exists_previous_prefix_witness = ff_q_etcc_column_count_exists_previous_prefix_witness_column_count_bits_decoded * S ((S (ff_i_etcc_column_count_exists_previous_prefix_witness_column_count_bits)) * etcc_column_scale_column_count_exists_previous_prefix_witness) + (ff_bit_etcc_column_count_exists_previous_prefix_witness_column_count_bits))) /\ (ff_bit_etcc_column_count_exists_previous_prefix_witness_column_count_bits = 0 \/ ff_bit_etcc_column_count_exists_previous_prefix_witness_column_count_bits = 1))))) /\ etcc_row_count_column_count_exists_previous_prefix_witness + etcc_count_column_count_exists_previous_prefix = k)))))
36. 0036apply IH
37. 0037exact hprevious
38. 0038cases hprefix
39. 0039cases hprefix_witness
40. 0040have hlast : exists m. (exists etcc_row_count_column_count_exists_last etcc_column_code_column_count_exists_last etcc_column_scale_column_count_exists_last. ((((((exists ff_h_etcc_column_count_exists_last_first_entry. ff_h_etcc_column_count_exists_last_first_entry + S (etcc_row_count_column_count_exists_last) = S ((S (l)) * ac)) /\ exists ff_q_etcc_column_count_exists_last_first_entry. ab = ff_q_etcc_column_count_exists_last_first_entry * S ((S (l)) * ac) + (etcc_row_count_column_count_exists_last))) /\ (exists erc_row_code_etcc_column_count_exists_last_row_semantics erc_row_scale_etcc_column_count_exists_last_row_semantics. ((forall eri_column_erc_etcc_column_count_exists_last_row_semantics_row. (exists eri_gap_erc_etcc_column_count_exists_last_row_semantics_row_bound. eri_gap_erc_etcc_column_count_exists_last_row_semantics_row_bound + S (eri_column_erc_etcc_column_count_exists_last_row_semantics_row) = k) -> exists eri_bit_erc_etcc_column_count_exists_last_row_semantics_row. ((((exists ff_h_eri_erc_etcc_column_count_exists_last_row_semantics_row_decoded. ff_h_eri_erc_etcc_column_count_exists_last_row_semantics_row_decoded + S (eri_bit_erc_etcc_column_count_exists_last_row_semantics_row) = S ((S (eri_column_erc_etcc_column_count_exists_last_row_semantics_row)) * erc_row_scale_etcc_column_count_exists_last_row_semantics)) /\ exists ff_q_eri_erc_etcc_column_count_exists_last_row_semantics_row_decoded. erc_row_code_etcc_column_count_exists_last_row_semantics = ff_q_eri_erc_etcc_column_count_exists_last_row_semantics_row_decoded * S ((S (eri_column_erc_etcc_column_count_exists_last_row_semantics_row)) * erc_row_scale_etcc_column_count_exists_last_row_semantics) + (eri_bit_erc_etcc_column_count_exists_last_row_semantics_row))) /\ (((eri_bit_erc_etcc_column_count_exists_last_row_semantics_row = 0 /\ ((exists eri_gap_erc_etcc_column_count_exists_last_row_semantics_row_choice_left. eri_gap_erc_etcc_column_count_exists_last_row_semantics_row_choice_left + S (q * S l) = p * S eri_column_erc_etcc_column_count_exists_last_row_semantics_row) /\ ~(exists eri_gap_erc_etcc_column_count_exists_last_row_semantics_row_choice_right. eri_gap_erc_etcc_column_count_exists_last_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_column_count_exists_last_row_semantics_row) = q * S l))) \/ (eri_bit_erc_etcc_column_count_exists_last_row_semantics_row = 1 /\ ((exists eri_gap_erc_etcc_column_count_exists_last_row_semantics_row_choice_right. eri_gap_erc_etcc_column_count_exists_last_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_column_count_exists_last_row_semantics_row) = q * S l) /\ ~(exists eri_gap_erc_etcc_column_count_exists_last_row_semantics_row_choice_left. eri_gap_erc_etcc_column_count_exists_last_row_semantics_row_choice_left + S (q * S l) = p * S eri_column_erc_etcc_column_count_exists_last_row_semantics_row))))))) /\ (((exists ff_u_erc_etcc_column_count_exists_last_row_semantics_count_sum ff_v_erc_etcc_column_count_exists_last_row_semantics_count_sum. ((((exists ff_h_erc_etcc_column_count_exists_last_row_semantics_count_sum_start. ff_h_erc_etcc_column_count_exists_last_row_semantics_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_etcc_column_count_exists_last_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_last_row_semantics_count_sum_start. ff_u_erc_etcc_column_count_exists_last_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_last_row_semantics_count_sum_start * S ((S (0)) * ff_v_erc_etcc_column_count_exists_last_row_semantics_count_sum) + (0))) /\ ((((exists ff_h_erc_etcc_column_count_exists_last_row_semantics_count_sum_terminal. ff_h_erc_etcc_column_count_exists_last_row_semantics_count_sum_terminal + S (etcc_row_count_column_count_exists_last) = S ((S (k)) * ff_v_erc_etcc_column_count_exists_last_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_last_row_semantics_count_sum_terminal. ff_u_erc_etcc_column_count_exists_last_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_last_row_semantics_count_sum_terminal * S ((S (k)) * ff_v_erc_etcc_column_count_exists_last_row_semantics_count_sum) + (etcc_row_count_column_count_exists_last))) /\ forall ff_i_erc_etcc_column_count_exists_last_row_semantics_count_sum. (exists ff_lt_erc_etcc_column_count_exists_last_row_semantics_count_sum_bound. ff_lt_erc_etcc_column_count_exists_last_row_semantics_count_sum_bound + S ff_i_erc_etcc_column_count_exists_last_row_semantics_count_sum = k) -> exists ff_a_erc_etcc_column_count_exists_last_row_semantics_count_sum ff_r_erc_etcc_column_count_exists_last_row_semantics_count_sum ff_s_erc_etcc_column_count_exists_last_row_semantics_count_sum. ((((exists ff_h_erc_etcc_column_count_exists_last_row_semantics_count_sum_summand. ff_h_erc_etcc_column_count_exists_last_row_semantics_count_sum_summand + S (ff_a_erc_etcc_column_count_exists_last_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_column_count_exists_last_row_semantics_count_sum)) * erc_row_scale_etcc_column_count_exists_last_row_semantics)) /\ exists ff_q_erc_etcc_column_count_exists_last_row_semantics_count_sum_summand. erc_row_code_etcc_column_count_exists_last_row_semantics = ff_q_erc_etcc_column_count_exists_last_row_semantics_count_sum_summand * S ((S (ff_i_erc_etcc_column_count_exists_last_row_semantics_count_sum)) * erc_row_scale_etcc_column_count_exists_last_row_semantics) + (ff_a_erc_etcc_column_count_exists_last_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_column_count_exists_last_row_semantics_count_sum_partial. ff_h_erc_etcc_column_count_exists_last_row_semantics_count_sum_partial + S (ff_r_erc_etcc_column_count_exists_last_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_column_count_exists_last_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_last_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_last_row_semantics_count_sum_partial. ff_u_erc_etcc_column_count_exists_last_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_last_row_semantics_count_sum_partial * S ((S (ff_i_erc_etcc_column_count_exists_last_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_last_row_semantics_count_sum) + (ff_r_erc_etcc_column_count_exists_last_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_column_count_exists_last_row_semantics_count_sum_successor. ff_h_erc_etcc_column_count_exists_last_row_semantics_count_sum_successor + S (ff_s_erc_etcc_column_count_exists_last_row_semantics_count_sum) = S ((S (S ff_i_erc_etcc_column_count_exists_last_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_last_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_last_row_semantics_count_sum_successor. ff_u_erc_etcc_column_count_exists_last_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_last_row_semantics_count_sum_successor * S ((S (S ff_i_erc_etcc_column_count_exists_last_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_last_row_semantics_count_sum) + (ff_s_erc_etcc_column_count_exists_last_row_semantics_count_sum))) /\ ff_s_erc_etcc_column_count_exists_last_row_semantics_count_sum = ff_r_erc_etcc_column_count_exists_last_row_semantics_count_sum + ff_a_erc_etcc_column_count_exists_last_row_semantics_count_sum)))))) /\ (forall ff_i_erc_etcc_column_count_exists_last_row_semantics_count_bits. (exists ff_lt_erc_etcc_column_count_exists_last_row_semantics_count_bits_bound. ff_lt_erc_etcc_column_count_exists_last_row_semantics_count_bits_bound + S ff_i_erc_etcc_column_count_exists_last_row_semantics_count_bits = k) -> exists ff_bit_erc_etcc_column_count_exists_last_row_semantics_count_bits. ((((exists ff_h_erc_etcc_column_count_exists_last_row_semantics_count_bits_decoded. ff_h_erc_etcc_column_count_exists_last_row_semantics_count_bits_decoded + S (ff_bit_erc_etcc_column_count_exists_last_row_semantics_count_bits) = S ((S (ff_i_erc_etcc_column_count_exists_last_row_semantics_count_bits)) * erc_row_scale_etcc_column_count_exists_last_row_semantics)) /\ exists ff_q_erc_etcc_column_count_exists_last_row_semantics_count_bits_decoded. erc_row_code_etcc_column_count_exists_last_row_semantics = ff_q_erc_etcc_column_count_exists_last_row_semantics_count_bits_decoded * S ((S (ff_i_erc_etcc_column_count_exists_last_row_semantics_count_bits)) * erc_row_scale_etcc_column_count_exists_last_row_semantics) + (ff_bit_erc_etcc_column_count_exists_last_row_semantics_count_bits))) /\ (ff_bit_erc_etcc_column_count_exists_last_row_semantics_count_bits = 0 \/ ff_bit_erc_etcc_column_count_exists_last_row_semantics_count_bits = 1)))))))) /\ (forall etc_row_index_etcc_column_count_exists_last_column. (exists edt_lt_gap_etcc_column_count_exists_last_column_bound. edt_lt_gap_etcc_column_count_exists_last_column_bound + S (etc_row_index_etcc_column_count_exists_last_column) = k) -> exists etc_bit_etcc_column_count_exists_last_column. ((((exists ff_h_etc_etcc_column_count_exists_last_column_decoded. ff_h_etc_etcc_column_count_exists_last_column_decoded + S (etc_bit_etcc_column_count_exists_last_column) = S ((S (etc_row_index_etcc_column_count_exists_last_column)) * etcc_column_scale_column_count_exists_last)) /\ exists ff_q_etc_etcc_column_count_exists_last_column_decoded. etcc_column_code_column_count_exists_last = ff_q_etc_etcc_column_count_exists_last_column_decoded * S ((S (etc_row_index_etcc_column_count_exists_last_column)) * etcc_column_scale_column_count_exists_last) + (etc_bit_etcc_column_count_exists_last_column))) /\ (exists etc_count_etcc_column_count_exists_last_column_witness etc_row_code_etcc_column_count_exists_last_column_witness etc_row_scale_etcc_column_count_exists_last_column_witness. ((((((exists ff_h_etc_etcc_column_count_exists_last_column_witness_outer_entry. ff_h_etc_etcc_column_count_exists_last_column_witness_outer_entry + S (etc_count_etcc_column_count_exists_last_column_witness) = S ((S (etc_row_index_etcc_column_count_exists_last_column)) * bc)) /\ exists ff_q_etc_etcc_column_count_exists_last_column_witness_outer_entry. bb = ff_q_etc_etcc_column_count_exists_last_column_witness_outer_entry * S ((S (etc_row_index_etcc_column_count_exists_last_column)) * bc) + (etc_count_etcc_column_count_exists_last_column_witness))) /\ (forall eri_column_etc_etcc_column_count_exists_last_column_witness_row. (exists eri_gap_etc_etcc_column_count_exists_last_column_witness_row_bound. eri_gap_etc_etcc_column_count_exists_last_column_witness_row_bound + S (eri_column_etc_etcc_column_count_exists_last_column_witness_row) = h) -> exists eri_bit_etc_etcc_column_count_exists_last_column_witness_row. ((((exists ff_h_eri_etc_etcc_column_count_exists_last_column_witness_row_decoded. ff_h_eri_etc_etcc_column_count_exists_last_column_witness_row_decoded + S (eri_bit_etc_etcc_column_count_exists_last_column_witness_row) = S ((S (eri_column_etc_etcc_column_count_exists_last_column_witness_row)) * etc_row_scale_etcc_column_count_exists_last_column_witness)) /\ exists ff_q_eri_etc_etcc_column_count_exists_last_column_witness_row_decoded. etc_row_code_etcc_column_count_exists_last_column_witness = ff_q_eri_etc_etcc_column_count_exists_last_column_witness_row_decoded * S ((S (eri_column_etc_etcc_column_count_exists_last_column_witness_row)) * etc_row_scale_etcc_column_count_exists_last_column_witness) + (eri_bit_etc_etcc_column_count_exists_last_column_witness_row))) /\ (((eri_bit_etc_etcc_column_count_exists_last_column_witness_row = 0 /\ ((exists eri_gap_etc_etcc_column_count_exists_last_column_witness_row_choice_left. eri_gap_etc_etcc_column_count_exists_last_column_witness_row_choice_left + S (p * S etc_row_index_etcc_column_count_exists_last_column) = q * S eri_column_etc_etcc_column_count_exists_last_column_witness_row) /\ ~(exists eri_gap_etc_etcc_column_count_exists_last_column_witness_row_choice_right. eri_gap_etc_etcc_column_count_exists_last_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_column_count_exists_last_column_witness_row) = p * S etc_row_index_etcc_column_count_exists_last_column))) \/ (eri_bit_etc_etcc_column_count_exists_last_column_witness_row = 1 /\ ((exists eri_gap_etc_etcc_column_count_exists_last_column_witness_row_choice_right. eri_gap_etc_etcc_column_count_exists_last_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_column_count_exists_last_column_witness_row) = p * S etc_row_index_etcc_column_count_exists_last_column) /\ ~(exists eri_gap_etc_etcc_column_count_exists_last_column_witness_row_choice_left. eri_gap_etc_etcc_column_count_exists_last_column_witness_row_choice_left + S (p * S etc_row_index_etcc_column_count_exists_last_column) = q * S eri_column_etc_etcc_column_count_exists_last_column_witness_row)))))))) /\ (((exists ff_u_etc_etcc_column_count_exists_last_column_witness_count_relation_sum ff_v_etc_etcc_column_count_exists_last_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_start. ff_h_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_etcc_column_count_exists_last_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_start. ff_u_etc_etcc_column_count_exists_last_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_etcc_column_count_exists_last_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_terminal. ff_h_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_terminal + S (etc_count_etcc_column_count_exists_last_column_witness) = S ((S (h)) * ff_v_etc_etcc_column_count_exists_last_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_terminal. ff_u_etc_etcc_column_count_exists_last_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_etcc_column_count_exists_last_column_witness_count_relation_sum) + (etc_count_etcc_column_count_exists_last_column_witness))) /\ forall ff_i_etc_etcc_column_count_exists_last_column_witness_count_relation_sum. (exists ff_lt_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_bound. ff_lt_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_bound + S ff_i_etc_etcc_column_count_exists_last_column_witness_count_relation_sum = h) -> exists ff_a_etc_etcc_column_count_exists_last_column_witness_count_relation_sum ff_r_etc_etcc_column_count_exists_last_column_witness_count_relation_sum ff_s_etc_etcc_column_count_exists_last_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_summand. ff_h_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_summand + S (ff_a_etc_etcc_column_count_exists_last_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_column_count_exists_last_column_witness_count_relation_sum)) * etc_row_scale_etcc_column_count_exists_last_column_witness)) /\ exists ff_q_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_summand. etc_row_code_etcc_column_count_exists_last_column_witness = ff_q_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_etcc_column_count_exists_last_column_witness_count_relation_sum)) * etc_row_scale_etcc_column_count_exists_last_column_witness) + (ff_a_etc_etcc_column_count_exists_last_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_partial. ff_h_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_partial + S (ff_r_etc_etcc_column_count_exists_last_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_column_count_exists_last_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_last_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_partial. ff_u_etc_etcc_column_count_exists_last_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_etcc_column_count_exists_last_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_last_column_witness_count_relation_sum) + (ff_r_etc_etcc_column_count_exists_last_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_successor. ff_h_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_successor + S (ff_s_etc_etcc_column_count_exists_last_column_witness_count_relation_sum) = S ((S (S ff_i_etc_etcc_column_count_exists_last_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_last_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_successor. ff_u_etc_etcc_column_count_exists_last_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_last_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_etcc_column_count_exists_last_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_last_column_witness_count_relation_sum) + (ff_s_etc_etcc_column_count_exists_last_column_witness_count_relation_sum))) /\ ff_s_etc_etcc_column_count_exists_last_column_witness_count_relation_sum = ff_r_etc_etcc_column_count_exists_last_column_witness_count_relation_sum + ff_a_etc_etcc_column_count_exists_last_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_etcc_column_count_exists_last_column_witness_count_relation_bits. (exists ff_lt_etc_etcc_column_count_exists_last_column_witness_count_relation_bits_bound. ff_lt_etc_etcc_column_count_exists_last_column_witness_count_relation_bits_bound + S ff_i_etc_etcc_column_count_exists_last_column_witness_count_relation_bits = h) -> exists ff_bit_etc_etcc_column_count_exists_last_column_witness_count_relation_bits. ((((exists ff_h_etc_etcc_column_count_exists_last_column_witness_count_relation_bits_decoded. ff_h_etc_etcc_column_count_exists_last_column_witness_count_relation_bits_decoded + S (ff_bit_etc_etcc_column_count_exists_last_column_witness_count_relation_bits) = S ((S (ff_i_etc_etcc_column_count_exists_last_column_witness_count_relation_bits)) * etc_row_scale_etcc_column_count_exists_last_column_witness)) /\ exists ff_q_etc_etcc_column_count_exists_last_column_witness_count_relation_bits_decoded. etc_row_code_etcc_column_count_exists_last_column_witness = ff_q_etc_etcc_column_count_exists_last_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_etcc_column_count_exists_last_column_witness_count_relation_bits)) * etc_row_scale_etcc_column_count_exists_last_column_witness) + (ff_bit_etc_etcc_column_count_exists_last_column_witness_count_relation_bits))) /\ (ff_bit_etc_etcc_column_count_exists_last_column_witness_count_relation_bits = 0 \/ ff_bit_etc_etcc_column_count_exists_last_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_etcc_column_count_exists_last_column_witness_inner_entry. ff_h_etc_etcc_column_count_exists_last_column_witness_inner_entry + S (etc_bit_etcc_column_count_exists_last_column) = S ((S (l)) * etc_row_scale_etcc_column_count_exists_last_column_witness)) /\ exists ff_q_etc_etcc_column_count_exists_last_column_witness_inner_entry. etc_row_code_etcc_column_count_exists_last_column_witness = ff_q_etc_etcc_column_count_exists_last_column_witness_inner_entry * S ((S (l)) * etc_row_scale_etcc_column_count_exists_last_column_witness) + (etc_bit_etcc_column_count_exists_last_column)))))))) /\ ((((exists ff_u_etcc_column_count_exists_last_column_count_sum ff_v_etcc_column_count_exists_last_column_count_sum. ((((exists ff_h_etcc_column_count_exists_last_column_count_sum_start. ff_h_etcc_column_count_exists_last_column_count_sum_start + S (0) = S ((S (0)) * ff_v_etcc_column_count_exists_last_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_last_column_count_sum_start. ff_u_etcc_column_count_exists_last_column_count_sum = ff_q_etcc_column_count_exists_last_column_count_sum_start * S ((S (0)) * ff_v_etcc_column_count_exists_last_column_count_sum) + (0))) /\ ((((exists ff_h_etcc_column_count_exists_last_column_count_sum_terminal. ff_h_etcc_column_count_exists_last_column_count_sum_terminal + S (m) = S ((S (k)) * ff_v_etcc_column_count_exists_last_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_last_column_count_sum_terminal. ff_u_etcc_column_count_exists_last_column_count_sum = ff_q_etcc_column_count_exists_last_column_count_sum_terminal * S ((S (k)) * ff_v_etcc_column_count_exists_last_column_count_sum) + (m))) /\ forall ff_i_etcc_column_count_exists_last_column_count_sum. (exists ff_lt_etcc_column_count_exists_last_column_count_sum_bound. ff_lt_etcc_column_count_exists_last_column_count_sum_bound + S ff_i_etcc_column_count_exists_last_column_count_sum = k) -> exists ff_a_etcc_column_count_exists_last_column_count_sum ff_r_etcc_column_count_exists_last_column_count_sum ff_s_etcc_column_count_exists_last_column_count_sum. ((((exists ff_h_etcc_column_count_exists_last_column_count_sum_summand. ff_h_etcc_column_count_exists_last_column_count_sum_summand + S (ff_a_etcc_column_count_exists_last_column_count_sum) = S ((S (ff_i_etcc_column_count_exists_last_column_count_sum)) * etcc_column_scale_column_count_exists_last)) /\ exists ff_q_etcc_column_count_exists_last_column_count_sum_summand. etcc_column_code_column_count_exists_last = ff_q_etcc_column_count_exists_last_column_count_sum_summand * S ((S (ff_i_etcc_column_count_exists_last_column_count_sum)) * etcc_column_scale_column_count_exists_last) + (ff_a_etcc_column_count_exists_last_column_count_sum))) /\ ((((exists ff_h_etcc_column_count_exists_last_column_count_sum_partial. ff_h_etcc_column_count_exists_last_column_count_sum_partial + S (ff_r_etcc_column_count_exists_last_column_count_sum) = S ((S (ff_i_etcc_column_count_exists_last_column_count_sum)) * ff_v_etcc_column_count_exists_last_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_last_column_count_sum_partial. ff_u_etcc_column_count_exists_last_column_count_sum = ff_q_etcc_column_count_exists_last_column_count_sum_partial * S ((S (ff_i_etcc_column_count_exists_last_column_count_sum)) * ff_v_etcc_column_count_exists_last_column_count_sum) + (ff_r_etcc_column_count_exists_last_column_count_sum))) /\ ((((exists ff_h_etcc_column_count_exists_last_column_count_sum_successor. ff_h_etcc_column_count_exists_last_column_count_sum_successor + S (ff_s_etcc_column_count_exists_last_column_count_sum) = S ((S (S ff_i_etcc_column_count_exists_last_column_count_sum)) * ff_v_etcc_column_count_exists_last_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_last_column_count_sum_successor. ff_u_etcc_column_count_exists_last_column_count_sum = ff_q_etcc_column_count_exists_last_column_count_sum_successor * S ((S (S ff_i_etcc_column_count_exists_last_column_count_sum)) * ff_v_etcc_column_count_exists_last_column_count_sum) + (ff_s_etcc_column_count_exists_last_column_count_sum))) /\ ff_s_etcc_column_count_exists_last_column_count_sum = ff_r_etcc_column_count_exists_last_column_count_sum + ff_a_etcc_column_count_exists_last_column_count_sum)))))) /\ (forall ff_i_etcc_column_count_exists_last_column_count_bits. (exists ff_lt_etcc_column_count_exists_last_column_count_bits_bound. ff_lt_etcc_column_count_exists_last_column_count_bits_bound + S ff_i_etcc_column_count_exists_last_column_count_bits = k) -> exists ff_bit_etcc_column_count_exists_last_column_count_bits. ((((exists ff_h_etcc_column_count_exists_last_column_count_bits_decoded. ff_h_etcc_column_count_exists_last_column_count_bits_decoded + S (ff_bit_etcc_column_count_exists_last_column_count_bits) = S ((S (ff_i_etcc_column_count_exists_last_column_count_bits)) * etcc_column_scale_column_count_exists_last)) /\ exists ff_q_etcc_column_count_exists_last_column_count_bits_decoded. etcc_column_code_column_count_exists_last = ff_q_etcc_column_count_exists_last_column_count_bits_decoded * S ((S (ff_i_etcc_column_count_exists_last_column_count_bits)) * etcc_column_scale_column_count_exists_last) + (ff_bit_etcc_column_count_exists_last_column_count_bits))) /\ (ff_bit_etcc_column_count_exists_last_column_count_bits = 0 \/ ff_bit_etcc_column_count_exists_last_column_count_bits = 1))))) /\ etcc_row_count_column_count_exists_last + m = k)))
41. 0041specialize hchoices l
42. 0042apply hchoices
43. 0043specialize le_refl (S l)
44. 0044exact le_refl
45. 0045have hnext : exists db dc. (forall etcc_row_index_column_count_exists_successor. (exists edt_lt_gap_column_count_exists_successor_bound. edt_lt_gap_column_count_exists_successor_bound + S (etcc_row_index_column_count_exists_successor) = S l) -> exists etcc_count_column_count_exists_successor. ((((exists ff_h_etcc_column_count_exists_successor_decoded. ff_h_etcc_column_count_exists_successor_decoded + S (etcc_count_column_count_exists_successor) = S ((S (etcc_row_index_column_count_exists_successor)) * dc)) /\ exists ff_q_etcc_column_count_exists_successor_decoded. db = ff_q_etcc_column_count_exists_successor_decoded * S ((S (etcc_row_index_column_count_exists_successor)) * dc) + (etcc_count_column_count_exists_successor))) /\ (exists etcc_row_count_column_count_exists_successor_witness etcc_column_code_column_count_exists_successor_witness etcc_column_scale_column_count_exists_successor_witness. ((((((exists ff_h_etcc_column_count_exists_successor_witness_first_entry. ff_h_etcc_column_count_exists_successor_witness_first_entry + S (etcc_row_count_column_count_exists_successor_witness) = S ((S (etcc_row_index_column_count_exists_successor)) * ac)) /\ exists ff_q_etcc_column_count_exists_successor_witness_first_entry. ab = ff_q_etcc_column_count_exists_successor_witness_first_entry * S ((S (etcc_row_index_column_count_exists_successor)) * ac) + (etcc_row_count_column_count_exists_successor_witness))) /\ (exists erc_row_code_etcc_column_count_exists_successor_witness_row_semantics erc_row_scale_etcc_column_count_exists_successor_witness_row_semantics. ((forall eri_column_erc_etcc_column_count_exists_successor_witness_row_semantics_row. (exists eri_gap_erc_etcc_column_count_exists_successor_witness_row_semantics_row_bound. eri_gap_erc_etcc_column_count_exists_successor_witness_row_semantics_row_bound + S (eri_column_erc_etcc_column_count_exists_successor_witness_row_semantics_row) = k) -> exists eri_bit_erc_etcc_column_count_exists_successor_witness_row_semantics_row. ((((exists ff_h_eri_erc_etcc_column_count_exists_successor_witness_row_semantics_row_decoded. ff_h_eri_erc_etcc_column_count_exists_successor_witness_row_semantics_row_decoded + S (eri_bit_erc_etcc_column_count_exists_successor_witness_row_semantics_row) = S ((S (eri_column_erc_etcc_column_count_exists_successor_witness_row_semantics_row)) * erc_row_scale_etcc_column_count_exists_successor_witness_row_semantics)) /\ exists ff_q_eri_erc_etcc_column_count_exists_successor_witness_row_semantics_row_decoded. erc_row_code_etcc_column_count_exists_successor_witness_row_semantics = ff_q_eri_erc_etcc_column_count_exists_successor_witness_row_semantics_row_decoded * S ((S (eri_column_erc_etcc_column_count_exists_successor_witness_row_semantics_row)) * erc_row_scale_etcc_column_count_exists_successor_witness_row_semantics) + (eri_bit_erc_etcc_column_count_exists_successor_witness_row_semantics_row))) /\ (((eri_bit_erc_etcc_column_count_exists_successor_witness_row_semantics_row = 0 /\ ((exists eri_gap_erc_etcc_column_count_exists_successor_witness_row_semantics_row_choice_left. eri_gap_erc_etcc_column_count_exists_successor_witness_row_semantics_row_choice_left + S (q * S etcc_row_index_column_count_exists_successor) = p * S eri_column_erc_etcc_column_count_exists_successor_witness_row_semantics_row) /\ ~(exists eri_gap_erc_etcc_column_count_exists_successor_witness_row_semantics_row_choice_right. eri_gap_erc_etcc_column_count_exists_successor_witness_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_column_count_exists_successor_witness_row_semantics_row) = q * S etcc_row_index_column_count_exists_successor))) \/ (eri_bit_erc_etcc_column_count_exists_successor_witness_row_semantics_row = 1 /\ ((exists eri_gap_erc_etcc_column_count_exists_successor_witness_row_semantics_row_choice_right. eri_gap_erc_etcc_column_count_exists_successor_witness_row_semantics_row_choice_right + S (p * S eri_column_erc_etcc_column_count_exists_successor_witness_row_semantics_row) = q * S etcc_row_index_column_count_exists_successor) /\ ~(exists eri_gap_erc_etcc_column_count_exists_successor_witness_row_semantics_row_choice_left. eri_gap_erc_etcc_column_count_exists_successor_witness_row_semantics_row_choice_left + S (q * S etcc_row_index_column_count_exists_successor) = p * S eri_column_erc_etcc_column_count_exists_successor_witness_row_semantics_row))))))) /\ (((exists ff_u_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum ff_v_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum. ((((exists ff_h_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_start. ff_h_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_start. ff_u_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_start * S ((S (0)) * ff_v_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum) + (0))) /\ ((((exists ff_h_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_terminal. ff_h_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_terminal + S (etcc_row_count_column_count_exists_successor_witness) = S ((S (k)) * ff_v_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_terminal. ff_u_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_terminal * S ((S (k)) * ff_v_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum) + (etcc_row_count_column_count_exists_successor_witness))) /\ forall ff_i_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum. (exists ff_lt_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_bound. ff_lt_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_bound + S ff_i_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum = k) -> exists ff_a_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum ff_r_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum ff_s_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum. ((((exists ff_h_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_summand. ff_h_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_summand + S (ff_a_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum)) * erc_row_scale_etcc_column_count_exists_successor_witness_row_semantics)) /\ exists ff_q_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_summand. erc_row_code_etcc_column_count_exists_successor_witness_row_semantics = ff_q_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_summand * S ((S (ff_i_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum)) * erc_row_scale_etcc_column_count_exists_successor_witness_row_semantics) + (ff_a_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_partial. ff_h_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_partial + S (ff_r_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum) = S ((S (ff_i_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_partial. ff_u_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_partial * S ((S (ff_i_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum) + (ff_r_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum))) /\ ((((exists ff_h_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_successor. ff_h_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_successor + S (ff_s_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum) = S ((S (S ff_i_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum)) /\ exists ff_q_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_successor. ff_u_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum = ff_q_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum_successor * S ((S (S ff_i_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum)) * ff_v_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum) + (ff_s_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum))) /\ ff_s_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum = ff_r_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum + ff_a_erc_etcc_column_count_exists_successor_witness_row_semantics_count_sum)))))) /\ (forall ff_i_erc_etcc_column_count_exists_successor_witness_row_semantics_count_bits. (exists ff_lt_erc_etcc_column_count_exists_successor_witness_row_semantics_count_bits_bound. ff_lt_erc_etcc_column_count_exists_successor_witness_row_semantics_count_bits_bound + S ff_i_erc_etcc_column_count_exists_successor_witness_row_semantics_count_bits = k) -> exists ff_bit_erc_etcc_column_count_exists_successor_witness_row_semantics_count_bits. ((((exists ff_h_erc_etcc_column_count_exists_successor_witness_row_semantics_count_bits_decoded. ff_h_erc_etcc_column_count_exists_successor_witness_row_semantics_count_bits_decoded + S (ff_bit_erc_etcc_column_count_exists_successor_witness_row_semantics_count_bits) = S ((S (ff_i_erc_etcc_column_count_exists_successor_witness_row_semantics_count_bits)) * erc_row_scale_etcc_column_count_exists_successor_witness_row_semantics)) /\ exists ff_q_erc_etcc_column_count_exists_successor_witness_row_semantics_count_bits_decoded. erc_row_code_etcc_column_count_exists_successor_witness_row_semantics = ff_q_erc_etcc_column_count_exists_successor_witness_row_semantics_count_bits_decoded * S ((S (ff_i_erc_etcc_column_count_exists_successor_witness_row_semantics_count_bits)) * erc_row_scale_etcc_column_count_exists_successor_witness_row_semantics) + (ff_bit_erc_etcc_column_count_exists_successor_witness_row_semantics_count_bits))) /\ (ff_bit_erc_etcc_column_count_exists_successor_witness_row_semantics_count_bits = 0 \/ ff_bit_erc_etcc_column_count_exists_successor_witness_row_semantics_count_bits = 1)))))))) /\ (forall etc_row_index_etcc_column_count_exists_successor_witness_column. (exists edt_lt_gap_etcc_column_count_exists_successor_witness_column_bound. edt_lt_gap_etcc_column_count_exists_successor_witness_column_bound + S (etc_row_index_etcc_column_count_exists_successor_witness_column) = k) -> exists etc_bit_etcc_column_count_exists_successor_witness_column. ((((exists ff_h_etc_etcc_column_count_exists_successor_witness_column_decoded. ff_h_etc_etcc_column_count_exists_successor_witness_column_decoded + S (etc_bit_etcc_column_count_exists_successor_witness_column) = S ((S (etc_row_index_etcc_column_count_exists_successor_witness_column)) * etcc_column_scale_column_count_exists_successor_witness)) /\ exists ff_q_etc_etcc_column_count_exists_successor_witness_column_decoded. etcc_column_code_column_count_exists_successor_witness = ff_q_etc_etcc_column_count_exists_successor_witness_column_decoded * S ((S (etc_row_index_etcc_column_count_exists_successor_witness_column)) * etcc_column_scale_column_count_exists_successor_witness) + (etc_bit_etcc_column_count_exists_successor_witness_column))) /\ (exists etc_count_etcc_column_count_exists_successor_witness_column_witness etc_row_code_etcc_column_count_exists_successor_witness_column_witness etc_row_scale_etcc_column_count_exists_successor_witness_column_witness. ((((((exists ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_outer_entry. ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_outer_entry + S (etc_count_etcc_column_count_exists_successor_witness_column_witness) = S ((S (etc_row_index_etcc_column_count_exists_successor_witness_column)) * bc)) /\ exists ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_outer_entry. bb = ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_outer_entry * S ((S (etc_row_index_etcc_column_count_exists_successor_witness_column)) * bc) + (etc_count_etcc_column_count_exists_successor_witness_column_witness))) /\ (forall eri_column_etc_etcc_column_count_exists_successor_witness_column_witness_row. (exists eri_gap_etc_etcc_column_count_exists_successor_witness_column_witness_row_bound. eri_gap_etc_etcc_column_count_exists_successor_witness_column_witness_row_bound + S (eri_column_etc_etcc_column_count_exists_successor_witness_column_witness_row) = h) -> exists eri_bit_etc_etcc_column_count_exists_successor_witness_column_witness_row. ((((exists ff_h_eri_etc_etcc_column_count_exists_successor_witness_column_witness_row_decoded. ff_h_eri_etc_etcc_column_count_exists_successor_witness_column_witness_row_decoded + S (eri_bit_etc_etcc_column_count_exists_successor_witness_column_witness_row) = S ((S (eri_column_etc_etcc_column_count_exists_successor_witness_column_witness_row)) * etc_row_scale_etcc_column_count_exists_successor_witness_column_witness)) /\ exists ff_q_eri_etc_etcc_column_count_exists_successor_witness_column_witness_row_decoded. etc_row_code_etcc_column_count_exists_successor_witness_column_witness = ff_q_eri_etc_etcc_column_count_exists_successor_witness_column_witness_row_decoded * S ((S (eri_column_etc_etcc_column_count_exists_successor_witness_column_witness_row)) * etc_row_scale_etcc_column_count_exists_successor_witness_column_witness) + (eri_bit_etc_etcc_column_count_exists_successor_witness_column_witness_row))) /\ (((eri_bit_etc_etcc_column_count_exists_successor_witness_column_witness_row = 0 /\ ((exists eri_gap_etc_etcc_column_count_exists_successor_witness_column_witness_row_choice_left. eri_gap_etc_etcc_column_count_exists_successor_witness_column_witness_row_choice_left + S (p * S etc_row_index_etcc_column_count_exists_successor_witness_column) = q * S eri_column_etc_etcc_column_count_exists_successor_witness_column_witness_row) /\ ~(exists eri_gap_etc_etcc_column_count_exists_successor_witness_column_witness_row_choice_right. eri_gap_etc_etcc_column_count_exists_successor_witness_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_column_count_exists_successor_witness_column_witness_row) = p * S etc_row_index_etcc_column_count_exists_successor_witness_column))) \/ (eri_bit_etc_etcc_column_count_exists_successor_witness_column_witness_row = 1 /\ ((exists eri_gap_etc_etcc_column_count_exists_successor_witness_column_witness_row_choice_right. eri_gap_etc_etcc_column_count_exists_successor_witness_column_witness_row_choice_right + S (q * S eri_column_etc_etcc_column_count_exists_successor_witness_column_witness_row) = p * S etc_row_index_etcc_column_count_exists_successor_witness_column) /\ ~(exists eri_gap_etc_etcc_column_count_exists_successor_witness_column_witness_row_choice_left. eri_gap_etc_etcc_column_count_exists_successor_witness_column_witness_row_choice_left + S (p * S etc_row_index_etcc_column_count_exists_successor_witness_column) = q * S eri_column_etc_etcc_column_count_exists_successor_witness_column_witness_row)))))))) /\ (((exists ff_u_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum ff_v_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_start. ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_start. ff_u_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_terminal. ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_terminal + S (etc_count_etcc_column_count_exists_successor_witness_column_witness) = S ((S (h)) * ff_v_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_terminal. ff_u_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum) + (etc_count_etcc_column_count_exists_successor_witness_column_witness))) /\ forall ff_i_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum. (exists ff_lt_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_bound. ff_lt_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_bound + S ff_i_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum = h) -> exists ff_a_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum ff_r_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum ff_s_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum. ((((exists ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_summand. ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_summand + S (ff_a_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum)) * etc_row_scale_etcc_column_count_exists_successor_witness_column_witness)) /\ exists ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_summand. etc_row_code_etcc_column_count_exists_successor_witness_column_witness = ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_summand * S ((S (ff_i_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum)) * etc_row_scale_etcc_column_count_exists_successor_witness_column_witness) + (ff_a_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_partial. ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_partial + S (ff_r_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum) = S ((S (ff_i_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_partial. ff_u_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_partial * S ((S (ff_i_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum) + (ff_r_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum))) /\ ((((exists ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_successor. ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_successor + S (ff_s_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum) = S ((S (S ff_i_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum)) /\ exists ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_successor. ff_u_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum = ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum_successor * S ((S (S ff_i_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum)) * ff_v_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum) + (ff_s_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum))) /\ ff_s_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum = ff_r_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum + ff_a_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_sum)))))) /\ (forall ff_i_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_bits. (exists ff_lt_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_bits_bound. ff_lt_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_bits_bound + S ff_i_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_bits = h) -> exists ff_bit_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_bits. ((((exists ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_bits_decoded. ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_bits_decoded + S (ff_bit_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_bits) = S ((S (ff_i_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_bits)) * etc_row_scale_etcc_column_count_exists_successor_witness_column_witness)) /\ exists ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_bits_decoded. etc_row_code_etcc_column_count_exists_successor_witness_column_witness = ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_bits_decoded * S ((S (ff_i_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_bits)) * etc_row_scale_etcc_column_count_exists_successor_witness_column_witness) + (ff_bit_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_bits))) /\ (ff_bit_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_bits = 0 \/ ff_bit_etc_etcc_column_count_exists_successor_witness_column_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_inner_entry. ff_h_etc_etcc_column_count_exists_successor_witness_column_witness_inner_entry + S (etc_bit_etcc_column_count_exists_successor_witness_column) = S ((S (etcc_row_index_column_count_exists_successor)) * etc_row_scale_etcc_column_count_exists_successor_witness_column_witness)) /\ exists ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_inner_entry. etc_row_code_etcc_column_count_exists_successor_witness_column_witness = ff_q_etc_etcc_column_count_exists_successor_witness_column_witness_inner_entry * S ((S (etcc_row_index_column_count_exists_successor)) * etc_row_scale_etcc_column_count_exists_successor_witness_column_witness) + (etc_bit_etcc_column_count_exists_successor_witness_column)))))))) /\ ((((exists ff_u_etcc_column_count_exists_successor_witness_column_count_sum ff_v_etcc_column_count_exists_successor_witness_column_count_sum. ((((exists ff_h_etcc_column_count_exists_successor_witness_column_count_sum_start. ff_h_etcc_column_count_exists_successor_witness_column_count_sum_start + S (0) = S ((S (0)) * ff_v_etcc_column_count_exists_successor_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_successor_witness_column_count_sum_start. ff_u_etcc_column_count_exists_successor_witness_column_count_sum = ff_q_etcc_column_count_exists_successor_witness_column_count_sum_start * S ((S (0)) * ff_v_etcc_column_count_exists_successor_witness_column_count_sum) + (0))) /\ ((((exists ff_h_etcc_column_count_exists_successor_witness_column_count_sum_terminal. ff_h_etcc_column_count_exists_successor_witness_column_count_sum_terminal + S (etcc_count_column_count_exists_successor) = S ((S (k)) * ff_v_etcc_column_count_exists_successor_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_successor_witness_column_count_sum_terminal. ff_u_etcc_column_count_exists_successor_witness_column_count_sum = ff_q_etcc_column_count_exists_successor_witness_column_count_sum_terminal * S ((S (k)) * ff_v_etcc_column_count_exists_successor_witness_column_count_sum) + (etcc_count_column_count_exists_successor))) /\ forall ff_i_etcc_column_count_exists_successor_witness_column_count_sum. (exists ff_lt_etcc_column_count_exists_successor_witness_column_count_sum_bound. ff_lt_etcc_column_count_exists_successor_witness_column_count_sum_bound + S ff_i_etcc_column_count_exists_successor_witness_column_count_sum = k) -> exists ff_a_etcc_column_count_exists_successor_witness_column_count_sum ff_r_etcc_column_count_exists_successor_witness_column_count_sum ff_s_etcc_column_count_exists_successor_witness_column_count_sum. ((((exists ff_h_etcc_column_count_exists_successor_witness_column_count_sum_summand. ff_h_etcc_column_count_exists_successor_witness_column_count_sum_summand + S (ff_a_etcc_column_count_exists_successor_witness_column_count_sum) = S ((S (ff_i_etcc_column_count_exists_successor_witness_column_count_sum)) * etcc_column_scale_column_count_exists_successor_witness)) /\ exists ff_q_etcc_column_count_exists_successor_witness_column_count_sum_summand. etcc_column_code_column_count_exists_successor_witness = ff_q_etcc_column_count_exists_successor_witness_column_count_sum_summand * S ((S (ff_i_etcc_column_count_exists_successor_witness_column_count_sum)) * etcc_column_scale_column_count_exists_successor_witness) + (ff_a_etcc_column_count_exists_successor_witness_column_count_sum))) /\ ((((exists ff_h_etcc_column_count_exists_successor_witness_column_count_sum_partial. ff_h_etcc_column_count_exists_successor_witness_column_count_sum_partial + S (ff_r_etcc_column_count_exists_successor_witness_column_count_sum) = S ((S (ff_i_etcc_column_count_exists_successor_witness_column_count_sum)) * ff_v_etcc_column_count_exists_successor_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_successor_witness_column_count_sum_partial. ff_u_etcc_column_count_exists_successor_witness_column_count_sum = ff_q_etcc_column_count_exists_successor_witness_column_count_sum_partial * S ((S (ff_i_etcc_column_count_exists_successor_witness_column_count_sum)) * ff_v_etcc_column_count_exists_successor_witness_column_count_sum) + (ff_r_etcc_column_count_exists_successor_witness_column_count_sum))) /\ ((((exists ff_h_etcc_column_count_exists_successor_witness_column_count_sum_successor. ff_h_etcc_column_count_exists_successor_witness_column_count_sum_successor + S (ff_s_etcc_column_count_exists_successor_witness_column_count_sum) = S ((S (S ff_i_etcc_column_count_exists_successor_witness_column_count_sum)) * ff_v_etcc_column_count_exists_successor_witness_column_count_sum)) /\ exists ff_q_etcc_column_count_exists_successor_witness_column_count_sum_successor. ff_u_etcc_column_count_exists_successor_witness_column_count_sum = ff_q_etcc_column_count_exists_successor_witness_column_count_sum_successor * S ((S (S ff_i_etcc_column_count_exists_successor_witness_column_count_sum)) * ff_v_etcc_column_count_exists_successor_witness_column_count_sum) + (ff_s_etcc_column_count_exists_successor_witness_column_count_sum))) /\ ff_s_etcc_column_count_exists_successor_witness_column_count_sum = ff_r_etcc_column_count_exists_successor_witness_column_count_sum + ff_a_etcc_column_count_exists_successor_witness_column_count_sum)))))) /\ (forall ff_i_etcc_column_count_exists_successor_witness_column_count_bits. (exists ff_lt_etcc_column_count_exists_successor_witness_column_count_bits_bound. ff_lt_etcc_column_count_exists_successor_witness_column_count_bits_bound + S ff_i_etcc_column_count_exists_successor_witness_column_count_bits = k) -> exists ff_bit_etcc_column_count_exists_successor_witness_column_count_bits. ((((exists ff_h_etcc_column_count_exists_successor_witness_column_count_bits_decoded. ff_h_etcc_column_count_exists_successor_witness_column_count_bits_decoded + S (ff_bit_etcc_column_count_exists_successor_witness_column_count_bits) = S ((S (ff_i_etcc_column_count_exists_successor_witness_column_count_bits)) * etcc_column_scale_column_count_exists_successor_witness)) /\ exists ff_q_etcc_column_count_exists_successor_witness_column_count_bits_decoded. etcc_column_code_column_count_exists_successor_witness = ff_q_etcc_column_count_exists_successor_witness_column_count_bits_decoded * S ((S (ff_i_etcc_column_count_exists_successor_witness_column_count_bits)) * etcc_column_scale_column_count_exists_successor_witness) + (ff_bit_etcc_column_count_exists_successor_witness_column_count_bits))) /\ (ff_bit_etcc_column_count_exists_successor_witness_column_count_bits = 0 \/ ff_bit_etcc_column_count_exists_successor_witness_column_count_bits = 1))))) /\ etcc_row_count_column_count_exists_successor_witness + etcc_count_column_count_exists_successor = k)))))
46. 0046specialize eisenstein_transposed_column_count_prefix_extend p
47. 0047specialize eisenstein_transposed_column_count_prefix_extend q
48. 0048specialize eisenstein_transposed_column_count_prefix_extend h
49. 0049specialize eisenstein_transposed_column_count_prefix_extend k
50. 0050specialize eisenstein_transposed_column_count_prefix_extend ab
51. 0051specialize eisenstein_transposed_column_count_prefix_extend ac
52. 0052specialize eisenstein_transposed_column_count_prefix_extend bb
53. 0053specialize eisenstein_transposed_column_count_prefix_extend bc
54. 0054specialize eisenstein_transposed_column_count_prefix_extend x
55. 0055specialize eisenstein_transposed_column_count_prefix_extend x1
56. 0056specialize eisenstein_transposed_column_count_prefix_extend l
57. 0057apply eisenstein_transposed_column_count_prefix_extend
58. 0058exact hprefix_witness_witness
59. 0059exact hlast
60. 0060exact hnext