PA00AY · theorem

paired_inverse_witness_append

Alpha v34 checked-use theorem · independently closed; not Stable

A two-entry append preserves every old inverse pair and adds the new one.

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

∀ u. ∀ v. ∀ b. ∀ c. ∀ z. ∀ d. ∀ m. ∀ i. ∀ j. (∀ x. Lt(x,m) → ∃ y. ∃ n. BetaAt(b,c,x + x,y) ∧ (BetaAt(b,c,S (x + x),n) ∧ BetaAt(u,v,y,n))) → BetaAt(z,d,m + m,i) ∧ (BetaAt(z,d,S (m + m),j) ∧ (∀ x. ∀ y. Lt(x,m + m) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y))) → BetaAt(u,v,i,j) → ∀ x. Lt(x,S m) → ∃ y. ∃ n. BetaAt(z,d,x + x,y) ∧ (BetaAt(z,d,S (x + x),n) ∧ BetaAt(u,v,y,n))

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

PD0002 Lt PD0013 BetaAt

14 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

10 occurrences

Exact expanded native-PA statement
forall u v b c z d m i j. (forall wpop_pair_wpop_old_pairs. (exists wpo_gap_wpop_old_pairs_pair_bound. wpo_gap_wpop_old_pairs_pair_bound + S (wpop_pair_wpop_old_pairs) = m) -> exists wpop_left_wpop_old_pairs wpop_right_wpop_old_pairs. ((((exists wpo_beta_height_wpop_old_pairs_left_entry. wpo_beta_height_wpop_old_pairs_left_entry + S (wpop_left_wpop_old_pairs) = S ((S (wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs)) * c)) /\ exists wpo_beta_quotient_wpop_old_pairs_left_entry. b = wpo_beta_quotient_wpop_old_pairs_left_entry * S ((S (wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs)) * c) + (wpop_left_wpop_old_pairs))) /\ ((((exists wpo_beta_height_wpop_old_pairs_right_entry. wpo_beta_height_wpop_old_pairs_right_entry + S (wpop_right_wpop_old_pairs) = S ((S (S (wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs))) * c)) /\ exists wpo_beta_quotient_wpop_old_pairs_right_entry. b = wpo_beta_quotient_wpop_old_pairs_right_entry * S ((S (S (wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs))) * c) + (wpop_right_wpop_old_pairs))) /\ (((exists wpo_beta_height_wpop_old_pairs_inverse_entry. wpo_beta_height_wpop_old_pairs_inverse_entry + S (wpop_right_wpop_old_pairs) = S ((S (wpop_left_wpop_old_pairs)) * v)) /\ exists wpo_beta_quotient_wpop_old_pairs_inverse_entry. u = wpo_beta_quotient_wpop_old_pairs_inverse_entry * S ((S (wpop_left_wpop_old_pairs)) * v) + (wpop_right_wpop_old_pairs)))))) -> (((((exists wpo_beta_height_wpop_append_trace_first. wpo_beta_height_wpop_append_trace_first + S (i) = S ((S (m + m)) * d)) /\ exists wpo_beta_quotient_wpop_append_trace_first. z = wpo_beta_quotient_wpop_append_trace_first * S ((S (m + m)) * d) + (i))) /\ ((((exists wpo_beta_height_wpop_append_trace_second. wpo_beta_height_wpop_append_trace_second + S (j) = S ((S (S (m + m))) * d)) /\ exists wpo_beta_quotient_wpop_append_trace_second. z = wpo_beta_quotient_wpop_append_trace_second * S ((S (S (m + m))) * d) + (j))) /\ (forall wpo_old_index_wpop_append_trace wpo_old_value_wpop_append_trace. (exists wpo_gap_wpop_append_trace_old_bound. wpo_gap_wpop_append_trace_old_bound + S (wpo_old_index_wpop_append_trace) = m + m) -> (((exists wpo_beta_height_wpop_append_trace_old_entry. wpo_beta_height_wpop_append_trace_old_entry + S (wpo_old_value_wpop_append_trace) = S ((S (wpo_old_index_wpop_append_trace)) * c)) /\ exists wpo_beta_quotient_wpop_append_trace_old_entry. b = wpo_beta_quotient_wpop_append_trace_old_entry * S ((S (wpo_old_index_wpop_append_trace)) * c) + (wpo_old_value_wpop_append_trace))) -> (((exists wpo_beta_height_wpop_append_trace_new_entry. wpo_beta_height_wpop_append_trace_new_entry + S (wpo_old_value_wpop_append_trace) = S ((S (wpo_old_index_wpop_append_trace)) * d)) /\ exists wpo_beta_quotient_wpop_append_trace_new_entry. z = wpo_beta_quotient_wpop_append_trace_new_entry * S ((S (wpo_old_index_wpop_append_trace)) * d) + (wpo_old_value_wpop_append_trace))))))) -> (((exists wpo_beta_height_wpop_inverse_edge. wpo_beta_height_wpop_inverse_edge + S (j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_wpop_inverse_edge. u = wpo_beta_quotient_wpop_inverse_edge * S ((S (i)) * v) + (j))) -> (forall wpop_pair_wpop_new_pairs. (exists wpo_gap_wpop_new_pairs_pair_bound. wpo_gap_wpop_new_pairs_pair_bound + S (wpop_pair_wpop_new_pairs) = S m) -> exists wpop_left_wpop_new_pairs wpop_right_wpop_new_pairs. ((((exists wpo_beta_height_wpop_new_pairs_left_entry. wpo_beta_height_wpop_new_pairs_left_entry + S (wpop_left_wpop_new_pairs) = S ((S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs)) * d)) /\ exists wpo_beta_quotient_wpop_new_pairs_left_entry. z = wpo_beta_quotient_wpop_new_pairs_left_entry * S ((S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs)) * d) + (wpop_left_wpop_new_pairs))) /\ ((((exists wpo_beta_height_wpop_new_pairs_right_entry. wpo_beta_height_wpop_new_pairs_right_entry + S (wpop_right_wpop_new_pairs) = S ((S (S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs))) * d)) /\ exists wpo_beta_quotient_wpop_new_pairs_right_entry. z = wpo_beta_quotient_wpop_new_pairs_right_entry * S ((S (S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs))) * d) + (wpop_right_wpop_new_pairs))) /\ (((exists wpo_beta_height_wpop_new_pairs_inverse_entry. wpo_beta_height_wpop_new_pairs_inverse_entry + S (wpop_right_wpop_new_pairs) = S ((S (wpop_left_wpop_new_pairs)) * v)) /\ exists wpo_beta_quotient_wpop_new_pairs_inverse_entry. u = wpo_beta_quotient_wpop_new_pairs_inverse_entry * S ((S (wpop_left_wpop_new_pairs)) * v) + (wpop_right_wpop_new_pairs))))))

