MX000A

signed_positive_table_entry_transport

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Transport a real positive lookup across prefix equality by first constructing the target lookup; no encoding or zero-value equality is required.

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 expanded first-order arithmetic statement

forall N F G i z. (exists dst_positive_code_entry_target_table dst_positive_scale_entry_target_table dst_negative_code_entry_target_table dst_negative_scale_entry_target_table. (((G) = (((((dst_positive_code_entry_target_table) + (dst_positive_scale_entry_target_table)) * S ((dst_positive_code_entry_target_table) + (dst_positive_scale_entry_target_table)) + ((dst_positive_scale_entry_target_table) + (dst_positive_scale_entry_target_table))) + (((dst_negative_code_entry_target_table) + (dst_negative_scale_entry_target_table)) * S ((dst_negative_code_entry_target_table) + (dst_negative_scale_entry_target_table)) + ((dst_negative_scale_entry_target_table) + (dst_negative_scale_entry_target_table)))) * S ((((dst_positive_code_entry_target_table) + (dst_positive_scale_entry_target_table)) * S ((dst_positive_code_entry_target_table) + (dst_positive_scale_entry_target_table)) + ((dst_positive_scale_entry_target_table) + (dst_positive_scale_entry_target_table))) + (((dst_negative_code_entry_target_table) + (dst_negative_scale_entry_target_table)) * S ((dst_negative_code_entry_target_table) + (dst_negative_scale_entry_target_table)) + ((dst_negative_scale_entry_target_table) + (dst_negative_scale_entry_target_table)))) + ((((dst_negative_code_entry_target_table) + (dst_negative_scale_entry_target_table)) * S ((dst_negative_code_entry_target_table) + (dst_negative_scale_entry_target_table)) + ((dst_negative_scale_entry_target_table) + (dst_negative_scale_entry_target_table))) + (((dst_negative_code_entry_target_table) + (dst_negative_scale_entry_target_table)) * S ((dst_negative_code_entry_target_table) + (dst_negative_scale_entry_target_table)) + ((dst_negative_scale_entry_target_table) + (dst_negative_scale_entry_target_table)))))) /\ (forall dst_index_entry_target_table. (exists pvs_le_gap_entry_target_tabledomain. pvs_le_gap_entry_target_tabledomain + (dst_index_entry_target_table) = (N)) -> exists dst_positive_entry_target_table dst_negative_entry_target_table dst_value_entry_target_table. ((((exists ff_h_pvs_entry_target_tableentrypositive. ff_h_pvs_entry_target_tableentrypositive + S (dst_positive_entry_target_table) = S ((S (dst_index_entry_target_table)) * dst_positive_scale_entry_target_table)) /\ exists ff_q_pvs_entry_target_tableentrypositive. dst_positive_code_entry_target_table = ff_q_pvs_entry_target_tableentrypositive * S ((S (dst_index_entry_target_table)) * dst_positive_scale_entry_target_table) + (dst_positive_entry_target_table))) /\ (((((exists ff_h_pvs_entry_target_tableentrynegative. ff_h_pvs_entry_target_tableentrynegative + S (dst_negative_entry_target_table) = S ((S (dst_index_entry_target_table)) * dst_negative_scale_entry_target_table)) /\ exists ff_q_pvs_entry_target_tableentrynegative. dst_negative_code_entry_target_table = ff_q_pvs_entry_target_tableentrynegative * S ((S (dst_index_entry_target_table)) * dst_negative_scale_entry_target_table) + (dst_negative_entry_target_table))) /\ (exists ge_balance_positive_entry_target_tableentryvalue ge_balance_negative_entry_target_tableentryvalue. (((((dst_value_entry_target_table) = 2 * (ge_balance_positive_entry_target_tableentryvalue) /\ (ge_balance_negative_entry_target_tableentryvalue) = 0) \/ exists ge_signed_half_entry_target_tableentryvaluedecode. (((dst_value_entry_target_table) = 2 * ge_signed_half_entry_target_tableentryvaluedecode + 1 /\ (ge_balance_positive_entry_target_tableentryvalue) = 0) /\ (ge_balance_negative_entry_target_tableentryvalue) = S ge_signed_half_entry_target_tableentryvaluedecode))) /\ ((dst_positive_entry_target_table) + ge_balance_negative_entry_target_tableentryvalue = (dst_negative_entry_target_table) + ge_balance_positive_entry_target_tableentryvalue))))))))) -> (forall dm_index_entry_positive_equal dm_first_value_entry_positive_equal dm_second_value_entry_positive_equal. ~(dm_index_entry_positive_equal=0) -> (exists pvs_le_gap_entry_positive_equaldomain. pvs_le_gap_entry_positive_equaldomain + (dm_index_entry_positive_equal) = (N)) -> (exists dst_positive_code_entry_positive_equalfirst dst_positive_scale_entry_positive_equalfirst dst_negative_code_entry_positive_equalfirst dst_negative_scale_entry_positive_equalfirst dst_positive_entry_positive_equalfirst dst_negative_entry_positive_equalfirst. (((F) = (((((dst_positive_code_entry_positive_equalfirst) + (dst_positive_scale_entry_positive_equalfirst)) * S ((dst_positive_code_entry_positive_equalfirst) + (dst_positive_scale_entry_positive_equalfirst)) + ((dst_positive_scale_entry_positive_equalfirst) + (dst_positive_scale_entry_positive_equalfirst))) + (((dst_negative_code_entry_positive_equalfirst) + (dst_negative_scale_entry_positive_equalfirst)) * S ((dst_negative_code_entry_positive_equalfirst) + (dst_negative_scale_entry_positive_equalfirst)) + ((dst_negative_scale_entry_positive_equalfirst) + (dst_negative_scale_entry_positive_equalfirst)))) * S ((((dst_positive_code_entry_positive_equalfirst) + (dst_positive_scale_entry_positive_equalfirst)) * S ((dst_positive_code_entry_positive_equalfirst) + (dst_positive_scale_entry_positive_equalfirst)) + ((dst_positive_scale_entry_positive_equalfirst) + (dst_positive_scale_entry_positive_equalfirst))) + (((dst_negative_code_entry_positive_equalfirst) + (dst_negative_scale_entry_positive_equalfirst)) * S ((dst_negative_code_entry_positive_equalfirst) + (dst_negative_scale_entry_positive_equalfirst)) + ((dst_negative_scale_entry_positive_equalfirst) + (dst_negative_scale_entry_positive_equalfirst)))) + ((((dst_negative_code_entry_positive_equalfirst) + (dst_negative_scale_entry_positive_equalfirst)) * S ((dst_negative_code_entry_positive_equalfirst) + (dst_negative_scale_entry_positive_equalfirst)) + ((dst_negative_scale_entry_positive_equalfirst) + (dst_negative_scale_entry_positive_equalfirst))) + (((dst_negative_code_entry_positive_equalfirst) + (dst_negative_scale_entry_positive_equalfirst)) * S ((dst_negative_code_entry_positive_equalfirst) + (dst_negative_scale_entry_positive_equalfirst)) + ((dst_negative_scale_entry_positive_equalfirst) + (dst_negative_scale_entry_positive_equalfirst)))))) /\ (((((exists ff_h_pvs_entry_positive_equalfirstpositive. ff_h_pvs_entry_positive_equalfirstpositive + S (dst_positive_entry_positive_equalfirst) = S ((S (dm_index_entry_positive_equal)) * dst_positive_scale_entry_positive_equalfirst)) /\ exists ff_q_pvs_entry_positive_equalfirstpositive. dst_positive_code_entry_positive_equalfirst = ff_q_pvs_entry_positive_equalfirstpositive * S ((S (dm_index_entry_positive_equal)) * dst_positive_scale_entry_positive_equalfirst) + (dst_positive_entry_positive_equalfirst))) /\ (((((exists ff_h_pvs_entry_positive_equalfirstnegative. ff_h_pvs_entry_positive_equalfirstnegative + S (dst_negative_entry_positive_equalfirst) = S ((S (dm_index_entry_positive_equal)) * dst_negative_scale_entry_positive_equalfirst)) /\ exists ff_q_pvs_entry_positive_equalfirstnegative. dst_negative_code_entry_positive_equalfirst = ff_q_pvs_entry_positive_equalfirstnegative * S ((S (dm_index_entry_positive_equal)) * dst_negative_scale_entry_positive_equalfirst) + (dst_negative_entry_positive_equalfirst))) /\ (exists ge_balance_positive_entry_positive_equalfirstvalue ge_balance_negative_entry_positive_equalfirstvalue. (((((dm_first_value_entry_positive_equal) = 2 * (ge_balance_positive_entry_positive_equalfirstvalue) /\ (ge_balance_negative_entry_positive_equalfirstvalue) = 0) \/ exists ge_signed_half_entry_positive_equalfirstvaluedecode. (((dm_first_value_entry_positive_equal) = 2 * ge_signed_half_entry_positive_equalfirstvaluedecode + 1 /\ (ge_balance_positive_entry_positive_equalfirstvalue) = 0) /\ (ge_balance_negative_entry_positive_equalfirstvalue) = S ge_signed_half_entry_positive_equalfirstvaluedecode))) /\ ((dst_positive_entry_positive_equalfirst) + ge_balance_negative_entry_positive_equalfirstvalue = (dst_negative_entry_positive_equalfirst) + ge_balance_positive_entry_positive_equalfirstvalue))))))))) -> (exists dst_positive_code_entry_positive_equalsecond dst_positive_scale_entry_positive_equalsecond dst_negative_code_entry_positive_equalsecond dst_negative_scale_entry_positive_equalsecond dst_positive_entry_positive_equalsecond dst_negative_entry_positive_equalsecond. (((G) = (((((dst_positive_code_entry_positive_equalsecond) + (dst_positive_scale_entry_positive_equalsecond)) * S ((dst_positive_code_entry_positive_equalsecond) + (dst_positive_scale_entry_positive_equalsecond)) + ((dst_positive_scale_entry_positive_equalsecond) + (dst_positive_scale_entry_positive_equalsecond))) + (((dst_negative_code_entry_positive_equalsecond) + (dst_negative_scale_entry_positive_equalsecond)) * S ((dst_negative_code_entry_positive_equalsecond) + (dst_negative_scale_entry_positive_equalsecond)) + ((dst_negative_scale_entry_positive_equalsecond) + (dst_negative_scale_entry_positive_equalsecond)))) * S ((((dst_positive_code_entry_positive_equalsecond) + (dst_positive_scale_entry_positive_equalsecond)) * S ((dst_positive_code_entry_positive_equalsecond) + (dst_positive_scale_entry_positive_equalsecond)) + ((dst_positive_scale_entry_positive_equalsecond) + (dst_positive_scale_entry_positive_equalsecond))) + (((dst_negative_code_entry_positive_equalsecond) + (dst_negative_scale_entry_positive_equalsecond)) * S ((dst_negative_code_entry_positive_equalsecond) + (dst_negative_scale_entry_positive_equalsecond)) + ((dst_negative_scale_entry_positive_equalsecond) + (dst_negative_scale_entry_positive_equalsecond)))) + ((((dst_negative_code_entry_positive_equalsecond) + (dst_negative_scale_entry_positive_equalsecond)) * S ((dst_negative_code_entry_positive_equalsecond) + (dst_negative_scale_entry_positive_equalsecond)) + ((dst_negative_scale_entry_positive_equalsecond) + (dst_negative_scale_entry_positive_equalsecond))) + (((dst_negative_code_entry_positive_equalsecond) + (dst_negative_scale_entry_positive_equalsecond)) * S ((dst_negative_code_entry_positive_equalsecond) + (dst_negative_scale_entry_positive_equalsecond)) + ((dst_negative_scale_entry_positive_equalsecond) + (dst_negative_scale_entry_positive_equalsecond)))))) /\ (((((exists ff_h_pvs_entry_positive_equalsecondpositive. ff_h_pvs_entry_positive_equalsecondpositive + S (dst_positive_entry_positive_equalsecond) = S ((S (dm_index_entry_positive_equal)) * dst_positive_scale_entry_positive_equalsecond)) /\ exists ff_q_pvs_entry_positive_equalsecondpositive. dst_positive_code_entry_positive_equalsecond = ff_q_pvs_entry_positive_equalsecondpositive * S ((S (dm_index_entry_positive_equal)) * dst_positive_scale_entry_positive_equalsecond) + (dst_positive_entry_positive_equalsecond))) /\ (((((exists ff_h_pvs_entry_positive_equalsecondnegative. ff_h_pvs_entry_positive_equalsecondnegative + S (dst_negative_entry_positive_equalsecond) = S ((S (dm_index_entry_positive_equal)) * dst_negative_scale_entry_positive_equalsecond)) /\ exists ff_q_pvs_entry_positive_equalsecondnegative. dst_negative_code_entry_positive_equalsecond = ff_q_pvs_entry_positive_equalsecondnegative * S ((S (dm_index_entry_positive_equal)) * dst_negative_scale_entry_positive_equalsecond) + (dst_negative_entry_positive_equalsecond))) /\ (exists ge_balance_positive_entry_positive_equalsecondvalue ge_balance_negative_entry_positive_equalsecondvalue. (((((dm_second_value_entry_positive_equal) = 2 * (ge_balance_positive_entry_positive_equalsecondvalue) /\ (ge_balance_negative_entry_positive_equalsecondvalue) = 0) \/ exists ge_signed_half_entry_positive_equalsecondvaluedecode. (((dm_second_value_entry_positive_equal) = 2 * ge_signed_half_entry_positive_equalsecondvaluedecode + 1 /\ (ge_balance_positive_entry_positive_equalsecondvalue) = 0) /\ (ge_balance_negative_entry_positive_equalsecondvalue) = S ge_signed_half_entry_positive_equalsecondvaluedecode))) /\ ((dst_positive_entry_positive_equalsecond) + ge_balance_negative_entry_positive_equalsecondvalue = (dst_negative_entry_positive_equalsecond) + ge_balance_positive_entry_positive_equalsecondvalue))))))))) -> dm_first_value_entry_positive_equal=dm_second_value_entry_positive_equal) -> ~(i=0) -> (exists pvs_le_gap_entry_bound. pvs_le_gap_entry_bound + (i) = (N)) -> (exists dst_positive_code_entry_source dst_positive_scale_entry_source dst_negative_code_entry_source dst_negative_scale_entry_source dst_positive_entry_source dst_negative_entry_source. (((F) = (((((dst_positive_code_entry_source) + (dst_positive_scale_entry_source)) * S ((dst_positive_code_entry_source) + (dst_positive_scale_entry_source)) + ((dst_positive_scale_entry_source) + (dst_positive_scale_entry_source))) + (((dst_negative_code_entry_source) + (dst_negative_scale_entry_source)) * S ((dst_negative_code_entry_source) + (dst_negative_scale_entry_source)) + ((dst_negative_scale_entry_source) + (dst_negative_scale_entry_source)))) * S ((((dst_positive_code_entry_source) + (dst_positive_scale_entry_source)) * S ((dst_positive_code_entry_source) + (dst_positive_scale_entry_source)) + ((dst_positive_scale_entry_source) + (dst_positive_scale_entry_source))) + (((dst_negative_code_entry_source) + (dst_negative_scale_entry_source)) * S ((dst_negative_code_entry_source) + (dst_negative_scale_entry_source)) + ((dst_negative_scale_entry_source) + (dst_negative_scale_entry_source)))) + ((((dst_negative_code_entry_source) + (dst_negative_scale_entry_source)) * S ((dst_negative_code_entry_source) + (dst_negative_scale_entry_source)) + ((dst_negative_scale_entry_source) + (dst_negative_scale_entry_source))) + (((dst_negative_code_entry_source) + (dst_negative_scale_entry_source)) * S ((dst_negative_code_entry_source) + (dst_negative_scale_entry_source)) + ((dst_negative_scale_entry_source) + (dst_negative_scale_entry_source)))))) /\ (((((exists ff_h_pvs_entry_sourcepositive. ff_h_pvs_entry_sourcepositive + S (dst_positive_entry_source) = S ((S (i)) * dst_positive_scale_entry_source)) /\ exists ff_q_pvs_entry_sourcepositive. dst_positive_code_entry_source = ff_q_pvs_entry_sourcepositive * S ((S (i)) * dst_positive_scale_entry_source) + (dst_positive_entry_source))) /\ (((((exists ff_h_pvs_entry_sourcenegative. ff_h_pvs_entry_sourcenegative + S (dst_negative_entry_source) = S ((S (i)) * dst_negative_scale_entry_source)) /\ exists ff_q_pvs_entry_sourcenegative. dst_negative_code_entry_source = ff_q_pvs_entry_sourcenegative * S ((S (i)) * dst_negative_scale_entry_source) + (dst_negative_entry_source))) /\ (exists ge_balance_positive_entry_sourcevalue ge_balance_negative_entry_sourcevalue. (((((z) = 2 * (ge_balance_positive_entry_sourcevalue) /\ (ge_balance_negative_entry_sourcevalue) = 0) \/ exists ge_signed_half_entry_sourcevaluedecode. (((z) = 2 * ge_signed_half_entry_sourcevaluedecode + 1 /\ (ge_balance_positive_entry_sourcevalue) = 0) /\ (ge_balance_negative_entry_sourcevalue) = S ge_signed_half_entry_sourcevaluedecode))) /\ ((dst_positive_entry_source) + ge_balance_negative_entry_sourcevalue = (dst_negative_entry_source) + ge_balance_positive_entry_sourcevalue))))))))) -> (exists dst_positive_code_entry_target dst_positive_scale_entry_target dst_negative_code_entry_target dst_negative_scale_entry_target dst_positive_entry_target dst_negative_entry_target. (((G) = (((((dst_positive_code_entry_target) + (dst_positive_scale_entry_target)) * S ((dst_positive_code_entry_target) + (dst_positive_scale_entry_target)) + ((dst_positive_scale_entry_target) + (dst_positive_scale_entry_target))) + (((dst_negative_code_entry_target) + (dst_negative_scale_entry_target)) * S ((dst_negative_code_entry_target) + (dst_negative_scale_entry_target)) + ((dst_negative_scale_entry_target) + (dst_negative_scale_entry_target)))) * S ((((dst_positive_code_entry_target) + (dst_positive_scale_entry_target)) * S ((dst_positive_code_entry_target) + (dst_positive_scale_entry_target)) + ((dst_positive_scale_entry_target) + (dst_positive_scale_entry_target))) + (((dst_negative_code_entry_target) + (dst_negative_scale_entry_target)) * S ((dst_negative_code_entry_target) + (dst_negative_scale_entry_target)) + ((dst_negative_scale_entry_target) + (dst_negative_scale_entry_target)))) + ((((dst_negative_code_entry_target) + (dst_negative_scale_entry_target)) * S ((dst_negative_code_entry_target) + (dst_negative_scale_entry_target)) + ((dst_negative_scale_entry_target) + (dst_negative_scale_entry_target))) + (((dst_negative_code_entry_target) + (dst_negative_scale_entry_target)) * S ((dst_negative_code_entry_target) + (dst_negative_scale_entry_target)) + ((dst_negative_scale_entry_target) + (dst_negative_scale_entry_target)))))) /\ (((((exists ff_h_pvs_entry_targetpositive. ff_h_pvs_entry_targetpositive + S (dst_positive_entry_target) = S ((S (i)) * dst_positive_scale_entry_target)) /\ exists ff_q_pvs_entry_targetpositive. dst_positive_code_entry_target = ff_q_pvs_entry_targetpositive * S ((S (i)) * dst_positive_scale_entry_target) + (dst_positive_entry_target))) /\ (((((exists ff_h_pvs_entry_targetnegative. ff_h_pvs_entry_targetnegative + S (dst_negative_entry_target) = S ((S (i)) * dst_negative_scale_entry_target)) /\ exists ff_q_pvs_entry_targetnegative. dst_negative_code_entry_target = ff_q_pvs_entry_targetnegative * S ((S (i)) * dst_negative_scale_entry_target) + (dst_negative_entry_target))) /\ (exists ge_balance_positive_entry_targetvalue ge_balance_negative_entry_targetvalue. (((((z) = 2 * (ge_balance_positive_entry_targetvalue) /\ (ge_balance_negative_entry_targetvalue) = 0) \/ exists ge_signed_half_entry_targetvaluedecode. (((z) = 2 * ge_signed_half_entry_targetvaluedecode + 1 /\ (ge_balance_positive_entry_targetvalue) = 0) /\ (ge_balance_negative_entry_targetvalue) = S ge_signed_half_entry_targetvaluedecode))) /\ ((dst_positive_entry_target) + ge_balance_negative_entry_targetvalue = (dst_negative_entry_target) + ge_balance_positive_entry_targetvalue)))))))))

