PA00B9 · theorem

beta_adjacent_unit_pairs_product_one

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

Adjacent inverse pairs multiply to one across an exact beta-coded even prefix.

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. ∀ b. ∀ c. ∀ m. ∀ Q. (∀ x. ∀ y. ∀ z. Lt(x,m) → BetaAt(b,c,x + x,y) → BetaAt(b,c,S (x + x),z) → BalancedInverse(p,y,z)) → Product(b,c,m + m,Q) → ModEq(p,Q,1)

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 PD0008 ModEq PD0013 BetaAt PD0014 Product PD0031 BalancedInverse

6 occurrences

In local proof propositions

PD0002 Lt PD0008 ModEq PD0013 BetaAt PD0014 Product PD0031 BalancedInverse

14 occurrences

Exact expanded native-PA statement
forall p b c m Q. (forall wpp_pair_pairs wpp_left_pairs wpp_right_pairs. (exists wpp_gap_pairs_pair_bound. wpp_gap_pairs_pair_bound + S (wpp_pair_pairs) = m) -> (((exists wpp_beta_height_pairs_left_entry. wpp_beta_height_pairs_left_entry + S (wpp_left_pairs) = S ((S ((wpp_pair_pairs + wpp_pair_pairs))) * c)) /\ exists wpp_beta_quotient_pairs_left_entry. b = wpp_beta_quotient_pairs_left_entry * S ((S ((wpp_pair_pairs + wpp_pair_pairs))) * c) + (wpp_left_pairs))) -> (((exists wpp_beta_height_pairs_right_entry. wpp_beta_height_pairs_right_entry + S (wpp_right_pairs) = S ((S (S (wpp_pair_pairs + wpp_pair_pairs))) * c)) /\ exists wpp_beta_quotient_pairs_right_entry. b = wpp_beta_quotient_pairs_right_entry * S ((S (S (wpp_pair_pairs + wpp_pair_pairs))) * c) + (wpp_right_pairs))) -> (exists wpp_mod_left_pairs_pair_mod wpp_mod_right_pairs_pair_mod. (wpp_left_pairs * wpp_right_pairs) + p * wpp_mod_left_pairs_pair_mod = (1) + p * wpp_mod_right_pairs_pair_mod)) -> (exists wpp_trace_code_pair_product wpp_trace_scale_pair_product. ((((exists wpp_beta_height_pair_product_start. wpp_beta_height_pair_product_start + S (1) = S ((S (0)) * wpp_trace_scale_pair_product)) /\ exists wpp_beta_quotient_pair_product_start. wpp_trace_code_pair_product = wpp_beta_quotient_pair_product_start * S ((S (0)) * wpp_trace_scale_pair_product) + (1))) /\ ((((exists wpp_beta_height_pair_product_terminal. wpp_beta_height_pair_product_terminal + S (Q) = S ((S (m + m)) * wpp_trace_scale_pair_product)) /\ exists wpp_beta_quotient_pair_product_terminal. wpp_trace_code_pair_product = wpp_beta_quotient_pair_product_terminal * S ((S (m + m)) * wpp_trace_scale_pair_product) + (Q))) /\ forall wpp_index_pair_product. (exists wpp_gap_pair_product_bound. wpp_gap_pair_product_bound + S (wpp_index_pair_product) = m + m) -> exists wpp_factor_pair_product wpp_prefix_pair_product wpp_successor_pair_product. ((((exists wpp_beta_height_pair_product_factor. wpp_beta_height_pair_product_factor + S (wpp_factor_pair_product) = S ((S (wpp_index_pair_product)) * c)) /\ exists wpp_beta_quotient_pair_product_factor. b = wpp_beta_quotient_pair_product_factor * S ((S (wpp_index_pair_product)) * c) + (wpp_factor_pair_product))) /\ ((((exists wpp_beta_height_pair_product_prefix. wpp_beta_height_pair_product_prefix + S (wpp_prefix_pair_product) = S ((S (wpp_index_pair_product)) * wpp_trace_scale_pair_product)) /\ exists wpp_beta_quotient_pair_product_prefix. wpp_trace_code_pair_product = wpp_beta_quotient_pair_product_prefix * S ((S (wpp_index_pair_product)) * wpp_trace_scale_pair_product) + (wpp_prefix_pair_product))) /\ ((((exists wpp_beta_height_pair_product_successor. wpp_beta_height_pair_product_successor + S (wpp_successor_pair_product) = S ((S (S (wpp_index_pair_product))) * wpp_trace_scale_pair_product)) /\ exists wpp_beta_quotient_pair_product_successor. wpp_trace_code_pair_product = wpp_beta_quotient_pair_product_successor * S ((S (S (wpp_index_pair_product))) * wpp_trace_scale_pair_product) + (wpp_successor_pair_product))) /\ wpp_successor_pair_product = wpp_prefix_pair_product * wpp_factor_pair_product)))))) -> (exists wpp_mod_left_pair_result wpp_mod_right_pair_result. (Q) + p * wpp_mod_left_pair_result = (1) + p * wpp_mod_right_pair_result)