Proof neighborhood

Direct theorem prerequisites

PA003D finite_lt_succ_eq_or_lt PA009Q pair_index_left_below_double PA009R pair_index_right_below_double

Direct theorem dependents

PA00B0 prime_pair_order_paired_state_step

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

75 script commands · 25 reading checkpoints · 7 local claims

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
finite lt succ eq or ltpair index left below doublepair index right below double
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro u
  2. L2
    intro v
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro z
  6. L6
    intro d
  7. L7
    intro m
  8. L8
    intro i
  9. L9
    intro j
  10. L10
    intro hold_pairs
02Fix variables and assumptionsL11–12

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro htrace
  2. L12
    intro hedge
03Separate the logical casesL13–14

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L13
    cases htrace
  2. L14
    cases htrace_right
04Fix variables and assumptionsL15–16

Work with arbitrary variables or the premises of the current implication.

  1. L15
    intro t
  2. L16
    intro ht
05Establish hsplitL17–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L17
    have hsplit : t = m ∨ Lt(t,m)Definitions: Lt(t,m)Original native command in the exact edition
  2. L18
    specialize finite_lt_succ_eq_or_lt m
  3. L19
    specialize finite_lt_succ_eq_or_lt t
  4. L20
    apply finite_lt_succ_eq_or_lt
  5. L21
    exact ht
06Separate the logical casesL22–22

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L22
    cases hsplit
07Establish hleft_positionL23–26

Establish this local claim before using it. It is not an additional assumption.

  1. L23
    have hleft_position : t + t = m + m
  2. L24
    rewrite hsplit_left
  3. L25
    rewrite hsplit_left
  4. L26
    refl
08Establish hright_positionL27–29

Establish this local claim before using it. It is not an additional assumption.

  1. L27
    have hright_position : S (t + t) = S (m + m)
  2. L28
    congr
  3. L29
    exact hleft_position
09Construct an explicit witnessL30–31

Supply the displayed value, then prove that it has the required property.

  1. L30
    exists i
  2. L31
    exists j
10Separate the logical casesL32–32

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L32
    split
11Calculate and transport equalitiesL33–34

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L33
    rewrite hleft_position
  2. L34
    rewrite hleft_position
12Use earlier factsL35–35

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L35
    exact htrace_left
13Separate the logical casesL36–36

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L36
    split
14Calculate and transport equalitiesL37–38

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L37
    rewrite hright_position
  2. L38
    rewrite hright_position
15Use earlier factsL39–40

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L39
    exact htrace_right_left
  2. L40
    exact hedge
16Establish holdL41–43

