PA00E9

eisenstein_transposed_column_prefix_exists

Alpha v34 checked-use theorem · independently closed; not Stable

Every finite family of swapped-row cell choices has one beta-coded column.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

forall p q h bb bc i k. (forall etc_row_index_transposed_column_choices. (exists edt_lt_gap_transposed_column_choices_bound. edt_lt_gap_transposed_column_choices_bound + S (etc_row_index_transposed_column_choices) = k) -> exists etc_bit_transposed_column_choices. (exists etc_count_transposed_column_choices_witness etc_row_code_transposed_column_choices_witness etc_row_scale_transposed_column_choices_witness. ((((((exists ff_h_etc_transposed_column_choices_witness_outer_entry. ff_h_etc_transposed_column_choices_witness_outer_entry + S (etc_count_transposed_column_choices_witness) = S ((S (etc_row_index_transposed_column_choices)) * bc)) /\ exists ff_q_etc_transposed_column_choices_witness_outer_entry. bb = ff_q_etc_transposed_column_choices_witness_outer_entry * S ((S (etc_row_index_transposed_column_choices)) * bc) + (etc_count_transposed_column_choices_witness))) /\ (forall eri_column_etc_transposed_column_choices_witness_row. (exists eri_gap_etc_transposed_column_choices_witness_row_bound. eri_gap_etc_transposed_column_choices_witness_row_bound + S (eri_column_etc_transposed_column_choices_witness_row) = h) -> exists eri_bit_etc_transposed_column_choices_witness_row. ((((exists ff_h_eri_etc_transposed_column_choices_witness_row_decoded. ff_h_eri_etc_transposed_column_choices_witness_row_decoded + S (eri_bit_etc_transposed_column_choices_witness_row) = S ((S (eri_column_etc_transposed_column_choices_witness_row)) * etc_row_scale_transposed_column_choices_witness)) /\ exists ff_q_eri_etc_transposed_column_choices_witness_row_decoded. etc_row_code_transposed_column_choices_witness = ff_q_eri_etc_transposed_column_choices_witness_row_decoded * S ((S (eri_column_etc_transposed_column_choices_witness_row)) * etc_row_scale_transposed_column_choices_witness) + (eri_bit_etc_transposed_column_choices_witness_row))) /\ (((eri_bit_etc_transposed_column_choices_witness_row = 0 /\ ((exists eri_gap_etc_transposed_column_choices_witness_row_choice_left. eri_gap_etc_transposed_column_choices_witness_row_choice_left + S (p * S etc_row_index_transposed_column_choices) = q * S eri_column_etc_transposed_column_choices_witness_row) /\ ~(exists eri_gap_etc_transposed_column_choices_witness_row_choice_right. eri_gap_etc_transposed_column_choices_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_choices_witness_row) = p * S etc_row_index_transposed_column_choices))) \/ (eri_bit_etc_transposed_column_choices_witness_row = 1 /\ ((exists eri_gap_etc_transposed_column_choices_witness_row_choice_right. eri_gap_etc_transposed_column_choices_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_choices_witness_row) = p * S etc_row_index_transposed_column_choices) /\ ~(exists eri_gap_etc_transposed_column_choices_witness_row_choice_left. eri_gap_etc_transposed_column_choices_witness_row_choice_left + S (p * S etc_row_index_transposed_column_choices) = q * S eri_column_etc_transposed_column_choices_witness_row)))))))) /\ (((exists ff_u_etc_transposed_column_choices_witness_count_relation_sum ff_v_etc_transposed_column_choices_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_choices_witness_count_relation_sum_start. ff_h_etc_transposed_column_choices_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_choices_witness_count_relation_sum_start. ff_u_etc_transposed_column_choices_witness_count_relation_sum = ff_q_etc_transposed_column_choices_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_transposed_column_choices_witness_count_relation_sum_terminal. ff_h_etc_transposed_column_choices_witness_count_relation_sum_terminal + S (etc_count_transposed_column_choices_witness) = S ((S (h)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_choices_witness_count_relation_sum_terminal. ff_u_etc_transposed_column_choices_witness_count_relation_sum = ff_q_etc_transposed_column_choices_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum) + (etc_count_transposed_column_choices_witness))) /\ forall ff_i_etc_transposed_column_choices_witness_count_relation_sum. (exists ff_lt_etc_transposed_column_choices_witness_count_relation_sum_bound. ff_lt_etc_transposed_column_choices_witness_count_relation_sum_bound + S ff_i_etc_transposed_column_choices_witness_count_relation_sum = h) -> exists ff_a_etc_transposed_column_choices_witness_count_relation_sum ff_r_etc_transposed_column_choices_witness_count_relation_sum ff_s_etc_transposed_column_choices_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_choices_witness_count_relation_sum_summand. ff_h_etc_transposed_column_choices_witness_count_relation_sum_summand + S (ff_a_etc_transposed_column_choices_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_choices_witness_count_relation_sum)) * etc_row_scale_transposed_column_choices_witness)) /\ exists ff_q_etc_transposed_column_choices_witness_count_relation_sum_summand. etc_row_code_transposed_column_choices_witness = ff_q_etc_transposed_column_choices_witness_count_relation_sum_summand * S ((S (ff_i_etc_transposed_column_choices_witness_count_relation_sum)) * etc_row_scale_transposed_column_choices_witness) + (ff_a_etc_transposed_column_choices_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_choices_witness_count_relation_sum_partial. ff_h_etc_transposed_column_choices_witness_count_relation_sum_partial + S (ff_r_etc_transposed_column_choices_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_choices_witness_count_relation_sum)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_choices_witness_count_relation_sum_partial. ff_u_etc_transposed_column_choices_witness_count_relation_sum = ff_q_etc_transposed_column_choices_witness_count_relation_sum_partial * S ((S (ff_i_etc_transposed_column_choices_witness_count_relation_sum)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum) + (ff_r_etc_transposed_column_choices_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_choices_witness_count_relation_sum_successor. ff_h_etc_transposed_column_choices_witness_count_relation_sum_successor + S (ff_s_etc_transposed_column_choices_witness_count_relation_sum) = S ((S (S ff_i_etc_transposed_column_choices_witness_count_relation_sum)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_choices_witness_count_relation_sum_successor. ff_u_etc_transposed_column_choices_witness_count_relation_sum = ff_q_etc_transposed_column_choices_witness_count_relation_sum_successor * S ((S (S ff_i_etc_transposed_column_choices_witness_count_relation_sum)) * ff_v_etc_transposed_column_choices_witness_count_relation_sum) + (ff_s_etc_transposed_column_choices_witness_count_relation_sum))) /\ ff_s_etc_transposed_column_choices_witness_count_relation_sum = ff_r_etc_transposed_column_choices_witness_count_relation_sum + ff_a_etc_transposed_column_choices_witness_count_relation_sum)))))) /\ (forall ff_i_etc_transposed_column_choices_witness_count_relation_bits. (exists ff_lt_etc_transposed_column_choices_witness_count_relation_bits_bound. ff_lt_etc_transposed_column_choices_witness_count_relation_bits_bound + S ff_i_etc_transposed_column_choices_witness_count_relation_bits = h) -> exists ff_bit_etc_transposed_column_choices_witness_count_relation_bits. ((((exists ff_h_etc_transposed_column_choices_witness_count_relation_bits_decoded. ff_h_etc_transposed_column_choices_witness_count_relation_bits_decoded + S (ff_bit_etc_transposed_column_choices_witness_count_relation_bits) = S ((S (ff_i_etc_transposed_column_choices_witness_count_relation_bits)) * etc_row_scale_transposed_column_choices_witness)) /\ exists ff_q_etc_transposed_column_choices_witness_count_relation_bits_decoded. etc_row_code_transposed_column_choices_witness = ff_q_etc_transposed_column_choices_witness_count_relation_bits_decoded * S ((S (ff_i_etc_transposed_column_choices_witness_count_relation_bits)) * etc_row_scale_transposed_column_choices_witness) + (ff_bit_etc_transposed_column_choices_witness_count_relation_bits))) /\ (ff_bit_etc_transposed_column_choices_witness_count_relation_bits = 0 \/ ff_bit_etc_transposed_column_choices_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_transposed_column_choices_witness_inner_entry. ff_h_etc_transposed_column_choices_witness_inner_entry + S (etc_bit_transposed_column_choices) = S ((S (i)) * etc_row_scale_transposed_column_choices_witness)) /\ exists ff_q_etc_transposed_column_choices_witness_inner_entry. etc_row_code_transposed_column_choices_witness = ff_q_etc_transposed_column_choices_witness_inner_entry * S ((S (i)) * etc_row_scale_transposed_column_choices_witness) + (etc_bit_transposed_column_choices)))))) -> (exists z e. (forall etc_row_index_transposed_column_exists_result. (exists edt_lt_gap_transposed_column_exists_result_bound. edt_lt_gap_transposed_column_exists_result_bound + S (etc_row_index_transposed_column_exists_result) = k) -> exists etc_bit_transposed_column_exists_result. ((((exists ff_h_etc_transposed_column_exists_result_decoded. ff_h_etc_transposed_column_exists_result_decoded + S (etc_bit_transposed_column_exists_result) = S ((S (etc_row_index_transposed_column_exists_result)) * e)) /\ exists ff_q_etc_transposed_column_exists_result_decoded. z = ff_q_etc_transposed_column_exists_result_decoded * S ((S (etc_row_index_transposed_column_exists_result)) * e) + (etc_bit_transposed_column_exists_result))) /\ (exists etc_count_transposed_column_exists_result_witness etc_row_code_transposed_column_exists_result_witness etc_row_scale_transposed_column_exists_result_witness. ((((((exists ff_h_etc_transposed_column_exists_result_witness_outer_entry. ff_h_etc_transposed_column_exists_result_witness_outer_entry + S (etc_count_transposed_column_exists_result_witness) = S ((S (etc_row_index_transposed_column_exists_result)) * bc)) /\ exists ff_q_etc_transposed_column_exists_result_witness_outer_entry. bb = ff_q_etc_transposed_column_exists_result_witness_outer_entry * S ((S (etc_row_index_transposed_column_exists_result)) * bc) + (etc_count_transposed_column_exists_result_witness))) /\ (forall eri_column_etc_transposed_column_exists_result_witness_row. (exists eri_gap_etc_transposed_column_exists_result_witness_row_bound. eri_gap_etc_transposed_column_exists_result_witness_row_bound + S (eri_column_etc_transposed_column_exists_result_witness_row) = h) -> exists eri_bit_etc_transposed_column_exists_result_witness_row. ((((exists ff_h_eri_etc_transposed_column_exists_result_witness_row_decoded. ff_h_eri_etc_transposed_column_exists_result_witness_row_decoded + S (eri_bit_etc_transposed_column_exists_result_witness_row) = S ((S (eri_column_etc_transposed_column_exists_result_witness_row)) * etc_row_scale_transposed_column_exists_result_witness)) /\ exists ff_q_eri_etc_transposed_column_exists_result_witness_row_decoded. etc_row_code_transposed_column_exists_result_witness = ff_q_eri_etc_transposed_column_exists_result_witness_row_decoded * S ((S (eri_column_etc_transposed_column_exists_result_witness_row)) * etc_row_scale_transposed_column_exists_result_witness) + (eri_bit_etc_transposed_column_exists_result_witness_row))) /\ (((eri_bit_etc_transposed_column_exists_result_witness_row = 0 /\ ((exists eri_gap_etc_transposed_column_exists_result_witness_row_choice_left. eri_gap_etc_transposed_column_exists_result_witness_row_choice_left + S (p * S etc_row_index_transposed_column_exists_result) = q * S eri_column_etc_transposed_column_exists_result_witness_row) /\ ~(exists eri_gap_etc_transposed_column_exists_result_witness_row_choice_right. eri_gap_etc_transposed_column_exists_result_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_exists_result_witness_row) = p * S etc_row_index_transposed_column_exists_result))) \/ (eri_bit_etc_transposed_column_exists_result_witness_row = 1 /\ ((exists eri_gap_etc_transposed_column_exists_result_witness_row_choice_right. eri_gap_etc_transposed_column_exists_result_witness_row_choice_right + S (q * S eri_column_etc_transposed_column_exists_result_witness_row) = p * S etc_row_index_transposed_column_exists_result) /\ ~(exists eri_gap_etc_transposed_column_exists_result_witness_row_choice_left. eri_gap_etc_transposed_column_exists_result_witness_row_choice_left + S (p * S etc_row_index_transposed_column_exists_result) = q * S eri_column_etc_transposed_column_exists_result_witness_row)))))))) /\ (((exists ff_u_etc_transposed_column_exists_result_witness_count_relation_sum ff_v_etc_transposed_column_exists_result_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_exists_result_witness_count_relation_sum_start. ff_h_etc_transposed_column_exists_result_witness_count_relation_sum_start + S (0) = S ((S (0)) * ff_v_etc_transposed_column_exists_result_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_result_witness_count_relation_sum_start. ff_u_etc_transposed_column_exists_result_witness_count_relation_sum = ff_q_etc_transposed_column_exists_result_witness_count_relation_sum_start * S ((S (0)) * ff_v_etc_transposed_column_exists_result_witness_count_relation_sum) + (0))) /\ ((((exists ff_h_etc_transposed_column_exists_result_witness_count_relation_sum_terminal. ff_h_etc_transposed_column_exists_result_witness_count_relation_sum_terminal + S (etc_count_transposed_column_exists_result_witness) = S ((S (h)) * ff_v_etc_transposed_column_exists_result_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_result_witness_count_relation_sum_terminal. ff_u_etc_transposed_column_exists_result_witness_count_relation_sum = ff_q_etc_transposed_column_exists_result_witness_count_relation_sum_terminal * S ((S (h)) * ff_v_etc_transposed_column_exists_result_witness_count_relation_sum) + (etc_count_transposed_column_exists_result_witness))) /\ forall ff_i_etc_transposed_column_exists_result_witness_count_relation_sum. (exists ff_lt_etc_transposed_column_exists_result_witness_count_relation_sum_bound. ff_lt_etc_transposed_column_exists_result_witness_count_relation_sum_bound + S ff_i_etc_transposed_column_exists_result_witness_count_relation_sum = h) -> exists ff_a_etc_transposed_column_exists_result_witness_count_relation_sum ff_r_etc_transposed_column_exists_result_witness_count_relation_sum ff_s_etc_transposed_column_exists_result_witness_count_relation_sum. ((((exists ff_h_etc_transposed_column_exists_result_witness_count_relation_sum_summand. ff_h_etc_transposed_column_exists_result_witness_count_relation_sum_summand + S (ff_a_etc_transposed_column_exists_result_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_exists_result_witness_count_relation_sum)) * etc_row_scale_transposed_column_exists_result_witness)) /\ exists ff_q_etc_transposed_column_exists_result_witness_count_relation_sum_summand. etc_row_code_transposed_column_exists_result_witness = ff_q_etc_transposed_column_exists_result_witness_count_relation_sum_summand * S ((S (ff_i_etc_transposed_column_exists_result_witness_count_relation_sum)) * etc_row_scale_transposed_column_exists_result_witness) + (ff_a_etc_transposed_column_exists_result_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_exists_result_witness_count_relation_sum_partial. ff_h_etc_transposed_column_exists_result_witness_count_relation_sum_partial + S (ff_r_etc_transposed_column_exists_result_witness_count_relation_sum) = S ((S (ff_i_etc_transposed_column_exists_result_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_result_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_result_witness_count_relation_sum_partial. ff_u_etc_transposed_column_exists_result_witness_count_relation_sum = ff_q_etc_transposed_column_exists_result_witness_count_relation_sum_partial * S ((S (ff_i_etc_transposed_column_exists_result_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_result_witness_count_relation_sum) + (ff_r_etc_transposed_column_exists_result_witness_count_relation_sum))) /\ ((((exists ff_h_etc_transposed_column_exists_result_witness_count_relation_sum_successor. ff_h_etc_transposed_column_exists_result_witness_count_relation_sum_successor + S (ff_s_etc_transposed_column_exists_result_witness_count_relation_sum) = S ((S (S ff_i_etc_transposed_column_exists_result_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_result_witness_count_relation_sum)) /\ exists ff_q_etc_transposed_column_exists_result_witness_count_relation_sum_successor. ff_u_etc_transposed_column_exists_result_witness_count_relation_sum = ff_q_etc_transposed_column_exists_result_witness_count_relation_sum_successor * S ((S (S ff_i_etc_transposed_column_exists_result_witness_count_relation_sum)) * ff_v_etc_transposed_column_exists_result_witness_count_relation_sum) + (ff_s_etc_transposed_column_exists_result_witness_count_relation_sum))) /\ ff_s_etc_transposed_column_exists_result_witness_count_relation_sum = ff_r_etc_transposed_column_exists_result_witness_count_relation_sum + ff_a_etc_transposed_column_exists_result_witness_count_relation_sum)))))) /\ (forall ff_i_etc_transposed_column_exists_result_witness_count_relation_bits. (exists ff_lt_etc_transposed_column_exists_result_witness_count_relation_bits_bound. ff_lt_etc_transposed_column_exists_result_witness_count_relation_bits_bound + S ff_i_etc_transposed_column_exists_result_witness_count_relation_bits = h) -> exists ff_bit_etc_transposed_column_exists_result_witness_count_relation_bits. ((((exists ff_h_etc_transposed_column_exists_result_witness_count_relation_bits_decoded. ff_h_etc_transposed_column_exists_result_witness_count_relation_bits_decoded + S (ff_bit_etc_transposed_column_exists_result_witness_count_relation_bits) = S ((S (ff_i_etc_transposed_column_exists_result_witness_count_relation_bits)) * etc_row_scale_transposed_column_exists_result_witness)) /\ exists ff_q_etc_transposed_column_exists_result_witness_count_relation_bits_decoded. etc_row_code_transposed_column_exists_result_witness = ff_q_etc_transposed_column_exists_result_witness_count_relation_bits_decoded * S ((S (ff_i_etc_transposed_column_exists_result_witness_count_relation_bits)) * etc_row_scale_transposed_column_exists_result_witness) + (ff_bit_etc_transposed_column_exists_result_witness_count_relation_bits))) /\ (ff_bit_etc_transposed_column_exists_result_witness_count_relation_bits = 0 \/ ff_bit_etc_transposed_column_exists_result_witness_count_relation_bits = 1)))))) /\ (((exists ff_h_etc_transposed_column_exists_result_witness_inner_entry. ff_h_etc_transposed_column_exists_result_witness_inner_entry + S (etc_bit_transposed_column_exists_result) = S ((S (i)) * etc_row_scale_transposed_column_exists_result_witness)) /\ exists ff_q_etc_transposed_column_exists_result_witness_inner_entry. etc_row_code_transposed_column_exists_result_witness = ff_q_etc_transposed_column_exists_result_witness_inner_entry * S ((S (i)) * etc_row_scale_transposed_column_exists_result_witness) + (etc_bit_transposed_column_exists_result))))))))

Structural proof guide

Generated structural guide

Every finite family of swapped-row cell choices has one beta-coded column.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero, le_succ, le_refl, eisenstein_transposed_column_prefix_extend as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (3), intermediate claims (5).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA00E8 eisenstein_transposed_column_prefix_extend

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA00E8 eisenstein_transposed_column_prefix_extend

Direct dependents

PA00EF eisenstein_row_transposed_column_count_partition PA00F7 eisenstein_fubini_column_count_witness_retarget

Formal native tactic body

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

Read the argument

Proof checkpoints

56 script commands · 12 reading checkpoints · 5 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (5)
add eq zero rightsucc ne zerole succle refleisenstein transposed column prefix extend

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–6

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro h
  4. L4
    intro bb
  5. L5
    intro bc
  6. L6
    intro i
02Induction on kL7–8

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L7
    induction k
  2. L8
    intro hchoices
03Construct an explicit witnessL9–10

Supply the displayed value, then prove that it has the required property.

  1. L9
    exists 0
  2. L10
    exists 0
04Fix variables and assumptionsL11–12

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro j
  2. L12
    intro hj
05Separate the logical casesL13–14

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L13
    exfalso
  2. L14
    cases hj
06Establish hsjL15–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L15
    have hsj : S j = 0
  2. L16
    specialize add_eq_zero_right x
  3. L17
    specialize add_eq_zero_right (S j)
  4. L18
    apply add_eq_zero_right
  5. L19
    exact hj_witness
  6. L20
    specialize succ_ne_zero j
  7. L21
    apply succ_ne_zero
  8. L22
    exact hsj
  9. L23
    intro hchoices
07Establish hprevious_choicesL24–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hchoices.

  1. L24
    have hprevious_choices · expand full local formula (645 characters)have hprevious_choices : ∀ etc_row_index_transposed_column_exists_previous_choices. Lt(etc_row_index_transposed_column_exists_previous_choices,k) → ∃ x. ∃ y. ∃ z. ∃ n. BetaAt(bb,bc,etc_row_index_transposed_column_exists_previous_choices,y) ∧ (∀ m. Lt(m,h) → ∃ j. BetaAt(z,n,m,j) ∧ (j = 0 ∧ (Lt(p · S etc_row_index_transposed_column_exists_previous_choices,q · S m) ∧ ¬Lt(q · S m,p · S etc_row_index_transposed_column_exists_previous_choices)) ∨ j = 1 ∧ (Lt(q · S m,p · S etc_row_index_transposed_column_exists_previous_choices) ∧ ¬Lt(p · S etc_row_index_transposed_column_exists_previous_choices,q · S m)))) ∧ BitCount(z,n,h,y) ∧ BetaAt(z,n,i,x)
    Definitions: LtBetaAtBitCount
  2. L25
    intro j
  3. L26
    intro hj
  4. L27
    specialize hchoices j
  5. L28
    apply hchoices
  6. L29
    specialize le_succ (S j)
  7. L30
    specialize le_succ k
  8. L31
    apply le_succ
  9. L32
    exact hj
08Establish hpreviousL33–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

  1. L33
    have hprevious : ∃ z. ∃ e. ∀ x. Lt(x,k) → ∃ y. BetaAt(z,e,x,y) ∧ (∃ n. ∃ m. ∃ j. BetaAt(bb,bc,x,n) ∧ (∀ u. Lt(u,h) → ∃ v. BetaAt(m,j,u,v) ∧ (v = 0 ∧ (Lt(p · S x,q · S u) ∧ ¬Lt(q · S u,p · S x)) ∨ v = 1 ∧ (Lt(q · S u,p · S x) ∧ ¬Lt(p · S x,q · S u)))) ∧ BitCount(m,j,h,n) ∧ BetaAt(m,j,i,y))Definitions: LtBetaAtBitCount
  2. L34
    apply IH
  3. L35
    exact hprevious_choices
09Separate the logical casesL36–37

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L36
    cases hprevious
  2. L37
    cases hprevious_witness
10Establish hlastL38–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hchoices.

  1. L38
    have hlast : ∃ d. ∃ x. ∃ y. ∃ z. BetaAt(bb,bc,k,x) ∧ (∀ n. Lt(n,h) → ∃ m. BetaAt(y,z,n,m) ∧ (m = 0 ∧ (Lt(p · S k,q · S n) ∧ ¬Lt(q · S n,p · S k)) ∨ m = 1 ∧ (Lt(q · S n,p · S k) ∧ ¬Lt(p · S k,q · S n)))) ∧ BitCount(y,z,h,x) ∧ BetaAt(y,z,i,d)Definitions: LtBetaAtBitCount
  2. L39
    specialize hchoices k
  3. L40
    apply hchoices
  4. L41
    specialize le_refl (S k)
  5. L42
    exact le_refl
11Establish hnextL43–52

Establish this local claim before using it. It is not an additional assumption.

  1. L43
    have hnext : ∃ z. ∃ e. ∀ x. Lt(x,S k) → ∃ y. BetaAt(z,e,x,y) ∧ (∃ n. ∃ m. ∃ j. BetaAt(bb,bc,x,n) ∧ (∀ u. Lt(u,h) → ∃ v. BetaAt(m,j,u,v) ∧ (v = 0 ∧ (Lt(p · S x,q · S u) ∧ ¬Lt(q · S u,p · S x)) ∨ v = 1 ∧ (Lt(q · S u,p · S x) ∧ ¬Lt(p · S x,q · S u)))) ∧ BitCount(m,j,h,n) ∧ BetaAt(m,j,i,y))Definitions: LtBetaAtBitCount
  2. L44
    specialize eisenstein_transposed_column_prefix_extend p
  3. L45
    specialize eisenstein_transposed_column_prefix_extend q
  4. L46
    specialize eisenstein_transposed_column_prefix_extend h
  5. L47
    specialize eisenstein_transposed_column_prefix_extend bb
  6. L48
    specialize eisenstein_transposed_column_prefix_extend bc
  7. L49
    specialize eisenstein_transposed_column_prefix_extend i
  8. L50
    specialize eisenstein_transposed_column_prefix_extend x
  9. L51
    specialize eisenstein_transposed_column_prefix_extend x1
  10. L52
    specialize eisenstein_transposed_column_prefix_extend k
12Use earlier factsL53–56

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L53
    apply eisenstein_transposed_column_prefix_extend
  2. L54
    exact hprevious_witness_witness
  3. L55
    exact hlast
  4. L56
    exact hnext

Library-wide reading audit

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