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.
Statement with defined notation
∀ qb. ∀ qc. ∀ db. ∀ dc. ∀ l. ∃ 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)))Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.
Definitions used by this theorem
In the theorem statement
In local proof propositions
Exact expanded first-order 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)))))))))))))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.
Read the argument
Proof checkpoints
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)
01Fix variables and assumptionsL1–5
02Induction on lL6–7
03Establish hpreviousL8–9
Establish this local claim before using it. It is not an additional assumption.
- 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: Lt(x,l)BetaAt(qb,qc,x,y)BetaAt(db,dc,x,n)BetaAt(z,t,x,m)Choose(y,n,m)Original native command in the exact edition - L9
exact IH
04Separate the logical casesL10–11
05Use earlier factsL12–20
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L12
specialize lucas_choose_prefix_extend qb - L13
specialize lucas_choose_prefix_extend qc - L14
specialize lucas_choose_prefix_extend db - L15
specialize lucas_choose_prefix_extend dc - L16
specialize lucas_choose_prefix_extend x - L17
specialize lucas_choose_prefix_extend x1 - L18
specialize lucas_choose_prefix_extend l - L19
apply lucas_choose_prefix_extend - L20
exact hprevious_witness_witness
Original defined command ledger · 20 lines
- 0001
intro qb - 0002
intro qc - 0003
intro db - 0004
intro dc - 0005
intro l - 0006
induction l - 0007
apply lucas_choose_prefix_empty - 0008
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)))Exact native replay line
have 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))))))))))))) - 0009
exact IH - 0010
cases hprevious - 0011
cases hprevious_witness - 0012
specialize lucas_choose_prefix_extend qb - 0013
specialize lucas_choose_prefix_extend qc - 0014
specialize lucas_choose_prefix_extend db - 0015
specialize lucas_choose_prefix_extend dc - 0016
specialize lucas_choose_prefix_extend x - 0017
specialize lucas_choose_prefix_extend x1 - 0018
specialize lucas_choose_prefix_extend l - 0019
apply lucas_choose_prefix_extend - 0020
exact hprevious_witness_witness