Proof neighborhood

Direct theorem prerequisites

PA009Y beta_product_double_succ_decompose PA0049 beta_product_zero PA002O le_succ PA001A le_refl PA0023 mod_eq_refl PA004E mod_eq_mul PA000E add_succ_left PA000B mul_assoc PA000M one_mul

Direct theorem dependents

PA00BA paired_pair_order_product_one_exists

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

96 script commands · 16 reading checkpoints · 11 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 (8)
beta product double succ decomposebeta product zerole succle reflmod eq reflmod eq mulmul assocone mul
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
02Induction on mL4–7

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction m
  2. L5
    intro Q
  3. L6
    intro hpairs
  4. L7
    intro hproduct
03Establish hzeroL8–12

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

  1. L8
    have hzero : 0 + 0 = 0
  2. L9
    simp
  3. L10
    rewrite hzero at hproduct
  4. L11
    rewrite hzero at hproduct
  5. L12
    rewrite hzero at hproduct
04Establish hQL13–22

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

  1. L13
    have hQ : Q = 1
  2. L14
    specialize beta_product_zero b
  3. L15
    specialize beta_product_zero c
  4. L16
    specialize beta_product_zero Q
  5. L17
    apply beta_product_zero
  6. L18
    exact hproduct
  7. L19
    rewrite hQ
  8. L20
    specialize mod_eq_refl p
  9. L21
    specialize mod_eq_refl 1
  10. L22
    exact mod_eq_refl
05Fix variables and assumptionsL23–25

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

  1. L23
    intro Q
  2. L24
    intro hpairs
  3. L25
    intro hproduct
06Establish hdoubleL26–27

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

  1. L26
    have hdouble : S m + S m = S (S (m + m))
  2. L27
    simp [add_succ_left]
07Establish hdecompositionL28–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product double succ decompose.

  1. L28
    have hdecomposition : ∃ wpp_left_factor_successor_decomposition. ∃ wpp_right_factor_successor_decomposition. ∃ wpp_prefix_product_successor_decomposition. BetaAt(b,c,m + m,wpp_left_factor_successor_decomposition) ∧ (BetaAt(b,c,S (m + m),wpp_right_factor_successor_decomposition) ∧ (Product(b,c,m + m,wpp_prefix_product_successor_decomposition) ∧ Q = wpp_prefix_product_successor_decomposition · wpp_left_factor_successor_decomposition · wpp_right_factor_successor_decomposition))Definitions: BetaAt(b,c,m + m,wpp_left_factor_successor_decomposition)BetaAt(b,c,S (m + m),wpp_right_factor_successor_decomposition)Product(b,c,m + m,wpp_prefix_product_successor_decomposition)Original native command in the exact edition
  2. L29
    specialize beta_product_double_succ_decompose b
  3. L30
    specialize beta_product_double_succ_decompose c
  4. L31
    specialize beta_product_double_succ_decompose (m + m)
  5. L32
    specialize beta_product_double_succ_decompose (S m + S m)
  6. L33
    specialize beta_product_double_succ_decompose Q
  7. L34
    apply beta_product_double_succ_decompose
  8. L35
    exact hdouble
  9. L36
    exact hproduct
