LU001G

lucas_choose_prefix_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Every pair of beta-coded natural source streams has an actual beta-coded relational-binomial coefficient stream of every finite length.

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 first-order arithmetic statement

forall qb qc db dc l. exists z t. (forall lmd_choose_index_choose_total. (exists lmd_gap_choose_total_bound. lmd_gap_choose_total_bound + S (lmd_choose_index_choose_total) = (l)) -> exists lmd_choose_upper_choose_total lmd_choose_lower_choose_total lmd_choose_value_choose_total. ((((exists ff_h_lmd_choose_total_upper. ff_h_lmd_choose_total_upper + S (lmd_choose_upper_choose_total) = S ((S (lmd_choose_index_choose_total)) * qc)) /\ exists ff_q_lmd_choose_total_upper. qb = ff_q_lmd_choose_total_upper * S ((S (lmd_choose_index_choose_total)) * qc) + (lmd_choose_upper_choose_total))) /\ ((((exists ff_h_lmd_choose_total_lower. ff_h_lmd_choose_total_lower + S (lmd_choose_lower_choose_total) = S ((S (lmd_choose_index_choose_total)) * dc)) /\ exists ff_q_lmd_choose_total_lower. db = ff_q_lmd_choose_total_lower * S ((S (lmd_choose_index_choose_total)) * dc) + (lmd_choose_lower_choose_total))) /\ ((((exists ff_h_lmd_choose_total_result. ff_h_lmd_choose_total_result + S (lmd_choose_value_choose_total) = S ((S (lmd_choose_index_choose_total)) * t)) /\ exists ff_q_lmd_choose_total_result. z = ff_q_lmd_choose_total_result * S ((S (lmd_choose_index_choose_total)) * t) + (lmd_choose_value_choose_total))) /\ (((exists bcf_lt_gap_lmd_choose_total_choose_out_of_range. bcf_lt_gap_lmd_choose_total_choose_out_of_range + S (lmd_choose_upper_choose_total) = lmd_choose_lower_choose_total) /\ lmd_choose_value_choose_total = 0) \/ ((exists bcf_le_gap_lmd_choose_total_choose_in_range. bcf_le_gap_lmd_choose_total_choose_in_range + (lmd_choose_lower_choose_total) = lmd_choose_upper_choose_total) /\ (exists bcf_row_code_code_lmd_choose_total_choose bcf_row_code_scale_lmd_choose_total_choose bcf_row_scale_code_lmd_choose_total_choose bcf_row_scale_scale_lmd_choose_total_choose bcf_row_code_lmd_choose_total_choose bcf_row_scale_lmd_choose_total_choose. ((forall bcf_row_index_lmd_choose_total_choose_table. (exists bcf_lt_gap_lmd_choose_total_choose_table_row_bound. bcf_lt_gap_lmd_choose_total_choose_table_row_bound + S (bcf_row_index_lmd_choose_total_choose_table) = S (lmd_choose_upper_choose_total)) -> exists bcf_row_code_lmd_choose_total_choose_table bcf_row_scale_lmd_choose_total_choose_table. ((((exists bcf_height_lmd_choose_total_choose_table_decoded_row_code. bcf_height_lmd_choose_total_choose_table_decoded_row_code + S (bcf_row_code_lmd_choose_total_choose_table) = S ((S (bcf_row_index_lmd_choose_total_choose_table)) * bcf_row_code_scale_lmd_choose_total_choose)) /\ exists bcf_quotient_lmd_choose_total_choose_table_decoded_row_code. bcf_row_code_code_lmd_choose_total_choose = bcf_quotient_lmd_choose_total_choose_table_decoded_row_code * S ((S (bcf_row_index_lmd_choose_total_choose_table)) * bcf_row_code_scale_lmd_choose_total_choose) + (bcf_row_code_lmd_choose_total_choose_table))) /\ ((((exists bcf_height_lmd_choose_total_choose_table_decoded_row_scale. bcf_height_lmd_choose_total_choose_table_decoded_row_scale + S (bcf_row_scale_lmd_choose_total_choose_table) = S ((S (bcf_row_index_lmd_choose_total_choose_table)) * bcf_row_scale_scale_lmd_choose_total_choose)) /\ exists bcf_quotient_lmd_choose_total_choose_table_decoded_row_scale. bcf_row_scale_code_lmd_choose_total_choose = bcf_quotient_lmd_choose_total_choose_table_decoded_row_scale * S ((S (bcf_row_index_lmd_choose_total_choose_table)) * bcf_row_scale_scale_lmd_choose_total_choose) + (bcf_row_scale_lmd_choose_total_choose_table))) /\ ((bcf_row_index_lmd_choose_total_choose_table = 0 /\ (forall bcf_index_lmd_choose_total_choose_table_zero_row. (exists bcf_lt_gap_lmd_choose_total_choose_table_zero_row_bound. bcf_lt_gap_lmd_choose_total_choose_table_zero_row_bound + S (bcf_index_lmd_choose_total_choose_table_zero_row) = S (lmd_choose_upper_choose_total)) -> exists bcf_value_lmd_choose_total_choose_table_zero_row. ((((exists bcf_height_lmd_choose_total_choose_table_zero_row_entry. bcf_height_lmd_choose_total_choose_table_zero_row_entry + S (bcf_value_lmd_choose_total_choose_table_zero_row) = S ((S (bcf_index_lmd_choose_total_choose_table_zero_row)) * bcf_row_scale_lmd_choose_total_choose_table)) /\ exists bcf_quotient_lmd_choose_total_choose_table_zero_row_entry. bcf_row_code_lmd_choose_total_choose_table = bcf_quotient_lmd_choose_total_choose_table_zero_row_entry * S ((S (bcf_index_lmd_choose_total_choose_table_zero_row)) * bcf_row_scale_lmd_choose_total_choose_table) + (bcf_value_lmd_choose_total_choose_table_zero_row))) /\ ((bcf_index_lmd_choose_total_choose_table_zero_row = 0 /\ bcf_value_lmd_choose_total_choose_table_zero_row = 1) \/ exists bcf_predecessor_lmd_choose_total_choose_table_zero_row. bcf_index_lmd_choose_total_choose_table_zero_row = S bcf_predecessor_lmd_choose_total_choose_table_zero_row /\ bcf_value_lmd_choose_total_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lmd_choose_total_choose_table bcf_previous_code_lmd_choose_total_choose_table bcf_previous_scale_lmd_choose_total_choose_table. bcf_row_index_lmd_choose_total_choose_table = S bcf_predecessor_lmd_choose_total_choose_table /\ ((((exists bcf_height_lmd_choose_total_choose_table_decoded_previous_code. bcf_height_lmd_choose_total_choose_table_decoded_previous_code + S (bcf_previous_code_lmd_choose_total_choose_table) = S ((S (bcf_predecessor_lmd_choose_total_choose_table)) * bcf_row_code_scale_lmd_choose_total_choose)) /\ exists bcf_quotient_lmd_choose_total_choose_table_decoded_previous_code. bcf_row_code_code_lmd_choose_total_choose = bcf_quotient_lmd_choose_total_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lmd_choose_total_choose_table)) * bcf_row_code_scale_lmd_choose_total_choose) + (bcf_previous_code_lmd_choose_total_choose_table))) /\ ((((exists bcf_height_lmd_choose_total_choose_table_decoded_previous_scale. bcf_height_lmd_choose_total_choose_table_decoded_previous_scale + S (bcf_previous_scale_lmd_choose_total_choose_table) = S ((S (bcf_predecessor_lmd_choose_total_choose_table)) * bcf_row_scale_scale_lmd_choose_total_choose)) /\ exists bcf_quotient_lmd_choose_total_choose_table_decoded_previous_scale. bcf_row_scale_code_lmd_choose_total_choose = bcf_quotient_lmd_choose_total_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lmd_choose_total_choose_table)) * bcf_row_scale_scale_lmd_choose_total_choose) + (bcf_previous_scale_lmd_choose_total_choose_table))) /\ (forall bcf_index_lmd_choose_total_choose_table_row_step. (exists bcf_lt_gap_lmd_choose_total_choose_table_row_step_bound. bcf_lt_gap_lmd_choose_total_choose_table_row_step_bound + S (bcf_index_lmd_choose_total_choose_table_row_step) = S (lmd_choose_upper_choose_total)) -> exists bcf_value_lmd_choose_total_choose_table_row_step. ((((exists bcf_height_lmd_choose_total_choose_table_row_step_entry. bcf_height_lmd_choose_total_choose_table_row_step_entry + S (bcf_value_lmd_choose_total_choose_table_row_step) = S ((S (bcf_index_lmd_choose_total_choose_table_row_step)) * bcf_row_scale_lmd_choose_total_choose_table)) /\ exists bcf_quotient_lmd_choose_total_choose_table_row_step_entry. bcf_row_code_lmd_choose_total_choose_table = bcf_quotient_lmd_choose_total_choose_table_row_step_entry * S ((S (bcf_index_lmd_choose_total_choose_table_row_step)) * bcf_row_scale_lmd_choose_total_choose_table) + (bcf_value_lmd_choose_total_choose_table_row_step))) /\ ((bcf_index_lmd_choose_total_choose_table_row_step = 0 /\ bcf_value_lmd_choose_total_choose_table_row_step = 1) \/ exists bcf_predecessor_lmd_choose_total_choose_table_row_step bcf_left_lmd_choose_total_choose_table_row_step bcf_right_lmd_choose_total_choose_table_row_step. bcf_index_lmd_choose_total_choose_table_row_step = S bcf_predecessor_lmd_choose_total_choose_table_row_step /\ ((((exists bcf_height_lmd_choose_total_choose_table_row_step_previous_left. bcf_height_lmd_choose_total_choose_table_row_step_previous_left + S (bcf_left_lmd_choose_total_choose_table_row_step) = S ((S (bcf_predecessor_lmd_choose_total_choose_table_row_step)) * bcf_previous_scale_lmd_choose_total_choose_table)) /\ exists bcf_quotient_lmd_choose_total_choose_table_row_step_previous_left. bcf_previous_code_lmd_choose_total_choose_table = bcf_quotient_lmd_choose_total_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lmd_choose_total_choose_table_row_step)) * bcf_previous_scale_lmd_choose_total_choose_table) + (bcf_left_lmd_choose_total_choose_table_row_step))) /\ ((((exists bcf_height_lmd_choose_total_choose_table_row_step_previous_right. bcf_height_lmd_choose_total_choose_table_row_step_previous_right + S (bcf_right_lmd_choose_total_choose_table_row_step) = S ((S (S (bcf_predecessor_lmd_choose_total_choose_table_row_step))) * bcf_previous_scale_lmd_choose_total_choose_table)) /\ exists bcf_quotient_lmd_choose_total_choose_table_row_step_previous_right. bcf_previous_code_lmd_choose_total_choose_table = bcf_quotient_lmd_choose_total_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lmd_choose_total_choose_table_row_step))) * bcf_previous_scale_lmd_choose_total_choose_table) + (bcf_right_lmd_choose_total_choose_table_row_step))) /\ bcf_value_lmd_choose_total_choose_table_row_step = bcf_left_lmd_choose_total_choose_table_row_step + bcf_right_lmd_choose_total_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lmd_choose_total_choose_decoded_row_code. bcf_height_lmd_choose_total_choose_decoded_row_code + S (bcf_row_code_lmd_choose_total_choose) = S ((S (lmd_choose_upper_choose_total)) * bcf_row_code_scale_lmd_choose_total_choose)) /\ exists bcf_quotient_lmd_choose_total_choose_decoded_row_code. bcf_row_code_code_lmd_choose_total_choose = bcf_quotient_lmd_choose_total_choose_decoded_row_code * S ((S (lmd_choose_upper_choose_total)) * bcf_row_code_scale_lmd_choose_total_choose) + (bcf_row_code_lmd_choose_total_choose))) /\ ((((exists bcf_height_lmd_choose_total_choose_decoded_row_scale. bcf_height_lmd_choose_total_choose_decoded_row_scale + S (bcf_row_scale_lmd_choose_total_choose) = S ((S (lmd_choose_upper_choose_total)) * bcf_row_scale_scale_lmd_choose_total_choose)) /\ exists bcf_quotient_lmd_choose_total_choose_decoded_row_scale. bcf_row_scale_code_lmd_choose_total_choose = bcf_quotient_lmd_choose_total_choose_decoded_row_scale * S ((S (lmd_choose_upper_choose_total)) * bcf_row_scale_scale_lmd_choose_total_choose) + (bcf_row_scale_lmd_choose_total_choose))) /\ (((exists bcf_height_lmd_choose_total_choose_decoded_value. bcf_height_lmd_choose_total_choose_decoded_value + S (lmd_choose_value_choose_total) = S ((S (lmd_choose_lower_choose_total)) * bcf_row_scale_lmd_choose_total_choose)) /\ exists bcf_quotient_lmd_choose_total_choose_decoded_value. bcf_row_code_lmd_choose_total_choose = bcf_quotient_lmd_choose_total_choose_decoded_value * S ((S (lmd_choose_lower_choose_total)) * bcf_row_scale_lmd_choose_total_choose) + (lmd_choose_value_choose_total)))))))))))))

