PA00BE · theorem

prime_wilson_terminal_product_package_exists

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

Package terminal PairOrder history, coverage, lifted product, and equality with residues 2,...,p-2.

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. ∀ u. ∀ v. ∀ r. ∀ m. p = S n → Prime(p) → InversePrefix(p,n,u,v,n) → n = S r → n = S S (m + m) → ∃ x. ∃ y. ∃ z. ∃ k. ∃ i. ∃ j. ∃ w. ∃ x0. (∀ x1. ∀ x2. ∀ x3. Lt(x1,m + m) → BetaAt(x,y,x1,x2) → BetaAt(u,v,x2,x3) → ContainsPrefix(x,y,m + m,x3)) ∧ ((∀ x1. Lt(x1,m + m) → ∃ x2. BetaAt(x,y,x1,x2) ∧ Lt(x2,n)) ∧ ((∀ x1. ∀ x2. Lt(x1,m + m) → BetaAt(x,y,x1,x2) → ¬x2 = 0 ∧ ¬S x2 = n) ∧ InjectivePrefix(x,y,m + m))) ∧ ((∀ x1. Lt(x1,m) → ∃ x2. ∃ x3. BetaAt(x,y,x1 + x1,x2) ∧ (BetaAt(x,y,S (x1 + x1),x3) ∧ BetaAt(u,v,x2,x3))) ∧ ((∀ x1. Lt(x1,S S (m + m)) → ¬x1 = 0 ∧ ¬S x1 = S S (m + m) → ContainsPrefix(x,y,m + m,x1)) ∧ ((∀ x1. ∀ x2. Lt(x1,m + m) → BetaAt(x,y,x1,x2) → BetaAt(z,k,x1,S x2)) ∧ ((∀ x1. ∀ x2. ∀ x3. Lt(x1,m) → BetaAt(z,k,x1 + x1,x2) → BetaAt(z,k,S (x1 + x1),x3) → BalancedInverse(p,x2,x3)) ∧ (Product(z,k,m + m,i) ∧ (ModEq(p,i,1) ∧ (Range(j,w,2,m + m) ∧ (Product(j,w,m + m,x0) ∧ x0 = i))))))))

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 PD0004 Prime PD0008 ModEq PD0013 BetaAt PD0014 Product PD0018 Range PD0025 InjectivePrefix PD0027 ContainsPrefix PD0031 BalancedInverse PD0037 InversePrefix

29 occurrences

In local proof propositions

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

68 occurrences

