MK000B

multinomial_binomial_prefix_exists

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

Construct all actual binomial factors for any finite decoded part and partial-sum tables.

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 b c sb sc l. exists cb cc. (forall mkm_index_binexists_target. (exists mkm_lt_binexists_target_bound. mkm_lt_binexists_target_bound + S (mkm_index_binexists_target) = (l)) -> (exists mkm_value_binexists_target_point mkm_partial_binexists_target_point mkm_factor_binexists_target_point. (((exists fs_h_mkm_binexists_target_point_source. fs_h_mkm_binexists_target_point_source + S (mkm_value_binexists_target_point) = S ((S (mkm_index_binexists_target)) * c)) /\ exists fs_q_mkm_binexists_target_point_source. b = fs_q_mkm_binexists_target_point_source * S ((S (mkm_index_binexists_target)) * c) + (mkm_value_binexists_target_point))) /\ ((((exists fs_h_mkm_binexists_target_point_partial. fs_h_mkm_binexists_target_point_partial + S (mkm_partial_binexists_target_point) = S ((S (mkm_index_binexists_target)) * sc)) /\ exists fs_q_mkm_binexists_target_point_partial. sb = fs_q_mkm_binexists_target_point_partial * S ((S (mkm_index_binexists_target)) * sc) + (mkm_partial_binexists_target_point))) /\ ((((exists bcf_lt_gap_mkm_binexists_target_point_choose_out_of_range. bcf_lt_gap_mkm_binexists_target_point_choose_out_of_range + S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point) = mkm_partial_binexists_target_point) /\ mkm_factor_binexists_target_point = 0) \/ ((exists bcf_le_gap_mkm_binexists_target_point_choose_in_range. bcf_le_gap_mkm_binexists_target_point_choose_in_range + (mkm_partial_binexists_target_point) = mkm_partial_binexists_target_point + mkm_value_binexists_target_point) /\ (exists bcf_row_code_code_mkm_binexists_target_point_choose bcf_row_code_scale_mkm_binexists_target_point_choose bcf_row_scale_code_mkm_binexists_target_point_choose bcf_row_scale_scale_mkm_binexists_target_point_choose bcf_row_code_mkm_binexists_target_point_choose bcf_row_scale_mkm_binexists_target_point_choose. ((forall bcf_row_index_mkm_binexists_target_point_choose_table. (exists bcf_lt_gap_mkm_binexists_target_point_choose_table_row_bound. bcf_lt_gap_mkm_binexists_target_point_choose_table_row_bound + S (bcf_row_index_mkm_binexists_target_point_choose_table) = S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point)) -> exists bcf_row_code_mkm_binexists_target_point_choose_table bcf_row_scale_mkm_binexists_target_point_choose_table. ((((exists bcf_height_mkm_binexists_target_point_choose_table_decoded_row_code. bcf_height_mkm_binexists_target_point_choose_table_decoded_row_code + S (bcf_row_code_mkm_binexists_target_point_choose_table) = S ((S (bcf_row_index_mkm_binexists_target_point_choose_table)) * bcf_row_code_scale_mkm_binexists_target_point_choose)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_decoded_row_code. bcf_row_code_code_mkm_binexists_target_point_choose = bcf_quotient_mkm_binexists_target_point_choose_table_decoded_row_code * S ((S (bcf_row_index_mkm_binexists_target_point_choose_table)) * bcf_row_code_scale_mkm_binexists_target_point_choose) + (bcf_row_code_mkm_binexists_target_point_choose_table))) /\ ((((exists bcf_height_mkm_binexists_target_point_choose_table_decoded_row_scale. bcf_height_mkm_binexists_target_point_choose_table_decoded_row_scale + S (bcf_row_scale_mkm_binexists_target_point_choose_table) = S ((S (bcf_row_index_mkm_binexists_target_point_choose_table)) * bcf_row_scale_scale_mkm_binexists_target_point_choose)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_decoded_row_scale. bcf_row_scale_code_mkm_binexists_target_point_choose = bcf_quotient_mkm_binexists_target_point_choose_table_decoded_row_scale * S ((S (bcf_row_index_mkm_binexists_target_point_choose_table)) * bcf_row_scale_scale_mkm_binexists_target_point_choose) + (bcf_row_scale_mkm_binexists_target_point_choose_table))) /\ ((bcf_row_index_mkm_binexists_target_point_choose_table = 0 /\ (forall bcf_index_mkm_binexists_target_point_choose_table_zero_row. (exists bcf_lt_gap_mkm_binexists_target_point_choose_table_zero_row_bound. bcf_lt_gap_mkm_binexists_target_point_choose_table_zero_row_bound + S (bcf_index_mkm_binexists_target_point_choose_table_zero_row) = S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point)) -> exists bcf_value_mkm_binexists_target_point_choose_table_zero_row. ((((exists bcf_height_mkm_binexists_target_point_choose_table_zero_row_entry. bcf_height_mkm_binexists_target_point_choose_table_zero_row_entry + S (bcf_value_mkm_binexists_target_point_choose_table_zero_row) = S ((S (bcf_index_mkm_binexists_target_point_choose_table_zero_row)) * bcf_row_scale_mkm_binexists_target_point_choose_table)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_zero_row_entry. bcf_row_code_mkm_binexists_target_point_choose_table = bcf_quotient_mkm_binexists_target_point_choose_table_zero_row_entry * S ((S (bcf_index_mkm_binexists_target_point_choose_table_zero_row)) * bcf_row_scale_mkm_binexists_target_point_choose_table) + (bcf_value_mkm_binexists_target_point_choose_table_zero_row))) /\ ((bcf_index_mkm_binexists_target_point_choose_table_zero_row = 0 /\ bcf_value_mkm_binexists_target_point_choose_table_zero_row = 1) \/ exists bcf_predecessor_mkm_binexists_target_point_choose_table_zero_row. bcf_index_mkm_binexists_target_point_choose_table_zero_row = S bcf_predecessor_mkm_binexists_target_point_choose_table_zero_row /\ bcf_value_mkm_binexists_target_point_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_mkm_binexists_target_point_choose_table bcf_previous_code_mkm_binexists_target_point_choose_table bcf_previous_scale_mkm_binexists_target_point_choose_table. bcf_row_index_mkm_binexists_target_point_choose_table = S bcf_predecessor_mkm_binexists_target_point_choose_table /\ ((((exists bcf_height_mkm_binexists_target_point_choose_table_decoded_previous_code. bcf_height_mkm_binexists_target_point_choose_table_decoded_previous_code + S (bcf_previous_code_mkm_binexists_target_point_choose_table) = S ((S (bcf_predecessor_mkm_binexists_target_point_choose_table)) * bcf_row_code_scale_mkm_binexists_target_point_choose)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_decoded_previous_code. bcf_row_code_code_mkm_binexists_target_point_choose = bcf_quotient_mkm_binexists_target_point_choose_table_decoded_previous_code * S ((S (bcf_predecessor_mkm_binexists_target_point_choose_table)) * bcf_row_code_scale_mkm_binexists_target_point_choose) + (bcf_previous_code_mkm_binexists_target_point_choose_table))) /\ ((((exists bcf_height_mkm_binexists_target_point_choose_table_decoded_previous_scale. bcf_height_mkm_binexists_target_point_choose_table_decoded_previous_scale + S (bcf_previous_scale_mkm_binexists_target_point_choose_table) = S ((S (bcf_predecessor_mkm_binexists_target_point_choose_table)) * bcf_row_scale_scale_mkm_binexists_target_point_choose)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_decoded_previous_scale. bcf_row_scale_code_mkm_binexists_target_point_choose = bcf_quotient_mkm_binexists_target_point_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_mkm_binexists_target_point_choose_table)) * bcf_row_scale_scale_mkm_binexists_target_point_choose) + (bcf_previous_scale_mkm_binexists_target_point_choose_table))) /\ (forall bcf_index_mkm_binexists_target_point_choose_table_row_step. (exists bcf_lt_gap_mkm_binexists_target_point_choose_table_row_step_bound. bcf_lt_gap_mkm_binexists_target_point_choose_table_row_step_bound + S (bcf_index_mkm_binexists_target_point_choose_table_row_step) = S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point)) -> exists bcf_value_mkm_binexists_target_point_choose_table_row_step. ((((exists bcf_height_mkm_binexists_target_point_choose_table_row_step_entry. bcf_height_mkm_binexists_target_point_choose_table_row_step_entry + S (bcf_value_mkm_binexists_target_point_choose_table_row_step) = S ((S (bcf_index_mkm_binexists_target_point_choose_table_row_step)) * bcf_row_scale_mkm_binexists_target_point_choose_table)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_row_step_entry. bcf_row_code_mkm_binexists_target_point_choose_table = bcf_quotient_mkm_binexists_target_point_choose_table_row_step_entry * S ((S (bcf_index_mkm_binexists_target_point_choose_table_row_step)) * bcf_row_scale_mkm_binexists_target_point_choose_table) + (bcf_value_mkm_binexists_target_point_choose_table_row_step))) /\ ((bcf_index_mkm_binexists_target_point_choose_table_row_step = 0 /\ bcf_value_mkm_binexists_target_point_choose_table_row_step = 1) \/ exists bcf_predecessor_mkm_binexists_target_point_choose_table_row_step bcf_left_mkm_binexists_target_point_choose_table_row_step bcf_right_mkm_binexists_target_point_choose_table_row_step. bcf_index_mkm_binexists_target_point_choose_table_row_step = S bcf_predecessor_mkm_binexists_target_point_choose_table_row_step /\ ((((exists bcf_height_mkm_binexists_target_point_choose_table_row_step_previous_left. bcf_height_mkm_binexists_target_point_choose_table_row_step_previous_left + S (bcf_left_mkm_binexists_target_point_choose_table_row_step) = S ((S (bcf_predecessor_mkm_binexists_target_point_choose_table_row_step)) * bcf_previous_scale_mkm_binexists_target_point_choose_table)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_row_step_previous_left. bcf_previous_code_mkm_binexists_target_point_choose_table = bcf_quotient_mkm_binexists_target_point_choose_table_row_step_previous_left * S ((S (bcf_predecessor_mkm_binexists_target_point_choose_table_row_step)) * bcf_previous_scale_mkm_binexists_target_point_choose_table) + (bcf_left_mkm_binexists_target_point_choose_table_row_step))) /\ ((((exists bcf_height_mkm_binexists_target_point_choose_table_row_step_previous_right. bcf_height_mkm_binexists_target_point_choose_table_row_step_previous_right + S (bcf_right_mkm_binexists_target_point_choose_table_row_step) = S ((S (S (bcf_predecessor_mkm_binexists_target_point_choose_table_row_step))) * bcf_previous_scale_mkm_binexists_target_point_choose_table)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_row_step_previous_right. bcf_previous_code_mkm_binexists_target_point_choose_table = bcf_quotient_mkm_binexists_target_point_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_mkm_binexists_target_point_choose_table_row_step))) * bcf_previous_scale_mkm_binexists_target_point_choose_table) + (bcf_right_mkm_binexists_target_point_choose_table_row_step))) /\ bcf_value_mkm_binexists_target_point_choose_table_row_step = bcf_left_mkm_binexists_target_point_choose_table_row_step + bcf_right_mkm_binexists_target_point_choose_table_row_step))))))))))) /\ ((((exists bcf_height_mkm_binexists_target_point_choose_decoded_row_code. bcf_height_mkm_binexists_target_point_choose_decoded_row_code + S (bcf_row_code_mkm_binexists_target_point_choose) = S ((S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point)) * bcf_row_code_scale_mkm_binexists_target_point_choose)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_decoded_row_code. bcf_row_code_code_mkm_binexists_target_point_choose = bcf_quotient_mkm_binexists_target_point_choose_decoded_row_code * S ((S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point)) * bcf_row_code_scale_mkm_binexists_target_point_choose) + (bcf_row_code_mkm_binexists_target_point_choose))) /\ ((((exists bcf_height_mkm_binexists_target_point_choose_decoded_row_scale. bcf_height_mkm_binexists_target_point_choose_decoded_row_scale + S (bcf_row_scale_mkm_binexists_target_point_choose) = S ((S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point)) * bcf_row_scale_scale_mkm_binexists_target_point_choose)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_decoded_row_scale. bcf_row_scale_code_mkm_binexists_target_point_choose = bcf_quotient_mkm_binexists_target_point_choose_decoded_row_scale * S ((S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point)) * bcf_row_scale_scale_mkm_binexists_target_point_choose) + (bcf_row_scale_mkm_binexists_target_point_choose))) /\ (((exists bcf_height_mkm_binexists_target_point_choose_decoded_value. bcf_height_mkm_binexists_target_point_choose_decoded_value + S (mkm_factor_binexists_target_point) = S ((S (mkm_partial_binexists_target_point)) * bcf_row_scale_mkm_binexists_target_point_choose)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_decoded_value. bcf_row_code_mkm_binexists_target_point_choose = bcf_quotient_mkm_binexists_target_point_choose_decoded_value * S ((S (mkm_partial_binexists_target_point)) * bcf_row_scale_mkm_binexists_target_point_choose) + (mkm_factor_binexists_target_point))))))))) /\ (((exists fs_h_mkm_binexists_target_point_factor. fs_h_mkm_binexists_target_point_factor + S (mkm_factor_binexists_target_point) = S ((S (mkm_index_binexists_target)) * cc)) /\ exists fs_q_mkm_binexists_target_point_factor. cb = fs_q_mkm_binexists_target_point_factor * S ((S (mkm_index_binexists_target)) * cc) + (mkm_factor_binexists_target_point)))))))

