PA009V · theorem

scaled_inverse_pair_order_paired_iteration

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

Iterate exactly one adjacent scaled orbit for every stored pair.

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. ∀ a. ∀ n. ∀ u. ∀ v. p = S n → Prime(p) → ¬QRes(p,a) → ScaledInversePrefix(p,a,n,u,v,n) → ∀ x. ∀ y. x + x + (y + y) = n → ∃ z. ∃ m. (∀ k. ∀ i. ∀ j. Lt(k,x + x) → BetaAt(z,m,k,i) → BetaAt(u,v,i,S j) → ContainsPrefix(z,m,x + x,j)) ∧ ((∀ k. Lt(k,x + x) → ∃ i. BetaAt(z,m,k,i) ∧ Lt(i,n)) ∧ InjectivePrefix(z,m,x + x)) ∧ (∀ k. Lt(k,x) → ∃ i. ∃ j. BetaAt(z,m,k + k,i) ∧ (BetaAt(z,m,S (k + k),j) ∧ BetaAt(u,v,i,S j)))

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 PD0013 BetaAt PD0021 QRes PD0025 InjectivePrefix PD0027 ContainsPrefix PD0039 ScaledInversePrefix

15 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0025 InjectivePrefix PD0027 ContainsPrefix

41 occurrences