08Separate the logical casesL37–42

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

  1. L37
    cases hdecomposition
  2. L38
    cases hdecomposition_witness
  3. L39
    cases hdecomposition_witness_witness
  4. L40
    cases hdecomposition_witness_witness_witness
  5. L41
    cases hdecomposition_witness_witness_witness_right
  6. L42
    cases hdecomposition_witness_witness_witness_right_right
09Establish hpairs_allL43–44

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

  1. L43
    have hpairs_all : ∀ wpp_pair_all_successor_pairs. ∀ wpp_left_all_successor_pairs. ∀ wpp_right_all_successor_pairs. Lt(wpp_pair_all_successor_pairs,S m) → BetaAt(b,c,wpp_pair_all_successor_pairs + wpp_pair_all_successor_pairs,wpp_left_all_successor_pairs) → BetaAt(b,c,S (wpp_pair_all_successor_pairs + wpp_pair_all_successor_pairs),wpp_right_all_successor_pairs) → BalancedInverse(p,wpp_left_all_successor_pairs,wpp_right_all_successor_pairs)Definitions: Lt(wpp_pair_all_successor_pairs,S m)BetaAt(b,c,wpp_pair_all_successor_pairs + wpp_pair_all_successor_pairs,wpp_left_all_successor_pairs)BetaAt(b,c,S (wpp_pair_all_successor_pairs + wpp_pair_all_successor_pairs),wpp_right_all_successor_pairs)BalancedInverse(p,wpp_left_all_successor_pairs,wpp_right_all_successor_pairs)Original native command in the exact edition
  2. L44
    exact hpairs
10Establish hpairs_prefixL45–54

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

  1. L45
    have hpairs_prefix : ∀ wpp_pair_prefix_pairs. ∀ wpp_left_prefix_pairs. ∀ wpp_right_prefix_pairs. Lt(wpp_pair_prefix_pairs,m) → BetaAt(b,c,wpp_pair_prefix_pairs + wpp_pair_prefix_pairs,wpp_left_prefix_pairs) → BetaAt(b,c,S (wpp_pair_prefix_pairs + wpp_pair_prefix_pairs),wpp_right_prefix_pairs) → BalancedInverse(p,wpp_left_prefix_pairs,wpp_right_prefix_pairs)Definitions: Lt(wpp_pair_prefix_pairs,m)BetaAt(b,c,wpp_pair_prefix_pairs + wpp_pair_prefix_pairs,wpp_left_prefix_pairs)BetaAt(b,c,S (wpp_pair_prefix_pairs + wpp_pair_prefix_pairs),wpp_right_prefix_pairs)BalancedInverse(p,wpp_left_prefix_pairs,wpp_right_prefix_pairs)Original native command in the exact edition
  2. L46
    intro t
  3. L47
    intro a
  4. L48
    intro d
  5. L49
    intro ht
  6. L50
    intro ha
  7. L51
    intro hd
  8. L52
    specialize hpairs_all t
  9. L53
    specialize hpairs_all a
  10. L54
    specialize hpairs_all d
11Use earlier factsL55–61

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

  1. L55
    apply hpairs_all
  2. L56
    specialize le_succ (S t)
  3. L57
    specialize le_succ m
  4. L58
    apply le_succ
  5. L59
    exact ht
  6. L60
    exact ha
  7. L61
    exact hd
12Establish hprefixL62–66

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

  1. L62
    have hprefix : ModEq(p,x2,1)Definitions: ModEq(p,x2,1)Original native command in the exact edition
  2. L63
    specialize IH x2
  3. L64
    apply IH
  4. L65
    exact hpairs_prefix
  5. L66
    exact hdecomposition_witness_witness_witness_right_right_left
13Establish hlastL67–75

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

  1. L67
    have hlast : BalancedInverse(p,x,x1)Definitions: BalancedInverse(p,x,x1)Original native command in the exact edition
  2. L68
    specialize hpairs m
  3. L69
    specialize hpairs x
  4. L70
    specialize hpairs x1
  5. L71
    apply hpairs
  6. L72
    specialize le_refl (S m)
  7. L73
    exact le_refl
  8. L74
    exact hdecomposition_witness_witness_witness_left
  9. L75
    exact hdecomposition_witness_witness_witness_right_left