Constructive proof overview

Generated structural guide

Construct all actual binomial factors for any finite decoded part and partial-sum tables.

The unchanged tactic script uses 4 declared prerequisites and contains 50 exact native proof lines.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

MK0008 multinomial_binomial_prefix_empty beta_at_exists Stable theorem; checked-use authorized choose_exists Alpha theorem; checked-use authorized MK000A multinomial_binomial_prefix_extend

Direct dependents

MK000D multinomial_exists_of_sum

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

50 script commands · 14 reading checkpoints · 4 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)
multinomial binomial prefix emptymultinomial binomial 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–4

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro sb
  4. L4
    intro sc
02Induction on lL5–5

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

  1. L5
    induction l
03Construct an explicit witnessL6–7

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

  1. L6
    exists 0
  2. L7
    exists 0
04Use earlier factsL8–14

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

  1. L8
    specialize multinomial_binomial_prefix_empty b
  2. L9
    specialize multinomial_binomial_prefix_empty c
  3. L10
    specialize multinomial_binomial_prefix_empty sb
  4. L11
    specialize multinomial_binomial_prefix_empty sc
  5. L12
    specialize multinomial_binomial_prefix_empty 0
  6. L13
    specialize multinomial_binomial_prefix_empty 0
  7. L14
    apply multinomial_binomial_prefix_empty
