PA00BF · theorem

prime_terminal_range_two_product_mod_one_exists

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

Project the terminal PairOrder package to its canonical nonendpoint product modulo 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

∀ p. ∀ n. ∀ m. p = S n → Prime(p) → n = S S (m + m) → ∃ x. ∃ y. ∃ z. Range(x,y,2,m + m) ∧ (Product(x,y,m + m,z) ∧ ModEq(p,z,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

PD0004 Prime PD0008 ModEq PD0014 Product PD0018 Range

4 occurrences

In local proof propositions

PD0002 Lt PD0008 ModEq PD0013 BetaAt PD0014 Product PD0018 Range PD0025 InjectivePrefix PD0027 ContainsPrefix PD0031 BalancedInverse PD0037 InversePrefix

56 occurrences

Exact expanded native-PA statement
forall p n m. p = S n -> ((~(p = 1) /\ forall wip_prime_left_wer_shape_prime wip_prime_right_wer_shape_prime. p = wip_prime_left_wer_shape_prime * wip_prime_right_wer_shape_prime -> wip_prime_left_wer_shape_prime = 1 \/ wip_prime_right_wer_shape_prime = 1)) -> n = S (S (m + m)) -> (exists z d P. ((forall wtp_range_index_wer_terminal_range. (exists wtp_range_gap_wer_terminal_range. wtp_range_gap_wer_terminal_range + S wtp_range_index_wer_terminal_range = m + m) -> (((exists ff_h_wer_terminal_range_decoded. ff_h_wer_terminal_range_decoded + S (2 + wtp_range_index_wer_terminal_range) = S ((S (wtp_range_index_wer_terminal_range)) * d)) /\ exists ff_q_wer_terminal_range_decoded. z = ff_q_wer_terminal_range_decoded * S ((S (wtp_range_index_wer_terminal_range)) * d) + (2 + wtp_range_index_wer_terminal_range)))) /\ (((exists ff_u_wer_terminal_canonical_product ff_v_wer_terminal_canonical_product. ((((exists ff_h_wer_terminal_canonical_product_start. ff_h_wer_terminal_canonical_product_start + S (1) = S ((S (0)) * ff_v_wer_terminal_canonical_product)) /\ exists ff_q_wer_terminal_canonical_product_start. ff_u_wer_terminal_canonical_product = ff_q_wer_terminal_canonical_product_start * S ((S (0)) * ff_v_wer_terminal_canonical_product) + (1))) /\ ((((exists ff_h_wer_terminal_canonical_product_terminal. ff_h_wer_terminal_canonical_product_terminal + S (P) = S ((S (m + m)) * ff_v_wer_terminal_canonical_product)) /\ exists ff_q_wer_terminal_canonical_product_terminal. ff_u_wer_terminal_canonical_product = ff_q_wer_terminal_canonical_product_terminal * S ((S (m + m)) * ff_v_wer_terminal_canonical_product) + (P))) /\ forall ff_i_wer_terminal_canonical_product. (exists ff_lt_wer_terminal_canonical_product_bound. ff_lt_wer_terminal_canonical_product_bound + S ff_i_wer_terminal_canonical_product = m + m) -> exists ff_p_wer_terminal_canonical_product ff_r_wer_terminal_canonical_product ff_s_wer_terminal_canonical_product. ((((exists ff_h_wer_terminal_canonical_product_factor. ff_h_wer_terminal_canonical_product_factor + S (ff_p_wer_terminal_canonical_product) = S ((S (ff_i_wer_terminal_canonical_product)) * d)) /\ exists ff_q_wer_terminal_canonical_product_factor. z = ff_q_wer_terminal_canonical_product_factor * S ((S (ff_i_wer_terminal_canonical_product)) * d) + (ff_p_wer_terminal_canonical_product))) /\ ((((exists ff_h_wer_terminal_canonical_product_partial. ff_h_wer_terminal_canonical_product_partial + S (ff_r_wer_terminal_canonical_product) = S ((S (ff_i_wer_terminal_canonical_product)) * ff_v_wer_terminal_canonical_product)) /\ exists ff_q_wer_terminal_canonical_product_partial. ff_u_wer_terminal_canonical_product = ff_q_wer_terminal_canonical_product_partial * S ((S (ff_i_wer_terminal_canonical_product)) * ff_v_wer_terminal_canonical_product) + (ff_r_wer_terminal_canonical_product))) /\ ((((exists ff_h_wer_terminal_canonical_product_successor. ff_h_wer_terminal_canonical_product_successor + S (ff_s_wer_terminal_canonical_product) = S ((S (S ff_i_wer_terminal_canonical_product)) * ff_v_wer_terminal_canonical_product)) /\ exists ff_q_wer_terminal_canonical_product_successor. ff_u_wer_terminal_canonical_product = ff_q_wer_terminal_canonical_product_successor * S ((S (S ff_i_wer_terminal_canonical_product)) * ff_v_wer_terminal_canonical_product) + (ff_s_wer_terminal_canonical_product))) /\ ff_s_wer_terminal_canonical_product = ff_r_wer_terminal_canonical_product * ff_p_wer_terminal_canonical_product)))))) /\ (exists wpp_mod_left_wer_terminal_projection_mod wpp_mod_right_wer_terminal_projection_mod. (P) + p * wpp_mod_left_wer_terminal_projection_mod = (1) + p * wpp_mod_right_wer_terminal_projection_mod)))))

Proof neighborhood

Direct theorem prerequisites

PA00A7 prime_inverse_prefix_exists PA00BE prime_wilson_terminal_product_package_exists

Direct theorem dependents

PA00BJ prime_factorial_wilson_congruence

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

57 script commands · 14 reading checkpoints · 4 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 (2)
prime inverse prefix existsprime wilson terminal product package exists
01Fix variables and assumptionsL1–6

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro m
  4. L4
    intro hpn
  5. L5
    intro hp
  6. L6
    intro hterminal
02Establish hinverseL7–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime inverse prefix exists.

  1. L7
    have hinverse : ∃ u. ∃ v. InversePrefix(p,n,u,v,n)Definitions: InversePrefix(p,n,u,v,n)Original native command in the exact edition
  2. L8
    specialize prime_inverse_prefix_exists p
  3. L9
    specialize prime_inverse_prefix_exists n
  4. L10
    apply prime_inverse_prefix_exists
  5. L11
    exact hpn
  6. L12
    exact hp
03Separate the logical casesL13–14

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

  1. L13
    cases hinverse
  2. L14
    cases hinverse_witness
04Establish hpackageL15–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime wilson terminal product package exists.

  1. L15
    have hpackage · expand full local formula (755 characters)have hpackage : ∃ b. ∃ c. ∃ f. ∃ g. ∃ Q. ∃ z. ∃ d. ∃ P. (∀ y. ∀ k. ∀ i. Lt(y,m + m) → BetaAt(b,c,y,k) → BetaAt(x,x1,k,i) → ContainsPrefix(b,c,m + m,i)) ∧ ((∀ y. Lt(y,m + m) → ∃ k. BetaAt(b,c,y,k) ∧ Lt(k,n)) ∧ ((∀ y. ∀ k. Lt(y,m + m) → BetaAt(b,c,y,k) → ¬k = 0 ∧ ¬S k = n) ∧ InjectivePrefix(b,c,m + m))) ∧ ((∀ y. Lt(y,m) → ∃ k. ∃ i. BetaAt(b,c,y + y,k) ∧ (BetaAt(b,c,S (y + y),i) ∧ BetaAt(x,x1,k,i))) ∧ ((∀ y. Lt(y,S S (m + m)) → ¬y = 0 ∧ ¬S y = S S (m + m) → ContainsPrefix(b,c,m + m,y)) ∧ ((∀ y. ∀ k. Lt(y,m + m) → BetaAt(b,c,y,k) → BetaAt(f,g,y,S k)) ∧ ((∀ y. ∀ k. ∀ i. Lt(y,m) → BetaAt(f,g,y + y,k) → BetaAt(f,g,S (y + y),i) → BalancedInverse(p,k,i)) ∧ (Product(f,g,m + m,Q) ∧ (ModEq(p,Q,1) ∧ (Range(z,d,2,m + m) ∧ (Product(z,d,m + m,P) ∧ P = Q))))))))
    Definitions: Lt(y,m + m)BetaAt(b,c,y,k)BetaAt(x,x1,k,i)ContainsPrefix(b,c,m + m,i)Lt(k,n)InjectivePrefix(b,c,m + m)Lt(y,m)BetaAt(b,c,y + y,k)BetaAt(b,c,S (y + y),i)Lt(y,S S (m + m))ContainsPrefix(b,c,m + m,y)BetaAt(f,g,y,S k)BetaAt(f,g,y + y,k)BetaAt(f,g,S (y + y),i)BalancedInverse(p,k,i)Product(f,g,m + m,Q)ModEq(p,Q,1)Range(z,d,2,m + m)Product(z,d,m + m,P)Original native command in the exact edition
  2. L16
    specialize prime_wilson_terminal_product_package_exists p
  3. L17
    specialize prime_wilson_terminal_product_package_exists n
  4. L18
    specialize prime_wilson_terminal_product_package_exists x
  5. L19
    specialize prime_wilson_terminal_product_package_exists x1
  6. L20
    specialize prime_wilson_terminal_product_package_exists (S (m + m))
  7. L21
    specialize prime_wilson_terminal_product_package_exists m
  8. L22
    apply prime_wilson_terminal_product_package_exists
  9. L23
    exact hpn
  10. L24
    exact hp
05Use earlier factsL25–27

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

  1. L25
    exact hinverse_witness_witness
  2. L26
    exact hterminal
  3. L27
    exact hterminal
06Separate the logical casesL28–35

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

  1. L28
    cases hpackage
  2. L29
    cases hpackage_witness
  3. L30
    cases hpackage_witness_witness
  4. L31
    cases hpackage_witness_witness_witness
  5. L32
    cases hpackage_witness_witness_witness_witness
  6. L33
    cases hpackage_witness_witness_witness_witness_witness
  7. L34
    cases hpackage_witness_witness_witness_witness_witness_witness
  8. L35
    cases hpackage_witness_witness_witness_witness_witness_witness_witness
07Establish hpartsL36–37

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

  1. L36
    have hparts · expand full local formula (748 characters)have hparts : (∀ y. ∀ z. ∀ k. Lt(y,m + m) → BetaAt(x2,x3,y,z) → BetaAt(x,x1,z,k) → ContainsPrefix(x2,x3,m + m,k)) ∧ ((∀ y. Lt(y,m + m) → ∃ z. BetaAt(x2,x3,y,z) ∧ Lt(z,n)) ∧ ((∀ y. ∀ z. Lt(y,m + m) → BetaAt(x2,x3,y,z) → ¬z = 0 ∧ ¬S z = n) ∧ InjectivePrefix(x2,x3,m + m))) ∧ ((∀ y. Lt(y,m) → ∃ z. ∃ k. BetaAt(x2,x3,y + y,z) ∧ (BetaAt(x2,x3,S (y + y),k) ∧ BetaAt(x,x1,z,k))) ∧ ((∀ y. Lt(y,S S (m + m)) → ¬y = 0 ∧ ¬S y = S S (m + m) → ContainsPrefix(x2,x3,m + m,y)) ∧ ((∀ y. ∀ z. Lt(y,m + m) → BetaAt(x2,x3,y,z) → BetaAt(x4,x5,y,S z)) ∧ ((∀ y. ∀ z. ∀ k. Lt(y,m) → BetaAt(x4,x5,y + y,z) → BetaAt(x4,x5,S (y + y),k) → BalancedInverse(p,z,k)) ∧ (Product(x4,x5,m + m,x6) ∧ (ModEq(p,x6,1) ∧ (Range(x7,x8,2,m + m) ∧ (Product(x7,x8,m + m,x9) ∧ x9 = x6))))))))
    Definitions: Lt(y,m + m)BetaAt(x2,x3,y,z)BetaAt(x,x1,z,k)ContainsPrefix(x2,x3,m + m,k)Lt(z,n)InjectivePrefix(x2,x3,m + m)Lt(y,m)BetaAt(x2,x3,y + y,z)BetaAt(x2,x3,S (y + y),k)Lt(y,S S (m + m))ContainsPrefix(x2,x3,m + m,y)BetaAt(x4,x5,y,S z)BetaAt(x4,x5,y + y,z)BetaAt(x4,x5,S (y + y),k)BalancedInverse(p,z,k)Product(x4,x5,m + m,x6)ModEq(p,x6,1)Range(x7,x8,2,m + m)Product(x7,x8,m + m,x9)Original native command in the exact edition
  2. L37
    exact hpackage_witness_witness_witness_witness_witness_witness_witness_witness
08Separate the logical casesL38–46

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

  1. L38
    cases hparts
  2. L39
    cases hparts_right
  3. L40
    cases hparts_right_right
  4. L41
    cases hparts_right_right_right
  5. L42
    cases hparts_right_right_right_right
  6. L43
    cases hparts_right_right_right_right_right
  7. L44
    cases hparts_right_right_right_right_right_right
  8. L45
    cases hparts_right_right_right_right_right_right_right
  9. L46
    cases hparts_right_right_right_right_right_right_right_right
09Establish hmod_productL47–49

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

  1. L47
    have hmod_product : ModEq(p,x9,1)Definitions: ModEq(p,x9,1)Original native command in the exact edition
  2. L48
    rewrite hparts_right_right_right_right_right_right_right_right_right
  3. L49
    exact hparts_right_right_right_right_right_right_left
10Construct an explicit witnessL50–52

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

  1. L50
    exists x7
  2. L51
    exists x8
  3. L52
    exists x9
11Separate the logical casesL53–53

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

  1. L53
    split
12Use earlier factsL54–54

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

  1. L54
    exact hparts_right_right_right_right_right_right_right_left
13Separate the logical casesL55–55

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

  1. L55
    split
14Use earlier factsL56–57

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

  1. L56
    exact hparts_right_right_right_right_right_right_right_right_left
  2. L57
    exact hmod_product

Library-wide reading audit

Original defined command ledger · 57 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro m
  4. 0004intro hpn
  5. 0005intro hp
  6. 0006intro hterminal
  7. 0007have hinverse : ∃ u. ∃ v. InversePrefix(p,n,u,v,n)
    Exact native replay linehave hinverse : exists u v. (forall wip_index_wer_terminal_inverse. (exists wip_gap_wer_terminal_inverse_prefix_bound. wip_gap_wer_terminal_inverse_prefix_bound + S wip_index_wer_terminal_inverse = n) -> exists wip_mate_wer_terminal_inverse. ((((exists wip_beta_height_wer_terminal_inverse_decoded. wip_beta_height_wer_terminal_inverse_decoded + S (wip_mate_wer_terminal_inverse) = S ((S (wip_index_wer_terminal_inverse)) * v)) /\ exists wip_beta_quotient_wer_terminal_inverse_decoded. u = wip_beta_quotient_wer_terminal_inverse_decoded * S ((S (wip_index_wer_terminal_inverse)) * v) + (wip_mate_wer_terminal_inverse))) /\ ((exists wip_gap_wer_terminal_inverse_inverse_index_bound. wip_gap_wer_terminal_inverse_inverse_index_bound + S wip_index_wer_terminal_inverse = n) /\ ((exists wip_gap_wer_terminal_inverse_inverse_mate_bound. wip_gap_wer_terminal_inverse_inverse_mate_bound + S wip_mate_wer_terminal_inverse = n) /\ (exists wip_mod_left_wer_terminal_inverse_inverse_mod wip_mod_right_wer_terminal_inverse_inverse_mod. ((S wip_index_wer_terminal_inverse) * S wip_mate_wer_terminal_inverse) + p * wip_mod_left_wer_terminal_inverse_inverse_mod = 1 + p * wip_mod_right_wer_terminal_inverse_inverse_mod)))))
  8. 0008specialize prime_inverse_prefix_exists p
  9. 0009specialize prime_inverse_prefix_exists n
  10. 0010apply prime_inverse_prefix_exists
  11. 0011exact hpn
  12. 0012exact hp
  13. 0013cases hinverse
  14. 0014cases hinverse_witness
  15. 0015have hpackage : ∃ b. ∃ c. ∃ f. ∃ g. ∃ Q. ∃ z. ∃ d. ∃ P. (∀ y. ∀ k. ∀ i. Lt(y,m + m) → BetaAt(b,c,y,k) → BetaAt(x,x1,k,i) → ContainsPrefix(b,c,m + m,i)) ∧ ((∀ y. Lt(y,m + m) → ∃ k. BetaAt(b,c,y,k) ∧ Lt(k,n)) ∧ ((∀ y. ∀ k. Lt(y,m + m) → BetaAt(b,c,y,k) → ¬k = 0 ∧ ¬S k = n) ∧ InjectivePrefix(b,c,m + m))) ∧ ((∀ y. Lt(y,m) → ∃ k. ∃ i. BetaAt(b,c,y + y,k) ∧ (BetaAt(b,c,S (y + y),i) ∧ BetaAt(x,x1,k,i))) ∧ ((∀ y. Lt(y,S S (m + m)) → ¬y = 0 ∧ ¬S y = S S (m + m) → ContainsPrefix(b,c,m + m,y)) ∧ ((∀ y. ∀ k. Lt(y,m + m) → BetaAt(b,c,y,k) → BetaAt(f,g,y,S k)) ∧ ((∀ y. ∀ k. ∀ i. Lt(y,m) → BetaAt(f,g,y + y,k) → BetaAt(f,g,S (y + y),i) → BalancedInverse(p,k,i)) ∧ (Product(f,g,m + m,Q) ∧ (ModEq(p,Q,1) ∧ (Range(z,d,2,m + m) ∧ (Product(z,d,m + m,P) ∧ P = Q))))))))
    Exact native replay linehave hpackage : exists b c f g Q z d P. ((((forall wpo_position_wer_terminal_state_x_closed wpo_source_wer_terminal_state_x_closed wpo_mate_wer_terminal_state_x_closed. (exists wpo_gap_wer_terminal_state_x_closed_position_bound. wpo_gap_wer_terminal_state_x_closed_position_bound + S (wpo_position_wer_terminal_state_x_closed) = m + m) -> (((exists wpo_beta_height_wer_terminal_state_x_closed_source_entry. wpo_beta_height_wer_terminal_state_x_closed_source_entry + S (wpo_source_wer_terminal_state_x_closed) = S ((S (wpo_position_wer_terminal_state_x_closed)) * c)) /\ exists wpo_beta_quotient_wer_terminal_state_x_closed_source_entry. b = wpo_beta_quotient_wer_terminal_state_x_closed_source_entry * S ((S (wpo_position_wer_terminal_state_x_closed)) * c) + (wpo_source_wer_terminal_state_x_closed))) -> (((exists wpo_beta_height_wer_terminal_state_x_closed_inverse_entry. wpo_beta_height_wer_terminal_state_x_closed_inverse_entry + S (wpo_mate_wer_terminal_state_x_closed) = S ((S (wpo_source_wer_terminal_state_x_closed)) * x1)) /\ exists wpo_beta_quotient_wer_terminal_state_x_closed_inverse_entry. x = wpo_beta_quotient_wer_terminal_state_x_closed_inverse_entry * S ((S (wpo_source_wer_terminal_state_x_closed)) * x1) + (wpo_mate_wer_terminal_state_x_closed))) -> exists wpo_mate_position_wer_terminal_state_x_closed. ((exists wpo_gap_wer_terminal_state_x_closed_mate_bound. wpo_gap_wer_terminal_state_x_closed_mate_bound + S (wpo_mate_position_wer_terminal_state_x_closed) = m + m) /\ (((exists wpo_beta_height_wer_terminal_state_x_closed_mate_entry. wpo_beta_height_wer_terminal_state_x_closed_mate_entry + S (wpo_mate_wer_terminal_state_x_closed) = S ((S (wpo_mate_position_wer_terminal_state_x_closed)) * c)) /\ exists wpo_beta_quotient_wer_terminal_state_x_closed_mate_entry. b = wpo_beta_quotient_wer_terminal_state_x_closed_mate_entry * S ((S (wpo_mate_position_wer_terminal_state_x_closed)) * c) + (wpo_mate_wer_terminal_state_x_closed))))) /\ ((forall fom_index_wer_terminal_state_x_bounded. (exists fom_gap_wer_terminal_state_x_bounded_index_bound. fom_gap_wer_terminal_state_x_bounded_index_bound + S (fom_index_wer_terminal_state_x_bounded) = m + m) -> exists fom_value_wer_terminal_state_x_bounded. ((((exists fom_beta_height_wer_terminal_state_x_bounded_entry. fom_beta_height_wer_terminal_state_x_bounded_entry + S (fom_value_wer_terminal_state_x_bounded) = S ((S (fom_index_wer_terminal_state_x_bounded)) * c)) /\ exists fom_beta_quotient_wer_terminal_state_x_bounded_entry. b = fom_beta_quotient_wer_terminal_state_x_bounded_entry * S ((S (fom_index_wer_terminal_state_x_bounded)) * c) + (fom_value_wer_terminal_state_x_bounded))) /\ (exists fom_gap_wer_terminal_state_x_bounded_value_bound. fom_gap_wer_terminal_state_x_bounded_value_bound + S (fom_value_wer_terminal_state_x_bounded) = n))) /\ ((forall wpo_position_wer_terminal_state_x_nonendpoint wpo_value_wer_terminal_state_x_nonendpoint. (exists wpo_gap_wer_terminal_state_x_nonendpoint_position_bound. wpo_gap_wer_terminal_state_x_nonendpoint_position_bound + S (wpo_position_wer_terminal_state_x_nonendpoint) = m + m) -> (((exists wpo_beta_height_wer_terminal_state_x_nonendpoint_entry. wpo_beta_height_wer_terminal_state_x_nonendpoint_entry + S (wpo_value_wer_terminal_state_x_nonendpoint) = S ((S (wpo_position_wer_terminal_state_x_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wer_terminal_state_x_nonendpoint_entry. b = wpo_beta_quotient_wer_terminal_state_x_nonendpoint_entry * S ((S (wpo_position_wer_terminal_state_x_nonendpoint)) * c) + (wpo_value_wer_terminal_state_x_nonendpoint))) -> (~(wpo_value_wer_terminal_state_x_nonendpoint = 0) /\ ~((S wpo_value_wer_terminal_state_x_nonendpoint) = n))) /\ (forall wpo_injective_left_wer_terminal_state_x_injective wpo_injective_right_wer_terminal_state_x_injective wpo_injective_value_wer_terminal_state_x_injective. (exists wpo_gap_wer_terminal_state_x_injective_left_bound. wpo_gap_wer_terminal_state_x_injective_left_bound + S (wpo_injective_left_wer_terminal_state_x_injective) = m + m) -> (exists wpo_gap_wer_terminal_state_x_injective_right_bound. wpo_gap_wer_terminal_state_x_injective_right_bound + S (wpo_injective_right_wer_terminal_state_x_injective) = m + m) -> (((exists wpo_beta_height_wer_terminal_state_x_injective_left_entry. wpo_beta_height_wer_terminal_state_x_injective_left_entry + S (wpo_injective_value_wer_terminal_state_x_injective) = S ((S (wpo_injective_left_wer_terminal_state_x_injective)) * c)) /\ exists wpo_beta_quotient_wer_terminal_state_x_injective_left_entry. b = wpo_beta_quotient_wer_terminal_state_x_injective_left_entry * S ((S (wpo_injective_left_wer_terminal_state_x_injective)) * c) + (wpo_injective_value_wer_terminal_state_x_injective))) -> (((exists wpo_beta_height_wer_terminal_state_x_injective_right_entry. wpo_beta_height_wer_terminal_state_x_injective_right_entry + S (wpo_injective_value_wer_terminal_state_x_injective) = S ((S (wpo_injective_right_wer_terminal_state_x_injective)) * c)) /\ exists wpo_beta_quotient_wer_terminal_state_x_injective_right_entry. b = wpo_beta_quotient_wer_terminal_state_x_injective_right_entry * S ((S (wpo_injective_right_wer_terminal_state_x_injective)) * c) + (wpo_injective_value_wer_terminal_state_x_injective))) -> wpo_injective_left_wer_terminal_state_x_injective = wpo_injective_right_wer_terminal_state_x_injective))))) /\ (((forall wpop_pair_wer_terminal_history_x. (exists wpo_gap_wer_terminal_history_x_pair_bound. wpo_gap_wer_terminal_history_x_pair_bound + S (wpop_pair_wer_terminal_history_x) = m) -> exists wpop_left_wer_terminal_history_x wpop_right_wer_terminal_history_x. ((((exists wpo_beta_height_wer_terminal_history_x_left_entry. wpo_beta_height_wer_terminal_history_x_left_entry + S (wpop_left_wer_terminal_history_x) = S ((S (wpop_pair_wer_terminal_history_x + wpop_pair_wer_terminal_history_x)) * c)) /\ exists wpo_beta_quotient_wer_terminal_history_x_left_entry. b = wpo_beta_quotient_wer_terminal_history_x_left_entry * S ((S (wpop_pair_wer_terminal_history_x + wpop_pair_wer_terminal_history_x)) * c) + (wpop_left_wer_terminal_history_x))) /\ ((((exists wpo_beta_height_wer_terminal_history_x_right_entry. wpo_beta_height_wer_terminal_history_x_right_entry + S (wpop_right_wer_terminal_history_x) = S ((S (S (wpop_pair_wer_terminal_history_x + wpop_pair_wer_terminal_history_x))) * c)) /\ exists wpo_beta_quotient_wer_terminal_history_x_right_entry. b = wpo_beta_quotient_wer_terminal_history_x_right_entry * S ((S (S (wpop_pair_wer_terminal_history_x + wpop_pair_wer_terminal_history_x))) * c) + (wpop_right_wer_terminal_history_x))) /\ (((exists wpo_beta_height_wer_terminal_history_x_inverse_entry. wpo_beta_height_wer_terminal_history_x_inverse_entry + S (wpop_right_wer_terminal_history_x) = S ((S (wpop_left_wer_terminal_history_x)) * x1)) /\ exists wpo_beta_quotient_wer_terminal_history_x_inverse_entry. x = wpo_beta_quotient_wer_terminal_history_x_inverse_entry * S ((S (wpop_left_wer_terminal_history_x)) * x1) + (wpop_right_wer_terminal_history_x)))))) /\ (((forall s. (exists wpo_gap_wer_terminal_coverage_value_bound. wpo_gap_wer_terminal_coverage_value_bound + S (s) = S (S (m + m))) -> (~(s = 0) /\ ~((S s) = S (S (m + m)))) -> exists q. ((exists wpo_gap_wer_terminal_coverage_index_bound. wpo_gap_wer_terminal_coverage_index_bound + S (q) = m + m) /\ (((exists wpo_beta_height_wer_terminal_coverage_entry. wpo_beta_height_wer_terminal_coverage_entry + S (s) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_wer_terminal_coverage_entry. b = wpo_beta_quotient_wer_terminal_coverage_entry * S ((S (q)) * c) + (s))))) /\ (((forall wsl_index_wer_terminal_lift wsl_value_wer_terminal_lift. (exists wpo_gap_wer_terminal_lift_bound. wpo_gap_wer_terminal_lift_bound + S (wsl_index_wer_terminal_lift) = m + m) -> (((exists wpo_beta_height_wer_terminal_lift_source. wpo_beta_height_wer_terminal_lift_source + S (wsl_value_wer_terminal_lift) = S ((S (wsl_index_wer_terminal_lift)) * c)) /\ exists wpo_beta_quotient_wer_terminal_lift_source. b = wpo_beta_quotient_wer_terminal_lift_source * S ((S (wsl_index_wer_terminal_lift)) * c) + (wsl_value_wer_terminal_lift))) -> (((exists wpo_beta_height_wer_terminal_lift_target. wpo_beta_height_wer_terminal_lift_target + S (S wsl_value_wer_terminal_lift) = S ((S (wsl_index_wer_terminal_lift)) * g)) /\ exists wpo_beta_quotient_wer_terminal_lift_target. f = wpo_beta_quotient_wer_terminal_lift_target * S ((S (wsl_index_wer_terminal_lift)) * g) + (S wsl_value_wer_terminal_lift)))) /\ (((forall wpp_pair_wer_terminal_adjacent wpp_left_wer_terminal_adjacent wpp_right_wer_terminal_adjacent. (exists wpp_gap_wer_terminal_adjacent_pair_bound. wpp_gap_wer_terminal_adjacent_pair_bound + S (wpp_pair_wer_terminal_adjacent) = m) -> (((exists wpp_beta_height_wer_terminal_adjacent_left_entry. wpp_beta_height_wer_terminal_adjacent_left_entry + S (wpp_left_wer_terminal_adjacent) = S ((S ((wpp_pair_wer_terminal_adjacent + wpp_pair_wer_terminal_adjacent))) * g)) /\ exists wpp_beta_quotient_wer_terminal_adjacent_left_entry. f = wpp_beta_quotient_wer_terminal_adjacent_left_entry * S ((S ((wpp_pair_wer_terminal_adjacent + wpp_pair_wer_terminal_adjacent))) * g) + (wpp_left_wer_terminal_adjacent))) -> (((exists wpp_beta_height_wer_terminal_adjacent_right_entry. wpp_beta_height_wer_terminal_adjacent_right_entry + S (wpp_right_wer_terminal_adjacent) = S ((S (S (wpp_pair_wer_terminal_adjacent + wpp_pair_wer_terminal_adjacent))) * g)) /\ exists wpp_beta_quotient_wer_terminal_adjacent_right_entry. f = wpp_beta_quotient_wer_terminal_adjacent_right_entry * S ((S (S (wpp_pair_wer_terminal_adjacent + wpp_pair_wer_terminal_adjacent))) * g) + (wpp_right_wer_terminal_adjacent))) -> (exists wpp_mod_left_wer_terminal_adjacent_pair_mod wpp_mod_right_wer_terminal_adjacent_pair_mod. (wpp_left_wer_terminal_adjacent * wpp_right_wer_terminal_adjacent) + p * wpp_mod_left_wer_terminal_adjacent_pair_mod = (1) + p * wpp_mod_right_wer_terminal_adjacent_pair_mod)) /\ (((exists ff_u_wer_terminal_lifted_product ff_v_wer_terminal_lifted_product. ((((exists ff_h_wer_terminal_lifted_product_start. ff_h_wer_terminal_lifted_product_start + S (1) = S ((S (0)) * ff_v_wer_terminal_lifted_product)) /\ exists ff_q_wer_terminal_lifted_product_start. ff_u_wer_terminal_lifted_product = ff_q_wer_terminal_lifted_product_start * S ((S (0)) * ff_v_wer_terminal_lifted_product) + (1))) /\ ((((exists ff_h_wer_terminal_lifted_product_terminal. ff_h_wer_terminal_lifted_product_terminal + S (Q) = S ((S (m + m)) * ff_v_wer_terminal_lifted_product)) /\ exists ff_q_wer_terminal_lifted_product_terminal. ff_u_wer_terminal_lifted_product = ff_q_wer_terminal_lifted_product_terminal * S ((S (m + m)) * ff_v_wer_terminal_lifted_product) + (Q))) /\ forall ff_i_wer_terminal_lifted_product. (exists ff_lt_wer_terminal_lifted_product_bound. ff_lt_wer_terminal_lifted_product_bound + S ff_i_wer_terminal_lifted_product = m + m) -> exists ff_p_wer_terminal_lifted_product ff_r_wer_terminal_lifted_product ff_s_wer_terminal_lifted_product. ((((exists ff_h_wer_terminal_lifted_product_factor. ff_h_wer_terminal_lifted_product_factor + S (ff_p_wer_terminal_lifted_product) = S ((S (ff_i_wer_terminal_lifted_product)) * g)) /\ exists ff_q_wer_terminal_lifted_product_factor. f = ff_q_wer_terminal_lifted_product_factor * S ((S (ff_i_wer_terminal_lifted_product)) * g) + (ff_p_wer_terminal_lifted_product))) /\ ((((exists ff_h_wer_terminal_lifted_product_partial. ff_h_wer_terminal_lifted_product_partial + S (ff_r_wer_terminal_lifted_product) = S ((S (ff_i_wer_terminal_lifted_product)) * ff_v_wer_terminal_lifted_product)) /\ exists ff_q_wer_terminal_lifted_product_partial. ff_u_wer_terminal_lifted_product = ff_q_wer_terminal_lifted_product_partial * S ((S (ff_i_wer_terminal_lifted_product)) * ff_v_wer_terminal_lifted_product) + (ff_r_wer_terminal_lifted_product))) /\ ((((exists ff_h_wer_terminal_lifted_product_successor. ff_h_wer_terminal_lifted_product_successor + S (ff_s_wer_terminal_lifted_product) = S ((S (S ff_i_wer_terminal_lifted_product)) * ff_v_wer_terminal_lifted_product)) /\ exists ff_q_wer_terminal_lifted_product_successor. ff_u_wer_terminal_lifted_product = ff_q_wer_terminal_lifted_product_successor * S ((S (S ff_i_wer_terminal_lifted_product)) * ff_v_wer_terminal_lifted_product) + (ff_s_wer_terminal_lifted_product))) /\ ff_s_wer_terminal_lifted_product = ff_r_wer_terminal_lifted_product * ff_p_wer_terminal_lifted_product)))))) /\ (((exists wpp_mod_left_wer_terminal_mod_one wpp_mod_right_wer_terminal_mod_one. (Q) + p * wpp_mod_left_wer_terminal_mod_one = (1) + p * wpp_mod_right_wer_terminal_mod_one) /\ (((forall wtp_range_index_wer_terminal_range. (exists wtp_range_gap_wer_terminal_range. wtp_range_gap_wer_terminal_range + S wtp_range_index_wer_terminal_range = m + m) -> (((exists ff_h_wer_terminal_range_decoded. ff_h_wer_terminal_range_decoded + S (2 + wtp_range_index_wer_terminal_range) = S ((S (wtp_range_index_wer_terminal_range)) * d)) /\ exists ff_q_wer_terminal_range_decoded. z = ff_q_wer_terminal_range_decoded * S ((S (wtp_range_index_wer_terminal_range)) * d) + (2 + wtp_range_index_wer_terminal_range)))) /\ (((exists ff_u_wer_terminal_canonical_product ff_v_wer_terminal_canonical_product. ((((exists ff_h_wer_terminal_canonical_product_start. ff_h_wer_terminal_canonical_product_start + S (1) = S ((S (0)) * ff_v_wer_terminal_canonical_product)) /\ exists ff_q_wer_terminal_canonical_product_start. ff_u_wer_terminal_canonical_product = ff_q_wer_terminal_canonical_product_start * S ((S (0)) * ff_v_wer_terminal_canonical_product) + (1))) /\ ((((exists ff_h_wer_terminal_canonical_product_terminal. ff_h_wer_terminal_canonical_product_terminal + S (P) = S ((S (m + m)) * ff_v_wer_terminal_canonical_product)) /\ exists ff_q_wer_terminal_canonical_product_terminal. ff_u_wer_terminal_canonical_product = ff_q_wer_terminal_canonical_product_terminal * S ((S (m + m)) * ff_v_wer_terminal_canonical_product) + (P))) /\ forall ff_i_wer_terminal_canonical_product. (exists ff_lt_wer_terminal_canonical_product_bound. ff_lt_wer_terminal_canonical_product_bound + S ff_i_wer_terminal_canonical_product = m + m) -> exists ff_p_wer_terminal_canonical_product ff_r_wer_terminal_canonical_product ff_s_wer_terminal_canonical_product. ((((exists ff_h_wer_terminal_canonical_product_factor. ff_h_wer_terminal_canonical_product_factor + S (ff_p_wer_terminal_canonical_product) = S ((S (ff_i_wer_terminal_canonical_product)) * d)) /\ exists ff_q_wer_terminal_canonical_product_factor. z = ff_q_wer_terminal_canonical_product_factor * S ((S (ff_i_wer_terminal_canonical_product)) * d) + (ff_p_wer_terminal_canonical_product))) /\ ((((exists ff_h_wer_terminal_canonical_product_partial. ff_h_wer_terminal_canonical_product_partial + S (ff_r_wer_terminal_canonical_product) = S ((S (ff_i_wer_terminal_canonical_product)) * ff_v_wer_terminal_canonical_product)) /\ exists ff_q_wer_terminal_canonical_product_partial. ff_u_wer_terminal_canonical_product = ff_q_wer_terminal_canonical_product_partial * S ((S (ff_i_wer_terminal_canonical_product)) * ff_v_wer_terminal_canonical_product) + (ff_r_wer_terminal_canonical_product))) /\ ((((exists ff_h_wer_terminal_canonical_product_successor. ff_h_wer_terminal_canonical_product_successor + S (ff_s_wer_terminal_canonical_product) = S ((S (S ff_i_wer_terminal_canonical_product)) * ff_v_wer_terminal_canonical_product)) /\ exists ff_q_wer_terminal_canonical_product_successor. ff_u_wer_terminal_canonical_product = ff_q_wer_terminal_canonical_product_successor * S ((S (S ff_i_wer_terminal_canonical_product)) * ff_v_wer_terminal_canonical_product) + (ff_s_wer_terminal_canonical_product))) /\ ff_s_wer_terminal_canonical_product = ff_r_wer_terminal_canonical_product * ff_p_wer_terminal_canonical_product)))))) /\ (P = Q))))))))))))))))))
  16. 0016specialize prime_wilson_terminal_product_package_exists p
  17. 0017specialize prime_wilson_terminal_product_package_exists n
  18. 0018specialize prime_wilson_terminal_product_package_exists x
  19. 0019specialize prime_wilson_terminal_product_package_exists x1
  20. 0020specialize prime_wilson_terminal_product_package_exists (S (m + m))
  21. 0021specialize prime_wilson_terminal_product_package_exists m
  22. 0022apply prime_wilson_terminal_product_package_exists
  23. 0023exact hpn
  24. 0024exact hp
  25. 0025exact hinverse_witness_witness
  26. 0026exact hterminal
  27. 0027exact hterminal
  28. 0028cases hpackage
  29. 0029cases hpackage_witness
  30. 0030cases hpackage_witness_witness
  31. 0031cases hpackage_witness_witness_witness
  32. 0032cases hpackage_witness_witness_witness_witness
  33. 0033cases hpackage_witness_witness_witness_witness_witness
  34. 0034cases hpackage_witness_witness_witness_witness_witness_witness
  35. 0035cases hpackage_witness_witness_witness_witness_witness_witness_witness
  36. 0036have hparts : (∀ y. ∀ z. ∀ k. Lt(y,m + m) → BetaAt(x2,x3,y,z) → BetaAt(x,x1,z,k) → ContainsPrefix(x2,x3,m + m,k)) ∧ ((∀ y. Lt(y,m + m) → ∃ z. BetaAt(x2,x3,y,z) ∧ Lt(z,n)) ∧ ((∀ y. ∀ z. Lt(y,m + m) → BetaAt(x2,x3,y,z) → ¬z = 0 ∧ ¬S z = n) ∧ InjectivePrefix(x2,x3,m + m))) ∧ ((∀ y. Lt(y,m) → ∃ z. ∃ k. BetaAt(x2,x3,y + y,z) ∧ (BetaAt(x2,x3,S (y + y),k) ∧ BetaAt(x,x1,z,k))) ∧ ((∀ y. Lt(y,S S (m + m)) → ¬y = 0 ∧ ¬S y = S S (m + m) → ContainsPrefix(x2,x3,m + m,y)) ∧ ((∀ y. ∀ z. Lt(y,m + m) → BetaAt(x2,x3,y,z) → BetaAt(x4,x5,y,S z)) ∧ ((∀ y. ∀ z. ∀ k. Lt(y,m) → BetaAt(x4,x5,y + y,z) → BetaAt(x4,x5,S (y + y),k) → BalancedInverse(p,z,k)) ∧ (Product(x4,x5,m + m,x6) ∧ (ModEq(p,x6,1) ∧ (Range(x7,x8,2,m + m) ∧ (Product(x7,x8,m + m,x9) ∧ x9 = x6))))))))
    Exact native replay linehave hparts : ((((forall wpo_position_wer_witness_state_closed wpo_source_wer_witness_state_closed wpo_mate_wer_witness_state_closed. (exists wpo_gap_wer_witness_state_closed_position_bound. wpo_gap_wer_witness_state_closed_position_bound + S (wpo_position_wer_witness_state_closed) = m + m) -> (((exists wpo_beta_height_wer_witness_state_closed_source_entry. wpo_beta_height_wer_witness_state_closed_source_entry + S (wpo_source_wer_witness_state_closed) = S ((S (wpo_position_wer_witness_state_closed)) * x3)) /\ exists wpo_beta_quotient_wer_witness_state_closed_source_entry. x2 = wpo_beta_quotient_wer_witness_state_closed_source_entry * S ((S (wpo_position_wer_witness_state_closed)) * x3) + (wpo_source_wer_witness_state_closed))) -> (((exists wpo_beta_height_wer_witness_state_closed_inverse_entry. wpo_beta_height_wer_witness_state_closed_inverse_entry + S (wpo_mate_wer_witness_state_closed) = S ((S (wpo_source_wer_witness_state_closed)) * x1)) /\ exists wpo_beta_quotient_wer_witness_state_closed_inverse_entry. x = wpo_beta_quotient_wer_witness_state_closed_inverse_entry * S ((S (wpo_source_wer_witness_state_closed)) * x1) + (wpo_mate_wer_witness_state_closed))) -> exists wpo_mate_position_wer_witness_state_closed. ((exists wpo_gap_wer_witness_state_closed_mate_bound. wpo_gap_wer_witness_state_closed_mate_bound + S (wpo_mate_position_wer_witness_state_closed) = m + m) /\ (((exists wpo_beta_height_wer_witness_state_closed_mate_entry. wpo_beta_height_wer_witness_state_closed_mate_entry + S (wpo_mate_wer_witness_state_closed) = S ((S (wpo_mate_position_wer_witness_state_closed)) * x3)) /\ exists wpo_beta_quotient_wer_witness_state_closed_mate_entry. x2 = wpo_beta_quotient_wer_witness_state_closed_mate_entry * S ((S (wpo_mate_position_wer_witness_state_closed)) * x3) + (wpo_mate_wer_witness_state_closed))))) /\ ((forall fom_index_wer_witness_state_bounded. (exists fom_gap_wer_witness_state_bounded_index_bound. fom_gap_wer_witness_state_bounded_index_bound + S (fom_index_wer_witness_state_bounded) = m + m) -> exists fom_value_wer_witness_state_bounded. ((((exists fom_beta_height_wer_witness_state_bounded_entry. fom_beta_height_wer_witness_state_bounded_entry + S (fom_value_wer_witness_state_bounded) = S ((S (fom_index_wer_witness_state_bounded)) * x3)) /\ exists fom_beta_quotient_wer_witness_state_bounded_entry. x2 = fom_beta_quotient_wer_witness_state_bounded_entry * S ((S (fom_index_wer_witness_state_bounded)) * x3) + (fom_value_wer_witness_state_bounded))) /\ (exists fom_gap_wer_witness_state_bounded_value_bound. fom_gap_wer_witness_state_bounded_value_bound + S (fom_value_wer_witness_state_bounded) = n))) /\ ((forall wpo_position_wer_witness_state_nonendpoint wpo_value_wer_witness_state_nonendpoint. (exists wpo_gap_wer_witness_state_nonendpoint_position_bound. wpo_gap_wer_witness_state_nonendpoint_position_bound + S (wpo_position_wer_witness_state_nonendpoint) = m + m) -> (((exists wpo_beta_height_wer_witness_state_nonendpoint_entry. wpo_beta_height_wer_witness_state_nonendpoint_entry + S (wpo_value_wer_witness_state_nonendpoint) = S ((S (wpo_position_wer_witness_state_nonendpoint)) * x3)) /\ exists wpo_beta_quotient_wer_witness_state_nonendpoint_entry. x2 = wpo_beta_quotient_wer_witness_state_nonendpoint_entry * S ((S (wpo_position_wer_witness_state_nonendpoint)) * x3) + (wpo_value_wer_witness_state_nonendpoint))) -> (~(wpo_value_wer_witness_state_nonendpoint = 0) /\ ~((S wpo_value_wer_witness_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wer_witness_state_injective wpo_injective_right_wer_witness_state_injective wpo_injective_value_wer_witness_state_injective. (exists wpo_gap_wer_witness_state_injective_left_bound. wpo_gap_wer_witness_state_injective_left_bound + S (wpo_injective_left_wer_witness_state_injective) = m + m) -> (exists wpo_gap_wer_witness_state_injective_right_bound. wpo_gap_wer_witness_state_injective_right_bound + S (wpo_injective_right_wer_witness_state_injective) = m + m) -> (((exists wpo_beta_height_wer_witness_state_injective_left_entry. wpo_beta_height_wer_witness_state_injective_left_entry + S (wpo_injective_value_wer_witness_state_injective) = S ((S (wpo_injective_left_wer_witness_state_injective)) * x3)) /\ exists wpo_beta_quotient_wer_witness_state_injective_left_entry. x2 = wpo_beta_quotient_wer_witness_state_injective_left_entry * S ((S (wpo_injective_left_wer_witness_state_injective)) * x3) + (wpo_injective_value_wer_witness_state_injective))) -> (((exists wpo_beta_height_wer_witness_state_injective_right_entry. wpo_beta_height_wer_witness_state_injective_right_entry + S (wpo_injective_value_wer_witness_state_injective) = S ((S (wpo_injective_right_wer_witness_state_injective)) * x3)) /\ exists wpo_beta_quotient_wer_witness_state_injective_right_entry. x2 = wpo_beta_quotient_wer_witness_state_injective_right_entry * S ((S (wpo_injective_right_wer_witness_state_injective)) * x3) + (wpo_injective_value_wer_witness_state_injective))) -> wpo_injective_left_wer_witness_state_injective = wpo_injective_right_wer_witness_state_injective))))) /\ (((forall wpop_pair_wer_witness_history. (exists wpo_gap_wer_witness_history_pair_bound. wpo_gap_wer_witness_history_pair_bound + S (wpop_pair_wer_witness_history) = m) -> exists wpop_left_wer_witness_history wpop_right_wer_witness_history. ((((exists wpo_beta_height_wer_witness_history_left_entry. wpo_beta_height_wer_witness_history_left_entry + S (wpop_left_wer_witness_history) = S ((S (wpop_pair_wer_witness_history + wpop_pair_wer_witness_history)) * x3)) /\ exists wpo_beta_quotient_wer_witness_history_left_entry. x2 = wpo_beta_quotient_wer_witness_history_left_entry * S ((S (wpop_pair_wer_witness_history + wpop_pair_wer_witness_history)) * x3) + (wpop_left_wer_witness_history))) /\ ((((exists wpo_beta_height_wer_witness_history_right_entry. wpo_beta_height_wer_witness_history_right_entry + S (wpop_right_wer_witness_history) = S ((S (S (wpop_pair_wer_witness_history + wpop_pair_wer_witness_history))) * x3)) /\ exists wpo_beta_quotient_wer_witness_history_right_entry. x2 = wpo_beta_quotient_wer_witness_history_right_entry * S ((S (S (wpop_pair_wer_witness_history + wpop_pair_wer_witness_history))) * x3) + (wpop_right_wer_witness_history))) /\ (((exists wpo_beta_height_wer_witness_history_inverse_entry. wpo_beta_height_wer_witness_history_inverse_entry + S (wpop_right_wer_witness_history) = S ((S (wpop_left_wer_witness_history)) * x1)) /\ exists wpo_beta_quotient_wer_witness_history_inverse_entry. x = wpo_beta_quotient_wer_witness_history_inverse_entry * S ((S (wpop_left_wer_witness_history)) * x1) + (wpop_right_wer_witness_history)))))) /\ (((forall s. (exists wpo_gap_wer_terminal_coverage_value_bound. wpo_gap_wer_terminal_coverage_value_bound + S (s) = S (S (m + m))) -> (~(s = 0) /\ ~((S s) = S (S (m + m)))) -> exists q. ((exists wpo_gap_wer_terminal_coverage_index_bound. wpo_gap_wer_terminal_coverage_index_bound + S (q) = m + m) /\ (((exists wpo_beta_height_wer_witness_coverage_entry. wpo_beta_height_wer_witness_coverage_entry + S (s) = S ((S (q)) * x3)) /\ exists wpo_beta_quotient_wer_witness_coverage_entry. x2 = wpo_beta_quotient_wer_witness_coverage_entry * S ((S (q)) * x3) + (s))))) /\ (((forall wsl_index_wer_witness_lift wsl_value_wer_witness_lift. (exists wpo_gap_wer_witness_lift_bound. wpo_gap_wer_witness_lift_bound + S (wsl_index_wer_witness_lift) = m + m) -> (((exists wpo_beta_height_wer_witness_lift_source. wpo_beta_height_wer_witness_lift_source + S (wsl_value_wer_witness_lift) = S ((S (wsl_index_wer_witness_lift)) * x3)) /\ exists wpo_beta_quotient_wer_witness_lift_source. x2 = wpo_beta_quotient_wer_witness_lift_source * S ((S (wsl_index_wer_witness_lift)) * x3) + (wsl_value_wer_witness_lift))) -> (((exists wpo_beta_height_wer_witness_lift_target. wpo_beta_height_wer_witness_lift_target + S (S wsl_value_wer_witness_lift) = S ((S (wsl_index_wer_witness_lift)) * x5)) /\ exists wpo_beta_quotient_wer_witness_lift_target. x4 = wpo_beta_quotient_wer_witness_lift_target * S ((S (wsl_index_wer_witness_lift)) * x5) + (S wsl_value_wer_witness_lift)))) /\ (((forall wpp_pair_wer_witness_adjacent wpp_left_wer_witness_adjacent wpp_right_wer_witness_adjacent. (exists wpp_gap_wer_witness_adjacent_pair_bound. wpp_gap_wer_witness_adjacent_pair_bound + S (wpp_pair_wer_witness_adjacent) = m) -> (((exists wpp_beta_height_wer_witness_adjacent_left_entry. wpp_beta_height_wer_witness_adjacent_left_entry + S (wpp_left_wer_witness_adjacent) = S ((S ((wpp_pair_wer_witness_adjacent + wpp_pair_wer_witness_adjacent))) * x5)) /\ exists wpp_beta_quotient_wer_witness_adjacent_left_entry. x4 = wpp_beta_quotient_wer_witness_adjacent_left_entry * S ((S ((wpp_pair_wer_witness_adjacent + wpp_pair_wer_witness_adjacent))) * x5) + (wpp_left_wer_witness_adjacent))) -> (((exists wpp_beta_height_wer_witness_adjacent_right_entry. wpp_beta_height_wer_witness_adjacent_right_entry + S (wpp_right_wer_witness_adjacent) = S ((S (S (wpp_pair_wer_witness_adjacent + wpp_pair_wer_witness_adjacent))) * x5)) /\ exists wpp_beta_quotient_wer_witness_adjacent_right_entry. x4 = wpp_beta_quotient_wer_witness_adjacent_right_entry * S ((S (S (wpp_pair_wer_witness_adjacent + wpp_pair_wer_witness_adjacent))) * x5) + (wpp_right_wer_witness_adjacent))) -> (exists wpp_mod_left_wer_witness_adjacent_pair_mod wpp_mod_right_wer_witness_adjacent_pair_mod. (wpp_left_wer_witness_adjacent * wpp_right_wer_witness_adjacent) + p * wpp_mod_left_wer_witness_adjacent_pair_mod = (1) + p * wpp_mod_right_wer_witness_adjacent_pair_mod)) /\ (((exists ff_u_wer_witness_lifted_product ff_v_wer_witness_lifted_product. ((((exists ff_h_wer_witness_lifted_product_start. ff_h_wer_witness_lifted_product_start + S (1) = S ((S (0)) * ff_v_wer_witness_lifted_product)) /\ exists ff_q_wer_witness_lifted_product_start. ff_u_wer_witness_lifted_product = ff_q_wer_witness_lifted_product_start * S ((S (0)) * ff_v_wer_witness_lifted_product) + (1))) /\ ((((exists ff_h_wer_witness_lifted_product_terminal. ff_h_wer_witness_lifted_product_terminal + S (x6) = S ((S (m + m)) * ff_v_wer_witness_lifted_product)) /\ exists ff_q_wer_witness_lifted_product_terminal. ff_u_wer_witness_lifted_product = ff_q_wer_witness_lifted_product_terminal * S ((S (m + m)) * ff_v_wer_witness_lifted_product) + (x6))) /\ forall ff_i_wer_witness_lifted_product. (exists ff_lt_wer_witness_lifted_product_bound. ff_lt_wer_witness_lifted_product_bound + S ff_i_wer_witness_lifted_product = m + m) -> exists ff_p_wer_witness_lifted_product ff_r_wer_witness_lifted_product ff_s_wer_witness_lifted_product. ((((exists ff_h_wer_witness_lifted_product_factor. ff_h_wer_witness_lifted_product_factor + S (ff_p_wer_witness_lifted_product) = S ((S (ff_i_wer_witness_lifted_product)) * x5)) /\ exists ff_q_wer_witness_lifted_product_factor. x4 = ff_q_wer_witness_lifted_product_factor * S ((S (ff_i_wer_witness_lifted_product)) * x5) + (ff_p_wer_witness_lifted_product))) /\ ((((exists ff_h_wer_witness_lifted_product_partial. ff_h_wer_witness_lifted_product_partial + S (ff_r_wer_witness_lifted_product) = S ((S (ff_i_wer_witness_lifted_product)) * ff_v_wer_witness_lifted_product)) /\ exists ff_q_wer_witness_lifted_product_partial. ff_u_wer_witness_lifted_product = ff_q_wer_witness_lifted_product_partial * S ((S (ff_i_wer_witness_lifted_product)) * ff_v_wer_witness_lifted_product) + (ff_r_wer_witness_lifted_product))) /\ ((((exists ff_h_wer_witness_lifted_product_successor. ff_h_wer_witness_lifted_product_successor + S (ff_s_wer_witness_lifted_product) = S ((S (S ff_i_wer_witness_lifted_product)) * ff_v_wer_witness_lifted_product)) /\ exists ff_q_wer_witness_lifted_product_successor. ff_u_wer_witness_lifted_product = ff_q_wer_witness_lifted_product_successor * S ((S (S ff_i_wer_witness_lifted_product)) * ff_v_wer_witness_lifted_product) + (ff_s_wer_witness_lifted_product))) /\ ff_s_wer_witness_lifted_product = ff_r_wer_witness_lifted_product * ff_p_wer_witness_lifted_product)))))) /\ (((exists wpp_mod_left_wer_witness_mod_one wpp_mod_right_wer_witness_mod_one. (x6) + p * wpp_mod_left_wer_witness_mod_one = (1) + p * wpp_mod_right_wer_witness_mod_one) /\ (((forall wtp_range_index_wer_witness_range. (exists wtp_range_gap_wer_witness_range. wtp_range_gap_wer_witness_range + S wtp_range_index_wer_witness_range = m + m) -> (((exists ff_h_wer_witness_range_decoded. ff_h_wer_witness_range_decoded + S (2 + wtp_range_index_wer_witness_range) = S ((S (wtp_range_index_wer_witness_range)) * x8)) /\ exists ff_q_wer_witness_range_decoded. x7 = ff_q_wer_witness_range_decoded * S ((S (wtp_range_index_wer_witness_range)) * x8) + (2 + wtp_range_index_wer_witness_range)))) /\ (((exists ff_u_wer_witness_product ff_v_wer_witness_product. ((((exists ff_h_wer_witness_product_start. ff_h_wer_witness_product_start + S (1) = S ((S (0)) * ff_v_wer_witness_product)) /\ exists ff_q_wer_witness_product_start. ff_u_wer_witness_product = ff_q_wer_witness_product_start * S ((S (0)) * ff_v_wer_witness_product) + (1))) /\ ((((exists ff_h_wer_witness_product_terminal. ff_h_wer_witness_product_terminal + S (x9) = S ((S (m + m)) * ff_v_wer_witness_product)) /\ exists ff_q_wer_witness_product_terminal. ff_u_wer_witness_product = ff_q_wer_witness_product_terminal * S ((S (m + m)) * ff_v_wer_witness_product) + (x9))) /\ forall ff_i_wer_witness_product. (exists ff_lt_wer_witness_product_bound. ff_lt_wer_witness_product_bound + S ff_i_wer_witness_product = m + m) -> exists ff_p_wer_witness_product ff_r_wer_witness_product ff_s_wer_witness_product. ((((exists ff_h_wer_witness_product_factor. ff_h_wer_witness_product_factor + S (ff_p_wer_witness_product) = S ((S (ff_i_wer_witness_product)) * x8)) /\ exists ff_q_wer_witness_product_factor. x7 = ff_q_wer_witness_product_factor * S ((S (ff_i_wer_witness_product)) * x8) + (ff_p_wer_witness_product))) /\ ((((exists ff_h_wer_witness_product_partial. ff_h_wer_witness_product_partial + S (ff_r_wer_witness_product) = S ((S (ff_i_wer_witness_product)) * ff_v_wer_witness_product)) /\ exists ff_q_wer_witness_product_partial. ff_u_wer_witness_product = ff_q_wer_witness_product_partial * S ((S (ff_i_wer_witness_product)) * ff_v_wer_witness_product) + (ff_r_wer_witness_product))) /\ ((((exists ff_h_wer_witness_product_successor. ff_h_wer_witness_product_successor + S (ff_s_wer_witness_product) = S ((S (S ff_i_wer_witness_product)) * ff_v_wer_witness_product)) /\ exists ff_q_wer_witness_product_successor. ff_u_wer_witness_product = ff_q_wer_witness_product_successor * S ((S (S ff_i_wer_witness_product)) * ff_v_wer_witness_product) + (ff_s_wer_witness_product))) /\ ff_s_wer_witness_product = ff_r_wer_witness_product * ff_p_wer_witness_product)))))) /\ (x9 = x6))))))))))))))))))
  37. 0037exact hpackage_witness_witness_witness_witness_witness_witness_witness_witness
  38. 0038cases hparts
  39. 0039cases hparts_right
  40. 0040cases hparts_right_right
  41. 0041cases hparts_right_right_right
  42. 0042cases hparts_right_right_right_right
  43. 0043cases hparts_right_right_right_right_right
  44. 0044cases hparts_right_right_right_right_right_right
  45. 0045cases hparts_right_right_right_right_right_right_right
  46. 0046cases hparts_right_right_right_right_right_right_right_right
  47. 0047have hmod_product : ModEq(p,x9,1)
    Exact native replay linehave hmod_product : exists wpp_mod_left_wer_witness_mod_product wpp_mod_right_wer_witness_mod_product. (x9) + p * wpp_mod_left_wer_witness_mod_product = (1) + p * wpp_mod_right_wer_witness_mod_product
  48. 0048rewrite hparts_right_right_right_right_right_right_right_right_right
  49. 0049exact hparts_right_right_right_right_right_right_left
  50. 0050exists x7
  51. 0051exists x8
  52. 0052exists x9
  53. 0053split
  54. 0054exact hparts_right_right_right_right_right_right_right_left
  55. 0055split
  56. 0056exact hparts_right_right_right_right_right_right_right_right_left
  57. 0057exact hmod_product