14Establish hfoldL76–84

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

  1. L76
    have hfold : ModEq(p,x2 · (x · x1),1 · 1)Definitions: ModEq(p,x2 · (x · x1),1 · 1)Original native command in the exact edition
  2. L77
    specialize mod_eq_mul p
  3. L78
    specialize mod_eq_mul x2
  4. L79
    specialize mod_eq_mul 1
  5. L80
    specialize mod_eq_mul (x * x1)
  6. L81
    specialize mod_eq_mul 1
  7. L82
    apply mod_eq_mul
  8. L83
    exact hprefix
  9. L84
    exact hlast
15Establish honeL85–88

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

  1. L85
    have hone : 1 * 1 = 1
  2. L86
    specialize one_mul 1
  3. L87
    exact one_mul
  4. L88
    rewrite hone at hfold
16Establish hassocL89–96

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

  1. L89
    have hassoc : (x2 * x) * x1 = x2 * (x * x1)
  2. L90
    specialize mul_assoc x2
  3. L91
    specialize mul_assoc x
  4. L92
    specialize mul_assoc x1
  5. L93
    exact mul_assoc
  6. L94
    rewrite hdecomposition_witness_witness_witness_right_right_right
  7. L95
    rewrite hassoc
  8. L96
    exact hfold

Library-wide reading audit

