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
∀ p. ∀ n. ∀ u. ∀ v. ∀ b. ∀ c. ∀ m. InversePrefix(p,n,u,v,n) → (∀ x. Lt(x,m + m) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) → (∀ x. Lt(x,m) → ∃ y. ∃ z. BetaAt(b,c,x + x,y) ∧ (BetaAt(b,c,S (x + x),z) ∧ BetaAt(u,v,y,z))) → ∃ x. ∃ y. (∀ z. ∀ k. Lt(z,m + m) → BetaAt(b,c,z,k) → BetaAt(x,y,z,S k)) ∧ (∀ z. ∀ k. ∀ i. Lt(z,m) → BetaAt(x,y,z + z,k) → BetaAt(x,y,S (z + z),i) → BalancedInverse(p,k,i))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
15 occurrences
In local proof propositions
3 occurrences
Exact expanded native-PA statement
forall p n u v b c m. (forall wip_index_wsl_inverse. (exists wip_gap_wsl_inverse_prefix_bound. wip_gap_wsl_inverse_prefix_bound + S wip_index_wsl_inverse = n) -> exists wip_mate_wsl_inverse. ((((exists wip_beta_height_wsl_inverse_decoded. wip_beta_height_wsl_inverse_decoded + S (wip_mate_wsl_inverse) = S ((S (wip_index_wsl_inverse)) * v)) /\ exists wip_beta_quotient_wsl_inverse_decoded. u = wip_beta_quotient_wsl_inverse_decoded * S ((S (wip_index_wsl_inverse)) * v) + (wip_mate_wsl_inverse))) /\ ((exists wip_gap_wsl_inverse_inverse_index_bound. wip_gap_wsl_inverse_inverse_index_bound + S wip_index_wsl_inverse = n) /\ ((exists wip_gap_wsl_inverse_inverse_mate_bound. wip_gap_wsl_inverse_inverse_mate_bound + S wip_mate_wsl_inverse = n) /\ (exists wip_mod_left_wsl_inverse_inverse_mod wip_mod_right_wsl_inverse_inverse_mod. ((S wip_index_wsl_inverse) * S wip_mate_wsl_inverse) + p * wip_mod_left_wsl_inverse_inverse_mod = 1 + p * wip_mod_right_wsl_inverse_inverse_mod))))) -> (forall fom_index_wsl_bounded. (exists fom_gap_wsl_bounded_index_bound. fom_gap_wsl_bounded_index_bound + S (fom_index_wsl_bounded) = m + m) -> exists fom_value_wsl_bounded. ((((exists fom_beta_height_wsl_bounded_entry. fom_beta_height_wsl_bounded_entry + S (fom_value_wsl_bounded) = S ((S (fom_index_wsl_bounded)) * c)) /\ exists fom_beta_quotient_wsl_bounded_entry. b = fom_beta_quotient_wsl_bounded_entry * S ((S (fom_index_wsl_bounded)) * c) + (fom_value_wsl_bounded))) /\ (exists fom_gap_wsl_bounded_value_bound. fom_gap_wsl_bounded_value_bound + S (fom_value_wsl_bounded) = n))) -> (forall wpop_pair_wsl_pairs. (exists wpo_gap_wsl_pairs_pair_bound. wpo_gap_wsl_pairs_pair_bound + S (wpop_pair_wsl_pairs) = m) -> exists wpop_left_wsl_pairs wpop_right_wsl_pairs. ((((exists wpo_beta_height_wsl_pairs_left_entry. wpo_beta_height_wsl_pairs_left_entry + S (wpop_left_wsl_pairs) = S ((S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs)) * c)) /\ exists wpo_beta_quotient_wsl_pairs_left_entry. b = wpo_beta_quotient_wsl_pairs_left_entry * S ((S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs)) * c) + (wpop_left_wsl_pairs))) /\ ((((exists wpo_beta_height_wsl_pairs_right_entry. wpo_beta_height_wsl_pairs_right_entry + S (wpop_right_wsl_pairs) = S ((S (S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs))) * c)) /\ exists wpo_beta_quotient_wsl_pairs_right_entry. b = wpo_beta_quotient_wsl_pairs_right_entry * S ((S (S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs))) * c) + (wpop_right_wsl_pairs))) /\ (((exists wpo_beta_height_wsl_pairs_inverse_entry. wpo_beta_height_wsl_pairs_inverse_entry + S (wpop_right_wsl_pairs) = S ((S (wpop_left_wsl_pairs)) * v)) /\ exists wpo_beta_quotient_wsl_pairs_inverse_entry. u = wpo_beta_quotient_wsl_pairs_inverse_entry * S ((S (wpop_left_wsl_pairs)) * v) + (wpop_right_wsl_pairs)))))) -> (exists f g. ((forall wsl_index_wsl_lift wsl_value_wsl_lift. (exists wpo_gap_wsl_lift_bound. wpo_gap_wsl_lift_bound + S (wsl_index_wsl_lift) = m + m) -> (((exists wpo_beta_height_wsl_lift_source. wpo_beta_height_wsl_lift_source + S (wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * c)) /\ exists wpo_beta_quotient_wsl_lift_source. b = wpo_beta_quotient_wsl_lift_source * S ((S (wsl_index_wsl_lift)) * c) + (wsl_value_wsl_lift))) -> (((exists wpo_beta_height_wsl_lift_target. wpo_beta_height_wsl_lift_target + S (S wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * g)) /\ exists wpo_beta_quotient_wsl_lift_target. f = wpo_beta_quotient_wsl_lift_target * S ((S (wsl_index_wsl_lift)) * g) + (S wsl_value_wsl_lift)))) /\ (forall wpp_pair_wsl_adjacent wpp_left_wsl_adjacent wpp_right_wsl_adjacent. (exists wpp_gap_wsl_adjacent_pair_bound. wpp_gap_wsl_adjacent_pair_bound + S (wpp_pair_wsl_adjacent) = m) -> (((exists wpp_beta_height_wsl_adjacent_left_entry. wpp_beta_height_wsl_adjacent_left_entry + S (wpp_left_wsl_adjacent) = S ((S ((wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g)) /\ exists wpp_beta_quotient_wsl_adjacent_left_entry. f = wpp_beta_quotient_wsl_adjacent_left_entry * S ((S ((wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g) + (wpp_left_wsl_adjacent))) -> (((exists wpp_beta_height_wsl_adjacent_right_entry. wpp_beta_height_wsl_adjacent_right_entry + S (wpp_right_wsl_adjacent) = S ((S (S (wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g)) /\ exists wpp_beta_quotient_wsl_adjacent_right_entry. f = wpp_beta_quotient_wsl_adjacent_right_entry * S ((S (S (wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g) + (wpp_right_wsl_adjacent))) -> (exists wpp_mod_left_wsl_adjacent_pair_mod wpp_mod_right_wsl_adjacent_pair_mod. (wpp_left_wsl_adjacent * wpp_right_wsl_adjacent) + p * wpp_mod_left_wsl_adjacent_pair_mod = (1) + p * wpp_mod_right_wsl_adjacent_pair_mod))))Proof neighborhood
Direct theorem prerequisites
Direct 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 (2)
01Fix variables and assumptionsL1–10
02Establish hlift_existsL11–15
Establish this local claim before using it. It is not an additional assumption.
- L11
have hlift_exists : ∃ f. ∃ g. ∀ x. ∀ y. Lt(x,m + m) → BetaAt(b,c,x,y) → BetaAt(f,g,x,S y)Definitions: Lt(x,m + m)BetaAt(b,c,x,y)BetaAt(f,g,x,S y)Original native command in the exact edition - L12
specialize pair_order_successor_lift_exists b - L13
specialize pair_order_successor_lift_exists c - L14
specialize pair_order_successor_lift_exists m - L15
exact pair_order_successor_lift_exists
03Separate the logical casesL16–17
04Construct an explicit witnessL18–19
05Separate the logical casesL20–20
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L20
split
06Use earlier factsL21–30
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L21
exact hlift_exists_witness_witness - L22
specialize paired_successor_lift_adjacent_units p - L23
specialize paired_successor_lift_adjacent_units n - L24
specialize paired_successor_lift_adjacent_units u - L25
specialize paired_successor_lift_adjacent_units v - L26
specialize paired_successor_lift_adjacent_units b - L27
specialize paired_successor_lift_adjacent_units c - L28
specialize paired_successor_lift_adjacent_units x - L29
specialize paired_successor_lift_adjacent_units x1 - L30
specialize paired_successor_lift_adjacent_units m
Original defined command ledger · 35 lines
- 0001
intro p - 0002
intro n - 0003
intro u - 0004
intro v - 0005
intro b - 0006
intro c - 0007
intro m - 0008
intro hinverse - 0009
intro hbounded - 0010
intro hpairs - 0011
have hlift_exists : ∃ f. ∃ g. ∀ x. ∀ y. Lt(x,m + m) → BetaAt(b,c,x,y) → BetaAt(f,g,x,S y)Exact native replay line
have hlift_exists : exists f g. (forall wsl_index_wsl_lift wsl_value_wsl_lift. (exists wpo_gap_wsl_lift_bound. wpo_gap_wsl_lift_bound + S (wsl_index_wsl_lift) = m + m) -> (((exists wpo_beta_height_wsl_lift_source. wpo_beta_height_wsl_lift_source + S (wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * c)) /\ exists wpo_beta_quotient_wsl_lift_source. b = wpo_beta_quotient_wsl_lift_source * S ((S (wsl_index_wsl_lift)) * c) + (wsl_value_wsl_lift))) -> (((exists wpo_beta_height_wsl_lift_target. wpo_beta_height_wsl_lift_target + S (S wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * g)) /\ exists wpo_beta_quotient_wsl_lift_target. f = wpo_beta_quotient_wsl_lift_target * S ((S (wsl_index_wsl_lift)) * g) + (S wsl_value_wsl_lift)))) - 0012
specialize pair_order_successor_lift_exists b - 0013
specialize pair_order_successor_lift_exists c - 0014
specialize pair_order_successor_lift_exists m - 0015
exact pair_order_successor_lift_exists - 0016
cases hlift_exists - 0017
cases hlift_exists_witness - 0018
exists x - 0019
exists x1 - 0020
split - 0021
exact hlift_exists_witness_witness - 0022
specialize paired_successor_lift_adjacent_units p - 0023
specialize paired_successor_lift_adjacent_units n - 0024
specialize paired_successor_lift_adjacent_units u - 0025
specialize paired_successor_lift_adjacent_units v - 0026
specialize paired_successor_lift_adjacent_units b - 0027
specialize paired_successor_lift_adjacent_units c - 0028
specialize paired_successor_lift_adjacent_units x - 0029
specialize paired_successor_lift_adjacent_units x1 - 0030
specialize paired_successor_lift_adjacent_units m - 0031
apply paired_successor_lift_adjacent_units - 0032
exact hinverse - 0033
exact hbounded - 0034
exact hpairs - 0035
exact hlift_exists_witness_witness