Establish this local claim before using it. It is not an additional assumption.

  1. L41
    have hold : ∀ wpop_pair_wpop_old_pairs. Lt(wpop_pair_wpop_old_pairs,m) → ∃ x. ∃ y. BetaAt(b,c,wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs,x) ∧ (BetaAt(b,c,S (wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs),y) ∧ BetaAt(u,v,x,y))Definitions: Lt(wpop_pair_wpop_old_pairs,m)BetaAt(b,c,wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs,x)BetaAt(b,c,S (wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs),y)BetaAt(u,v,x,y)Original native command in the exact edition
  2. L42
    exact hold_pairs
  3. L43
    specialize hold t
17Establish hold_atL44–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hold.

  1. L44
    have hold_at : ∃ oi. ∃ oj. BetaAt(b,c,t + t,oi) ∧ (BetaAt(b,c,S (t + t),oj) ∧ BetaAt(u,v,oi,oj))Definitions: BetaAt(b,c,t + t,oi)BetaAt(b,c,S (t + t),oj)BetaAt(u,v,oi,oj)Original native command in the exact edition
  2. L45
    apply hold
  3. L46
    exact hsplit_right
18Separate the logical casesL47–50

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L47
    cases hold_at
  2. L48
    cases hold_at_witness
  3. L49
    cases hold_at_witness_witness
  4. L50
    cases hold_at_witness_witness_right
19Establish hleft_boundL51–55

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair index left below double.

  1. L51
    have hleft_bound : Lt(t + t,m + m)Definitions: Lt(t + t,m + m)Original native command in the exact edition
  2. L52
    specialize pair_index_left_below_double t
  3. L53
    specialize pair_index_left_below_double m
  4. L54
    apply pair_index_left_below_double
  5. L55
    exact hsplit_right
20Establish hright_boundL56–60

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair index right below double.

  1. L56
    have hright_bound : Lt(S (t + t),m + m)Definitions: Lt(S (t + t),m + m)Original native command in the exact edition
  2. L57
    specialize pair_index_right_below_double t
  3. L58
    specialize pair_index_right_below_double m
  4. L59
    apply pair_index_right_below_double
  5. L60
    exact hsplit_right
21Construct an explicit witnessL61–62

Supply the displayed value, then prove that it has the required property.

  1. L61
    exists x
  2. L62
    exists x1
22Separate the logical casesL63–63

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L63
    split
23Use earlier factsL64–68

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L64
    specialize htrace_right_right (t + t)
  2. L65
    specialize htrace_right_right x
  3. L66
    apply htrace_right_right
  4. L67
    exact hleft_bound
  5. L68
    exact hold_at_witness_witness_left
24Separate the logical casesL69–69

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L69
    split