Constructive proof overview

Generated structural guide

Transport a real positive lookup across prefix equality by first constructing the target lookup; no encoding or zero-value equality is required.

The unchanged tactic script uses 1 declared prerequisite and contains 29 exact native proof lines.

Alpha v34 checked-use · first admitted v32 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

signed_table_lookup_any Alpha theorem; checked-use authorized

Direct dependents

MX000B signed_multiplicative_positive_extensional

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

29 script commands · 6 reading checkpoints · 2 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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro G
  4. L4
    intro i
  5. L5
    intro z
  6. L6
    intro hG
  7. L7
    intro he
  8. L8
    intro hi
  9. L9
    intro hb
  10. L10
    intro hz
02Establish hvL11–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed table lookup any.

  1. L11
    have hv : ∃ v. ArithAt(G,i,v)Definitions: ArithAt
  2. L12
    specialize signed_table_lookup_any (N)
  3. L13
    specialize signed_table_lookup_any (G)
  4. L14
    specialize signed_table_lookup_any (i)
  5. L15
    apply signed_table_lookup_any
  6. L16
    exact hG
03Separate the logical casesL17–17

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

  1. L17
    cases hv
04Establish heqL18–27

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

  1. L18
    have heq : z=x
  2. L19
    specialize he (i)
  3. L20
    specialize he (z)
  4. L21
    specialize he (x)
  5. L22
    apply he
  6. L23
    exact hi
  7. L24
    exact hb
  8. L25
    exact hz
  9. L26
    exact hv_witness
  10. L27
    rewrite heq