Constructive proof overview

Generated structural guide

Every pair of beta-coded natural source streams has an actual beta-coded relational-binomial coefficient stream of every finite length.

The unchanged tactic script uses 2 declared prerequisites and contains 20 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Historical empty-context replay experiment only; that experiment persisted no certificate and granted no release authority. Current checked use follows separately sealed, independently verified proof bundles; there is no Stable promotion.

Proof neighborhood

Direct dependencies

LU001E lucas_choose_prefix_empty LU001F lucas_choose_prefix_extend

Direct dependents

LU001Q lucas_theorem_for_length

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

20 script commands · 5 reading checkpoints · 1 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 (2)
lucas choose prefix emptylucas choose 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–5

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

  1. L1
    intro qb
  2. L2
    intro qc
  3. L3
    intro db
  4. L4
    intro dc
  5. L5
    intro l
02Induction on lL6–7

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

  1. L6
    induction l
  2. L7
    apply lucas_choose_prefix_empty
03Establish hpreviousL8–9

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

  1. L8
    have hprevious : ∃ z. ∃ t. ∀ x. Lt(x,l) → ∃ y. ∃ n. ∃ m. BetaAt(qb,qc,x,y) ∧ (BetaAt(db,dc,x,n) ∧ (BetaAt(z,t,x,m) ∧ Choose(y,n,m)))Definitions: LtBetaAtChoose
  2. L9
    exact IH