05Establish hprefixL15–16

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

  1. L15
    have hprefix : ∃ cb. ∃ cc. MultinomialBinomialPrefix(b,c,sb,sc,cb,cc,l)Definitions: MultinomialBinomialPrefix
  2. L16
    apply IH
06Separate the logical casesL17–18

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

  1. L17
    cases hprefix
  2. L18
    cases hprefix_witness
07Establish hpartL19–23

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

  1. L19
    have hpart : exists a. ((exists fs_h_mkm_binexists_part. fs_h_mkm_binexists_part + S (a) = S ((S (l)) * c)) /\ exists fs_q_mkm_binexists_part. b = fs_q_mkm_binexists_part * S ((S (l)) * c) + (a))
  2. L20
    specialize beta_at_exists b
  3. L21
    specialize beta_at_exists c
  4. L22
    specialize beta_at_exists l
  5. L23
    apply beta_at_exists
08Separate the logical casesL24–24

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

  1. L24
    cases hpart
09Establish hpartialL25–29

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

  1. L25
    have hpartial : exists u. ((exists fs_h_mkm_binexists_partial. fs_h_mkm_binexists_partial + S (u) = S ((S (l)) * sc)) /\ exists fs_q_mkm_binexists_partial. sb = fs_q_mkm_binexists_partial * S ((S (l)) * sc) + (u))
  2. L26
    specialize beta_at_exists sb
  3. L27
    specialize beta_at_exists sc
  4. L28
    specialize beta_at_exists l
  5. L29
    apply beta_at_exists
10Separate the logical casesL30–30

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

  1. L30
    cases hpartial
11Establish hchooseL31–34

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

  1. L31
    have hchoose : ∃ C. Choose(x3 + x2,x3,C)Definitions: Choose
  2. L32
    specialize choose_exists (x3 + x2)
  3. L33
    specialize choose_exists x3
  4. L34
    apply choose_exists
12Separate the logical casesL35–35

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

  1. L35
    cases hchoose
13Use earlier factsL36–45

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

  1. L36
    specialize multinomial_binomial_prefix_extend b
  2. L37
    specialize multinomial_binomial_prefix_extend c
  3. L38
    specialize multinomial_binomial_prefix_extend sb
  4. L39
    specialize multinomial_binomial_prefix_extend sc
  5. L40
    specialize multinomial_binomial_prefix_extend x
  6. L41
    specialize multinomial_binomial_prefix_extend x1
  7. L42
    specialize multinomial_binomial_prefix_extend l
  8. L43
    specialize multinomial_binomial_prefix_extend x2
  9. L44
    specialize multinomial_binomial_prefix_extend x3
  10. L45
    specialize multinomial_binomial_prefix_extend x4
14Use earlier factsL46–50

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

  1. L46
    apply multinomial_binomial_prefix_extend
  2. L47
    exact hprefix_witness_witness
  3. L48
    exact hpart_witness
  4. L49
    exact hpartial_witness
  5. L50
    exact hchoose_witness