05Calculate and transport equalitiesL28–28

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

  1. L28
    rewrite heq
06Use earlier factsL29–29

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

  1. L29
    exact hv_witness

Library-wide reading audit

Original exact command ledger · 29 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro G
  4. 0004intro i
  5. 0005intro z
  6. 0006intro hG
  7. 0007intro he
  8. 0008intro hi
  9. 0009intro hb
  10. 0010intro hz
  11. 0011have hv : exists v. (exists dst_positive_code_positive_entry_actual dst_positive_scale_positive_entry_actual dst_negative_code_positive_entry_actual dst_negative_scale_positive_entry_actual dst_positive_positive_entry_actual dst_negative_positive_entry_actual. (((G) = (((((dst_positive_code_positive_entry_actual) + (dst_positive_scale_positive_entry_actual)) * S ((dst_positive_code_positive_entry_actual) + (dst_positive_scale_positive_entry_actual)) + ((dst_positive_scale_positive_entry_actual) + (dst_positive_scale_positive_entry_actual))) + (((dst_negative_code_positive_entry_actual) + (dst_negative_scale_positive_entry_actual)) * S ((dst_negative_code_positive_entry_actual) + (dst_negative_scale_positive_entry_actual)) + ((dst_negative_scale_positive_entry_actual) + (dst_negative_scale_positive_entry_actual)))) * S ((((dst_positive_code_positive_entry_actual) + (dst_positive_scale_positive_entry_actual)) * S ((dst_positive_code_positive_entry_actual) + (dst_positive_scale_positive_entry_actual)) + ((dst_positive_scale_positive_entry_actual) + (dst_positive_scale_positive_entry_actual))) + (((dst_negative_code_positive_entry_actual) + (dst_negative_scale_positive_entry_actual)) * S ((dst_negative_code_positive_entry_actual) + (dst_negative_scale_positive_entry_actual)) + ((dst_negative_scale_positive_entry_actual) + (dst_negative_scale_positive_entry_actual)))) + ((((dst_negative_code_positive_entry_actual) + (dst_negative_scale_positive_entry_actual)) * S ((dst_negative_code_positive_entry_actual) + (dst_negative_scale_positive_entry_actual)) + ((dst_negative_scale_positive_entry_actual) + (dst_negative_scale_positive_entry_actual))) + (((dst_negative_code_positive_entry_actual) + (dst_negative_scale_positive_entry_actual)) * S ((dst_negative_code_positive_entry_actual) + (dst_negative_scale_positive_entry_actual)) + ((dst_negative_scale_positive_entry_actual) + (dst_negative_scale_positive_entry_actual)))))) /\ (((((exists ff_h_pvs_positive_entry_actualpositive. ff_h_pvs_positive_entry_actualpositive + S (dst_positive_positive_entry_actual) = S ((S (i)) * dst_positive_scale_positive_entry_actual)) /\ exists ff_q_pvs_positive_entry_actualpositive. dst_positive_code_positive_entry_actual = ff_q_pvs_positive_entry_actualpositive * S ((S (i)) * dst_positive_scale_positive_entry_actual) + (dst_positive_positive_entry_actual))) /\ (((((exists ff_h_pvs_positive_entry_actualnegative. ff_h_pvs_positive_entry_actualnegative + S (dst_negative_positive_entry_actual) = S ((S (i)) * dst_negative_scale_positive_entry_actual)) /\ exists ff_q_pvs_positive_entry_actualnegative. dst_negative_code_positive_entry_actual = ff_q_pvs_positive_entry_actualnegative * S ((S (i)) * dst_negative_scale_positive_entry_actual) + (dst_negative_positive_entry_actual))) /\ (exists ge_balance_positive_positive_entry_actualvalue ge_balance_negative_positive_entry_actualvalue. (((((v) = 2 * (ge_balance_positive_positive_entry_actualvalue) /\ (ge_balance_negative_positive_entry_actualvalue) = 0) \/ exists ge_signed_half_positive_entry_actualvaluedecode. (((v) = 2 * ge_signed_half_positive_entry_actualvaluedecode + 1 /\ (ge_balance_positive_positive_entry_actualvalue) = 0) /\ (ge_balance_negative_positive_entry_actualvalue) = S ge_signed_half_positive_entry_actualvaluedecode))) /\ ((dst_positive_positive_entry_actual) + ge_balance_negative_positive_entry_actualvalue = (dst_negative_positive_entry_actual) + ge_balance_positive_positive_entry_actualvalue)))))))))
  12. 0012specialize signed_table_lookup_any (N)
  13. 0013specialize signed_table_lookup_any (G)
  14. 0014specialize signed_table_lookup_any (i)
  15. 0015apply signed_table_lookup_any
  16. 0016exact hG
  17. 0017cases hv
  18. 0018have heq : z=x
  19. 0019specialize he (i)
  20. 0020specialize he (z)
  21. 0021specialize he (x)
  22. 0022apply he
  23. 0023exact hi
  24. 0024exact hb
  25. 0025exact hz
  26. 0026exact hv_witness
  27. 0027rewrite heq
  28. 0028rewrite heq
  29. 0029exact hv_witness