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
∀ b. ∀ c. ∀ l. ∀ n. Sum(b,c,S l,n) → BetaAt(b,c,l,0) → Sum(b,c,l,n)Every 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
3 occurrences
In local proof propositions
2 occurrences
Exact expanded native-PA statement
forall b c l n. (exists fs_u_blrr_drop_successor fs_v_blrr_drop_successor. ((((exists fs_h_blrr_drop_successor_body_start. fs_h_blrr_drop_successor_body_start + S (0) = S ((S (0)) * fs_v_blrr_drop_successor)) /\ exists fs_q_blrr_drop_successor_body_start. fs_u_blrr_drop_successor = fs_q_blrr_drop_successor_body_start * S ((S (0)) * fs_v_blrr_drop_successor) + (0))) /\ ((((exists fs_h_blrr_drop_successor_body_terminal. fs_h_blrr_drop_successor_body_terminal + S (n) = S ((S (S l)) * fs_v_blrr_drop_successor)) /\ exists fs_q_blrr_drop_successor_body_terminal. fs_u_blrr_drop_successor = fs_q_blrr_drop_successor_body_terminal * S ((S (S l)) * fs_v_blrr_drop_successor) + (n))) /\ forall fs_i_blrr_drop_successor_body_steps. (exists fs_lt_blrr_drop_successor_body_steps_bound. fs_lt_blrr_drop_successor_body_steps_bound + S fs_i_blrr_drop_successor_body_steps = S l) -> exists fs_a_blrr_drop_successor_body_steps fs_r_blrr_drop_successor_body_steps fs_s_blrr_drop_successor_body_steps. ((((exists fs_h_blrr_drop_successor_body_steps_summand. fs_h_blrr_drop_successor_body_steps_summand + S (fs_a_blrr_drop_successor_body_steps) = S ((S (fs_i_blrr_drop_successor_body_steps)) * c)) /\ exists fs_q_blrr_drop_successor_body_steps_summand. b = fs_q_blrr_drop_successor_body_steps_summand * S ((S (fs_i_blrr_drop_successor_body_steps)) * c) + (fs_a_blrr_drop_successor_body_steps))) /\ ((((exists fs_h_blrr_drop_successor_body_steps_partial. fs_h_blrr_drop_successor_body_steps_partial + S (fs_r_blrr_drop_successor_body_steps) = S ((S (fs_i_blrr_drop_successor_body_steps)) * fs_v_blrr_drop_successor)) /\ exists fs_q_blrr_drop_successor_body_steps_partial. fs_u_blrr_drop_successor = fs_q_blrr_drop_successor_body_steps_partial * S ((S (fs_i_blrr_drop_successor_body_steps)) * fs_v_blrr_drop_successor) + (fs_r_blrr_drop_successor_body_steps))) /\ ((((exists fs_h_blrr_drop_successor_body_steps_successor. fs_h_blrr_drop_successor_body_steps_successor + S (fs_s_blrr_drop_successor_body_steps) = S ((S (S fs_i_blrr_drop_successor_body_steps)) * fs_v_blrr_drop_successor)) /\ exists fs_q_blrr_drop_successor_body_steps_successor. fs_u_blrr_drop_successor = fs_q_blrr_drop_successor_body_steps_successor * S ((S (S fs_i_blrr_drop_successor_body_steps)) * fs_v_blrr_drop_successor) + (fs_s_blrr_drop_successor_body_steps))) /\ fs_s_blrr_drop_successor_body_steps = fs_r_blrr_drop_successor_body_steps + fs_a_blrr_drop_successor_body_steps)))))) -> (((exists fs_h_blrr_drop_zero. fs_h_blrr_drop_zero + S (0) = S ((S (l)) * c)) /\ exists fs_q_blrr_drop_zero. b = fs_q_blrr_drop_zero * S ((S (l)) * c) + (0))) -> (exists ff_u_blrr_drop_predecessor ff_v_blrr_drop_predecessor. ((((exists ff_h_blrr_drop_predecessor_start. ff_h_blrr_drop_predecessor_start + S (0) = S ((S (0)) * ff_v_blrr_drop_predecessor)) /\ exists ff_q_blrr_drop_predecessor_start. ff_u_blrr_drop_predecessor = ff_q_blrr_drop_predecessor_start * S ((S (0)) * ff_v_blrr_drop_predecessor) + (0))) /\ ((((exists ff_h_blrr_drop_predecessor_terminal. ff_h_blrr_drop_predecessor_terminal + S (n) = S ((S (l)) * ff_v_blrr_drop_predecessor)) /\ exists ff_q_blrr_drop_predecessor_terminal. ff_u_blrr_drop_predecessor = ff_q_blrr_drop_predecessor_terminal * S ((S (l)) * ff_v_blrr_drop_predecessor) + (n))) /\ forall ff_i_blrr_drop_predecessor. (exists ff_lt_blrr_drop_predecessor_bound. ff_lt_blrr_drop_predecessor_bound + S ff_i_blrr_drop_predecessor = l) -> exists ff_a_blrr_drop_predecessor ff_r_blrr_drop_predecessor ff_s_blrr_drop_predecessor. ((((exists ff_h_blrr_drop_predecessor_summand. ff_h_blrr_drop_predecessor_summand + S (ff_a_blrr_drop_predecessor) = S ((S (ff_i_blrr_drop_predecessor)) * c)) /\ exists ff_q_blrr_drop_predecessor_summand. b = ff_q_blrr_drop_predecessor_summand * S ((S (ff_i_blrr_drop_predecessor)) * c) + (ff_a_blrr_drop_predecessor))) /\ ((((exists ff_h_blrr_drop_predecessor_partial. ff_h_blrr_drop_predecessor_partial + S (ff_r_blrr_drop_predecessor) = S ((S (ff_i_blrr_drop_predecessor)) * ff_v_blrr_drop_predecessor)) /\ exists ff_q_blrr_drop_predecessor_partial. ff_u_blrr_drop_predecessor = ff_q_blrr_drop_predecessor_partial * S ((S (ff_i_blrr_drop_predecessor)) * ff_v_blrr_drop_predecessor) + (ff_r_blrr_drop_predecessor))) /\ ((((exists ff_h_blrr_drop_predecessor_successor. ff_h_blrr_drop_predecessor_successor + S (ff_s_blrr_drop_predecessor) = S ((S (S ff_i_blrr_drop_predecessor)) * ff_v_blrr_drop_predecessor)) /\ exists ff_q_blrr_drop_predecessor_successor. ff_u_blrr_drop_predecessor = ff_q_blrr_drop_predecessor_successor * S ((S (S ff_i_blrr_drop_predecessor)) * ff_v_blrr_drop_predecessor) + (ff_s_blrr_drop_predecessor))) /\ ff_s_blrr_drop_predecessor = ff_r_blrr_drop_predecessor + ff_a_blrr_drop_predecessor))))))Proof neighborhood
Direct theorem prerequisites
Direct 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 (2)
01Fix variables and assumptionsL1–6
02Establish hdecompositionL7–13
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum succ decompose.
- L7
have hdecomposition : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Sum(b,c,l,r) ∧ n = r + a)Definitions: BetaAt(b,c,l,a)Sum(b,c,l,r)Original native command in the exact edition - L8
specialize beta_sum_succ_decompose b - L9
specialize beta_sum_succ_decompose c - L10
specialize beta_sum_succ_decompose l - L11
specialize beta_sum_succ_decompose n - L12
apply beta_sum_succ_decompose - L13
exact hsum
03Separate the logical casesL14–17
04Establish haL18–26
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
05Establish hnL27–34
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA3.
Original defined command ledger · 34 lines
- 0001
intro b - 0002
intro c - 0003
intro l - 0004
intro n - 0005
intro hsum - 0006
intro hzero - 0007
have hdecomposition : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Sum(b,c,l,r) ∧ n = r + a)Exact native replay line
have hdecomposition : exists a r. (((exists ff_h_blrr_drop_decomposition_entry. ff_h_blrr_drop_decomposition_entry + S (a) = S ((S (l)) * c)) /\ exists ff_q_blrr_drop_decomposition_entry. b = ff_q_blrr_drop_decomposition_entry * S ((S (l)) * c) + (a))) /\ ((exists ff_u_blrr_drop_decomposition_prefix ff_v_blrr_drop_decomposition_prefix. ((((exists ff_h_blrr_drop_decomposition_prefix_start. ff_h_blrr_drop_decomposition_prefix_start + S (0) = S ((S (0)) * ff_v_blrr_drop_decomposition_prefix)) /\ exists ff_q_blrr_drop_decomposition_prefix_start. ff_u_blrr_drop_decomposition_prefix = ff_q_blrr_drop_decomposition_prefix_start * S ((S (0)) * ff_v_blrr_drop_decomposition_prefix) + (0))) /\ ((((exists ff_h_blrr_drop_decomposition_prefix_terminal. ff_h_blrr_drop_decomposition_prefix_terminal + S (r) = S ((S (l)) * ff_v_blrr_drop_decomposition_prefix)) /\ exists ff_q_blrr_drop_decomposition_prefix_terminal. ff_u_blrr_drop_decomposition_prefix = ff_q_blrr_drop_decomposition_prefix_terminal * S ((S (l)) * ff_v_blrr_drop_decomposition_prefix) + (r))) /\ forall ff_i_blrr_drop_decomposition_prefix. (exists ff_lt_blrr_drop_decomposition_prefix_bound. ff_lt_blrr_drop_decomposition_prefix_bound + S ff_i_blrr_drop_decomposition_prefix = l) -> exists ff_a_blrr_drop_decomposition_prefix ff_r_blrr_drop_decomposition_prefix ff_s_blrr_drop_decomposition_prefix. ((((exists ff_h_blrr_drop_decomposition_prefix_summand. ff_h_blrr_drop_decomposition_prefix_summand + S (ff_a_blrr_drop_decomposition_prefix) = S ((S (ff_i_blrr_drop_decomposition_prefix)) * c)) /\ exists ff_q_blrr_drop_decomposition_prefix_summand. b = ff_q_blrr_drop_decomposition_prefix_summand * S ((S (ff_i_blrr_drop_decomposition_prefix)) * c) + (ff_a_blrr_drop_decomposition_prefix))) /\ ((((exists ff_h_blrr_drop_decomposition_prefix_partial. ff_h_blrr_drop_decomposition_prefix_partial + S (ff_r_blrr_drop_decomposition_prefix) = S ((S (ff_i_blrr_drop_decomposition_prefix)) * ff_v_blrr_drop_decomposition_prefix)) /\ exists ff_q_blrr_drop_decomposition_prefix_partial. ff_u_blrr_drop_decomposition_prefix = ff_q_blrr_drop_decomposition_prefix_partial * S ((S (ff_i_blrr_drop_decomposition_prefix)) * ff_v_blrr_drop_decomposition_prefix) + (ff_r_blrr_drop_decomposition_prefix))) /\ ((((exists ff_h_blrr_drop_decomposition_prefix_successor. ff_h_blrr_drop_decomposition_prefix_successor + S (ff_s_blrr_drop_decomposition_prefix) = S ((S (S ff_i_blrr_drop_decomposition_prefix)) * ff_v_blrr_drop_decomposition_prefix)) /\ exists ff_q_blrr_drop_decomposition_prefix_successor. ff_u_blrr_drop_decomposition_prefix = ff_q_blrr_drop_decomposition_prefix_successor * S ((S (S ff_i_blrr_drop_decomposition_prefix)) * ff_v_blrr_drop_decomposition_prefix) + (ff_s_blrr_drop_decomposition_prefix))) /\ ff_s_blrr_drop_decomposition_prefix = ff_r_blrr_drop_decomposition_prefix + ff_a_blrr_drop_decomposition_prefix)))))) /\ n = r + a) - 0008
specialize beta_sum_succ_decompose b - 0009
specialize beta_sum_succ_decompose c - 0010
specialize beta_sum_succ_decompose l - 0011
specialize beta_sum_succ_decompose n - 0012
apply beta_sum_succ_decompose - 0013
exact hsum - 0014
cases hdecomposition - 0015
cases hdecomposition_witness - 0016
cases hdecomposition_witness_witness - 0017
cases hdecomposition_witness_witness_right - 0018
have ha : x = 0 - 0019
specialize beta_at_unique b - 0020
specialize beta_at_unique c - 0021
specialize beta_at_unique l - 0022
specialize beta_at_unique x - 0023
specialize beta_at_unique 0 - 0024
apply beta_at_unique - 0025
exact hdecomposition_witness_witness_left - 0026
exact hzero - 0027
have hn : n = x1 - 0028
trans x1 + x - 0029
exact hdecomposition_witness_witness_right_right - 0030
rewrite ha - 0031
apply PA3 - 0032
rewrite hn - 0033
rewrite hn - 0034
exact hdecomposition_witness_witness_right_left