MX0041

signed_support_incidence_flat_prefix_exists

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

Ordinary induction constructs the entire inclusive prefix by real beta-stream extension, with no choice or sum oracle.

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 A r s M l. (exists dst_positive_code_prefix_exists_source dst_positive_scale_prefix_exists_source dst_negative_code_prefix_exists_source dst_negative_scale_prefix_exists_source. (((A) = (((((dst_positive_code_prefix_exists_source) + (dst_positive_scale_prefix_exists_source)) * S ((dst_positive_code_prefix_exists_source) + (dst_positive_scale_prefix_exists_source)) + ((dst_positive_scale_prefix_exists_source) + (dst_positive_scale_prefix_exists_source))) + (((dst_negative_code_prefix_exists_source) + (dst_negative_scale_prefix_exists_source)) * S ((dst_negative_code_prefix_exists_source) + (dst_negative_scale_prefix_exists_source)) + ((dst_negative_scale_prefix_exists_source) + (dst_negative_scale_prefix_exists_source)))) * S ((((dst_positive_code_prefix_exists_source) + (dst_positive_scale_prefix_exists_source)) * S ((dst_positive_code_prefix_exists_source) + (dst_positive_scale_prefix_exists_source)) + ((dst_positive_scale_prefix_exists_source) + (dst_positive_scale_prefix_exists_source))) + (((dst_negative_code_prefix_exists_source) + (dst_negative_scale_prefix_exists_source)) * S ((dst_negative_code_prefix_exists_source) + (dst_negative_scale_prefix_exists_source)) + ((dst_negative_scale_prefix_exists_source) + (dst_negative_scale_prefix_exists_source)))) + ((((dst_negative_code_prefix_exists_source) + (dst_negative_scale_prefix_exists_source)) * S ((dst_negative_code_prefix_exists_source) + (dst_negative_scale_prefix_exists_source)) + ((dst_negative_scale_prefix_exists_source) + (dst_negative_scale_prefix_exists_source))) + (((dst_negative_code_prefix_exists_source) + (dst_negative_scale_prefix_exists_source)) * S ((dst_negative_code_prefix_exists_source) + (dst_negative_scale_prefix_exists_source)) + ((dst_negative_scale_prefix_exists_source) + (dst_negative_scale_prefix_exists_source)))))) /\ (forall dst_index_prefix_exists_source. (exists pvs_le_gap_prefix_exists_sourcedomain. pvs_le_gap_prefix_exists_sourcedomain + (dst_index_prefix_exists_source) = (0)) -> exists dst_positive_prefix_exists_source dst_negative_prefix_exists_source dst_value_prefix_exists_source. ((((exists ff_h_pvs_prefix_exists_sourceentrypositive. ff_h_pvs_prefix_exists_sourceentrypositive + S (dst_positive_prefix_exists_source) = S ((S (dst_index_prefix_exists_source)) * dst_positive_scale_prefix_exists_source)) /\ exists ff_q_pvs_prefix_exists_sourceentrypositive. dst_positive_code_prefix_exists_source = ff_q_pvs_prefix_exists_sourceentrypositive * S ((S (dst_index_prefix_exists_source)) * dst_positive_scale_prefix_exists_source) + (dst_positive_prefix_exists_source))) /\ (((((exists ff_h_pvs_prefix_exists_sourceentrynegative. ff_h_pvs_prefix_exists_sourceentrynegative + S (dst_negative_prefix_exists_source) = S ((S (dst_index_prefix_exists_source)) * dst_negative_scale_prefix_exists_source)) /\ exists ff_q_pvs_prefix_exists_sourceentrynegative. dst_negative_code_prefix_exists_source = ff_q_pvs_prefix_exists_sourceentrynegative * S ((S (dst_index_prefix_exists_source)) * dst_negative_scale_prefix_exists_source) + (dst_negative_prefix_exists_source))) /\ (exists ge_balance_positive_prefix_exists_sourceentryvalue ge_balance_negative_prefix_exists_sourceentryvalue. (((((dst_value_prefix_exists_source) = 2 * (ge_balance_positive_prefix_exists_sourceentryvalue) /\ (ge_balance_negative_prefix_exists_sourceentryvalue) = 0) \/ exists ge_signed_half_prefix_exists_sourceentryvaluedecode. (((dst_value_prefix_exists_source) = 2 * ge_signed_half_prefix_exists_sourceentryvaluedecode + 1 /\ (ge_balance_positive_prefix_exists_sourceentryvalue) = 0) /\ (ge_balance_negative_prefix_exists_sourceentryvalue) = S ge_signed_half_prefix_exists_sourceentryvaluedecode))) /\ ((dst_positive_prefix_exists_source) + ge_balance_negative_prefix_exists_sourceentryvalue = (dst_negative_prefix_exists_source) + ge_balance_positive_prefix_exists_sourceentryvalue))))))))) -> exists T. (((exists dst_positive_code_prefix_exists_resulttable dst_positive_scale_prefix_exists_resulttable dst_negative_code_prefix_exists_resulttable dst_negative_scale_prefix_exists_resulttable. (((T) = (((((dst_positive_code_prefix_exists_resulttable) + (dst_positive_scale_prefix_exists_resulttable)) * S ((dst_positive_code_prefix_exists_resulttable) + (dst_positive_scale_prefix_exists_resulttable)) + ((dst_positive_scale_prefix_exists_resulttable) + (dst_positive_scale_prefix_exists_resulttable))) + (((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) * S ((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) + ((dst_negative_scale_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)))) * S ((((dst_positive_code_prefix_exists_resulttable) + (dst_positive_scale_prefix_exists_resulttable)) * S ((dst_positive_code_prefix_exists_resulttable) + (dst_positive_scale_prefix_exists_resulttable)) + ((dst_positive_scale_prefix_exists_resulttable) + (dst_positive_scale_prefix_exists_resulttable))) + (((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) * S ((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) + ((dst_negative_scale_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)))) + ((((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) * S ((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) + ((dst_negative_scale_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable))) + (((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) * S ((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) + ((dst_negative_scale_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)))))) /\ (forall dst_index_prefix_exists_resulttable. (exists pvs_le_gap_prefix_exists_resulttabledomain. pvs_le_gap_prefix_exists_resulttabledomain + (dst_index_prefix_exists_resulttable) = (l)) -> exists dst_positive_prefix_exists_resulttable dst_negative_prefix_exists_resulttable dst_value_prefix_exists_resulttable. ((((exists ff_h_pvs_prefix_exists_resulttableentrypositive. ff_h_pvs_prefix_exists_resulttableentrypositive + S (dst_positive_prefix_exists_resulttable) = S ((S (dst_index_prefix_exists_resulttable)) * dst_positive_scale_prefix_exists_resulttable)) /\ exists ff_q_pvs_prefix_exists_resulttableentrypositive. dst_positive_code_prefix_exists_resulttable = ff_q_pvs_prefix_exists_resulttableentrypositive * S ((S (dst_index_prefix_exists_resulttable)) * dst_positive_scale_prefix_exists_resulttable) + (dst_positive_prefix_exists_resulttable))) /\ (((((exists ff_h_pvs_prefix_exists_resulttableentrynegative. ff_h_pvs_prefix_exists_resulttableentrynegative + S (dst_negative_prefix_exists_resulttable) = S ((S (dst_index_prefix_exists_resulttable)) * dst_negative_scale_prefix_exists_resulttable)) /\ exists ff_q_pvs_prefix_exists_resulttableentrynegative. dst_negative_code_prefix_exists_resulttable = ff_q_pvs_prefix_exists_resulttableentrynegative * S ((S (dst_index_prefix_exists_resulttable)) * dst_negative_scale_prefix_exists_resulttable) + (dst_negative_prefix_exists_resulttable))) /\ (exists ge_balance_positive_prefix_exists_resulttableentryvalue ge_balance_negative_prefix_exists_resulttableentryvalue. (((((dst_value_prefix_exists_resulttable) = 2 * (ge_balance_positive_prefix_exists_resulttableentryvalue) /\ (ge_balance_negative_prefix_exists_resulttableentryvalue) = 0) \/ exists ge_signed_half_prefix_exists_resulttableentryvaluedecode. (((dst_value_prefix_exists_resulttable) = 2 * ge_signed_half_prefix_exists_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_exists_resulttableentryvalue) = 0) /\ (ge_balance_negative_prefix_exists_resulttableentryvalue) = S ge_signed_half_prefix_exists_resulttableentryvaluedecode))) /\ ((dst_positive_prefix_exists_resulttable) + ge_balance_negative_prefix_exists_resulttableentryvalue = (dst_negative_prefix_exists_resulttable) + ge_balance_positive_prefix_exists_resulttableentryvalue))))))))) /\ (forall ssr_prefix_index_prefix_exists_result ssr_prefix_value_prefix_exists_result. (exists pvs_le_gap_prefix_exists_resultbound. pvs_le_gap_prefix_exists_resultbound + (ssr_prefix_index_prefix_exists_result) = (l)) -> (exists dst_positive_code_prefix_exists_resultlookup dst_positive_scale_prefix_exists_resultlookup dst_negative_code_prefix_exists_resultlookup dst_negative_scale_prefix_exists_resultlookup dst_positive_prefix_exists_resultlookup dst_negative_prefix_exists_resultlookup. (((T) = (((((dst_positive_code_prefix_exists_resultlookup) + (dst_positive_scale_prefix_exists_resultlookup)) * S ((dst_positive_code_prefix_exists_resultlookup) + (dst_positive_scale_prefix_exists_resultlookup)) + ((dst_positive_scale_prefix_exists_resultlookup) + (dst_positive_scale_prefix_exists_resultlookup))) + (((dst_negative_code_prefix_exists_resultlookup) + (dst_negative_scale_prefix_exists_resultlookup)) * S ((dst_negative_code_prefix_exists_resultlookup) + (dst_negative_scale_prefix_exists_resultlookup)) + ((dst_negative_scale_prefix_exists_resultlookup) + (dst_negative_scale_prefix_exists_resultlookup)))) * S ((((dst_positive_code_prefix_exists_resultlookup) + (dst_positive_scale_prefix_exists_resultlookup)) * S ((dst_positive_code_prefix_exists_resultlookup) + (dst_positive_scale_prefix_exists_resultlookup)) + ((dst_positive_scale_prefix_exists_resultlookup) + (dst_positive_scale_prefix_exists_resultlookup))) + (((dst_negative_code_prefix_exists_resultlookup) + (dst_negative_scale_prefix_exists_resultlookup)) * S ((dst_negative_code_prefix_exists_resultlookup) + (dst_negative_scale_prefix_exists_resultlookup)) + ((dst_negative_scale_prefix_exists_resultlookup) + (dst_negative_scale_prefix_exists_resultlookup)))) + ((((dst_negative_code_prefix_exists_resultlookup) + (dst_negative_scale_prefix_exists_resultlookup)) * S ((dst_negative_code_prefix_exists_resultlookup) + (dst_negative_scale_prefix_exists_resultlookup)) + ((dst_negative_scale_prefix_exists_resultlookup) + (dst_negative_scale_prefix_exists_resultlookup))) + (((dst_negative_code_prefix_exists_resultlookup) + (dst_negative_scale_prefix_exists_resultlookup)) * S ((dst_negative_code_prefix_exists_resultlookup) + (dst_negative_scale_prefix_exists_resultlookup)) + ((dst_negative_scale_prefix_exists_resultlookup) + (dst_negative_scale_prefix_exists_resultlookup)))))) /\ (((((exists ff_h_pvs_prefix_exists_resultlookuppositive. ff_h_pvs_prefix_exists_resultlookuppositive + S (dst_positive_prefix_exists_resultlookup) = S ((S (ssr_prefix_index_prefix_exists_result)) * dst_positive_scale_prefix_exists_resultlookup)) /\ exists ff_q_pvs_prefix_exists_resultlookuppositive. dst_positive_code_prefix_exists_resultlookup = ff_q_pvs_prefix_exists_resultlookuppositive * S ((S (ssr_prefix_index_prefix_exists_result)) * dst_positive_scale_prefix_exists_resultlookup) + (dst_positive_prefix_exists_resultlookup))) /\ (((((exists ff_h_pvs_prefix_exists_resultlookupnegative. ff_h_pvs_prefix_exists_resultlookupnegative + S (dst_negative_prefix_exists_resultlookup) = S ((S (ssr_prefix_index_prefix_exists_result)) * dst_negative_scale_prefix_exists_resultlookup)) /\ exists ff_q_pvs_prefix_exists_resultlookupnegative. dst_negative_code_prefix_exists_resultlookup = ff_q_pvs_prefix_exists_resultlookupnegative * S ((S (ssr_prefix_index_prefix_exists_result)) * dst_negative_scale_prefix_exists_resultlookup) + (dst_negative_prefix_exists_resultlookup))) /\ (exists ge_balance_positive_prefix_exists_resultlookupvalue ge_balance_negative_prefix_exists_resultlookupvalue. (((((ssr_prefix_value_prefix_exists_result) = 2 * (ge_balance_positive_prefix_exists_resultlookupvalue) /\ (ge_balance_negative_prefix_exists_resultlookupvalue) = 0) \/ exists ge_signed_half_prefix_exists_resultlookupvaluedecode. (((ssr_prefix_value_prefix_exists_result) = 2 * ge_signed_half_prefix_exists_resultlookupvaluedecode + 1 /\ (ge_balance_positive_prefix_exists_resultlookupvalue) = 0) /\ (ge_balance_negative_prefix_exists_resultlookupvalue) = S ge_signed_half_prefix_exists_resultlookupvaluedecode))) /\ ((dst_positive_prefix_exists_resultlookup) + ge_balance_negative_prefix_exists_resultlookupvalue = (dst_negative_prefix_exists_resultlookup) + ge_balance_positive_prefix_exists_resultlookupvalue))))))))) -> (exists ssr_flat_row_prefix_exists_resultentry ssr_flat_column_prefix_exists_resultentry. (((ssr_prefix_index_prefix_exists_result)=(((S (M))*(ssr_flat_row_prefix_exists_resultentry)+(ssr_flat_column_prefix_exists_resultentry)))) /\ (((exists pvs_gap_prefix_exists_resultentryremainder. pvs_gap_prefix_exists_resultentryremainder + S (ssr_flat_column_prefix_exists_resultentry) = (S (M))) /\ (exists ssr_entry_value_prefix_exists_resultentryentry ssr_entry_image_prefix_exists_resultentryentry. ((exists dst_positive_code_prefix_exists_resultentryentrysource dst_positive_scale_prefix_exists_resultentryentrysource dst_negative_code_prefix_exists_resultentryentrysource dst_negative_scale_prefix_exists_resultentryentrysource dst_positive_prefix_exists_resultentryentrysource dst_negative_prefix_exists_resultentryentrysource. (((A) = (((((dst_positive_code_prefix_exists_resultentryentrysource) + (dst_positive_scale_prefix_exists_resultentryentrysource)) * S ((dst_positive_code_prefix_exists_resultentryentrysource) + (dst_positive_scale_prefix_exists_resultentryentrysource)) + ((dst_positive_scale_prefix_exists_resultentryentrysource) + (dst_positive_scale_prefix_exists_resultentryentrysource))) + (((dst_negative_code_prefix_exists_resultentryentrysource) + (dst_negative_scale_prefix_exists_resultentryentrysource)) * S ((dst_negative_code_prefix_exists_resultentryentrysource) + (dst_negative_scale_prefix_exists_resultentryentrysource)) + ((dst_negative_scale_prefix_exists_resultentryentrysource) + (dst_negative_scale_prefix_exists_resultentryentrysource)))) * S ((((dst_positive_code_prefix_exists_resultentryentrysource) + (dst_positive_scale_prefix_exists_resultentryentrysource)) * S ((dst_positive_code_prefix_exists_resultentryentrysource) + (dst_positive_scale_prefix_exists_resultentryentrysource)) + ((dst_positive_scale_prefix_exists_resultentryentrysource) + (dst_positive_scale_prefix_exists_resultentryentrysource))) + (((dst_negative_code_prefix_exists_resultentryentrysource) + (dst_negative_scale_prefix_exists_resultentryentrysource)) * S ((dst_negative_code_prefix_exists_resultentryentrysource) + (dst_negative_scale_prefix_exists_resultentryentrysource)) + ((dst_negative_scale_prefix_exists_resultentryentrysource) + (dst_negative_scale_prefix_exists_resultentryentrysource)))) + ((((dst_negative_code_prefix_exists_resultentryentrysource) + (dst_negative_scale_prefix_exists_resultentryentrysource)) * S ((dst_negative_code_prefix_exists_resultentryentrysource) + (dst_negative_scale_prefix_exists_resultentryentrysource)) + ((dst_negative_scale_prefix_exists_resultentryentrysource) + (dst_negative_scale_prefix_exists_resultentryentrysource))) + (((dst_negative_code_prefix_exists_resultentryentrysource) + (dst_negative_scale_prefix_exists_resultentryentrysource)) * S ((dst_negative_code_prefix_exists_resultentryentrysource) + (dst_negative_scale_prefix_exists_resultentryentrysource)) + ((dst_negative_scale_prefix_exists_resultentryentrysource) + (dst_negative_scale_prefix_exists_resultentryentrysource)))))) /\ (((((exists ff_h_pvs_prefix_exists_resultentryentrysourcepositive. ff_h_pvs_prefix_exists_resultentryentrysourcepositive + S (dst_positive_prefix_exists_resultentryentrysource) = S ((S (ssr_flat_row_prefix_exists_resultentry)) * dst_positive_scale_prefix_exists_resultentryentrysource)) /\ exists ff_q_pvs_prefix_exists_resultentryentrysourcepositive. dst_positive_code_prefix_exists_resultentryentrysource = ff_q_pvs_prefix_exists_resultentryentrysourcepositive * S ((S (ssr_flat_row_prefix_exists_resultentry)) * dst_positive_scale_prefix_exists_resultentryentrysource) + (dst_positive_prefix_exists_resultentryentrysource))) /\ (((((exists ff_h_pvs_prefix_exists_resultentryentrysourcenegative. ff_h_pvs_prefix_exists_resultentryentrysourcenegative + S (dst_negative_prefix_exists_resultentryentrysource) = S ((S (ssr_flat_row_prefix_exists_resultentry)) * dst_negative_scale_prefix_exists_resultentryentrysource)) /\ exists ff_q_pvs_prefix_exists_resultentryentrysourcenegative. dst_negative_code_prefix_exists_resultentryentrysource = ff_q_pvs_prefix_exists_resultentryentrysourcenegative * S ((S (ssr_flat_row_prefix_exists_resultentry)) * dst_negative_scale_prefix_exists_resultentryentrysource) + (dst_negative_prefix_exists_resultentryentrysource))) /\ (exists ge_balance_positive_prefix_exists_resultentryentrysourcevalue ge_balance_negative_prefix_exists_resultentryentrysourcevalue. (((((ssr_entry_value_prefix_exists_resultentryentry) = 2 * (ge_balance_positive_prefix_exists_resultentryentrysourcevalue) /\ (ge_balance_negative_prefix_exists_resultentryentrysourcevalue) = 0) \/ exists ge_signed_half_prefix_exists_resultentryentrysourcevaluedecode. (((ssr_entry_value_prefix_exists_resultentryentry) = 2 * ge_signed_half_prefix_exists_resultentryentrysourcevaluedecode + 1 /\ (ge_balance_positive_prefix_exists_resultentryentrysourcevalue) = 0) /\ (ge_balance_negative_prefix_exists_resultentryentrysourcevalue) = S ge_signed_half_prefix_exists_resultentryentrysourcevaluedecode))) /\ ((dst_positive_prefix_exists_resultentryentrysource) + ge_balance_negative_prefix_exists_resultentryentrysourcevalue = (dst_negative_prefix_exists_resultentryentrysource) + ge_balance_positive_prefix_exists_resultentryentrysourcevalue))))))))) /\ (((((exists ff_h_pvs_prefix_exists_resultentryentrymap. ff_h_pvs_prefix_exists_resultentryentrymap + S (ssr_entry_image_prefix_exists_resultentryentry) = S ((S (ssr_flat_row_prefix_exists_resultentry)) * s)) /\ exists ff_q_pvs_prefix_exists_resultentryentrymap. r = ff_q_pvs_prefix_exists_resultentryentrymap * S ((S (ssr_flat_row_prefix_exists_resultentry)) * s) + (ssr_entry_image_prefix_exists_resultentryentry))) /\ (((((ssr_flat_column_prefix_exists_resultentry)=(ssr_entry_image_prefix_exists_resultentryentry)) /\ ((ssr_prefix_value_prefix_exists_result)=(ssr_entry_value_prefix_exists_resultentryentry)))) \/ (((~((ssr_flat_column_prefix_exists_resultentry)=(ssr_entry_image_prefix_exists_resultentryentry))) /\ ((ssr_prefix_value_prefix_exists_result)=0)))))))))))))))

Constructive proof overview

Generated structural guide

Ordinary induction constructs the entire inclusive prefix by real beta-stream extension, with no choice or sum oracle.

The unchanged tactic script uses 4 declared prerequisites and contains 61 exact native proof lines.

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

Proof neighborhood

Direct dependencies

MX003D signed_support_incidence_flat_entry_exists arithmetic_signed_table_singleton Alpha theorem; checked-use authorized MX003F signed_support_incidence_flat_prefix_zero MX0040 signed_support_incidence_flat_prefix_append

Direct dependents

MX0043 signed_support_incidence_exists

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

61 script commands · 18 reading checkpoints · 5 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.

Named ingredients (3)
signed support incidence flat entry existssigned support incidence flat prefix zerosigned support incidence flat prefix append

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–5

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

  1. L1
    intro A
  2. L2
    intro r
  3. L3
    intro s
  4. L4
    intro M
  5. L5
    intro l
02Induction on lL6–7

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

  1. L6
    induction l
  2. L7
    intro hA
03Establish hvL8–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed support incidence flat entry exists.

  1. L8
    have hv : ∃ z. SignedIncidenceFlatEntry(A,r,s,M,0,z)Definitions: SignedIncidenceFlatEntry
  2. L9
    specialize signed_support_incidence_flat_entry_exists (A)
  3. L10
    specialize signed_support_incidence_flat_entry_exists (r)
  4. L11
    specialize signed_support_incidence_flat_entry_exists (s)
  5. L12
    specialize signed_support_incidence_flat_entry_exists (M)
  6. L13
    specialize signed_support_incidence_flat_entry_exists (0)
  7. L14
    apply signed_support_incidence_flat_entry_exists
  8. L15
    exact hA
04Separate the logical casesL16–16

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

  1. L16
    cases hv
05Establish htL17–19

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

  1. L17
    have ht : ∃ T. ArithTable(0,T) ∧ ArithAt(T,0,x)Definitions: ArithTableArithAt
  2. L18
    specialize arithmetic_signed_table_singleton (x)
  3. L19
    apply arithmetic_signed_table_singleton
06Separate the logical casesL20–21

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

  1. L20
    cases ht
  2. L21
    cases ht_witness
07Construct an explicit witnessL22–22

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

  1. L22
    exists x1
08Use earlier factsL23–32

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

  1. L23
    specialize signed_support_incidence_flat_prefix_zero (A)
  2. L24
    specialize signed_support_incidence_flat_prefix_zero (r)
  3. L25
    specialize signed_support_incidence_flat_prefix_zero (s)
  4. L26
    specialize signed_support_incidence_flat_prefix_zero (M)
  5. L27
    specialize signed_support_incidence_flat_prefix_zero (x1)
  6. L28
    specialize signed_support_incidence_flat_prefix_zero (x)
  7. L29
    apply signed_support_incidence_flat_prefix_zero
  8. L30
    exact ht_witness_left
  9. L31
    exact ht_witness_right
  10. L32
    exact hv_witness
09Fix variables and assumptionsL33–33

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

  1. L33
    intro hA
10Establish hpL34–36

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

  1. L34
    have hp : ∃ T. SignedIncidenceFlatPrefix(A,r,s,M,l,T)Definitions: SignedIncidenceFlatPrefix
  2. L35
    apply IH
  3. L36
    exact hA
11Separate the logical casesL37–37

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

  1. L37
    cases hp
12Establish hvL38–45

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed support incidence flat entry exists.

  1. L38
    have hv : ∃ z. SignedIncidenceFlatEntry(A,r,s,M,S l,z)Definitions: SignedIncidenceFlatEntry
  2. L39
    specialize signed_support_incidence_flat_entry_exists (A)
  3. L40
    specialize signed_support_incidence_flat_entry_exists (r)
  4. L41
    specialize signed_support_incidence_flat_entry_exists (s)
  5. L42
    specialize signed_support_incidence_flat_entry_exists (M)
  6. L43
    specialize signed_support_incidence_flat_entry_exists (S l)
  7. L44
    apply signed_support_incidence_flat_entry_exists
  8. L45
    exact hA
13Separate the logical casesL46–46

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

  1. L46
    cases hv
14Establish hextL47–56

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed support incidence flat prefix append.

  1. L47
    have hext : ∃ U. SignedIncidenceFlatPrefix(A,r,s,M,S l,U) ∧ ArithTableEqual(x,U,S l)Definitions: ArithTableEqualSignedIncidenceFlatPrefix
  2. L48
    specialize signed_support_incidence_flat_prefix_append (A)
  3. L49
    specialize signed_support_incidence_flat_prefix_append (r)
  4. L50
    specialize signed_support_incidence_flat_prefix_append (s)
  5. L51
    specialize signed_support_incidence_flat_prefix_append (M)
  6. L52
    specialize signed_support_incidence_flat_prefix_append (l)
  7. L53
    specialize signed_support_incidence_flat_prefix_append (x)
  8. L54
    specialize signed_support_incidence_flat_prefix_append (x1)
  9. L55
    apply signed_support_incidence_flat_prefix_append
  10. L56
    exact hp_witness
15Use earlier factsL57–57

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

  1. L57
    exact hv_witness
16Separate the logical casesL58–59

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

  1. L58
    cases hext
  2. L59
    cases hext_witness
17Construct an explicit witnessL60–60

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

  1. L60
    exists x2
18Use earlier factsL61–61

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

  1. L61
    exact hext_witness_left

Library-wide reading audit

Original exact command ledger · 61 lines
  1. 0001intro A
  2. 0002intro r
  3. 0003intro s
  4. 0004intro M
  5. 0005intro l
  6. 0006induction l
  7. 0007intro hA
  8. 0008have hv : exists z. (exists ssr_flat_row_prefix_first_value ssr_flat_column_prefix_first_value. (((0)=(((S (M))*(ssr_flat_row_prefix_first_value)+(ssr_flat_column_prefix_first_value)))) /\ (((exists pvs_gap_prefix_first_valueremainder. pvs_gap_prefix_first_valueremainder + S (ssr_flat_column_prefix_first_value) = (S (M))) /\ (exists ssr_entry_value_prefix_first_valueentry ssr_entry_image_prefix_first_valueentry. ((exists dst_positive_code_prefix_first_valueentrysource dst_positive_scale_prefix_first_valueentrysource dst_negative_code_prefix_first_valueentrysource dst_negative_scale_prefix_first_valueentrysource dst_positive_prefix_first_valueentrysource dst_negative_prefix_first_valueentrysource. (((A) = (((((dst_positive_code_prefix_first_valueentrysource) + (dst_positive_scale_prefix_first_valueentrysource)) * S ((dst_positive_code_prefix_first_valueentrysource) + (dst_positive_scale_prefix_first_valueentrysource)) + ((dst_positive_scale_prefix_first_valueentrysource) + (dst_positive_scale_prefix_first_valueentrysource))) + (((dst_negative_code_prefix_first_valueentrysource) + (dst_negative_scale_prefix_first_valueentrysource)) * S ((dst_negative_code_prefix_first_valueentrysource) + (dst_negative_scale_prefix_first_valueentrysource)) + ((dst_negative_scale_prefix_first_valueentrysource) + (dst_negative_scale_prefix_first_valueentrysource)))) * S ((((dst_positive_code_prefix_first_valueentrysource) + (dst_positive_scale_prefix_first_valueentrysource)) * S ((dst_positive_code_prefix_first_valueentrysource) + (dst_positive_scale_prefix_first_valueentrysource)) + ((dst_positive_scale_prefix_first_valueentrysource) + (dst_positive_scale_prefix_first_valueentrysource))) + (((dst_negative_code_prefix_first_valueentrysource) + (dst_negative_scale_prefix_first_valueentrysource)) * S ((dst_negative_code_prefix_first_valueentrysource) + (dst_negative_scale_prefix_first_valueentrysource)) + ((dst_negative_scale_prefix_first_valueentrysource) + (dst_negative_scale_prefix_first_valueentrysource)))) + ((((dst_negative_code_prefix_first_valueentrysource) + (dst_negative_scale_prefix_first_valueentrysource)) * S ((dst_negative_code_prefix_first_valueentrysource) + (dst_negative_scale_prefix_first_valueentrysource)) + ((dst_negative_scale_prefix_first_valueentrysource) + (dst_negative_scale_prefix_first_valueentrysource))) + (((dst_negative_code_prefix_first_valueentrysource) + (dst_negative_scale_prefix_first_valueentrysource)) * S ((dst_negative_code_prefix_first_valueentrysource) + (dst_negative_scale_prefix_first_valueentrysource)) + ((dst_negative_scale_prefix_first_valueentrysource) + (dst_negative_scale_prefix_first_valueentrysource)))))) /\ (((((exists ff_h_pvs_prefix_first_valueentrysourcepositive. ff_h_pvs_prefix_first_valueentrysourcepositive + S (dst_positive_prefix_first_valueentrysource) = S ((S (ssr_flat_row_prefix_first_value)) * dst_positive_scale_prefix_first_valueentrysource)) /\ exists ff_q_pvs_prefix_first_valueentrysourcepositive. dst_positive_code_prefix_first_valueentrysource = ff_q_pvs_prefix_first_valueentrysourcepositive * S ((S (ssr_flat_row_prefix_first_value)) * dst_positive_scale_prefix_first_valueentrysource) + (dst_positive_prefix_first_valueentrysource))) /\ (((((exists ff_h_pvs_prefix_first_valueentrysourcenegative. ff_h_pvs_prefix_first_valueentrysourcenegative + S (dst_negative_prefix_first_valueentrysource) = S ((S (ssr_flat_row_prefix_first_value)) * dst_negative_scale_prefix_first_valueentrysource)) /\ exists ff_q_pvs_prefix_first_valueentrysourcenegative. dst_negative_code_prefix_first_valueentrysource = ff_q_pvs_prefix_first_valueentrysourcenegative * S ((S (ssr_flat_row_prefix_first_value)) * dst_negative_scale_prefix_first_valueentrysource) + (dst_negative_prefix_first_valueentrysource))) /\ (exists ge_balance_positive_prefix_first_valueentrysourcevalue ge_balance_negative_prefix_first_valueentrysourcevalue. (((((ssr_entry_value_prefix_first_valueentry) = 2 * (ge_balance_positive_prefix_first_valueentrysourcevalue) /\ (ge_balance_negative_prefix_first_valueentrysourcevalue) = 0) \/ exists ge_signed_half_prefix_first_valueentrysourcevaluedecode. (((ssr_entry_value_prefix_first_valueentry) = 2 * ge_signed_half_prefix_first_valueentrysourcevaluedecode + 1 /\ (ge_balance_positive_prefix_first_valueentrysourcevalue) = 0) /\ (ge_balance_negative_prefix_first_valueentrysourcevalue) = S ge_signed_half_prefix_first_valueentrysourcevaluedecode))) /\ ((dst_positive_prefix_first_valueentrysource) + ge_balance_negative_prefix_first_valueentrysourcevalue = (dst_negative_prefix_first_valueentrysource) + ge_balance_positive_prefix_first_valueentrysourcevalue))))))))) /\ (((((exists ff_h_pvs_prefix_first_valueentrymap. ff_h_pvs_prefix_first_valueentrymap + S (ssr_entry_image_prefix_first_valueentry) = S ((S (ssr_flat_row_prefix_first_value)) * s)) /\ exists ff_q_pvs_prefix_first_valueentrymap. r = ff_q_pvs_prefix_first_valueentrymap * S ((S (ssr_flat_row_prefix_first_value)) * s) + (ssr_entry_image_prefix_first_valueentry))) /\ (((((ssr_flat_column_prefix_first_value)=(ssr_entry_image_prefix_first_valueentry)) /\ ((z)=(ssr_entry_value_prefix_first_valueentry)))) \/ (((~((ssr_flat_column_prefix_first_value)=(ssr_entry_image_prefix_first_valueentry))) /\ ((z)=0))))))))))))
  9. 0009specialize signed_support_incidence_flat_entry_exists (A)
  10. 0010specialize signed_support_incidence_flat_entry_exists (r)
  11. 0011specialize signed_support_incidence_flat_entry_exists (s)
  12. 0012specialize signed_support_incidence_flat_entry_exists (M)
  13. 0013specialize signed_support_incidence_flat_entry_exists (0)
  14. 0014apply signed_support_incidence_flat_entry_exists
  15. 0015exact hA
  16. 0016cases hv
  17. 0017have ht : exists T. (((exists dst_positive_code_prefix_first_table dst_positive_scale_prefix_first_table dst_negative_code_prefix_first_table dst_negative_scale_prefix_first_table. (((T) = (((((dst_positive_code_prefix_first_table) + (dst_positive_scale_prefix_first_table)) * S ((dst_positive_code_prefix_first_table) + (dst_positive_scale_prefix_first_table)) + ((dst_positive_scale_prefix_first_table) + (dst_positive_scale_prefix_first_table))) + (((dst_negative_code_prefix_first_table) + (dst_negative_scale_prefix_first_table)) * S ((dst_negative_code_prefix_first_table) + (dst_negative_scale_prefix_first_table)) + ((dst_negative_scale_prefix_first_table) + (dst_negative_scale_prefix_first_table)))) * S ((((dst_positive_code_prefix_first_table) + (dst_positive_scale_prefix_first_table)) * S ((dst_positive_code_prefix_first_table) + (dst_positive_scale_prefix_first_table)) + ((dst_positive_scale_prefix_first_table) + (dst_positive_scale_prefix_first_table))) + (((dst_negative_code_prefix_first_table) + (dst_negative_scale_prefix_first_table)) * S ((dst_negative_code_prefix_first_table) + (dst_negative_scale_prefix_first_table)) + ((dst_negative_scale_prefix_first_table) + (dst_negative_scale_prefix_first_table)))) + ((((dst_negative_code_prefix_first_table) + (dst_negative_scale_prefix_first_table)) * S ((dst_negative_code_prefix_first_table) + (dst_negative_scale_prefix_first_table)) + ((dst_negative_scale_prefix_first_table) + (dst_negative_scale_prefix_first_table))) + (((dst_negative_code_prefix_first_table) + (dst_negative_scale_prefix_first_table)) * S ((dst_negative_code_prefix_first_table) + (dst_negative_scale_prefix_first_table)) + ((dst_negative_scale_prefix_first_table) + (dst_negative_scale_prefix_first_table)))))) /\ (forall dst_index_prefix_first_table. (exists pvs_le_gap_prefix_first_tabledomain. pvs_le_gap_prefix_first_tabledomain + (dst_index_prefix_first_table) = (0)) -> exists dst_positive_prefix_first_table dst_negative_prefix_first_table dst_value_prefix_first_table. ((((exists ff_h_pvs_prefix_first_tableentrypositive. ff_h_pvs_prefix_first_tableentrypositive + S (dst_positive_prefix_first_table) = S ((S (dst_index_prefix_first_table)) * dst_positive_scale_prefix_first_table)) /\ exists ff_q_pvs_prefix_first_tableentrypositive. dst_positive_code_prefix_first_table = ff_q_pvs_prefix_first_tableentrypositive * S ((S (dst_index_prefix_first_table)) * dst_positive_scale_prefix_first_table) + (dst_positive_prefix_first_table))) /\ (((((exists ff_h_pvs_prefix_first_tableentrynegative. ff_h_pvs_prefix_first_tableentrynegative + S (dst_negative_prefix_first_table) = S ((S (dst_index_prefix_first_table)) * dst_negative_scale_prefix_first_table)) /\ exists ff_q_pvs_prefix_first_tableentrynegative. dst_negative_code_prefix_first_table = ff_q_pvs_prefix_first_tableentrynegative * S ((S (dst_index_prefix_first_table)) * dst_negative_scale_prefix_first_table) + (dst_negative_prefix_first_table))) /\ (exists ge_balance_positive_prefix_first_tableentryvalue ge_balance_negative_prefix_first_tableentryvalue. (((((dst_value_prefix_first_table) = 2 * (ge_balance_positive_prefix_first_tableentryvalue) /\ (ge_balance_negative_prefix_first_tableentryvalue) = 0) \/ exists ge_signed_half_prefix_first_tableentryvaluedecode. (((dst_value_prefix_first_table) = 2 * ge_signed_half_prefix_first_tableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_first_tableentryvalue) = 0) /\ (ge_balance_negative_prefix_first_tableentryvalue) = S ge_signed_half_prefix_first_tableentryvaluedecode))) /\ ((dst_positive_prefix_first_table) + ge_balance_negative_prefix_first_tableentryvalue = (dst_negative_prefix_first_table) + ge_balance_positive_prefix_first_tableentryvalue))))))))) /\ (exists dst_positive_code_prefix_first_entry dst_positive_scale_prefix_first_entry dst_negative_code_prefix_first_entry dst_negative_scale_prefix_first_entry dst_positive_prefix_first_entry dst_negative_prefix_first_entry. (((T) = (((((dst_positive_code_prefix_first_entry) + (dst_positive_scale_prefix_first_entry)) * S ((dst_positive_code_prefix_first_entry) + (dst_positive_scale_prefix_first_entry)) + ((dst_positive_scale_prefix_first_entry) + (dst_positive_scale_prefix_first_entry))) + (((dst_negative_code_prefix_first_entry) + (dst_negative_scale_prefix_first_entry)) * S ((dst_negative_code_prefix_first_entry) + (dst_negative_scale_prefix_first_entry)) + ((dst_negative_scale_prefix_first_entry) + (dst_negative_scale_prefix_first_entry)))) * S ((((dst_positive_code_prefix_first_entry) + (dst_positive_scale_prefix_first_entry)) * S ((dst_positive_code_prefix_first_entry) + (dst_positive_scale_prefix_first_entry)) + ((dst_positive_scale_prefix_first_entry) + (dst_positive_scale_prefix_first_entry))) + (((dst_negative_code_prefix_first_entry) + (dst_negative_scale_prefix_first_entry)) * S ((dst_negative_code_prefix_first_entry) + (dst_negative_scale_prefix_first_entry)) + ((dst_negative_scale_prefix_first_entry) + (dst_negative_scale_prefix_first_entry)))) + ((((dst_negative_code_prefix_first_entry) + (dst_negative_scale_prefix_first_entry)) * S ((dst_negative_code_prefix_first_entry) + (dst_negative_scale_prefix_first_entry)) + ((dst_negative_scale_prefix_first_entry) + (dst_negative_scale_prefix_first_entry))) + (((dst_negative_code_prefix_first_entry) + (dst_negative_scale_prefix_first_entry)) * S ((dst_negative_code_prefix_first_entry) + (dst_negative_scale_prefix_first_entry)) + ((dst_negative_scale_prefix_first_entry) + (dst_negative_scale_prefix_first_entry)))))) /\ (((((exists ff_h_pvs_prefix_first_entrypositive. ff_h_pvs_prefix_first_entrypositive + S (dst_positive_prefix_first_entry) = S ((S (0)) * dst_positive_scale_prefix_first_entry)) /\ exists ff_q_pvs_prefix_first_entrypositive. dst_positive_code_prefix_first_entry = ff_q_pvs_prefix_first_entrypositive * S ((S (0)) * dst_positive_scale_prefix_first_entry) + (dst_positive_prefix_first_entry))) /\ (((((exists ff_h_pvs_prefix_first_entrynegative. ff_h_pvs_prefix_first_entrynegative + S (dst_negative_prefix_first_entry) = S ((S (0)) * dst_negative_scale_prefix_first_entry)) /\ exists ff_q_pvs_prefix_first_entrynegative. dst_negative_code_prefix_first_entry = ff_q_pvs_prefix_first_entrynegative * S ((S (0)) * dst_negative_scale_prefix_first_entry) + (dst_negative_prefix_first_entry))) /\ (exists ge_balance_positive_prefix_first_entryvalue ge_balance_negative_prefix_first_entryvalue. (((((x) = 2 * (ge_balance_positive_prefix_first_entryvalue) /\ (ge_balance_negative_prefix_first_entryvalue) = 0) \/ exists ge_signed_half_prefix_first_entryvaluedecode. (((x) = 2 * ge_signed_half_prefix_first_entryvaluedecode + 1 /\ (ge_balance_positive_prefix_first_entryvalue) = 0) /\ (ge_balance_negative_prefix_first_entryvalue) = S ge_signed_half_prefix_first_entryvaluedecode))) /\ ((dst_positive_prefix_first_entry) + ge_balance_negative_prefix_first_entryvalue = (dst_negative_prefix_first_entry) + ge_balance_positive_prefix_first_entryvalue)))))))))))
  18. 0018specialize arithmetic_signed_table_singleton (x)
  19. 0019apply arithmetic_signed_table_singleton
  20. 0020cases ht
  21. 0021cases ht_witness
  22. 0022exists x1
  23. 0023specialize signed_support_incidence_flat_prefix_zero (A)
  24. 0024specialize signed_support_incidence_flat_prefix_zero (r)
  25. 0025specialize signed_support_incidence_flat_prefix_zero (s)
  26. 0026specialize signed_support_incidence_flat_prefix_zero (M)
  27. 0027specialize signed_support_incidence_flat_prefix_zero (x1)
  28. 0028specialize signed_support_incidence_flat_prefix_zero (x)
  29. 0029apply signed_support_incidence_flat_prefix_zero
  30. 0030exact ht_witness_left
  31. 0031exact ht_witness_right
  32. 0032exact hv_witness
  33. 0033intro hA
  34. 0034have hp : exists T. (((exists dst_positive_code_prefix_previoustable dst_positive_scale_prefix_previoustable dst_negative_code_prefix_previoustable dst_negative_scale_prefix_previoustable. (((T) = (((((dst_positive_code_prefix_previoustable) + (dst_positive_scale_prefix_previoustable)) * S ((dst_positive_code_prefix_previoustable) + (dst_positive_scale_prefix_previoustable)) + ((dst_positive_scale_prefix_previoustable) + (dst_positive_scale_prefix_previoustable))) + (((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) * S ((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) + ((dst_negative_scale_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)))) * S ((((dst_positive_code_prefix_previoustable) + (dst_positive_scale_prefix_previoustable)) * S ((dst_positive_code_prefix_previoustable) + (dst_positive_scale_prefix_previoustable)) + ((dst_positive_scale_prefix_previoustable) + (dst_positive_scale_prefix_previoustable))) + (((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) * S ((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) + ((dst_negative_scale_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)))) + ((((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) * S ((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) + ((dst_negative_scale_prefix_previoustable) + (dst_negative_scale_prefix_previoustable))) + (((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) * S ((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) + ((dst_negative_scale_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)))))) /\ (forall dst_index_prefix_previoustable. (exists pvs_le_gap_prefix_previoustabledomain. pvs_le_gap_prefix_previoustabledomain + (dst_index_prefix_previoustable) = (l)) -> exists dst_positive_prefix_previoustable dst_negative_prefix_previoustable dst_value_prefix_previoustable. ((((exists ff_h_pvs_prefix_previoustableentrypositive. ff_h_pvs_prefix_previoustableentrypositive + S (dst_positive_prefix_previoustable) = S ((S (dst_index_prefix_previoustable)) * dst_positive_scale_prefix_previoustable)) /\ exists ff_q_pvs_prefix_previoustableentrypositive. dst_positive_code_prefix_previoustable = ff_q_pvs_prefix_previoustableentrypositive * S ((S (dst_index_prefix_previoustable)) * dst_positive_scale_prefix_previoustable) + (dst_positive_prefix_previoustable))) /\ (((((exists ff_h_pvs_prefix_previoustableentrynegative. ff_h_pvs_prefix_previoustableentrynegative + S (dst_negative_prefix_previoustable) = S ((S (dst_index_prefix_previoustable)) * dst_negative_scale_prefix_previoustable)) /\ exists ff_q_pvs_prefix_previoustableentrynegative. dst_negative_code_prefix_previoustable = ff_q_pvs_prefix_previoustableentrynegative * S ((S (dst_index_prefix_previoustable)) * dst_negative_scale_prefix_previoustable) + (dst_negative_prefix_previoustable))) /\ (exists ge_balance_positive_prefix_previoustableentryvalue ge_balance_negative_prefix_previoustableentryvalue. (((((dst_value_prefix_previoustable) = 2 * (ge_balance_positive_prefix_previoustableentryvalue) /\ (ge_balance_negative_prefix_previoustableentryvalue) = 0) \/ exists ge_signed_half_prefix_previoustableentryvaluedecode. (((dst_value_prefix_previoustable) = 2 * ge_signed_half_prefix_previoustableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_previoustableentryvalue) = 0) /\ (ge_balance_negative_prefix_previoustableentryvalue) = S ge_signed_half_prefix_previoustableentryvaluedecode))) /\ ((dst_positive_prefix_previoustable) + ge_balance_negative_prefix_previoustableentryvalue = (dst_negative_prefix_previoustable) + ge_balance_positive_prefix_previoustableentryvalue))))))))) /\ (forall ssr_prefix_index_prefix_previous ssr_prefix_value_prefix_previous. (exists pvs_le_gap_prefix_previousbound. pvs_le_gap_prefix_previousbound + (ssr_prefix_index_prefix_previous) = (l)) -> (exists dst_positive_code_prefix_previouslookup dst_positive_scale_prefix_previouslookup dst_negative_code_prefix_previouslookup dst_negative_scale_prefix_previouslookup dst_positive_prefix_previouslookup dst_negative_prefix_previouslookup. (((T) = (((((dst_positive_code_prefix_previouslookup) + (dst_positive_scale_prefix_previouslookup)) * S ((dst_positive_code_prefix_previouslookup) + (dst_positive_scale_prefix_previouslookup)) + ((dst_positive_scale_prefix_previouslookup) + (dst_positive_scale_prefix_previouslookup))) + (((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) * S ((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) + ((dst_negative_scale_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)))) * S ((((dst_positive_code_prefix_previouslookup) + (dst_positive_scale_prefix_previouslookup)) * S ((dst_positive_code_prefix_previouslookup) + (dst_positive_scale_prefix_previouslookup)) + ((dst_positive_scale_prefix_previouslookup) + (dst_positive_scale_prefix_previouslookup))) + (((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) * S ((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) + ((dst_negative_scale_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)))) + ((((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) * S ((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) + ((dst_negative_scale_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup))) + (((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) * S ((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) + ((dst_negative_scale_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)))))) /\ (((((exists ff_h_pvs_prefix_previouslookuppositive. ff_h_pvs_prefix_previouslookuppositive + S (dst_positive_prefix_previouslookup) = S ((S (ssr_prefix_index_prefix_previous)) * dst_positive_scale_prefix_previouslookup)) /\ exists ff_q_pvs_prefix_previouslookuppositive. dst_positive_code_prefix_previouslookup = ff_q_pvs_prefix_previouslookuppositive * S ((S (ssr_prefix_index_prefix_previous)) * dst_positive_scale_prefix_previouslookup) + (dst_positive_prefix_previouslookup))) /\ (((((exists ff_h_pvs_prefix_previouslookupnegative. ff_h_pvs_prefix_previouslookupnegative + S (dst_negative_prefix_previouslookup) = S ((S (ssr_prefix_index_prefix_previous)) * dst_negative_scale_prefix_previouslookup)) /\ exists ff_q_pvs_prefix_previouslookupnegative. dst_negative_code_prefix_previouslookup = ff_q_pvs_prefix_previouslookupnegative * S ((S (ssr_prefix_index_prefix_previous)) * dst_negative_scale_prefix_previouslookup) + (dst_negative_prefix_previouslookup))) /\ (exists ge_balance_positive_prefix_previouslookupvalue ge_balance_negative_prefix_previouslookupvalue. (((((ssr_prefix_value_prefix_previous) = 2 * (ge_balance_positive_prefix_previouslookupvalue) /\ (ge_balance_negative_prefix_previouslookupvalue) = 0) \/ exists ge_signed_half_prefix_previouslookupvaluedecode. (((ssr_prefix_value_prefix_previous) = 2 * ge_signed_half_prefix_previouslookupvaluedecode + 1 /\ (ge_balance_positive_prefix_previouslookupvalue) = 0) /\ (ge_balance_negative_prefix_previouslookupvalue) = S ge_signed_half_prefix_previouslookupvaluedecode))) /\ ((dst_positive_prefix_previouslookup) + ge_balance_negative_prefix_previouslookupvalue = (dst_negative_prefix_previouslookup) + ge_balance_positive_prefix_previouslookupvalue))))))))) -> (exists ssr_flat_row_prefix_previousentry ssr_flat_column_prefix_previousentry. (((ssr_prefix_index_prefix_previous)=(((S (M))*(ssr_flat_row_prefix_previousentry)+(ssr_flat_column_prefix_previousentry)))) /\ (((exists pvs_gap_prefix_previousentryremainder. pvs_gap_prefix_previousentryremainder + S (ssr_flat_column_prefix_previousentry) = (S (M))) /\ (exists ssr_entry_value_prefix_previousentryentry ssr_entry_image_prefix_previousentryentry. ((exists dst_positive_code_prefix_previousentryentrysource dst_positive_scale_prefix_previousentryentrysource dst_negative_code_prefix_previousentryentrysource dst_negative_scale_prefix_previousentryentrysource dst_positive_prefix_previousentryentrysource dst_negative_prefix_previousentryentrysource. (((A) = (((((dst_positive_code_prefix_previousentryentrysource) + (dst_positive_scale_prefix_previousentryentrysource)) * S ((dst_positive_code_prefix_previousentryentrysource) + (dst_positive_scale_prefix_previousentryentrysource)) + ((dst_positive_scale_prefix_previousentryentrysource) + (dst_positive_scale_prefix_previousentryentrysource))) + (((dst_negative_code_prefix_previousentryentrysource) + (dst_negative_scale_prefix_previousentryentrysource)) * S ((dst_negative_code_prefix_previousentryentrysource) + (dst_negative_scale_prefix_previousentryentrysource)) + ((dst_negative_scale_prefix_previousentryentrysource) + (dst_negative_scale_prefix_previousentryentrysource)))) * S ((((dst_positive_code_prefix_previousentryentrysource) + (dst_positive_scale_prefix_previousentryentrysource)) * S ((dst_positive_code_prefix_previousentryentrysource) + (dst_positive_scale_prefix_previousentryentrysource)) + ((dst_positive_scale_prefix_previousentryentrysource) + (dst_positive_scale_prefix_previousentryentrysource))) + (((dst_negative_code_prefix_previousentryentrysource) + (dst_negative_scale_prefix_previousentryentrysource)) * S ((dst_negative_code_prefix_previousentryentrysource) + (dst_negative_scale_prefix_previousentryentrysource)) + ((dst_negative_scale_prefix_previousentryentrysource) + (dst_negative_scale_prefix_previousentryentrysource)))) + ((((dst_negative_code_prefix_previousentryentrysource) + (dst_negative_scale_prefix_previousentryentrysource)) * S ((dst_negative_code_prefix_previousentryentrysource) + (dst_negative_scale_prefix_previousentryentrysource)) + ((dst_negative_scale_prefix_previousentryentrysource) + (dst_negative_scale_prefix_previousentryentrysource))) + (((dst_negative_code_prefix_previousentryentrysource) + (dst_negative_scale_prefix_previousentryentrysource)) * S ((dst_negative_code_prefix_previousentryentrysource) + (dst_negative_scale_prefix_previousentryentrysource)) + ((dst_negative_scale_prefix_previousentryentrysource) + (dst_negative_scale_prefix_previousentryentrysource)))))) /\ (((((exists ff_h_pvs_prefix_previousentryentrysourcepositive. ff_h_pvs_prefix_previousentryentrysourcepositive + S (dst_positive_prefix_previousentryentrysource) = S ((S (ssr_flat_row_prefix_previousentry)) * dst_positive_scale_prefix_previousentryentrysource)) /\ exists ff_q_pvs_prefix_previousentryentrysourcepositive. dst_positive_code_prefix_previousentryentrysource = ff_q_pvs_prefix_previousentryentrysourcepositive * S ((S (ssr_flat_row_prefix_previousentry)) * dst_positive_scale_prefix_previousentryentrysource) + (dst_positive_prefix_previousentryentrysource))) /\ (((((exists ff_h_pvs_prefix_previousentryentrysourcenegative. ff_h_pvs_prefix_previousentryentrysourcenegative + S (dst_negative_prefix_previousentryentrysource) = S ((S (ssr_flat_row_prefix_previousentry)) * dst_negative_scale_prefix_previousentryentrysource)) /\ exists ff_q_pvs_prefix_previousentryentrysourcenegative. dst_negative_code_prefix_previousentryentrysource = ff_q_pvs_prefix_previousentryentrysourcenegative * S ((S (ssr_flat_row_prefix_previousentry)) * dst_negative_scale_prefix_previousentryentrysource) + (dst_negative_prefix_previousentryentrysource))) /\ (exists ge_balance_positive_prefix_previousentryentrysourcevalue ge_balance_negative_prefix_previousentryentrysourcevalue. (((((ssr_entry_value_prefix_previousentryentry) = 2 * (ge_balance_positive_prefix_previousentryentrysourcevalue) /\ (ge_balance_negative_prefix_previousentryentrysourcevalue) = 0) \/ exists ge_signed_half_prefix_previousentryentrysourcevaluedecode. (((ssr_entry_value_prefix_previousentryentry) = 2 * ge_signed_half_prefix_previousentryentrysourcevaluedecode + 1 /\ (ge_balance_positive_prefix_previousentryentrysourcevalue) = 0) /\ (ge_balance_negative_prefix_previousentryentrysourcevalue) = S ge_signed_half_prefix_previousentryentrysourcevaluedecode))) /\ ((dst_positive_prefix_previousentryentrysource) + ge_balance_negative_prefix_previousentryentrysourcevalue = (dst_negative_prefix_previousentryentrysource) + ge_balance_positive_prefix_previousentryentrysourcevalue))))))))) /\ (((((exists ff_h_pvs_prefix_previousentryentrymap. ff_h_pvs_prefix_previousentryentrymap + S (ssr_entry_image_prefix_previousentryentry) = S ((S (ssr_flat_row_prefix_previousentry)) * s)) /\ exists ff_q_pvs_prefix_previousentryentrymap. r = ff_q_pvs_prefix_previousentryentrymap * S ((S (ssr_flat_row_prefix_previousentry)) * s) + (ssr_entry_image_prefix_previousentryentry))) /\ (((((ssr_flat_column_prefix_previousentry)=(ssr_entry_image_prefix_previousentryentry)) /\ ((ssr_prefix_value_prefix_previous)=(ssr_entry_value_prefix_previousentryentry)))) \/ (((~((ssr_flat_column_prefix_previousentry)=(ssr_entry_image_prefix_previousentryentry))) /\ ((ssr_prefix_value_prefix_previous)=0)))))))))))))))
  35. 0035apply IH
  36. 0036exact hA
  37. 0037cases hp
  38. 0038have hv : exists z. (exists ssr_flat_row_prefix_next_value ssr_flat_column_prefix_next_value. (((S l)=(((S (M))*(ssr_flat_row_prefix_next_value)+(ssr_flat_column_prefix_next_value)))) /\ (((exists pvs_gap_prefix_next_valueremainder. pvs_gap_prefix_next_valueremainder + S (ssr_flat_column_prefix_next_value) = (S (M))) /\ (exists ssr_entry_value_prefix_next_valueentry ssr_entry_image_prefix_next_valueentry. ((exists dst_positive_code_prefix_next_valueentrysource dst_positive_scale_prefix_next_valueentrysource dst_negative_code_prefix_next_valueentrysource dst_negative_scale_prefix_next_valueentrysource dst_positive_prefix_next_valueentrysource dst_negative_prefix_next_valueentrysource. (((A) = (((((dst_positive_code_prefix_next_valueentrysource) + (dst_positive_scale_prefix_next_valueentrysource)) * S ((dst_positive_code_prefix_next_valueentrysource) + (dst_positive_scale_prefix_next_valueentrysource)) + ((dst_positive_scale_prefix_next_valueentrysource) + (dst_positive_scale_prefix_next_valueentrysource))) + (((dst_negative_code_prefix_next_valueentrysource) + (dst_negative_scale_prefix_next_valueentrysource)) * S ((dst_negative_code_prefix_next_valueentrysource) + (dst_negative_scale_prefix_next_valueentrysource)) + ((dst_negative_scale_prefix_next_valueentrysource) + (dst_negative_scale_prefix_next_valueentrysource)))) * S ((((dst_positive_code_prefix_next_valueentrysource) + (dst_positive_scale_prefix_next_valueentrysource)) * S ((dst_positive_code_prefix_next_valueentrysource) + (dst_positive_scale_prefix_next_valueentrysource)) + ((dst_positive_scale_prefix_next_valueentrysource) + (dst_positive_scale_prefix_next_valueentrysource))) + (((dst_negative_code_prefix_next_valueentrysource) + (dst_negative_scale_prefix_next_valueentrysource)) * S ((dst_negative_code_prefix_next_valueentrysource) + (dst_negative_scale_prefix_next_valueentrysource)) + ((dst_negative_scale_prefix_next_valueentrysource) + (dst_negative_scale_prefix_next_valueentrysource)))) + ((((dst_negative_code_prefix_next_valueentrysource) + (dst_negative_scale_prefix_next_valueentrysource)) * S ((dst_negative_code_prefix_next_valueentrysource) + (dst_negative_scale_prefix_next_valueentrysource)) + ((dst_negative_scale_prefix_next_valueentrysource) + (dst_negative_scale_prefix_next_valueentrysource))) + (((dst_negative_code_prefix_next_valueentrysource) + (dst_negative_scale_prefix_next_valueentrysource)) * S ((dst_negative_code_prefix_next_valueentrysource) + (dst_negative_scale_prefix_next_valueentrysource)) + ((dst_negative_scale_prefix_next_valueentrysource) + (dst_negative_scale_prefix_next_valueentrysource)))))) /\ (((((exists ff_h_pvs_prefix_next_valueentrysourcepositive. ff_h_pvs_prefix_next_valueentrysourcepositive + S (dst_positive_prefix_next_valueentrysource) = S ((S (ssr_flat_row_prefix_next_value)) * dst_positive_scale_prefix_next_valueentrysource)) /\ exists ff_q_pvs_prefix_next_valueentrysourcepositive. dst_positive_code_prefix_next_valueentrysource = ff_q_pvs_prefix_next_valueentrysourcepositive * S ((S (ssr_flat_row_prefix_next_value)) * dst_positive_scale_prefix_next_valueentrysource) + (dst_positive_prefix_next_valueentrysource))) /\ (((((exists ff_h_pvs_prefix_next_valueentrysourcenegative. ff_h_pvs_prefix_next_valueentrysourcenegative + S (dst_negative_prefix_next_valueentrysource) = S ((S (ssr_flat_row_prefix_next_value)) * dst_negative_scale_prefix_next_valueentrysource)) /\ exists ff_q_pvs_prefix_next_valueentrysourcenegative. dst_negative_code_prefix_next_valueentrysource = ff_q_pvs_prefix_next_valueentrysourcenegative * S ((S (ssr_flat_row_prefix_next_value)) * dst_negative_scale_prefix_next_valueentrysource) + (dst_negative_prefix_next_valueentrysource))) /\ (exists ge_balance_positive_prefix_next_valueentrysourcevalue ge_balance_negative_prefix_next_valueentrysourcevalue. (((((ssr_entry_value_prefix_next_valueentry) = 2 * (ge_balance_positive_prefix_next_valueentrysourcevalue) /\ (ge_balance_negative_prefix_next_valueentrysourcevalue) = 0) \/ exists ge_signed_half_prefix_next_valueentrysourcevaluedecode. (((ssr_entry_value_prefix_next_valueentry) = 2 * ge_signed_half_prefix_next_valueentrysourcevaluedecode + 1 /\ (ge_balance_positive_prefix_next_valueentrysourcevalue) = 0) /\ (ge_balance_negative_prefix_next_valueentrysourcevalue) = S ge_signed_half_prefix_next_valueentrysourcevaluedecode))) /\ ((dst_positive_prefix_next_valueentrysource) + ge_balance_negative_prefix_next_valueentrysourcevalue = (dst_negative_prefix_next_valueentrysource) + ge_balance_positive_prefix_next_valueentrysourcevalue))))))))) /\ (((((exists ff_h_pvs_prefix_next_valueentrymap. ff_h_pvs_prefix_next_valueentrymap + S (ssr_entry_image_prefix_next_valueentry) = S ((S (ssr_flat_row_prefix_next_value)) * s)) /\ exists ff_q_pvs_prefix_next_valueentrymap. r = ff_q_pvs_prefix_next_valueentrymap * S ((S (ssr_flat_row_prefix_next_value)) * s) + (ssr_entry_image_prefix_next_valueentry))) /\ (((((ssr_flat_column_prefix_next_value)=(ssr_entry_image_prefix_next_valueentry)) /\ ((z)=(ssr_entry_value_prefix_next_valueentry)))) \/ (((~((ssr_flat_column_prefix_next_value)=(ssr_entry_image_prefix_next_valueentry))) /\ ((z)=0))))))))))))
  39. 0039specialize signed_support_incidence_flat_entry_exists (A)
  40. 0040specialize signed_support_incidence_flat_entry_exists (r)
  41. 0041specialize signed_support_incidence_flat_entry_exists (s)
  42. 0042specialize signed_support_incidence_flat_entry_exists (M)
  43. 0043specialize signed_support_incidence_flat_entry_exists (S l)
  44. 0044apply signed_support_incidence_flat_entry_exists
  45. 0045exact hA
  46. 0046cases hv
  47. 0047have hext : exists U. (((((exists dst_positive_code_prefix_nexttable dst_positive_scale_prefix_nexttable dst_negative_code_prefix_nexttable dst_negative_scale_prefix_nexttable. (((U) = (((((dst_positive_code_prefix_nexttable) + (dst_positive_scale_prefix_nexttable)) * S ((dst_positive_code_prefix_nexttable) + (dst_positive_scale_prefix_nexttable)) + ((dst_positive_scale_prefix_nexttable) + (dst_positive_scale_prefix_nexttable))) + (((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) * S ((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) + ((dst_negative_scale_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)))) * S ((((dst_positive_code_prefix_nexttable) + (dst_positive_scale_prefix_nexttable)) * S ((dst_positive_code_prefix_nexttable) + (dst_positive_scale_prefix_nexttable)) + ((dst_positive_scale_prefix_nexttable) + (dst_positive_scale_prefix_nexttable))) + (((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) * S ((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) + ((dst_negative_scale_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)))) + ((((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) * S ((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) + ((dst_negative_scale_prefix_nexttable) + (dst_negative_scale_prefix_nexttable))) + (((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) * S ((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) + ((dst_negative_scale_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)))))) /\ (forall dst_index_prefix_nexttable. (exists pvs_le_gap_prefix_nexttabledomain. pvs_le_gap_prefix_nexttabledomain + (dst_index_prefix_nexttable) = (S l)) -> exists dst_positive_prefix_nexttable dst_negative_prefix_nexttable dst_value_prefix_nexttable. ((((exists ff_h_pvs_prefix_nexttableentrypositive. ff_h_pvs_prefix_nexttableentrypositive + S (dst_positive_prefix_nexttable) = S ((S (dst_index_prefix_nexttable)) * dst_positive_scale_prefix_nexttable)) /\ exists ff_q_pvs_prefix_nexttableentrypositive. dst_positive_code_prefix_nexttable = ff_q_pvs_prefix_nexttableentrypositive * S ((S (dst_index_prefix_nexttable)) * dst_positive_scale_prefix_nexttable) + (dst_positive_prefix_nexttable))) /\ (((((exists ff_h_pvs_prefix_nexttableentrynegative. ff_h_pvs_prefix_nexttableentrynegative + S (dst_negative_prefix_nexttable) = S ((S (dst_index_prefix_nexttable)) * dst_negative_scale_prefix_nexttable)) /\ exists ff_q_pvs_prefix_nexttableentrynegative. dst_negative_code_prefix_nexttable = ff_q_pvs_prefix_nexttableentrynegative * S ((S (dst_index_prefix_nexttable)) * dst_negative_scale_prefix_nexttable) + (dst_negative_prefix_nexttable))) /\ (exists ge_balance_positive_prefix_nexttableentryvalue ge_balance_negative_prefix_nexttableentryvalue. (((((dst_value_prefix_nexttable) = 2 * (ge_balance_positive_prefix_nexttableentryvalue) /\ (ge_balance_negative_prefix_nexttableentryvalue) = 0) \/ exists ge_signed_half_prefix_nexttableentryvaluedecode. (((dst_value_prefix_nexttable) = 2 * ge_signed_half_prefix_nexttableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_nexttableentryvalue) = 0) /\ (ge_balance_negative_prefix_nexttableentryvalue) = S ge_signed_half_prefix_nexttableentryvaluedecode))) /\ ((dst_positive_prefix_nexttable) + ge_balance_negative_prefix_nexttableentryvalue = (dst_negative_prefix_nexttable) + ge_balance_positive_prefix_nexttableentryvalue))))))))) /\ (forall ssr_prefix_index_prefix_next ssr_prefix_value_prefix_next. (exists pvs_le_gap_prefix_nextbound. pvs_le_gap_prefix_nextbound + (ssr_prefix_index_prefix_next) = (S l)) -> (exists dst_positive_code_prefix_nextlookup dst_positive_scale_prefix_nextlookup dst_negative_code_prefix_nextlookup dst_negative_scale_prefix_nextlookup dst_positive_prefix_nextlookup dst_negative_prefix_nextlookup. (((U) = (((((dst_positive_code_prefix_nextlookup) + (dst_positive_scale_prefix_nextlookup)) * S ((dst_positive_code_prefix_nextlookup) + (dst_positive_scale_prefix_nextlookup)) + ((dst_positive_scale_prefix_nextlookup) + (dst_positive_scale_prefix_nextlookup))) + (((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) * S ((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) + ((dst_negative_scale_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)))) * S ((((dst_positive_code_prefix_nextlookup) + (dst_positive_scale_prefix_nextlookup)) * S ((dst_positive_code_prefix_nextlookup) + (dst_positive_scale_prefix_nextlookup)) + ((dst_positive_scale_prefix_nextlookup) + (dst_positive_scale_prefix_nextlookup))) + (((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) * S ((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) + ((dst_negative_scale_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)))) + ((((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) * S ((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) + ((dst_negative_scale_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup))) + (((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) * S ((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) + ((dst_negative_scale_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)))))) /\ (((((exists ff_h_pvs_prefix_nextlookuppositive. ff_h_pvs_prefix_nextlookuppositive + S (dst_positive_prefix_nextlookup) = S ((S (ssr_prefix_index_prefix_next)) * dst_positive_scale_prefix_nextlookup)) /\ exists ff_q_pvs_prefix_nextlookuppositive. dst_positive_code_prefix_nextlookup = ff_q_pvs_prefix_nextlookuppositive * S ((S (ssr_prefix_index_prefix_next)) * dst_positive_scale_prefix_nextlookup) + (dst_positive_prefix_nextlookup))) /\ (((((exists ff_h_pvs_prefix_nextlookupnegative. ff_h_pvs_prefix_nextlookupnegative + S (dst_negative_prefix_nextlookup) = S ((S (ssr_prefix_index_prefix_next)) * dst_negative_scale_prefix_nextlookup)) /\ exists ff_q_pvs_prefix_nextlookupnegative. dst_negative_code_prefix_nextlookup = ff_q_pvs_prefix_nextlookupnegative * S ((S (ssr_prefix_index_prefix_next)) * dst_negative_scale_prefix_nextlookup) + (dst_negative_prefix_nextlookup))) /\ (exists ge_balance_positive_prefix_nextlookupvalue ge_balance_negative_prefix_nextlookupvalue. (((((ssr_prefix_value_prefix_next) = 2 * (ge_balance_positive_prefix_nextlookupvalue) /\ (ge_balance_negative_prefix_nextlookupvalue) = 0) \/ exists ge_signed_half_prefix_nextlookupvaluedecode. (((ssr_prefix_value_prefix_next) = 2 * ge_signed_half_prefix_nextlookupvaluedecode + 1 /\ (ge_balance_positive_prefix_nextlookupvalue) = 0) /\ (ge_balance_negative_prefix_nextlookupvalue) = S ge_signed_half_prefix_nextlookupvaluedecode))) /\ ((dst_positive_prefix_nextlookup) + ge_balance_negative_prefix_nextlookupvalue = (dst_negative_prefix_nextlookup) + ge_balance_positive_prefix_nextlookupvalue))))))))) -> (exists ssr_flat_row_prefix_nextentry ssr_flat_column_prefix_nextentry. (((ssr_prefix_index_prefix_next)=(((S (M))*(ssr_flat_row_prefix_nextentry)+(ssr_flat_column_prefix_nextentry)))) /\ (((exists pvs_gap_prefix_nextentryremainder. pvs_gap_prefix_nextentryremainder + S (ssr_flat_column_prefix_nextentry) = (S (M))) /\ (exists ssr_entry_value_prefix_nextentryentry ssr_entry_image_prefix_nextentryentry. ((exists dst_positive_code_prefix_nextentryentrysource dst_positive_scale_prefix_nextentryentrysource dst_negative_code_prefix_nextentryentrysource dst_negative_scale_prefix_nextentryentrysource dst_positive_prefix_nextentryentrysource dst_negative_prefix_nextentryentrysource. (((A) = (((((dst_positive_code_prefix_nextentryentrysource) + (dst_positive_scale_prefix_nextentryentrysource)) * S ((dst_positive_code_prefix_nextentryentrysource) + (dst_positive_scale_prefix_nextentryentrysource)) + ((dst_positive_scale_prefix_nextentryentrysource) + (dst_positive_scale_prefix_nextentryentrysource))) + (((dst_negative_code_prefix_nextentryentrysource) + (dst_negative_scale_prefix_nextentryentrysource)) * S ((dst_negative_code_prefix_nextentryentrysource) + (dst_negative_scale_prefix_nextentryentrysource)) + ((dst_negative_scale_prefix_nextentryentrysource) + (dst_negative_scale_prefix_nextentryentrysource)))) * S ((((dst_positive_code_prefix_nextentryentrysource) + (dst_positive_scale_prefix_nextentryentrysource)) * S ((dst_positive_code_prefix_nextentryentrysource) + (dst_positive_scale_prefix_nextentryentrysource)) + ((dst_positive_scale_prefix_nextentryentrysource) + (dst_positive_scale_prefix_nextentryentrysource))) + (((dst_negative_code_prefix_nextentryentrysource) + (dst_negative_scale_prefix_nextentryentrysource)) * S ((dst_negative_code_prefix_nextentryentrysource) + (dst_negative_scale_prefix_nextentryentrysource)) + ((dst_negative_scale_prefix_nextentryentrysource) + (dst_negative_scale_prefix_nextentryentrysource)))) + ((((dst_negative_code_prefix_nextentryentrysource) + (dst_negative_scale_prefix_nextentryentrysource)) * S ((dst_negative_code_prefix_nextentryentrysource) + (dst_negative_scale_prefix_nextentryentrysource)) + ((dst_negative_scale_prefix_nextentryentrysource) + (dst_negative_scale_prefix_nextentryentrysource))) + (((dst_negative_code_prefix_nextentryentrysource) + (dst_negative_scale_prefix_nextentryentrysource)) * S ((dst_negative_code_prefix_nextentryentrysource) + (dst_negative_scale_prefix_nextentryentrysource)) + ((dst_negative_scale_prefix_nextentryentrysource) + (dst_negative_scale_prefix_nextentryentrysource)))))) /\ (((((exists ff_h_pvs_prefix_nextentryentrysourcepositive. ff_h_pvs_prefix_nextentryentrysourcepositive + S (dst_positive_prefix_nextentryentrysource) = S ((S (ssr_flat_row_prefix_nextentry)) * dst_positive_scale_prefix_nextentryentrysource)) /\ exists ff_q_pvs_prefix_nextentryentrysourcepositive. dst_positive_code_prefix_nextentryentrysource = ff_q_pvs_prefix_nextentryentrysourcepositive * S ((S (ssr_flat_row_prefix_nextentry)) * dst_positive_scale_prefix_nextentryentrysource) + (dst_positive_prefix_nextentryentrysource))) /\ (((((exists ff_h_pvs_prefix_nextentryentrysourcenegative. ff_h_pvs_prefix_nextentryentrysourcenegative + S (dst_negative_prefix_nextentryentrysource) = S ((S (ssr_flat_row_prefix_nextentry)) * dst_negative_scale_prefix_nextentryentrysource)) /\ exists ff_q_pvs_prefix_nextentryentrysourcenegative. dst_negative_code_prefix_nextentryentrysource = ff_q_pvs_prefix_nextentryentrysourcenegative * S ((S (ssr_flat_row_prefix_nextentry)) * dst_negative_scale_prefix_nextentryentrysource) + (dst_negative_prefix_nextentryentrysource))) /\ (exists ge_balance_positive_prefix_nextentryentrysourcevalue ge_balance_negative_prefix_nextentryentrysourcevalue. (((((ssr_entry_value_prefix_nextentryentry) = 2 * (ge_balance_positive_prefix_nextentryentrysourcevalue) /\ (ge_balance_negative_prefix_nextentryentrysourcevalue) = 0) \/ exists ge_signed_half_prefix_nextentryentrysourcevaluedecode. (((ssr_entry_value_prefix_nextentryentry) = 2 * ge_signed_half_prefix_nextentryentrysourcevaluedecode + 1 /\ (ge_balance_positive_prefix_nextentryentrysourcevalue) = 0) /\ (ge_balance_negative_prefix_nextentryentrysourcevalue) = S ge_signed_half_prefix_nextentryentrysourcevaluedecode))) /\ ((dst_positive_prefix_nextentryentrysource) + ge_balance_negative_prefix_nextentryentrysourcevalue = (dst_negative_prefix_nextentryentrysource) + ge_balance_positive_prefix_nextentryentrysourcevalue))))))))) /\ (((((exists ff_h_pvs_prefix_nextentryentrymap. ff_h_pvs_prefix_nextentryentrymap + S (ssr_entry_image_prefix_nextentryentry) = S ((S (ssr_flat_row_prefix_nextentry)) * s)) /\ exists ff_q_pvs_prefix_nextentryentrymap. r = ff_q_pvs_prefix_nextentryentrymap * S ((S (ssr_flat_row_prefix_nextentry)) * s) + (ssr_entry_image_prefix_nextentryentry))) /\ (((((ssr_flat_column_prefix_nextentry)=(ssr_entry_image_prefix_nextentryentry)) /\ ((ssr_prefix_value_prefix_next)=(ssr_entry_value_prefix_nextentryentry)))) \/ (((~((ssr_flat_column_prefix_nextentry)=(ssr_entry_image_prefix_nextentryentry))) /\ ((ssr_prefix_value_prefix_next)=0))))))))))))))) /\ (forall dst_index_prefix_preserved dst_first_prefix_preserved dst_second_prefix_preserved. (exists pvs_gap_prefix_preservedbound. pvs_gap_prefix_preservedbound + S (dst_index_prefix_preserved) = (S l)) -> (exists dst_positive_code_prefix_preservedfirst dst_positive_scale_prefix_preservedfirst dst_negative_code_prefix_preservedfirst dst_negative_scale_prefix_preservedfirst dst_positive_prefix_preservedfirst dst_negative_prefix_preservedfirst. (((x) = (((((dst_positive_code_prefix_preservedfirst) + (dst_positive_scale_prefix_preservedfirst)) * S ((dst_positive_code_prefix_preservedfirst) + (dst_positive_scale_prefix_preservedfirst)) + ((dst_positive_scale_prefix_preservedfirst) + (dst_positive_scale_prefix_preservedfirst))) + (((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) * S ((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) + ((dst_negative_scale_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)))) * S ((((dst_positive_code_prefix_preservedfirst) + (dst_positive_scale_prefix_preservedfirst)) * S ((dst_positive_code_prefix_preservedfirst) + (dst_positive_scale_prefix_preservedfirst)) + ((dst_positive_scale_prefix_preservedfirst) + (dst_positive_scale_prefix_preservedfirst))) + (((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) * S ((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) + ((dst_negative_scale_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)))) + ((((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) * S ((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) + ((dst_negative_scale_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst))) + (((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) * S ((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) + ((dst_negative_scale_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)))))) /\ (((((exists ff_h_pvs_prefix_preservedfirstpositive. ff_h_pvs_prefix_preservedfirstpositive + S (dst_positive_prefix_preservedfirst) = S ((S (dst_index_prefix_preserved)) * dst_positive_scale_prefix_preservedfirst)) /\ exists ff_q_pvs_prefix_preservedfirstpositive. dst_positive_code_prefix_preservedfirst = ff_q_pvs_prefix_preservedfirstpositive * S ((S (dst_index_prefix_preserved)) * dst_positive_scale_prefix_preservedfirst) + (dst_positive_prefix_preservedfirst))) /\ (((((exists ff_h_pvs_prefix_preservedfirstnegative. ff_h_pvs_prefix_preservedfirstnegative + S (dst_negative_prefix_preservedfirst) = S ((S (dst_index_prefix_preserved)) * dst_negative_scale_prefix_preservedfirst)) /\ exists ff_q_pvs_prefix_preservedfirstnegative. dst_negative_code_prefix_preservedfirst = ff_q_pvs_prefix_preservedfirstnegative * S ((S (dst_index_prefix_preserved)) * dst_negative_scale_prefix_preservedfirst) + (dst_negative_prefix_preservedfirst))) /\ (exists ge_balance_positive_prefix_preservedfirstvalue ge_balance_negative_prefix_preservedfirstvalue. (((((dst_first_prefix_preserved) = 2 * (ge_balance_positive_prefix_preservedfirstvalue) /\ (ge_balance_negative_prefix_preservedfirstvalue) = 0) \/ exists ge_signed_half_prefix_preservedfirstvaluedecode. (((dst_first_prefix_preserved) = 2 * ge_signed_half_prefix_preservedfirstvaluedecode + 1 /\ (ge_balance_positive_prefix_preservedfirstvalue) = 0) /\ (ge_balance_negative_prefix_preservedfirstvalue) = S ge_signed_half_prefix_preservedfirstvaluedecode))) /\ ((dst_positive_prefix_preservedfirst) + ge_balance_negative_prefix_preservedfirstvalue = (dst_negative_prefix_preservedfirst) + ge_balance_positive_prefix_preservedfirstvalue))))))))) -> (exists dst_positive_code_prefix_preservedsecond dst_positive_scale_prefix_preservedsecond dst_negative_code_prefix_preservedsecond dst_negative_scale_prefix_preservedsecond dst_positive_prefix_preservedsecond dst_negative_prefix_preservedsecond. (((U) = (((((dst_positive_code_prefix_preservedsecond) + (dst_positive_scale_prefix_preservedsecond)) * S ((dst_positive_code_prefix_preservedsecond) + (dst_positive_scale_prefix_preservedsecond)) + ((dst_positive_scale_prefix_preservedsecond) + (dst_positive_scale_prefix_preservedsecond))) + (((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) * S ((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) + ((dst_negative_scale_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)))) * S ((((dst_positive_code_prefix_preservedsecond) + (dst_positive_scale_prefix_preservedsecond)) * S ((dst_positive_code_prefix_preservedsecond) + (dst_positive_scale_prefix_preservedsecond)) + ((dst_positive_scale_prefix_preservedsecond) + (dst_positive_scale_prefix_preservedsecond))) + (((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) * S ((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) + ((dst_negative_scale_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)))) + ((((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) * S ((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) + ((dst_negative_scale_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond))) + (((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) * S ((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) + ((dst_negative_scale_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)))))) /\ (((((exists ff_h_pvs_prefix_preservedsecondpositive. ff_h_pvs_prefix_preservedsecondpositive + S (dst_positive_prefix_preservedsecond) = S ((S (dst_index_prefix_preserved)) * dst_positive_scale_prefix_preservedsecond)) /\ exists ff_q_pvs_prefix_preservedsecondpositive. dst_positive_code_prefix_preservedsecond = ff_q_pvs_prefix_preservedsecondpositive * S ((S (dst_index_prefix_preserved)) * dst_positive_scale_prefix_preservedsecond) + (dst_positive_prefix_preservedsecond))) /\ (((((exists ff_h_pvs_prefix_preservedsecondnegative. ff_h_pvs_prefix_preservedsecondnegative + S (dst_negative_prefix_preservedsecond) = S ((S (dst_index_prefix_preserved)) * dst_negative_scale_prefix_preservedsecond)) /\ exists ff_q_pvs_prefix_preservedsecondnegative. dst_negative_code_prefix_preservedsecond = ff_q_pvs_prefix_preservedsecondnegative * S ((S (dst_index_prefix_preserved)) * dst_negative_scale_prefix_preservedsecond) + (dst_negative_prefix_preservedsecond))) /\ (exists ge_balance_positive_prefix_preservedsecondvalue ge_balance_negative_prefix_preservedsecondvalue. (((((dst_second_prefix_preserved) = 2 * (ge_balance_positive_prefix_preservedsecondvalue) /\ (ge_balance_negative_prefix_preservedsecondvalue) = 0) \/ exists ge_signed_half_prefix_preservedsecondvaluedecode. (((dst_second_prefix_preserved) = 2 * ge_signed_half_prefix_preservedsecondvaluedecode + 1 /\ (ge_balance_positive_prefix_preservedsecondvalue) = 0) /\ (ge_balance_negative_prefix_preservedsecondvalue) = S ge_signed_half_prefix_preservedsecondvaluedecode))) /\ ((dst_positive_prefix_preservedsecond) + ge_balance_negative_prefix_preservedsecondvalue = (dst_negative_prefix_preservedsecond) + ge_balance_positive_prefix_preservedsecondvalue))))))))) -> dst_first_prefix_preserved = dst_second_prefix_preserved)))
  48. 0048specialize signed_support_incidence_flat_prefix_append (A)
  49. 0049specialize signed_support_incidence_flat_prefix_append (r)
  50. 0050specialize signed_support_incidence_flat_prefix_append (s)
  51. 0051specialize signed_support_incidence_flat_prefix_append (M)
  52. 0052specialize signed_support_incidence_flat_prefix_append (l)
  53. 0053specialize signed_support_incidence_flat_prefix_append (x)
  54. 0054specialize signed_support_incidence_flat_prefix_append (x1)
  55. 0055apply signed_support_incidence_flat_prefix_append
  56. 0056exact hp_witness
  57. 0057exact hv_witness
  58. 0058cases hext
  59. 0059cases hext_witness
  60. 0060exists x2
  61. 0061exact hext_witness_left