PA00AY

paired_inverse_witness_append

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

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

Exact expanded 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))))))

Structural proof guide

Generated structural guide

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

Use the direct prerequisites finite_lt_succ_eq_or_lt, pair_index_left_below_double, pair_index_right_below_double as previously established PA formulas.

The proof proceeds by case analysis (7), intermediate claims (7), equality transport (6).

Referenced ingredients

PA003D finite_lt_succ_eq_or_lt PA009Q pair_index_left_below_double PA009R pair_index_right_below_double

Proof neighborhood

Direct dependencies

PA003D finite_lt_succ_eq_or_lt PA009Q pair_index_left_below_double PA009R pair_index_right_below_double

Direct dependents

PA00B0 prime_pair_order_paired_state_step

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  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 \/ 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 : 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 : 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 : 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 : 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