Original defined command ledger · 96 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004induction m
  5. 0005intro Q
  6. 0006intro hpairs
  7. 0007intro hproduct
  8. 0008have hzero : 0 + 0 = 0
  9. 0009simp
  10. 0010rewrite hzero at hproduct
  11. 0011rewrite hzero at hproduct
  12. 0012rewrite hzero at hproduct
  13. 0013have hQ : Q = 1
  14. 0014specialize beta_product_zero b
  15. 0015specialize beta_product_zero c
  16. 0016specialize beta_product_zero Q
  17. 0017apply beta_product_zero
  18. 0018exact hproduct
  19. 0019rewrite hQ
  20. 0020specialize mod_eq_refl p
  21. 0021specialize mod_eq_refl 1
  22. 0022exact mod_eq_refl
  23. 0023intro Q
  24. 0024intro hpairs
  25. 0025intro hproduct
  26. 0026have hdouble : S m + S m = S (S (m + m))
  27. 0027simp [add_succ_left]
  28. 0028have hdecomposition : ∃ wpp_left_factor_successor_decomposition. ∃ wpp_right_factor_successor_decomposition. ∃ wpp_prefix_product_successor_decomposition. BetaAt(b,c,m + m,wpp_left_factor_successor_decomposition) ∧ (BetaAt(b,c,S (m + m),wpp_right_factor_successor_decomposition) ∧ (Product(b,c,m + m,wpp_prefix_product_successor_decomposition) ∧ Q = wpp_prefix_product_successor_decomposition · wpp_left_factor_successor_decomposition · wpp_right_factor_successor_decomposition))
    Exact native replay linehave hdecomposition : exists wpp_left_factor_successor_decomposition wpp_right_factor_successor_decomposition wpp_prefix_product_successor_decomposition. (((exists wpp_beta_height_successor_decomposition_left_entry. wpp_beta_height_successor_decomposition_left_entry + S (wpp_left_factor_successor_decomposition) = S ((S (m + m)) * c)) /\ exists wpp_beta_quotient_successor_decomposition_left_entry. b = wpp_beta_quotient_successor_decomposition_left_entry * S ((S (m + m)) * c) + (wpp_left_factor_successor_decomposition))) /\ ((((exists wpp_beta_height_successor_decomposition_right_entry. wpp_beta_height_successor_decomposition_right_entry + S (wpp_right_factor_successor_decomposition) = S ((S (S (m + m))) * c)) /\ exists wpp_beta_quotient_successor_decomposition_right_entry. b = wpp_beta_quotient_successor_decomposition_right_entry * S ((S (S (m + m))) * c) + (wpp_right_factor_successor_decomposition))) /\ ((exists wpp_trace_code_successor_decomposition_prefix wpp_trace_scale_successor_decomposition_prefix. ((((exists wpp_beta_height_successor_decomposition_prefix_start. wpp_beta_height_successor_decomposition_prefix_start + S (1) = S ((S (0)) * wpp_trace_scale_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_successor_decomposition_prefix_start. wpp_trace_code_successor_decomposition_prefix = wpp_beta_quotient_successor_decomposition_prefix_start * S ((S (0)) * wpp_trace_scale_successor_decomposition_prefix) + (1))) /\ ((((exists wpp_beta_height_successor_decomposition_prefix_terminal. wpp_beta_height_successor_decomposition_prefix_terminal + S (wpp_prefix_product_successor_decomposition) = S ((S (m + m)) * wpp_trace_scale_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_successor_decomposition_prefix_terminal. wpp_trace_code_successor_decomposition_prefix = wpp_beta_quotient_successor_decomposition_prefix_terminal * S ((S (m + m)) * wpp_trace_scale_successor_decomposition_prefix) + (wpp_prefix_product_successor_decomposition))) /\ forall wpp_index_successor_decomposition_prefix. (exists wpp_gap_successor_decomposition_prefix_bound. wpp_gap_successor_decomposition_prefix_bound + S (wpp_index_successor_decomposition_prefix) = m + m) -> exists wpp_factor_successor_decomposition_prefix wpp_prefix_successor_decomposition_prefix wpp_successor_successor_decomposition_prefix. ((((exists wpp_beta_height_successor_decomposition_prefix_factor. wpp_beta_height_successor_decomposition_prefix_factor + S (wpp_factor_successor_decomposition_prefix) = S ((S (wpp_index_successor_decomposition_prefix)) * c)) /\ exists wpp_beta_quotient_successor_decomposition_prefix_factor. b = wpp_beta_quotient_successor_decomposition_prefix_factor * S ((S (wpp_index_successor_decomposition_prefix)) * c) + (wpp_factor_successor_decomposition_prefix))) /\ ((((exists wpp_beta_height_successor_decomposition_prefix_prefix. wpp_beta_height_successor_decomposition_prefix_prefix + S (wpp_prefix_successor_decomposition_prefix) = S ((S (wpp_index_successor_decomposition_prefix)) * wpp_trace_scale_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_successor_decomposition_prefix_prefix. wpp_trace_code_successor_decomposition_prefix = wpp_beta_quotient_successor_decomposition_prefix_prefix * S ((S (wpp_index_successor_decomposition_prefix)) * wpp_trace_scale_successor_decomposition_prefix) + (wpp_prefix_successor_decomposition_prefix))) /\ ((((exists wpp_beta_height_successor_decomposition_prefix_successor. wpp_beta_height_successor_decomposition_prefix_successor + S (wpp_successor_successor_decomposition_prefix) = S ((S (S (wpp_index_successor_decomposition_prefix))) * wpp_trace_scale_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_successor_decomposition_prefix_successor. wpp_trace_code_successor_decomposition_prefix = wpp_beta_quotient_successor_decomposition_prefix_successor * S ((S (S (wpp_index_successor_decomposition_prefix))) * wpp_trace_scale_successor_decomposition_prefix) + (wpp_successor_successor_decomposition_prefix))) /\ wpp_successor_successor_decomposition_prefix = wpp_prefix_successor_decomposition_prefix * wpp_factor_successor_decomposition_prefix)))))) /\ Q = (wpp_prefix_product_successor_decomposition * wpp_left_factor_successor_decomposition) * wpp_right_factor_successor_decomposition))
  29. 0029specialize beta_product_double_succ_decompose b
  30. 0030specialize beta_product_double_succ_decompose c
  31. 0031specialize beta_product_double_succ_decompose (m + m)
  32. 0032specialize beta_product_double_succ_decompose (S m + S m)
  33. 0033specialize beta_product_double_succ_decompose Q
  34. 0034apply beta_product_double_succ_decompose
  35. 0035exact hdouble
  36. 0036exact hproduct
  37. 0037cases hdecomposition
  38. 0038cases hdecomposition_witness
  39. 0039cases hdecomposition_witness_witness
  40. 0040cases hdecomposition_witness_witness_witness
  41. 0041cases hdecomposition_witness_witness_witness_right
  42. 0042cases hdecomposition_witness_witness_witness_right_right
  43. 0043have hpairs_all : ∀ wpp_pair_all_successor_pairs. ∀ wpp_left_all_successor_pairs. ∀ wpp_right_all_successor_pairs. Lt(wpp_pair_all_successor_pairs,S m) → BetaAt(b,c,wpp_pair_all_successor_pairs + wpp_pair_all_successor_pairs,wpp_left_all_successor_pairs) → BetaAt(b,c,S (wpp_pair_all_successor_pairs + wpp_pair_all_successor_pairs),wpp_right_all_successor_pairs) → BalancedInverse(p,wpp_left_all_successor_pairs,wpp_right_all_successor_pairs)
    Exact native replay linehave hpairs_all : forall wpp_pair_all_successor_pairs wpp_left_all_successor_pairs wpp_right_all_successor_pairs. (exists wpp_gap_all_successor_pairs_pair_bound. wpp_gap_all_successor_pairs_pair_bound + S (wpp_pair_all_successor_pairs) = S m) -> (((exists wpp_beta_height_all_successor_pairs_left_entry. wpp_beta_height_all_successor_pairs_left_entry + S (wpp_left_all_successor_pairs) = S ((S ((wpp_pair_all_successor_pairs + wpp_pair_all_successor_pairs))) * c)) /\ exists wpp_beta_quotient_all_successor_pairs_left_entry. b = wpp_beta_quotient_all_successor_pairs_left_entry * S ((S ((wpp_pair_all_successor_pairs + wpp_pair_all_successor_pairs))) * c) + (wpp_left_all_successor_pairs))) -> (((exists wpp_beta_height_all_successor_pairs_right_entry. wpp_beta_height_all_successor_pairs_right_entry + S (wpp_right_all_successor_pairs) = S ((S (S (wpp_pair_all_successor_pairs + wpp_pair_all_successor_pairs))) * c)) /\ exists wpp_beta_quotient_all_successor_pairs_right_entry. b = wpp_beta_quotient_all_successor_pairs_right_entry * S ((S (S (wpp_pair_all_successor_pairs + wpp_pair_all_successor_pairs))) * c) + (wpp_right_all_successor_pairs))) -> (exists wpp_mod_left_all_successor_pairs_pair_mod wpp_mod_right_all_successor_pairs_pair_mod. (wpp_left_all_successor_pairs * wpp_right_all_successor_pairs) + p * wpp_mod_left_all_successor_pairs_pair_mod = (1) + p * wpp_mod_right_all_successor_pairs_pair_mod)
  44. 0044exact hpairs
  45. 0045have hpairs_prefix : ∀ wpp_pair_prefix_pairs. ∀ wpp_left_prefix_pairs. ∀ wpp_right_prefix_pairs. Lt(wpp_pair_prefix_pairs,m) → BetaAt(b,c,wpp_pair_prefix_pairs + wpp_pair_prefix_pairs,wpp_left_prefix_pairs) → BetaAt(b,c,S (wpp_pair_prefix_pairs + wpp_pair_prefix_pairs),wpp_right_prefix_pairs) → BalancedInverse(p,wpp_left_prefix_pairs,wpp_right_prefix_pairs)
    Exact native replay linehave hpairs_prefix : forall wpp_pair_prefix_pairs wpp_left_prefix_pairs wpp_right_prefix_pairs. (exists wpp_gap_prefix_pairs_pair_bound. wpp_gap_prefix_pairs_pair_bound + S (wpp_pair_prefix_pairs) = m) -> (((exists wpp_beta_height_prefix_pairs_left_entry. wpp_beta_height_prefix_pairs_left_entry + S (wpp_left_prefix_pairs) = S ((S ((wpp_pair_prefix_pairs + wpp_pair_prefix_pairs))) * c)) /\ exists wpp_beta_quotient_prefix_pairs_left_entry. b = wpp_beta_quotient_prefix_pairs_left_entry * S ((S ((wpp_pair_prefix_pairs + wpp_pair_prefix_pairs))) * c) + (wpp_left_prefix_pairs))) -> (((exists wpp_beta_height_prefix_pairs_right_entry. wpp_beta_height_prefix_pairs_right_entry + S (wpp_right_prefix_pairs) = S ((S (S (wpp_pair_prefix_pairs + wpp_pair_prefix_pairs))) * c)) /\ exists wpp_beta_quotient_prefix_pairs_right_entry. b = wpp_beta_quotient_prefix_pairs_right_entry * S ((S (S (wpp_pair_prefix_pairs + wpp_pair_prefix_pairs))) * c) + (wpp_right_prefix_pairs))) -> (exists wpp_mod_left_prefix_pairs_pair_mod wpp_mod_right_prefix_pairs_pair_mod. (wpp_left_prefix_pairs * wpp_right_prefix_pairs) + p * wpp_mod_left_prefix_pairs_pair_mod = (1) + p * wpp_mod_right_prefix_pairs_pair_mod)
  46. 0046intro t
  47. 0047intro a
  48. 0048intro d
  49. 0049intro ht
  50. 0050intro ha
  51. 0051intro hd
  52. 0052specialize hpairs_all t
  53. 0053specialize hpairs_all a
  54. 0054specialize hpairs_all d
  55. 0055apply hpairs_all
  56. 0056specialize le_succ (S t)
  57. 0057specialize le_succ m
  58. 0058apply le_succ
  59. 0059exact ht
  60. 0060exact ha
  61. 0061exact hd
  62. 0062have hprefix : ModEq(p,x2,1)
    Exact native replay linehave hprefix : exists wpp_mod_left_prefix_congruence wpp_mod_right_prefix_congruence. (x2) + p * wpp_mod_left_prefix_congruence = (1) + p * wpp_mod_right_prefix_congruence
  63. 0063specialize IH x2
  64. 0064apply IH
  65. 0065exact hpairs_prefix
  66. 0066exact hdecomposition_witness_witness_witness_right_right_left
  67. 0067have hlast : BalancedInverse(p,x,x1)
    Exact native replay linehave hlast : exists wpp_mod_left_last_pair_congruence wpp_mod_right_last_pair_congruence. (x * x1) + p * wpp_mod_left_last_pair_congruence = (1) + p * wpp_mod_right_last_pair_congruence
  68. 0068specialize hpairs m
  69. 0069specialize hpairs x
  70. 0070specialize hpairs x1
  71. 0071apply hpairs
  72. 0072specialize le_refl (S m)
  73. 0073exact le_refl
  74. 0074exact hdecomposition_witness_witness_witness_left
  75. 0075exact hdecomposition_witness_witness_witness_right_left
  76. 0076have hfold : ModEq(p,x2 · (x · x1),1 · 1)
    Exact native replay linehave hfold : exists wpp_mod_left_folded_congruence wpp_mod_right_folded_congruence. (x2 * (x * x1)) + p * wpp_mod_left_folded_congruence = (1 * 1) + p * wpp_mod_right_folded_congruence
  77. 0077specialize mod_eq_mul p
  78. 0078specialize mod_eq_mul x2
  79. 0079specialize mod_eq_mul 1
  80. 0080specialize mod_eq_mul (x * x1)
  81. 0081specialize mod_eq_mul 1
  82. 0082apply mod_eq_mul
  83. 0083exact hprefix
  84. 0084exact hlast
  85. 0085have hone : 1 * 1 = 1
  86. 0086specialize one_mul 1
  87. 0087exact one_mul
  88. 0088rewrite hone at hfold
  89. 0089have hassoc : (x2 * x) * x1 = x2 * (x * x1)
  90. 0090specialize mul_assoc x2
  91. 0091specialize mul_assoc x
  92. 0092specialize mul_assoc x1
  93. 0093exact mul_assoc
  94. 0094rewrite hdecomposition_witness_witness_witness_right_right_right
  95. 0095rewrite hassoc
  96. 0096exact hfold