Library-wide reading audit

Original exact command ledger · 50 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro sb
  4. 0004intro sc
  5. 0005induction l
  6. 0006exists 0
  7. 0007exists 0
  8. 0008specialize multinomial_binomial_prefix_empty b
  9. 0009specialize multinomial_binomial_prefix_empty c
  10. 0010specialize multinomial_binomial_prefix_empty sb
  11. 0011specialize multinomial_binomial_prefix_empty sc
  12. 0012specialize multinomial_binomial_prefix_empty 0
  13. 0013specialize multinomial_binomial_prefix_empty 0
  14. 0014apply multinomial_binomial_prefix_empty
  15. 0015have hprefix : exists cb cc. forall mkm_index_binexists_prefix. (exists mkm_lt_binexists_prefix_bound. mkm_lt_binexists_prefix_bound + S (mkm_index_binexists_prefix) = (l)) -> (exists mkm_value_binexists_prefix_point mkm_partial_binexists_prefix_point mkm_factor_binexists_prefix_point. (((exists fs_h_mkm_binexists_prefix_point_source. fs_h_mkm_binexists_prefix_point_source + S (mkm_value_binexists_prefix_point) = S ((S (mkm_index_binexists_prefix)) * c)) /\ exists fs_q_mkm_binexists_prefix_point_source. b = fs_q_mkm_binexists_prefix_point_source * S ((S (mkm_index_binexists_prefix)) * c) + (mkm_value_binexists_prefix_point))) /\ ((((exists fs_h_mkm_binexists_prefix_point_partial. fs_h_mkm_binexists_prefix_point_partial + S (mkm_partial_binexists_prefix_point) = S ((S (mkm_index_binexists_prefix)) * sc)) /\ exists fs_q_mkm_binexists_prefix_point_partial. sb = fs_q_mkm_binexists_prefix_point_partial * S ((S (mkm_index_binexists_prefix)) * sc) + (mkm_partial_binexists_prefix_point))) /\ ((((exists bcf_lt_gap_mkm_binexists_prefix_point_choose_out_of_range. bcf_lt_gap_mkm_binexists_prefix_point_choose_out_of_range + S (mkm_partial_binexists_prefix_point + mkm_value_binexists_prefix_point) = mkm_partial_binexists_prefix_point) /\ mkm_factor_binexists_prefix_point = 0) \/ ((exists bcf_le_gap_mkm_binexists_prefix_point_choose_in_range. bcf_le_gap_mkm_binexists_prefix_point_choose_in_range + (mkm_partial_binexists_prefix_point) = mkm_partial_binexists_prefix_point + mkm_value_binexists_prefix_point) /\ (exists bcf_row_code_code_mkm_binexists_prefix_point_choose bcf_row_code_scale_mkm_binexists_prefix_point_choose bcf_row_scale_code_mkm_binexists_prefix_point_choose bcf_row_scale_scale_mkm_binexists_prefix_point_choose bcf_row_code_mkm_binexists_prefix_point_choose bcf_row_scale_mkm_binexists_prefix_point_choose. ((forall bcf_row_index_mkm_binexists_prefix_point_choose_table. (exists bcf_lt_gap_mkm_binexists_prefix_point_choose_table_row_bound. bcf_lt_gap_mkm_binexists_prefix_point_choose_table_row_bound + S (bcf_row_index_mkm_binexists_prefix_point_choose_table) = S (mkm_partial_binexists_prefix_point + mkm_value_binexists_prefix_point)) -> exists bcf_row_code_mkm_binexists_prefix_point_choose_table bcf_row_scale_mkm_binexists_prefix_point_choose_table. ((((exists bcf_height_mkm_binexists_prefix_point_choose_table_decoded_row_code. bcf_height_mkm_binexists_prefix_point_choose_table_decoded_row_code + S (bcf_row_code_mkm_binexists_prefix_point_choose_table) = S ((S (bcf_row_index_mkm_binexists_prefix_point_choose_table)) * bcf_row_code_scale_mkm_binexists_prefix_point_choose)) /\ exists bcf_quotient_mkm_binexists_prefix_point_choose_table_decoded_row_code. bcf_row_code_code_mkm_binexists_prefix_point_choose = bcf_quotient_mkm_binexists_prefix_point_choose_table_decoded_row_code * S ((S (bcf_row_index_mkm_binexists_prefix_point_choose_table)) * bcf_row_code_scale_mkm_binexists_prefix_point_choose) + (bcf_row_code_mkm_binexists_prefix_point_choose_table))) /\ ((((exists bcf_height_mkm_binexists_prefix_point_choose_table_decoded_row_scale. bcf_height_mkm_binexists_prefix_point_choose_table_decoded_row_scale + S (bcf_row_scale_mkm_binexists_prefix_point_choose_table) = S ((S (bcf_row_index_mkm_binexists_prefix_point_choose_table)) * bcf_row_scale_scale_mkm_binexists_prefix_point_choose)) /\ exists bcf_quotient_mkm_binexists_prefix_point_choose_table_decoded_row_scale. bcf_row_scale_code_mkm_binexists_prefix_point_choose = bcf_quotient_mkm_binexists_prefix_point_choose_table_decoded_row_scale * S ((S (bcf_row_index_mkm_binexists_prefix_point_choose_table)) * bcf_row_scale_scale_mkm_binexists_prefix_point_choose) + (bcf_row_scale_mkm_binexists_prefix_point_choose_table))) /\ ((bcf_row_index_mkm_binexists_prefix_point_choose_table = 0 /\ (forall bcf_index_mkm_binexists_prefix_point_choose_table_zero_row. (exists bcf_lt_gap_mkm_binexists_prefix_point_choose_table_zero_row_bound. bcf_lt_gap_mkm_binexists_prefix_point_choose_table_zero_row_bound + S (bcf_index_mkm_binexists_prefix_point_choose_table_zero_row) = S (mkm_partial_binexists_prefix_point + mkm_value_binexists_prefix_point)) -> exists bcf_value_mkm_binexists_prefix_point_choose_table_zero_row. ((((exists bcf_height_mkm_binexists_prefix_point_choose_table_zero_row_entry. bcf_height_mkm_binexists_prefix_point_choose_table_zero_row_entry + S (bcf_value_mkm_binexists_prefix_point_choose_table_zero_row) = S ((S (bcf_index_mkm_binexists_prefix_point_choose_table_zero_row)) * bcf_row_scale_mkm_binexists_prefix_point_choose_table)) /\ exists bcf_quotient_mkm_binexists_prefix_point_choose_table_zero_row_entry. bcf_row_code_mkm_binexists_prefix_point_choose_table = bcf_quotient_mkm_binexists_prefix_point_choose_table_zero_row_entry * S ((S (bcf_index_mkm_binexists_prefix_point_choose_table_zero_row)) * bcf_row_scale_mkm_binexists_prefix_point_choose_table) + (bcf_value_mkm_binexists_prefix_point_choose_table_zero_row))) /\ ((bcf_index_mkm_binexists_prefix_point_choose_table_zero_row = 0 /\ bcf_value_mkm_binexists_prefix_point_choose_table_zero_row = 1) \/ exists bcf_predecessor_mkm_binexists_prefix_point_choose_table_zero_row. bcf_index_mkm_binexists_prefix_point_choose_table_zero_row = S bcf_predecessor_mkm_binexists_prefix_point_choose_table_zero_row /\ bcf_value_mkm_binexists_prefix_point_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_mkm_binexists_prefix_point_choose_table bcf_previous_code_mkm_binexists_prefix_point_choose_table bcf_previous_scale_mkm_binexists_prefix_point_choose_table. bcf_row_index_mkm_binexists_prefix_point_choose_table = S bcf_predecessor_mkm_binexists_prefix_point_choose_table /\ ((((exists bcf_height_mkm_binexists_prefix_point_choose_table_decoded_previous_code. bcf_height_mkm_binexists_prefix_point_choose_table_decoded_previous_code + S (bcf_previous_code_mkm_binexists_prefix_point_choose_table) = S ((S (bcf_predecessor_mkm_binexists_prefix_point_choose_table)) * bcf_row_code_scale_mkm_binexists_prefix_point_choose)) /\ exists bcf_quotient_mkm_binexists_prefix_point_choose_table_decoded_previous_code. bcf_row_code_code_mkm_binexists_prefix_point_choose = bcf_quotient_mkm_binexists_prefix_point_choose_table_decoded_previous_code * S ((S (bcf_predecessor_mkm_binexists_prefix_point_choose_table)) * bcf_row_code_scale_mkm_binexists_prefix_point_choose) + (bcf_previous_code_mkm_binexists_prefix_point_choose_table))) /\ ((((exists bcf_height_mkm_binexists_prefix_point_choose_table_decoded_previous_scale. bcf_height_mkm_binexists_prefix_point_choose_table_decoded_previous_scale + S (bcf_previous_scale_mkm_binexists_prefix_point_choose_table) = S ((S (bcf_predecessor_mkm_binexists_prefix_point_choose_table)) * bcf_row_scale_scale_mkm_binexists_prefix_point_choose)) /\ exists bcf_quotient_mkm_binexists_prefix_point_choose_table_decoded_previous_scale. bcf_row_scale_code_mkm_binexists_prefix_point_choose = bcf_quotient_mkm_binexists_prefix_point_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_mkm_binexists_prefix_point_choose_table)) * bcf_row_scale_scale_mkm_binexists_prefix_point_choose) + (bcf_previous_scale_mkm_binexists_prefix_point_choose_table))) /\ (forall bcf_index_mkm_binexists_prefix_point_choose_table_row_step. (exists bcf_lt_gap_mkm_binexists_prefix_point_choose_table_row_step_bound. bcf_lt_gap_mkm_binexists_prefix_point_choose_table_row_step_bound + S (bcf_index_mkm_binexists_prefix_point_choose_table_row_step) = S (mkm_partial_binexists_prefix_point + mkm_value_binexists_prefix_point)) -> exists bcf_value_mkm_binexists_prefix_point_choose_table_row_step. ((((exists bcf_height_mkm_binexists_prefix_point_choose_table_row_step_entry. bcf_height_mkm_binexists_prefix_point_choose_table_row_step_entry + S (bcf_value_mkm_binexists_prefix_point_choose_table_row_step) = S ((S (bcf_index_mkm_binexists_prefix_point_choose_table_row_step)) * bcf_row_scale_mkm_binexists_prefix_point_choose_table)) /\ exists bcf_quotient_mkm_binexists_prefix_point_choose_table_row_step_entry. bcf_row_code_mkm_binexists_prefix_point_choose_table = bcf_quotient_mkm_binexists_prefix_point_choose_table_row_step_entry * S ((S (bcf_index_mkm_binexists_prefix_point_choose_table_row_step)) * bcf_row_scale_mkm_binexists_prefix_point_choose_table) + (bcf_value_mkm_binexists_prefix_point_choose_table_row_step))) /\ ((bcf_index_mkm_binexists_prefix_point_choose_table_row_step = 0 /\ bcf_value_mkm_binexists_prefix_point_choose_table_row_step = 1) \/ exists bcf_predecessor_mkm_binexists_prefix_point_choose_table_row_step bcf_left_mkm_binexists_prefix_point_choose_table_row_step bcf_right_mkm_binexists_prefix_point_choose_table_row_step. bcf_index_mkm_binexists_prefix_point_choose_table_row_step = S bcf_predecessor_mkm_binexists_prefix_point_choose_table_row_step /\ ((((exists bcf_height_mkm_binexists_prefix_point_choose_table_row_step_previous_left. bcf_height_mkm_binexists_prefix_point_choose_table_row_step_previous_left + S (bcf_left_mkm_binexists_prefix_point_choose_table_row_step) = S ((S (bcf_predecessor_mkm_binexists_prefix_point_choose_table_row_step)) * bcf_previous_scale_mkm_binexists_prefix_point_choose_table)) /\ exists bcf_quotient_mkm_binexists_prefix_point_choose_table_row_step_previous_left. bcf_previous_code_mkm_binexists_prefix_point_choose_table = bcf_quotient_mkm_binexists_prefix_point_choose_table_row_step_previous_left * S ((S (bcf_predecessor_mkm_binexists_prefix_point_choose_table_row_step)) * bcf_previous_scale_mkm_binexists_prefix_point_choose_table) + (bcf_left_mkm_binexists_prefix_point_choose_table_row_step))) /\ ((((exists bcf_height_mkm_binexists_prefix_point_choose_table_row_step_previous_right. bcf_height_mkm_binexists_prefix_point_choose_table_row_step_previous_right + S (bcf_right_mkm_binexists_prefix_point_choose_table_row_step) = S ((S (S (bcf_predecessor_mkm_binexists_prefix_point_choose_table_row_step))) * bcf_previous_scale_mkm_binexists_prefix_point_choose_table)) /\ exists bcf_quotient_mkm_binexists_prefix_point_choose_table_row_step_previous_right. bcf_previous_code_mkm_binexists_prefix_point_choose_table = bcf_quotient_mkm_binexists_prefix_point_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_mkm_binexists_prefix_point_choose_table_row_step))) * bcf_previous_scale_mkm_binexists_prefix_point_choose_table) + (bcf_right_mkm_binexists_prefix_point_choose_table_row_step))) /\ bcf_value_mkm_binexists_prefix_point_choose_table_row_step = bcf_left_mkm_binexists_prefix_point_choose_table_row_step + bcf_right_mkm_binexists_prefix_point_choose_table_row_step))))))))))) /\ ((((exists bcf_height_mkm_binexists_prefix_point_choose_decoded_row_code. bcf_height_mkm_binexists_prefix_point_choose_decoded_row_code + S (bcf_row_code_mkm_binexists_prefix_point_choose) = S ((S (mkm_partial_binexists_prefix_point + mkm_value_binexists_prefix_point)) * bcf_row_code_scale_mkm_binexists_prefix_point_choose)) /\ exists bcf_quotient_mkm_binexists_prefix_point_choose_decoded_row_code. bcf_row_code_code_mkm_binexists_prefix_point_choose = bcf_quotient_mkm_binexists_prefix_point_choose_decoded_row_code * S ((S (mkm_partial_binexists_prefix_point + mkm_value_binexists_prefix_point)) * bcf_row_code_scale_mkm_binexists_prefix_point_choose) + (bcf_row_code_mkm_binexists_prefix_point_choose))) /\ ((((exists bcf_height_mkm_binexists_prefix_point_choose_decoded_row_scale. bcf_height_mkm_binexists_prefix_point_choose_decoded_row_scale + S (bcf_row_scale_mkm_binexists_prefix_point_choose) = S ((S (mkm_partial_binexists_prefix_point + mkm_value_binexists_prefix_point)) * bcf_row_scale_scale_mkm_binexists_prefix_point_choose)) /\ exists bcf_quotient_mkm_binexists_prefix_point_choose_decoded_row_scale. bcf_row_scale_code_mkm_binexists_prefix_point_choose = bcf_quotient_mkm_binexists_prefix_point_choose_decoded_row_scale * S ((S (mkm_partial_binexists_prefix_point + mkm_value_binexists_prefix_point)) * bcf_row_scale_scale_mkm_binexists_prefix_point_choose) + (bcf_row_scale_mkm_binexists_prefix_point_choose))) /\ (((exists bcf_height_mkm_binexists_prefix_point_choose_decoded_value. bcf_height_mkm_binexists_prefix_point_choose_decoded_value + S (mkm_factor_binexists_prefix_point) = S ((S (mkm_partial_binexists_prefix_point)) * bcf_row_scale_mkm_binexists_prefix_point_choose)) /\ exists bcf_quotient_mkm_binexists_prefix_point_choose_decoded_value. bcf_row_code_mkm_binexists_prefix_point_choose = bcf_quotient_mkm_binexists_prefix_point_choose_decoded_value * S ((S (mkm_partial_binexists_prefix_point)) * bcf_row_scale_mkm_binexists_prefix_point_choose) + (mkm_factor_binexists_prefix_point))))))))) /\ (((exists fs_h_mkm_binexists_prefix_point_factor. fs_h_mkm_binexists_prefix_point_factor + S (mkm_factor_binexists_prefix_point) = S ((S (mkm_index_binexists_prefix)) * cc)) /\ exists fs_q_mkm_binexists_prefix_point_factor. cb = fs_q_mkm_binexists_prefix_point_factor * S ((S (mkm_index_binexists_prefix)) * cc) + (mkm_factor_binexists_prefix_point))))))
  16. 0016apply IH
  17. 0017cases hprefix
  18. 0018cases hprefix_witness
  19. 0019have hpart : exists a. ((exists fs_h_mkm_binexists_part. fs_h_mkm_binexists_part + S (a) = S ((S (l)) * c)) /\ exists fs_q_mkm_binexists_part. b = fs_q_mkm_binexists_part * S ((S (l)) * c) + (a))
  20. 0020specialize beta_at_exists b
  21. 0021specialize beta_at_exists c
  22. 0022specialize beta_at_exists l
  23. 0023apply beta_at_exists
  24. 0024cases hpart
  25. 0025have hpartial : exists u. ((exists fs_h_mkm_binexists_partial. fs_h_mkm_binexists_partial + S (u) = S ((S (l)) * sc)) /\ exists fs_q_mkm_binexists_partial. sb = fs_q_mkm_binexists_partial * S ((S (l)) * sc) + (u))
  26. 0026specialize beta_at_exists sb
  27. 0027specialize beta_at_exists sc
  28. 0028specialize beta_at_exists l
  29. 0029apply beta_at_exists
  30. 0030cases hpartial
  31. 0031have hchoose : exists C. ((exists bcf_lt_gap_mkm_binexists_choose_out_of_range. bcf_lt_gap_mkm_binexists_choose_out_of_range + S (x3 + x2) = x3) /\ C = 0) \/ ((exists bcf_le_gap_mkm_binexists_choose_in_range. bcf_le_gap_mkm_binexists_choose_in_range + (x3) = x3 + x2) /\ (exists bcf_row_code_code_mkm_binexists_choose bcf_row_code_scale_mkm_binexists_choose bcf_row_scale_code_mkm_binexists_choose bcf_row_scale_scale_mkm_binexists_choose bcf_row_code_mkm_binexists_choose bcf_row_scale_mkm_binexists_choose. ((forall bcf_row_index_mkm_binexists_choose_table. (exists bcf_lt_gap_mkm_binexists_choose_table_row_bound. bcf_lt_gap_mkm_binexists_choose_table_row_bound + S (bcf_row_index_mkm_binexists_choose_table) = S (x3 + x2)) -> exists bcf_row_code_mkm_binexists_choose_table bcf_row_scale_mkm_binexists_choose_table. ((((exists bcf_height_mkm_binexists_choose_table_decoded_row_code. bcf_height_mkm_binexists_choose_table_decoded_row_code + S (bcf_row_code_mkm_binexists_choose_table) = S ((S (bcf_row_index_mkm_binexists_choose_table)) * bcf_row_code_scale_mkm_binexists_choose)) /\ exists bcf_quotient_mkm_binexists_choose_table_decoded_row_code. bcf_row_code_code_mkm_binexists_choose = bcf_quotient_mkm_binexists_choose_table_decoded_row_code * S ((S (bcf_row_index_mkm_binexists_choose_table)) * bcf_row_code_scale_mkm_binexists_choose) + (bcf_row_code_mkm_binexists_choose_table))) /\ ((((exists bcf_height_mkm_binexists_choose_table_decoded_row_scale. bcf_height_mkm_binexists_choose_table_decoded_row_scale + S (bcf_row_scale_mkm_binexists_choose_table) = S ((S (bcf_row_index_mkm_binexists_choose_table)) * bcf_row_scale_scale_mkm_binexists_choose)) /\ exists bcf_quotient_mkm_binexists_choose_table_decoded_row_scale. bcf_row_scale_code_mkm_binexists_choose = bcf_quotient_mkm_binexists_choose_table_decoded_row_scale * S ((S (bcf_row_index_mkm_binexists_choose_table)) * bcf_row_scale_scale_mkm_binexists_choose) + (bcf_row_scale_mkm_binexists_choose_table))) /\ ((bcf_row_index_mkm_binexists_choose_table = 0 /\ (forall bcf_index_mkm_binexists_choose_table_zero_row. (exists bcf_lt_gap_mkm_binexists_choose_table_zero_row_bound. bcf_lt_gap_mkm_binexists_choose_table_zero_row_bound + S (bcf_index_mkm_binexists_choose_table_zero_row) = S (x3 + x2)) -> exists bcf_value_mkm_binexists_choose_table_zero_row. ((((exists bcf_height_mkm_binexists_choose_table_zero_row_entry. bcf_height_mkm_binexists_choose_table_zero_row_entry + S (bcf_value_mkm_binexists_choose_table_zero_row) = S ((S (bcf_index_mkm_binexists_choose_table_zero_row)) * bcf_row_scale_mkm_binexists_choose_table)) /\ exists bcf_quotient_mkm_binexists_choose_table_zero_row_entry. bcf_row_code_mkm_binexists_choose_table = bcf_quotient_mkm_binexists_choose_table_zero_row_entry * S ((S (bcf_index_mkm_binexists_choose_table_zero_row)) * bcf_row_scale_mkm_binexists_choose_table) + (bcf_value_mkm_binexists_choose_table_zero_row))) /\ ((bcf_index_mkm_binexists_choose_table_zero_row = 0 /\ bcf_value_mkm_binexists_choose_table_zero_row = 1) \/ exists bcf_predecessor_mkm_binexists_choose_table_zero_row. bcf_index_mkm_binexists_choose_table_zero_row = S bcf_predecessor_mkm_binexists_choose_table_zero_row /\ bcf_value_mkm_binexists_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_mkm_binexists_choose_table bcf_previous_code_mkm_binexists_choose_table bcf_previous_scale_mkm_binexists_choose_table. bcf_row_index_mkm_binexists_choose_table = S bcf_predecessor_mkm_binexists_choose_table /\ ((((exists bcf_height_mkm_binexists_choose_table_decoded_previous_code. bcf_height_mkm_binexists_choose_table_decoded_previous_code + S (bcf_previous_code_mkm_binexists_choose_table) = S ((S (bcf_predecessor_mkm_binexists_choose_table)) * bcf_row_code_scale_mkm_binexists_choose)) /\ exists bcf_quotient_mkm_binexists_choose_table_decoded_previous_code. bcf_row_code_code_mkm_binexists_choose = bcf_quotient_mkm_binexists_choose_table_decoded_previous_code * S ((S (bcf_predecessor_mkm_binexists_choose_table)) * bcf_row_code_scale_mkm_binexists_choose) + (bcf_previous_code_mkm_binexists_choose_table))) /\ ((((exists bcf_height_mkm_binexists_choose_table_decoded_previous_scale. bcf_height_mkm_binexists_choose_table_decoded_previous_scale + S (bcf_previous_scale_mkm_binexists_choose_table) = S ((S (bcf_predecessor_mkm_binexists_choose_table)) * bcf_row_scale_scale_mkm_binexists_choose)) /\ exists bcf_quotient_mkm_binexists_choose_table_decoded_previous_scale. bcf_row_scale_code_mkm_binexists_choose = bcf_quotient_mkm_binexists_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_mkm_binexists_choose_table)) * bcf_row_scale_scale_mkm_binexists_choose) + (bcf_previous_scale_mkm_binexists_choose_table))) /\ (forall bcf_index_mkm_binexists_choose_table_row_step. (exists bcf_lt_gap_mkm_binexists_choose_table_row_step_bound. bcf_lt_gap_mkm_binexists_choose_table_row_step_bound + S (bcf_index_mkm_binexists_choose_table_row_step) = S (x3 + x2)) -> exists bcf_value_mkm_binexists_choose_table_row_step. ((((exists bcf_height_mkm_binexists_choose_table_row_step_entry. bcf_height_mkm_binexists_choose_table_row_step_entry + S (bcf_value_mkm_binexists_choose_table_row_step) = S ((S (bcf_index_mkm_binexists_choose_table_row_step)) * bcf_row_scale_mkm_binexists_choose_table)) /\ exists bcf_quotient_mkm_binexists_choose_table_row_step_entry. bcf_row_code_mkm_binexists_choose_table = bcf_quotient_mkm_binexists_choose_table_row_step_entry * S ((S (bcf_index_mkm_binexists_choose_table_row_step)) * bcf_row_scale_mkm_binexists_choose_table) + (bcf_value_mkm_binexists_choose_table_row_step))) /\ ((bcf_index_mkm_binexists_choose_table_row_step = 0 /\ bcf_value_mkm_binexists_choose_table_row_step = 1) \/ exists bcf_predecessor_mkm_binexists_choose_table_row_step bcf_left_mkm_binexists_choose_table_row_step bcf_right_mkm_binexists_choose_table_row_step. bcf_index_mkm_binexists_choose_table_row_step = S bcf_predecessor_mkm_binexists_choose_table_row_step /\ ((((exists bcf_height_mkm_binexists_choose_table_row_step_previous_left. bcf_height_mkm_binexists_choose_table_row_step_previous_left + S (bcf_left_mkm_binexists_choose_table_row_step) = S ((S (bcf_predecessor_mkm_binexists_choose_table_row_step)) * bcf_previous_scale_mkm_binexists_choose_table)) /\ exists bcf_quotient_mkm_binexists_choose_table_row_step_previous_left. bcf_previous_code_mkm_binexists_choose_table = bcf_quotient_mkm_binexists_choose_table_row_step_previous_left * S ((S (bcf_predecessor_mkm_binexists_choose_table_row_step)) * bcf_previous_scale_mkm_binexists_choose_table) + (bcf_left_mkm_binexists_choose_table_row_step))) /\ ((((exists bcf_height_mkm_binexists_choose_table_row_step_previous_right. bcf_height_mkm_binexists_choose_table_row_step_previous_right + S (bcf_right_mkm_binexists_choose_table_row_step) = S ((S (S (bcf_predecessor_mkm_binexists_choose_table_row_step))) * bcf_previous_scale_mkm_binexists_choose_table)) /\ exists bcf_quotient_mkm_binexists_choose_table_row_step_previous_right. bcf_previous_code_mkm_binexists_choose_table = bcf_quotient_mkm_binexists_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_mkm_binexists_choose_table_row_step))) * bcf_previous_scale_mkm_binexists_choose_table) + (bcf_right_mkm_binexists_choose_table_row_step))) /\ bcf_value_mkm_binexists_choose_table_row_step = bcf_left_mkm_binexists_choose_table_row_step + bcf_right_mkm_binexists_choose_table_row_step))))))))))) /\ ((((exists bcf_height_mkm_binexists_choose_decoded_row_code. bcf_height_mkm_binexists_choose_decoded_row_code + S (bcf_row_code_mkm_binexists_choose) = S ((S (x3 + x2)) * bcf_row_code_scale_mkm_binexists_choose)) /\ exists bcf_quotient_mkm_binexists_choose_decoded_row_code. bcf_row_code_code_mkm_binexists_choose = bcf_quotient_mkm_binexists_choose_decoded_row_code * S ((S (x3 + x2)) * bcf_row_code_scale_mkm_binexists_choose) + (bcf_row_code_mkm_binexists_choose))) /\ ((((exists bcf_height_mkm_binexists_choose_decoded_row_scale. bcf_height_mkm_binexists_choose_decoded_row_scale + S (bcf_row_scale_mkm_binexists_choose) = S ((S (x3 + x2)) * bcf_row_scale_scale_mkm_binexists_choose)) /\ exists bcf_quotient_mkm_binexists_choose_decoded_row_scale. bcf_row_scale_code_mkm_binexists_choose = bcf_quotient_mkm_binexists_choose_decoded_row_scale * S ((S (x3 + x2)) * bcf_row_scale_scale_mkm_binexists_choose) + (bcf_row_scale_mkm_binexists_choose))) /\ (((exists bcf_height_mkm_binexists_choose_decoded_value. bcf_height_mkm_binexists_choose_decoded_value + S (C) = S ((S (x3)) * bcf_row_scale_mkm_binexists_choose)) /\ exists bcf_quotient_mkm_binexists_choose_decoded_value. bcf_row_code_mkm_binexists_choose = bcf_quotient_mkm_binexists_choose_decoded_value * S ((S (x3)) * bcf_row_scale_mkm_binexists_choose) + (C))))))))
  32. 0032specialize choose_exists (x3 + x2)
  33. 0033specialize choose_exists x3
  34. 0034apply choose_exists
  35. 0035cases hchoose
  36. 0036specialize multinomial_binomial_prefix_extend b
  37. 0037specialize multinomial_binomial_prefix_extend c
  38. 0038specialize multinomial_binomial_prefix_extend sb
  39. 0039specialize multinomial_binomial_prefix_extend sc
  40. 0040specialize multinomial_binomial_prefix_extend x
  41. 0041specialize multinomial_binomial_prefix_extend x1
  42. 0042specialize multinomial_binomial_prefix_extend l
  43. 0043specialize multinomial_binomial_prefix_extend x2
  44. 0044specialize multinomial_binomial_prefix_extend x3
  45. 0045specialize multinomial_binomial_prefix_extend x4
  46. 0046apply multinomial_binomial_prefix_extend
  47. 0047exact hprefix_witness_witness
  48. 0048exact hpart_witness
  49. 0049exact hpartial_witness
  50. 0050exact hchoose_witness