04Separate the logical casesL10–11

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

  1. L10
    cases hprevious
  2. L11
    cases hprevious_witness
05Use earlier factsL12–20

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

  1. L12
    specialize lucas_choose_prefix_extend qb
  2. L13
    specialize lucas_choose_prefix_extend qc
  3. L14
    specialize lucas_choose_prefix_extend db
  4. L15
    specialize lucas_choose_prefix_extend dc
  5. L16
    specialize lucas_choose_prefix_extend x
  6. L17
    specialize lucas_choose_prefix_extend x1
  7. L18
    specialize lucas_choose_prefix_extend l
  8. L19
    apply lucas_choose_prefix_extend
  9. L20
    exact hprevious_witness_witness

Library-wide reading audit

Original exact command ledger · 20 lines
  1. 0001intro qb
  2. 0002intro qc
  3. 0003intro db
  4. 0004intro dc
  5. 0005intro l
  6. 0006induction l
  7. 0007apply lucas_choose_prefix_empty
  8. 0008have hprevious : exists z t. (forall lmd_choose_index_choose_previous. (exists lmd_gap_choose_previous_bound. lmd_gap_choose_previous_bound + S (lmd_choose_index_choose_previous) = (l)) -> exists lmd_choose_upper_choose_previous lmd_choose_lower_choose_previous lmd_choose_value_choose_previous. ((((exists ff_h_lmd_choose_previous_upper. ff_h_lmd_choose_previous_upper + S (lmd_choose_upper_choose_previous) = S ((S (lmd_choose_index_choose_previous)) * qc)) /\ exists ff_q_lmd_choose_previous_upper. qb = ff_q_lmd_choose_previous_upper * S ((S (lmd_choose_index_choose_previous)) * qc) + (lmd_choose_upper_choose_previous))) /\ ((((exists ff_h_lmd_choose_previous_lower. ff_h_lmd_choose_previous_lower + S (lmd_choose_lower_choose_previous) = S ((S (lmd_choose_index_choose_previous)) * dc)) /\ exists ff_q_lmd_choose_previous_lower. db = ff_q_lmd_choose_previous_lower * S ((S (lmd_choose_index_choose_previous)) * dc) + (lmd_choose_lower_choose_previous))) /\ ((((exists ff_h_lmd_choose_previous_result. ff_h_lmd_choose_previous_result + S (lmd_choose_value_choose_previous) = S ((S (lmd_choose_index_choose_previous)) * t)) /\ exists ff_q_lmd_choose_previous_result. z = ff_q_lmd_choose_previous_result * S ((S (lmd_choose_index_choose_previous)) * t) + (lmd_choose_value_choose_previous))) /\ (((exists bcf_lt_gap_lmd_choose_previous_choose_out_of_range. bcf_lt_gap_lmd_choose_previous_choose_out_of_range + S (lmd_choose_upper_choose_previous) = lmd_choose_lower_choose_previous) /\ lmd_choose_value_choose_previous = 0) \/ ((exists bcf_le_gap_lmd_choose_previous_choose_in_range. bcf_le_gap_lmd_choose_previous_choose_in_range + (lmd_choose_lower_choose_previous) = lmd_choose_upper_choose_previous) /\ (exists bcf_row_code_code_lmd_choose_previous_choose bcf_row_code_scale_lmd_choose_previous_choose bcf_row_scale_code_lmd_choose_previous_choose bcf_row_scale_scale_lmd_choose_previous_choose bcf_row_code_lmd_choose_previous_choose bcf_row_scale_lmd_choose_previous_choose. ((forall bcf_row_index_lmd_choose_previous_choose_table. (exists bcf_lt_gap_lmd_choose_previous_choose_table_row_bound. bcf_lt_gap_lmd_choose_previous_choose_table_row_bound + S (bcf_row_index_lmd_choose_previous_choose_table) = S (lmd_choose_upper_choose_previous)) -> exists bcf_row_code_lmd_choose_previous_choose_table bcf_row_scale_lmd_choose_previous_choose_table. ((((exists bcf_height_lmd_choose_previous_choose_table_decoded_row_code. bcf_height_lmd_choose_previous_choose_table_decoded_row_code + S (bcf_row_code_lmd_choose_previous_choose_table) = S ((S (bcf_row_index_lmd_choose_previous_choose_table)) * bcf_row_code_scale_lmd_choose_previous_choose)) /\ exists bcf_quotient_lmd_choose_previous_choose_table_decoded_row_code. bcf_row_code_code_lmd_choose_previous_choose = bcf_quotient_lmd_choose_previous_choose_table_decoded_row_code * S ((S (bcf_row_index_lmd_choose_previous_choose_table)) * bcf_row_code_scale_lmd_choose_previous_choose) + (bcf_row_code_lmd_choose_previous_choose_table))) /\ ((((exists bcf_height_lmd_choose_previous_choose_table_decoded_row_scale. bcf_height_lmd_choose_previous_choose_table_decoded_row_scale + S (bcf_row_scale_lmd_choose_previous_choose_table) = S ((S (bcf_row_index_lmd_choose_previous_choose_table)) * bcf_row_scale_scale_lmd_choose_previous_choose)) /\ exists bcf_quotient_lmd_choose_previous_choose_table_decoded_row_scale. bcf_row_scale_code_lmd_choose_previous_choose = bcf_quotient_lmd_choose_previous_choose_table_decoded_row_scale * S ((S (bcf_row_index_lmd_choose_previous_choose_table)) * bcf_row_scale_scale_lmd_choose_previous_choose) + (bcf_row_scale_lmd_choose_previous_choose_table))) /\ ((bcf_row_index_lmd_choose_previous_choose_table = 0 /\ (forall bcf_index_lmd_choose_previous_choose_table_zero_row. (exists bcf_lt_gap_lmd_choose_previous_choose_table_zero_row_bound. bcf_lt_gap_lmd_choose_previous_choose_table_zero_row_bound + S (bcf_index_lmd_choose_previous_choose_table_zero_row) = S (lmd_choose_upper_choose_previous)) -> exists bcf_value_lmd_choose_previous_choose_table_zero_row. ((((exists bcf_height_lmd_choose_previous_choose_table_zero_row_entry. bcf_height_lmd_choose_previous_choose_table_zero_row_entry + S (bcf_value_lmd_choose_previous_choose_table_zero_row) = S ((S (bcf_index_lmd_choose_previous_choose_table_zero_row)) * bcf_row_scale_lmd_choose_previous_choose_table)) /\ exists bcf_quotient_lmd_choose_previous_choose_table_zero_row_entry. bcf_row_code_lmd_choose_previous_choose_table = bcf_quotient_lmd_choose_previous_choose_table_zero_row_entry * S ((S (bcf_index_lmd_choose_previous_choose_table_zero_row)) * bcf_row_scale_lmd_choose_previous_choose_table) + (bcf_value_lmd_choose_previous_choose_table_zero_row))) /\ ((bcf_index_lmd_choose_previous_choose_table_zero_row = 0 /\ bcf_value_lmd_choose_previous_choose_table_zero_row = 1) \/ exists bcf_predecessor_lmd_choose_previous_choose_table_zero_row. bcf_index_lmd_choose_previous_choose_table_zero_row = S bcf_predecessor_lmd_choose_previous_choose_table_zero_row /\ bcf_value_lmd_choose_previous_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lmd_choose_previous_choose_table bcf_previous_code_lmd_choose_previous_choose_table bcf_previous_scale_lmd_choose_previous_choose_table. bcf_row_index_lmd_choose_previous_choose_table = S bcf_predecessor_lmd_choose_previous_choose_table /\ ((((exists bcf_height_lmd_choose_previous_choose_table_decoded_previous_code. bcf_height_lmd_choose_previous_choose_table_decoded_previous_code + S (bcf_previous_code_lmd_choose_previous_choose_table) = S ((S (bcf_predecessor_lmd_choose_previous_choose_table)) * bcf_row_code_scale_lmd_choose_previous_choose)) /\ exists bcf_quotient_lmd_choose_previous_choose_table_decoded_previous_code. bcf_row_code_code_lmd_choose_previous_choose = bcf_quotient_lmd_choose_previous_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lmd_choose_previous_choose_table)) * bcf_row_code_scale_lmd_choose_previous_choose) + (bcf_previous_code_lmd_choose_previous_choose_table))) /\ ((((exists bcf_height_lmd_choose_previous_choose_table_decoded_previous_scale. bcf_height_lmd_choose_previous_choose_table_decoded_previous_scale + S (bcf_previous_scale_lmd_choose_previous_choose_table) = S ((S (bcf_predecessor_lmd_choose_previous_choose_table)) * bcf_row_scale_scale_lmd_choose_previous_choose)) /\ exists bcf_quotient_lmd_choose_previous_choose_table_decoded_previous_scale. bcf_row_scale_code_lmd_choose_previous_choose = bcf_quotient_lmd_choose_previous_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lmd_choose_previous_choose_table)) * bcf_row_scale_scale_lmd_choose_previous_choose) + (bcf_previous_scale_lmd_choose_previous_choose_table))) /\ (forall bcf_index_lmd_choose_previous_choose_table_row_step. (exists bcf_lt_gap_lmd_choose_previous_choose_table_row_step_bound. bcf_lt_gap_lmd_choose_previous_choose_table_row_step_bound + S (bcf_index_lmd_choose_previous_choose_table_row_step) = S (lmd_choose_upper_choose_previous)) -> exists bcf_value_lmd_choose_previous_choose_table_row_step. ((((exists bcf_height_lmd_choose_previous_choose_table_row_step_entry. bcf_height_lmd_choose_previous_choose_table_row_step_entry + S (bcf_value_lmd_choose_previous_choose_table_row_step) = S ((S (bcf_index_lmd_choose_previous_choose_table_row_step)) * bcf_row_scale_lmd_choose_previous_choose_table)) /\ exists bcf_quotient_lmd_choose_previous_choose_table_row_step_entry. bcf_row_code_lmd_choose_previous_choose_table = bcf_quotient_lmd_choose_previous_choose_table_row_step_entry * S ((S (bcf_index_lmd_choose_previous_choose_table_row_step)) * bcf_row_scale_lmd_choose_previous_choose_table) + (bcf_value_lmd_choose_previous_choose_table_row_step))) /\ ((bcf_index_lmd_choose_previous_choose_table_row_step = 0 /\ bcf_value_lmd_choose_previous_choose_table_row_step = 1) \/ exists bcf_predecessor_lmd_choose_previous_choose_table_row_step bcf_left_lmd_choose_previous_choose_table_row_step bcf_right_lmd_choose_previous_choose_table_row_step. bcf_index_lmd_choose_previous_choose_table_row_step = S bcf_predecessor_lmd_choose_previous_choose_table_row_step /\ ((((exists bcf_height_lmd_choose_previous_choose_table_row_step_previous_left. bcf_height_lmd_choose_previous_choose_table_row_step_previous_left + S (bcf_left_lmd_choose_previous_choose_table_row_step) = S ((S (bcf_predecessor_lmd_choose_previous_choose_table_row_step)) * bcf_previous_scale_lmd_choose_previous_choose_table)) /\ exists bcf_quotient_lmd_choose_previous_choose_table_row_step_previous_left. bcf_previous_code_lmd_choose_previous_choose_table = bcf_quotient_lmd_choose_previous_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lmd_choose_previous_choose_table_row_step)) * bcf_previous_scale_lmd_choose_previous_choose_table) + (bcf_left_lmd_choose_previous_choose_table_row_step))) /\ ((((exists bcf_height_lmd_choose_previous_choose_table_row_step_previous_right. bcf_height_lmd_choose_previous_choose_table_row_step_previous_right + S (bcf_right_lmd_choose_previous_choose_table_row_step) = S ((S (S (bcf_predecessor_lmd_choose_previous_choose_table_row_step))) * bcf_previous_scale_lmd_choose_previous_choose_table)) /\ exists bcf_quotient_lmd_choose_previous_choose_table_row_step_previous_right. bcf_previous_code_lmd_choose_previous_choose_table = bcf_quotient_lmd_choose_previous_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lmd_choose_previous_choose_table_row_step))) * bcf_previous_scale_lmd_choose_previous_choose_table) + (bcf_right_lmd_choose_previous_choose_table_row_step))) /\ bcf_value_lmd_choose_previous_choose_table_row_step = bcf_left_lmd_choose_previous_choose_table_row_step + bcf_right_lmd_choose_previous_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lmd_choose_previous_choose_decoded_row_code. bcf_height_lmd_choose_previous_choose_decoded_row_code + S (bcf_row_code_lmd_choose_previous_choose) = S ((S (lmd_choose_upper_choose_previous)) * bcf_row_code_scale_lmd_choose_previous_choose)) /\ exists bcf_quotient_lmd_choose_previous_choose_decoded_row_code. bcf_row_code_code_lmd_choose_previous_choose = bcf_quotient_lmd_choose_previous_choose_decoded_row_code * S ((S (lmd_choose_upper_choose_previous)) * bcf_row_code_scale_lmd_choose_previous_choose) + (bcf_row_code_lmd_choose_previous_choose))) /\ ((((exists bcf_height_lmd_choose_previous_choose_decoded_row_scale. bcf_height_lmd_choose_previous_choose_decoded_row_scale + S (bcf_row_scale_lmd_choose_previous_choose) = S ((S (lmd_choose_upper_choose_previous)) * bcf_row_scale_scale_lmd_choose_previous_choose)) /\ exists bcf_quotient_lmd_choose_previous_choose_decoded_row_scale. bcf_row_scale_code_lmd_choose_previous_choose = bcf_quotient_lmd_choose_previous_choose_decoded_row_scale * S ((S (lmd_choose_upper_choose_previous)) * bcf_row_scale_scale_lmd_choose_previous_choose) + (bcf_row_scale_lmd_choose_previous_choose))) /\ (((exists bcf_height_lmd_choose_previous_choose_decoded_value. bcf_height_lmd_choose_previous_choose_decoded_value + S (lmd_choose_value_choose_previous) = S ((S (lmd_choose_lower_choose_previous)) * bcf_row_scale_lmd_choose_previous_choose)) /\ exists bcf_quotient_lmd_choose_previous_choose_decoded_value. bcf_row_code_lmd_choose_previous_choose = bcf_quotient_lmd_choose_previous_choose_decoded_value * S ((S (lmd_choose_lower_choose_previous)) * bcf_row_scale_lmd_choose_previous_choose) + (lmd_choose_value_choose_previous)))))))))))))
  9. 0009exact IH
  10. 0010cases hprevious
  11. 0011cases hprevious_witness
  12. 0012specialize lucas_choose_prefix_extend qb
  13. 0013specialize lucas_choose_prefix_extend qc
  14. 0014specialize lucas_choose_prefix_extend db
  15. 0015specialize lucas_choose_prefix_extend dc
  16. 0016specialize lucas_choose_prefix_extend x
  17. 0017specialize lucas_choose_prefix_extend x1
  18. 0018specialize lucas_choose_prefix_extend l
  19. 0019apply lucas_choose_prefix_extend
  20. 0020exact hprevious_witness_witness