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
∀ n. ∀ k. ∀ j. ∀ x. ∀ y. k + j = n → Choose(n,k,x) → Choose(S n,k,y) → S j · y = S n · xEvery purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
2 occurrences
In local proof propositions
5 occurrences
Exact expanded native-PA statement
forall n k j x y. k + j = n -> (((exists bcf_lt_gap_bcwv_lower_out_of_range. bcf_lt_gap_bcwv_lower_out_of_range + S (n) = k) /\ x = 0) \/ ((exists bcf_le_gap_bcwv_lower_in_range. bcf_le_gap_bcwv_lower_in_range + (k) = n) /\ (exists bcf_row_code_code_bcwv_lower bcf_row_code_scale_bcwv_lower bcf_row_scale_code_bcwv_lower bcf_row_scale_scale_bcwv_lower bcf_row_code_bcwv_lower bcf_row_scale_bcwv_lower. ((forall bcf_row_index_bcwv_lower_table. (exists bcf_lt_gap_bcwv_lower_table_row_bound. bcf_lt_gap_bcwv_lower_table_row_bound + S (bcf_row_index_bcwv_lower_table) = S (n)) -> exists bcf_row_code_bcwv_lower_table bcf_row_scale_bcwv_lower_table. ((((exists bcf_height_bcwv_lower_table_decoded_row_code. bcf_height_bcwv_lower_table_decoded_row_code + S (bcf_row_code_bcwv_lower_table) = S ((S (bcf_row_index_bcwv_lower_table)) * bcf_row_code_scale_bcwv_lower)) /\ exists bcf_quotient_bcwv_lower_table_decoded_row_code. bcf_row_code_code_bcwv_lower = bcf_quotient_bcwv_lower_table_decoded_row_code * S ((S (bcf_row_index_bcwv_lower_table)) * bcf_row_code_scale_bcwv_lower) + (bcf_row_code_bcwv_lower_table))) /\ ((((exists bcf_height_bcwv_lower_table_decoded_row_scale. bcf_height_bcwv_lower_table_decoded_row_scale + S (bcf_row_scale_bcwv_lower_table) = S ((S (bcf_row_index_bcwv_lower_table)) * bcf_row_scale_scale_bcwv_lower)) /\ exists bcf_quotient_bcwv_lower_table_decoded_row_scale. bcf_row_scale_code_bcwv_lower = bcf_quotient_bcwv_lower_table_decoded_row_scale * S ((S (bcf_row_index_bcwv_lower_table)) * bcf_row_scale_scale_bcwv_lower) + (bcf_row_scale_bcwv_lower_table))) /\ ((bcf_row_index_bcwv_lower_table = 0 /\ (forall bcf_index_bcwv_lower_table_zero_row. (exists bcf_lt_gap_bcwv_lower_table_zero_row_bound. bcf_lt_gap_bcwv_lower_table_zero_row_bound + S (bcf_index_bcwv_lower_table_zero_row) = S (n)) -> exists bcf_value_bcwv_lower_table_zero_row. ((((exists bcf_height_bcwv_lower_table_zero_row_entry. bcf_height_bcwv_lower_table_zero_row_entry + S (bcf_value_bcwv_lower_table_zero_row) = S ((S (bcf_index_bcwv_lower_table_zero_row)) * bcf_row_scale_bcwv_lower_table)) /\ exists bcf_quotient_bcwv_lower_table_zero_row_entry. bcf_row_code_bcwv_lower_table = bcf_quotient_bcwv_lower_table_zero_row_entry * S ((S (bcf_index_bcwv_lower_table_zero_row)) * bcf_row_scale_bcwv_lower_table) + (bcf_value_bcwv_lower_table_zero_row))) /\ ((bcf_index_bcwv_lower_table_zero_row = 0 /\ bcf_value_bcwv_lower_table_zero_row = 1) \/ exists bcf_predecessor_bcwv_lower_table_zero_row. bcf_index_bcwv_lower_table_zero_row = S bcf_predecessor_bcwv_lower_table_zero_row /\ bcf_value_bcwv_lower_table_zero_row = 0)))) \/ exists bcf_predecessor_bcwv_lower_table bcf_previous_code_bcwv_lower_table bcf_previous_scale_bcwv_lower_table. bcf_row_index_bcwv_lower_table = S bcf_predecessor_bcwv_lower_table /\ ((((exists bcf_height_bcwv_lower_table_decoded_previous_code. bcf_height_bcwv_lower_table_decoded_previous_code + S (bcf_previous_code_bcwv_lower_table) = S ((S (bcf_predecessor_bcwv_lower_table)) * bcf_row_code_scale_bcwv_lower)) /\ exists bcf_quotient_bcwv_lower_table_decoded_previous_code. bcf_row_code_code_bcwv_lower = bcf_quotient_bcwv_lower_table_decoded_previous_code * S ((S (bcf_predecessor_bcwv_lower_table)) * bcf_row_code_scale_bcwv_lower) + (bcf_previous_code_bcwv_lower_table))) /\ ((((exists bcf_height_bcwv_lower_table_decoded_previous_scale. bcf_height_bcwv_lower_table_decoded_previous_scale + S (bcf_previous_scale_bcwv_lower_table) = S ((S (bcf_predecessor_bcwv_lower_table)) * bcf_row_scale_scale_bcwv_lower)) /\ exists bcf_quotient_bcwv_lower_table_decoded_previous_scale. bcf_row_scale_code_bcwv_lower = bcf_quotient_bcwv_lower_table_decoded_previous_scale * S ((S (bcf_predecessor_bcwv_lower_table)) * bcf_row_scale_scale_bcwv_lower) + (bcf_previous_scale_bcwv_lower_table))) /\ (forall bcf_index_bcwv_lower_table_row_step. (exists bcf_lt_gap_bcwv_lower_table_row_step_bound. bcf_lt_gap_bcwv_lower_table_row_step_bound + S (bcf_index_bcwv_lower_table_row_step) = S (n)) -> exists bcf_value_bcwv_lower_table_row_step. ((((exists bcf_height_bcwv_lower_table_row_step_entry. bcf_height_bcwv_lower_table_row_step_entry + S (bcf_value_bcwv_lower_table_row_step) = S ((S (bcf_index_bcwv_lower_table_row_step)) * bcf_row_scale_bcwv_lower_table)) /\ exists bcf_quotient_bcwv_lower_table_row_step_entry. bcf_row_code_bcwv_lower_table = bcf_quotient_bcwv_lower_table_row_step_entry * S ((S (bcf_index_bcwv_lower_table_row_step)) * bcf_row_scale_bcwv_lower_table) + (bcf_value_bcwv_lower_table_row_step))) /\ ((bcf_index_bcwv_lower_table_row_step = 0 /\ bcf_value_bcwv_lower_table_row_step = 1) \/ exists bcf_predecessor_bcwv_lower_table_row_step bcf_left_bcwv_lower_table_row_step bcf_right_bcwv_lower_table_row_step. bcf_index_bcwv_lower_table_row_step = S bcf_predecessor_bcwv_lower_table_row_step /\ ((((exists bcf_height_bcwv_lower_table_row_step_previous_left. bcf_height_bcwv_lower_table_row_step_previous_left + S (bcf_left_bcwv_lower_table_row_step) = S ((S (bcf_predecessor_bcwv_lower_table_row_step)) * bcf_previous_scale_bcwv_lower_table)) /\ exists bcf_quotient_bcwv_lower_table_row_step_previous_left. bcf_previous_code_bcwv_lower_table = bcf_quotient_bcwv_lower_table_row_step_previous_left * S ((S (bcf_predecessor_bcwv_lower_table_row_step)) * bcf_previous_scale_bcwv_lower_table) + (bcf_left_bcwv_lower_table_row_step))) /\ ((((exists bcf_height_bcwv_lower_table_row_step_previous_right. bcf_height_bcwv_lower_table_row_step_previous_right + S (bcf_right_bcwv_lower_table_row_step) = S ((S (S (bcf_predecessor_bcwv_lower_table_row_step))) * bcf_previous_scale_bcwv_lower_table)) /\ exists bcf_quotient_bcwv_lower_table_row_step_previous_right. bcf_previous_code_bcwv_lower_table = bcf_quotient_bcwv_lower_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcwv_lower_table_row_step))) * bcf_previous_scale_bcwv_lower_table) + (bcf_right_bcwv_lower_table_row_step))) /\ bcf_value_bcwv_lower_table_row_step = bcf_left_bcwv_lower_table_row_step + bcf_right_bcwv_lower_table_row_step))))))))))) /\ ((((exists bcf_height_bcwv_lower_decoded_row_code. bcf_height_bcwv_lower_decoded_row_code + S (bcf_row_code_bcwv_lower) = S ((S (n)) * bcf_row_code_scale_bcwv_lower)) /\ exists bcf_quotient_bcwv_lower_decoded_row_code. bcf_row_code_code_bcwv_lower = bcf_quotient_bcwv_lower_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcwv_lower) + (bcf_row_code_bcwv_lower))) /\ ((((exists bcf_height_bcwv_lower_decoded_row_scale. bcf_height_bcwv_lower_decoded_row_scale + S (bcf_row_scale_bcwv_lower) = S ((S (n)) * bcf_row_scale_scale_bcwv_lower)) /\ exists bcf_quotient_bcwv_lower_decoded_row_scale. bcf_row_scale_code_bcwv_lower = bcf_quotient_bcwv_lower_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcwv_lower) + (bcf_row_scale_bcwv_lower))) /\ (((exists bcf_height_bcwv_lower_decoded_value. bcf_height_bcwv_lower_decoded_value + S (x) = S ((S (k)) * bcf_row_scale_bcwv_lower)) /\ exists bcf_quotient_bcwv_lower_decoded_value. bcf_row_code_bcwv_lower = bcf_quotient_bcwv_lower_decoded_value * S ((S (k)) * bcf_row_scale_bcwv_lower) + (x))))))))) -> (((exists bcf_lt_gap_bcwv_upper_out_of_range. bcf_lt_gap_bcwv_upper_out_of_range + S (S n) = k) /\ y = 0) \/ ((exists bcf_le_gap_bcwv_upper_in_range. bcf_le_gap_bcwv_upper_in_range + (k) = S n) /\ (exists bcf_row_code_code_bcwv_upper bcf_row_code_scale_bcwv_upper bcf_row_scale_code_bcwv_upper bcf_row_scale_scale_bcwv_upper bcf_row_code_bcwv_upper bcf_row_scale_bcwv_upper. ((forall bcf_row_index_bcwv_upper_table. (exists bcf_lt_gap_bcwv_upper_table_row_bound. bcf_lt_gap_bcwv_upper_table_row_bound + S (bcf_row_index_bcwv_upper_table) = S (S n)) -> exists bcf_row_code_bcwv_upper_table bcf_row_scale_bcwv_upper_table. ((((exists bcf_height_bcwv_upper_table_decoded_row_code. bcf_height_bcwv_upper_table_decoded_row_code + S (bcf_row_code_bcwv_upper_table) = S ((S (bcf_row_index_bcwv_upper_table)) * bcf_row_code_scale_bcwv_upper)) /\ exists bcf_quotient_bcwv_upper_table_decoded_row_code. bcf_row_code_code_bcwv_upper = bcf_quotient_bcwv_upper_table_decoded_row_code * S ((S (bcf_row_index_bcwv_upper_table)) * bcf_row_code_scale_bcwv_upper) + (bcf_row_code_bcwv_upper_table))) /\ ((((exists bcf_height_bcwv_upper_table_decoded_row_scale. bcf_height_bcwv_upper_table_decoded_row_scale + S (bcf_row_scale_bcwv_upper_table) = S ((S (bcf_row_index_bcwv_upper_table)) * bcf_row_scale_scale_bcwv_upper)) /\ exists bcf_quotient_bcwv_upper_table_decoded_row_scale. bcf_row_scale_code_bcwv_upper = bcf_quotient_bcwv_upper_table_decoded_row_scale * S ((S (bcf_row_index_bcwv_upper_table)) * bcf_row_scale_scale_bcwv_upper) + (bcf_row_scale_bcwv_upper_table))) /\ ((bcf_row_index_bcwv_upper_table = 0 /\ (forall bcf_index_bcwv_upper_table_zero_row. (exists bcf_lt_gap_bcwv_upper_table_zero_row_bound. bcf_lt_gap_bcwv_upper_table_zero_row_bound + S (bcf_index_bcwv_upper_table_zero_row) = S (S n)) -> exists bcf_value_bcwv_upper_table_zero_row. ((((exists bcf_height_bcwv_upper_table_zero_row_entry. bcf_height_bcwv_upper_table_zero_row_entry + S (bcf_value_bcwv_upper_table_zero_row) = S ((S (bcf_index_bcwv_upper_table_zero_row)) * bcf_row_scale_bcwv_upper_table)) /\ exists bcf_quotient_bcwv_upper_table_zero_row_entry. bcf_row_code_bcwv_upper_table = bcf_quotient_bcwv_upper_table_zero_row_entry * S ((S (bcf_index_bcwv_upper_table_zero_row)) * bcf_row_scale_bcwv_upper_table) + (bcf_value_bcwv_upper_table_zero_row))) /\ ((bcf_index_bcwv_upper_table_zero_row = 0 /\ bcf_value_bcwv_upper_table_zero_row = 1) \/ exists bcf_predecessor_bcwv_upper_table_zero_row. bcf_index_bcwv_upper_table_zero_row = S bcf_predecessor_bcwv_upper_table_zero_row /\ bcf_value_bcwv_upper_table_zero_row = 0)))) \/ exists bcf_predecessor_bcwv_upper_table bcf_previous_code_bcwv_upper_table bcf_previous_scale_bcwv_upper_table. bcf_row_index_bcwv_upper_table = S bcf_predecessor_bcwv_upper_table /\ ((((exists bcf_height_bcwv_upper_table_decoded_previous_code. bcf_height_bcwv_upper_table_decoded_previous_code + S (bcf_previous_code_bcwv_upper_table) = S ((S (bcf_predecessor_bcwv_upper_table)) * bcf_row_code_scale_bcwv_upper)) /\ exists bcf_quotient_bcwv_upper_table_decoded_previous_code. bcf_row_code_code_bcwv_upper = bcf_quotient_bcwv_upper_table_decoded_previous_code * S ((S (bcf_predecessor_bcwv_upper_table)) * bcf_row_code_scale_bcwv_upper) + (bcf_previous_code_bcwv_upper_table))) /\ ((((exists bcf_height_bcwv_upper_table_decoded_previous_scale. bcf_height_bcwv_upper_table_decoded_previous_scale + S (bcf_previous_scale_bcwv_upper_table) = S ((S (bcf_predecessor_bcwv_upper_table)) * bcf_row_scale_scale_bcwv_upper)) /\ exists bcf_quotient_bcwv_upper_table_decoded_previous_scale. bcf_row_scale_code_bcwv_upper = bcf_quotient_bcwv_upper_table_decoded_previous_scale * S ((S (bcf_predecessor_bcwv_upper_table)) * bcf_row_scale_scale_bcwv_upper) + (bcf_previous_scale_bcwv_upper_table))) /\ (forall bcf_index_bcwv_upper_table_row_step. (exists bcf_lt_gap_bcwv_upper_table_row_step_bound. bcf_lt_gap_bcwv_upper_table_row_step_bound + S (bcf_index_bcwv_upper_table_row_step) = S (S n)) -> exists bcf_value_bcwv_upper_table_row_step. ((((exists bcf_height_bcwv_upper_table_row_step_entry. bcf_height_bcwv_upper_table_row_step_entry + S (bcf_value_bcwv_upper_table_row_step) = S ((S (bcf_index_bcwv_upper_table_row_step)) * bcf_row_scale_bcwv_upper_table)) /\ exists bcf_quotient_bcwv_upper_table_row_step_entry. bcf_row_code_bcwv_upper_table = bcf_quotient_bcwv_upper_table_row_step_entry * S ((S (bcf_index_bcwv_upper_table_row_step)) * bcf_row_scale_bcwv_upper_table) + (bcf_value_bcwv_upper_table_row_step))) /\ ((bcf_index_bcwv_upper_table_row_step = 0 /\ bcf_value_bcwv_upper_table_row_step = 1) \/ exists bcf_predecessor_bcwv_upper_table_row_step bcf_left_bcwv_upper_table_row_step bcf_right_bcwv_upper_table_row_step. bcf_index_bcwv_upper_table_row_step = S bcf_predecessor_bcwv_upper_table_row_step /\ ((((exists bcf_height_bcwv_upper_table_row_step_previous_left. bcf_height_bcwv_upper_table_row_step_previous_left + S (bcf_left_bcwv_upper_table_row_step) = S ((S (bcf_predecessor_bcwv_upper_table_row_step)) * bcf_previous_scale_bcwv_upper_table)) /\ exists bcf_quotient_bcwv_upper_table_row_step_previous_left. bcf_previous_code_bcwv_upper_table = bcf_quotient_bcwv_upper_table_row_step_previous_left * S ((S (bcf_predecessor_bcwv_upper_table_row_step)) * bcf_previous_scale_bcwv_upper_table) + (bcf_left_bcwv_upper_table_row_step))) /\ ((((exists bcf_height_bcwv_upper_table_row_step_previous_right. bcf_height_bcwv_upper_table_row_step_previous_right + S (bcf_right_bcwv_upper_table_row_step) = S ((S (S (bcf_predecessor_bcwv_upper_table_row_step))) * bcf_previous_scale_bcwv_upper_table)) /\ exists bcf_quotient_bcwv_upper_table_row_step_previous_right. bcf_previous_code_bcwv_upper_table = bcf_quotient_bcwv_upper_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcwv_upper_table_row_step))) * bcf_previous_scale_bcwv_upper_table) + (bcf_right_bcwv_upper_table_row_step))) /\ bcf_value_bcwv_upper_table_row_step = bcf_left_bcwv_upper_table_row_step + bcf_right_bcwv_upper_table_row_step))))))))))) /\ ((((exists bcf_height_bcwv_upper_decoded_row_code. bcf_height_bcwv_upper_decoded_row_code + S (bcf_row_code_bcwv_upper) = S ((S (S n)) * bcf_row_code_scale_bcwv_upper)) /\ exists bcf_quotient_bcwv_upper_decoded_row_code. bcf_row_code_code_bcwv_upper = bcf_quotient_bcwv_upper_decoded_row_code * S ((S (S n)) * bcf_row_code_scale_bcwv_upper) + (bcf_row_code_bcwv_upper))) /\ ((((exists bcf_height_bcwv_upper_decoded_row_scale. bcf_height_bcwv_upper_decoded_row_scale + S (bcf_row_scale_bcwv_upper) = S ((S (S n)) * bcf_row_scale_scale_bcwv_upper)) /\ exists bcf_quotient_bcwv_upper_decoded_row_scale. bcf_row_scale_code_bcwv_upper = bcf_quotient_bcwv_upper_decoded_row_scale * S ((S (S n)) * bcf_row_scale_scale_bcwv_upper) + (bcf_row_scale_bcwv_upper))) /\ (((exists bcf_height_bcwv_upper_decoded_value. bcf_height_bcwv_upper_decoded_value + S (y) = S ((S (k)) * bcf_row_scale_bcwv_upper)) /\ exists bcf_quotient_bcwv_upper_decoded_value. bcf_row_code_bcwv_upper = bcf_quotient_bcwv_upper_decoded_value * S ((S (k)) * bcf_row_scale_bcwv_upper) + (y))))))))) -> S j * y = S n * xProof neighborhood
Direct theorem prerequisites
BT000Q zero_or_succ BT0000 zero_add BT0001 add_succ_left BT0003 add_assoc BT0005 mul_succ_left BT0007 mul_add BT00T8 choose_exists BT00TE choose_zero BT00TK choose_self_of_eq BT00TJ choose_succ_succDirect theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
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 (10)
01Induction on nL1–1
Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.
- L1
induction n
02Induction on kL2–8
03Establish hjL9–13
04Establish hxL14–18
05Establish hyL19–28
06Calculate and transport equalitiesL29–31
07Use earlier factsL32–32
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L32
exact hx
08Fix variables and assumptionsL33–38
09Use earlier factsL39–40
10Calculate and transport equalitiesL41–41
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L41
rewrite add_succ_left at hsum
11Separate the logical casesL42–42
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L42
exfalso
12Use earlier factsL43–44
13Induction on kL45–51
14Establish hjL52–56
15Establish hxL57–61
16Establish hyL62–71
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose zero.
17Calculate and transport equalitiesL72–74
18Use earlier factsL75–75
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L75
exact hx
19Fix variables and assumptionsL76–81
20Use earlier factsL82–82
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L82
specialize zero_or_succ j
21Separate the logical casesL83–83
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L83
cases zero_or_succ
22Establish ha_existsL84–87
Establish this local claim before using it. It is not an additional assumption.
- L84
have ha_exists : ∃ a. Choose(n,k,a)Definitions: Choose(n,k,a)Original native command in the exact edition - L85
specialize choose_exists n - L86
specialize choose_exists k - L87
exact choose_exists
23Separate the logical casesL88–88
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L88
cases ha_exists
24Establish hb_existsL89–92
Establish this local claim before using it. It is not an additional assumption.
- L89
have hb_exists : ∃ b. Choose(S n,k,b)Definitions: Choose(S n,k,b)Original native command in the exact edition - L90
specialize choose_exists (S n) - L91
specialize choose_exists k - L92
exact choose_exists
25Separate the logical casesL93–93
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L93
cases hb_exists
26Calculate and transport equalitiesL94–95
27Establish hkL96–98
28Establish hprevious_sumL99–102
29Establish ha_oneL103–109
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose self of eq.
30Establish hx_oneL110–116
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose self of eq.
31Establish hweightedL117–125
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
32Establish hy_sumL126–135
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose succ succ.
33Establish hsame_oneL136–140
34Establish hone_scaleL141–150
35Calculate and transport equalitiesL151–151
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L151
symm
36Use earlier factsL152–152
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L152
exact hx_one
37Calculate and transport equalitiesL153–156
38Use earlier factsL157–157
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L157
exact hy_sum
39Calculate and transport equalitiesL158–158
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L158
trans S 0 * x2 + S 0 * x
40Use earlier factsL159–159
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L159
apply mul_add
41Calculate and transport equalitiesL160–161
42Use earlier factsL162–162
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L162
exact hweighted
43Calculate and transport equalitiesL163–167
44Use earlier factsL168–171
45Calculate and transport equalitiesL172–172
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L172
symm
46Use earlier factsL173–173
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L173
exact mul_succ_left
47Separate the logical casesL174–174
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L174
cases zero_or_succ_right
48Establish ha_existsL175–178
Establish this local claim before using it. It is not an additional assumption.
- L175
have ha_exists : ∃ a. Choose(n,k,a)Definitions: Choose(n,k,a)Original native command in the exact edition - L176
specialize choose_exists n - L177
specialize choose_exists k - L178
exact choose_exists
49Separate the logical casesL179–179
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L179
cases ha_exists
50Establish hb_existsL180–183
Establish this local claim before using it. It is not an additional assumption.
- L180
have hb_exists : ∃ b. Choose(n,S k,b)Definitions: Choose(n,S k,b)Original native command in the exact edition - L181
specialize choose_exists n - L182
specialize choose_exists (S k) - L183
exact choose_exists
51Separate the logical casesL184–184
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L184
cases hb_exists
52Establish hc_existsL185–188
Establish this local claim before using it. It is not an additional assumption.
- L185
have hc_exists : ∃ c. Choose(S n,k,c)Definitions: Choose(S n,k,c)Original native command in the exact edition - L186
specialize choose_exists (S n) - L187
specialize choose_exists k - L188
exact choose_exists
53Separate the logical casesL189–189
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L189
cases hc_exists
54Calculate and transport equalitiesL190–190
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L190
rewrite zero_or_succ_right_witness at hsum
55Establish hsecond_complementL191–196
56Establish hfirst_complementL197–203
57Establish hx_sumL204–213
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose succ succ.
58Establish hy_sumL214–223
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose succ succ.
59Establish hfirst_weightL224–232
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
60Establish hsecond_weightL233–242
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
61Calculate and transport equalitiesL243–245
62Use earlier factsL246–246
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L246
exact hy_sum
63Calculate and transport equalitiesL247–247
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L247
trans S (S x1) * x4 + S (S x1) * x
64Use earlier factsL248–248
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L248
apply mul_add
65Calculate and transport equalitiesL249–250
66Use earlier factsL251–254
67Calculate and transport equalitiesL255–258
68Use earlier factsL259–259
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L259
exact hsecond_weight
69Calculate and transport equalitiesL260–261
70Use earlier factsL262–264
71Calculate and transport equalitiesL265–265
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L265
symm
72Use earlier factsL266–266
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L266
apply add_assoc
73Calculate and transport equalitiesL267–268
74Use earlier factsL269–271
75Calculate and transport equalitiesL272–272
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L272
symm
76Use earlier factsL273–273
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L273
apply mul_add
77Calculate and transport equalitiesL274–279
78Use earlier factsL280–280
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L280
exact hx_sum
79Calculate and transport equalitiesL281–281
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L281
refl
80Use earlier factsL282–283
81Calculate and transport equalitiesL284–284
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L284
symm
82Use earlier factsL285–285
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L285
exact mul_succ_left
Original defined command ledger · 285 lines
- 0001
induction n - 0002
induction k - 0003
intro j - 0004
intro x - 0005
intro y - 0006
intro hsum - 0007
intro hlower - 0008
intro hupper - 0009
have hj : j = 0 - 0010
trans 0 + j - 0011
symm - 0012
apply zero_add - 0013
exact hsum - 0014
have hx : x = 1 - 0015
specialize choose_zero 0 - 0016
specialize choose_zero x - 0017
apply choose_zero - 0018
exact hlower - 0019
have hy : y = 1 - 0020
specialize choose_zero (S 0) - 0021
specialize choose_zero y - 0022
apply choose_zero - 0023
exact hupper - 0024
rewrite hj - 0025
trans S 0 * 1 - 0026
congr - 0027
refl - 0028
exact hy - 0029
congr - 0030
refl - 0031
symm - 0032
exact hx - 0033
intro j - 0034
intro x - 0035
intro y - 0036
intro hsum - 0037
intro hlower - 0038
intro hupper - 0039
specialize add_succ_left k - 0040
specialize add_succ_left j - 0041
rewrite add_succ_left at hsum - 0042
exfalso - 0043
apply PA1 - 0044
exact hsum - 0045
induction k - 0046
intro j - 0047
intro x - 0048
intro y - 0049
intro hsum - 0050
intro hlower - 0051
intro hupper - 0052
have hj : j = S n - 0053
trans 0 + j - 0054
symm - 0055
apply zero_add - 0056
exact hsum - 0057
have hx : x = 1 - 0058
specialize choose_zero (S n) - 0059
specialize choose_zero x - 0060
apply choose_zero - 0061
exact hlower - 0062
have hy : y = 1 - 0063
specialize choose_zero (S (S n)) - 0064
specialize choose_zero y - 0065
apply choose_zero - 0066
exact hupper - 0067
rewrite hj - 0068
trans S (S n) * 1 - 0069
congr - 0070
refl - 0071
exact hy - 0072
congr - 0073
refl - 0074
symm - 0075
exact hx - 0076
intro j - 0077
intro x - 0078
intro y - 0079
intro hsum - 0080
intro hlower - 0081
intro hupper - 0082
specialize zero_or_succ j - 0083
cases zero_or_succ - 0084
have ha_exists : ∃ a. Choose(n,k,a)Exact native replay line
have ha_exists : exists a. (((exists bcf_lt_gap_bcwv_previous_left_out_of_range. bcf_lt_gap_bcwv_previous_left_out_of_range + S (n) = k) /\ a = 0) \/ ((exists bcf_le_gap_bcwv_previous_left_in_range. bcf_le_gap_bcwv_previous_left_in_range + (k) = n) /\ (exists bcf_row_code_code_bcwv_previous_left bcf_row_code_scale_bcwv_previous_left bcf_row_scale_code_bcwv_previous_left bcf_row_scale_scale_bcwv_previous_left bcf_row_code_bcwv_previous_left bcf_row_scale_bcwv_previous_left. ((forall bcf_row_index_bcwv_previous_left_table. (exists bcf_lt_gap_bcwv_previous_left_table_row_bound. bcf_lt_gap_bcwv_previous_left_table_row_bound + S (bcf_row_index_bcwv_previous_left_table) = S (n)) -> exists bcf_row_code_bcwv_previous_left_table bcf_row_scale_bcwv_previous_left_table. ((((exists bcf_height_bcwv_previous_left_table_decoded_row_code. bcf_height_bcwv_previous_left_table_decoded_row_code + S (bcf_row_code_bcwv_previous_left_table) = S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_row_code. bcf_row_code_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_row_code * S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left) + (bcf_row_code_bcwv_previous_left_table))) /\ ((((exists bcf_height_bcwv_previous_left_table_decoded_row_scale. bcf_height_bcwv_previous_left_table_decoded_row_scale + S (bcf_row_scale_bcwv_previous_left_table) = S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_row_scale. bcf_row_scale_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_row_scale * S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left) + (bcf_row_scale_bcwv_previous_left_table))) /\ ((bcf_row_index_bcwv_previous_left_table = 0 /\ (forall bcf_index_bcwv_previous_left_table_zero_row. (exists bcf_lt_gap_bcwv_previous_left_table_zero_row_bound. bcf_lt_gap_bcwv_previous_left_table_zero_row_bound + S (bcf_index_bcwv_previous_left_table_zero_row) = S (n)) -> exists bcf_value_bcwv_previous_left_table_zero_row. ((((exists bcf_height_bcwv_previous_left_table_zero_row_entry. bcf_height_bcwv_previous_left_table_zero_row_entry + S (bcf_value_bcwv_previous_left_table_zero_row) = S ((S (bcf_index_bcwv_previous_left_table_zero_row)) * bcf_row_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_zero_row_entry. bcf_row_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_zero_row_entry * S ((S (bcf_index_bcwv_previous_left_table_zero_row)) * bcf_row_scale_bcwv_previous_left_table) + (bcf_value_bcwv_previous_left_table_zero_row))) /\ ((bcf_index_bcwv_previous_left_table_zero_row = 0 /\ bcf_value_bcwv_previous_left_table_zero_row = 1) \/ exists bcf_predecessor_bcwv_previous_left_table_zero_row. bcf_index_bcwv_previous_left_table_zero_row = S bcf_predecessor_bcwv_previous_left_table_zero_row /\ bcf_value_bcwv_previous_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcwv_previous_left_table bcf_previous_code_bcwv_previous_left_table bcf_previous_scale_bcwv_previous_left_table. bcf_row_index_bcwv_previous_left_table = S bcf_predecessor_bcwv_previous_left_table /\ ((((exists bcf_height_bcwv_previous_left_table_decoded_previous_code. bcf_height_bcwv_previous_left_table_decoded_previous_code + S (bcf_previous_code_bcwv_previous_left_table) = S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_previous_code. bcf_row_code_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left) + (bcf_previous_code_bcwv_previous_left_table))) /\ ((((exists bcf_height_bcwv_previous_left_table_decoded_previous_scale. bcf_height_bcwv_previous_left_table_decoded_previous_scale + S (bcf_previous_scale_bcwv_previous_left_table) = S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_previous_scale. bcf_row_scale_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left) + (bcf_previous_scale_bcwv_previous_left_table))) /\ (forall bcf_index_bcwv_previous_left_table_row_step. (exists bcf_lt_gap_bcwv_previous_left_table_row_step_bound. bcf_lt_gap_bcwv_previous_left_table_row_step_bound + S (bcf_index_bcwv_previous_left_table_row_step) = S (n)) -> exists bcf_value_bcwv_previous_left_table_row_step. ((((exists bcf_height_bcwv_previous_left_table_row_step_entry. bcf_height_bcwv_previous_left_table_row_step_entry + S (bcf_value_bcwv_previous_left_table_row_step) = S ((S (bcf_index_bcwv_previous_left_table_row_step)) * bcf_row_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_row_step_entry. bcf_row_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_row_step_entry * S ((S (bcf_index_bcwv_previous_left_table_row_step)) * bcf_row_scale_bcwv_previous_left_table) + (bcf_value_bcwv_previous_left_table_row_step))) /\ ((bcf_index_bcwv_previous_left_table_row_step = 0 /\ bcf_value_bcwv_previous_left_table_row_step = 1) \/ exists bcf_predecessor_bcwv_previous_left_table_row_step bcf_left_bcwv_previous_left_table_row_step bcf_right_bcwv_previous_left_table_row_step. bcf_index_bcwv_previous_left_table_row_step = S bcf_predecessor_bcwv_previous_left_table_row_step /\ ((((exists bcf_height_bcwv_previous_left_table_row_step_previous_left. bcf_height_bcwv_previous_left_table_row_step_previous_left + S (bcf_left_bcwv_previous_left_table_row_step) = S ((S (bcf_predecessor_bcwv_previous_left_table_row_step)) * bcf_previous_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_row_step_previous_left. bcf_previous_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcwv_previous_left_table_row_step)) * bcf_previous_scale_bcwv_previous_left_table) + (bcf_left_bcwv_previous_left_table_row_step))) /\ ((((exists bcf_height_bcwv_previous_left_table_row_step_previous_right. bcf_height_bcwv_previous_left_table_row_step_previous_right + S (bcf_right_bcwv_previous_left_table_row_step) = S ((S (S (bcf_predecessor_bcwv_previous_left_table_row_step))) * bcf_previous_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_row_step_previous_right. bcf_previous_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcwv_previous_left_table_row_step))) * bcf_previous_scale_bcwv_previous_left_table) + (bcf_right_bcwv_previous_left_table_row_step))) /\ bcf_value_bcwv_previous_left_table_row_step = bcf_left_bcwv_previous_left_table_row_step + bcf_right_bcwv_previous_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcwv_previous_left_decoded_row_code. bcf_height_bcwv_previous_left_decoded_row_code + S (bcf_row_code_bcwv_previous_left) = S ((S (n)) * bcf_row_code_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_decoded_row_code. bcf_row_code_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcwv_previous_left) + (bcf_row_code_bcwv_previous_left))) /\ ((((exists bcf_height_bcwv_previous_left_decoded_row_scale. bcf_height_bcwv_previous_left_decoded_row_scale + S (bcf_row_scale_bcwv_previous_left) = S ((S (n)) * bcf_row_scale_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_decoded_row_scale. bcf_row_scale_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcwv_previous_left) + (bcf_row_scale_bcwv_previous_left))) /\ (((exists bcf_height_bcwv_previous_left_decoded_value. bcf_height_bcwv_previous_left_decoded_value + S (a) = S ((S (k)) * bcf_row_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_decoded_value. bcf_row_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_decoded_value * S ((S (k)) * bcf_row_scale_bcwv_previous_left) + (a))))))))) - 0085
specialize choose_exists n - 0086
specialize choose_exists k - 0087
exact choose_exists - 0088
cases ha_exists - 0089
have hb_exists : ∃ b. Choose(S n,k,b)Exact native replay line
have hb_exists : exists b. (((exists bcf_lt_gap_bcwv_successor_left_out_of_range. bcf_lt_gap_bcwv_successor_left_out_of_range + S (S n) = k) /\ b = 0) \/ ((exists bcf_le_gap_bcwv_successor_left_in_range. bcf_le_gap_bcwv_successor_left_in_range + (k) = S n) /\ (exists bcf_row_code_code_bcwv_successor_left bcf_row_code_scale_bcwv_successor_left bcf_row_scale_code_bcwv_successor_left bcf_row_scale_scale_bcwv_successor_left bcf_row_code_bcwv_successor_left bcf_row_scale_bcwv_successor_left. ((forall bcf_row_index_bcwv_successor_left_table. (exists bcf_lt_gap_bcwv_successor_left_table_row_bound. bcf_lt_gap_bcwv_successor_left_table_row_bound + S (bcf_row_index_bcwv_successor_left_table) = S (S n)) -> exists bcf_row_code_bcwv_successor_left_table bcf_row_scale_bcwv_successor_left_table. ((((exists bcf_height_bcwv_successor_left_table_decoded_row_code. bcf_height_bcwv_successor_left_table_decoded_row_code + S (bcf_row_code_bcwv_successor_left_table) = S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_row_code. bcf_row_code_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_row_code * S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left) + (bcf_row_code_bcwv_successor_left_table))) /\ ((((exists bcf_height_bcwv_successor_left_table_decoded_row_scale. bcf_height_bcwv_successor_left_table_decoded_row_scale + S (bcf_row_scale_bcwv_successor_left_table) = S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_row_scale. bcf_row_scale_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_row_scale * S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left) + (bcf_row_scale_bcwv_successor_left_table))) /\ ((bcf_row_index_bcwv_successor_left_table = 0 /\ (forall bcf_index_bcwv_successor_left_table_zero_row. (exists bcf_lt_gap_bcwv_successor_left_table_zero_row_bound. bcf_lt_gap_bcwv_successor_left_table_zero_row_bound + S (bcf_index_bcwv_successor_left_table_zero_row) = S (S n)) -> exists bcf_value_bcwv_successor_left_table_zero_row. ((((exists bcf_height_bcwv_successor_left_table_zero_row_entry. bcf_height_bcwv_successor_left_table_zero_row_entry + S (bcf_value_bcwv_successor_left_table_zero_row) = S ((S (bcf_index_bcwv_successor_left_table_zero_row)) * bcf_row_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_zero_row_entry. bcf_row_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_zero_row_entry * S ((S (bcf_index_bcwv_successor_left_table_zero_row)) * bcf_row_scale_bcwv_successor_left_table) + (bcf_value_bcwv_successor_left_table_zero_row))) /\ ((bcf_index_bcwv_successor_left_table_zero_row = 0 /\ bcf_value_bcwv_successor_left_table_zero_row = 1) \/ exists bcf_predecessor_bcwv_successor_left_table_zero_row. bcf_index_bcwv_successor_left_table_zero_row = S bcf_predecessor_bcwv_successor_left_table_zero_row /\ bcf_value_bcwv_successor_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcwv_successor_left_table bcf_previous_code_bcwv_successor_left_table bcf_previous_scale_bcwv_successor_left_table. bcf_row_index_bcwv_successor_left_table = S bcf_predecessor_bcwv_successor_left_table /\ ((((exists bcf_height_bcwv_successor_left_table_decoded_previous_code. bcf_height_bcwv_successor_left_table_decoded_previous_code + S (bcf_previous_code_bcwv_successor_left_table) = S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_previous_code. bcf_row_code_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left) + (bcf_previous_code_bcwv_successor_left_table))) /\ ((((exists bcf_height_bcwv_successor_left_table_decoded_previous_scale. bcf_height_bcwv_successor_left_table_decoded_previous_scale + S (bcf_previous_scale_bcwv_successor_left_table) = S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_previous_scale. bcf_row_scale_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left) + (bcf_previous_scale_bcwv_successor_left_table))) /\ (forall bcf_index_bcwv_successor_left_table_row_step. (exists bcf_lt_gap_bcwv_successor_left_table_row_step_bound. bcf_lt_gap_bcwv_successor_left_table_row_step_bound + S (bcf_index_bcwv_successor_left_table_row_step) = S (S n)) -> exists bcf_value_bcwv_successor_left_table_row_step. ((((exists bcf_height_bcwv_successor_left_table_row_step_entry. bcf_height_bcwv_successor_left_table_row_step_entry + S (bcf_value_bcwv_successor_left_table_row_step) = S ((S (bcf_index_bcwv_successor_left_table_row_step)) * bcf_row_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_row_step_entry. bcf_row_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_row_step_entry * S ((S (bcf_index_bcwv_successor_left_table_row_step)) * bcf_row_scale_bcwv_successor_left_table) + (bcf_value_bcwv_successor_left_table_row_step))) /\ ((bcf_index_bcwv_successor_left_table_row_step = 0 /\ bcf_value_bcwv_successor_left_table_row_step = 1) \/ exists bcf_predecessor_bcwv_successor_left_table_row_step bcf_left_bcwv_successor_left_table_row_step bcf_right_bcwv_successor_left_table_row_step. bcf_index_bcwv_successor_left_table_row_step = S bcf_predecessor_bcwv_successor_left_table_row_step /\ ((((exists bcf_height_bcwv_successor_left_table_row_step_previous_left. bcf_height_bcwv_successor_left_table_row_step_previous_left + S (bcf_left_bcwv_successor_left_table_row_step) = S ((S (bcf_predecessor_bcwv_successor_left_table_row_step)) * bcf_previous_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_row_step_previous_left. bcf_previous_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcwv_successor_left_table_row_step)) * bcf_previous_scale_bcwv_successor_left_table) + (bcf_left_bcwv_successor_left_table_row_step))) /\ ((((exists bcf_height_bcwv_successor_left_table_row_step_previous_right. bcf_height_bcwv_successor_left_table_row_step_previous_right + S (bcf_right_bcwv_successor_left_table_row_step) = S ((S (S (bcf_predecessor_bcwv_successor_left_table_row_step))) * bcf_previous_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_row_step_previous_right. bcf_previous_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcwv_successor_left_table_row_step))) * bcf_previous_scale_bcwv_successor_left_table) + (bcf_right_bcwv_successor_left_table_row_step))) /\ bcf_value_bcwv_successor_left_table_row_step = bcf_left_bcwv_successor_left_table_row_step + bcf_right_bcwv_successor_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcwv_successor_left_decoded_row_code. bcf_height_bcwv_successor_left_decoded_row_code + S (bcf_row_code_bcwv_successor_left) = S ((S (S n)) * bcf_row_code_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_decoded_row_code. bcf_row_code_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_decoded_row_code * S ((S (S n)) * bcf_row_code_scale_bcwv_successor_left) + (bcf_row_code_bcwv_successor_left))) /\ ((((exists bcf_height_bcwv_successor_left_decoded_row_scale. bcf_height_bcwv_successor_left_decoded_row_scale + S (bcf_row_scale_bcwv_successor_left) = S ((S (S n)) * bcf_row_scale_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_decoded_row_scale. bcf_row_scale_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_decoded_row_scale * S ((S (S n)) * bcf_row_scale_scale_bcwv_successor_left) + (bcf_row_scale_bcwv_successor_left))) /\ (((exists bcf_height_bcwv_successor_left_decoded_value. bcf_height_bcwv_successor_left_decoded_value + S (b) = S ((S (k)) * bcf_row_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_decoded_value. bcf_row_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_decoded_value * S ((S (k)) * bcf_row_scale_bcwv_successor_left) + (b))))))))) - 0090
specialize choose_exists (S n) - 0091
specialize choose_exists k - 0092
exact choose_exists - 0093
cases hb_exists - 0094
rewrite zero_or_succ_left at hsum - 0095
rewrite PA3 at hsum - 0096
have hk : k = n - 0097
apply PA2 - 0098
exact hsum - 0099
have hprevious_sum : k + 0 = n - 0100
trans k - 0101
apply PA3 - 0102
exact hk - 0103
have ha_one : x1 = 1 - 0104
specialize choose_self_of_eq n - 0105
specialize choose_self_of_eq k - 0106
specialize choose_self_of_eq x1 - 0107
apply choose_self_of_eq - 0108
exact hk - 0109
exact ha_exists_witness - 0110
have hx_one : x = 1 - 0111
specialize choose_self_of_eq (S n) - 0112
specialize choose_self_of_eq (S k) - 0113
specialize choose_self_of_eq x - 0114
apply choose_self_of_eq - 0115
exact hsum - 0116
exact hlower - 0117
have hweighted : S 0 * x2 = S n * x1 - 0118
specialize IH k - 0119
specialize IH 0 - 0120
specialize IH x1 - 0121
specialize IH x2 - 0122
apply IH - 0123
exact hprevious_sum - 0124
exact ha_exists_witness - 0125
exact hb_exists_witness - 0126
have hy_sum : y = x2 + x - 0127
specialize choose_succ_succ (S n) - 0128
specialize choose_succ_succ k - 0129
specialize choose_succ_succ x2 - 0130
specialize choose_succ_succ x - 0131
specialize choose_succ_succ y - 0132
apply choose_succ_succ - 0133
exact hb_exists_witness - 0134
exact hlower - 0135
exact hupper - 0136
have hsame_one : x1 = x - 0137
trans 1 - 0138
exact ha_one - 0139
symm - 0140
exact hx_one - 0141
have hone_scale : S 0 * x = x - 0142
trans S 0 * 1 - 0143
congr - 0144
refl - 0145
exact hx_one - 0146
trans 1 - 0147
trans S 0 * 0 + S 0 - 0148
apply PA6 - 0149
rewrite PA5 - 0150
apply zero_add - 0151
symm - 0152
exact hx_one - 0153
rewrite zero_or_succ_left - 0154
trans S 0 * (x2 + x) - 0155
congr - 0156
refl - 0157
exact hy_sum - 0158
trans S 0 * x2 + S 0 * x - 0159
apply mul_add - 0160
trans S n * x1 + S 0 * x - 0161
congr - 0162
exact hweighted - 0163
refl - 0164
trans S n * x + x - 0165
congr - 0166
congr - 0167
refl - 0168
exact hsame_one - 0169
exact hone_scale - 0170
specialize mul_succ_left (S n) - 0171
specialize mul_succ_left x - 0172
symm - 0173
exact mul_succ_left - 0174
cases zero_or_succ_right - 0175
have ha_exists : ∃ a. Choose(n,k,a)Exact native replay line
have ha_exists : exists a. (((exists bcf_lt_gap_bcwv_previous_left_out_of_range. bcf_lt_gap_bcwv_previous_left_out_of_range + S (n) = k) /\ a = 0) \/ ((exists bcf_le_gap_bcwv_previous_left_in_range. bcf_le_gap_bcwv_previous_left_in_range + (k) = n) /\ (exists bcf_row_code_code_bcwv_previous_left bcf_row_code_scale_bcwv_previous_left bcf_row_scale_code_bcwv_previous_left bcf_row_scale_scale_bcwv_previous_left bcf_row_code_bcwv_previous_left bcf_row_scale_bcwv_previous_left. ((forall bcf_row_index_bcwv_previous_left_table. (exists bcf_lt_gap_bcwv_previous_left_table_row_bound. bcf_lt_gap_bcwv_previous_left_table_row_bound + S (bcf_row_index_bcwv_previous_left_table) = S (n)) -> exists bcf_row_code_bcwv_previous_left_table bcf_row_scale_bcwv_previous_left_table. ((((exists bcf_height_bcwv_previous_left_table_decoded_row_code. bcf_height_bcwv_previous_left_table_decoded_row_code + S (bcf_row_code_bcwv_previous_left_table) = S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_row_code. bcf_row_code_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_row_code * S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left) + (bcf_row_code_bcwv_previous_left_table))) /\ ((((exists bcf_height_bcwv_previous_left_table_decoded_row_scale. bcf_height_bcwv_previous_left_table_decoded_row_scale + S (bcf_row_scale_bcwv_previous_left_table) = S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_row_scale. bcf_row_scale_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_row_scale * S ((S (bcf_row_index_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left) + (bcf_row_scale_bcwv_previous_left_table))) /\ ((bcf_row_index_bcwv_previous_left_table = 0 /\ (forall bcf_index_bcwv_previous_left_table_zero_row. (exists bcf_lt_gap_bcwv_previous_left_table_zero_row_bound. bcf_lt_gap_bcwv_previous_left_table_zero_row_bound + S (bcf_index_bcwv_previous_left_table_zero_row) = S (n)) -> exists bcf_value_bcwv_previous_left_table_zero_row. ((((exists bcf_height_bcwv_previous_left_table_zero_row_entry. bcf_height_bcwv_previous_left_table_zero_row_entry + S (bcf_value_bcwv_previous_left_table_zero_row) = S ((S (bcf_index_bcwv_previous_left_table_zero_row)) * bcf_row_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_zero_row_entry. bcf_row_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_zero_row_entry * S ((S (bcf_index_bcwv_previous_left_table_zero_row)) * bcf_row_scale_bcwv_previous_left_table) + (bcf_value_bcwv_previous_left_table_zero_row))) /\ ((bcf_index_bcwv_previous_left_table_zero_row = 0 /\ bcf_value_bcwv_previous_left_table_zero_row = 1) \/ exists bcf_predecessor_bcwv_previous_left_table_zero_row. bcf_index_bcwv_previous_left_table_zero_row = S bcf_predecessor_bcwv_previous_left_table_zero_row /\ bcf_value_bcwv_previous_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcwv_previous_left_table bcf_previous_code_bcwv_previous_left_table bcf_previous_scale_bcwv_previous_left_table. bcf_row_index_bcwv_previous_left_table = S bcf_predecessor_bcwv_previous_left_table /\ ((((exists bcf_height_bcwv_previous_left_table_decoded_previous_code. bcf_height_bcwv_previous_left_table_decoded_previous_code + S (bcf_previous_code_bcwv_previous_left_table) = S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_previous_code. bcf_row_code_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_code_scale_bcwv_previous_left) + (bcf_previous_code_bcwv_previous_left_table))) /\ ((((exists bcf_height_bcwv_previous_left_table_decoded_previous_scale. bcf_height_bcwv_previous_left_table_decoded_previous_scale + S (bcf_previous_scale_bcwv_previous_left_table) = S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_table_decoded_previous_scale. bcf_row_scale_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcwv_previous_left_table)) * bcf_row_scale_scale_bcwv_previous_left) + (bcf_previous_scale_bcwv_previous_left_table))) /\ (forall bcf_index_bcwv_previous_left_table_row_step. (exists bcf_lt_gap_bcwv_previous_left_table_row_step_bound. bcf_lt_gap_bcwv_previous_left_table_row_step_bound + S (bcf_index_bcwv_previous_left_table_row_step) = S (n)) -> exists bcf_value_bcwv_previous_left_table_row_step. ((((exists bcf_height_bcwv_previous_left_table_row_step_entry. bcf_height_bcwv_previous_left_table_row_step_entry + S (bcf_value_bcwv_previous_left_table_row_step) = S ((S (bcf_index_bcwv_previous_left_table_row_step)) * bcf_row_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_row_step_entry. bcf_row_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_row_step_entry * S ((S (bcf_index_bcwv_previous_left_table_row_step)) * bcf_row_scale_bcwv_previous_left_table) + (bcf_value_bcwv_previous_left_table_row_step))) /\ ((bcf_index_bcwv_previous_left_table_row_step = 0 /\ bcf_value_bcwv_previous_left_table_row_step = 1) \/ exists bcf_predecessor_bcwv_previous_left_table_row_step bcf_left_bcwv_previous_left_table_row_step bcf_right_bcwv_previous_left_table_row_step. bcf_index_bcwv_previous_left_table_row_step = S bcf_predecessor_bcwv_previous_left_table_row_step /\ ((((exists bcf_height_bcwv_previous_left_table_row_step_previous_left. bcf_height_bcwv_previous_left_table_row_step_previous_left + S (bcf_left_bcwv_previous_left_table_row_step) = S ((S (bcf_predecessor_bcwv_previous_left_table_row_step)) * bcf_previous_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_row_step_previous_left. bcf_previous_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcwv_previous_left_table_row_step)) * bcf_previous_scale_bcwv_previous_left_table) + (bcf_left_bcwv_previous_left_table_row_step))) /\ ((((exists bcf_height_bcwv_previous_left_table_row_step_previous_right. bcf_height_bcwv_previous_left_table_row_step_previous_right + S (bcf_right_bcwv_previous_left_table_row_step) = S ((S (S (bcf_predecessor_bcwv_previous_left_table_row_step))) * bcf_previous_scale_bcwv_previous_left_table)) /\ exists bcf_quotient_bcwv_previous_left_table_row_step_previous_right. bcf_previous_code_bcwv_previous_left_table = bcf_quotient_bcwv_previous_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcwv_previous_left_table_row_step))) * bcf_previous_scale_bcwv_previous_left_table) + (bcf_right_bcwv_previous_left_table_row_step))) /\ bcf_value_bcwv_previous_left_table_row_step = bcf_left_bcwv_previous_left_table_row_step + bcf_right_bcwv_previous_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcwv_previous_left_decoded_row_code. bcf_height_bcwv_previous_left_decoded_row_code + S (bcf_row_code_bcwv_previous_left) = S ((S (n)) * bcf_row_code_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_decoded_row_code. bcf_row_code_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcwv_previous_left) + (bcf_row_code_bcwv_previous_left))) /\ ((((exists bcf_height_bcwv_previous_left_decoded_row_scale. bcf_height_bcwv_previous_left_decoded_row_scale + S (bcf_row_scale_bcwv_previous_left) = S ((S (n)) * bcf_row_scale_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_decoded_row_scale. bcf_row_scale_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcwv_previous_left) + (bcf_row_scale_bcwv_previous_left))) /\ (((exists bcf_height_bcwv_previous_left_decoded_value. bcf_height_bcwv_previous_left_decoded_value + S (a) = S ((S (k)) * bcf_row_scale_bcwv_previous_left)) /\ exists bcf_quotient_bcwv_previous_left_decoded_value. bcf_row_code_bcwv_previous_left = bcf_quotient_bcwv_previous_left_decoded_value * S ((S (k)) * bcf_row_scale_bcwv_previous_left) + (a))))))))) - 0176
specialize choose_exists n - 0177
specialize choose_exists k - 0178
exact choose_exists - 0179
cases ha_exists - 0180
have hb_exists : ∃ b. Choose(n,S k,b)Exact native replay line
have hb_exists : exists b. (((exists bcf_lt_gap_bcwv_previous_right_out_of_range. bcf_lt_gap_bcwv_previous_right_out_of_range + S (n) = S k) /\ b = 0) \/ ((exists bcf_le_gap_bcwv_previous_right_in_range. bcf_le_gap_bcwv_previous_right_in_range + (S k) = n) /\ (exists bcf_row_code_code_bcwv_previous_right bcf_row_code_scale_bcwv_previous_right bcf_row_scale_code_bcwv_previous_right bcf_row_scale_scale_bcwv_previous_right bcf_row_code_bcwv_previous_right bcf_row_scale_bcwv_previous_right. ((forall bcf_row_index_bcwv_previous_right_table. (exists bcf_lt_gap_bcwv_previous_right_table_row_bound. bcf_lt_gap_bcwv_previous_right_table_row_bound + S (bcf_row_index_bcwv_previous_right_table) = S (n)) -> exists bcf_row_code_bcwv_previous_right_table bcf_row_scale_bcwv_previous_right_table. ((((exists bcf_height_bcwv_previous_right_table_decoded_row_code. bcf_height_bcwv_previous_right_table_decoded_row_code + S (bcf_row_code_bcwv_previous_right_table) = S ((S (bcf_row_index_bcwv_previous_right_table)) * bcf_row_code_scale_bcwv_previous_right)) /\ exists bcf_quotient_bcwv_previous_right_table_decoded_row_code. bcf_row_code_code_bcwv_previous_right = bcf_quotient_bcwv_previous_right_table_decoded_row_code * S ((S (bcf_row_index_bcwv_previous_right_table)) * bcf_row_code_scale_bcwv_previous_right) + (bcf_row_code_bcwv_previous_right_table))) /\ ((((exists bcf_height_bcwv_previous_right_table_decoded_row_scale. bcf_height_bcwv_previous_right_table_decoded_row_scale + S (bcf_row_scale_bcwv_previous_right_table) = S ((S (bcf_row_index_bcwv_previous_right_table)) * bcf_row_scale_scale_bcwv_previous_right)) /\ exists bcf_quotient_bcwv_previous_right_table_decoded_row_scale. bcf_row_scale_code_bcwv_previous_right = bcf_quotient_bcwv_previous_right_table_decoded_row_scale * S ((S (bcf_row_index_bcwv_previous_right_table)) * bcf_row_scale_scale_bcwv_previous_right) + (bcf_row_scale_bcwv_previous_right_table))) /\ ((bcf_row_index_bcwv_previous_right_table = 0 /\ (forall bcf_index_bcwv_previous_right_table_zero_row. (exists bcf_lt_gap_bcwv_previous_right_table_zero_row_bound. bcf_lt_gap_bcwv_previous_right_table_zero_row_bound + S (bcf_index_bcwv_previous_right_table_zero_row) = S (n)) -> exists bcf_value_bcwv_previous_right_table_zero_row. ((((exists bcf_height_bcwv_previous_right_table_zero_row_entry. bcf_height_bcwv_previous_right_table_zero_row_entry + S (bcf_value_bcwv_previous_right_table_zero_row) = S ((S (bcf_index_bcwv_previous_right_table_zero_row)) * bcf_row_scale_bcwv_previous_right_table)) /\ exists bcf_quotient_bcwv_previous_right_table_zero_row_entry. bcf_row_code_bcwv_previous_right_table = bcf_quotient_bcwv_previous_right_table_zero_row_entry * S ((S (bcf_index_bcwv_previous_right_table_zero_row)) * bcf_row_scale_bcwv_previous_right_table) + (bcf_value_bcwv_previous_right_table_zero_row))) /\ ((bcf_index_bcwv_previous_right_table_zero_row = 0 /\ bcf_value_bcwv_previous_right_table_zero_row = 1) \/ exists bcf_predecessor_bcwv_previous_right_table_zero_row. bcf_index_bcwv_previous_right_table_zero_row = S bcf_predecessor_bcwv_previous_right_table_zero_row /\ bcf_value_bcwv_previous_right_table_zero_row = 0)))) \/ exists bcf_predecessor_bcwv_previous_right_table bcf_previous_code_bcwv_previous_right_table bcf_previous_scale_bcwv_previous_right_table. bcf_row_index_bcwv_previous_right_table = S bcf_predecessor_bcwv_previous_right_table /\ ((((exists bcf_height_bcwv_previous_right_table_decoded_previous_code. bcf_height_bcwv_previous_right_table_decoded_previous_code + S (bcf_previous_code_bcwv_previous_right_table) = S ((S (bcf_predecessor_bcwv_previous_right_table)) * bcf_row_code_scale_bcwv_previous_right)) /\ exists bcf_quotient_bcwv_previous_right_table_decoded_previous_code. bcf_row_code_code_bcwv_previous_right = bcf_quotient_bcwv_previous_right_table_decoded_previous_code * S ((S (bcf_predecessor_bcwv_previous_right_table)) * bcf_row_code_scale_bcwv_previous_right) + (bcf_previous_code_bcwv_previous_right_table))) /\ ((((exists bcf_height_bcwv_previous_right_table_decoded_previous_scale. bcf_height_bcwv_previous_right_table_decoded_previous_scale + S (bcf_previous_scale_bcwv_previous_right_table) = S ((S (bcf_predecessor_bcwv_previous_right_table)) * bcf_row_scale_scale_bcwv_previous_right)) /\ exists bcf_quotient_bcwv_previous_right_table_decoded_previous_scale. bcf_row_scale_code_bcwv_previous_right = bcf_quotient_bcwv_previous_right_table_decoded_previous_scale * S ((S (bcf_predecessor_bcwv_previous_right_table)) * bcf_row_scale_scale_bcwv_previous_right) + (bcf_previous_scale_bcwv_previous_right_table))) /\ (forall bcf_index_bcwv_previous_right_table_row_step. (exists bcf_lt_gap_bcwv_previous_right_table_row_step_bound. bcf_lt_gap_bcwv_previous_right_table_row_step_bound + S (bcf_index_bcwv_previous_right_table_row_step) = S (n)) -> exists bcf_value_bcwv_previous_right_table_row_step. ((((exists bcf_height_bcwv_previous_right_table_row_step_entry. bcf_height_bcwv_previous_right_table_row_step_entry + S (bcf_value_bcwv_previous_right_table_row_step) = S ((S (bcf_index_bcwv_previous_right_table_row_step)) * bcf_row_scale_bcwv_previous_right_table)) /\ exists bcf_quotient_bcwv_previous_right_table_row_step_entry. bcf_row_code_bcwv_previous_right_table = bcf_quotient_bcwv_previous_right_table_row_step_entry * S ((S (bcf_index_bcwv_previous_right_table_row_step)) * bcf_row_scale_bcwv_previous_right_table) + (bcf_value_bcwv_previous_right_table_row_step))) /\ ((bcf_index_bcwv_previous_right_table_row_step = 0 /\ bcf_value_bcwv_previous_right_table_row_step = 1) \/ exists bcf_predecessor_bcwv_previous_right_table_row_step bcf_left_bcwv_previous_right_table_row_step bcf_right_bcwv_previous_right_table_row_step. bcf_index_bcwv_previous_right_table_row_step = S bcf_predecessor_bcwv_previous_right_table_row_step /\ ((((exists bcf_height_bcwv_previous_right_table_row_step_previous_left. bcf_height_bcwv_previous_right_table_row_step_previous_left + S (bcf_left_bcwv_previous_right_table_row_step) = S ((S (bcf_predecessor_bcwv_previous_right_table_row_step)) * bcf_previous_scale_bcwv_previous_right_table)) /\ exists bcf_quotient_bcwv_previous_right_table_row_step_previous_left. bcf_previous_code_bcwv_previous_right_table = bcf_quotient_bcwv_previous_right_table_row_step_previous_left * S ((S (bcf_predecessor_bcwv_previous_right_table_row_step)) * bcf_previous_scale_bcwv_previous_right_table) + (bcf_left_bcwv_previous_right_table_row_step))) /\ ((((exists bcf_height_bcwv_previous_right_table_row_step_previous_right. bcf_height_bcwv_previous_right_table_row_step_previous_right + S (bcf_right_bcwv_previous_right_table_row_step) = S ((S (S (bcf_predecessor_bcwv_previous_right_table_row_step))) * bcf_previous_scale_bcwv_previous_right_table)) /\ exists bcf_quotient_bcwv_previous_right_table_row_step_previous_right. bcf_previous_code_bcwv_previous_right_table = bcf_quotient_bcwv_previous_right_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcwv_previous_right_table_row_step))) * bcf_previous_scale_bcwv_previous_right_table) + (bcf_right_bcwv_previous_right_table_row_step))) /\ bcf_value_bcwv_previous_right_table_row_step = bcf_left_bcwv_previous_right_table_row_step + bcf_right_bcwv_previous_right_table_row_step))))))))))) /\ ((((exists bcf_height_bcwv_previous_right_decoded_row_code. bcf_height_bcwv_previous_right_decoded_row_code + S (bcf_row_code_bcwv_previous_right) = S ((S (n)) * bcf_row_code_scale_bcwv_previous_right)) /\ exists bcf_quotient_bcwv_previous_right_decoded_row_code. bcf_row_code_code_bcwv_previous_right = bcf_quotient_bcwv_previous_right_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcwv_previous_right) + (bcf_row_code_bcwv_previous_right))) /\ ((((exists bcf_height_bcwv_previous_right_decoded_row_scale. bcf_height_bcwv_previous_right_decoded_row_scale + S (bcf_row_scale_bcwv_previous_right) = S ((S (n)) * bcf_row_scale_scale_bcwv_previous_right)) /\ exists bcf_quotient_bcwv_previous_right_decoded_row_scale. bcf_row_scale_code_bcwv_previous_right = bcf_quotient_bcwv_previous_right_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcwv_previous_right) + (bcf_row_scale_bcwv_previous_right))) /\ (((exists bcf_height_bcwv_previous_right_decoded_value. bcf_height_bcwv_previous_right_decoded_value + S (b) = S ((S (S k)) * bcf_row_scale_bcwv_previous_right)) /\ exists bcf_quotient_bcwv_previous_right_decoded_value. bcf_row_code_bcwv_previous_right = bcf_quotient_bcwv_previous_right_decoded_value * S ((S (S k)) * bcf_row_scale_bcwv_previous_right) + (b))))))))) - 0181
specialize choose_exists n - 0182
specialize choose_exists (S k) - 0183
exact choose_exists - 0184
cases hb_exists - 0185
have hc_exists : ∃ c. Choose(S n,k,c)Exact native replay line
have hc_exists : exists c. (((exists bcf_lt_gap_bcwv_successor_left_out_of_range. bcf_lt_gap_bcwv_successor_left_out_of_range + S (S n) = k) /\ c = 0) \/ ((exists bcf_le_gap_bcwv_successor_left_in_range. bcf_le_gap_bcwv_successor_left_in_range + (k) = S n) /\ (exists bcf_row_code_code_bcwv_successor_left bcf_row_code_scale_bcwv_successor_left bcf_row_scale_code_bcwv_successor_left bcf_row_scale_scale_bcwv_successor_left bcf_row_code_bcwv_successor_left bcf_row_scale_bcwv_successor_left. ((forall bcf_row_index_bcwv_successor_left_table. (exists bcf_lt_gap_bcwv_successor_left_table_row_bound. bcf_lt_gap_bcwv_successor_left_table_row_bound + S (bcf_row_index_bcwv_successor_left_table) = S (S n)) -> exists bcf_row_code_bcwv_successor_left_table bcf_row_scale_bcwv_successor_left_table. ((((exists bcf_height_bcwv_successor_left_table_decoded_row_code. bcf_height_bcwv_successor_left_table_decoded_row_code + S (bcf_row_code_bcwv_successor_left_table) = S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_row_code. bcf_row_code_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_row_code * S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left) + (bcf_row_code_bcwv_successor_left_table))) /\ ((((exists bcf_height_bcwv_successor_left_table_decoded_row_scale. bcf_height_bcwv_successor_left_table_decoded_row_scale + S (bcf_row_scale_bcwv_successor_left_table) = S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_row_scale. bcf_row_scale_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_row_scale * S ((S (bcf_row_index_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left) + (bcf_row_scale_bcwv_successor_left_table))) /\ ((bcf_row_index_bcwv_successor_left_table = 0 /\ (forall bcf_index_bcwv_successor_left_table_zero_row. (exists bcf_lt_gap_bcwv_successor_left_table_zero_row_bound. bcf_lt_gap_bcwv_successor_left_table_zero_row_bound + S (bcf_index_bcwv_successor_left_table_zero_row) = S (S n)) -> exists bcf_value_bcwv_successor_left_table_zero_row. ((((exists bcf_height_bcwv_successor_left_table_zero_row_entry. bcf_height_bcwv_successor_left_table_zero_row_entry + S (bcf_value_bcwv_successor_left_table_zero_row) = S ((S (bcf_index_bcwv_successor_left_table_zero_row)) * bcf_row_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_zero_row_entry. bcf_row_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_zero_row_entry * S ((S (bcf_index_bcwv_successor_left_table_zero_row)) * bcf_row_scale_bcwv_successor_left_table) + (bcf_value_bcwv_successor_left_table_zero_row))) /\ ((bcf_index_bcwv_successor_left_table_zero_row = 0 /\ bcf_value_bcwv_successor_left_table_zero_row = 1) \/ exists bcf_predecessor_bcwv_successor_left_table_zero_row. bcf_index_bcwv_successor_left_table_zero_row = S bcf_predecessor_bcwv_successor_left_table_zero_row /\ bcf_value_bcwv_successor_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcwv_successor_left_table bcf_previous_code_bcwv_successor_left_table bcf_previous_scale_bcwv_successor_left_table. bcf_row_index_bcwv_successor_left_table = S bcf_predecessor_bcwv_successor_left_table /\ ((((exists bcf_height_bcwv_successor_left_table_decoded_previous_code. bcf_height_bcwv_successor_left_table_decoded_previous_code + S (bcf_previous_code_bcwv_successor_left_table) = S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_previous_code. bcf_row_code_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_code_scale_bcwv_successor_left) + (bcf_previous_code_bcwv_successor_left_table))) /\ ((((exists bcf_height_bcwv_successor_left_table_decoded_previous_scale. bcf_height_bcwv_successor_left_table_decoded_previous_scale + S (bcf_previous_scale_bcwv_successor_left_table) = S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_table_decoded_previous_scale. bcf_row_scale_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcwv_successor_left_table)) * bcf_row_scale_scale_bcwv_successor_left) + (bcf_previous_scale_bcwv_successor_left_table))) /\ (forall bcf_index_bcwv_successor_left_table_row_step. (exists bcf_lt_gap_bcwv_successor_left_table_row_step_bound. bcf_lt_gap_bcwv_successor_left_table_row_step_bound + S (bcf_index_bcwv_successor_left_table_row_step) = S (S n)) -> exists bcf_value_bcwv_successor_left_table_row_step. ((((exists bcf_height_bcwv_successor_left_table_row_step_entry. bcf_height_bcwv_successor_left_table_row_step_entry + S (bcf_value_bcwv_successor_left_table_row_step) = S ((S (bcf_index_bcwv_successor_left_table_row_step)) * bcf_row_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_row_step_entry. bcf_row_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_row_step_entry * S ((S (bcf_index_bcwv_successor_left_table_row_step)) * bcf_row_scale_bcwv_successor_left_table) + (bcf_value_bcwv_successor_left_table_row_step))) /\ ((bcf_index_bcwv_successor_left_table_row_step = 0 /\ bcf_value_bcwv_successor_left_table_row_step = 1) \/ exists bcf_predecessor_bcwv_successor_left_table_row_step bcf_left_bcwv_successor_left_table_row_step bcf_right_bcwv_successor_left_table_row_step. bcf_index_bcwv_successor_left_table_row_step = S bcf_predecessor_bcwv_successor_left_table_row_step /\ ((((exists bcf_height_bcwv_successor_left_table_row_step_previous_left. bcf_height_bcwv_successor_left_table_row_step_previous_left + S (bcf_left_bcwv_successor_left_table_row_step) = S ((S (bcf_predecessor_bcwv_successor_left_table_row_step)) * bcf_previous_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_row_step_previous_left. bcf_previous_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcwv_successor_left_table_row_step)) * bcf_previous_scale_bcwv_successor_left_table) + (bcf_left_bcwv_successor_left_table_row_step))) /\ ((((exists bcf_height_bcwv_successor_left_table_row_step_previous_right. bcf_height_bcwv_successor_left_table_row_step_previous_right + S (bcf_right_bcwv_successor_left_table_row_step) = S ((S (S (bcf_predecessor_bcwv_successor_left_table_row_step))) * bcf_previous_scale_bcwv_successor_left_table)) /\ exists bcf_quotient_bcwv_successor_left_table_row_step_previous_right. bcf_previous_code_bcwv_successor_left_table = bcf_quotient_bcwv_successor_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcwv_successor_left_table_row_step))) * bcf_previous_scale_bcwv_successor_left_table) + (bcf_right_bcwv_successor_left_table_row_step))) /\ bcf_value_bcwv_successor_left_table_row_step = bcf_left_bcwv_successor_left_table_row_step + bcf_right_bcwv_successor_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcwv_successor_left_decoded_row_code. bcf_height_bcwv_successor_left_decoded_row_code + S (bcf_row_code_bcwv_successor_left) = S ((S (S n)) * bcf_row_code_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_decoded_row_code. bcf_row_code_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_decoded_row_code * S ((S (S n)) * bcf_row_code_scale_bcwv_successor_left) + (bcf_row_code_bcwv_successor_left))) /\ ((((exists bcf_height_bcwv_successor_left_decoded_row_scale. bcf_height_bcwv_successor_left_decoded_row_scale + S (bcf_row_scale_bcwv_successor_left) = S ((S (S n)) * bcf_row_scale_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_decoded_row_scale. bcf_row_scale_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_decoded_row_scale * S ((S (S n)) * bcf_row_scale_scale_bcwv_successor_left) + (bcf_row_scale_bcwv_successor_left))) /\ (((exists bcf_height_bcwv_successor_left_decoded_value. bcf_height_bcwv_successor_left_decoded_value + S (c) = S ((S (k)) * bcf_row_scale_bcwv_successor_left)) /\ exists bcf_quotient_bcwv_successor_left_decoded_value. bcf_row_code_bcwv_successor_left = bcf_quotient_bcwv_successor_left_decoded_value * S ((S (k)) * bcf_row_scale_bcwv_successor_left) + (c))))))))) - 0186
specialize choose_exists (S n) - 0187
specialize choose_exists k - 0188
exact choose_exists - 0189
cases hc_exists - 0190
rewrite zero_or_succ_right_witness at hsum - 0191
have hsecond_complement : S k + x1 = n - 0192
apply PA2 - 0193
trans S k + S x1 - 0194
symm - 0195
apply PA4 - 0196
exact hsum - 0197
have hfirst_complement : k + S x1 = n - 0198
trans S (k + x1) - 0199
apply PA4 - 0200
trans S k + x1 - 0201
symm - 0202
apply add_succ_left - 0203
exact hsecond_complement - 0204
have hx_sum : x = x2 + x3 - 0205
specialize choose_succ_succ n - 0206
specialize choose_succ_succ k - 0207
specialize choose_succ_succ x2 - 0208
specialize choose_succ_succ x3 - 0209
specialize choose_succ_succ x - 0210
apply choose_succ_succ - 0211
exact ha_exists_witness - 0212
exact hb_exists_witness - 0213
exact hlower - 0214
have hy_sum : y = x4 + x - 0215
specialize choose_succ_succ (S n) - 0216
specialize choose_succ_succ k - 0217
specialize choose_succ_succ x4 - 0218
specialize choose_succ_succ x - 0219
specialize choose_succ_succ y - 0220
apply choose_succ_succ - 0221
exact hc_exists_witness - 0222
exact hlower - 0223
exact hupper - 0224
have hfirst_weight : S (S x1) * x4 = S n * x2 - 0225
specialize IH k - 0226
specialize IH (S x1) - 0227
specialize IH x2 - 0228
specialize IH x4 - 0229
apply IH - 0230
exact hfirst_complement - 0231
exact ha_exists_witness - 0232
exact hc_exists_witness - 0233
have hsecond_weight : S x1 * x = S n * x3 - 0234
specialize IH (S k) - 0235
specialize IH x1 - 0236
specialize IH x3 - 0237
specialize IH x - 0238
apply IH - 0239
exact hsecond_complement - 0240
exact hb_exists_witness - 0241
exact hlower - 0242
rewrite zero_or_succ_right_witness - 0243
trans S (S x1) * (x4 + x) - 0244
congr - 0245
refl - 0246
exact hy_sum - 0247
trans S (S x1) * x4 + S (S x1) * x - 0248
apply mul_add - 0249
trans S n * x2 + (S x1 * x + x) - 0250
congr - 0251
exact hfirst_weight - 0252
specialize mul_succ_left (S x1) - 0253
specialize mul_succ_left x - 0254
apply mul_succ_left - 0255
trans S n * x2 + (S n * x3 + x) - 0256
congr - 0257
refl - 0258
congr - 0259
exact hsecond_weight - 0260
refl - 0261
trans (S n * x2 + S n * x3) + x - 0262
specialize add_assoc (S n * x2) - 0263
specialize add_assoc (S n * x3) - 0264
specialize add_assoc x - 0265
symm - 0266
apply add_assoc - 0267
trans S n * (x2 + x3) + x - 0268
congr - 0269
specialize mul_add (S n) - 0270
specialize mul_add x2 - 0271
specialize mul_add x3 - 0272
symm - 0273
apply mul_add - 0274
refl - 0275
trans S n * x + x - 0276
congr - 0277
congr - 0278
refl - 0279
symm - 0280
exact hx_sum - 0281
refl - 0282
specialize mul_succ_left (S n) - 0283
specialize mul_succ_left x - 0284
symm - 0285
exact mul_succ_left