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
∀ lb. ∀ lc. ∀ rb. ∀ rc. ∀ tb. ∀ tc. ∀ cb. ∀ cc. ∀ l. (∀ x. Lt(x,S l) → ∃ y. ∃ z. ∃ n. ∃ m. BetaAt(lb,lc,x,y) ∧ (BetaAt(rb,rc,x,z) ∧ (BetaAt(tb,tc,x,n) ∧ (BetaAt(cb,cc,x,m) ∧ (m = 0 ∧ n = y + z ∨ m = 1 ∧ n = S (y + z)))))) → ∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. ∃ m. BetaAt(lb,lc,x,y) ∧ (BetaAt(rb,rc,x,z) ∧ (BetaAt(tb,tc,x,n) ∧ (BetaAt(cb,cc,x,m) ∧ (m = 0 ∧ n = y + z ∨ m = 1 ∧ n = S (y + z)))))Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.
Definitions used by this theorem
In the theorem statement
In local proof propositions
none
Exact expanded first-order statement
forall lb lc rb rc tb tc cb cc l. (forall kmc_index_kmcpr_source. (exists bcf_lt_gap_kmcpr_source_bound. bcf_lt_gap_kmcpr_source_bound + S (kmc_index_kmcpr_source) = S l) -> exists kmc_left_kmcpr_source kmc_right_kmcpr_source kmc_total_kmcpr_source kmc_bit_kmcpr_source. (((exists fs_h_kmcpr_source_left. fs_h_kmcpr_source_left + S (kmc_left_kmcpr_source) = S ((S (kmc_index_kmcpr_source)) * lc)) /\ exists fs_q_kmcpr_source_left. lb = fs_q_kmcpr_source_left * S ((S (kmc_index_kmcpr_source)) * lc) + (kmc_left_kmcpr_source))) /\ ((((exists fs_h_kmcpr_source_right. fs_h_kmcpr_source_right + S (kmc_right_kmcpr_source) = S ((S (kmc_index_kmcpr_source)) * rc)) /\ exists fs_q_kmcpr_source_right. rb = fs_q_kmcpr_source_right * S ((S (kmc_index_kmcpr_source)) * rc) + (kmc_right_kmcpr_source))) /\ ((((exists fs_h_kmcpr_source_total. fs_h_kmcpr_source_total + S (kmc_total_kmcpr_source) = S ((S (kmc_index_kmcpr_source)) * tc)) /\ exists fs_q_kmcpr_source_total. tb = fs_q_kmcpr_source_total * S ((S (kmc_index_kmcpr_source)) * tc) + (kmc_total_kmcpr_source))) /\ ((((exists fs_h_kmcpr_source_bit. fs_h_kmcpr_source_bit + S (kmc_bit_kmcpr_source) = S ((S (kmc_index_kmcpr_source)) * cc)) /\ exists fs_q_kmcpr_source_bit. cb = fs_q_kmcpr_source_bit * S ((S (kmc_index_kmcpr_source)) * cc) + (kmc_bit_kmcpr_source))) /\ (((kmc_bit_kmcpr_source = 0 /\ kmc_total_kmcpr_source = kmc_left_kmcpr_source + kmc_right_kmcpr_source) \/ (kmc_bit_kmcpr_source = 1 /\ kmc_total_kmcpr_source = S (kmc_left_kmcpr_source + kmc_right_kmcpr_source)))))))) -> (forall kmc_index_kmcpr_result. (exists bcf_lt_gap_kmcpr_result_bound. bcf_lt_gap_kmcpr_result_bound + S (kmc_index_kmcpr_result) = l) -> exists kmc_left_kmcpr_result kmc_right_kmcpr_result kmc_total_kmcpr_result kmc_bit_kmcpr_result. (((exists fs_h_kmcpr_result_left. fs_h_kmcpr_result_left + S (kmc_left_kmcpr_result) = S ((S (kmc_index_kmcpr_result)) * lc)) /\ exists fs_q_kmcpr_result_left. lb = fs_q_kmcpr_result_left * S ((S (kmc_index_kmcpr_result)) * lc) + (kmc_left_kmcpr_result))) /\ ((((exists fs_h_kmcpr_result_right. fs_h_kmcpr_result_right + S (kmc_right_kmcpr_result) = S ((S (kmc_index_kmcpr_result)) * rc)) /\ exists fs_q_kmcpr_result_right. rb = fs_q_kmcpr_result_right * S ((S (kmc_index_kmcpr_result)) * rc) + (kmc_right_kmcpr_result))) /\ ((((exists fs_h_kmcpr_result_total. fs_h_kmcpr_result_total + S (kmc_total_kmcpr_result) = S ((S (kmc_index_kmcpr_result)) * tc)) /\ exists fs_q_kmcpr_result_total. tb = fs_q_kmcpr_result_total * S ((S (kmc_index_kmcpr_result)) * tc) + (kmc_total_kmcpr_result))) /\ ((((exists fs_h_kmcpr_result_bit. fs_h_kmcpr_result_bit + S (kmc_bit_kmcpr_result) = S ((S (kmc_index_kmcpr_result)) * cc)) /\ exists fs_q_kmcpr_result_bit. cb = fs_q_kmcpr_result_bit * S ((S (kmc_index_kmcpr_result)) * cc) + (kmc_bit_kmcpr_result))) /\ (((kmc_bit_kmcpr_result = 0 /\ kmc_total_kmcpr_result = kmc_left_kmcpr_result + kmc_right_kmcpr_result) \/ (kmc_bit_kmcpr_result = 1 /\ kmc_total_kmcpr_result = S (kmc_left_kmcpr_result + kmc_right_kmcpr_result))))))))Proof neighborhood
Direct theorem prerequisites
le_succ · Stable closed
Direct theorem dependents
Definition-aware tactic body
Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay 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.