25Use earlier factsL70–75

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L70
    specialize htrace_right_right (S (t + t))
  2. L71
    specialize htrace_right_right x1
  3. L72
    apply htrace_right_right
  4. L73
    exact hright_bound
  5. L74
    exact hold_at_witness_witness_right_left
  6. L75
    exact hold_at_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 75 lines
  1. 0001intro u
  2. 0002intro v
  3. 0003intro b
  4. 0004intro c
  5. 0005intro z
  6. 0006intro d
  7. 0007intro m
  8. 0008intro i
  9. 0009intro j
  10. 0010intro hold_pairs
  11. 0011intro htrace
  12. 0012intro hedge
  13. 0013cases htrace
  14. 0014cases htrace_right
  15. 0015intro t
  16. 0016intro ht
  17. 0017have hsplit : t = m ∨ Lt(t,m)
    Exact native replay linehave hsplit : t = m \/ exists h. h + S t = m
  18. 0018specialize finite_lt_succ_eq_or_lt m
  19. 0019specialize finite_lt_succ_eq_or_lt t
  20. 0020apply finite_lt_succ_eq_or_lt
  21. 0021exact ht
  22. 0022cases hsplit
  23. 0023have hleft_position : t + t = m + m
  24. 0024rewrite hsplit_left
  25. 0025rewrite hsplit_left
  26. 0026refl
  27. 0027have hright_position : S (t + t) = S (m + m)
  28. 0028congr
  29. 0029exact hleft_position
  30. 0030exists i
  31. 0031exists j
  32. 0032split
  33. 0033rewrite hleft_position
  34. 0034rewrite hleft_position
  35. 0035exact htrace_left
  36. 0036split
  37. 0037rewrite hright_position
  38. 0038rewrite hright_position
  39. 0039exact htrace_right_left
  40. 0040exact hedge
  41. 0041have hold : ∀ wpop_pair_wpop_old_pairs. Lt(wpop_pair_wpop_old_pairs,m) → ∃ x. ∃ y. BetaAt(b,c,wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs,x) ∧ (BetaAt(b,c,S (wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs),y) ∧ BetaAt(u,v,x,y))
    Exact native replay linehave hold : forall wpop_pair_wpop_old_pairs. (exists wpo_gap_wpop_old_pairs_pair_bound. wpo_gap_wpop_old_pairs_pair_bound + S (wpop_pair_wpop_old_pairs) = m) -> exists wpop_left_wpop_old_pairs wpop_right_wpop_old_pairs. ((((exists wpo_beta_height_wpop_old_pairs_left_entry. wpo_beta_height_wpop_old_pairs_left_entry + S (wpop_left_wpop_old_pairs) = S ((S (wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs)) * c)) /\ exists wpo_beta_quotient_wpop_old_pairs_left_entry. b = wpo_beta_quotient_wpop_old_pairs_left_entry * S ((S (wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs)) * c) + (wpop_left_wpop_old_pairs))) /\ ((((exists wpo_beta_height_wpop_old_pairs_right_entry. wpo_beta_height_wpop_old_pairs_right_entry + S (wpop_right_wpop_old_pairs) = S ((S (S (wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs))) * c)) /\ exists wpo_beta_quotient_wpop_old_pairs_right_entry. b = wpo_beta_quotient_wpop_old_pairs_right_entry * S ((S (S (wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs))) * c) + (wpop_right_wpop_old_pairs))) /\ (((exists wpo_beta_height_wpop_old_pairs_inverse_entry. wpo_beta_height_wpop_old_pairs_inverse_entry + S (wpop_right_wpop_old_pairs) = S ((S (wpop_left_wpop_old_pairs)) * v)) /\ exists wpo_beta_quotient_wpop_old_pairs_inverse_entry. u = wpo_beta_quotient_wpop_old_pairs_inverse_entry * S ((S (wpop_left_wpop_old_pairs)) * v) + (wpop_right_wpop_old_pairs)))))
  42. 0042exact hold_pairs
  43. 0043specialize hold t
  44. 0044have hold_at : ∃ oi. ∃ oj. BetaAt(b,c,t + t,oi) ∧ (BetaAt(b,c,S (t + t),oj) ∧ BetaAt(u,v,oi,oj))
    Exact native replay linehave hold_at : exists oi oj. ((((exists wpo_beta_height_wpop_old_left_at_t. wpo_beta_height_wpop_old_left_at_t + S (oi) = S ((S (t + t)) * c)) /\ exists wpo_beta_quotient_wpop_old_left_at_t. b = wpo_beta_quotient_wpop_old_left_at_t * S ((S (t + t)) * c) + (oi))) /\ ((((exists wpo_beta_height_wpop_old_right_at_t. wpo_beta_height_wpop_old_right_at_t + S (oj) = S ((S (S (t + t))) * c)) /\ exists wpo_beta_quotient_wpop_old_right_at_t. b = wpo_beta_quotient_wpop_old_right_at_t * S ((S (S (t + t))) * c) + (oj))) /\ (((exists wpo_beta_height_wpop_old_edge_at_t. wpo_beta_height_wpop_old_edge_at_t + S (oj) = S ((S (oi)) * v)) /\ exists wpo_beta_quotient_wpop_old_edge_at_t. u = wpo_beta_quotient_wpop_old_edge_at_t * S ((S (oi)) * v) + (oj)))))
  45. 0045apply hold
  46. 0046exact hsplit_right
  47. 0047cases hold_at
  48. 0048cases hold_at_witness
  49. 0049cases hold_at_witness_witness
  50. 0050cases hold_at_witness_witness_right
  51. 0051have hleft_bound : Lt(t + t,m + m)
    Exact native replay linehave hleft_bound : exists h. h + S (t + t) = m + m
  52. 0052specialize pair_index_left_below_double t
  53. 0053specialize pair_index_left_below_double m
  54. 0054apply pair_index_left_below_double
  55. 0055exact hsplit_right
  56. 0056have hright_bound : Lt(S (t + t),m + m)
    Exact native replay linehave hright_bound : exists h. h + S (S (t + t)) = m + m
  57. 0057specialize pair_index_right_below_double t
  58. 0058specialize pair_index_right_below_double m
  59. 0059apply pair_index_right_below_double
  60. 0060exact hsplit_right
  61. 0061exists x
  62. 0062exists x1
  63. 0063split
  64. 0064specialize htrace_right_right (t + t)
  65. 0065specialize htrace_right_right x
  66. 0066apply htrace_right_right
  67. 0067exact hleft_bound
  68. 0068exact hold_at_witness_witness_left
  69. 0069split
  70. 0070specialize htrace_right_right (S (t + t))
  71. 0071specialize htrace_right_right x1
  72. 0072apply htrace_right_right
  73. 0073exact hright_bound
  74. 0074exact hold_at_witness_witness_right_left
  75. 0075exact hold_at_witness_witness_right_right