Exact expanded native-PA statement
forall p n u v r m. p = S n -> ((~(p = 1) /\ forall wip_prime_left_wtp_cap_prime wip_prime_right_wtp_cap_prime. p = wip_prime_left_wtp_cap_prime * wip_prime_right_wtp_cap_prime -> wip_prime_left_wtp_cap_prime = 1 \/ wip_prime_right_wtp_cap_prime = 1)) -> (forall wip_index_wtp_cap_inverse. (exists wip_gap_wtp_cap_inverse_prefix_bound. wip_gap_wtp_cap_inverse_prefix_bound + S wip_index_wtp_cap_inverse = n) -> exists wip_mate_wtp_cap_inverse. ((((exists wip_beta_height_wtp_cap_inverse_decoded. wip_beta_height_wtp_cap_inverse_decoded + S (wip_mate_wtp_cap_inverse) = S ((S (wip_index_wtp_cap_inverse)) * v)) /\ exists wip_beta_quotient_wtp_cap_inverse_decoded. u = wip_beta_quotient_wtp_cap_inverse_decoded * S ((S (wip_index_wtp_cap_inverse)) * v) + (wip_mate_wtp_cap_inverse))) /\ ((exists wip_gap_wtp_cap_inverse_inverse_index_bound. wip_gap_wtp_cap_inverse_inverse_index_bound + S wip_index_wtp_cap_inverse = n) /\ ((exists wip_gap_wtp_cap_inverse_inverse_mate_bound. wip_gap_wtp_cap_inverse_inverse_mate_bound + S wip_mate_wtp_cap_inverse = n) /\ (exists wip_mod_left_wtp_cap_inverse_inverse_mod wip_mod_right_wtp_cap_inverse_inverse_mod. ((S wip_index_wtp_cap_inverse) * S wip_mate_wtp_cap_inverse) + p * wip_mod_left_wtp_cap_inverse_inverse_mod = 1 + p * wip_mod_right_wtp_cap_inverse_inverse_mod))))) -> n = S r -> n = S (S (m + m)) -> (exists b c f g Q z d P. ((((forall wpo_position_wtp_cap_state_closed wpo_source_wtp_cap_state_closed wpo_mate_wtp_cap_state_closed. (exists wpo_gap_wtp_cap_state_closed_position_bound. wpo_gap_wtp_cap_state_closed_position_bound + S (wpo_position_wtp_cap_state_closed) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_closed_source_entry. wpo_beta_height_wtp_cap_state_closed_source_entry + S (wpo_source_wtp_cap_state_closed) = S ((S (wpo_position_wtp_cap_state_closed)) * c)) /\ exists wpo_beta_quotient_wtp_cap_state_closed_source_entry. b = wpo_beta_quotient_wtp_cap_state_closed_source_entry * S ((S (wpo_position_wtp_cap_state_closed)) * c) + (wpo_source_wtp_cap_state_closed))) -> (((exists wpo_beta_height_wtp_cap_state_closed_inverse_entry. wpo_beta_height_wtp_cap_state_closed_inverse_entry + S (wpo_mate_wtp_cap_state_closed) = S ((S (wpo_source_wtp_cap_state_closed)) * v)) /\ exists wpo_beta_quotient_wtp_cap_state_closed_inverse_entry. u = wpo_beta_quotient_wtp_cap_state_closed_inverse_entry * S ((S (wpo_source_wtp_cap_state_closed)) * v) + (wpo_mate_wtp_cap_state_closed))) -> exists wpo_mate_position_wtp_cap_state_closed. ((exists wpo_gap_wtp_cap_state_closed_mate_bound. wpo_gap_wtp_cap_state_closed_mate_bound + S (wpo_mate_position_wtp_cap_state_closed) = m + m) /\ (((exists wpo_beta_height_wtp_cap_state_closed_mate_entry. wpo_beta_height_wtp_cap_state_closed_mate_entry + S (wpo_mate_wtp_cap_state_closed) = S ((S (wpo_mate_position_wtp_cap_state_closed)) * c)) /\ exists wpo_beta_quotient_wtp_cap_state_closed_mate_entry. b = wpo_beta_quotient_wtp_cap_state_closed_mate_entry * S ((S (wpo_mate_position_wtp_cap_state_closed)) * c) + (wpo_mate_wtp_cap_state_closed))))) /\ ((forall fom_index_wtp_cap_state_bounded. (exists fom_gap_wtp_cap_state_bounded_index_bound. fom_gap_wtp_cap_state_bounded_index_bound + S (fom_index_wtp_cap_state_bounded) = m + m) -> exists fom_value_wtp_cap_state_bounded. ((((exists fom_beta_height_wtp_cap_state_bounded_entry. fom_beta_height_wtp_cap_state_bounded_entry + S (fom_value_wtp_cap_state_bounded) = S ((S (fom_index_wtp_cap_state_bounded)) * c)) /\ exists fom_beta_quotient_wtp_cap_state_bounded_entry. b = fom_beta_quotient_wtp_cap_state_bounded_entry * S ((S (fom_index_wtp_cap_state_bounded)) * c) + (fom_value_wtp_cap_state_bounded))) /\ (exists fom_gap_wtp_cap_state_bounded_value_bound. fom_gap_wtp_cap_state_bounded_value_bound + S (fom_value_wtp_cap_state_bounded) = n))) /\ ((forall wpo_position_wtp_cap_state_nonendpoint wpo_value_wtp_cap_state_nonendpoint. (exists wpo_gap_wtp_cap_state_nonendpoint_position_bound. wpo_gap_wtp_cap_state_nonendpoint_position_bound + S (wpo_position_wtp_cap_state_nonendpoint) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_nonendpoint_entry. wpo_beta_height_wtp_cap_state_nonendpoint_entry + S (wpo_value_wtp_cap_state_nonendpoint) = S ((S (wpo_position_wtp_cap_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wtp_cap_state_nonendpoint_entry. b = wpo_beta_quotient_wtp_cap_state_nonendpoint_entry * S ((S (wpo_position_wtp_cap_state_nonendpoint)) * c) + (wpo_value_wtp_cap_state_nonendpoint))) -> (~(wpo_value_wtp_cap_state_nonendpoint = 0) /\ ~((S wpo_value_wtp_cap_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wtp_cap_state_injective wpo_injective_right_wtp_cap_state_injective wpo_injective_value_wtp_cap_state_injective. (exists wpo_gap_wtp_cap_state_injective_left_bound. wpo_gap_wtp_cap_state_injective_left_bound + S (wpo_injective_left_wtp_cap_state_injective) = m + m) -> (exists wpo_gap_wtp_cap_state_injective_right_bound. wpo_gap_wtp_cap_state_injective_right_bound + S (wpo_injective_right_wtp_cap_state_injective) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_injective_left_entry. wpo_beta_height_wtp_cap_state_injective_left_entry + S (wpo_injective_value_wtp_cap_state_injective) = S ((S (wpo_injective_left_wtp_cap_state_injective)) * c)) /\ exists wpo_beta_quotient_wtp_cap_state_injective_left_entry. b = wpo_beta_quotient_wtp_cap_state_injective_left_entry * S ((S (wpo_injective_left_wtp_cap_state_injective)) * c) + (wpo_injective_value_wtp_cap_state_injective))) -> (((exists wpo_beta_height_wtp_cap_state_injective_right_entry. wpo_beta_height_wtp_cap_state_injective_right_entry + S (wpo_injective_value_wtp_cap_state_injective) = S ((S (wpo_injective_right_wtp_cap_state_injective)) * c)) /\ exists wpo_beta_quotient_wtp_cap_state_injective_right_entry. b = wpo_beta_quotient_wtp_cap_state_injective_right_entry * S ((S (wpo_injective_right_wtp_cap_state_injective)) * c) + (wpo_injective_value_wtp_cap_state_injective))) -> wpo_injective_left_wtp_cap_state_injective = wpo_injective_right_wtp_cap_state_injective))))) /\ (((forall wpop_pair_wtp_cap_history. (exists wpo_gap_wtp_cap_history_pair_bound. wpo_gap_wtp_cap_history_pair_bound + S (wpop_pair_wtp_cap_history) = m) -> exists wpop_left_wtp_cap_history wpop_right_wtp_cap_history. ((((exists wpo_beta_height_wtp_cap_history_left_entry. wpo_beta_height_wtp_cap_history_left_entry + S (wpop_left_wtp_cap_history) = S ((S (wpop_pair_wtp_cap_history + wpop_pair_wtp_cap_history)) * c)) /\ exists wpo_beta_quotient_wtp_cap_history_left_entry. b = wpo_beta_quotient_wtp_cap_history_left_entry * S ((S (wpop_pair_wtp_cap_history + wpop_pair_wtp_cap_history)) * c) + (wpop_left_wtp_cap_history))) /\ ((((exists wpo_beta_height_wtp_cap_history_right_entry. wpo_beta_height_wtp_cap_history_right_entry + S (wpop_right_wtp_cap_history) = S ((S (S (wpop_pair_wtp_cap_history + wpop_pair_wtp_cap_history))) * c)) /\ exists wpo_beta_quotient_wtp_cap_history_right_entry. b = wpo_beta_quotient_wtp_cap_history_right_entry * S ((S (S (wpop_pair_wtp_cap_history + wpop_pair_wtp_cap_history))) * c) + (wpop_right_wtp_cap_history))) /\ (((exists wpo_beta_height_wtp_cap_history_inverse_entry. wpo_beta_height_wtp_cap_history_inverse_entry + S (wpop_right_wtp_cap_history) = S ((S (wpop_left_wtp_cap_history)) * v)) /\ exists wpo_beta_quotient_wtp_cap_history_inverse_entry. u = wpo_beta_quotient_wtp_cap_history_inverse_entry * S ((S (wpop_left_wtp_cap_history)) * v) + (wpop_right_wtp_cap_history)))))) /\ (((forall s. (exists wpo_gap_wtp_cap_coverage_value_bound. wpo_gap_wtp_cap_coverage_value_bound + S (s) = S (S (m + m))) -> (~(s = 0) /\ ~((S s) = S (S (m + m)))) -> exists q. ((exists wpo_gap_wtp_cap_coverage_index_bound. wpo_gap_wtp_cap_coverage_index_bound + S (q) = m + m) /\ (((exists wpo_beta_height_wtp_cap_coverage_entry. wpo_beta_height_wtp_cap_coverage_entry + S (s) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_wtp_cap_coverage_entry. b = wpo_beta_quotient_wtp_cap_coverage_entry * S ((S (q)) * c) + (s))))) /\ (((forall wsl_index_wtp_cap_lift wsl_value_wtp_cap_lift. (exists wpo_gap_wtp_cap_lift_bound. wpo_gap_wtp_cap_lift_bound + S (wsl_index_wtp_cap_lift) = m + m) -> (((exists wpo_beta_height_wtp_cap_lift_source. wpo_beta_height_wtp_cap_lift_source + S (wsl_value_wtp_cap_lift) = S ((S (wsl_index_wtp_cap_lift)) * c)) /\ exists wpo_beta_quotient_wtp_cap_lift_source. b = wpo_beta_quotient_wtp_cap_lift_source * S ((S (wsl_index_wtp_cap_lift)) * c) + (wsl_value_wtp_cap_lift))) -> (((exists wpo_beta_height_wtp_cap_lift_target. wpo_beta_height_wtp_cap_lift_target + S (S wsl_value_wtp_cap_lift) = S ((S (wsl_index_wtp_cap_lift)) * g)) /\ exists wpo_beta_quotient_wtp_cap_lift_target. f = wpo_beta_quotient_wtp_cap_lift_target * S ((S (wsl_index_wtp_cap_lift)) * g) + (S wsl_value_wtp_cap_lift)))) /\ (((forall wpp_pair_wtp_cap_adjacent wpp_left_wtp_cap_adjacent wpp_right_wtp_cap_adjacent. (exists wpp_gap_wtp_cap_adjacent_pair_bound. wpp_gap_wtp_cap_adjacent_pair_bound + S (wpp_pair_wtp_cap_adjacent) = m) -> (((exists wpp_beta_height_wtp_cap_adjacent_left_entry. wpp_beta_height_wtp_cap_adjacent_left_entry + S (wpp_left_wtp_cap_adjacent) = S ((S ((wpp_pair_wtp_cap_adjacent + wpp_pair_wtp_cap_adjacent))) * g)) /\ exists wpp_beta_quotient_wtp_cap_adjacent_left_entry. f = wpp_beta_quotient_wtp_cap_adjacent_left_entry * S ((S ((wpp_pair_wtp_cap_adjacent + wpp_pair_wtp_cap_adjacent))) * g) + (wpp_left_wtp_cap_adjacent))) -> (((exists wpp_beta_height_wtp_cap_adjacent_right_entry. wpp_beta_height_wtp_cap_adjacent_right_entry + S (wpp_right_wtp_cap_adjacent) = S ((S (S (wpp_pair_wtp_cap_adjacent + wpp_pair_wtp_cap_adjacent))) * g)) /\ exists wpp_beta_quotient_wtp_cap_adjacent_right_entry. f = wpp_beta_quotient_wtp_cap_adjacent_right_entry * S ((S (S (wpp_pair_wtp_cap_adjacent + wpp_pair_wtp_cap_adjacent))) * g) + (wpp_right_wtp_cap_adjacent))) -> (exists wpp_mod_left_wtp_cap_adjacent_pair_mod wpp_mod_right_wtp_cap_adjacent_pair_mod. (wpp_left_wtp_cap_adjacent * wpp_right_wtp_cap_adjacent) + p * wpp_mod_left_wtp_cap_adjacent_pair_mod = (1) + p * wpp_mod_right_wtp_cap_adjacent_pair_mod)) /\ (((exists ff_u_wtp_cap_lifted_product ff_v_wtp_cap_lifted_product. ((((exists ff_h_wtp_cap_lifted_product_start. ff_h_wtp_cap_lifted_product_start + S (1) = S ((S (0)) * ff_v_wtp_cap_lifted_product)) /\ exists ff_q_wtp_cap_lifted_product_start. ff_u_wtp_cap_lifted_product = ff_q_wtp_cap_lifted_product_start * S ((S (0)) * ff_v_wtp_cap_lifted_product) + (1))) /\ ((((exists ff_h_wtp_cap_lifted_product_terminal. ff_h_wtp_cap_lifted_product_terminal + S (Q) = S ((S (m + m)) * ff_v_wtp_cap_lifted_product)) /\ exists ff_q_wtp_cap_lifted_product_terminal. ff_u_wtp_cap_lifted_product = ff_q_wtp_cap_lifted_product_terminal * S ((S (m + m)) * ff_v_wtp_cap_lifted_product) + (Q))) /\ forall ff_i_wtp_cap_lifted_product. (exists ff_lt_wtp_cap_lifted_product_bound. ff_lt_wtp_cap_lifted_product_bound + S ff_i_wtp_cap_lifted_product = m + m) -> exists ff_p_wtp_cap_lifted_product ff_r_wtp_cap_lifted_product ff_s_wtp_cap_lifted_product. ((((exists ff_h_wtp_cap_lifted_product_factor. ff_h_wtp_cap_lifted_product_factor + S (ff_p_wtp_cap_lifted_product) = S ((S (ff_i_wtp_cap_lifted_product)) * g)) /\ exists ff_q_wtp_cap_lifted_product_factor. f = ff_q_wtp_cap_lifted_product_factor * S ((S (ff_i_wtp_cap_lifted_product)) * g) + (ff_p_wtp_cap_lifted_product))) /\ ((((exists ff_h_wtp_cap_lifted_product_partial. ff_h_wtp_cap_lifted_product_partial + S (ff_r_wtp_cap_lifted_product) = S ((S (ff_i_wtp_cap_lifted_product)) * ff_v_wtp_cap_lifted_product)) /\ exists ff_q_wtp_cap_lifted_product_partial. ff_u_wtp_cap_lifted_product = ff_q_wtp_cap_lifted_product_partial * S ((S (ff_i_wtp_cap_lifted_product)) * ff_v_wtp_cap_lifted_product) + (ff_r_wtp_cap_lifted_product))) /\ ((((exists ff_h_wtp_cap_lifted_product_successor. ff_h_wtp_cap_lifted_product_successor + S (ff_s_wtp_cap_lifted_product) = S ((S (S ff_i_wtp_cap_lifted_product)) * ff_v_wtp_cap_lifted_product)) /\ exists ff_q_wtp_cap_lifted_product_successor. ff_u_wtp_cap_lifted_product = ff_q_wtp_cap_lifted_product_successor * S ((S (S ff_i_wtp_cap_lifted_product)) * ff_v_wtp_cap_lifted_product) + (ff_s_wtp_cap_lifted_product))) /\ ff_s_wtp_cap_lifted_product = ff_r_wtp_cap_lifted_product * ff_p_wtp_cap_lifted_product)))))) /\ (((exists wpp_mod_left_wtp_cap_mod_one wpp_mod_right_wtp_cap_mod_one. (Q) + p * wpp_mod_left_wtp_cap_mod_one = (1) + p * wpp_mod_right_wtp_cap_mod_one) /\ (((forall wtp_range_index_wtp_cap_range_two. (exists wtp_range_gap_wtp_cap_range_two. wtp_range_gap_wtp_cap_range_two + S wtp_range_index_wtp_cap_range_two = m + m) -> (((exists ff_h_wtp_cap_range_two_decoded. ff_h_wtp_cap_range_two_decoded + S (2 + wtp_range_index_wtp_cap_range_two) = S ((S (wtp_range_index_wtp_cap_range_two)) * d)) /\ exists ff_q_wtp_cap_range_two_decoded. z = ff_q_wtp_cap_range_two_decoded * S ((S (wtp_range_index_wtp_cap_range_two)) * d) + (2 + wtp_range_index_wtp_cap_range_two)))) /\ (((exists ff_u_wtp_cap_canonical_product ff_v_wtp_cap_canonical_product. ((((exists ff_h_wtp_cap_canonical_product_start. ff_h_wtp_cap_canonical_product_start + S (1) = S ((S (0)) * ff_v_wtp_cap_canonical_product)) /\ exists ff_q_wtp_cap_canonical_product_start. ff_u_wtp_cap_canonical_product = ff_q_wtp_cap_canonical_product_start * S ((S (0)) * ff_v_wtp_cap_canonical_product) + (1))) /\ ((((exists ff_h_wtp_cap_canonical_product_terminal. ff_h_wtp_cap_canonical_product_terminal + S (P) = S ((S (m + m)) * ff_v_wtp_cap_canonical_product)) /\ exists ff_q_wtp_cap_canonical_product_terminal. ff_u_wtp_cap_canonical_product = ff_q_wtp_cap_canonical_product_terminal * S ((S (m + m)) * ff_v_wtp_cap_canonical_product) + (P))) /\ forall ff_i_wtp_cap_canonical_product. (exists ff_lt_wtp_cap_canonical_product_bound. ff_lt_wtp_cap_canonical_product_bound + S ff_i_wtp_cap_canonical_product = m + m) -> exists ff_p_wtp_cap_canonical_product ff_r_wtp_cap_canonical_product ff_s_wtp_cap_canonical_product. ((((exists ff_h_wtp_cap_canonical_product_factor. ff_h_wtp_cap_canonical_product_factor + S (ff_p_wtp_cap_canonical_product) = S ((S (ff_i_wtp_cap_canonical_product)) * d)) /\ exists ff_q_wtp_cap_canonical_product_factor. z = ff_q_wtp_cap_canonical_product_factor * S ((S (ff_i_wtp_cap_canonical_product)) * d) + (ff_p_wtp_cap_canonical_product))) /\ ((((exists ff_h_wtp_cap_canonical_product_partial. ff_h_wtp_cap_canonical_product_partial + S (ff_r_wtp_cap_canonical_product) = S ((S (ff_i_wtp_cap_canonical_product)) * ff_v_wtp_cap_canonical_product)) /\ exists ff_q_wtp_cap_canonical_product_partial. ff_u_wtp_cap_canonical_product = ff_q_wtp_cap_canonical_product_partial * S ((S (ff_i_wtp_cap_canonical_product)) * ff_v_wtp_cap_canonical_product) + (ff_r_wtp_cap_canonical_product))) /\ ((((exists ff_h_wtp_cap_canonical_product_successor. ff_h_wtp_cap_canonical_product_successor + S (ff_s_wtp_cap_canonical_product) = S ((S (S ff_i_wtp_cap_canonical_product)) * ff_v_wtp_cap_canonical_product)) /\ exists ff_q_wtp_cap_canonical_product_successor. ff_u_wtp_cap_canonical_product = ff_q_wtp_cap_canonical_product_successor * S ((S (S ff_i_wtp_cap_canonical_product)) * ff_v_wtp_cap_canonical_product) + (ff_s_wtp_cap_canonical_product))) /\ ff_s_wtp_cap_canonical_product = ff_r_wtp_cap_canonical_product * ff_p_wtp_cap_canonical_product)))))) /\ (P = Q)))))))))))))))))))

Proof neighborhood

Direct theorem prerequisites

PA00B2 prime_pair_order_paired_terminal_state_exists PA00B5 pair_order_state_terminal_coverage PA00BA paired_pair_order_product_one_exists PA00BB pair_order_terminal_state_magnitude_range PA007D beta_magnitude_predecessor_recode_exists PA0030 beta_range_exists PA003X beta_product_exists PA00BD pair_order_terminal_successor_product_eq_range_two

Direct theorem dependents

PA00BF prime_terminal_range_two_product_mod_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

144 script commands · 42 reading checkpoints · 12 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)
prime pair order paired terminal state existspair order state terminal coveragepaired pair order product one existspair order terminal state magnitude rangebeta magnitude predecessor recode existsbeta range existsbeta product existspair order terminal successor product eq range two
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro u
  4. L4
    intro v
  5. L5
    intro r
  6. L6
    intro m
  7. L7
    intro hpn
  8. L8
    intro hp
  9. L9
    intro hinverse
  10. L10
    intro hnr
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hterminal
03Establish hpair_stateL12–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime pair order paired terminal state exists.

  1. L12
    have hpair_state : ∃ b. ∃ c. (∀ x. ∀ y. ∀ z. Lt(x,m + m) → BetaAt(b,c,x,y) → BetaAt(u,v,y,z) → ContainsPrefix(b,c,m + m,z)) ∧ ((∀ x. Lt(x,m + m) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) ∧ ((∀ x. ∀ y. Lt(x,m + m) → BetaAt(b,c,x,y) → ¬y = 0 ∧ ¬S y = n) ∧ InjectivePrefix(b,c,m + m))) ∧ (∀ x. Lt(x,m) → ∃ y. ∃ z. BetaAt(b,c,x + x,y) ∧ (BetaAt(b,c,S (x + x),z) ∧ BetaAt(u,v,y,z)))Definitions: Lt(x,m + m)BetaAt(b,c,x,y)BetaAt(u,v,y,z)ContainsPrefix(b,c,m + m,z)Lt(y,n)InjectivePrefix(b,c,m + m)Lt(x,m)BetaAt(b,c,x + x,y)BetaAt(b,c,S (x + x),z)Original native command in the exact edition
  2. L13
    specialize prime_pair_order_paired_terminal_state_exists p
  3. L14
    specialize prime_pair_order_paired_terminal_state_exists n
  4. L15
    specialize prime_pair_order_paired_terminal_state_exists u
  5. L16
    specialize prime_pair_order_paired_terminal_state_exists v
  6. L17
    specialize prime_pair_order_paired_terminal_state_exists r
  7. L18
    specialize prime_pair_order_paired_terminal_state_exists m
  8. L19
    apply prime_pair_order_paired_terminal_state_exists
  9. L20
    exact hpn
  10. L21
    exact hp
04Use earlier factsL22–24

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

  1. L22
    exact hinverse
  2. L23
    exact hnr
  3. L24
    exact hterminal
05Separate the logical casesL25–27

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

  1. L25
    cases hpair_state
  2. L26
    cases hpair_state_witness
  3. L27
    cases hpair_state_witness_witness
06Establish hstateL28–29

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

  1. L28
    have hstate : (∀ y. ∀ z. ∀ k. Lt(y,m + m) → BetaAt(x,x1,y,z) → BetaAt(u,v,z,k) → ContainsPrefix(x,x1,m + m,k)) ∧ ((∀ y. Lt(y,m + m) → ∃ z. BetaAt(x,x1,y,z) ∧ Lt(z,n)) ∧ ((∀ y. ∀ z. Lt(y,m + m) → BetaAt(x,x1,y,z) → ¬z = 0 ∧ ¬S z = n) ∧ InjectivePrefix(x,x1,m + m)))Definitions: Lt(y,m + m)BetaAt(x,x1,y,z)BetaAt(u,v,z,k)ContainsPrefix(x,x1,m + m,k)Lt(z,n)InjectivePrefix(x,x1,m + m)Original native command in the exact edition
  2. L29
    exact hpair_state_witness_witness_left
07Establish hhistoryL30–31

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

  1. L30
    have hhistory : ∀ wpop_pair_wtp_cap_history_x. Lt(wpop_pair_wtp_cap_history_x,m) → ∃ y. ∃ z. BetaAt(x,x1,wpop_pair_wtp_cap_history_x + wpop_pair_wtp_cap_history_x,y) ∧ (BetaAt(x,x1,S (wpop_pair_wtp_cap_history_x + wpop_pair_wtp_cap_history_x),z) ∧ BetaAt(u,v,y,z))Definitions: Lt(wpop_pair_wtp_cap_history_x,m)BetaAt(x,x1,wpop_pair_wtp_cap_history_x + wpop_pair_wtp_cap_history_x,y)BetaAt(x,x1,S (wpop_pair_wtp_cap_history_x + wpop_pair_wtp_cap_history_x),z)BetaAt(u,v,y,z)Original native command in the exact edition
  2. L31
    exact hpair_state_witness_witness_right
08Establish hstate_partsL32–33

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

  1. L32
    have hstate_parts : (∀ y. ∀ z. ∀ k. Lt(y,m + m) → BetaAt(x,x1,y,z) → BetaAt(u,v,z,k) → ContainsPrefix(x,x1,m + m,k)) ∧ ((∀ y. Lt(y,m + m) → ∃ z. BetaAt(x,x1,y,z) ∧ Lt(z,n)) ∧ ((∀ y. ∀ z. Lt(y,m + m) → BetaAt(x,x1,y,z) → ¬z = 0 ∧ ¬S z = n) ∧ InjectivePrefix(x,x1,m + m)))Definitions: Lt(y,m + m)BetaAt(x,x1,y,z)BetaAt(u,v,z,k)ContainsPrefix(x,x1,m + m,k)Lt(z,n)InjectivePrefix(x,x1,m + m)Original native command in the exact edition
  2. L33
    exact hstate
09Separate the logical casesL34–36

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

  1. L34
    cases hstate_parts
  2. L35
    cases hstate_parts_right
  3. L36
    cases hstate_parts_right_right
10Establish hexact_stateL37–40

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

  1. L37
    have hexact_state : (∀ y. ∀ z. ∀ n. Lt(y,m + m) → BetaAt(x,x1,y,z) → BetaAt(u,v,z,n) → ContainsPrefix(x,x1,m + m,n)) ∧ ((∀ y. Lt(y,m + m) → ∃ z. BetaAt(x,x1,y,z) ∧ Lt(z,S S (m + m))) ∧ ((∀ y. ∀ z. Lt(y,m + m) → BetaAt(x,x1,y,z) → ¬z = 0 ∧ ¬S z = S S (m + m)) ∧ InjectivePrefix(x,x1,m + m)))Definitions: Lt(y,m + m)BetaAt(x,x1,y,z)BetaAt(u,v,z,n)ContainsPrefix(x,x1,m + m,n)Lt(z,S S (m + m))InjectivePrefix(x,x1,m + m)Original native command in the exact edition
  2. L38
    rewrite <- hterminal
  3. L39
    rewrite <- hterminal
  4. L40
    exact hstate
11Establish hcoverageL41–48

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair order state terminal coverage.

  1. L41
    have hcoverage : ∀ s. Lt(s,S S (m + m)) → ¬s = 0 ∧ ¬S s = S S (m + m) → ContainsPrefix(x,x1,m + m,s)Definitions: Lt(s,S S (m + m))ContainsPrefix(x,x1,m + m,s)Original native command in the exact edition
  2. L42
    specialize pair_order_state_terminal_coverage u
  3. L43
    specialize pair_order_state_terminal_coverage v
  4. L44
    specialize pair_order_state_terminal_coverage x
  5. L45
    specialize pair_order_state_terminal_coverage x1
  6. L46
    specialize pair_order_state_terminal_coverage (m + m)
  7. L47
    apply pair_order_state_terminal_coverage
  8. L48
    exact hexact_state
12Establish hrangeL49–58

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair order terminal state magnitude range.

  1. L49
    have hrange : ∀ gmp_index_wtp_cap_range. Lt(gmp_index_wtp_cap_range,m + m) → ∃ y. BetaAt(x,x1,gmp_index_wtp_cap_range,y) ∧ (Lt(0,y) ∧ Le(y,m + m))Definitions: Lt(gmp_index_wtp_cap_range,m + m)BetaAt(x,x1,gmp_index_wtp_cap_range,y)Lt(0,y)Le(y,m + m)Original native command in the exact edition
  2. L50
    specialize pair_order_terminal_state_magnitude_range u
  3. L51
    specialize pair_order_terminal_state_magnitude_range v
  4. L52
    specialize pair_order_terminal_state_magnitude_range x
  5. L53
    specialize pair_order_terminal_state_magnitude_range x1
  6. L54
    specialize pair_order_terminal_state_magnitude_range (m + m)
  7. L55
    specialize pair_order_terminal_state_magnitude_range n
  8. L56
    apply pair_order_terminal_state_magnitude_range
  9. L57
    exact hterminal
  10. L58
    exact hstate
13Establish hfactor_productL59–68

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply paired pair order product one exists.

  1. L59
    have hfactor_product : ∃ f. ∃ g. ∃ Q. (∀ y. ∀ z. Lt(y,m + m) → BetaAt(x,x1,y,z) → BetaAt(f,g,y,S z)) ∧ ((∀ y. ∀ z. ∀ n. Lt(y,m) → BetaAt(f,g,y + y,z) → BetaAt(f,g,S (y + y),n) → BalancedInverse(p,z,n)) ∧ (Product(f,g,m + m,Q) ∧ ModEq(p,Q,1)))Definitions: Lt(y,m + m)BetaAt(x,x1,y,z)BetaAt(f,g,y,S z)Lt(y,m)BetaAt(f,g,y + y,z)BetaAt(f,g,S (y + y),n)BalancedInverse(p,z,n)Product(f,g,m + m,Q)ModEq(p,Q,1)Original native command in the exact edition
  2. L60
    specialize paired_pair_order_product_one_exists p
  3. L61
    specialize paired_pair_order_product_one_exists n
  4. L62
    specialize paired_pair_order_product_one_exists u
  5. L63
    specialize paired_pair_order_product_one_exists v
  6. L64
    specialize paired_pair_order_product_one_exists x
  7. L65
    specialize paired_pair_order_product_one_exists x1
  8. L66
    specialize paired_pair_order_product_one_exists m
  9. L67
    apply paired_pair_order_product_one_exists
  10. L68
    exact hinverse
14Use earlier factsL69–70

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

  1. L69
    exact hstate_parts_right_left
  2. L70
    exact hhistory
15Separate the logical casesL71–76

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

  1. L71
    cases hfactor_product
  2. L72
    cases hfactor_product_witness
  3. L73
    cases hfactor_product_witness_witness
  4. L74
    cases hfactor_product_witness_witness_witness
  5. L75
    cases hfactor_product_witness_witness_witness_right
  6. L76
    cases hfactor_product_witness_witness_witness_right_right
16Establish hcanonical_range_existsL77–80

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

  1. L77
    have hcanonical_range_exists : ∃ z. ∃ d. Range(z,d,2,m + m)Definitions: Range(z,d,2,m + m)Original native command in the exact edition
  2. L78
    specialize beta_range_exists 2
  3. L79
    specialize beta_range_exists (m + m)
  4. L80
    exact beta_range_exists
17Separate the logical casesL81–82

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

  1. L81
    cases hcanonical_range_exists
  2. L82
    cases hcanonical_range_exists_witness
18Establish hcanonical_product_existsL83–87

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

  1. L83
    have hcanonical_product_exists : ∃ P. Product(x5,x6,m + m,P)Definitions: Product(x5,x6,m + m,P)Original native command in the exact edition
  2. L84
    specialize beta_product_exists x5
  3. L85
    specialize beta_product_exists x6
  4. L86
    specialize beta_product_exists (m + m)
  5. L87
    exact beta_product_exists
19Separate the logical casesL88–88

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

  1. L88
    cases hcanonical_product_exists
20Establish hrecode_existsL89–95

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta magnitude predecessor recode exists.

  1. L89
    have hrecode_exists : ∃ rb. ∃ rc. ∀ gmp_index_wtp_cap_recode. ∀ gmp_predecessor_wtp_cap_recode. Lt(gmp_index_wtp_cap_recode,m + m) → BetaAt(x,x1,gmp_index_wtp_cap_recode,S gmp_predecessor_wtp_cap_recode) → BetaAt(rb,rc,gmp_index_wtp_cap_recode,gmp_predecessor_wtp_cap_recode)Definitions: Lt(gmp_index_wtp_cap_recode,m + m)BetaAt(x,x1,gmp_index_wtp_cap_recode,S gmp_predecessor_wtp_cap_recode)BetaAt(rb,rc,gmp_index_wtp_cap_recode,gmp_predecessor_wtp_cap_recode)Original native command in the exact edition
  2. L90
    specialize beta_magnitude_predecessor_recode_exists x
  3. L91
    specialize beta_magnitude_predecessor_recode_exists x1
  4. L92
    specialize beta_magnitude_predecessor_recode_exists (m + m)
  5. L93
    specialize beta_magnitude_predecessor_recode_exists (m + m)
  6. L94
    apply beta_magnitude_predecessor_recode_exists
  7. L95
    exact hrange
21Separate the logical casesL96–97

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

  1. L96
    cases hrecode_exists
  2. L97
    cases hrecode_exists_witness
22Establish hequalL98–107

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

  1. L98
    have hequal : x7 = x4
  2. L99
    specialize pair_order_terminal_successor_product_eq_range_two x
  3. L100
    specialize pair_order_terminal_successor_product_eq_range_two x1
  4. L101
    specialize pair_order_terminal_successor_product_eq_range_two x8
  5. L102
    specialize pair_order_terminal_successor_product_eq_range_two x9
  6. L103
    specialize pair_order_terminal_successor_product_eq_range_two x5
  7. L104
    specialize pair_order_terminal_successor_product_eq_range_two x6
  8. L105
    specialize pair_order_terminal_successor_product_eq_range_two x2
  9. L106
    specialize pair_order_terminal_successor_product_eq_range_two x3
  10. L107
    specialize pair_order_terminal_successor_product_eq_range_two (m + m)
23Use earlier factsL108–117

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

  1. L108
    specialize pair_order_terminal_successor_product_eq_range_two x7
  2. L109
    specialize pair_order_terminal_successor_product_eq_range_two x4
  3. L110
    apply pair_order_terminal_successor_product_eq_range_two
  4. L111
    exact hrange
  5. L112
    exact hstate_parts_right_right_right
  6. L113
    exact hrecode_exists_witness_witness
  7. L114
    exact hfactor_product_witness_witness_witness_left
  8. L115
    exact hcanonical_range_exists_witness_witness
  9. L116
    exact hcanonical_product_exists_witness
  10. L117
    exact hfactor_product_witness_witness_witness_right_right_left
24Construct an explicit witnessL118–125

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

  1. L118
    exists x
  2. L119
    exists x1
  3. L120
    exists x2
  4. L121
    exists x3
  5. L122
    exists x4
  6. L123
    exists x5
  7. L124
    exists x6
  8. L125
    exists x7
25Separate the logical casesL126–126

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

  1. L126
    split
26Use earlier factsL127–127

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

  1. L127
    exact hstate
27Separate the logical casesL128–128

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

  1. L128
    split
28Use earlier factsL129–129

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

  1. L129
    exact hhistory
29Separate the logical casesL130–130

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

  1. L130
    split
30Use earlier factsL131–131

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

  1. L131
    exact hcoverage
31Separate the logical casesL132–132

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

  1. L132
    split
32Use earlier factsL133–133

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

  1. L133
    exact hfactor_product_witness_witness_witness_left
33Separate the logical casesL134–134

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

  1. L134
    split
34Use earlier factsL135–135

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

  1. L135
    exact hfactor_product_witness_witness_witness_right_left
35Separate the logical casesL136–136

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

  1. L136
    split
36Use earlier factsL137–137

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

  1. L137
    exact hfactor_product_witness_witness_witness_right_right_left
37Separate the logical casesL138–138

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

  1. L138
    split
38Use earlier factsL139–139

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

  1. L139
    exact hfactor_product_witness_witness_witness_right_right_right
39Separate the logical casesL140–140

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

  1. L140
    split
40Use earlier factsL141–141

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

  1. L141
    exact hcanonical_range_exists_witness_witness
41Separate the logical casesL142–142

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

  1. L142
    split
42Use earlier factsL143–144

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

  1. L143
    exact hcanonical_product_exists_witness
  2. L144
    exact hequal

Library-wide reading audit

Original defined command ledger · 144 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro u
  4. 0004intro v
  5. 0005intro r
  6. 0006intro m
  7. 0007intro hpn
  8. 0008intro hp
  9. 0009intro hinverse
  10. 0010intro hnr
  11. 0011intro hterminal
  12. 0012have hpair_state : ∃ b. ∃ c. (∀ x. ∀ y. ∀ z. Lt(x,m + m) → BetaAt(b,c,x,y) → BetaAt(u,v,y,z) → ContainsPrefix(b,c,m + m,z)) ∧ ((∀ x. Lt(x,m + m) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) ∧ ((∀ x. ∀ y. Lt(x,m + m) → BetaAt(b,c,x,y) → ¬y = 0 ∧ ¬S y = n) ∧ InjectivePrefix(b,c,m + m))) ∧ (∀ x. Lt(x,m) → ∃ y. ∃ z. BetaAt(b,c,x + x,y) ∧ (BetaAt(b,c,S (x + x),z) ∧ BetaAt(u,v,y,z)))
    Exact native replay linehave hpair_state : exists b c. ((((forall wpo_position_wtp_cap_state_closed wpo_source_wtp_cap_state_closed wpo_mate_wtp_cap_state_closed. (exists wpo_gap_wtp_cap_state_closed_position_bound. wpo_gap_wtp_cap_state_closed_position_bound + S (wpo_position_wtp_cap_state_closed) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_closed_source_entry. wpo_beta_height_wtp_cap_state_closed_source_entry + S (wpo_source_wtp_cap_state_closed) = S ((S (wpo_position_wtp_cap_state_closed)) * c)) /\ exists wpo_beta_quotient_wtp_cap_state_closed_source_entry. b = wpo_beta_quotient_wtp_cap_state_closed_source_entry * S ((S (wpo_position_wtp_cap_state_closed)) * c) + (wpo_source_wtp_cap_state_closed))) -> (((exists wpo_beta_height_wtp_cap_state_closed_inverse_entry. wpo_beta_height_wtp_cap_state_closed_inverse_entry + S (wpo_mate_wtp_cap_state_closed) = S ((S (wpo_source_wtp_cap_state_closed)) * v)) /\ exists wpo_beta_quotient_wtp_cap_state_closed_inverse_entry. u = wpo_beta_quotient_wtp_cap_state_closed_inverse_entry * S ((S (wpo_source_wtp_cap_state_closed)) * v) + (wpo_mate_wtp_cap_state_closed))) -> exists wpo_mate_position_wtp_cap_state_closed. ((exists wpo_gap_wtp_cap_state_closed_mate_bound. wpo_gap_wtp_cap_state_closed_mate_bound + S (wpo_mate_position_wtp_cap_state_closed) = m + m) /\ (((exists wpo_beta_height_wtp_cap_state_closed_mate_entry. wpo_beta_height_wtp_cap_state_closed_mate_entry + S (wpo_mate_wtp_cap_state_closed) = S ((S (wpo_mate_position_wtp_cap_state_closed)) * c)) /\ exists wpo_beta_quotient_wtp_cap_state_closed_mate_entry. b = wpo_beta_quotient_wtp_cap_state_closed_mate_entry * S ((S (wpo_mate_position_wtp_cap_state_closed)) * c) + (wpo_mate_wtp_cap_state_closed))))) /\ ((forall fom_index_wtp_cap_state_bounded. (exists fom_gap_wtp_cap_state_bounded_index_bound. fom_gap_wtp_cap_state_bounded_index_bound + S (fom_index_wtp_cap_state_bounded) = m + m) -> exists fom_value_wtp_cap_state_bounded. ((((exists fom_beta_height_wtp_cap_state_bounded_entry. fom_beta_height_wtp_cap_state_bounded_entry + S (fom_value_wtp_cap_state_bounded) = S ((S (fom_index_wtp_cap_state_bounded)) * c)) /\ exists fom_beta_quotient_wtp_cap_state_bounded_entry. b = fom_beta_quotient_wtp_cap_state_bounded_entry * S ((S (fom_index_wtp_cap_state_bounded)) * c) + (fom_value_wtp_cap_state_bounded))) /\ (exists fom_gap_wtp_cap_state_bounded_value_bound. fom_gap_wtp_cap_state_bounded_value_bound + S (fom_value_wtp_cap_state_bounded) = n))) /\ ((forall wpo_position_wtp_cap_state_nonendpoint wpo_value_wtp_cap_state_nonendpoint. (exists wpo_gap_wtp_cap_state_nonendpoint_position_bound. wpo_gap_wtp_cap_state_nonendpoint_position_bound + S (wpo_position_wtp_cap_state_nonendpoint) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_nonendpoint_entry. wpo_beta_height_wtp_cap_state_nonendpoint_entry + S (wpo_value_wtp_cap_state_nonendpoint) = S ((S (wpo_position_wtp_cap_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wtp_cap_state_nonendpoint_entry. b = wpo_beta_quotient_wtp_cap_state_nonendpoint_entry * S ((S (wpo_position_wtp_cap_state_nonendpoint)) * c) + (wpo_value_wtp_cap_state_nonendpoint))) -> (~(wpo_value_wtp_cap_state_nonendpoint = 0) /\ ~((S wpo_value_wtp_cap_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wtp_cap_state_injective wpo_injective_right_wtp_cap_state_injective wpo_injective_value_wtp_cap_state_injective. (exists wpo_gap_wtp_cap_state_injective_left_bound. wpo_gap_wtp_cap_state_injective_left_bound + S (wpo_injective_left_wtp_cap_state_injective) = m + m) -> (exists wpo_gap_wtp_cap_state_injective_right_bound. wpo_gap_wtp_cap_state_injective_right_bound + S (wpo_injective_right_wtp_cap_state_injective) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_injective_left_entry. wpo_beta_height_wtp_cap_state_injective_left_entry + S (wpo_injective_value_wtp_cap_state_injective) = S ((S (wpo_injective_left_wtp_cap_state_injective)) * c)) /\ exists wpo_beta_quotient_wtp_cap_state_injective_left_entry. b = wpo_beta_quotient_wtp_cap_state_injective_left_entry * S ((S (wpo_injective_left_wtp_cap_state_injective)) * c) + (wpo_injective_value_wtp_cap_state_injective))) -> (((exists wpo_beta_height_wtp_cap_state_injective_right_entry. wpo_beta_height_wtp_cap_state_injective_right_entry + S (wpo_injective_value_wtp_cap_state_injective) = S ((S (wpo_injective_right_wtp_cap_state_injective)) * c)) /\ exists wpo_beta_quotient_wtp_cap_state_injective_right_entry. b = wpo_beta_quotient_wtp_cap_state_injective_right_entry * S ((S (wpo_injective_right_wtp_cap_state_injective)) * c) + (wpo_injective_value_wtp_cap_state_injective))) -> wpo_injective_left_wtp_cap_state_injective = wpo_injective_right_wtp_cap_state_injective))))) /\ (forall wpop_pair_wtp_cap_history. (exists wpo_gap_wtp_cap_history_pair_bound. wpo_gap_wtp_cap_history_pair_bound + S (wpop_pair_wtp_cap_history) = m) -> exists wpop_left_wtp_cap_history wpop_right_wtp_cap_history. ((((exists wpo_beta_height_wtp_cap_history_left_entry. wpo_beta_height_wtp_cap_history_left_entry + S (wpop_left_wtp_cap_history) = S ((S (wpop_pair_wtp_cap_history + wpop_pair_wtp_cap_history)) * c)) /\ exists wpo_beta_quotient_wtp_cap_history_left_entry. b = wpo_beta_quotient_wtp_cap_history_left_entry * S ((S (wpop_pair_wtp_cap_history + wpop_pair_wtp_cap_history)) * c) + (wpop_left_wtp_cap_history))) /\ ((((exists wpo_beta_height_wtp_cap_history_right_entry. wpo_beta_height_wtp_cap_history_right_entry + S (wpop_right_wtp_cap_history) = S ((S (S (wpop_pair_wtp_cap_history + wpop_pair_wtp_cap_history))) * c)) /\ exists wpo_beta_quotient_wtp_cap_history_right_entry. b = wpo_beta_quotient_wtp_cap_history_right_entry * S ((S (S (wpop_pair_wtp_cap_history + wpop_pair_wtp_cap_history))) * c) + (wpop_right_wtp_cap_history))) /\ (((exists wpo_beta_height_wtp_cap_history_inverse_entry. wpo_beta_height_wtp_cap_history_inverse_entry + S (wpop_right_wtp_cap_history) = S ((S (wpop_left_wtp_cap_history)) * v)) /\ exists wpo_beta_quotient_wtp_cap_history_inverse_entry. u = wpo_beta_quotient_wtp_cap_history_inverse_entry * S ((S (wpop_left_wtp_cap_history)) * v) + (wpop_right_wtp_cap_history)))))))
  13. 0013specialize prime_pair_order_paired_terminal_state_exists p
  14. 0014specialize prime_pair_order_paired_terminal_state_exists n
  15. 0015specialize prime_pair_order_paired_terminal_state_exists u
  16. 0016specialize prime_pair_order_paired_terminal_state_exists v
  17. 0017specialize prime_pair_order_paired_terminal_state_exists r
  18. 0018specialize prime_pair_order_paired_terminal_state_exists m
  19. 0019apply prime_pair_order_paired_terminal_state_exists
  20. 0020exact hpn
  21. 0021exact hp
  22. 0022exact hinverse
  23. 0023exact hnr
  24. 0024exact hterminal
  25. 0025cases hpair_state
  26. 0026cases hpair_state_witness
  27. 0027cases hpair_state_witness_witness
  28. 0028have hstate : (∀ y. ∀ z. ∀ k. Lt(y,m + m) → BetaAt(x,x1,y,z) → BetaAt(u,v,z,k) → ContainsPrefix(x,x1,m + m,k)) ∧ ((∀ y. Lt(y,m + m) → ∃ z. BetaAt(x,x1,y,z) ∧ Lt(z,n)) ∧ ((∀ y. ∀ z. Lt(y,m + m) → BetaAt(x,x1,y,z) → ¬z = 0 ∧ ¬S z = n) ∧ InjectivePrefix(x,x1,m + m)))
    Exact native replay linehave hstate : ((forall wpo_position_wtp_cap_state_x_closed wpo_source_wtp_cap_state_x_closed wpo_mate_wtp_cap_state_x_closed. (exists wpo_gap_wtp_cap_state_x_closed_position_bound. wpo_gap_wtp_cap_state_x_closed_position_bound + S (wpo_position_wtp_cap_state_x_closed) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_x_closed_source_entry. wpo_beta_height_wtp_cap_state_x_closed_source_entry + S (wpo_source_wtp_cap_state_x_closed) = S ((S (wpo_position_wtp_cap_state_x_closed)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_closed_source_entry. x = wpo_beta_quotient_wtp_cap_state_x_closed_source_entry * S ((S (wpo_position_wtp_cap_state_x_closed)) * x1) + (wpo_source_wtp_cap_state_x_closed))) -> (((exists wpo_beta_height_wtp_cap_state_x_closed_inverse_entry. wpo_beta_height_wtp_cap_state_x_closed_inverse_entry + S (wpo_mate_wtp_cap_state_x_closed) = S ((S (wpo_source_wtp_cap_state_x_closed)) * v)) /\ exists wpo_beta_quotient_wtp_cap_state_x_closed_inverse_entry. u = wpo_beta_quotient_wtp_cap_state_x_closed_inverse_entry * S ((S (wpo_source_wtp_cap_state_x_closed)) * v) + (wpo_mate_wtp_cap_state_x_closed))) -> exists wpo_mate_position_wtp_cap_state_x_closed. ((exists wpo_gap_wtp_cap_state_x_closed_mate_bound. wpo_gap_wtp_cap_state_x_closed_mate_bound + S (wpo_mate_position_wtp_cap_state_x_closed) = m + m) /\ (((exists wpo_beta_height_wtp_cap_state_x_closed_mate_entry. wpo_beta_height_wtp_cap_state_x_closed_mate_entry + S (wpo_mate_wtp_cap_state_x_closed) = S ((S (wpo_mate_position_wtp_cap_state_x_closed)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_closed_mate_entry. x = wpo_beta_quotient_wtp_cap_state_x_closed_mate_entry * S ((S (wpo_mate_position_wtp_cap_state_x_closed)) * x1) + (wpo_mate_wtp_cap_state_x_closed))))) /\ ((forall fom_index_wtp_cap_state_x_bounded. (exists fom_gap_wtp_cap_state_x_bounded_index_bound. fom_gap_wtp_cap_state_x_bounded_index_bound + S (fom_index_wtp_cap_state_x_bounded) = m + m) -> exists fom_value_wtp_cap_state_x_bounded. ((((exists fom_beta_height_wtp_cap_state_x_bounded_entry. fom_beta_height_wtp_cap_state_x_bounded_entry + S (fom_value_wtp_cap_state_x_bounded) = S ((S (fom_index_wtp_cap_state_x_bounded)) * x1)) /\ exists fom_beta_quotient_wtp_cap_state_x_bounded_entry. x = fom_beta_quotient_wtp_cap_state_x_bounded_entry * S ((S (fom_index_wtp_cap_state_x_bounded)) * x1) + (fom_value_wtp_cap_state_x_bounded))) /\ (exists fom_gap_wtp_cap_state_x_bounded_value_bound. fom_gap_wtp_cap_state_x_bounded_value_bound + S (fom_value_wtp_cap_state_x_bounded) = n))) /\ ((forall wpo_position_wtp_cap_state_x_nonendpoint wpo_value_wtp_cap_state_x_nonendpoint. (exists wpo_gap_wtp_cap_state_x_nonendpoint_position_bound. wpo_gap_wtp_cap_state_x_nonendpoint_position_bound + S (wpo_position_wtp_cap_state_x_nonendpoint) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_x_nonendpoint_entry. wpo_beta_height_wtp_cap_state_x_nonendpoint_entry + S (wpo_value_wtp_cap_state_x_nonendpoint) = S ((S (wpo_position_wtp_cap_state_x_nonendpoint)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_nonendpoint_entry. x = wpo_beta_quotient_wtp_cap_state_x_nonendpoint_entry * S ((S (wpo_position_wtp_cap_state_x_nonendpoint)) * x1) + (wpo_value_wtp_cap_state_x_nonendpoint))) -> (~(wpo_value_wtp_cap_state_x_nonendpoint = 0) /\ ~((S wpo_value_wtp_cap_state_x_nonendpoint) = n))) /\ (forall wpo_injective_left_wtp_cap_state_x_injective wpo_injective_right_wtp_cap_state_x_injective wpo_injective_value_wtp_cap_state_x_injective. (exists wpo_gap_wtp_cap_state_x_injective_left_bound. wpo_gap_wtp_cap_state_x_injective_left_bound + S (wpo_injective_left_wtp_cap_state_x_injective) = m + m) -> (exists wpo_gap_wtp_cap_state_x_injective_right_bound. wpo_gap_wtp_cap_state_x_injective_right_bound + S (wpo_injective_right_wtp_cap_state_x_injective) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_x_injective_left_entry. wpo_beta_height_wtp_cap_state_x_injective_left_entry + S (wpo_injective_value_wtp_cap_state_x_injective) = S ((S (wpo_injective_left_wtp_cap_state_x_injective)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_injective_left_entry. x = wpo_beta_quotient_wtp_cap_state_x_injective_left_entry * S ((S (wpo_injective_left_wtp_cap_state_x_injective)) * x1) + (wpo_injective_value_wtp_cap_state_x_injective))) -> (((exists wpo_beta_height_wtp_cap_state_x_injective_right_entry. wpo_beta_height_wtp_cap_state_x_injective_right_entry + S (wpo_injective_value_wtp_cap_state_x_injective) = S ((S (wpo_injective_right_wtp_cap_state_x_injective)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_injective_right_entry. x = wpo_beta_quotient_wtp_cap_state_x_injective_right_entry * S ((S (wpo_injective_right_wtp_cap_state_x_injective)) * x1) + (wpo_injective_value_wtp_cap_state_x_injective))) -> wpo_injective_left_wtp_cap_state_x_injective = wpo_injective_right_wtp_cap_state_x_injective))))
  29. 0029exact hpair_state_witness_witness_left
  30. 0030have hhistory : ∀ wpop_pair_wtp_cap_history_x. Lt(wpop_pair_wtp_cap_history_x,m) → ∃ y. ∃ z. BetaAt(x,x1,wpop_pair_wtp_cap_history_x + wpop_pair_wtp_cap_history_x,y) ∧ (BetaAt(x,x1,S (wpop_pair_wtp_cap_history_x + wpop_pair_wtp_cap_history_x),z) ∧ BetaAt(u,v,y,z))
    Exact native replay linehave hhistory : forall wpop_pair_wtp_cap_history_x. (exists wpo_gap_wtp_cap_history_x_pair_bound. wpo_gap_wtp_cap_history_x_pair_bound + S (wpop_pair_wtp_cap_history_x) = m) -> exists wpop_left_wtp_cap_history_x wpop_right_wtp_cap_history_x. ((((exists wpo_beta_height_wtp_cap_history_x_left_entry. wpo_beta_height_wtp_cap_history_x_left_entry + S (wpop_left_wtp_cap_history_x) = S ((S (wpop_pair_wtp_cap_history_x + wpop_pair_wtp_cap_history_x)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_history_x_left_entry. x = wpo_beta_quotient_wtp_cap_history_x_left_entry * S ((S (wpop_pair_wtp_cap_history_x + wpop_pair_wtp_cap_history_x)) * x1) + (wpop_left_wtp_cap_history_x))) /\ ((((exists wpo_beta_height_wtp_cap_history_x_right_entry. wpo_beta_height_wtp_cap_history_x_right_entry + S (wpop_right_wtp_cap_history_x) = S ((S (S (wpop_pair_wtp_cap_history_x + wpop_pair_wtp_cap_history_x))) * x1)) /\ exists wpo_beta_quotient_wtp_cap_history_x_right_entry. x = wpo_beta_quotient_wtp_cap_history_x_right_entry * S ((S (S (wpop_pair_wtp_cap_history_x + wpop_pair_wtp_cap_history_x))) * x1) + (wpop_right_wtp_cap_history_x))) /\ (((exists wpo_beta_height_wtp_cap_history_x_inverse_entry. wpo_beta_height_wtp_cap_history_x_inverse_entry + S (wpop_right_wtp_cap_history_x) = S ((S (wpop_left_wtp_cap_history_x)) * v)) /\ exists wpo_beta_quotient_wtp_cap_history_x_inverse_entry. u = wpo_beta_quotient_wtp_cap_history_x_inverse_entry * S ((S (wpop_left_wtp_cap_history_x)) * v) + (wpop_right_wtp_cap_history_x)))))
  31. 0031exact hpair_state_witness_witness_right
  32. 0032have hstate_parts : (∀ y. ∀ z. ∀ k. Lt(y,m + m) → BetaAt(x,x1,y,z) → BetaAt(u,v,z,k) → ContainsPrefix(x,x1,m + m,k)) ∧ ((∀ y. Lt(y,m + m) → ∃ z. BetaAt(x,x1,y,z) ∧ Lt(z,n)) ∧ ((∀ y. ∀ z. Lt(y,m + m) → BetaAt(x,x1,y,z) → ¬z = 0 ∧ ¬S z = n) ∧ InjectivePrefix(x,x1,m + m)))
    Exact native replay linehave hstate_parts : ((forall wpo_position_wtp_cap_state_x_closed wpo_source_wtp_cap_state_x_closed wpo_mate_wtp_cap_state_x_closed. (exists wpo_gap_wtp_cap_state_x_closed_position_bound. wpo_gap_wtp_cap_state_x_closed_position_bound + S (wpo_position_wtp_cap_state_x_closed) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_x_closed_source_entry. wpo_beta_height_wtp_cap_state_x_closed_source_entry + S (wpo_source_wtp_cap_state_x_closed) = S ((S (wpo_position_wtp_cap_state_x_closed)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_closed_source_entry. x = wpo_beta_quotient_wtp_cap_state_x_closed_source_entry * S ((S (wpo_position_wtp_cap_state_x_closed)) * x1) + (wpo_source_wtp_cap_state_x_closed))) -> (((exists wpo_beta_height_wtp_cap_state_x_closed_inverse_entry. wpo_beta_height_wtp_cap_state_x_closed_inverse_entry + S (wpo_mate_wtp_cap_state_x_closed) = S ((S (wpo_source_wtp_cap_state_x_closed)) * v)) /\ exists wpo_beta_quotient_wtp_cap_state_x_closed_inverse_entry. u = wpo_beta_quotient_wtp_cap_state_x_closed_inverse_entry * S ((S (wpo_source_wtp_cap_state_x_closed)) * v) + (wpo_mate_wtp_cap_state_x_closed))) -> exists wpo_mate_position_wtp_cap_state_x_closed. ((exists wpo_gap_wtp_cap_state_x_closed_mate_bound. wpo_gap_wtp_cap_state_x_closed_mate_bound + S (wpo_mate_position_wtp_cap_state_x_closed) = m + m) /\ (((exists wpo_beta_height_wtp_cap_state_x_closed_mate_entry. wpo_beta_height_wtp_cap_state_x_closed_mate_entry + S (wpo_mate_wtp_cap_state_x_closed) = S ((S (wpo_mate_position_wtp_cap_state_x_closed)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_closed_mate_entry. x = wpo_beta_quotient_wtp_cap_state_x_closed_mate_entry * S ((S (wpo_mate_position_wtp_cap_state_x_closed)) * x1) + (wpo_mate_wtp_cap_state_x_closed))))) /\ ((forall fom_index_wtp_cap_state_x_bounded. (exists fom_gap_wtp_cap_state_x_bounded_index_bound. fom_gap_wtp_cap_state_x_bounded_index_bound + S (fom_index_wtp_cap_state_x_bounded) = m + m) -> exists fom_value_wtp_cap_state_x_bounded. ((((exists fom_beta_height_wtp_cap_state_x_bounded_entry. fom_beta_height_wtp_cap_state_x_bounded_entry + S (fom_value_wtp_cap_state_x_bounded) = S ((S (fom_index_wtp_cap_state_x_bounded)) * x1)) /\ exists fom_beta_quotient_wtp_cap_state_x_bounded_entry. x = fom_beta_quotient_wtp_cap_state_x_bounded_entry * S ((S (fom_index_wtp_cap_state_x_bounded)) * x1) + (fom_value_wtp_cap_state_x_bounded))) /\ (exists fom_gap_wtp_cap_state_x_bounded_value_bound. fom_gap_wtp_cap_state_x_bounded_value_bound + S (fom_value_wtp_cap_state_x_bounded) = n))) /\ ((forall wpo_position_wtp_cap_state_x_nonendpoint wpo_value_wtp_cap_state_x_nonendpoint. (exists wpo_gap_wtp_cap_state_x_nonendpoint_position_bound. wpo_gap_wtp_cap_state_x_nonendpoint_position_bound + S (wpo_position_wtp_cap_state_x_nonendpoint) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_x_nonendpoint_entry. wpo_beta_height_wtp_cap_state_x_nonendpoint_entry + S (wpo_value_wtp_cap_state_x_nonendpoint) = S ((S (wpo_position_wtp_cap_state_x_nonendpoint)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_nonendpoint_entry. x = wpo_beta_quotient_wtp_cap_state_x_nonendpoint_entry * S ((S (wpo_position_wtp_cap_state_x_nonendpoint)) * x1) + (wpo_value_wtp_cap_state_x_nonendpoint))) -> (~(wpo_value_wtp_cap_state_x_nonendpoint = 0) /\ ~((S wpo_value_wtp_cap_state_x_nonendpoint) = n))) /\ (forall wpo_injective_left_wtp_cap_state_x_injective wpo_injective_right_wtp_cap_state_x_injective wpo_injective_value_wtp_cap_state_x_injective. (exists wpo_gap_wtp_cap_state_x_injective_left_bound. wpo_gap_wtp_cap_state_x_injective_left_bound + S (wpo_injective_left_wtp_cap_state_x_injective) = m + m) -> (exists wpo_gap_wtp_cap_state_x_injective_right_bound. wpo_gap_wtp_cap_state_x_injective_right_bound + S (wpo_injective_right_wtp_cap_state_x_injective) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_x_injective_left_entry. wpo_beta_height_wtp_cap_state_x_injective_left_entry + S (wpo_injective_value_wtp_cap_state_x_injective) = S ((S (wpo_injective_left_wtp_cap_state_x_injective)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_injective_left_entry. x = wpo_beta_quotient_wtp_cap_state_x_injective_left_entry * S ((S (wpo_injective_left_wtp_cap_state_x_injective)) * x1) + (wpo_injective_value_wtp_cap_state_x_injective))) -> (((exists wpo_beta_height_wtp_cap_state_x_injective_right_entry. wpo_beta_height_wtp_cap_state_x_injective_right_entry + S (wpo_injective_value_wtp_cap_state_x_injective) = S ((S (wpo_injective_right_wtp_cap_state_x_injective)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_injective_right_entry. x = wpo_beta_quotient_wtp_cap_state_x_injective_right_entry * S ((S (wpo_injective_right_wtp_cap_state_x_injective)) * x1) + (wpo_injective_value_wtp_cap_state_x_injective))) -> wpo_injective_left_wtp_cap_state_x_injective = wpo_injective_right_wtp_cap_state_x_injective))))
  33. 0033exact hstate
  34. 0034cases hstate_parts
  35. 0035cases hstate_parts_right
  36. 0036cases hstate_parts_right_right
  37. 0037have hexact_state : (∀ y. ∀ z. ∀ n. Lt(y,m + m) → BetaAt(x,x1,y,z) → BetaAt(u,v,z,n) → ContainsPrefix(x,x1,m + m,n)) ∧ ((∀ y. Lt(y,m + m) → ∃ z. BetaAt(x,x1,y,z) ∧ Lt(z,S S (m + m))) ∧ ((∀ y. ∀ z. Lt(y,m + m) → BetaAt(x,x1,y,z) → ¬z = 0 ∧ ¬S z = S S (m + m)) ∧ InjectivePrefix(x,x1,m + m)))
    Exact native replay linehave hexact_state : ((forall wpo_position_wtp_cap_exact_state_x_closed wpo_source_wtp_cap_exact_state_x_closed wpo_mate_wtp_cap_exact_state_x_closed. (exists wpo_gap_wtp_cap_exact_state_x_closed_position_bound. wpo_gap_wtp_cap_exact_state_x_closed_position_bound + S (wpo_position_wtp_cap_exact_state_x_closed) = m + m) -> (((exists wpo_beta_height_wtp_cap_exact_state_x_closed_source_entry. wpo_beta_height_wtp_cap_exact_state_x_closed_source_entry + S (wpo_source_wtp_cap_exact_state_x_closed) = S ((S (wpo_position_wtp_cap_exact_state_x_closed)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_exact_state_x_closed_source_entry. x = wpo_beta_quotient_wtp_cap_exact_state_x_closed_source_entry * S ((S (wpo_position_wtp_cap_exact_state_x_closed)) * x1) + (wpo_source_wtp_cap_exact_state_x_closed))) -> (((exists wpo_beta_height_wtp_cap_exact_state_x_closed_inverse_entry. wpo_beta_height_wtp_cap_exact_state_x_closed_inverse_entry + S (wpo_mate_wtp_cap_exact_state_x_closed) = S ((S (wpo_source_wtp_cap_exact_state_x_closed)) * v)) /\ exists wpo_beta_quotient_wtp_cap_exact_state_x_closed_inverse_entry. u = wpo_beta_quotient_wtp_cap_exact_state_x_closed_inverse_entry * S ((S (wpo_source_wtp_cap_exact_state_x_closed)) * v) + (wpo_mate_wtp_cap_exact_state_x_closed))) -> exists wpo_mate_position_wtp_cap_exact_state_x_closed. ((exists wpo_gap_wtp_cap_exact_state_x_closed_mate_bound. wpo_gap_wtp_cap_exact_state_x_closed_mate_bound + S (wpo_mate_position_wtp_cap_exact_state_x_closed) = m + m) /\ (((exists wpo_beta_height_wtp_cap_exact_state_x_closed_mate_entry. wpo_beta_height_wtp_cap_exact_state_x_closed_mate_entry + S (wpo_mate_wtp_cap_exact_state_x_closed) = S ((S (wpo_mate_position_wtp_cap_exact_state_x_closed)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_exact_state_x_closed_mate_entry. x = wpo_beta_quotient_wtp_cap_exact_state_x_closed_mate_entry * S ((S (wpo_mate_position_wtp_cap_exact_state_x_closed)) * x1) + (wpo_mate_wtp_cap_exact_state_x_closed))))) /\ ((forall fom_index_wtp_cap_exact_state_x_bounded. (exists fom_gap_wtp_cap_exact_state_x_bounded_index_bound. fom_gap_wtp_cap_exact_state_x_bounded_index_bound + S (fom_index_wtp_cap_exact_state_x_bounded) = m + m) -> exists fom_value_wtp_cap_exact_state_x_bounded. ((((exists fom_beta_height_wtp_cap_exact_state_x_bounded_entry. fom_beta_height_wtp_cap_exact_state_x_bounded_entry + S (fom_value_wtp_cap_exact_state_x_bounded) = S ((S (fom_index_wtp_cap_exact_state_x_bounded)) * x1)) /\ exists fom_beta_quotient_wtp_cap_exact_state_x_bounded_entry. x = fom_beta_quotient_wtp_cap_exact_state_x_bounded_entry * S ((S (fom_index_wtp_cap_exact_state_x_bounded)) * x1) + (fom_value_wtp_cap_exact_state_x_bounded))) /\ (exists fom_gap_wtp_cap_exact_state_x_bounded_value_bound. fom_gap_wtp_cap_exact_state_x_bounded_value_bound + S (fom_value_wtp_cap_exact_state_x_bounded) = S (S (m + m))))) /\ ((forall wpo_position_wtp_cap_exact_state_x_nonendpoint wpo_value_wtp_cap_exact_state_x_nonendpoint. (exists wpo_gap_wtp_cap_exact_state_x_nonendpoint_position_bound. wpo_gap_wtp_cap_exact_state_x_nonendpoint_position_bound + S (wpo_position_wtp_cap_exact_state_x_nonendpoint) = m + m) -> (((exists wpo_beta_height_wtp_cap_exact_state_x_nonendpoint_entry. wpo_beta_height_wtp_cap_exact_state_x_nonendpoint_entry + S (wpo_value_wtp_cap_exact_state_x_nonendpoint) = S ((S (wpo_position_wtp_cap_exact_state_x_nonendpoint)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_exact_state_x_nonendpoint_entry. x = wpo_beta_quotient_wtp_cap_exact_state_x_nonendpoint_entry * S ((S (wpo_position_wtp_cap_exact_state_x_nonendpoint)) * x1) + (wpo_value_wtp_cap_exact_state_x_nonendpoint))) -> (~(wpo_value_wtp_cap_exact_state_x_nonendpoint = 0) /\ ~((S wpo_value_wtp_cap_exact_state_x_nonendpoint) = S (S (m + m))))) /\ (forall wpo_injective_left_wtp_cap_exact_state_x_injective wpo_injective_right_wtp_cap_exact_state_x_injective wpo_injective_value_wtp_cap_exact_state_x_injective. (exists wpo_gap_wtp_cap_exact_state_x_injective_left_bound. wpo_gap_wtp_cap_exact_state_x_injective_left_bound + S (wpo_injective_left_wtp_cap_exact_state_x_injective) = m + m) -> (exists wpo_gap_wtp_cap_exact_state_x_injective_right_bound. wpo_gap_wtp_cap_exact_state_x_injective_right_bound + S (wpo_injective_right_wtp_cap_exact_state_x_injective) = m + m) -> (((exists wpo_beta_height_wtp_cap_exact_state_x_injective_left_entry. wpo_beta_height_wtp_cap_exact_state_x_injective_left_entry + S (wpo_injective_value_wtp_cap_exact_state_x_injective) = S ((S (wpo_injective_left_wtp_cap_exact_state_x_injective)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_exact_state_x_injective_left_entry. x = wpo_beta_quotient_wtp_cap_exact_state_x_injective_left_entry * S ((S (wpo_injective_left_wtp_cap_exact_state_x_injective)) * x1) + (wpo_injective_value_wtp_cap_exact_state_x_injective))) -> (((exists wpo_beta_height_wtp_cap_exact_state_x_injective_right_entry. wpo_beta_height_wtp_cap_exact_state_x_injective_right_entry + S (wpo_injective_value_wtp_cap_exact_state_x_injective) = S ((S (wpo_injective_right_wtp_cap_exact_state_x_injective)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_exact_state_x_injective_right_entry. x = wpo_beta_quotient_wtp_cap_exact_state_x_injective_right_entry * S ((S (wpo_injective_right_wtp_cap_exact_state_x_injective)) * x1) + (wpo_injective_value_wtp_cap_exact_state_x_injective))) -> wpo_injective_left_wtp_cap_exact_state_x_injective = wpo_injective_right_wtp_cap_exact_state_x_injective))))
  38. 0038rewrite <- hterminal
  39. 0039rewrite <- hterminal
  40. 0040exact hstate
  41. 0041have hcoverage : ∀ s. Lt(s,S S (m + m)) → ¬s = 0 ∧ ¬S s = S S (m + m) → ContainsPrefix(x,x1,m + m,s)
    Exact native replay linehave hcoverage : forall s. (exists wpo_gap_wtp_cap_coverage_value_bound. wpo_gap_wtp_cap_coverage_value_bound + S (s) = S (S (m + m))) -> (~(s = 0) /\ ~((S s) = S (S (m + m)))) -> exists q. ((exists wpo_gap_wtp_cap_coverage_index_bound. wpo_gap_wtp_cap_coverage_index_bound + S (q) = m + m) /\ (((exists wpo_beta_height_wtp_cap_coverage_entry_x. wpo_beta_height_wtp_cap_coverage_entry_x + S (s) = S ((S (q)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_coverage_entry_x. x = wpo_beta_quotient_wtp_cap_coverage_entry_x * S ((S (q)) * x1) + (s))))
  42. 0042specialize pair_order_state_terminal_coverage u
  43. 0043specialize pair_order_state_terminal_coverage v
  44. 0044specialize pair_order_state_terminal_coverage x
  45. 0045specialize pair_order_state_terminal_coverage x1
  46. 0046specialize pair_order_state_terminal_coverage (m + m)
  47. 0047apply pair_order_state_terminal_coverage
  48. 0048exact hexact_state
  49. 0049have hrange : ∀ gmp_index_wtp_cap_range. Lt(gmp_index_wtp_cap_range,m + m) → ∃ y. BetaAt(x,x1,gmp_index_wtp_cap_range,y) ∧ (Lt(0,y) ∧ Le(y,m + m))
    Exact native replay linehave hrange : forall gmp_index_wtp_cap_range. (exists gsp_lt_gap_wtp_cap_range_index_bound. gsp_lt_gap_wtp_cap_range_index_bound + S gmp_index_wtp_cap_range = m + m) -> exists gmp_magnitude_wtp_cap_range. ((((exists ff_h_gmp_wtp_cap_range_decoded. ff_h_gmp_wtp_cap_range_decoded + S (gmp_magnitude_wtp_cap_range) = S ((S (gmp_index_wtp_cap_range)) * x1)) /\ exists ff_q_gmp_wtp_cap_range_decoded. x = ff_q_gmp_wtp_cap_range_decoded * S ((S (gmp_index_wtp_cap_range)) * x1) + (gmp_magnitude_wtp_cap_range))) /\ ((exists gsp_lt_gap_wtp_cap_range_positive. gsp_lt_gap_wtp_cap_range_positive + S 0 = gmp_magnitude_wtp_cap_range) /\ (exists gsp_le_gap_wtp_cap_range_bounded. gsp_le_gap_wtp_cap_range_bounded + gmp_magnitude_wtp_cap_range = m + m)))
  50. 0050specialize pair_order_terminal_state_magnitude_range u
  51. 0051specialize pair_order_terminal_state_magnitude_range v
  52. 0052specialize pair_order_terminal_state_magnitude_range x
  53. 0053specialize pair_order_terminal_state_magnitude_range x1
  54. 0054specialize pair_order_terminal_state_magnitude_range (m + m)
  55. 0055specialize pair_order_terminal_state_magnitude_range n
  56. 0056apply pair_order_terminal_state_magnitude_range
  57. 0057exact hterminal
  58. 0058exact hstate
  59. 0059have hfactor_product : ∃ f. ∃ g. ∃ Q. (∀ y. ∀ z. Lt(y,m + m) → BetaAt(x,x1,y,z) → BetaAt(f,g,y,S z)) ∧ ((∀ y. ∀ z. ∀ n. Lt(y,m) → BetaAt(f,g,y + y,z) → BetaAt(f,g,S (y + y),n) → BalancedInverse(p,z,n)) ∧ (Product(f,g,m + m,Q) ∧ ModEq(p,Q,1)))
    Exact native replay linehave hfactor_product : exists f g Q. ((forall wsl_index_wtp_cap_lift_x wsl_value_wtp_cap_lift_x. (exists wpo_gap_wtp_cap_lift_x_bound. wpo_gap_wtp_cap_lift_x_bound + S (wsl_index_wtp_cap_lift_x) = m + m) -> (((exists wpo_beta_height_wtp_cap_lift_x_source. wpo_beta_height_wtp_cap_lift_x_source + S (wsl_value_wtp_cap_lift_x) = S ((S (wsl_index_wtp_cap_lift_x)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_lift_x_source. x = wpo_beta_quotient_wtp_cap_lift_x_source * S ((S (wsl_index_wtp_cap_lift_x)) * x1) + (wsl_value_wtp_cap_lift_x))) -> (((exists wpo_beta_height_wtp_cap_lift_x_target. wpo_beta_height_wtp_cap_lift_x_target + S (S wsl_value_wtp_cap_lift_x) = S ((S (wsl_index_wtp_cap_lift_x)) * g)) /\ exists wpo_beta_quotient_wtp_cap_lift_x_target. f = wpo_beta_quotient_wtp_cap_lift_x_target * S ((S (wsl_index_wtp_cap_lift_x)) * g) + (S wsl_value_wtp_cap_lift_x)))) /\ (((forall wpp_pair_wtp_cap_adjacent wpp_left_wtp_cap_adjacent wpp_right_wtp_cap_adjacent. (exists wpp_gap_wtp_cap_adjacent_pair_bound. wpp_gap_wtp_cap_adjacent_pair_bound + S (wpp_pair_wtp_cap_adjacent) = m) -> (((exists wpp_beta_height_wtp_cap_adjacent_left_entry. wpp_beta_height_wtp_cap_adjacent_left_entry + S (wpp_left_wtp_cap_adjacent) = S ((S ((wpp_pair_wtp_cap_adjacent + wpp_pair_wtp_cap_adjacent))) * g)) /\ exists wpp_beta_quotient_wtp_cap_adjacent_left_entry. f = wpp_beta_quotient_wtp_cap_adjacent_left_entry * S ((S ((wpp_pair_wtp_cap_adjacent + wpp_pair_wtp_cap_adjacent))) * g) + (wpp_left_wtp_cap_adjacent))) -> (((exists wpp_beta_height_wtp_cap_adjacent_right_entry. wpp_beta_height_wtp_cap_adjacent_right_entry + S (wpp_right_wtp_cap_adjacent) = S ((S (S (wpp_pair_wtp_cap_adjacent + wpp_pair_wtp_cap_adjacent))) * g)) /\ exists wpp_beta_quotient_wtp_cap_adjacent_right_entry. f = wpp_beta_quotient_wtp_cap_adjacent_right_entry * S ((S (S (wpp_pair_wtp_cap_adjacent + wpp_pair_wtp_cap_adjacent))) * g) + (wpp_right_wtp_cap_adjacent))) -> (exists wpp_mod_left_wtp_cap_adjacent_pair_mod wpp_mod_right_wtp_cap_adjacent_pair_mod. (wpp_left_wtp_cap_adjacent * wpp_right_wtp_cap_adjacent) + p * wpp_mod_left_wtp_cap_adjacent_pair_mod = (1) + p * wpp_mod_right_wtp_cap_adjacent_pair_mod)) /\ (((exists ff_u_wtp_cap_lifted_product ff_v_wtp_cap_lifted_product. ((((exists ff_h_wtp_cap_lifted_product_start. ff_h_wtp_cap_lifted_product_start + S (1) = S ((S (0)) * ff_v_wtp_cap_lifted_product)) /\ exists ff_q_wtp_cap_lifted_product_start. ff_u_wtp_cap_lifted_product = ff_q_wtp_cap_lifted_product_start * S ((S (0)) * ff_v_wtp_cap_lifted_product) + (1))) /\ ((((exists ff_h_wtp_cap_lifted_product_terminal. ff_h_wtp_cap_lifted_product_terminal + S (Q) = S ((S (m + m)) * ff_v_wtp_cap_lifted_product)) /\ exists ff_q_wtp_cap_lifted_product_terminal. ff_u_wtp_cap_lifted_product = ff_q_wtp_cap_lifted_product_terminal * S ((S (m + m)) * ff_v_wtp_cap_lifted_product) + (Q))) /\ forall ff_i_wtp_cap_lifted_product. (exists ff_lt_wtp_cap_lifted_product_bound. ff_lt_wtp_cap_lifted_product_bound + S ff_i_wtp_cap_lifted_product = m + m) -> exists ff_p_wtp_cap_lifted_product ff_r_wtp_cap_lifted_product ff_s_wtp_cap_lifted_product. ((((exists ff_h_wtp_cap_lifted_product_factor. ff_h_wtp_cap_lifted_product_factor + S (ff_p_wtp_cap_lifted_product) = S ((S (ff_i_wtp_cap_lifted_product)) * g)) /\ exists ff_q_wtp_cap_lifted_product_factor. f = ff_q_wtp_cap_lifted_product_factor * S ((S (ff_i_wtp_cap_lifted_product)) * g) + (ff_p_wtp_cap_lifted_product))) /\ ((((exists ff_h_wtp_cap_lifted_product_partial. ff_h_wtp_cap_lifted_product_partial + S (ff_r_wtp_cap_lifted_product) = S ((S (ff_i_wtp_cap_lifted_product)) * ff_v_wtp_cap_lifted_product)) /\ exists ff_q_wtp_cap_lifted_product_partial. ff_u_wtp_cap_lifted_product = ff_q_wtp_cap_lifted_product_partial * S ((S (ff_i_wtp_cap_lifted_product)) * ff_v_wtp_cap_lifted_product) + (ff_r_wtp_cap_lifted_product))) /\ ((((exists ff_h_wtp_cap_lifted_product_successor. ff_h_wtp_cap_lifted_product_successor + S (ff_s_wtp_cap_lifted_product) = S ((S (S ff_i_wtp_cap_lifted_product)) * ff_v_wtp_cap_lifted_product)) /\ exists ff_q_wtp_cap_lifted_product_successor. ff_u_wtp_cap_lifted_product = ff_q_wtp_cap_lifted_product_successor * S ((S (S ff_i_wtp_cap_lifted_product)) * ff_v_wtp_cap_lifted_product) + (ff_s_wtp_cap_lifted_product))) /\ ff_s_wtp_cap_lifted_product = ff_r_wtp_cap_lifted_product * ff_p_wtp_cap_lifted_product)))))) /\ (exists wpp_mod_left_wtp_cap_mod_one wpp_mod_right_wtp_cap_mod_one. (Q) + p * wpp_mod_left_wtp_cap_mod_one = (1) + p * wpp_mod_right_wtp_cap_mod_one))))))
  60. 0060specialize paired_pair_order_product_one_exists p
  61. 0061specialize paired_pair_order_product_one_exists n
  62. 0062specialize paired_pair_order_product_one_exists u
  63. 0063specialize paired_pair_order_product_one_exists v
  64. 0064specialize paired_pair_order_product_one_exists x
  65. 0065specialize paired_pair_order_product_one_exists x1
  66. 0066specialize paired_pair_order_product_one_exists m
  67. 0067apply paired_pair_order_product_one_exists
  68. 0068exact hinverse
  69. 0069exact hstate_parts_right_left
  70. 0070exact hhistory
  71. 0071cases hfactor_product
  72. 0072cases hfactor_product_witness
  73. 0073cases hfactor_product_witness_witness
  74. 0074cases hfactor_product_witness_witness_witness
  75. 0075cases hfactor_product_witness_witness_witness_right
  76. 0076cases hfactor_product_witness_witness_witness_right_right
  77. 0077have hcanonical_range_exists : ∃ z. ∃ d. Range(z,d,2,m + m)
    Exact native replay linehave hcanonical_range_exists : exists z d. (forall wtp_range_index_wtp_cap_range_two. (exists wtp_range_gap_wtp_cap_range_two. wtp_range_gap_wtp_cap_range_two + S wtp_range_index_wtp_cap_range_two = m + m) -> (((exists ff_h_wtp_cap_range_two_decoded. ff_h_wtp_cap_range_two_decoded + S (2 + wtp_range_index_wtp_cap_range_two) = S ((S (wtp_range_index_wtp_cap_range_two)) * d)) /\ exists ff_q_wtp_cap_range_two_decoded. z = ff_q_wtp_cap_range_two_decoded * S ((S (wtp_range_index_wtp_cap_range_two)) * d) + (2 + wtp_range_index_wtp_cap_range_two))))
  78. 0078specialize beta_range_exists 2
  79. 0079specialize beta_range_exists (m + m)
  80. 0080exact beta_range_exists
  81. 0081cases hcanonical_range_exists
  82. 0082cases hcanonical_range_exists_witness
  83. 0083have hcanonical_product_exists : ∃ P. Product(x5,x6,m + m,P)
    Exact native replay linehave hcanonical_product_exists : exists P. (exists ff_u_wtp_cap_canonical_product_x5_x6 ff_v_wtp_cap_canonical_product_x5_x6. ((((exists ff_h_wtp_cap_canonical_product_x5_x6_start. ff_h_wtp_cap_canonical_product_x5_x6_start + S (1) = S ((S (0)) * ff_v_wtp_cap_canonical_product_x5_x6)) /\ exists ff_q_wtp_cap_canonical_product_x5_x6_start. ff_u_wtp_cap_canonical_product_x5_x6 = ff_q_wtp_cap_canonical_product_x5_x6_start * S ((S (0)) * ff_v_wtp_cap_canonical_product_x5_x6) + (1))) /\ ((((exists ff_h_wtp_cap_canonical_product_x5_x6_terminal. ff_h_wtp_cap_canonical_product_x5_x6_terminal + S (P) = S ((S (m + m)) * ff_v_wtp_cap_canonical_product_x5_x6)) /\ exists ff_q_wtp_cap_canonical_product_x5_x6_terminal. ff_u_wtp_cap_canonical_product_x5_x6 = ff_q_wtp_cap_canonical_product_x5_x6_terminal * S ((S (m + m)) * ff_v_wtp_cap_canonical_product_x5_x6) + (P))) /\ forall ff_i_wtp_cap_canonical_product_x5_x6. (exists ff_lt_wtp_cap_canonical_product_x5_x6_bound. ff_lt_wtp_cap_canonical_product_x5_x6_bound + S ff_i_wtp_cap_canonical_product_x5_x6 = m + m) -> exists ff_p_wtp_cap_canonical_product_x5_x6 ff_r_wtp_cap_canonical_product_x5_x6 ff_s_wtp_cap_canonical_product_x5_x6. ((((exists ff_h_wtp_cap_canonical_product_x5_x6_factor. ff_h_wtp_cap_canonical_product_x5_x6_factor + S (ff_p_wtp_cap_canonical_product_x5_x6) = S ((S (ff_i_wtp_cap_canonical_product_x5_x6)) * x6)) /\ exists ff_q_wtp_cap_canonical_product_x5_x6_factor. x5 = ff_q_wtp_cap_canonical_product_x5_x6_factor * S ((S (ff_i_wtp_cap_canonical_product_x5_x6)) * x6) + (ff_p_wtp_cap_canonical_product_x5_x6))) /\ ((((exists ff_h_wtp_cap_canonical_product_x5_x6_partial. ff_h_wtp_cap_canonical_product_x5_x6_partial + S (ff_r_wtp_cap_canonical_product_x5_x6) = S ((S (ff_i_wtp_cap_canonical_product_x5_x6)) * ff_v_wtp_cap_canonical_product_x5_x6)) /\ exists ff_q_wtp_cap_canonical_product_x5_x6_partial. ff_u_wtp_cap_canonical_product_x5_x6 = ff_q_wtp_cap_canonical_product_x5_x6_partial * S ((S (ff_i_wtp_cap_canonical_product_x5_x6)) * ff_v_wtp_cap_canonical_product_x5_x6) + (ff_r_wtp_cap_canonical_product_x5_x6))) /\ ((((exists ff_h_wtp_cap_canonical_product_x5_x6_successor. ff_h_wtp_cap_canonical_product_x5_x6_successor + S (ff_s_wtp_cap_canonical_product_x5_x6) = S ((S (S ff_i_wtp_cap_canonical_product_x5_x6)) * ff_v_wtp_cap_canonical_product_x5_x6)) /\ exists ff_q_wtp_cap_canonical_product_x5_x6_successor. ff_u_wtp_cap_canonical_product_x5_x6 = ff_q_wtp_cap_canonical_product_x5_x6_successor * S ((S (S ff_i_wtp_cap_canonical_product_x5_x6)) * ff_v_wtp_cap_canonical_product_x5_x6) + (ff_s_wtp_cap_canonical_product_x5_x6))) /\ ff_s_wtp_cap_canonical_product_x5_x6 = ff_r_wtp_cap_canonical_product_x5_x6 * ff_p_wtp_cap_canonical_product_x5_x6))))))
  84. 0084specialize beta_product_exists x5
  85. 0085specialize beta_product_exists x6
  86. 0086specialize beta_product_exists (m + m)
  87. 0087exact beta_product_exists
  88. 0088cases hcanonical_product_exists
  89. 0089have hrecode_exists : ∃ rb. ∃ rc. ∀ gmp_index_wtp_cap_recode. ∀ gmp_predecessor_wtp_cap_recode. Lt(gmp_index_wtp_cap_recode,m + m) → BetaAt(x,x1,gmp_index_wtp_cap_recode,S gmp_predecessor_wtp_cap_recode) → BetaAt(rb,rc,gmp_index_wtp_cap_recode,gmp_predecessor_wtp_cap_recode)
    Exact native replay linehave hrecode_exists : exists rb rc. forall gmp_index_wtp_cap_recode gmp_predecessor_wtp_cap_recode. (exists gsp_lt_gap_wtp_cap_recode_index_bound. gsp_lt_gap_wtp_cap_recode_index_bound + S gmp_index_wtp_cap_recode = m + m) -> (((exists gsp_beta_height_gmp_wtp_cap_recode_source. gsp_beta_height_gmp_wtp_cap_recode_source + S (S gmp_predecessor_wtp_cap_recode) = S ((S (gmp_index_wtp_cap_recode)) * x1)) /\ exists gsp_beta_quotient_gmp_wtp_cap_recode_source. x = gsp_beta_quotient_gmp_wtp_cap_recode_source * S ((S (gmp_index_wtp_cap_recode)) * x1) + (S gmp_predecessor_wtp_cap_recode))) -> (((exists ff_h_gmp_wtp_cap_recode_target. ff_h_gmp_wtp_cap_recode_target + S (gmp_predecessor_wtp_cap_recode) = S ((S (gmp_index_wtp_cap_recode)) * rc)) /\ exists ff_q_gmp_wtp_cap_recode_target. rb = ff_q_gmp_wtp_cap_recode_target * S ((S (gmp_index_wtp_cap_recode)) * rc) + (gmp_predecessor_wtp_cap_recode)))
  90. 0090specialize beta_magnitude_predecessor_recode_exists x
  91. 0091specialize beta_magnitude_predecessor_recode_exists x1
  92. 0092specialize beta_magnitude_predecessor_recode_exists (m + m)
  93. 0093specialize beta_magnitude_predecessor_recode_exists (m + m)
  94. 0094apply beta_magnitude_predecessor_recode_exists
  95. 0095exact hrange
  96. 0096cases hrecode_exists
  97. 0097cases hrecode_exists_witness
  98. 0098have hequal : x7 = x4
  99. 0099specialize pair_order_terminal_successor_product_eq_range_two x
  100. 0100specialize pair_order_terminal_successor_product_eq_range_two x1
  101. 0101specialize pair_order_terminal_successor_product_eq_range_two x8
  102. 0102specialize pair_order_terminal_successor_product_eq_range_two x9
  103. 0103specialize pair_order_terminal_successor_product_eq_range_two x5
  104. 0104specialize pair_order_terminal_successor_product_eq_range_two x6
  105. 0105specialize pair_order_terminal_successor_product_eq_range_two x2
  106. 0106specialize pair_order_terminal_successor_product_eq_range_two x3
  107. 0107specialize pair_order_terminal_successor_product_eq_range_two (m + m)
  108. 0108specialize pair_order_terminal_successor_product_eq_range_two x7
  109. 0109specialize pair_order_terminal_successor_product_eq_range_two x4
  110. 0110apply pair_order_terminal_successor_product_eq_range_two
  111. 0111exact hrange
  112. 0112exact hstate_parts_right_right_right
  113. 0113exact hrecode_exists_witness_witness
  114. 0114exact hfactor_product_witness_witness_witness_left
  115. 0115exact hcanonical_range_exists_witness_witness
  116. 0116exact hcanonical_product_exists_witness
  117. 0117exact hfactor_product_witness_witness_witness_right_right_left
  118. 0118exists x
  119. 0119exists x1
  120. 0120exists x2
  121. 0121exists x3
  122. 0122exists x4
  123. 0123exists x5
  124. 0124exists x6
  125. 0125exists x7
  126. 0126split
  127. 0127exact hstate
  128. 0128split
  129. 0129exact hhistory
  130. 0130split
  131. 0131exact hcoverage
  132. 0132split
  133. 0133exact hfactor_product_witness_witness_witness_left
  134. 0134split
  135. 0135exact hfactor_product_witness_witness_witness_right_left
  136. 0136split
  137. 0137exact hfactor_product_witness_witness_witness_right_right_left
  138. 0138split
  139. 0139exact hfactor_product_witness_witness_witness_right_right_right
  140. 0140split
  141. 0141exact hcanonical_range_exists_witness_witness
  142. 0142split
  143. 0143exact hcanonical_product_exists_witness
  144. 0144exact hequal