PA00AB

paired_inverse_witness_zero

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

The adjacent inverse-pair witness invariant is vacuous at zero.

Exact expanded PA statement

forall u v b c. (forall wpop_pair_wpop_zero_pairs. (exists wpo_gap_wpop_zero_pairs_pair_bound. wpo_gap_wpop_zero_pairs_pair_bound + S (wpop_pair_wpop_zero_pairs) = 0) -> exists wpop_left_wpop_zero_pairs wpop_right_wpop_zero_pairs. ((((exists wpo_beta_height_wpop_zero_pairs_left_entry. wpo_beta_height_wpop_zero_pairs_left_entry + S (wpop_left_wpop_zero_pairs) = S ((S (wpop_pair_wpop_zero_pairs + wpop_pair_wpop_zero_pairs)) * c)) /\ exists wpo_beta_quotient_wpop_zero_pairs_left_entry. b = wpo_beta_quotient_wpop_zero_pairs_left_entry * S ((S (wpop_pair_wpop_zero_pairs + wpop_pair_wpop_zero_pairs)) * c) + (wpop_left_wpop_zero_pairs))) /\ ((((exists wpo_beta_height_wpop_zero_pairs_right_entry. wpo_beta_height_wpop_zero_pairs_right_entry + S (wpop_right_wpop_zero_pairs) = S ((S (S (wpop_pair_wpop_zero_pairs + wpop_pair_wpop_zero_pairs))) * c)) /\ exists wpo_beta_quotient_wpop_zero_pairs_right_entry. b = wpo_beta_quotient_wpop_zero_pairs_right_entry * S ((S (S (wpop_pair_wpop_zero_pairs + wpop_pair_wpop_zero_pairs))) * c) + (wpop_right_wpop_zero_pairs))) /\ (((exists wpo_beta_height_wpop_zero_pairs_inverse_entry. wpo_beta_height_wpop_zero_pairs_inverse_entry + S (wpop_right_wpop_zero_pairs) = S ((S (wpop_left_wpop_zero_pairs)) * v)) /\ exists wpo_beta_quotient_wpop_zero_pairs_inverse_entry. u = wpo_beta_quotient_wpop_zero_pairs_inverse_entry * S ((S (wpop_left_wpop_zero_pairs)) * v) + (wpop_right_wpop_zero_pairs))))))

Structural proof guide

Generated structural guide

The adjacent inverse-pair witness invariant is vacuous at zero.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (1).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero

Direct dependents

PA00B1 prime_pair_order_paired_iteration

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 t
  6. 0006intro ht
  7. 0007exfalso
  8. 0008cases ht
  9. 0009have hst : S t = 0
  10. 0010specialize add_eq_zero_right x
  11. 0011specialize add_eq_zero_right (S t)
  12. 0012apply add_eq_zero_right
  13. 0013exact ht_witness
  14. 0014specialize succ_ne_zero t
  15. 0015apply succ_ne_zero
  16. 0016exact hst