Exact expanded native-PA statement
forall p a n u v. p = S n -> ((~(p = 1) /\ forall esi_prime_left_iteration_prime esi_prime_right_iteration_prime. p = esi_prime_left_iteration_prime * esi_prime_right_iteration_prime -> esi_prime_left_iteration_prime = 1 \/ esi_prime_right_iteration_prime = 1)) -> ~(exists qr_x_iteration_nonresidue. exists qr_u_iteration_nonresidue qr_v_iteration_nonresidue. qr_x_iteration_nonresidue * qr_x_iteration_nonresidue + p * qr_u_iteration_nonresidue = a + p * qr_v_iteration_nonresidue) -> (forall esip_index_iteration_prefix. (exists esip_gap_iteration_prefix_prefix_bound. esip_gap_iteration_prefix_prefix_bound + S (esip_index_iteration_prefix) = n) -> exists esip_mate_iteration_prefix. ((((exists ff_h_esip_iteration_prefix_entry. ff_h_esip_iteration_prefix_entry + S (esip_mate_iteration_prefix) = S ((S (esip_index_iteration_prefix)) * v)) /\ exists ff_q_esip_iteration_prefix_entry. u = ff_q_esip_iteration_prefix_entry * S ((S (esip_index_iteration_prefix)) * v) + (esip_mate_iteration_prefix))) /\ ((exists esip_gap_iteration_prefix_relation_index_bound. esip_gap_iteration_prefix_relation_index_bound + S (esip_index_iteration_prefix) = n) /\ ((((~((S esip_index_iteration_prefix) = 0) /\ (exists esip_gap_iteration_prefix_relation_scaled_left_bound. esip_gap_iteration_prefix_relation_scaled_left_bound + S (S esip_index_iteration_prefix) = p))) /\ (((~(esip_mate_iteration_prefix = 0) /\ (exists esip_gap_iteration_prefix_relation_scaled_right_bound. esip_gap_iteration_prefix_relation_scaled_right_bound + S (esip_mate_iteration_prefix) = p))) /\ (exists esi_mod_left_iteration_prefix_relation_scaled_mod esi_mod_right_iteration_prefix_relation_scaled_mod. ((S esip_index_iteration_prefix) * esip_mate_iteration_prefix) + p * esi_mod_left_iteration_prefix_relation_scaled_mod = (a) + p * esi_mod_right_iteration_prefix_relation_scaled_mod))))))) -> forall m k. (m + m) + (k + k) = n -> (exists b c. (((((forall espo_position_iteration_state_closed espo_source_iteration_state_closed espo_mate_iteration_state_closed. (exists wpo_gap_iteration_state_closed_position_bound. wpo_gap_iteration_state_closed_position_bound + S (espo_position_iteration_state_closed) = m + m) -> (((exists wpo_beta_height_iteration_state_closed_source_entry. wpo_beta_height_iteration_state_closed_source_entry + S (espo_source_iteration_state_closed) = S ((S (espo_position_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_iteration_state_closed_source_entry. b = wpo_beta_quotient_iteration_state_closed_source_entry * S ((S (espo_position_iteration_state_closed)) * c) + (espo_source_iteration_state_closed))) -> (((exists wpo_beta_height_iteration_state_closed_scaled_entry. wpo_beta_height_iteration_state_closed_scaled_entry + S (S espo_mate_iteration_state_closed) = S ((S (espo_source_iteration_state_closed)) * v)) /\ exists wpo_beta_quotient_iteration_state_closed_scaled_entry. u = wpo_beta_quotient_iteration_state_closed_scaled_entry * S ((S (espo_source_iteration_state_closed)) * v) + (S espo_mate_iteration_state_closed))) -> exists espo_mate_position_iteration_state_closed. ((exists wpo_gap_iteration_state_closed_mate_bound. wpo_gap_iteration_state_closed_mate_bound + S (espo_mate_position_iteration_state_closed) = m + m) /\ (((exists wpo_beta_height_iteration_state_closed_mate_entry. wpo_beta_height_iteration_state_closed_mate_entry + S (espo_mate_iteration_state_closed) = S ((S (espo_mate_position_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_iteration_state_closed_mate_entry. b = wpo_beta_quotient_iteration_state_closed_mate_entry * S ((S (espo_mate_position_iteration_state_closed)) * c) + (espo_mate_iteration_state_closed))))) /\ (((forall fom_index_iteration_state_bounded. (exists fom_gap_iteration_state_bounded_index_bound. fom_gap_iteration_state_bounded_index_bound + S (fom_index_iteration_state_bounded) = m + m) -> exists fom_value_iteration_state_bounded. ((((exists fom_beta_height_iteration_state_bounded_entry. fom_beta_height_iteration_state_bounded_entry + S (fom_value_iteration_state_bounded) = S ((S (fom_index_iteration_state_bounded)) * c)) /\ exists fom_beta_quotient_iteration_state_bounded_entry. b = fom_beta_quotient_iteration_state_bounded_entry * S ((S (fom_index_iteration_state_bounded)) * c) + (fom_value_iteration_state_bounded))) /\ (exists fom_gap_iteration_state_bounded_value_bound. fom_gap_iteration_state_bounded_value_bound + S (fom_value_iteration_state_bounded) = n))) /\ (forall wpo_injective_left_iteration_state_injective wpo_injective_right_iteration_state_injective wpo_injective_value_iteration_state_injective. (exists wpo_gap_iteration_state_injective_left_bound. wpo_gap_iteration_state_injective_left_bound + S (wpo_injective_left_iteration_state_injective) = m + m) -> (exists wpo_gap_iteration_state_injective_right_bound. wpo_gap_iteration_state_injective_right_bound + S (wpo_injective_right_iteration_state_injective) = m + m) -> (((exists wpo_beta_height_iteration_state_injective_left_entry. wpo_beta_height_iteration_state_injective_left_entry + S (wpo_injective_value_iteration_state_injective) = S ((S (wpo_injective_left_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_iteration_state_injective_left_entry. b = wpo_beta_quotient_iteration_state_injective_left_entry * S ((S (wpo_injective_left_iteration_state_injective)) * c) + (wpo_injective_value_iteration_state_injective))) -> (((exists wpo_beta_height_iteration_state_injective_right_entry. wpo_beta_height_iteration_state_injective_right_entry + S (wpo_injective_value_iteration_state_injective) = S ((S (wpo_injective_right_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_iteration_state_injective_right_entry. b = wpo_beta_quotient_iteration_state_injective_right_entry * S ((S (wpo_injective_right_iteration_state_injective)) * c) + (wpo_injective_value_iteration_state_injective))) -> wpo_injective_left_iteration_state_injective = wpo_injective_right_iteration_state_injective))))) /\ (forall espi_pair_iteration_history. (exists wpo_gap_iteration_history_pair_bound. wpo_gap_iteration_history_pair_bound + S (espi_pair_iteration_history) = m) -> exists espi_left_iteration_history espi_right_iteration_history. (((((exists wpo_beta_height_iteration_history_left_entry. wpo_beta_height_iteration_history_left_entry + S (espi_left_iteration_history) = S ((S (espi_pair_iteration_history + espi_pair_iteration_history)) * c)) /\ exists wpo_beta_quotient_iteration_history_left_entry. b = wpo_beta_quotient_iteration_history_left_entry * S ((S (espi_pair_iteration_history + espi_pair_iteration_history)) * c) + (espi_left_iteration_history))) /\ (((((exists wpo_beta_height_iteration_history_right_entry. wpo_beta_height_iteration_history_right_entry + S (espi_right_iteration_history) = S ((S (S (espi_pair_iteration_history + espi_pair_iteration_history))) * c)) /\ exists wpo_beta_quotient_iteration_history_right_entry. b = wpo_beta_quotient_iteration_history_right_entry * S ((S (S (espi_pair_iteration_history + espi_pair_iteration_history))) * c) + (espi_right_iteration_history))) /\ (((exists wpo_beta_height_iteration_history_scaled_edge. wpo_beta_height_iteration_history_scaled_edge + S (S espi_right_iteration_history) = S ((S (espi_left_iteration_history)) * v)) /\ exists wpo_beta_quotient_iteration_history_scaled_edge. u = wpo_beta_quotient_iteration_history_scaled_edge * S ((S (espi_left_iteration_history)) * v) + (S espi_right_iteration_history)))))))))))

Proof neighborhood

Direct theorem prerequisites

PA008X scaled_pair_order_state_zero PA008Y adjacent_scaled_orbit_history_zero PA0090 euler_pair_iteration_previous_balance PA0091 euler_pair_iteration_step_short PA009T scaled_inverse_pair_order_paired_state_step PA009U pair_order_double_succ_length

Direct theorem dependents

PA009W scaled_inverse_pair_order_terminal_package

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

101 script commands · 27 reading checkpoints · 11 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (6)
scaled pair order state zeroadjacent scaled orbit history zeroeuler pair iteration previous balanceeuler pair iteration step shortscaled inverse pair order paired state steppair order double succ length
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro n
  4. L4
    intro u
  5. L5
    intro v
  6. L6
    intro hpn
  7. L7
    intro hp
  8. L8
    intro hnotqres
  9. L9
    intro hprefix
02Induction on mL10–12

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

  1. L10
    induction m
  2. L11
    intro k
  3. L12
    intro hbalance
03Establish hzero_stateL13–17

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

  1. L13
    have hzero_state : ∃ b. ∃ c. (∀ x. ∀ y. ∀ z. Lt(x,0) → BetaAt(b,c,x,y) → BetaAt(u,v,y,S z) → ContainsPrefix(b,c,0,z)) ∧ ((∀ x. Lt(x,0) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) ∧ InjectivePrefix(b,c,0))Definitions: Lt(x,0)BetaAt(b,c,x,y)BetaAt(u,v,y,S z)ContainsPrefix(b,c,0,z)Lt(y,n)InjectivePrefix(b,c,0)Original native command in the exact edition
  2. L14
    specialize scaled_pair_order_state_zero u
  3. L15
    specialize scaled_pair_order_state_zero v
  4. L16
    specialize scaled_pair_order_state_zero n
  5. L17
    exact scaled_pair_order_state_zero
04Separate the logical casesL18–19

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

  1. L18
    cases hzero_state
  2. L19
    cases hzero_state_witness
05Establish hzeroL20–21

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

  1. L20
    have hzero : 0 + 0 = 0
  2. L21
    simp
06Construct an explicit witnessL22–23

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

  1. L22
    exists x
  2. L23
    exists x1
07Separate the logical casesL24–24

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

  1. L24
    split
08Calculate and transport equalitiesL25–29

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L25
    rewrite hzero
  2. L26
    rewrite hzero
  3. L27
    rewrite hzero
  4. L28
    rewrite hzero
  5. L29
    rewrite hzero
09Use earlier factsL30–35

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

  1. L30
    exact hzero_state_witness_witness
  2. L31
    specialize adjacent_scaled_orbit_history_zero u
  3. L32
    specialize adjacent_scaled_orbit_history_zero v
  4. L33
    specialize adjacent_scaled_orbit_history_zero x
  5. L34
    specialize adjacent_scaled_orbit_history_zero x1
  6. L35
    exact adjacent_scaled_orbit_history_zero
10Fix variables and assumptionsL36–37

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

  1. L36
    intro k
  2. L37
    intro hbalance
11Establish hprevious_normalizeL38–41

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

  1. L38
    have hprevious_normalize : (S m + S m) + (k + k) = (m + m) + (S k + S k)
  2. L39
    specialize euler_pair_iteration_previous_balance m
  3. L40
    specialize euler_pair_iteration_previous_balance k
  4. L41
    exact euler_pair_iteration_previous_balance
12Establish hprevious_balanceL42–46

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

  1. L42
    have hprevious_balance : (m + m) + (S k + S k) = n
  2. L43
    trans (S m + S m) + (k + k)
  3. L44
    symm
  4. L45
    exact hprevious_normalize
  5. L46
    exact hbalance
13Establish hpreviousL47–50

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

  1. L47
    have hprevious : ∃ b. ∃ c. (∀ x. ∀ y. ∀ z. Lt(x,m + m) → BetaAt(b,c,x,y) → BetaAt(u,v,y,S z) → ContainsPrefix(b,c,m + m,z)) ∧ ((∀ x. Lt(x,m + m) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(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,S z)))Definitions: Lt(x,m + m)BetaAt(b,c,x,y)BetaAt(u,v,y,S 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. L48
    specialize IH (S k)
  3. L49
    apply IH
  4. L50
    exact hprevious_balance
14Separate the logical casesL51–53

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

  1. L51
    cases hprevious
  2. L52
    cases hprevious_witness
  3. L53
    cases hprevious_witness_witness
15Establish hshort_normalizeL54–57

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

  1. L54
    have hshort_normalize : S (k + k) + S (m + m) = (S m + S m) + (k + k)
  2. L55
    specialize euler_pair_iteration_step_short m
  3. L56
    specialize euler_pair_iteration_step_short k
  4. L57
    exact euler_pair_iteration_step_short
16Establish hshort_eqL58–61

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

  1. L58
    have hshort_eq : S (k + k) + S (m + m) = n
  2. L59
    trans (S m + S m) + (k + k)
  3. L60
    exact hshort_normalize
  4. L61
    exact hbalance
17Establish hshortL62–62

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

  1. L62
    have hshort : Lt(m + m,n)Definitions: Lt(m + m,n)Original native command in the exact edition
18Construct an explicit witnessL63–63

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

  1. L63
    exists S (k + k)
19Use earlier factsL64–64

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

  1. L64
    exact hshort_eq
20Establish hnextL65–74

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply scaled inverse pair order paired state step.

  1. L65
    have hnext : ∃ z. ∃ d. (∀ x. ∀ y. ∀ k. Lt(x,S S (m + m)) → BetaAt(z,d,x,y) → BetaAt(u,v,y,S k) → ContainsPrefix(z,d,S S (m + m),k)) ∧ ((∀ x. Lt(x,S S (m + m)) → ∃ y. BetaAt(z,d,x,y) ∧ Lt(y,n)) ∧ InjectivePrefix(z,d,S S (m + m))) ∧ (∀ x. Lt(x,S m) → ∃ y. ∃ k. BetaAt(z,d,x + x,y) ∧ (BetaAt(z,d,S (x + x),k) ∧ BetaAt(u,v,y,S k)))Definitions: Lt(x,S S (m + m))BetaAt(z,d,x,y)BetaAt(u,v,y,S k)ContainsPrefix(z,d,S S (m + m),k)Lt(y,n)InjectivePrefix(z,d,S S (m + m))Lt(x,S m)BetaAt(z,d,x + x,y)BetaAt(z,d,S (x + x),k)Original native command in the exact edition
  2. L66
    specialize scaled_inverse_pair_order_paired_state_step p
  3. L67
    specialize scaled_inverse_pair_order_paired_state_step a
  4. L68
    specialize scaled_inverse_pair_order_paired_state_step n
  5. L69
    specialize scaled_inverse_pair_order_paired_state_step u
  6. L70
    specialize scaled_inverse_pair_order_paired_state_step v
  7. L71
    specialize scaled_inverse_pair_order_paired_state_step x
  8. L72
    specialize scaled_inverse_pair_order_paired_state_step x1
  9. L73
    specialize scaled_inverse_pair_order_paired_state_step m
  10. L74
    apply scaled_inverse_pair_order_paired_state_step
21Use earlier factsL75–81

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

  1. L75
    exact hpn
  2. L76
    exact hp
  3. L77
    exact hnotqres
  4. L78
    exact hprefix
  5. L79
    exact hshort
  6. L80
    exact hprevious_witness_witness_left
  7. L81
    exact hprevious_witness_witness_right
22Separate the logical casesL82–84

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

  1. L82
    cases hnext
  2. L83
    cases hnext_witness
  3. L84
    cases hnext_witness_witness
23Establish hlengthL85–89

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair order double succ length.

  1. L85
    have hlength : S (S (m + m)) = S m + S m
  2. L86
    specialize pair_order_double_succ_length (m + m)
  3. L87
    specialize pair_order_double_succ_length m
  4. L88
    apply pair_order_double_succ_length
  5. L89
    refl
24Establish hsuccessor_stateL90–96

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

  1. L90
    have hsuccessor_state : (∀ x. ∀ y. ∀ z. Lt(x,S m + S m) → BetaAt(x2,x3,x,y) → BetaAt(u,v,y,S z) → ContainsPrefix(x2,x3,S m + S m,z)) ∧ ((∀ x. Lt(x,S m + S m) → ∃ y. BetaAt(x2,x3,x,y) ∧ Lt(y,n)) ∧ InjectivePrefix(x2,x3,S m + S m))Definitions: Lt(x,S m + S m)BetaAt(x2,x3,x,y)BetaAt(u,v,y,S z)ContainsPrefix(x2,x3,S m + S m,z)Lt(y,n)InjectivePrefix(x2,x3,S m + S m)Original native command in the exact edition
  2. L91
    rewrite <- hlength
  3. L92
    rewrite <- hlength
  4. L93
    rewrite <- hlength
  5. L94
    rewrite <- hlength
  6. L95
    rewrite <- hlength
  7. L96
    exact hnext_witness_witness_left
25Construct an explicit witnessL97–98

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

  1. L97
    exists x2
  2. L98
    exists x3
26Separate the logical casesL99–99

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

  1. L99
    split
27Use earlier factsL100–101

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

  1. L100
    exact hsuccessor_state
  2. L101
    exact hnext_witness_witness_right

Library-wide reading audit

Original defined command ledger · 101 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro u
  5. 0005intro v
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro hnotqres
  9. 0009intro hprefix
  10. 0010induction m
  11. 0011intro k
  12. 0012intro hbalance
  13. 0013have hzero_state : ∃ b. ∃ c. (∀ x. ∀ y. ∀ z. Lt(x,0) → BetaAt(b,c,x,y) → BetaAt(u,v,y,S z) → ContainsPrefix(b,c,0,z)) ∧ ((∀ x. Lt(x,0) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) ∧ InjectivePrefix(b,c,0))
    Exact native replay linehave hzero_state : exists b c. (((forall espo_position_zero_state_closed espo_source_zero_state_closed espo_mate_zero_state_closed. (exists wpo_gap_zero_state_closed_position_bound. wpo_gap_zero_state_closed_position_bound + S (espo_position_zero_state_closed) = 0) -> (((exists wpo_beta_height_zero_state_closed_source_entry. wpo_beta_height_zero_state_closed_source_entry + S (espo_source_zero_state_closed) = S ((S (espo_position_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_zero_state_closed_source_entry. b = wpo_beta_quotient_zero_state_closed_source_entry * S ((S (espo_position_zero_state_closed)) * c) + (espo_source_zero_state_closed))) -> (((exists wpo_beta_height_zero_state_closed_scaled_entry. wpo_beta_height_zero_state_closed_scaled_entry + S (S espo_mate_zero_state_closed) = S ((S (espo_source_zero_state_closed)) * v)) /\ exists wpo_beta_quotient_zero_state_closed_scaled_entry. u = wpo_beta_quotient_zero_state_closed_scaled_entry * S ((S (espo_source_zero_state_closed)) * v) + (S espo_mate_zero_state_closed))) -> exists espo_mate_position_zero_state_closed. ((exists wpo_gap_zero_state_closed_mate_bound. wpo_gap_zero_state_closed_mate_bound + S (espo_mate_position_zero_state_closed) = 0) /\ (((exists wpo_beta_height_zero_state_closed_mate_entry. wpo_beta_height_zero_state_closed_mate_entry + S (espo_mate_zero_state_closed) = S ((S (espo_mate_position_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_zero_state_closed_mate_entry. b = wpo_beta_quotient_zero_state_closed_mate_entry * S ((S (espo_mate_position_zero_state_closed)) * c) + (espo_mate_zero_state_closed))))) /\ (((forall fom_index_zero_state_bounded. (exists fom_gap_zero_state_bounded_index_bound. fom_gap_zero_state_bounded_index_bound + S (fom_index_zero_state_bounded) = 0) -> exists fom_value_zero_state_bounded. ((((exists fom_beta_height_zero_state_bounded_entry. fom_beta_height_zero_state_bounded_entry + S (fom_value_zero_state_bounded) = S ((S (fom_index_zero_state_bounded)) * c)) /\ exists fom_beta_quotient_zero_state_bounded_entry. b = fom_beta_quotient_zero_state_bounded_entry * S ((S (fom_index_zero_state_bounded)) * c) + (fom_value_zero_state_bounded))) /\ (exists fom_gap_zero_state_bounded_value_bound. fom_gap_zero_state_bounded_value_bound + S (fom_value_zero_state_bounded) = n))) /\ (forall wpo_injective_left_zero_state_injective wpo_injective_right_zero_state_injective wpo_injective_value_zero_state_injective. (exists wpo_gap_zero_state_injective_left_bound. wpo_gap_zero_state_injective_left_bound + S (wpo_injective_left_zero_state_injective) = 0) -> (exists wpo_gap_zero_state_injective_right_bound. wpo_gap_zero_state_injective_right_bound + S (wpo_injective_right_zero_state_injective) = 0) -> (((exists wpo_beta_height_zero_state_injective_left_entry. wpo_beta_height_zero_state_injective_left_entry + S (wpo_injective_value_zero_state_injective) = S ((S (wpo_injective_left_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_zero_state_injective_left_entry. b = wpo_beta_quotient_zero_state_injective_left_entry * S ((S (wpo_injective_left_zero_state_injective)) * c) + (wpo_injective_value_zero_state_injective))) -> (((exists wpo_beta_height_zero_state_injective_right_entry. wpo_beta_height_zero_state_injective_right_entry + S (wpo_injective_value_zero_state_injective) = S ((S (wpo_injective_right_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_zero_state_injective_right_entry. b = wpo_beta_quotient_zero_state_injective_right_entry * S ((S (wpo_injective_right_zero_state_injective)) * c) + (wpo_injective_value_zero_state_injective))) -> wpo_injective_left_zero_state_injective = wpo_injective_right_zero_state_injective)))))
  14. 0014specialize scaled_pair_order_state_zero u
  15. 0015specialize scaled_pair_order_state_zero v
  16. 0016specialize scaled_pair_order_state_zero n
  17. 0017exact scaled_pair_order_state_zero
  18. 0018cases hzero_state
  19. 0019cases hzero_state_witness
  20. 0020have hzero : 0 + 0 = 0
  21. 0021simp
  22. 0022exists x
  23. 0023exists x1
  24. 0024split
  25. 0025rewrite hzero
  26. 0026rewrite hzero
  27. 0027rewrite hzero
  28. 0028rewrite hzero
  29. 0029rewrite hzero
  30. 0030exact hzero_state_witness_witness
  31. 0031specialize adjacent_scaled_orbit_history_zero u
  32. 0032specialize adjacent_scaled_orbit_history_zero v
  33. 0033specialize adjacent_scaled_orbit_history_zero x
  34. 0034specialize adjacent_scaled_orbit_history_zero x1
  35. 0035exact adjacent_scaled_orbit_history_zero
  36. 0036intro k
  37. 0037intro hbalance
  38. 0038have hprevious_normalize : (S m + S m) + (k + k) = (m + m) + (S k + S k)
  39. 0039specialize euler_pair_iteration_previous_balance m
  40. 0040specialize euler_pair_iteration_previous_balance k
  41. 0041exact euler_pair_iteration_previous_balance
  42. 0042have hprevious_balance : (m + m) + (S k + S k) = n
  43. 0043trans (S m + S m) + (k + k)
  44. 0044symm
  45. 0045exact hprevious_normalize
  46. 0046exact hbalance
  47. 0047have hprevious : ∃ b. ∃ c. (∀ x. ∀ y. ∀ z. Lt(x,m + m) → BetaAt(b,c,x,y) → BetaAt(u,v,y,S z) → ContainsPrefix(b,c,m + m,z)) ∧ ((∀ x. Lt(x,m + m) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(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,S z)))
    Exact native replay linehave hprevious : exists b c. (((((forall espo_position_iteration_state_closed espo_source_iteration_state_closed espo_mate_iteration_state_closed. (exists wpo_gap_iteration_state_closed_position_bound. wpo_gap_iteration_state_closed_position_bound + S (espo_position_iteration_state_closed) = m + m) -> (((exists wpo_beta_height_iteration_state_closed_source_entry. wpo_beta_height_iteration_state_closed_source_entry + S (espo_source_iteration_state_closed) = S ((S (espo_position_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_iteration_state_closed_source_entry. b = wpo_beta_quotient_iteration_state_closed_source_entry * S ((S (espo_position_iteration_state_closed)) * c) + (espo_source_iteration_state_closed))) -> (((exists wpo_beta_height_iteration_state_closed_scaled_entry. wpo_beta_height_iteration_state_closed_scaled_entry + S (S espo_mate_iteration_state_closed) = S ((S (espo_source_iteration_state_closed)) * v)) /\ exists wpo_beta_quotient_iteration_state_closed_scaled_entry. u = wpo_beta_quotient_iteration_state_closed_scaled_entry * S ((S (espo_source_iteration_state_closed)) * v) + (S espo_mate_iteration_state_closed))) -> exists espo_mate_position_iteration_state_closed. ((exists wpo_gap_iteration_state_closed_mate_bound. wpo_gap_iteration_state_closed_mate_bound + S (espo_mate_position_iteration_state_closed) = m + m) /\ (((exists wpo_beta_height_iteration_state_closed_mate_entry. wpo_beta_height_iteration_state_closed_mate_entry + S (espo_mate_iteration_state_closed) = S ((S (espo_mate_position_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_iteration_state_closed_mate_entry. b = wpo_beta_quotient_iteration_state_closed_mate_entry * S ((S (espo_mate_position_iteration_state_closed)) * c) + (espo_mate_iteration_state_closed))))) /\ (((forall fom_index_iteration_state_bounded. (exists fom_gap_iteration_state_bounded_index_bound. fom_gap_iteration_state_bounded_index_bound + S (fom_index_iteration_state_bounded) = m + m) -> exists fom_value_iteration_state_bounded. ((((exists fom_beta_height_iteration_state_bounded_entry. fom_beta_height_iteration_state_bounded_entry + S (fom_value_iteration_state_bounded) = S ((S (fom_index_iteration_state_bounded)) * c)) /\ exists fom_beta_quotient_iteration_state_bounded_entry. b = fom_beta_quotient_iteration_state_bounded_entry * S ((S (fom_index_iteration_state_bounded)) * c) + (fom_value_iteration_state_bounded))) /\ (exists fom_gap_iteration_state_bounded_value_bound. fom_gap_iteration_state_bounded_value_bound + S (fom_value_iteration_state_bounded) = n))) /\ (forall wpo_injective_left_iteration_state_injective wpo_injective_right_iteration_state_injective wpo_injective_value_iteration_state_injective. (exists wpo_gap_iteration_state_injective_left_bound. wpo_gap_iteration_state_injective_left_bound + S (wpo_injective_left_iteration_state_injective) = m + m) -> (exists wpo_gap_iteration_state_injective_right_bound. wpo_gap_iteration_state_injective_right_bound + S (wpo_injective_right_iteration_state_injective) = m + m) -> (((exists wpo_beta_height_iteration_state_injective_left_entry. wpo_beta_height_iteration_state_injective_left_entry + S (wpo_injective_value_iteration_state_injective) = S ((S (wpo_injective_left_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_iteration_state_injective_left_entry. b = wpo_beta_quotient_iteration_state_injective_left_entry * S ((S (wpo_injective_left_iteration_state_injective)) * c) + (wpo_injective_value_iteration_state_injective))) -> (((exists wpo_beta_height_iteration_state_injective_right_entry. wpo_beta_height_iteration_state_injective_right_entry + S (wpo_injective_value_iteration_state_injective) = S ((S (wpo_injective_right_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_iteration_state_injective_right_entry. b = wpo_beta_quotient_iteration_state_injective_right_entry * S ((S (wpo_injective_right_iteration_state_injective)) * c) + (wpo_injective_value_iteration_state_injective))) -> wpo_injective_left_iteration_state_injective = wpo_injective_right_iteration_state_injective))))) /\ (forall espi_pair_iteration_history. (exists wpo_gap_iteration_history_pair_bound. wpo_gap_iteration_history_pair_bound + S (espi_pair_iteration_history) = m) -> exists espi_left_iteration_history espi_right_iteration_history. (((((exists wpo_beta_height_iteration_history_left_entry. wpo_beta_height_iteration_history_left_entry + S (espi_left_iteration_history) = S ((S (espi_pair_iteration_history + espi_pair_iteration_history)) * c)) /\ exists wpo_beta_quotient_iteration_history_left_entry. b = wpo_beta_quotient_iteration_history_left_entry * S ((S (espi_pair_iteration_history + espi_pair_iteration_history)) * c) + (espi_left_iteration_history))) /\ (((((exists wpo_beta_height_iteration_history_right_entry. wpo_beta_height_iteration_history_right_entry + S (espi_right_iteration_history) = S ((S (S (espi_pair_iteration_history + espi_pair_iteration_history))) * c)) /\ exists wpo_beta_quotient_iteration_history_right_entry. b = wpo_beta_quotient_iteration_history_right_entry * S ((S (S (espi_pair_iteration_history + espi_pair_iteration_history))) * c) + (espi_right_iteration_history))) /\ (((exists wpo_beta_height_iteration_history_scaled_edge. wpo_beta_height_iteration_history_scaled_edge + S (S espi_right_iteration_history) = S ((S (espi_left_iteration_history)) * v)) /\ exists wpo_beta_quotient_iteration_history_scaled_edge. u = wpo_beta_quotient_iteration_history_scaled_edge * S ((S (espi_left_iteration_history)) * v) + (S espi_right_iteration_history))))))))))
  48. 0048specialize IH (S k)
  49. 0049apply IH
  50. 0050exact hprevious_balance
  51. 0051cases hprevious
  52. 0052cases hprevious_witness
  53. 0053cases hprevious_witness_witness
  54. 0054have hshort_normalize : S (k + k) + S (m + m) = (S m + S m) + (k + k)
  55. 0055specialize euler_pair_iteration_step_short m
  56. 0056specialize euler_pair_iteration_step_short k
  57. 0057exact euler_pair_iteration_step_short
  58. 0058have hshort_eq : S (k + k) + S (m + m) = n
  59. 0059trans (S m + S m) + (k + k)
  60. 0060exact hshort_normalize
  61. 0061exact hbalance
  62. 0062have hshort : Lt(m + m,n)
    Exact native replay linehave hshort : exists q. q + S (m + m) = n
  63. 0063exists S (k + k)
  64. 0064exact hshort_eq
  65. 0065have hnext : ∃ z. ∃ d. (∀ x. ∀ y. ∀ k. Lt(x,S S (m + m)) → BetaAt(z,d,x,y) → BetaAt(u,v,y,S k) → ContainsPrefix(z,d,S S (m + m),k)) ∧ ((∀ x. Lt(x,S S (m + m)) → ∃ y. BetaAt(z,d,x,y) ∧ Lt(y,n)) ∧ InjectivePrefix(z,d,S S (m + m))) ∧ (∀ x. Lt(x,S m) → ∃ y. ∃ k. BetaAt(z,d,x + x,y) ∧ (BetaAt(z,d,S (x + x),k) ∧ BetaAt(u,v,y,S k)))
    Exact native replay linehave hnext : exists z d. (((((forall espo_position_step_result_state_closed espo_source_step_result_state_closed espo_mate_step_result_state_closed. (exists wpo_gap_step_result_state_closed_position_bound. wpo_gap_step_result_state_closed_position_bound + S (espo_position_step_result_state_closed) = S (S (m + m))) -> (((exists wpo_beta_height_step_result_state_closed_source_entry. wpo_beta_height_step_result_state_closed_source_entry + S (espo_source_step_result_state_closed) = S ((S (espo_position_step_result_state_closed)) * d)) /\ exists wpo_beta_quotient_step_result_state_closed_source_entry. z = wpo_beta_quotient_step_result_state_closed_source_entry * S ((S (espo_position_step_result_state_closed)) * d) + (espo_source_step_result_state_closed))) -> (((exists wpo_beta_height_step_result_state_closed_scaled_entry. wpo_beta_height_step_result_state_closed_scaled_entry + S (S espo_mate_step_result_state_closed) = S ((S (espo_source_step_result_state_closed)) * v)) /\ exists wpo_beta_quotient_step_result_state_closed_scaled_entry. u = wpo_beta_quotient_step_result_state_closed_scaled_entry * S ((S (espo_source_step_result_state_closed)) * v) + (S espo_mate_step_result_state_closed))) -> exists espo_mate_position_step_result_state_closed. ((exists wpo_gap_step_result_state_closed_mate_bound. wpo_gap_step_result_state_closed_mate_bound + S (espo_mate_position_step_result_state_closed) = S (S (m + m))) /\ (((exists wpo_beta_height_step_result_state_closed_mate_entry. wpo_beta_height_step_result_state_closed_mate_entry + S (espo_mate_step_result_state_closed) = S ((S (espo_mate_position_step_result_state_closed)) * d)) /\ exists wpo_beta_quotient_step_result_state_closed_mate_entry. z = wpo_beta_quotient_step_result_state_closed_mate_entry * S ((S (espo_mate_position_step_result_state_closed)) * d) + (espo_mate_step_result_state_closed))))) /\ (((forall fom_index_step_result_state_bounded. (exists fom_gap_step_result_state_bounded_index_bound. fom_gap_step_result_state_bounded_index_bound + S (fom_index_step_result_state_bounded) = S (S (m + m))) -> exists fom_value_step_result_state_bounded. ((((exists fom_beta_height_step_result_state_bounded_entry. fom_beta_height_step_result_state_bounded_entry + S (fom_value_step_result_state_bounded) = S ((S (fom_index_step_result_state_bounded)) * d)) /\ exists fom_beta_quotient_step_result_state_bounded_entry. z = fom_beta_quotient_step_result_state_bounded_entry * S ((S (fom_index_step_result_state_bounded)) * d) + (fom_value_step_result_state_bounded))) /\ (exists fom_gap_step_result_state_bounded_value_bound. fom_gap_step_result_state_bounded_value_bound + S (fom_value_step_result_state_bounded) = n))) /\ (forall wpo_injective_left_step_result_state_injective wpo_injective_right_step_result_state_injective wpo_injective_value_step_result_state_injective. (exists wpo_gap_step_result_state_injective_left_bound. wpo_gap_step_result_state_injective_left_bound + S (wpo_injective_left_step_result_state_injective) = S (S (m + m))) -> (exists wpo_gap_step_result_state_injective_right_bound. wpo_gap_step_result_state_injective_right_bound + S (wpo_injective_right_step_result_state_injective) = S (S (m + m))) -> (((exists wpo_beta_height_step_result_state_injective_left_entry. wpo_beta_height_step_result_state_injective_left_entry + S (wpo_injective_value_step_result_state_injective) = S ((S (wpo_injective_left_step_result_state_injective)) * d)) /\ exists wpo_beta_quotient_step_result_state_injective_left_entry. z = wpo_beta_quotient_step_result_state_injective_left_entry * S ((S (wpo_injective_left_step_result_state_injective)) * d) + (wpo_injective_value_step_result_state_injective))) -> (((exists wpo_beta_height_step_result_state_injective_right_entry. wpo_beta_height_step_result_state_injective_right_entry + S (wpo_injective_value_step_result_state_injective) = S ((S (wpo_injective_right_step_result_state_injective)) * d)) /\ exists wpo_beta_quotient_step_result_state_injective_right_entry. z = wpo_beta_quotient_step_result_state_injective_right_entry * S ((S (wpo_injective_right_step_result_state_injective)) * d) + (wpo_injective_value_step_result_state_injective))) -> wpo_injective_left_step_result_state_injective = wpo_injective_right_step_result_state_injective))))) /\ (forall espi_pair_append_new_history. (exists wpo_gap_append_new_history_pair_bound. wpo_gap_append_new_history_pair_bound + S (espi_pair_append_new_history) = S m) -> exists espi_left_append_new_history espi_right_append_new_history. (((((exists wpo_beta_height_append_new_history_left_entry. wpo_beta_height_append_new_history_left_entry + S (espi_left_append_new_history) = S ((S (espi_pair_append_new_history + espi_pair_append_new_history)) * d)) /\ exists wpo_beta_quotient_append_new_history_left_entry. z = wpo_beta_quotient_append_new_history_left_entry * S ((S (espi_pair_append_new_history + espi_pair_append_new_history)) * d) + (espi_left_append_new_history))) /\ (((((exists wpo_beta_height_append_new_history_right_entry. wpo_beta_height_append_new_history_right_entry + S (espi_right_append_new_history) = S ((S (S (espi_pair_append_new_history + espi_pair_append_new_history))) * d)) /\ exists wpo_beta_quotient_append_new_history_right_entry. z = wpo_beta_quotient_append_new_history_right_entry * S ((S (S (espi_pair_append_new_history + espi_pair_append_new_history))) * d) + (espi_right_append_new_history))) /\ (((exists wpo_beta_height_append_new_history_scaled_edge. wpo_beta_height_append_new_history_scaled_edge + S (S espi_right_append_new_history) = S ((S (espi_left_append_new_history)) * v)) /\ exists wpo_beta_quotient_append_new_history_scaled_edge. u = wpo_beta_quotient_append_new_history_scaled_edge * S ((S (espi_left_append_new_history)) * v) + (S espi_right_append_new_history))))))))))
  66. 0066specialize scaled_inverse_pair_order_paired_state_step p
  67. 0067specialize scaled_inverse_pair_order_paired_state_step a
  68. 0068specialize scaled_inverse_pair_order_paired_state_step n
  69. 0069specialize scaled_inverse_pair_order_paired_state_step u
  70. 0070specialize scaled_inverse_pair_order_paired_state_step v
  71. 0071specialize scaled_inverse_pair_order_paired_state_step x
  72. 0072specialize scaled_inverse_pair_order_paired_state_step x1
  73. 0073specialize scaled_inverse_pair_order_paired_state_step m
  74. 0074apply scaled_inverse_pair_order_paired_state_step
  75. 0075exact hpn
  76. 0076exact hp
  77. 0077exact hnotqres
  78. 0078exact hprefix
  79. 0079exact hshort
  80. 0080exact hprevious_witness_witness_left
  81. 0081exact hprevious_witness_witness_right
  82. 0082cases hnext
  83. 0083cases hnext_witness
  84. 0084cases hnext_witness_witness
  85. 0085have hlength : S (S (m + m)) = S m + S m
  86. 0086specialize pair_order_double_succ_length (m + m)
  87. 0087specialize pair_order_double_succ_length m
  88. 0088apply pair_order_double_succ_length
  89. 0089refl
  90. 0090have hsuccessor_state : (∀ x. ∀ y. ∀ z. Lt(x,S m + S m) → BetaAt(x2,x3,x,y) → BetaAt(u,v,y,S z) → ContainsPrefix(x2,x3,S m + S m,z)) ∧ ((∀ x. Lt(x,S m + S m) → ∃ y. BetaAt(x2,x3,x,y) ∧ Lt(y,n)) ∧ InjectivePrefix(x2,x3,S m + S m))
    Exact native replay linehave hsuccessor_state : ((forall espo_position_successor_state_closed espo_source_successor_state_closed espo_mate_successor_state_closed. (exists wpo_gap_successor_state_closed_position_bound. wpo_gap_successor_state_closed_position_bound + S (espo_position_successor_state_closed) = S m + S m) -> (((exists wpo_beta_height_successor_state_closed_source_entry. wpo_beta_height_successor_state_closed_source_entry + S (espo_source_successor_state_closed) = S ((S (espo_position_successor_state_closed)) * x3)) /\ exists wpo_beta_quotient_successor_state_closed_source_entry. x2 = wpo_beta_quotient_successor_state_closed_source_entry * S ((S (espo_position_successor_state_closed)) * x3) + (espo_source_successor_state_closed))) -> (((exists wpo_beta_height_successor_state_closed_scaled_entry. wpo_beta_height_successor_state_closed_scaled_entry + S (S espo_mate_successor_state_closed) = S ((S (espo_source_successor_state_closed)) * v)) /\ exists wpo_beta_quotient_successor_state_closed_scaled_entry. u = wpo_beta_quotient_successor_state_closed_scaled_entry * S ((S (espo_source_successor_state_closed)) * v) + (S espo_mate_successor_state_closed))) -> exists espo_mate_position_successor_state_closed. ((exists wpo_gap_successor_state_closed_mate_bound. wpo_gap_successor_state_closed_mate_bound + S (espo_mate_position_successor_state_closed) = S m + S m) /\ (((exists wpo_beta_height_successor_state_closed_mate_entry. wpo_beta_height_successor_state_closed_mate_entry + S (espo_mate_successor_state_closed) = S ((S (espo_mate_position_successor_state_closed)) * x3)) /\ exists wpo_beta_quotient_successor_state_closed_mate_entry. x2 = wpo_beta_quotient_successor_state_closed_mate_entry * S ((S (espo_mate_position_successor_state_closed)) * x3) + (espo_mate_successor_state_closed))))) /\ (((forall fom_index_successor_state_bounded. (exists fom_gap_successor_state_bounded_index_bound. fom_gap_successor_state_bounded_index_bound + S (fom_index_successor_state_bounded) = S m + S m) -> exists fom_value_successor_state_bounded. ((((exists fom_beta_height_successor_state_bounded_entry. fom_beta_height_successor_state_bounded_entry + S (fom_value_successor_state_bounded) = S ((S (fom_index_successor_state_bounded)) * x3)) /\ exists fom_beta_quotient_successor_state_bounded_entry. x2 = fom_beta_quotient_successor_state_bounded_entry * S ((S (fom_index_successor_state_bounded)) * x3) + (fom_value_successor_state_bounded))) /\ (exists fom_gap_successor_state_bounded_value_bound. fom_gap_successor_state_bounded_value_bound + S (fom_value_successor_state_bounded) = n))) /\ (forall wpo_injective_left_successor_state_injective wpo_injective_right_successor_state_injective wpo_injective_value_successor_state_injective. (exists wpo_gap_successor_state_injective_left_bound. wpo_gap_successor_state_injective_left_bound + S (wpo_injective_left_successor_state_injective) = S m + S m) -> (exists wpo_gap_successor_state_injective_right_bound. wpo_gap_successor_state_injective_right_bound + S (wpo_injective_right_successor_state_injective) = S m + S m) -> (((exists wpo_beta_height_successor_state_injective_left_entry. wpo_beta_height_successor_state_injective_left_entry + S (wpo_injective_value_successor_state_injective) = S ((S (wpo_injective_left_successor_state_injective)) * x3)) /\ exists wpo_beta_quotient_successor_state_injective_left_entry. x2 = wpo_beta_quotient_successor_state_injective_left_entry * S ((S (wpo_injective_left_successor_state_injective)) * x3) + (wpo_injective_value_successor_state_injective))) -> (((exists wpo_beta_height_successor_state_injective_right_entry. wpo_beta_height_successor_state_injective_right_entry + S (wpo_injective_value_successor_state_injective) = S ((S (wpo_injective_right_successor_state_injective)) * x3)) /\ exists wpo_beta_quotient_successor_state_injective_right_entry. x2 = wpo_beta_quotient_successor_state_injective_right_entry * S ((S (wpo_injective_right_successor_state_injective)) * x3) + (wpo_injective_value_successor_state_injective))) -> wpo_injective_left_successor_state_injective = wpo_injective_right_successor_state_injective))))
  91. 0091rewrite <- hlength
  92. 0092rewrite <- hlength
  93. 0093rewrite <- hlength
  94. 0094rewrite <- hlength
  95. 0095rewrite <- hlength
  96. 0096exact hnext_witness_witness_left
  97. 0097exists x2
  98. 0098exists x3
  99. 0099split
  100. 0100exact hsuccessor_state
  101. 0101exact hnext_witness_witness_right