PA00B1 · theorem

prime_pair_order_paired_iteration

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

Iterate pair appends while retaining both bounded state and adjacent inverse history.

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

16 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0025 InjectivePrefix PD0027 ContainsPrefix

49 occurrences

Exact expanded native-PA statement
forall p n u v r. p = S n -> ((~(p = 1) /\ forall wip_prime_left_wpopi_prime wip_prime_right_wpopi_prime. p = wip_prime_left_wpopi_prime * wip_prime_right_wpopi_prime -> wip_prime_left_wpopi_prime = 1 \/ wip_prime_right_wpopi_prime = 1)) -> (forall wip_index_wpopi_inverse. (exists wip_gap_wpopi_inverse_prefix_bound. wip_gap_wpopi_inverse_prefix_bound + S wip_index_wpopi_inverse = n) -> exists wip_mate_wpopi_inverse. ((((exists wip_beta_height_wpopi_inverse_decoded. wip_beta_height_wpopi_inverse_decoded + S (wip_mate_wpopi_inverse) = S ((S (wip_index_wpopi_inverse)) * v)) /\ exists wip_beta_quotient_wpopi_inverse_decoded. u = wip_beta_quotient_wpopi_inverse_decoded * S ((S (wip_index_wpopi_inverse)) * v) + (wip_mate_wpopi_inverse))) /\ ((exists wip_gap_wpopi_inverse_inverse_index_bound. wip_gap_wpopi_inverse_inverse_index_bound + S wip_index_wpopi_inverse = n) /\ ((exists wip_gap_wpopi_inverse_inverse_mate_bound. wip_gap_wpopi_inverse_inverse_mate_bound + S wip_mate_wpopi_inverse = n) /\ (exists wip_mod_left_wpopi_inverse_inverse_mod wip_mod_right_wpopi_inverse_inverse_mod. ((S wip_index_wpopi_inverse) * S wip_mate_wpopi_inverse) + p * wip_mod_left_wpopi_inverse_inverse_mod = 1 + p * wip_mod_right_wpopi_inverse_inverse_mod))))) -> n = S r -> forall m k. (k + k) + S (S (m + m)) = n -> (exists b c. ((((forall wpo_position_wpopi_iteration_state_closed wpo_source_wpopi_iteration_state_closed wpo_mate_wpopi_iteration_state_closed. (exists wpo_gap_wpopi_iteration_state_closed_position_bound. wpo_gap_wpopi_iteration_state_closed_position_bound + S (wpo_position_wpopi_iteration_state_closed) = m + m) -> (((exists wpo_beta_height_wpopi_iteration_state_closed_source_entry. wpo_beta_height_wpopi_iteration_state_closed_source_entry + S (wpo_source_wpopi_iteration_state_closed) = S ((S (wpo_position_wpopi_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_closed_source_entry. b = wpo_beta_quotient_wpopi_iteration_state_closed_source_entry * S ((S (wpo_position_wpopi_iteration_state_closed)) * c) + (wpo_source_wpopi_iteration_state_closed))) -> (((exists wpo_beta_height_wpopi_iteration_state_closed_inverse_entry. wpo_beta_height_wpopi_iteration_state_closed_inverse_entry + S (wpo_mate_wpopi_iteration_state_closed) = S ((S (wpo_source_wpopi_iteration_state_closed)) * v)) /\ exists wpo_beta_quotient_wpopi_iteration_state_closed_inverse_entry. u = wpo_beta_quotient_wpopi_iteration_state_closed_inverse_entry * S ((S (wpo_source_wpopi_iteration_state_closed)) * v) + (wpo_mate_wpopi_iteration_state_closed))) -> exists wpo_mate_position_wpopi_iteration_state_closed. ((exists wpo_gap_wpopi_iteration_state_closed_mate_bound. wpo_gap_wpopi_iteration_state_closed_mate_bound + S (wpo_mate_position_wpopi_iteration_state_closed) = m + m) /\ (((exists wpo_beta_height_wpopi_iteration_state_closed_mate_entry. wpo_beta_height_wpopi_iteration_state_closed_mate_entry + S (wpo_mate_wpopi_iteration_state_closed) = S ((S (wpo_mate_position_wpopi_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_closed_mate_entry. b = wpo_beta_quotient_wpopi_iteration_state_closed_mate_entry * S ((S (wpo_mate_position_wpopi_iteration_state_closed)) * c) + (wpo_mate_wpopi_iteration_state_closed))))) /\ ((forall fom_index_wpopi_iteration_state_bounded. (exists fom_gap_wpopi_iteration_state_bounded_index_bound. fom_gap_wpopi_iteration_state_bounded_index_bound + S (fom_index_wpopi_iteration_state_bounded) = m + m) -> exists fom_value_wpopi_iteration_state_bounded. ((((exists fom_beta_height_wpopi_iteration_state_bounded_entry. fom_beta_height_wpopi_iteration_state_bounded_entry + S (fom_value_wpopi_iteration_state_bounded) = S ((S (fom_index_wpopi_iteration_state_bounded)) * c)) /\ exists fom_beta_quotient_wpopi_iteration_state_bounded_entry. b = fom_beta_quotient_wpopi_iteration_state_bounded_entry * S ((S (fom_index_wpopi_iteration_state_bounded)) * c) + (fom_value_wpopi_iteration_state_bounded))) /\ (exists fom_gap_wpopi_iteration_state_bounded_value_bound. fom_gap_wpopi_iteration_state_bounded_value_bound + S (fom_value_wpopi_iteration_state_bounded) = n))) /\ ((forall wpo_position_wpopi_iteration_state_nonendpoint wpo_value_wpopi_iteration_state_nonendpoint. (exists wpo_gap_wpopi_iteration_state_nonendpoint_position_bound. wpo_gap_wpopi_iteration_state_nonendpoint_position_bound + S (wpo_position_wpopi_iteration_state_nonendpoint) = m + m) -> (((exists wpo_beta_height_wpopi_iteration_state_nonendpoint_entry. wpo_beta_height_wpopi_iteration_state_nonendpoint_entry + S (wpo_value_wpopi_iteration_state_nonendpoint) = S ((S (wpo_position_wpopi_iteration_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_nonendpoint_entry. b = wpo_beta_quotient_wpopi_iteration_state_nonendpoint_entry * S ((S (wpo_position_wpopi_iteration_state_nonendpoint)) * c) + (wpo_value_wpopi_iteration_state_nonendpoint))) -> (~(wpo_value_wpopi_iteration_state_nonendpoint = 0) /\ ~((S wpo_value_wpopi_iteration_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpopi_iteration_state_injective wpo_injective_right_wpopi_iteration_state_injective wpo_injective_value_wpopi_iteration_state_injective. (exists wpo_gap_wpopi_iteration_state_injective_left_bound. wpo_gap_wpopi_iteration_state_injective_left_bound + S (wpo_injective_left_wpopi_iteration_state_injective) = m + m) -> (exists wpo_gap_wpopi_iteration_state_injective_right_bound. wpo_gap_wpopi_iteration_state_injective_right_bound + S (wpo_injective_right_wpopi_iteration_state_injective) = m + m) -> (((exists wpo_beta_height_wpopi_iteration_state_injective_left_entry. wpo_beta_height_wpopi_iteration_state_injective_left_entry + S (wpo_injective_value_wpopi_iteration_state_injective) = S ((S (wpo_injective_left_wpopi_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_injective_left_entry. b = wpo_beta_quotient_wpopi_iteration_state_injective_left_entry * S ((S (wpo_injective_left_wpopi_iteration_state_injective)) * c) + (wpo_injective_value_wpopi_iteration_state_injective))) -> (((exists wpo_beta_height_wpopi_iteration_state_injective_right_entry. wpo_beta_height_wpopi_iteration_state_injective_right_entry + S (wpo_injective_value_wpopi_iteration_state_injective) = S ((S (wpo_injective_right_wpopi_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_injective_right_entry. b = wpo_beta_quotient_wpopi_iteration_state_injective_right_entry * S ((S (wpo_injective_right_wpopi_iteration_state_injective)) * c) + (wpo_injective_value_wpopi_iteration_state_injective))) -> wpo_injective_left_wpopi_iteration_state_injective = wpo_injective_right_wpopi_iteration_state_injective))))) /\ (forall wpop_pair_wpopi_iteration_history. (exists wpo_gap_wpopi_iteration_history_pair_bound. wpo_gap_wpopi_iteration_history_pair_bound + S (wpop_pair_wpopi_iteration_history) = m) -> exists wpop_left_wpopi_iteration_history wpop_right_wpopi_iteration_history. ((((exists wpo_beta_height_wpopi_iteration_history_left_entry. wpo_beta_height_wpopi_iteration_history_left_entry + S (wpop_left_wpopi_iteration_history) = S ((S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_history_left_entry. b = wpo_beta_quotient_wpopi_iteration_history_left_entry * S ((S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history)) * c) + (wpop_left_wpopi_iteration_history))) /\ ((((exists wpo_beta_height_wpopi_iteration_history_right_entry. wpo_beta_height_wpopi_iteration_history_right_entry + S (wpop_right_wpopi_iteration_history) = S ((S (S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history))) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_history_right_entry. b = wpo_beta_quotient_wpopi_iteration_history_right_entry * S ((S (S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history))) * c) + (wpop_right_wpopi_iteration_history))) /\ (((exists wpo_beta_height_wpopi_iteration_history_inverse_entry. wpo_beta_height_wpopi_iteration_history_inverse_entry + S (wpop_right_wpopi_iteration_history) = S ((S (wpop_left_wpopi_iteration_history)) * v)) /\ exists wpo_beta_quotient_wpopi_iteration_history_inverse_entry. u = wpo_beta_quotient_wpopi_iteration_history_inverse_entry * S ((S (wpop_left_wpopi_iteration_history)) * v) + (wpop_right_wpopi_iteration_history))))))))

Proof neighborhood

Direct theorem prerequisites

PA00AA pair_order_state_zero PA00AB paired_inverse_witness_zero PA00AC pair_order_iteration_previous_balance PA00AD pair_order_iteration_step_room PA00B0 prime_pair_order_paired_state_step PA009U pair_order_double_succ_length

Direct theorem dependents

PA00B2 prime_pair_order_paired_terminal_state_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

104 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)
pair order state zeropaired inverse witness zeropair order iteration previous balancepair order iteration step roomprime 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 n
  3. L3
    intro u
  4. L4
    intro v
  5. L5
    intro r
  6. L6
    intro hpn
  7. L7
    intro hp
  8. L8
    intro hprefix
  9. L9
    intro hnr
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,z) → ContainsPrefix(b,c,0,z)) ∧ ((∀ x. Lt(x,0) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) ∧ ((∀ x. ∀ y. Lt(x,0) → BetaAt(b,c,x,y) → ¬y = 0 ∧ ¬S y = n) ∧ InjectivePrefix(b,c,0)))Definitions: Lt(x,0)BetaAt(b,c,x,y)BetaAt(u,v,y,z)ContainsPrefix(b,c,0,z)Lt(y,n)InjectivePrefix(b,c,0)Original native command in the exact edition
  2. L14
    specialize pair_order_state_zero u
  3. L15
    specialize pair_order_state_zero v
  4. L16
    specialize pair_order_state_zero n
  5. L17
    exact 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–30

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
  6. L30
    rewrite hzero
09Use earlier factsL31–36

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

  1. L31
    exact hzero_state_witness_witness
  2. L32
    specialize paired_inverse_witness_zero u
  3. L33
    specialize paired_inverse_witness_zero v
  4. L34
    specialize paired_inverse_witness_zero x
  5. L35
    specialize paired_inverse_witness_zero x1
  6. L36
    exact paired_inverse_witness_zero
10Fix variables and assumptionsL37–38

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

  1. L37
    intro k
  2. L38
    intro hbalance
11Establish hprevious_normalizeL39–42

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

  1. L39
    have hprevious_normalize : (k + k) + S (S (S m + S m)) = (S k + S k) + S (S (m + m))
  2. L40
    specialize pair_order_iteration_previous_balance m
  3. L41
    specialize pair_order_iteration_previous_balance k
  4. L42
    exact pair_order_iteration_previous_balance
12Establish hprevious_balanceL43–47

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

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

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

  1. L48
    have hprevious : ∃ 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. L49
    specialize IH (S k)
  3. L50
    apply IH
  4. L51
    exact hprevious_balance
14Separate the logical casesL52–54

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

  1. L52
    cases hprevious
  2. L53
    cases hprevious_witness
  3. L54
    cases hprevious_witness_witness
15Establish hroom_normalizeL55–58

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

  1. L55
    have hroom_normalize : (k + k) + S (S (S m + S m)) = S (k + k) + S (S (S (m + m)))
  2. L56
    specialize pair_order_iteration_step_room m
  3. L57
    specialize pair_order_iteration_step_room k
  4. L58
    exact pair_order_iteration_step_room
16Establish hroom_eqL59–63

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

  1. L59
    have hroom_eq : S (k + k) + S (S (S (m + m))) = n
  2. L60
    trans (k + k) + S (S (S m + S m))
  3. L61
    symm
  4. L62
    exact hroom_normalize
  5. L63
    exact hbalance
17Establish hroomL64–64

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

  1. L64
    have hroom : Lt(S S (m + m),n)Definitions: Lt(S S (m + m),n)Original native command in the exact edition
18Construct an explicit witnessL65–65

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

  1. L65
    exists S (k + k)
19Use earlier factsL66–66

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

  1. L66
    exact hroom_eq
20Establish hnextL67–76

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

  1. L67
    have hnext : ∃ z. ∃ d. (∀ x. ∀ y. ∀ k. Lt(x,S S (m + m)) → BetaAt(z,d,x,y) → BetaAt(u,v,y,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)) ∧ ((∀ x. ∀ y. Lt(x,S S (m + m)) → BetaAt(z,d,x,y) → ¬y = 0 ∧ ¬S 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,k)))Definitions: Lt(x,S S (m + m))BetaAt(z,d,x,y)BetaAt(u,v,y,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. L68
    specialize prime_pair_order_paired_state_step p
  3. L69
    specialize prime_pair_order_paired_state_step n
  4. L70
    specialize prime_pair_order_paired_state_step u
  5. L71
    specialize prime_pair_order_paired_state_step v
  6. L72
    specialize prime_pair_order_paired_state_step x
  7. L73
    specialize prime_pair_order_paired_state_step x1
  8. L74
    specialize prime_pair_order_paired_state_step m
  9. L75
    specialize prime_pair_order_paired_state_step r
  10. L76
    apply prime_pair_order_paired_state_step
21Use earlier factsL77–83

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

  1. L77
    exact hpn
  2. L78
    exact hp
  3. L79
    exact hprefix
  4. L80
    exact hnr
  5. L81
    exact hroom
  6. L82
    exact hprevious_witness_witness_left
  7. L83
    exact hprevious_witness_witness_right
22Separate the logical casesL84–86

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

  1. L84
    cases hnext
  2. L85
    cases hnext_witness
  3. L86
    cases hnext_witness_witness
23Establish hlengthL87–91

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

  1. L87
    have hlength : S (S (m + m)) = S m + S m
  2. L88
    specialize pair_order_double_succ_length (m + m)
  3. L89
    specialize pair_order_double_succ_length m
  4. L90
    apply pair_order_double_succ_length
  5. L91
    refl
24Establish hsuccessor_stateL92–99

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

  1. L92
    have hsuccessor_state : (∀ x. ∀ y. ∀ z. Lt(x,S m + S m) → BetaAt(x2,x3,x,y) → BetaAt(u,v,y,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)) ∧ ((∀ x. ∀ y. Lt(x,S m + S m) → BetaAt(x2,x3,x,y) → ¬y = 0 ∧ ¬S 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,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. L93
    rewrite <- hlength
  3. L94
    rewrite <- hlength
  4. L95
    rewrite <- hlength
  5. L96
    rewrite <- hlength
  6. L97
    rewrite <- hlength
  7. L98
    rewrite <- hlength
  8. L99
    exact hnext_witness_witness_left
25Construct an explicit witnessL100–101

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

  1. L100
    exists x2
  2. L101
    exists x3
26Separate the logical casesL102–102

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

  1. L102
    split
27Use earlier factsL103–104

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

  1. L103
    exact hsuccessor_state
  2. L104
    exact hnext_witness_witness_right

Library-wide reading audit

Original defined command ledger · 104 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro u
  4. 0004intro v
  5. 0005intro r
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro hprefix
  9. 0009intro hnr
  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,z) → ContainsPrefix(b,c,0,z)) ∧ ((∀ x. Lt(x,0) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) ∧ ((∀ x. ∀ y. Lt(x,0) → BetaAt(b,c,x,y) → ¬y = 0 ∧ ¬S y = n) ∧ InjectivePrefix(b,c,0)))
    Exact native replay linehave hzero_state : exists b c. (((forall wpo_position_wpopi_zero_state_closed wpo_source_wpopi_zero_state_closed wpo_mate_wpopi_zero_state_closed. (exists wpo_gap_wpopi_zero_state_closed_position_bound. wpo_gap_wpopi_zero_state_closed_position_bound + S (wpo_position_wpopi_zero_state_closed) = 0) -> (((exists wpo_beta_height_wpopi_zero_state_closed_source_entry. wpo_beta_height_wpopi_zero_state_closed_source_entry + S (wpo_source_wpopi_zero_state_closed) = S ((S (wpo_position_wpopi_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_zero_state_closed_source_entry. b = wpo_beta_quotient_wpopi_zero_state_closed_source_entry * S ((S (wpo_position_wpopi_zero_state_closed)) * c) + (wpo_source_wpopi_zero_state_closed))) -> (((exists wpo_beta_height_wpopi_zero_state_closed_inverse_entry. wpo_beta_height_wpopi_zero_state_closed_inverse_entry + S (wpo_mate_wpopi_zero_state_closed) = S ((S (wpo_source_wpopi_zero_state_closed)) * v)) /\ exists wpo_beta_quotient_wpopi_zero_state_closed_inverse_entry. u = wpo_beta_quotient_wpopi_zero_state_closed_inverse_entry * S ((S (wpo_source_wpopi_zero_state_closed)) * v) + (wpo_mate_wpopi_zero_state_closed))) -> exists wpo_mate_position_wpopi_zero_state_closed. ((exists wpo_gap_wpopi_zero_state_closed_mate_bound. wpo_gap_wpopi_zero_state_closed_mate_bound + S (wpo_mate_position_wpopi_zero_state_closed) = 0) /\ (((exists wpo_beta_height_wpopi_zero_state_closed_mate_entry. wpo_beta_height_wpopi_zero_state_closed_mate_entry + S (wpo_mate_wpopi_zero_state_closed) = S ((S (wpo_mate_position_wpopi_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_zero_state_closed_mate_entry. b = wpo_beta_quotient_wpopi_zero_state_closed_mate_entry * S ((S (wpo_mate_position_wpopi_zero_state_closed)) * c) + (wpo_mate_wpopi_zero_state_closed))))) /\ ((forall fom_index_wpopi_zero_state_bounded. (exists fom_gap_wpopi_zero_state_bounded_index_bound. fom_gap_wpopi_zero_state_bounded_index_bound + S (fom_index_wpopi_zero_state_bounded) = 0) -> exists fom_value_wpopi_zero_state_bounded. ((((exists fom_beta_height_wpopi_zero_state_bounded_entry. fom_beta_height_wpopi_zero_state_bounded_entry + S (fom_value_wpopi_zero_state_bounded) = S ((S (fom_index_wpopi_zero_state_bounded)) * c)) /\ exists fom_beta_quotient_wpopi_zero_state_bounded_entry. b = fom_beta_quotient_wpopi_zero_state_bounded_entry * S ((S (fom_index_wpopi_zero_state_bounded)) * c) + (fom_value_wpopi_zero_state_bounded))) /\ (exists fom_gap_wpopi_zero_state_bounded_value_bound. fom_gap_wpopi_zero_state_bounded_value_bound + S (fom_value_wpopi_zero_state_bounded) = n))) /\ ((forall wpo_position_wpopi_zero_state_nonendpoint wpo_value_wpopi_zero_state_nonendpoint. (exists wpo_gap_wpopi_zero_state_nonendpoint_position_bound. wpo_gap_wpopi_zero_state_nonendpoint_position_bound + S (wpo_position_wpopi_zero_state_nonendpoint) = 0) -> (((exists wpo_beta_height_wpopi_zero_state_nonendpoint_entry. wpo_beta_height_wpopi_zero_state_nonendpoint_entry + S (wpo_value_wpopi_zero_state_nonendpoint) = S ((S (wpo_position_wpopi_zero_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpopi_zero_state_nonendpoint_entry. b = wpo_beta_quotient_wpopi_zero_state_nonendpoint_entry * S ((S (wpo_position_wpopi_zero_state_nonendpoint)) * c) + (wpo_value_wpopi_zero_state_nonendpoint))) -> (~(wpo_value_wpopi_zero_state_nonendpoint = 0) /\ ~((S wpo_value_wpopi_zero_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpopi_zero_state_injective wpo_injective_right_wpopi_zero_state_injective wpo_injective_value_wpopi_zero_state_injective. (exists wpo_gap_wpopi_zero_state_injective_left_bound. wpo_gap_wpopi_zero_state_injective_left_bound + S (wpo_injective_left_wpopi_zero_state_injective) = 0) -> (exists wpo_gap_wpopi_zero_state_injective_right_bound. wpo_gap_wpopi_zero_state_injective_right_bound + S (wpo_injective_right_wpopi_zero_state_injective) = 0) -> (((exists wpo_beta_height_wpopi_zero_state_injective_left_entry. wpo_beta_height_wpopi_zero_state_injective_left_entry + S (wpo_injective_value_wpopi_zero_state_injective) = S ((S (wpo_injective_left_wpopi_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_zero_state_injective_left_entry. b = wpo_beta_quotient_wpopi_zero_state_injective_left_entry * S ((S (wpo_injective_left_wpopi_zero_state_injective)) * c) + (wpo_injective_value_wpopi_zero_state_injective))) -> (((exists wpo_beta_height_wpopi_zero_state_injective_right_entry. wpo_beta_height_wpopi_zero_state_injective_right_entry + S (wpo_injective_value_wpopi_zero_state_injective) = S ((S (wpo_injective_right_wpopi_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_zero_state_injective_right_entry. b = wpo_beta_quotient_wpopi_zero_state_injective_right_entry * S ((S (wpo_injective_right_wpopi_zero_state_injective)) * c) + (wpo_injective_value_wpopi_zero_state_injective))) -> wpo_injective_left_wpopi_zero_state_injective = wpo_injective_right_wpopi_zero_state_injective)))))
  14. 0014specialize pair_order_state_zero u
  15. 0015specialize pair_order_state_zero v
  16. 0016specialize pair_order_state_zero n
  17. 0017exact 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. 0030rewrite hzero
  31. 0031exact hzero_state_witness_witness
  32. 0032specialize paired_inverse_witness_zero u
  33. 0033specialize paired_inverse_witness_zero v
  34. 0034specialize paired_inverse_witness_zero x
  35. 0035specialize paired_inverse_witness_zero x1
  36. 0036exact paired_inverse_witness_zero
  37. 0037intro k
  38. 0038intro hbalance
  39. 0039have hprevious_normalize : (k + k) + S (S (S m + S m)) = (S k + S k) + S (S (m + m))
  40. 0040specialize pair_order_iteration_previous_balance m
  41. 0041specialize pair_order_iteration_previous_balance k
  42. 0042exact pair_order_iteration_previous_balance
  43. 0043have hprevious_balance : (S k + S k) + S (S (m + m)) = n
  44. 0044trans (k + k) + S (S (S m + S m))
  45. 0045symm
  46. 0046exact hprevious_normalize
  47. 0047exact hbalance
  48. 0048have hprevious : ∃ 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 hprevious : exists b c. ((((forall wpo_position_wpopi_iteration_state_closed wpo_source_wpopi_iteration_state_closed wpo_mate_wpopi_iteration_state_closed. (exists wpo_gap_wpopi_iteration_state_closed_position_bound. wpo_gap_wpopi_iteration_state_closed_position_bound + S (wpo_position_wpopi_iteration_state_closed) = m + m) -> (((exists wpo_beta_height_wpopi_iteration_state_closed_source_entry. wpo_beta_height_wpopi_iteration_state_closed_source_entry + S (wpo_source_wpopi_iteration_state_closed) = S ((S (wpo_position_wpopi_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_closed_source_entry. b = wpo_beta_quotient_wpopi_iteration_state_closed_source_entry * S ((S (wpo_position_wpopi_iteration_state_closed)) * c) + (wpo_source_wpopi_iteration_state_closed))) -> (((exists wpo_beta_height_wpopi_iteration_state_closed_inverse_entry. wpo_beta_height_wpopi_iteration_state_closed_inverse_entry + S (wpo_mate_wpopi_iteration_state_closed) = S ((S (wpo_source_wpopi_iteration_state_closed)) * v)) /\ exists wpo_beta_quotient_wpopi_iteration_state_closed_inverse_entry. u = wpo_beta_quotient_wpopi_iteration_state_closed_inverse_entry * S ((S (wpo_source_wpopi_iteration_state_closed)) * v) + (wpo_mate_wpopi_iteration_state_closed))) -> exists wpo_mate_position_wpopi_iteration_state_closed. ((exists wpo_gap_wpopi_iteration_state_closed_mate_bound. wpo_gap_wpopi_iteration_state_closed_mate_bound + S (wpo_mate_position_wpopi_iteration_state_closed) = m + m) /\ (((exists wpo_beta_height_wpopi_iteration_state_closed_mate_entry. wpo_beta_height_wpopi_iteration_state_closed_mate_entry + S (wpo_mate_wpopi_iteration_state_closed) = S ((S (wpo_mate_position_wpopi_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_closed_mate_entry. b = wpo_beta_quotient_wpopi_iteration_state_closed_mate_entry * S ((S (wpo_mate_position_wpopi_iteration_state_closed)) * c) + (wpo_mate_wpopi_iteration_state_closed))))) /\ ((forall fom_index_wpopi_iteration_state_bounded. (exists fom_gap_wpopi_iteration_state_bounded_index_bound. fom_gap_wpopi_iteration_state_bounded_index_bound + S (fom_index_wpopi_iteration_state_bounded) = m + m) -> exists fom_value_wpopi_iteration_state_bounded. ((((exists fom_beta_height_wpopi_iteration_state_bounded_entry. fom_beta_height_wpopi_iteration_state_bounded_entry + S (fom_value_wpopi_iteration_state_bounded) = S ((S (fom_index_wpopi_iteration_state_bounded)) * c)) /\ exists fom_beta_quotient_wpopi_iteration_state_bounded_entry. b = fom_beta_quotient_wpopi_iteration_state_bounded_entry * S ((S (fom_index_wpopi_iteration_state_bounded)) * c) + (fom_value_wpopi_iteration_state_bounded))) /\ (exists fom_gap_wpopi_iteration_state_bounded_value_bound. fom_gap_wpopi_iteration_state_bounded_value_bound + S (fom_value_wpopi_iteration_state_bounded) = n))) /\ ((forall wpo_position_wpopi_iteration_state_nonendpoint wpo_value_wpopi_iteration_state_nonendpoint. (exists wpo_gap_wpopi_iteration_state_nonendpoint_position_bound. wpo_gap_wpopi_iteration_state_nonendpoint_position_bound + S (wpo_position_wpopi_iteration_state_nonendpoint) = m + m) -> (((exists wpo_beta_height_wpopi_iteration_state_nonendpoint_entry. wpo_beta_height_wpopi_iteration_state_nonendpoint_entry + S (wpo_value_wpopi_iteration_state_nonendpoint) = S ((S (wpo_position_wpopi_iteration_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_nonendpoint_entry. b = wpo_beta_quotient_wpopi_iteration_state_nonendpoint_entry * S ((S (wpo_position_wpopi_iteration_state_nonendpoint)) * c) + (wpo_value_wpopi_iteration_state_nonendpoint))) -> (~(wpo_value_wpopi_iteration_state_nonendpoint = 0) /\ ~((S wpo_value_wpopi_iteration_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpopi_iteration_state_injective wpo_injective_right_wpopi_iteration_state_injective wpo_injective_value_wpopi_iteration_state_injective. (exists wpo_gap_wpopi_iteration_state_injective_left_bound. wpo_gap_wpopi_iteration_state_injective_left_bound + S (wpo_injective_left_wpopi_iteration_state_injective) = m + m) -> (exists wpo_gap_wpopi_iteration_state_injective_right_bound. wpo_gap_wpopi_iteration_state_injective_right_bound + S (wpo_injective_right_wpopi_iteration_state_injective) = m + m) -> (((exists wpo_beta_height_wpopi_iteration_state_injective_left_entry. wpo_beta_height_wpopi_iteration_state_injective_left_entry + S (wpo_injective_value_wpopi_iteration_state_injective) = S ((S (wpo_injective_left_wpopi_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_injective_left_entry. b = wpo_beta_quotient_wpopi_iteration_state_injective_left_entry * S ((S (wpo_injective_left_wpopi_iteration_state_injective)) * c) + (wpo_injective_value_wpopi_iteration_state_injective))) -> (((exists wpo_beta_height_wpopi_iteration_state_injective_right_entry. wpo_beta_height_wpopi_iteration_state_injective_right_entry + S (wpo_injective_value_wpopi_iteration_state_injective) = S ((S (wpo_injective_right_wpopi_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_injective_right_entry. b = wpo_beta_quotient_wpopi_iteration_state_injective_right_entry * S ((S (wpo_injective_right_wpopi_iteration_state_injective)) * c) + (wpo_injective_value_wpopi_iteration_state_injective))) -> wpo_injective_left_wpopi_iteration_state_injective = wpo_injective_right_wpopi_iteration_state_injective))))) /\ (forall wpop_pair_wpopi_iteration_history. (exists wpo_gap_wpopi_iteration_history_pair_bound. wpo_gap_wpopi_iteration_history_pair_bound + S (wpop_pair_wpopi_iteration_history) = m) -> exists wpop_left_wpopi_iteration_history wpop_right_wpopi_iteration_history. ((((exists wpo_beta_height_wpopi_iteration_history_left_entry. wpo_beta_height_wpopi_iteration_history_left_entry + S (wpop_left_wpopi_iteration_history) = S ((S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_history_left_entry. b = wpo_beta_quotient_wpopi_iteration_history_left_entry * S ((S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history)) * c) + (wpop_left_wpopi_iteration_history))) /\ ((((exists wpo_beta_height_wpopi_iteration_history_right_entry. wpo_beta_height_wpopi_iteration_history_right_entry + S (wpop_right_wpopi_iteration_history) = S ((S (S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history))) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_history_right_entry. b = wpo_beta_quotient_wpopi_iteration_history_right_entry * S ((S (S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history))) * c) + (wpop_right_wpopi_iteration_history))) /\ (((exists wpo_beta_height_wpopi_iteration_history_inverse_entry. wpo_beta_height_wpopi_iteration_history_inverse_entry + S (wpop_right_wpopi_iteration_history) = S ((S (wpop_left_wpopi_iteration_history)) * v)) /\ exists wpo_beta_quotient_wpopi_iteration_history_inverse_entry. u = wpo_beta_quotient_wpopi_iteration_history_inverse_entry * S ((S (wpop_left_wpopi_iteration_history)) * v) + (wpop_right_wpopi_iteration_history)))))))
  49. 0049specialize IH (S k)
  50. 0050apply IH
  51. 0051exact hprevious_balance
  52. 0052cases hprevious
  53. 0053cases hprevious_witness
  54. 0054cases hprevious_witness_witness
  55. 0055have hroom_normalize : (k + k) + S (S (S m + S m)) = S (k + k) + S (S (S (m + m)))
  56. 0056specialize pair_order_iteration_step_room m
  57. 0057specialize pair_order_iteration_step_room k
  58. 0058exact pair_order_iteration_step_room
  59. 0059have hroom_eq : S (k + k) + S (S (S (m + m))) = n
  60. 0060trans (k + k) + S (S (S m + S m))
  61. 0061symm
  62. 0062exact hroom_normalize
  63. 0063exact hbalance
  64. 0064have hroom : Lt(S S (m + m),n)
    Exact native replay linehave hroom : exists h. h + S (S (S (m + m))) = n
  65. 0065exists S (k + k)
  66. 0066exact hroom_eq
  67. 0067have hnext : ∃ z. ∃ d. (∀ x. ∀ y. ∀ k. Lt(x,S S (m + m)) → BetaAt(z,d,x,y) → BetaAt(u,v,y,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)) ∧ ((∀ x. ∀ y. Lt(x,S S (m + m)) → BetaAt(z,d,x,y) → ¬y = 0 ∧ ¬S 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,k)))
    Exact native replay linehave hnext : exists z d. ((((forall wpo_position_wpopi_next_state_closed wpo_source_wpopi_next_state_closed wpo_mate_wpopi_next_state_closed. (exists wpo_gap_wpopi_next_state_closed_position_bound. wpo_gap_wpopi_next_state_closed_position_bound + S (wpo_position_wpopi_next_state_closed) = S (S (m + m))) -> (((exists wpo_beta_height_wpopi_next_state_closed_source_entry. wpo_beta_height_wpopi_next_state_closed_source_entry + S (wpo_source_wpopi_next_state_closed) = S ((S (wpo_position_wpopi_next_state_closed)) * d)) /\ exists wpo_beta_quotient_wpopi_next_state_closed_source_entry. z = wpo_beta_quotient_wpopi_next_state_closed_source_entry * S ((S (wpo_position_wpopi_next_state_closed)) * d) + (wpo_source_wpopi_next_state_closed))) -> (((exists wpo_beta_height_wpopi_next_state_closed_inverse_entry. wpo_beta_height_wpopi_next_state_closed_inverse_entry + S (wpo_mate_wpopi_next_state_closed) = S ((S (wpo_source_wpopi_next_state_closed)) * v)) /\ exists wpo_beta_quotient_wpopi_next_state_closed_inverse_entry. u = wpo_beta_quotient_wpopi_next_state_closed_inverse_entry * S ((S (wpo_source_wpopi_next_state_closed)) * v) + (wpo_mate_wpopi_next_state_closed))) -> exists wpo_mate_position_wpopi_next_state_closed. ((exists wpo_gap_wpopi_next_state_closed_mate_bound. wpo_gap_wpopi_next_state_closed_mate_bound + S (wpo_mate_position_wpopi_next_state_closed) = S (S (m + m))) /\ (((exists wpo_beta_height_wpopi_next_state_closed_mate_entry. wpo_beta_height_wpopi_next_state_closed_mate_entry + S (wpo_mate_wpopi_next_state_closed) = S ((S (wpo_mate_position_wpopi_next_state_closed)) * d)) /\ exists wpo_beta_quotient_wpopi_next_state_closed_mate_entry. z = wpo_beta_quotient_wpopi_next_state_closed_mate_entry * S ((S (wpo_mate_position_wpopi_next_state_closed)) * d) + (wpo_mate_wpopi_next_state_closed))))) /\ ((forall fom_index_wpopi_next_state_bounded. (exists fom_gap_wpopi_next_state_bounded_index_bound. fom_gap_wpopi_next_state_bounded_index_bound + S (fom_index_wpopi_next_state_bounded) = S (S (m + m))) -> exists fom_value_wpopi_next_state_bounded. ((((exists fom_beta_height_wpopi_next_state_bounded_entry. fom_beta_height_wpopi_next_state_bounded_entry + S (fom_value_wpopi_next_state_bounded) = S ((S (fom_index_wpopi_next_state_bounded)) * d)) /\ exists fom_beta_quotient_wpopi_next_state_bounded_entry. z = fom_beta_quotient_wpopi_next_state_bounded_entry * S ((S (fom_index_wpopi_next_state_bounded)) * d) + (fom_value_wpopi_next_state_bounded))) /\ (exists fom_gap_wpopi_next_state_bounded_value_bound. fom_gap_wpopi_next_state_bounded_value_bound + S (fom_value_wpopi_next_state_bounded) = n))) /\ ((forall wpo_position_wpopi_next_state_nonendpoint wpo_value_wpopi_next_state_nonendpoint. (exists wpo_gap_wpopi_next_state_nonendpoint_position_bound. wpo_gap_wpopi_next_state_nonendpoint_position_bound + S (wpo_position_wpopi_next_state_nonendpoint) = S (S (m + m))) -> (((exists wpo_beta_height_wpopi_next_state_nonendpoint_entry. wpo_beta_height_wpopi_next_state_nonendpoint_entry + S (wpo_value_wpopi_next_state_nonendpoint) = S ((S (wpo_position_wpopi_next_state_nonendpoint)) * d)) /\ exists wpo_beta_quotient_wpopi_next_state_nonendpoint_entry. z = wpo_beta_quotient_wpopi_next_state_nonendpoint_entry * S ((S (wpo_position_wpopi_next_state_nonendpoint)) * d) + (wpo_value_wpopi_next_state_nonendpoint))) -> (~(wpo_value_wpopi_next_state_nonendpoint = 0) /\ ~((S wpo_value_wpopi_next_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpopi_next_state_injective wpo_injective_right_wpopi_next_state_injective wpo_injective_value_wpopi_next_state_injective. (exists wpo_gap_wpopi_next_state_injective_left_bound. wpo_gap_wpopi_next_state_injective_left_bound + S (wpo_injective_left_wpopi_next_state_injective) = S (S (m + m))) -> (exists wpo_gap_wpopi_next_state_injective_right_bound. wpo_gap_wpopi_next_state_injective_right_bound + S (wpo_injective_right_wpopi_next_state_injective) = S (S (m + m))) -> (((exists wpo_beta_height_wpopi_next_state_injective_left_entry. wpo_beta_height_wpopi_next_state_injective_left_entry + S (wpo_injective_value_wpopi_next_state_injective) = S ((S (wpo_injective_left_wpopi_next_state_injective)) * d)) /\ exists wpo_beta_quotient_wpopi_next_state_injective_left_entry. z = wpo_beta_quotient_wpopi_next_state_injective_left_entry * S ((S (wpo_injective_left_wpopi_next_state_injective)) * d) + (wpo_injective_value_wpopi_next_state_injective))) -> (((exists wpo_beta_height_wpopi_next_state_injective_right_entry. wpo_beta_height_wpopi_next_state_injective_right_entry + S (wpo_injective_value_wpopi_next_state_injective) = S ((S (wpo_injective_right_wpopi_next_state_injective)) * d)) /\ exists wpo_beta_quotient_wpopi_next_state_injective_right_entry. z = wpo_beta_quotient_wpopi_next_state_injective_right_entry * S ((S (wpo_injective_right_wpopi_next_state_injective)) * d) + (wpo_injective_value_wpopi_next_state_injective))) -> wpo_injective_left_wpopi_next_state_injective = wpo_injective_right_wpopi_next_state_injective))))) /\ (forall wpop_pair_wpop_new_pairs. (exists wpo_gap_wpop_new_pairs_pair_bound. wpo_gap_wpop_new_pairs_pair_bound + S (wpop_pair_wpop_new_pairs) = S m) -> exists wpop_left_wpop_new_pairs wpop_right_wpop_new_pairs. ((((exists wpo_beta_height_wpop_new_pairs_left_entry. wpo_beta_height_wpop_new_pairs_left_entry + S (wpop_left_wpop_new_pairs) = S ((S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs)) * d)) /\ exists wpo_beta_quotient_wpop_new_pairs_left_entry. z = wpo_beta_quotient_wpop_new_pairs_left_entry * S ((S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs)) * d) + (wpop_left_wpop_new_pairs))) /\ ((((exists wpo_beta_height_wpop_new_pairs_right_entry. wpo_beta_height_wpop_new_pairs_right_entry + S (wpop_right_wpop_new_pairs) = S ((S (S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs))) * d)) /\ exists wpo_beta_quotient_wpop_new_pairs_right_entry. z = wpo_beta_quotient_wpop_new_pairs_right_entry * S ((S (S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs))) * d) + (wpop_right_wpop_new_pairs))) /\ (((exists wpo_beta_height_wpop_new_pairs_inverse_entry. wpo_beta_height_wpop_new_pairs_inverse_entry + S (wpop_right_wpop_new_pairs) = S ((S (wpop_left_wpop_new_pairs)) * v)) /\ exists wpo_beta_quotient_wpop_new_pairs_inverse_entry. u = wpo_beta_quotient_wpop_new_pairs_inverse_entry * S ((S (wpop_left_wpop_new_pairs)) * v) + (wpop_right_wpop_new_pairs)))))))
  68. 0068specialize prime_pair_order_paired_state_step p
  69. 0069specialize prime_pair_order_paired_state_step n
  70. 0070specialize prime_pair_order_paired_state_step u
  71. 0071specialize prime_pair_order_paired_state_step v
  72. 0072specialize prime_pair_order_paired_state_step x
  73. 0073specialize prime_pair_order_paired_state_step x1
  74. 0074specialize prime_pair_order_paired_state_step m
  75. 0075specialize prime_pair_order_paired_state_step r
  76. 0076apply prime_pair_order_paired_state_step
  77. 0077exact hpn
  78. 0078exact hp
  79. 0079exact hprefix
  80. 0080exact hnr
  81. 0081exact hroom
  82. 0082exact hprevious_witness_witness_left
  83. 0083exact hprevious_witness_witness_right
  84. 0084cases hnext
  85. 0085cases hnext_witness
  86. 0086cases hnext_witness_witness
  87. 0087have hlength : S (S (m + m)) = S m + S m
  88. 0088specialize pair_order_double_succ_length (m + m)
  89. 0089specialize pair_order_double_succ_length m
  90. 0090apply pair_order_double_succ_length
  91. 0091refl
  92. 0092have hsuccessor_state : (∀ x. ∀ y. ∀ z. Lt(x,S m + S m) → BetaAt(x2,x3,x,y) → BetaAt(u,v,y,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)) ∧ ((∀ x. ∀ y. Lt(x,S m + S m) → BetaAt(x2,x3,x,y) → ¬y = 0 ∧ ¬S y = n) ∧ InjectivePrefix(x2,x3,S m + S m)))
    Exact native replay linehave hsuccessor_state : ((forall wpo_position_wpopi_successor_state_closed wpo_source_wpopi_successor_state_closed wpo_mate_wpopi_successor_state_closed. (exists wpo_gap_wpopi_successor_state_closed_position_bound. wpo_gap_wpopi_successor_state_closed_position_bound + S (wpo_position_wpopi_successor_state_closed) = S m + S m) -> (((exists wpo_beta_height_wpopi_successor_state_closed_source_entry. wpo_beta_height_wpopi_successor_state_closed_source_entry + S (wpo_source_wpopi_successor_state_closed) = S ((S (wpo_position_wpopi_successor_state_closed)) * x3)) /\ exists wpo_beta_quotient_wpopi_successor_state_closed_source_entry. x2 = wpo_beta_quotient_wpopi_successor_state_closed_source_entry * S ((S (wpo_position_wpopi_successor_state_closed)) * x3) + (wpo_source_wpopi_successor_state_closed))) -> (((exists wpo_beta_height_wpopi_successor_state_closed_inverse_entry. wpo_beta_height_wpopi_successor_state_closed_inverse_entry + S (wpo_mate_wpopi_successor_state_closed) = S ((S (wpo_source_wpopi_successor_state_closed)) * v)) /\ exists wpo_beta_quotient_wpopi_successor_state_closed_inverse_entry. u = wpo_beta_quotient_wpopi_successor_state_closed_inverse_entry * S ((S (wpo_source_wpopi_successor_state_closed)) * v) + (wpo_mate_wpopi_successor_state_closed))) -> exists wpo_mate_position_wpopi_successor_state_closed. ((exists wpo_gap_wpopi_successor_state_closed_mate_bound. wpo_gap_wpopi_successor_state_closed_mate_bound + S (wpo_mate_position_wpopi_successor_state_closed) = S m + S m) /\ (((exists wpo_beta_height_wpopi_successor_state_closed_mate_entry. wpo_beta_height_wpopi_successor_state_closed_mate_entry + S (wpo_mate_wpopi_successor_state_closed) = S ((S (wpo_mate_position_wpopi_successor_state_closed)) * x3)) /\ exists wpo_beta_quotient_wpopi_successor_state_closed_mate_entry. x2 = wpo_beta_quotient_wpopi_successor_state_closed_mate_entry * S ((S (wpo_mate_position_wpopi_successor_state_closed)) * x3) + (wpo_mate_wpopi_successor_state_closed))))) /\ ((forall fom_index_wpopi_successor_state_bounded. (exists fom_gap_wpopi_successor_state_bounded_index_bound. fom_gap_wpopi_successor_state_bounded_index_bound + S (fom_index_wpopi_successor_state_bounded) = S m + S m) -> exists fom_value_wpopi_successor_state_bounded. ((((exists fom_beta_height_wpopi_successor_state_bounded_entry. fom_beta_height_wpopi_successor_state_bounded_entry + S (fom_value_wpopi_successor_state_bounded) = S ((S (fom_index_wpopi_successor_state_bounded)) * x3)) /\ exists fom_beta_quotient_wpopi_successor_state_bounded_entry. x2 = fom_beta_quotient_wpopi_successor_state_bounded_entry * S ((S (fom_index_wpopi_successor_state_bounded)) * x3) + (fom_value_wpopi_successor_state_bounded))) /\ (exists fom_gap_wpopi_successor_state_bounded_value_bound. fom_gap_wpopi_successor_state_bounded_value_bound + S (fom_value_wpopi_successor_state_bounded) = n))) /\ ((forall wpo_position_wpopi_successor_state_nonendpoint wpo_value_wpopi_successor_state_nonendpoint. (exists wpo_gap_wpopi_successor_state_nonendpoint_position_bound. wpo_gap_wpopi_successor_state_nonendpoint_position_bound + S (wpo_position_wpopi_successor_state_nonendpoint) = S m + S m) -> (((exists wpo_beta_height_wpopi_successor_state_nonendpoint_entry. wpo_beta_height_wpopi_successor_state_nonendpoint_entry + S (wpo_value_wpopi_successor_state_nonendpoint) = S ((S (wpo_position_wpopi_successor_state_nonendpoint)) * x3)) /\ exists wpo_beta_quotient_wpopi_successor_state_nonendpoint_entry. x2 = wpo_beta_quotient_wpopi_successor_state_nonendpoint_entry * S ((S (wpo_position_wpopi_successor_state_nonendpoint)) * x3) + (wpo_value_wpopi_successor_state_nonendpoint))) -> (~(wpo_value_wpopi_successor_state_nonendpoint = 0) /\ ~((S wpo_value_wpopi_successor_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpopi_successor_state_injective wpo_injective_right_wpopi_successor_state_injective wpo_injective_value_wpopi_successor_state_injective. (exists wpo_gap_wpopi_successor_state_injective_left_bound. wpo_gap_wpopi_successor_state_injective_left_bound + S (wpo_injective_left_wpopi_successor_state_injective) = S m + S m) -> (exists wpo_gap_wpopi_successor_state_injective_right_bound. wpo_gap_wpopi_successor_state_injective_right_bound + S (wpo_injective_right_wpopi_successor_state_injective) = S m + S m) -> (((exists wpo_beta_height_wpopi_successor_state_injective_left_entry. wpo_beta_height_wpopi_successor_state_injective_left_entry + S (wpo_injective_value_wpopi_successor_state_injective) = S ((S (wpo_injective_left_wpopi_successor_state_injective)) * x3)) /\ exists wpo_beta_quotient_wpopi_successor_state_injective_left_entry. x2 = wpo_beta_quotient_wpopi_successor_state_injective_left_entry * S ((S (wpo_injective_left_wpopi_successor_state_injective)) * x3) + (wpo_injective_value_wpopi_successor_state_injective))) -> (((exists wpo_beta_height_wpopi_successor_state_injective_right_entry. wpo_beta_height_wpopi_successor_state_injective_right_entry + S (wpo_injective_value_wpopi_successor_state_injective) = S ((S (wpo_injective_right_wpopi_successor_state_injective)) * x3)) /\ exists wpo_beta_quotient_wpopi_successor_state_injective_right_entry. x2 = wpo_beta_quotient_wpopi_successor_state_injective_right_entry * S ((S (wpo_injective_right_wpopi_successor_state_injective)) * x3) + (wpo_injective_value_wpopi_successor_state_injective))) -> wpo_injective_left_wpopi_successor_state_injective = wpo_injective_right_wpopi_successor_state_injective))))
  93. 0093rewrite <- hlength
  94. 0094rewrite <- hlength
  95. 0095rewrite <- hlength
  96. 0096rewrite <- hlength
  97. 0097rewrite <- hlength
  98. 0098rewrite <- hlength
  99. 0099exact hnext_witness_witness_left
  100. 0100exists x2
  101. 0101exists x3
  102. 0102split
  103. 0103exact hsuccessor_state
  104. 0104exact hnext_witness_witness_right