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
∀ sb. ∀ sc. ∀ r. ∀ l. ∀ e. BitCount(sb,sc,l,e) → ∃ x. ∃ y. ∀ z. ∀ n. Lt(z,l) → BetaAt(sb,sc,z,n) → n = 0 ∧ BetaAt(x,y,z,1) ∨ n = 1 ∧ BetaAt(x,y,z,r)Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.
Definitions used by this theorem
In the theorem statement
5 occurrences
In local proof propositions
6 occurrences
Exact expanded native-PA statement
forall sb sc r l e. (((exists ff_u_recode_count_sum ff_v_recode_count_sum. ((((exists ff_h_recode_count_sum_start. ff_h_recode_count_sum_start + S (0) = S ((S (0)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_start. ff_u_recode_count_sum = ff_q_recode_count_sum_start * S ((S (0)) * ff_v_recode_count_sum) + (0))) /\ ((((exists ff_h_recode_count_sum_terminal. ff_h_recode_count_sum_terminal + S (e) = S ((S (l)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_terminal. ff_u_recode_count_sum = ff_q_recode_count_sum_terminal * S ((S (l)) * ff_v_recode_count_sum) + (e))) /\ forall ff_i_recode_count_sum. (exists ff_lt_recode_count_sum_bound. ff_lt_recode_count_sum_bound + S ff_i_recode_count_sum = l) -> exists ff_a_recode_count_sum ff_r_recode_count_sum ff_s_recode_count_sum. ((((exists ff_h_recode_count_sum_summand. ff_h_recode_count_sum_summand + S (ff_a_recode_count_sum) = S ((S (ff_i_recode_count_sum)) * sc)) /\ exists ff_q_recode_count_sum_summand. sb = ff_q_recode_count_sum_summand * S ((S (ff_i_recode_count_sum)) * sc) + (ff_a_recode_count_sum))) /\ ((((exists ff_h_recode_count_sum_partial. ff_h_recode_count_sum_partial + S (ff_r_recode_count_sum) = S ((S (ff_i_recode_count_sum)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_partial. ff_u_recode_count_sum = ff_q_recode_count_sum_partial * S ((S (ff_i_recode_count_sum)) * ff_v_recode_count_sum) + (ff_r_recode_count_sum))) /\ ((((exists ff_h_recode_count_sum_successor. ff_h_recode_count_sum_successor + S (ff_s_recode_count_sum) = S ((S (S ff_i_recode_count_sum)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_successor. ff_u_recode_count_sum = ff_q_recode_count_sum_successor * S ((S (S ff_i_recode_count_sum)) * ff_v_recode_count_sum) + (ff_s_recode_count_sum))) /\ ff_s_recode_count_sum = ff_r_recode_count_sum + ff_a_recode_count_sum)))))) /\ (forall ff_i_recode_count_bits. (exists ff_lt_recode_count_bits_bound. ff_lt_recode_count_bits_bound + S ff_i_recode_count_bits = l) -> exists ff_bit_recode_count_bits. ((((exists ff_h_recode_count_bits_decoded. ff_h_recode_count_bits_decoded + S (ff_bit_recode_count_bits) = S ((S (ff_i_recode_count_bits)) * sc)) /\ exists ff_q_recode_count_bits_decoded. sb = ff_q_recode_count_bits_decoded * S ((S (ff_i_recode_count_bits)) * sc) + (ff_bit_recode_count_bits))) /\ (ff_bit_recode_count_bits = 0 \/ ff_bit_recode_count_bits = 1))))) -> exists fb fc. (forall gspf_index_recode_result gspf_bit_recode_result. (exists gsp_lt_gap_recode_result_bound. gsp_lt_gap_recode_result_bound + S gspf_index_recode_result = l) -> (((exists ff_h_gspf_recode_result_bit. ff_h_gspf_recode_result_bit + S (gspf_bit_recode_result) = S ((S (gspf_index_recode_result)) * sc)) /\ exists ff_q_gspf_recode_result_bit. sb = ff_q_gspf_recode_result_bit * S ((S (gspf_index_recode_result)) * sc) + (gspf_bit_recode_result))) -> (((gspf_bit_recode_result = 0) /\ (((exists gsp_beta_height_gspf_recode_result_one. gsp_beta_height_gspf_recode_result_one + S (1) = S ((S (gspf_index_recode_result)) * fc)) /\ exists gsp_beta_quotient_gspf_recode_result_one. fb = gsp_beta_quotient_gspf_recode_result_one * S ((S (gspf_index_recode_result)) * fc) + (1)))) \/ ((gspf_bit_recode_result = 1) /\ (((exists ff_h_gspf_recode_result_predecessor. ff_h_gspf_recode_result_predecessor + S (r) = S ((S (gspf_index_recode_result)) * fc)) /\ exists ff_q_gspf_recode_result_predecessor. fb = ff_q_gspf_recode_result_predecessor * S ((S (gspf_index_recode_result)) * fc) + (r))))))Proof neighborhood
Direct theorem prerequisites
PA0004 add_eq_zero_right PA0005 succ_ne_zero PA0042 bit_count_succ_decompose PA007F beta_sign_factor_prefix_extendDirect theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (4)
01Fix variables and assumptionsL1–3
02Induction on lL4–6
03Construct an explicit witnessL7–8
04Fix variables and assumptionsL9–12
05Separate the logical casesL13–14
06Establish hsiL15–24
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.
07Establish hdecompL25–33
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bit count succ decompose.
- L25
have hdecomp : ∃ a. ∃ k. BetaAt(sb,sc,l,a) ∧ (BitCount(sb,sc,l,k) ∧ ((a = 0 ∨ a = 1) ∧ e = k + a))Definitions: BetaAt(sb,sc,l,a)BitCount(sb,sc,l,k)Original native command in the exact edition - L26
specialize bit_count_succ_decompose sb - L27
specialize bit_count_succ_decompose sc - L28
specialize bit_count_succ_decompose l - L29
specialize bit_count_succ_decompose (S l) - L30
specialize bit_count_succ_decompose e - L31
apply bit_count_succ_decompose - L32
refl - L33
exact hcount
08Separate the logical casesL34–38
09Establish hpreviousL39–42
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
- L39
have hprevious : ∃ fb. ∃ fc. ∀ x. ∀ y. Lt(x,l) → BetaAt(sb,sc,x,y) → y = 0 ∧ BetaAt(fb,fc,x,1) ∨ y = 1 ∧ BetaAt(fb,fc,x,r)Definitions: Lt(x,l)BetaAt(sb,sc,x,y)BetaAt(fb,fc,x,1)BetaAt(fb,fc,x,r)Original native command in the exact edition - L40
specialize IH x1 - L41
apply IH - L42
exact hdecomp_witness_witness_right_left
10Separate the logical casesL43–45
11Use earlier factsL46–55
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L46
specialize beta_sign_factor_prefix_extend sb - L47
specialize beta_sign_factor_prefix_extend sc - L48
specialize beta_sign_factor_prefix_extend x2 - L49
specialize beta_sign_factor_prefix_extend x3 - L50
specialize beta_sign_factor_prefix_extend r - L51
specialize beta_sign_factor_prefix_extend l - L52
specialize beta_sign_factor_prefix_extend x - L53
specialize beta_sign_factor_prefix_extend 1 - L54
apply beta_sign_factor_prefix_extend - L55
exact hprevious_witness_witness
12Use earlier factsL56–56
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L56
exact hdecomp_witness_witness_left
13Separate the logical casesL57–58
14Use earlier factsL59–59
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L59
exact hdecomp_witness_witness_right_right_left_left
15Calculate and transport equalitiesL60–60
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L60
refl
16Use earlier factsL61–70
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L61
specialize beta_sign_factor_prefix_extend sb - L62
specialize beta_sign_factor_prefix_extend sc - L63
specialize beta_sign_factor_prefix_extend x2 - L64
specialize beta_sign_factor_prefix_extend x3 - L65
specialize beta_sign_factor_prefix_extend r - L66
specialize beta_sign_factor_prefix_extend l - L67
specialize beta_sign_factor_prefix_extend x - L68
specialize beta_sign_factor_prefix_extend r - L69
apply beta_sign_factor_prefix_extend - L70
exact hprevious_witness_witness
17Use earlier factsL71–71
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L71
exact hdecomp_witness_witness_left
18Separate the logical casesL72–73
19Use earlier factsL74–74
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L74
exact hdecomp_witness_witness_right_right_left_right
20Calculate and transport equalitiesL75–75
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L75
refl
Original defined command ledger · 75 lines
- 0001
intro sb - 0002
intro sc - 0003
intro r - 0004
induction l - 0005
intro e - 0006
intro hcount - 0007
exists 0 - 0008
exists 0 - 0009
intro i - 0010
intro v - 0011
intro hi - 0012
intro hv - 0013
exfalso - 0014
cases hi - 0015
have hsi : S i = 0 - 0016
specialize add_eq_zero_right x - 0017
specialize add_eq_zero_right (S i) - 0018
apply add_eq_zero_right - 0019
exact hi_witness - 0020
specialize succ_ne_zero i - 0021
apply succ_ne_zero - 0022
exact hsi - 0023
intro e - 0024
intro hcount - 0025
have hdecomp : ∃ a. ∃ k. BetaAt(sb,sc,l,a) ∧ (BitCount(sb,sc,l,k) ∧ ((a = 0 ∨ a = 1) ∧ e = k + a))Exact native replay line
have hdecomp : exists a k. (((exists ff_h_recode_count_last. ff_h_recode_count_last + S (a) = S ((S (l)) * sc)) /\ exists ff_q_recode_count_last. sb = ff_q_recode_count_last * S ((S (l)) * sc) + (a))) /\ ((((exists ff_u_recode_count_prefix_sum ff_v_recode_count_prefix_sum. ((((exists ff_h_recode_count_prefix_sum_start. ff_h_recode_count_prefix_sum_start + S (0) = S ((S (0)) * ff_v_recode_count_prefix_sum)) /\ exists ff_q_recode_count_prefix_sum_start. ff_u_recode_count_prefix_sum = ff_q_recode_count_prefix_sum_start * S ((S (0)) * ff_v_recode_count_prefix_sum) + (0))) /\ ((((exists ff_h_recode_count_prefix_sum_terminal. ff_h_recode_count_prefix_sum_terminal + S (k) = S ((S (l)) * ff_v_recode_count_prefix_sum)) /\ exists ff_q_recode_count_prefix_sum_terminal. ff_u_recode_count_prefix_sum = ff_q_recode_count_prefix_sum_terminal * S ((S (l)) * ff_v_recode_count_prefix_sum) + (k))) /\ forall ff_i_recode_count_prefix_sum. (exists ff_lt_recode_count_prefix_sum_bound. ff_lt_recode_count_prefix_sum_bound + S ff_i_recode_count_prefix_sum = l) -> exists ff_a_recode_count_prefix_sum ff_r_recode_count_prefix_sum ff_s_recode_count_prefix_sum. ((((exists ff_h_recode_count_prefix_sum_summand. ff_h_recode_count_prefix_sum_summand + S (ff_a_recode_count_prefix_sum) = S ((S (ff_i_recode_count_prefix_sum)) * sc)) /\ exists ff_q_recode_count_prefix_sum_summand. sb = ff_q_recode_count_prefix_sum_summand * S ((S (ff_i_recode_count_prefix_sum)) * sc) + (ff_a_recode_count_prefix_sum))) /\ ((((exists ff_h_recode_count_prefix_sum_partial. ff_h_recode_count_prefix_sum_partial + S (ff_r_recode_count_prefix_sum) = S ((S (ff_i_recode_count_prefix_sum)) * ff_v_recode_count_prefix_sum)) /\ exists ff_q_recode_count_prefix_sum_partial. ff_u_recode_count_prefix_sum = ff_q_recode_count_prefix_sum_partial * S ((S (ff_i_recode_count_prefix_sum)) * ff_v_recode_count_prefix_sum) + (ff_r_recode_count_prefix_sum))) /\ ((((exists ff_h_recode_count_prefix_sum_successor. ff_h_recode_count_prefix_sum_successor + S (ff_s_recode_count_prefix_sum) = S ((S (S ff_i_recode_count_prefix_sum)) * ff_v_recode_count_prefix_sum)) /\ exists ff_q_recode_count_prefix_sum_successor. ff_u_recode_count_prefix_sum = ff_q_recode_count_prefix_sum_successor * S ((S (S ff_i_recode_count_prefix_sum)) * ff_v_recode_count_prefix_sum) + (ff_s_recode_count_prefix_sum))) /\ ff_s_recode_count_prefix_sum = ff_r_recode_count_prefix_sum + ff_a_recode_count_prefix_sum)))))) /\ (forall ff_i_recode_count_prefix_bits. (exists ff_lt_recode_count_prefix_bits_bound. ff_lt_recode_count_prefix_bits_bound + S ff_i_recode_count_prefix_bits = l) -> exists ff_bit_recode_count_prefix_bits. ((((exists ff_h_recode_count_prefix_bits_decoded. ff_h_recode_count_prefix_bits_decoded + S (ff_bit_recode_count_prefix_bits) = S ((S (ff_i_recode_count_prefix_bits)) * sc)) /\ exists ff_q_recode_count_prefix_bits_decoded. sb = ff_q_recode_count_prefix_bits_decoded * S ((S (ff_i_recode_count_prefix_bits)) * sc) + (ff_bit_recode_count_prefix_bits))) /\ (ff_bit_recode_count_prefix_bits = 0 \/ ff_bit_recode_count_prefix_bits = 1))))) /\ ((a = 0 \/ a = 1) /\ e = k + a)) - 0026
specialize bit_count_succ_decompose sb - 0027
specialize bit_count_succ_decompose sc - 0028
specialize bit_count_succ_decompose l - 0029
specialize bit_count_succ_decompose (S l) - 0030
specialize bit_count_succ_decompose e - 0031
apply bit_count_succ_decompose - 0032
refl - 0033
exact hcount - 0034
cases hdecomp - 0035
cases hdecomp_witness - 0036
cases hdecomp_witness_witness - 0037
cases hdecomp_witness_witness_right - 0038
cases hdecomp_witness_witness_right_right - 0039
have hprevious : ∃ fb. ∃ fc. ∀ x. ∀ y. Lt(x,l) → BetaAt(sb,sc,x,y) → y = 0 ∧ BetaAt(fb,fc,x,1) ∨ y = 1 ∧ BetaAt(fb,fc,x,r)Exact native replay line
have hprevious : exists fb fc. (forall gspf_index_recode_previous gspf_bit_recode_previous. (exists gsp_lt_gap_recode_previous_bound. gsp_lt_gap_recode_previous_bound + S gspf_index_recode_previous = l) -> (((exists ff_h_gspf_recode_previous_bit. ff_h_gspf_recode_previous_bit + S (gspf_bit_recode_previous) = S ((S (gspf_index_recode_previous)) * sc)) /\ exists ff_q_gspf_recode_previous_bit. sb = ff_q_gspf_recode_previous_bit * S ((S (gspf_index_recode_previous)) * sc) + (gspf_bit_recode_previous))) -> (((gspf_bit_recode_previous = 0) /\ (((exists gsp_beta_height_gspf_recode_previous_one. gsp_beta_height_gspf_recode_previous_one + S (1) = S ((S (gspf_index_recode_previous)) * fc)) /\ exists gsp_beta_quotient_gspf_recode_previous_one. fb = gsp_beta_quotient_gspf_recode_previous_one * S ((S (gspf_index_recode_previous)) * fc) + (1)))) \/ ((gspf_bit_recode_previous = 1) /\ (((exists ff_h_gspf_recode_previous_predecessor. ff_h_gspf_recode_previous_predecessor + S (r) = S ((S (gspf_index_recode_previous)) * fc)) /\ exists ff_q_gspf_recode_previous_predecessor. fb = ff_q_gspf_recode_previous_predecessor * S ((S (gspf_index_recode_previous)) * fc) + (r)))))) - 0040
specialize IH x1 - 0041
apply IH - 0042
exact hdecomp_witness_witness_right_left - 0043
cases hprevious - 0044
cases hprevious_witness - 0045
cases hdecomp_witness_witness_right_right_left - 0046
specialize beta_sign_factor_prefix_extend sb - 0047
specialize beta_sign_factor_prefix_extend sc - 0048
specialize beta_sign_factor_prefix_extend x2 - 0049
specialize beta_sign_factor_prefix_extend x3 - 0050
specialize beta_sign_factor_prefix_extend r - 0051
specialize beta_sign_factor_prefix_extend l - 0052
specialize beta_sign_factor_prefix_extend x - 0053
specialize beta_sign_factor_prefix_extend 1 - 0054
apply beta_sign_factor_prefix_extend - 0055
exact hprevious_witness_witness - 0056
exact hdecomp_witness_witness_left - 0057
left - 0058
split - 0059
exact hdecomp_witness_witness_right_right_left_left - 0060
refl - 0061
specialize beta_sign_factor_prefix_extend sb - 0062
specialize beta_sign_factor_prefix_extend sc - 0063
specialize beta_sign_factor_prefix_extend x2 - 0064
specialize beta_sign_factor_prefix_extend x3 - 0065
specialize beta_sign_factor_prefix_extend r - 0066
specialize beta_sign_factor_prefix_extend l - 0067
specialize beta_sign_factor_prefix_extend x - 0068
specialize beta_sign_factor_prefix_extend r - 0069
apply beta_sign_factor_prefix_extend - 0070
exact hprevious_witness_witness - 0071
exact hdecomp_witness_witness_left - 0072
right - 0073
split - 0074
exact hdecomp_witness_witness_right_right_left_right - 0075
refl