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. ∀ d. ∀ e. ∀ f. ∀ g. ∀ l. (∀ x. Lt(x,S l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(d,e,x,z) ∧ (BetaAt(f,g,x,n) ∧ (n = 0 ∧ z = y + y ∨ n = 1 ∧ z = S (y + y))))) → ∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(d,e,x,z) ∧ (BetaAt(f,g,x,n) ∧ (n = 0 ∧ z = y + y ∨ n = 1 ∧ z = S (y + y))))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
8 occurrences
In local proof propositions
none
0 occurrences
Exact expanded native-PA statement
forall b c d e f g l. (forall b5cc_index_b5ccpr_source. (exists bcf_lt_gap_b5ccpr_source_bound. bcf_lt_gap_b5ccpr_source_bound + S (b5cc_index_b5ccpr_source) = S l) -> exists b5cc_left_b5ccpr_source b5cc_right_b5ccpr_source b5cc_bit_b5ccpr_source. (((exists fs_h_b5cc_b5ccpr_source_left. fs_h_b5cc_b5ccpr_source_left + S (b5cc_left_b5ccpr_source) = S ((S (b5cc_index_b5ccpr_source)) * c)) /\ exists fs_q_b5cc_b5ccpr_source_left. b = fs_q_b5cc_b5ccpr_source_left * S ((S (b5cc_index_b5ccpr_source)) * c) + (b5cc_left_b5ccpr_source))) /\ ((((exists fs_h_b5cc_b5ccpr_source_right. fs_h_b5cc_b5ccpr_source_right + S (b5cc_right_b5ccpr_source) = S ((S (b5cc_index_b5ccpr_source)) * e)) /\ exists fs_q_b5cc_b5ccpr_source_right. d = fs_q_b5cc_b5ccpr_source_right * S ((S (b5cc_index_b5ccpr_source)) * e) + (b5cc_right_b5ccpr_source))) /\ ((((exists fs_h_b5cc_b5ccpr_source_bit. fs_h_b5cc_b5ccpr_source_bit + S (b5cc_bit_b5ccpr_source) = S ((S (b5cc_index_b5ccpr_source)) * g)) /\ exists fs_q_b5cc_b5ccpr_source_bit. f = fs_q_b5cc_b5ccpr_source_bit * S ((S (b5cc_index_b5ccpr_source)) * g) + (b5cc_bit_b5ccpr_source))) /\ (((b5cc_bit_b5ccpr_source = 0 /\ b5cc_right_b5ccpr_source = b5cc_left_b5ccpr_source + b5cc_left_b5ccpr_source) \/ (b5cc_bit_b5ccpr_source = 1 /\ b5cc_right_b5ccpr_source = S (b5cc_left_b5ccpr_source + b5cc_left_b5ccpr_source))))))) -> (forall b5cc_index_b5ccpr_result. (exists bcf_lt_gap_b5ccpr_result_bound. bcf_lt_gap_b5ccpr_result_bound + S (b5cc_index_b5ccpr_result) = l) -> exists b5cc_left_b5ccpr_result b5cc_right_b5ccpr_result b5cc_bit_b5ccpr_result. (((exists fs_h_b5cc_b5ccpr_result_left. fs_h_b5cc_b5ccpr_result_left + S (b5cc_left_b5ccpr_result) = S ((S (b5cc_index_b5ccpr_result)) * c)) /\ exists fs_q_b5cc_b5ccpr_result_left. b = fs_q_b5cc_b5ccpr_result_left * S ((S (b5cc_index_b5ccpr_result)) * c) + (b5cc_left_b5ccpr_result))) /\ ((((exists fs_h_b5cc_b5ccpr_result_right. fs_h_b5cc_b5ccpr_result_right + S (b5cc_right_b5ccpr_result) = S ((S (b5cc_index_b5ccpr_result)) * e)) /\ exists fs_q_b5cc_b5ccpr_result_right. d = fs_q_b5cc_b5ccpr_result_right * S ((S (b5cc_index_b5ccpr_result)) * e) + (b5cc_right_b5ccpr_result))) /\ ((((exists fs_h_b5cc_b5ccpr_result_bit. fs_h_b5cc_b5ccpr_result_bit + S (b5cc_bit_b5ccpr_result) = S ((S (b5cc_index_b5ccpr_result)) * g)) /\ exists fs_q_b5cc_b5ccpr_result_bit. f = fs_q_b5cc_b5ccpr_result_bit * S ((S (b5cc_index_b5ccpr_result)) * g) + (b5cc_bit_b5ccpr_result))) /\ (((b5cc_bit_b5ccpr_result = 0 /\ b5cc_right_b5ccpr_result = b5cc_left_b5ccpr_result + b5cc_left_b5ccpr_result) \/ (b5cc_bit_b5ccpr_result = 1 /\ b5cc_right_b5ccpr_result = S (b5cc_left_b5ccpr_result + b5cc_left_b5ccpr_result)))))))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.