Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Each retained summand has a witnessed n=d*q and actual signed multiplication. Zero and nondivisors contribute zero. Input and output values at zero are unrestricted; uniqueness is for positive represented values. The separate inverse family proves the unit-at-one criterion. Full G009 multiplicative-function closure is now admitted in the separate Alpha-v32 multiplicative-convolution family.
Exact theorem in conservative defined notation
∀ N. ∀ J. ∀ F. ∀ G. ∀ H. DirichletTable(N,F,G,H) → Le(J,N) → DirichletTable(J,F,G,H)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall N J F G H. (((exists dst_positive_code_table_restrict_sourceleft dst_positive_scale_table_restrict_sourceleft dst_negative_code_table_restrict_sourceleft dst_negative_scale_table_restrict_sourceleft. (((F) = (((((dst_positive_code_table_restrict_sourceleft) + (dst_positive_scale_table_restrict_sourceleft)) * S ((dst_positive_code_table_restrict_sourceleft) + (dst_positive_scale_table_restrict_sourceleft)) + ((dst_positive_scale_table_restrict_sourceleft) + (dst_positive_scale_table_restrict_sourceleft))) + (((dst_negative_code_table_restrict_sourceleft) + (dst_negative_scale_table_restrict_sourceleft)) * S ((dst_negative_code_table_restrict_sourceleft) + (dst_negative_scale_table_restrict_sourceleft)) + ((dst_negative_scale_table_restrict_sourceleft) + (dst_negative_scale_table_restrict_sourceleft)))) * S ((((dst_positive_code_table_restrict_sourceleft) + (dst_positive_scale_table_restrict_sourceleft)) * S ((dst_positive_code_table_restrict_sourceleft) + (dst_positive_scale_table_restrict_sourceleft)) + ((dst_positive_scale_table_restrict_sourceleft) + (dst_positive_scale_table_restrict_sourceleft))) + (((dst_negative_code_table_restrict_sourceleft) + (dst_negative_scale_table_restrict_sourceleft)) * S ((dst_negative_code_table_restrict_sourceleft) + (dst_negative_scale_table_restrict_sourceleft)) + ((dst_negative_scale_table_restrict_sourceleft) + (dst_negative_scale_table_restrict_sourceleft)))) + ((((dst_negative_code_table_restrict_sourceleft) + (dst_negative_scale_table_restrict_sourceleft)) * S ((dst_negative_code_table_restrict_sourceleft) + (dst_negative_scale_table_restrict_sourceleft)) + ((dst_negative_scale_table_restrict_sourceleft) + (dst_negative_scale_table_restrict_sourceleft))) + (((dst_negative_code_table_restrict_sourceleft) + (dst_negative_scale_table_restrict_sourceleft)) * S ((dst_negative_code_table_restrict_sourceleft) + (dst_negative_scale_table_restrict_sourceleft)) + ((dst_negative_scale_table_restrict_sourceleft) + (dst_negative_scale_table_restrict_sourceleft)))))) /\ (forall dst_index_table_restrict_sourceleft. (exists pvs_le_gap_table_restrict_sourceleftdomain. pvs_le_gap_table_restrict_sourceleftdomain + (dst_index_table_restrict_sourceleft) = (N)) -> exists dst_positive_table_restrict_sourceleft dst_negative_table_restrict_sourceleft dst_value_table_restrict_sourceleft. ((((exists ff_h_pvs_table_restrict_sourceleftentrypositive. ff_h_pvs_table_restrict_sourceleftentrypositive + S (dst_positive_table_restrict_sourceleft) = S ((S (dst_index_table_restrict_sourceleft)) * dst_positive_scale_table_restrict_sourceleft)) /\ exists ff_q_pvs_table_restrict_sourceleftentrypositive. dst_positive_code_table_restrict_sourceleft = ff_q_pvs_table_restrict_sourceleftentrypositive * S ((S (dst_index_table_restrict_sourceleft)) * dst_positive_scale_table_restrict_sourceleft) + (dst_positive_table_restrict_sourceleft))) /\ (((((exists ff_h_pvs_table_restrict_sourceleftentrynegative. ff_h_pvs_table_restrict_sourceleftentrynegative + S (dst_negative_table_restrict_sourceleft) = S ((S (dst_index_table_restrict_sourceleft)) * dst_negative_scale_table_restrict_sourceleft)) /\ exists ff_q_pvs_table_restrict_sourceleftentrynegative. dst_negative_code_table_restrict_sourceleft = ff_q_pvs_table_restrict_sourceleftentrynegative * S ((S (dst_index_table_restrict_sourceleft)) * dst_negative_scale_table_restrict_sourceleft) + (dst_negative_table_restrict_sourceleft))) /\ (exists ge_balance_positive_table_restrict_sourceleftentryvalue ge_balance_negative_table_restrict_sourceleftentryvalue. (((((dst_value_table_restrict_sourceleft) = 2 * (ge_balance_positive_table_restrict_sourceleftentryvalue) /\ (ge_balance_negative_table_restrict_sourceleftentryvalue) = 0) \/ exists ge_signed_half_table_restrict_sourceleftentryvaluedecode. (((dst_value_table_restrict_sourceleft) = 2 * ge_signed_half_table_restrict_sourceleftentryvaluedecode + 1 /\ (ge_balance_positive_table_restrict_sourceleftentryvalue) = 0) /\ (ge_balance_negative_table_restrict_sourceleftentryvalue) = S ge_signed_half_table_restrict_sourceleftentryvaluedecode))) /\ ((dst_positive_table_restrict_sourceleft) + ge_balance_negative_table_restrict_sourceleftentryvalue = (dst_negative_table_restrict_sourceleft) + ge_balance_positive_table_restrict_sourceleftentryvalue))))))))) /\ (((exists dst_positive_code_table_restrict_sourceright dst_positive_scale_table_restrict_sourceright dst_negative_code_table_restrict_sourceright dst_negative_scale_table_restrict_sourceright. (((G) = (((((dst_positive_code_table_restrict_sourceright) + (dst_positive_scale_table_restrict_sourceright)) * S ((dst_positive_code_table_restrict_sourceright) + (dst_positive_scale_table_restrict_sourceright)) + ((dst_positive_scale_table_restrict_sourceright) + (dst_positive_scale_table_restrict_sourceright))) + (((dst_negative_code_table_restrict_sourceright) + (dst_negative_scale_table_restrict_sourceright)) * S ((dst_negative_code_table_restrict_sourceright) + (dst_negative_scale_table_restrict_sourceright)) + ((dst_negative_scale_table_restrict_sourceright) + (dst_negative_scale_table_restrict_sourceright)))) * S ((((dst_positive_code_table_restrict_sourceright) + (dst_positive_scale_table_restrict_sourceright)) * S ((dst_positive_code_table_restrict_sourceright) + (dst_positive_scale_table_restrict_sourceright)) + ((dst_positive_scale_table_restrict_sourceright) + (dst_positive_scale_table_restrict_sourceright))) + (((dst_negative_code_table_restrict_sourceright) + (dst_negative_scale_table_restrict_sourceright)) * S ((dst_negative_code_table_restrict_sourceright) + (dst_negative_scale_table_restrict_sourceright)) + ((dst_negative_scale_table_restrict_sourceright) + (dst_negative_scale_table_restrict_sourceright)))) + ((((dst_negative_code_table_restrict_sourceright) + (dst_negative_scale_table_restrict_sourceright)) * S ((dst_negative_code_table_restrict_sourceright) + (dst_negative_scale_table_restrict_sourceright)) + ((dst_negative_scale_table_restrict_sourceright) + (dst_negative_scale_table_restrict_sourceright))) + (((dst_negative_code_table_restrict_sourceright) + (dst_negative_scale_table_restrict_sourceright)) * S ((dst_negative_code_table_restrict_sourceright) + (dst_negative_scale_table_restrict_sourceright)) + ((dst_negative_scale_table_restrict_sourceright) + (dst_negative_scale_table_restrict_sourceright)))))) /\ (forall dst_index_table_restrict_sourceright. (exists pvs_le_gap_table_restrict_sourcerightdomain. pvs_le_gap_table_restrict_sourcerightdomain + (dst_index_table_restrict_sourceright) = (N)) -> exists dst_positive_table_restrict_sourceright dst_negative_table_restrict_sourceright dst_value_table_restrict_sourceright. ((((exists ff_h_pvs_table_restrict_sourcerightentrypositive. ff_h_pvs_table_restrict_sourcerightentrypositive + S (dst_positive_table_restrict_sourceright) = S ((S (dst_index_table_restrict_sourceright)) * dst_positive_scale_table_restrict_sourceright)) /\ exists ff_q_pvs_table_restrict_sourcerightentrypositive. dst_positive_code_table_restrict_sourceright = ff_q_pvs_table_restrict_sourcerightentrypositive * S ((S (dst_index_table_restrict_sourceright)) * dst_positive_scale_table_restrict_sourceright) + (dst_positive_table_restrict_sourceright))) /\ (((((exists ff_h_pvs_table_restrict_sourcerightentrynegative. ff_h_pvs_table_restrict_sourcerightentrynegative + S (dst_negative_table_restrict_sourceright) = S ((S (dst_index_table_restrict_sourceright)) * dst_negative_scale_table_restrict_sourceright)) /\ exists ff_q_pvs_table_restrict_sourcerightentrynegative. dst_negative_code_table_restrict_sourceright = ff_q_pvs_table_restrict_sourcerightentrynegative * S ((S (dst_index_table_restrict_sourceright)) * dst_negative_scale_table_restrict_sourceright) + (dst_negative_table_restrict_sourceright))) /\ (exists ge_balance_positive_table_restrict_sourcerightentryvalue ge_balance_negative_table_restrict_sourcerightentryvalue. (((((dst_value_table_restrict_sourceright) = 2 * (ge_balance_positive_table_restrict_sourcerightentryvalue) /\ (ge_balance_negative_table_restrict_sourcerightentryvalue) = 0) \/ exists ge_signed_half_table_restrict_sourcerightentryvaluedecode. (((dst_value_table_restrict_sourceright) = 2 * ge_signed_half_table_restrict_sourcerightentryvaluedecode + 1 /\ (ge_balance_positive_table_restrict_sourcerightentryvalue) = 0) /\ (ge_balance_negative_table_restrict_sourcerightentryvalue) = S ge_signed_half_table_restrict_sourcerightentryvaluedecode))) /\ ((dst_positive_table_restrict_sourceright) + ge_balance_negative_table_restrict_sourcerightentryvalue = (dst_negative_table_restrict_sourceright) + ge_balance_positive_table_restrict_sourcerightentryvalue))))))))) /\ (((exists dst_positive_code_table_restrict_sourcetable dst_positive_scale_table_restrict_sourcetable dst_negative_code_table_restrict_sourcetable dst_negative_scale_table_restrict_sourcetable. (((H) = (((((dst_positive_code_table_restrict_sourcetable) + (dst_positive_scale_table_restrict_sourcetable)) * S ((dst_positive_code_table_restrict_sourcetable) + (dst_positive_scale_table_restrict_sourcetable)) + ((dst_positive_scale_table_restrict_sourcetable) + (dst_positive_scale_table_restrict_sourcetable))) + (((dst_negative_code_table_restrict_sourcetable) + (dst_negative_scale_table_restrict_sourcetable)) * S ((dst_negative_code_table_restrict_sourcetable) + (dst_negative_scale_table_restrict_sourcetable)) + ((dst_negative_scale_table_restrict_sourcetable) + (dst_negative_scale_table_restrict_sourcetable)))) * S ((((dst_positive_code_table_restrict_sourcetable) + (dst_positive_scale_table_restrict_sourcetable)) * S ((dst_positive_code_table_restrict_sourcetable) + (dst_positive_scale_table_restrict_sourcetable)) + ((dst_positive_scale_table_restrict_sourcetable) + (dst_positive_scale_table_restrict_sourcetable))) + (((dst_negative_code_table_restrict_sourcetable) + (dst_negative_scale_table_restrict_sourcetable)) * S ((dst_negative_code_table_restrict_sourcetable) + (dst_negative_scale_table_restrict_sourcetable)) + ((dst_negative_scale_table_restrict_sourcetable) + (dst_negative_scale_table_restrict_sourcetable)))) + ((((dst_negative_code_table_restrict_sourcetable) + (dst_negative_scale_table_restrict_sourcetable)) * S ((dst_negative_code_table_restrict_sourcetable) + (dst_negative_scale_table_restrict_sourcetable)) + ((dst_negative_scale_table_restrict_sourcetable) + (dst_negative_scale_table_restrict_sourcetable))) + (((dst_negative_code_table_restrict_sourcetable) + (dst_negative_scale_table_restrict_sourcetable)) * S ((dst_negative_code_table_restrict_sourcetable) + (dst_negative_scale_table_restrict_sourcetable)) + ((dst_negative_scale_table_restrict_sourcetable) + (dst_negative_scale_table_restrict_sourcetable)))))) /\ (forall dst_index_table_restrict_sourcetable. (exists pvs_le_gap_table_restrict_sourcetabledomain. pvs_le_gap_table_restrict_sourcetabledomain + (dst_index_table_restrict_sourcetable) = (N)) -> exists dst_positive_table_restrict_sourcetable dst_negative_table_restrict_sourcetable dst_value_table_restrict_sourcetable. ((((exists ff_h_pvs_table_restrict_sourcetableentrypositive. ff_h_pvs_table_restrict_sourcetableentrypositive + S (dst_positive_table_restrict_sourcetable) = S ((S (dst_index_table_restrict_sourcetable)) * dst_positive_scale_table_restrict_sourcetable)) /\ exists ff_q_pvs_table_restrict_sourcetableentrypositive. dst_positive_code_table_restrict_sourcetable = ff_q_pvs_table_restrict_sourcetableentrypositive * S ((S (dst_index_table_restrict_sourcetable)) * dst_positive_scale_table_restrict_sourcetable) + (dst_positive_table_restrict_sourcetable))) /\ (((((exists ff_h_pvs_table_restrict_sourcetableentrynegative. ff_h_pvs_table_restrict_sourcetableentrynegative + S (dst_negative_table_restrict_sourcetable) = S ((S (dst_index_table_restrict_sourcetable)) * dst_negative_scale_table_restrict_sourcetable)) /\ exists ff_q_pvs_table_restrict_sourcetableentrynegative. dst_negative_code_table_restrict_sourcetable = ff_q_pvs_table_restrict_sourcetableentrynegative * S ((S (dst_index_table_restrict_sourcetable)) * dst_negative_scale_table_restrict_sourcetable) + (dst_negative_table_restrict_sourcetable))) /\ (exists ge_balance_positive_table_restrict_sourcetableentryvalue ge_balance_negative_table_restrict_sourcetableentryvalue. (((((dst_value_table_restrict_sourcetable) = 2 * (ge_balance_positive_table_restrict_sourcetableentryvalue) /\ (ge_balance_negative_table_restrict_sourcetableentryvalue) = 0) \/ exists ge_signed_half_table_restrict_sourcetableentryvaluedecode. (((dst_value_table_restrict_sourcetable) = 2 * ge_signed_half_table_restrict_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_table_restrict_sourcetableentryvalue) = 0) /\ (ge_balance_negative_table_restrict_sourcetableentryvalue) = S ge_signed_half_table_restrict_sourcetableentryvaluedecode))) /\ ((dst_positive_table_restrict_sourcetable) + ge_balance_negative_table_restrict_sourcetableentryvalue = (dst_negative_table_restrict_sourcetable) + ge_balance_positive_table_restrict_sourcetableentryvalue))))))))) /\ (forall dc_input_table_restrict_source dc_output_table_restrict_source. ~(dc_input_table_restrict_source=0) -> (exists pvs_le_gap_table_restrict_sourcedomain. pvs_le_gap_table_restrict_sourcedomain + (dc_input_table_restrict_source) = (N)) -> (exists dst_positive_code_table_restrict_sourcelookup dst_positive_scale_table_restrict_sourcelookup dst_negative_code_table_restrict_sourcelookup dst_negative_scale_table_restrict_sourcelookup dst_positive_table_restrict_sourcelookup dst_negative_table_restrict_sourcelookup. (((H) = (((((dst_positive_code_table_restrict_sourcelookup) + (dst_positive_scale_table_restrict_sourcelookup)) * S ((dst_positive_code_table_restrict_sourcelookup) + (dst_positive_scale_table_restrict_sourcelookup)) + ((dst_positive_scale_table_restrict_sourcelookup) + (dst_positive_scale_table_restrict_sourcelookup))) + (((dst_negative_code_table_restrict_sourcelookup) + (dst_negative_scale_table_restrict_sourcelookup)) * S ((dst_negative_code_table_restrict_sourcelookup) + (dst_negative_scale_table_restrict_sourcelookup)) + ((dst_negative_scale_table_restrict_sourcelookup) + (dst_negative_scale_table_restrict_sourcelookup)))) * S ((((dst_positive_code_table_restrict_sourcelookup) + (dst_positive_scale_table_restrict_sourcelookup)) * S ((dst_positive_code_table_restrict_sourcelookup) + (dst_positive_scale_table_restrict_sourcelookup)) + ((dst_positive_scale_table_restrict_sourcelookup) + (dst_positive_scale_table_restrict_sourcelookup))) + (((dst_negative_code_table_restrict_sourcelookup) + (dst_negative_scale_table_restrict_sourcelookup)) * S ((dst_negative_code_table_restrict_sourcelookup) + (dst_negative_scale_table_restrict_sourcelookup)) + ((dst_negative_scale_table_restrict_sourcelookup) + (dst_negative_scale_table_restrict_sourcelookup)))) + ((((dst_negative_code_table_restrict_sourcelookup) + (dst_negative_scale_table_restrict_sourcelookup)) * S ((dst_negative_code_table_restrict_sourcelookup) + (dst_negative_scale_table_restrict_sourcelookup)) + ((dst_negative_scale_table_restrict_sourcelookup) + (dst_negative_scale_table_restrict_sourcelookup))) + (((dst_negative_code_table_restrict_sourcelookup) + (dst_negative_scale_table_restrict_sourcelookup)) * S ((dst_negative_code_table_restrict_sourcelookup) + (dst_negative_scale_table_restrict_sourcelookup)) + ((dst_negative_scale_table_restrict_sourcelookup) + (dst_negative_scale_table_restrict_sourcelookup)))))) /\ (((((exists ff_h_pvs_table_restrict_sourcelookuppositive. ff_h_pvs_table_restrict_sourcelookuppositive + S (dst_positive_table_restrict_sourcelookup) = S ((S (dc_input_table_restrict_source)) * dst_positive_scale_table_restrict_sourcelookup)) /\ exists ff_q_pvs_table_restrict_sourcelookuppositive. dst_positive_code_table_restrict_sourcelookup = ff_q_pvs_table_restrict_sourcelookuppositive * S ((S (dc_input_table_restrict_source)) * dst_positive_scale_table_restrict_sourcelookup) + (dst_positive_table_restrict_sourcelookup))) /\ (((((exists ff_h_pvs_table_restrict_sourcelookupnegative. ff_h_pvs_table_restrict_sourcelookupnegative + S (dst_negative_table_restrict_sourcelookup) = S ((S (dc_input_table_restrict_source)) * dst_negative_scale_table_restrict_sourcelookup)) /\ exists ff_q_pvs_table_restrict_sourcelookupnegative. dst_negative_code_table_restrict_sourcelookup = ff_q_pvs_table_restrict_sourcelookupnegative * S ((S (dc_input_table_restrict_source)) * dst_negative_scale_table_restrict_sourcelookup) + (dst_negative_table_restrict_sourcelookup))) /\ (exists ge_balance_positive_table_restrict_sourcelookupvalue ge_balance_negative_table_restrict_sourcelookupvalue. (((((dc_output_table_restrict_source) = 2 * (ge_balance_positive_table_restrict_sourcelookupvalue) /\ (ge_balance_negative_table_restrict_sourcelookupvalue) = 0) \/ exists ge_signed_half_table_restrict_sourcelookupvaluedecode. (((dc_output_table_restrict_source) = 2 * ge_signed_half_table_restrict_sourcelookupvaluedecode + 1 /\ (ge_balance_positive_table_restrict_sourcelookupvalue) = 0) /\ (ge_balance_negative_table_restrict_sourcelookupvalue) = S ge_signed_half_table_restrict_sourcelookupvaluedecode))) /\ ((dst_positive_table_restrict_sourcelookup) + ge_balance_negative_table_restrict_sourcelookupvalue = (dst_negative_table_restrict_sourcelookup) + ge_balance_positive_table_restrict_sourcelookupvalue))))))))) -> (((~((dc_input_table_restrict_source)=0)) /\ (exists dc_mask_table_restrict_sourcevalue. ((((exists dst_positive_code_table_restrict_sourcevaluemasktable dst_positive_scale_table_restrict_sourcevaluemasktable dst_negative_code_table_restrict_sourcevaluemasktable dst_negative_scale_table_restrict_sourcevaluemasktable. (((dc_mask_table_restrict_sourcevalue) = (((((dst_positive_code_table_restrict_sourcevaluemasktable) + (dst_positive_scale_table_restrict_sourcevaluemasktable)) * S ((dst_positive_code_table_restrict_sourcevaluemasktable) + (dst_positive_scale_table_restrict_sourcevaluemasktable)) + ((dst_positive_scale_table_restrict_sourcevaluemasktable) + (dst_positive_scale_table_restrict_sourcevaluemasktable))) + (((dst_negative_code_table_restrict_sourcevaluemasktable) + (dst_negative_scale_table_restrict_sourcevaluemasktable)) * S ((dst_negative_code_table_restrict_sourcevaluemasktable) + (dst_negative_scale_table_restrict_sourcevaluemasktable)) + ((dst_negative_scale_table_restrict_sourcevaluemasktable) + (dst_negative_scale_table_restrict_sourcevaluemasktable)))) * S ((((dst_positive_code_table_restrict_sourcevaluemasktable) + (dst_positive_scale_table_restrict_sourcevaluemasktable)) * S ((dst_positive_code_table_restrict_sourcevaluemasktable) + (dst_positive_scale_table_restrict_sourcevaluemasktable)) + ((dst_positive_scale_table_restrict_sourcevaluemasktable) + (dst_positive_scale_table_restrict_sourcevaluemasktable))) + (((dst_negative_code_table_restrict_sourcevaluemasktable) + (dst_negative_scale_table_restrict_sourcevaluemasktable)) * S ((dst_negative_code_table_restrict_sourcevaluemasktable) + (dst_negative_scale_table_restrict_sourcevaluemasktable)) + ((dst_negative_scale_table_restrict_sourcevaluemasktable) + (dst_negative_scale_table_restrict_sourcevaluemasktable)))) + ((((dst_negative_code_table_restrict_sourcevaluemasktable) + (dst_negative_scale_table_restrict_sourcevaluemasktable)) * S ((dst_negative_code_table_restrict_sourcevaluemasktable) + (dst_negative_scale_table_restrict_sourcevaluemasktable)) + ((dst_negative_scale_table_restrict_sourcevaluemasktable) + (dst_negative_scale_table_restrict_sourcevaluemasktable))) + (((dst_negative_code_table_restrict_sourcevaluemasktable) + (dst_negative_scale_table_restrict_sourcevaluemasktable)) * S ((dst_negative_code_table_restrict_sourcevaluemasktable) + (dst_negative_scale_table_restrict_sourcevaluemasktable)) + ((dst_negative_scale_table_restrict_sourcevaluemasktable) + (dst_negative_scale_table_restrict_sourcevaluemasktable)))))) /\ (forall dst_index_table_restrict_sourcevaluemasktable. (exists pvs_le_gap_table_restrict_sourcevaluemasktabledomain. pvs_le_gap_table_restrict_sourcevaluemasktabledomain + (dst_index_table_restrict_sourcevaluemasktable) = (dc_input_table_restrict_source)) -> exists dst_positive_table_restrict_sourcevaluemasktable dst_negative_table_restrict_sourcevaluemasktable dst_value_table_restrict_sourcevaluemasktable. ((((exists ff_h_pvs_table_restrict_sourcevaluemasktableentrypositive. ff_h_pvs_table_restrict_sourcevaluemasktableentrypositive + S (dst_positive_table_restrict_sourcevaluemasktable) = S ((S (dst_index_table_restrict_sourcevaluemasktable)) * dst_positive_scale_table_restrict_sourcevaluemasktable)) /\ exists ff_q_pvs_table_restrict_sourcevaluemasktableentrypositive. dst_positive_code_table_restrict_sourcevaluemasktable = ff_q_pvs_table_restrict_sourcevaluemasktableentrypositive * S ((S (dst_index_table_restrict_sourcevaluemasktable)) * dst_positive_scale_table_restrict_sourcevaluemasktable) + (dst_positive_table_restrict_sourcevaluemasktable))) /\ (((((exists ff_h_pvs_table_restrict_sourcevaluemasktableentrynegative. ff_h_pvs_table_restrict_sourcevaluemasktableentrynegative + S (dst_negative_table_restrict_sourcevaluemasktable) = S ((S (dst_index_table_restrict_sourcevaluemasktable)) * dst_negative_scale_table_restrict_sourcevaluemasktable)) /\ exists ff_q_pvs_table_restrict_sourcevaluemasktableentrynegative. dst_negative_code_table_restrict_sourcevaluemasktable = ff_q_pvs_table_restrict_sourcevaluemasktableentrynegative * S ((S (dst_index_table_restrict_sourcevaluemasktable)) * dst_negative_scale_table_restrict_sourcevaluemasktable) + (dst_negative_table_restrict_sourcevaluemasktable))) /\ (exists ge_balance_positive_table_restrict_sourcevaluemasktableentryvalue ge_balance_negative_table_restrict_sourcevaluemasktableentryvalue. (((((dst_value_table_restrict_sourcevaluemasktable) = 2 * (ge_balance_positive_table_restrict_sourcevaluemasktableentryvalue) /\ (ge_balance_negative_table_restrict_sourcevaluemasktableentryvalue) = 0) \/ exists ge_signed_half_table_restrict_sourcevaluemasktableentryvaluedecode. (((dst_value_table_restrict_sourcevaluemasktable) = 2 * ge_signed_half_table_restrict_sourcevaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_table_restrict_sourcevaluemasktableentryvalue) = 0) /\ (ge_balance_negative_table_restrict_sourcevaluemasktableentryvalue) = S ge_signed_half_table_restrict_sourcevaluemasktableentryvaluedecode))) /\ ((dst_positive_table_restrict_sourcevaluemasktable) + ge_balance_negative_table_restrict_sourcevaluemasktableentryvalue = (dst_negative_table_restrict_sourcevaluemasktable) + ge_balance_positive_table_restrict_sourcevaluemasktableentryvalue))))))))) /\ (forall dc_index_table_restrict_sourcevaluemask dc_value_table_restrict_sourcevaluemask. (exists pvs_le_gap_table_restrict_sourcevaluemaskdomain. pvs_le_gap_table_restrict_sourcevaluemaskdomain + (dc_index_table_restrict_sourcevaluemask) = (dc_input_table_restrict_source)) -> (exists dst_positive_code_table_restrict_sourcevaluemasklookup dst_positive_scale_table_restrict_sourcevaluemasklookup dst_negative_code_table_restrict_sourcevaluemasklookup dst_negative_scale_table_restrict_sourcevaluemasklookup dst_positive_table_restrict_sourcevaluemasklookup dst_negative_table_restrict_sourcevaluemasklookup. (((dc_mask_table_restrict_sourcevalue) = (((((dst_positive_code_table_restrict_sourcevaluemasklookup) + (dst_positive_scale_table_restrict_sourcevaluemasklookup)) * S ((dst_positive_code_table_restrict_sourcevaluemasklookup) + (dst_positive_scale_table_restrict_sourcevaluemasklookup)) + ((dst_positive_scale_table_restrict_sourcevaluemasklookup) + (dst_positive_scale_table_restrict_sourcevaluemasklookup))) + (((dst_negative_code_table_restrict_sourcevaluemasklookup) + (dst_negative_scale_table_restrict_sourcevaluemasklookup)) * S ((dst_negative_code_table_restrict_sourcevaluemasklookup) + (dst_negative_scale_table_restrict_sourcevaluemasklookup)) + ((dst_negative_scale_table_restrict_sourcevaluemasklookup) + (dst_negative_scale_table_restrict_sourcevaluemasklookup)))) * S ((((dst_positive_code_table_restrict_sourcevaluemasklookup) + (dst_positive_scale_table_restrict_sourcevaluemasklookup)) * S ((dst_positive_code_table_restrict_sourcevaluemasklookup) + (dst_positive_scale_table_restrict_sourcevaluemasklookup)) + ((dst_positive_scale_table_restrict_sourcevaluemasklookup) + (dst_positive_scale_table_restrict_sourcevaluemasklookup))) + (((dst_negative_code_table_restrict_sourcevaluemasklookup) + (dst_negative_scale_table_restrict_sourcevaluemasklookup)) * S ((dst_negative_code_table_restrict_sourcevaluemasklookup) + (dst_negative_scale_table_restrict_sourcevaluemasklookup)) + ((dst_negative_scale_table_restrict_sourcevaluemasklookup) + (dst_negative_scale_table_restrict_sourcevaluemasklookup)))) + ((((dst_negative_code_table_restrict_sourcevaluemasklookup) + (dst_negative_scale_table_restrict_sourcevaluemasklookup)) * S ((dst_negative_code_table_restrict_sourcevaluemasklookup) + (dst_negative_scale_table_restrict_sourcevaluemasklookup)) + ((dst_negative_scale_table_restrict_sourcevaluemasklookup) + (dst_negative_scale_table_restrict_sourcevaluemasklookup))) + (((dst_negative_code_table_restrict_sourcevaluemasklookup) + (dst_negative_scale_table_restrict_sourcevaluemasklookup)) * S ((dst_negative_code_table_restrict_sourcevaluemasklookup) + (dst_negative_scale_table_restrict_sourcevaluemasklookup)) + ((dst_negative_scale_table_restrict_sourcevaluemasklookup) + (dst_negative_scale_table_restrict_sourcevaluemasklookup)))))) /\ (((((exists ff_h_pvs_table_restrict_sourcevaluemasklookuppositive. ff_h_pvs_table_restrict_sourcevaluemasklookuppositive + S (dst_positive_table_restrict_sourcevaluemasklookup) = S ((S (dc_index_table_restrict_sourcevaluemask)) * dst_positive_scale_table_restrict_sourcevaluemasklookup)) /\ exists ff_q_pvs_table_restrict_sourcevaluemasklookuppositive. dst_positive_code_table_restrict_sourcevaluemasklookup = ff_q_pvs_table_restrict_sourcevaluemasklookuppositive * S ((S (dc_index_table_restrict_sourcevaluemask)) * dst_positive_scale_table_restrict_sourcevaluemasklookup) + (dst_positive_table_restrict_sourcevaluemasklookup))) /\ (((((exists ff_h_pvs_table_restrict_sourcevaluemasklookupnegative. ff_h_pvs_table_restrict_sourcevaluemasklookupnegative + S (dst_negative_table_restrict_sourcevaluemasklookup) = S ((S (dc_index_table_restrict_sourcevaluemask)) * dst_negative_scale_table_restrict_sourcevaluemasklookup)) /\ exists ff_q_pvs_table_restrict_sourcevaluemasklookupnegative. dst_negative_code_table_restrict_sourcevaluemasklookup = ff_q_pvs_table_restrict_sourcevaluemasklookupnegative * S ((S (dc_index_table_restrict_sourcevaluemask)) * dst_negative_scale_table_restrict_sourcevaluemasklookup) + (dst_negative_table_restrict_sourcevaluemasklookup))) /\ (exists ge_balance_positive_table_restrict_sourcevaluemasklookupvalue ge_balance_negative_table_restrict_sourcevaluemasklookupvalue. (((((dc_value_table_restrict_sourcevaluemask) = 2 * (ge_balance_positive_table_restrict_sourcevaluemasklookupvalue) /\ (ge_balance_negative_table_restrict_sourcevaluemasklookupvalue) = 0) \/ exists ge_signed_half_table_restrict_sourcevaluemasklookupvaluedecode. (((dc_value_table_restrict_sourcevaluemask) = 2 * ge_signed_half_table_restrict_sourcevaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_table_restrict_sourcevaluemasklookupvalue) = 0) /\ (ge_balance_negative_table_restrict_sourcevaluemasklookupvalue) = S ge_signed_half_table_restrict_sourcevaluemasklookupvaluedecode))) /\ ((dst_positive_table_restrict_sourcevaluemasklookup) + ge_balance_negative_table_restrict_sourcevaluemasklookupvalue = (dst_negative_table_restrict_sourcevaluemasklookup) + ge_balance_positive_table_restrict_sourcevaluemasklookupvalue))))))))) -> ((((~((dc_index_table_restrict_sourcevaluemask)=0)) /\ (exists dc_quotient_table_restrict_sourcevaluemaskentry dc_left_table_restrict_sourcevaluemaskentry dc_right_table_restrict_sourcevaluemaskentry. (((dc_input_table_restrict_source)=(dc_index_table_restrict_sourcevaluemask)*dc_quotient_table_restrict_sourcevaluemaskentry) /\ (((exists dst_positive_code_table_restrict_sourcevaluemaskentryleft dst_positive_scale_table_restrict_sourcevaluemaskentryleft dst_negative_code_table_restrict_sourcevaluemaskentryleft dst_negative_scale_table_restrict_sourcevaluemaskentryleft dst_positive_table_restrict_sourcevaluemaskentryleft dst_negative_table_restrict_sourcevaluemaskentryleft. (((F) = (((((dst_positive_code_table_restrict_sourcevaluemaskentryleft) + (dst_positive_scale_table_restrict_sourcevaluemaskentryleft)) * S ((dst_positive_code_table_restrict_sourcevaluemaskentryleft) + (dst_positive_scale_table_restrict_sourcevaluemaskentryleft)) + ((dst_positive_scale_table_restrict_sourcevaluemaskentryleft) + (dst_positive_scale_table_restrict_sourcevaluemaskentryleft))) + (((dst_negative_code_table_restrict_sourcevaluemaskentryleft) + (dst_negative_scale_table_restrict_sourcevaluemaskentryleft)) * S ((dst_negative_code_table_restrict_sourcevaluemaskentryleft) + (dst_negative_scale_table_restrict_sourcevaluemaskentryleft)) + ((dst_negative_scale_table_restrict_sourcevaluemaskentryleft) + (dst_negative_scale_table_restrict_sourcevaluemaskentryleft)))) * S ((((dst_positive_code_table_restrict_sourcevaluemaskentryleft) + (dst_positive_scale_table_restrict_sourcevaluemaskentryleft)) * S ((dst_positive_code_table_restrict_sourcevaluemaskentryleft) + (dst_positive_scale_table_restrict_sourcevaluemaskentryleft)) + ((dst_positive_scale_table_restrict_sourcevaluemaskentryleft) + (dst_positive_scale_table_restrict_sourcevaluemaskentryleft))) + (((dst_negative_code_table_restrict_sourcevaluemaskentryleft) + (dst_negative_scale_table_restrict_sourcevaluemaskentryleft)) * S ((dst_negative_code_table_restrict_sourcevaluemaskentryleft) + (dst_negative_scale_table_restrict_sourcevaluemaskentryleft)) + ((dst_negative_scale_table_restrict_sourcevaluemaskentryleft) + (dst_negative_scale_table_restrict_sourcevaluemaskentryleft)))) + ((((dst_negative_code_table_restrict_sourcevaluemaskentryleft) + (dst_negative_scale_table_restrict_sourcevaluemaskentryleft)) * S ((dst_negative_code_table_restrict_sourcevaluemaskentryleft) + (dst_negative_scale_table_restrict_sourcevaluemaskentryleft)) + ((dst_negative_scale_table_restrict_sourcevaluemaskentryleft) + (dst_negative_scale_table_restrict_sourcevaluemaskentryleft))) + (((dst_negative_code_table_restrict_sourcevaluemaskentryleft) + (dst_negative_scale_table_restrict_sourcevaluemaskentryleft)) * S ((dst_negative_code_table_restrict_sourcevaluemaskentryleft) + (dst_negative_scale_table_restrict_sourcevaluemaskentryleft)) + ((dst_negative_scale_table_restrict_sourcevaluemaskentryleft) + (dst_negative_scale_table_restrict_sourcevaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_table_restrict_sourcevaluemaskentryleftpositive. ff_h_pvs_table_restrict_sourcevaluemaskentryleftpositive + S (dst_positive_table_restrict_sourcevaluemaskentryleft) = S ((S (dc_index_table_restrict_sourcevaluemask)) * dst_positive_scale_table_restrict_sourcevaluemaskentryleft)) /\ exists ff_q_pvs_table_restrict_sourcevaluemaskentryleftpositive. dst_positive_code_table_restrict_sourcevaluemaskentryleft = ff_q_pvs_table_restrict_sourcevaluemaskentryleftpositive * S ((S (dc_index_table_restrict_sourcevaluemask)) * dst_positive_scale_table_restrict_sourcevaluemaskentryleft) + (dst_positive_table_restrict_sourcevaluemaskentryleft))) /\ (((((exists ff_h_pvs_table_restrict_sourcevaluemaskentryleftnegative. ff_h_pvs_table_restrict_sourcevaluemaskentryleftnegative + S (dst_negative_table_restrict_sourcevaluemaskentryleft) = S ((S (dc_index_table_restrict_sourcevaluemask)) * dst_negative_scale_table_restrict_sourcevaluemaskentryleft)) /\ exists ff_q_pvs_table_restrict_sourcevaluemaskentryleftnegative. dst_negative_code_table_restrict_sourcevaluemaskentryleft = ff_q_pvs_table_restrict_sourcevaluemaskentryleftnegative * S ((S (dc_index_table_restrict_sourcevaluemask)) * dst_negative_scale_table_restrict_sourcevaluemaskentryleft) + (dst_negative_table_restrict_sourcevaluemaskentryleft))) /\ (exists ge_balance_positive_table_restrict_sourcevaluemaskentryleftvalue ge_balance_negative_table_restrict_sourcevaluemaskentryleftvalue. (((((dc_left_table_restrict_sourcevaluemaskentry) = 2 * (ge_balance_positive_table_restrict_sourcevaluemaskentryleftvalue) /\ (ge_balance_negative_table_restrict_sourcevaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_table_restrict_sourcevaluemaskentryleftvaluedecode. (((dc_left_table_restrict_sourcevaluemaskentry) = 2 * ge_signed_half_table_restrict_sourcevaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_table_restrict_sourcevaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_table_restrict_sourcevaluemaskentryleftvalue) = S ge_signed_half_table_restrict_sourcevaluemaskentryleftvaluedecode))) /\ ((dst_positive_table_restrict_sourcevaluemaskentryleft) + ge_balance_negative_table_restrict_sourcevaluemaskentryleftvalue = (dst_negative_table_restrict_sourcevaluemaskentryleft) + ge_balance_positive_table_restrict_sourcevaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_table_restrict_sourcevaluemaskentryright dst_positive_scale_table_restrict_sourcevaluemaskentryright dst_negative_code_table_restrict_sourcevaluemaskentryright dst_negative_scale_table_restrict_sourcevaluemaskentryright dst_positive_table_restrict_sourcevaluemaskentryright dst_negative_table_restrict_sourcevaluemaskentryright. (((G) = (((((dst_positive_code_table_restrict_sourcevaluemaskentryright) + (dst_positive_scale_table_restrict_sourcevaluemaskentryright)) * S ((dst_positive_code_table_restrict_sourcevaluemaskentryright) + (dst_positive_scale_table_restrict_sourcevaluemaskentryright)) + ((dst_positive_scale_table_restrict_sourcevaluemaskentryright) + (dst_positive_scale_table_restrict_sourcevaluemaskentryright))) + (((dst_negative_code_table_restrict_sourcevaluemaskentryright) + (dst_negative_scale_table_restrict_sourcevaluemaskentryright)) * S ((dst_negative_code_table_restrict_sourcevaluemaskentryright) + (dst_negative_scale_table_restrict_sourcevaluemaskentryright)) + ((dst_negative_scale_table_restrict_sourcevaluemaskentryright) + (dst_negative_scale_table_restrict_sourcevaluemaskentryright)))) * S ((((dst_positive_code_table_restrict_sourcevaluemaskentryright) + (dst_positive_scale_table_restrict_sourcevaluemaskentryright)) * S ((dst_positive_code_table_restrict_sourcevaluemaskentryright) + (dst_positive_scale_table_restrict_sourcevaluemaskentryright)) + ((dst_positive_scale_table_restrict_sourcevaluemaskentryright) + (dst_positive_scale_table_restrict_sourcevaluemaskentryright))) + (((dst_negative_code_table_restrict_sourcevaluemaskentryright) + (dst_negative_scale_table_restrict_sourcevaluemaskentryright)) * S ((dst_negative_code_table_restrict_sourcevaluemaskentryright) + (dst_negative_scale_table_restrict_sourcevaluemaskentryright)) + ((dst_negative_scale_table_restrict_sourcevaluemaskentryright) + (dst_negative_scale_table_restrict_sourcevaluemaskentryright)))) + ((((dst_negative_code_table_restrict_sourcevaluemaskentryright) + (dst_negative_scale_table_restrict_sourcevaluemaskentryright)) * S ((dst_negative_code_table_restrict_sourcevaluemaskentryright) + (dst_negative_scale_table_restrict_sourcevaluemaskentryright)) + ((dst_negative_scale_table_restrict_sourcevaluemaskentryright) + (dst_negative_scale_table_restrict_sourcevaluemaskentryright))) + (((dst_negative_code_table_restrict_sourcevaluemaskentryright) + (dst_negative_scale_table_restrict_sourcevaluemaskentryright)) * S ((dst_negative_code_table_restrict_sourcevaluemaskentryright) + (dst_negative_scale_table_restrict_sourcevaluemaskentryright)) + ((dst_negative_scale_table_restrict_sourcevaluemaskentryright) + (dst_negative_scale_table_restrict_sourcevaluemaskentryright)))))) /\ (((((exists ff_h_pvs_table_restrict_sourcevaluemaskentryrightpositive. ff_h_pvs_table_restrict_sourcevaluemaskentryrightpositive + S (dst_positive_table_restrict_sourcevaluemaskentryright) = S ((S (dc_quotient_table_restrict_sourcevaluemaskentry)) * dst_positive_scale_table_restrict_sourcevaluemaskentryright)) /\ exists ff_q_pvs_table_restrict_sourcevaluemaskentryrightpositive. dst_positive_code_table_restrict_sourcevaluemaskentryright = ff_q_pvs_table_restrict_sourcevaluemaskentryrightpositive * S ((S (dc_quotient_table_restrict_sourcevaluemaskentry)) * dst_positive_scale_table_restrict_sourcevaluemaskentryright) + (dst_positive_table_restrict_sourcevaluemaskentryright))) /\ (((((exists ff_h_pvs_table_restrict_sourcevaluemaskentryrightnegative. ff_h_pvs_table_restrict_sourcevaluemaskentryrightnegative + S (dst_negative_table_restrict_sourcevaluemaskentryright) = S ((S (dc_quotient_table_restrict_sourcevaluemaskentry)) * dst_negative_scale_table_restrict_sourcevaluemaskentryright)) /\ exists ff_q_pvs_table_restrict_sourcevaluemaskentryrightnegative. dst_negative_code_table_restrict_sourcevaluemaskentryright = ff_q_pvs_table_restrict_sourcevaluemaskentryrightnegative * S ((S (dc_quotient_table_restrict_sourcevaluemaskentry)) * dst_negative_scale_table_restrict_sourcevaluemaskentryright) + (dst_negative_table_restrict_sourcevaluemaskentryright))) /\ (exists ge_balance_positive_table_restrict_sourcevaluemaskentryrightvalue ge_balance_negative_table_restrict_sourcevaluemaskentryrightvalue. (((((dc_right_table_restrict_sourcevaluemaskentry) = 2 * (ge_balance_positive_table_restrict_sourcevaluemaskentryrightvalue) /\ (ge_balance_negative_table_restrict_sourcevaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_table_restrict_sourcevaluemaskentryrightvaluedecode. (((dc_right_table_restrict_sourcevaluemaskentry) = 2 * ge_signed_half_table_restrict_sourcevaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_table_restrict_sourcevaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_table_restrict_sourcevaluemaskentryrightvalue) = S ge_signed_half_table_restrict_sourcevaluemaskentryrightvaluedecode))) /\ ((dst_positive_table_restrict_sourcevaluemaskentryright) + ge_balance_negative_table_restrict_sourcevaluemaskentryrightvalue = (dst_negative_table_restrict_sourcevaluemaskentryright) + ge_balance_positive_table_restrict_sourcevaluemaskentryrightvalue))))))))) /\ (exists sto_ap_table_restrict_sourcevaluemaskentryproduct sto_an_table_restrict_sourcevaluemaskentryproduct sto_bp_table_restrict_sourcevaluemaskentryproduct sto_bn_table_restrict_sourcevaluemaskentryproduct sto_cp_table_restrict_sourcevaluemaskentryproduct sto_cn_table_restrict_sourcevaluemaskentryproduct. (((((dc_left_table_restrict_sourcevaluemaskentry) = 2 * (sto_ap_table_restrict_sourcevaluemaskentryproduct) /\ (sto_an_table_restrict_sourcevaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_restrict_sourcevaluemaskentryproductleft. (((dc_left_table_restrict_sourcevaluemaskentry) = 2 * ge_signed_half_table_restrict_sourcevaluemaskentryproductleft + 1 /\ (sto_ap_table_restrict_sourcevaluemaskentryproduct) = 0) /\ (sto_an_table_restrict_sourcevaluemaskentryproduct) = S ge_signed_half_table_restrict_sourcevaluemaskentryproductleft))) /\ ((((((dc_right_table_restrict_sourcevaluemaskentry) = 2 * (sto_bp_table_restrict_sourcevaluemaskentryproduct) /\ (sto_bn_table_restrict_sourcevaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_restrict_sourcevaluemaskentryproductright. (((dc_right_table_restrict_sourcevaluemaskentry) = 2 * ge_signed_half_table_restrict_sourcevaluemaskentryproductright + 1 /\ (sto_bp_table_restrict_sourcevaluemaskentryproduct) = 0) /\ (sto_bn_table_restrict_sourcevaluemaskentryproduct) = S ge_signed_half_table_restrict_sourcevaluemaskentryproductright))) /\ ((((((dc_value_table_restrict_sourcevaluemask) = 2 * (sto_cp_table_restrict_sourcevaluemaskentryproduct) /\ (sto_cn_table_restrict_sourcevaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_restrict_sourcevaluemaskentryproductoutput. (((dc_value_table_restrict_sourcevaluemask) = 2 * ge_signed_half_table_restrict_sourcevaluemaskentryproductoutput + 1 /\ (sto_cp_table_restrict_sourcevaluemaskentryproduct) = 0) /\ (sto_cn_table_restrict_sourcevaluemaskentryproduct) = S ge_signed_half_table_restrict_sourcevaluemaskentryproductoutput))) /\ ((sto_ap_table_restrict_sourcevaluemaskentryproduct * sto_bp_table_restrict_sourcevaluemaskentryproduct + sto_an_table_restrict_sourcevaluemaskentryproduct * sto_bn_table_restrict_sourcevaluemaskentryproduct) + sto_cn_table_restrict_sourcevaluemaskentryproduct = (sto_ap_table_restrict_sourcevaluemaskentryproduct * sto_bn_table_restrict_sourcevaluemaskentryproduct + sto_an_table_restrict_sourcevaluemaskentryproduct * sto_bp_table_restrict_sourcevaluemaskentryproduct) + sto_cp_table_restrict_sourcevaluemaskentryproduct))))))))))))))) \/ ((((dc_index_table_restrict_sourcevaluemask)=0 \/ ~(exists pvs_factor_table_restrict_sourcevaluemaskentrynondivisor. (dc_input_table_restrict_source) = (dc_index_table_restrict_sourcevaluemask) * pvs_factor_table_restrict_sourcevaluemaskentrynondivisor)) /\ ((dc_value_table_restrict_sourcevaluemask)=0))))))) /\ (exists dst_positive_code_table_restrict_sourcevaluefold dst_positive_scale_table_restrict_sourcevaluefold dst_negative_code_table_restrict_sourcevaluefold dst_negative_scale_table_restrict_sourcevaluefold dst_positive_sum_table_restrict_sourcevaluefold dst_negative_sum_table_restrict_sourcevaluefold. (((dc_mask_table_restrict_sourcevalue) = (((((dst_positive_code_table_restrict_sourcevaluefold) + (dst_positive_scale_table_restrict_sourcevaluefold)) * S ((dst_positive_code_table_restrict_sourcevaluefold) + (dst_positive_scale_table_restrict_sourcevaluefold)) + ((dst_positive_scale_table_restrict_sourcevaluefold) + (dst_positive_scale_table_restrict_sourcevaluefold))) + (((dst_negative_code_table_restrict_sourcevaluefold) + (dst_negative_scale_table_restrict_sourcevaluefold)) * S ((dst_negative_code_table_restrict_sourcevaluefold) + (dst_negative_scale_table_restrict_sourcevaluefold)) + ((dst_negative_scale_table_restrict_sourcevaluefold) + (dst_negative_scale_table_restrict_sourcevaluefold)))) * S ((((dst_positive_code_table_restrict_sourcevaluefold) + (dst_positive_scale_table_restrict_sourcevaluefold)) * S ((dst_positive_code_table_restrict_sourcevaluefold) + (dst_positive_scale_table_restrict_sourcevaluefold)) + ((dst_positive_scale_table_restrict_sourcevaluefold) + (dst_positive_scale_table_restrict_sourcevaluefold))) + (((dst_negative_code_table_restrict_sourcevaluefold) + (dst_negative_scale_table_restrict_sourcevaluefold)) * S ((dst_negative_code_table_restrict_sourcevaluefold) + (dst_negative_scale_table_restrict_sourcevaluefold)) + ((dst_negative_scale_table_restrict_sourcevaluefold) + (dst_negative_scale_table_restrict_sourcevaluefold)))) + ((((dst_negative_code_table_restrict_sourcevaluefold) + (dst_negative_scale_table_restrict_sourcevaluefold)) * S ((dst_negative_code_table_restrict_sourcevaluefold) + (dst_negative_scale_table_restrict_sourcevaluefold)) + ((dst_negative_scale_table_restrict_sourcevaluefold) + (dst_negative_scale_table_restrict_sourcevaluefold))) + (((dst_negative_code_table_restrict_sourcevaluefold) + (dst_negative_scale_table_restrict_sourcevaluefold)) * S ((dst_negative_code_table_restrict_sourcevaluefold) + (dst_negative_scale_table_restrict_sourcevaluefold)) + ((dst_negative_scale_table_restrict_sourcevaluefold) + (dst_negative_scale_table_restrict_sourcevaluefold)))))) /\ (((exists fs_u_dst_table_restrict_sourcevaluefoldpositive fs_v_dst_table_restrict_sourcevaluefoldpositive. ((((exists fs_h_dst_table_restrict_sourcevaluefoldpositive_body_start. fs_h_dst_table_restrict_sourcevaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_table_restrict_sourcevaluefoldpositive)) /\ exists fs_q_dst_table_restrict_sourcevaluefoldpositive_body_start. fs_u_dst_table_restrict_sourcevaluefoldpositive = fs_q_dst_table_restrict_sourcevaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_table_restrict_sourcevaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_table_restrict_sourcevaluefoldpositive_body_terminal. fs_h_dst_table_restrict_sourcevaluefoldpositive_body_terminal + S (dst_positive_sum_table_restrict_sourcevaluefold) = S ((S (S (dc_input_table_restrict_source))) * fs_v_dst_table_restrict_sourcevaluefoldpositive)) /\ exists fs_q_dst_table_restrict_sourcevaluefoldpositive_body_terminal. fs_u_dst_table_restrict_sourcevaluefoldpositive = fs_q_dst_table_restrict_sourcevaluefoldpositive_body_terminal * S ((S (S (dc_input_table_restrict_source))) * fs_v_dst_table_restrict_sourcevaluefoldpositive) + (dst_positive_sum_table_restrict_sourcevaluefold))) /\ forall fs_i_dst_table_restrict_sourcevaluefoldpositive_body_steps. (exists fs_lt_dst_table_restrict_sourcevaluefoldpositive_body_steps_bound. fs_lt_dst_table_restrict_sourcevaluefoldpositive_body_steps_bound + S fs_i_dst_table_restrict_sourcevaluefoldpositive_body_steps = S (dc_input_table_restrict_source)) -> exists fs_a_dst_table_restrict_sourcevaluefoldpositive_body_steps fs_r_dst_table_restrict_sourcevaluefoldpositive_body_steps fs_s_dst_table_restrict_sourcevaluefoldpositive_body_steps. ((((exists fs_h_dst_table_restrict_sourcevaluefoldpositive_body_steps_summand. fs_h_dst_table_restrict_sourcevaluefoldpositive_body_steps_summand + S (fs_a_dst_table_restrict_sourcevaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_restrict_sourcevaluefoldpositive_body_steps)) * dst_positive_scale_table_restrict_sourcevaluefold)) /\ exists fs_q_dst_table_restrict_sourcevaluefoldpositive_body_steps_summand. dst_positive_code_table_restrict_sourcevaluefold = fs_q_dst_table_restrict_sourcevaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_table_restrict_sourcevaluefoldpositive_body_steps)) * dst_positive_scale_table_restrict_sourcevaluefold) + (fs_a_dst_table_restrict_sourcevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_restrict_sourcevaluefoldpositive_body_steps_partial. fs_h_dst_table_restrict_sourcevaluefoldpositive_body_steps_partial + S (fs_r_dst_table_restrict_sourcevaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_restrict_sourcevaluefoldpositive_body_steps)) * fs_v_dst_table_restrict_sourcevaluefoldpositive)) /\ exists fs_q_dst_table_restrict_sourcevaluefoldpositive_body_steps_partial. fs_u_dst_table_restrict_sourcevaluefoldpositive = fs_q_dst_table_restrict_sourcevaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_table_restrict_sourcevaluefoldpositive_body_steps)) * fs_v_dst_table_restrict_sourcevaluefoldpositive) + (fs_r_dst_table_restrict_sourcevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_restrict_sourcevaluefoldpositive_body_steps_successor. fs_h_dst_table_restrict_sourcevaluefoldpositive_body_steps_successor + S (fs_s_dst_table_restrict_sourcevaluefoldpositive_body_steps) = S ((S (S fs_i_dst_table_restrict_sourcevaluefoldpositive_body_steps)) * fs_v_dst_table_restrict_sourcevaluefoldpositive)) /\ exists fs_q_dst_table_restrict_sourcevaluefoldpositive_body_steps_successor. fs_u_dst_table_restrict_sourcevaluefoldpositive = fs_q_dst_table_restrict_sourcevaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_table_restrict_sourcevaluefoldpositive_body_steps)) * fs_v_dst_table_restrict_sourcevaluefoldpositive) + (fs_s_dst_table_restrict_sourcevaluefoldpositive_body_steps))) /\ fs_s_dst_table_restrict_sourcevaluefoldpositive_body_steps = fs_r_dst_table_restrict_sourcevaluefoldpositive_body_steps + fs_a_dst_table_restrict_sourcevaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_table_restrict_sourcevaluefoldnegative fs_v_dst_table_restrict_sourcevaluefoldnegative. ((((exists fs_h_dst_table_restrict_sourcevaluefoldnegative_body_start. fs_h_dst_table_restrict_sourcevaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_table_restrict_sourcevaluefoldnegative)) /\ exists fs_q_dst_table_restrict_sourcevaluefoldnegative_body_start. fs_u_dst_table_restrict_sourcevaluefoldnegative = fs_q_dst_table_restrict_sourcevaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_table_restrict_sourcevaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_table_restrict_sourcevaluefoldnegative_body_terminal. fs_h_dst_table_restrict_sourcevaluefoldnegative_body_terminal + S (dst_negative_sum_table_restrict_sourcevaluefold) = S ((S (S (dc_input_table_restrict_source))) * fs_v_dst_table_restrict_sourcevaluefoldnegative)) /\ exists fs_q_dst_table_restrict_sourcevaluefoldnegative_body_terminal. fs_u_dst_table_restrict_sourcevaluefoldnegative = fs_q_dst_table_restrict_sourcevaluefoldnegative_body_terminal * S ((S (S (dc_input_table_restrict_source))) * fs_v_dst_table_restrict_sourcevaluefoldnegative) + (dst_negative_sum_table_restrict_sourcevaluefold))) /\ forall fs_i_dst_table_restrict_sourcevaluefoldnegative_body_steps. (exists fs_lt_dst_table_restrict_sourcevaluefoldnegative_body_steps_bound. fs_lt_dst_table_restrict_sourcevaluefoldnegative_body_steps_bound + S fs_i_dst_table_restrict_sourcevaluefoldnegative_body_steps = S (dc_input_table_restrict_source)) -> exists fs_a_dst_table_restrict_sourcevaluefoldnegative_body_steps fs_r_dst_table_restrict_sourcevaluefoldnegative_body_steps fs_s_dst_table_restrict_sourcevaluefoldnegative_body_steps. ((((exists fs_h_dst_table_restrict_sourcevaluefoldnegative_body_steps_summand. fs_h_dst_table_restrict_sourcevaluefoldnegative_body_steps_summand + S (fs_a_dst_table_restrict_sourcevaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_restrict_sourcevaluefoldnegative_body_steps)) * dst_negative_scale_table_restrict_sourcevaluefold)) /\ exists fs_q_dst_table_restrict_sourcevaluefoldnegative_body_steps_summand. dst_negative_code_table_restrict_sourcevaluefold = fs_q_dst_table_restrict_sourcevaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_table_restrict_sourcevaluefoldnegative_body_steps)) * dst_negative_scale_table_restrict_sourcevaluefold) + (fs_a_dst_table_restrict_sourcevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_restrict_sourcevaluefoldnegative_body_steps_partial. fs_h_dst_table_restrict_sourcevaluefoldnegative_body_steps_partial + S (fs_r_dst_table_restrict_sourcevaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_restrict_sourcevaluefoldnegative_body_steps)) * fs_v_dst_table_restrict_sourcevaluefoldnegative)) /\ exists fs_q_dst_table_restrict_sourcevaluefoldnegative_body_steps_partial. fs_u_dst_table_restrict_sourcevaluefoldnegative = fs_q_dst_table_restrict_sourcevaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_table_restrict_sourcevaluefoldnegative_body_steps)) * fs_v_dst_table_restrict_sourcevaluefoldnegative) + (fs_r_dst_table_restrict_sourcevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_restrict_sourcevaluefoldnegative_body_steps_successor. fs_h_dst_table_restrict_sourcevaluefoldnegative_body_steps_successor + S (fs_s_dst_table_restrict_sourcevaluefoldnegative_body_steps) = S ((S (S fs_i_dst_table_restrict_sourcevaluefoldnegative_body_steps)) * fs_v_dst_table_restrict_sourcevaluefoldnegative)) /\ exists fs_q_dst_table_restrict_sourcevaluefoldnegative_body_steps_successor. fs_u_dst_table_restrict_sourcevaluefoldnegative = fs_q_dst_table_restrict_sourcevaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_table_restrict_sourcevaluefoldnegative_body_steps)) * fs_v_dst_table_restrict_sourcevaluefoldnegative) + (fs_s_dst_table_restrict_sourcevaluefoldnegative_body_steps))) /\ fs_s_dst_table_restrict_sourcevaluefoldnegative_body_steps = fs_r_dst_table_restrict_sourcevaluefoldnegative_body_steps + fs_a_dst_table_restrict_sourcevaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_table_restrict_sourcevaluefoldresult ge_balance_negative_table_restrict_sourcevaluefoldresult. (((((dc_output_table_restrict_source) = 2 * (ge_balance_positive_table_restrict_sourcevaluefoldresult) /\ (ge_balance_negative_table_restrict_sourcevaluefoldresult) = 0) \/ exists ge_signed_half_table_restrict_sourcevaluefoldresultdecode. (((dc_output_table_restrict_source) = 2 * ge_signed_half_table_restrict_sourcevaluefoldresultdecode + 1 /\ (ge_balance_positive_table_restrict_sourcevaluefoldresult) = 0) /\ (ge_balance_negative_table_restrict_sourcevaluefoldresult) = S ge_signed_half_table_restrict_sourcevaluefoldresultdecode))) /\ ((dst_positive_sum_table_restrict_sourcevaluefold) + ge_balance_negative_table_restrict_sourcevaluefoldresult = (dst_negative_sum_table_restrict_sourcevaluefold) + ge_balance_positive_table_restrict_sourcevaluefoldresult)))))))))))))))))))) -> (exists pvs_le_gap_table_restrict_bound. pvs_le_gap_table_restrict_bound + (J) = (N)) -> (((exists dst_positive_code_table_restrict_resultleft dst_positive_scale_table_restrict_resultleft dst_negative_code_table_restrict_resultleft dst_negative_scale_table_restrict_resultleft. (((F) = (((((dst_positive_code_table_restrict_resultleft) + (dst_positive_scale_table_restrict_resultleft)) * S ((dst_positive_code_table_restrict_resultleft) + (dst_positive_scale_table_restrict_resultleft)) + ((dst_positive_scale_table_restrict_resultleft) + (dst_positive_scale_table_restrict_resultleft))) + (((dst_negative_code_table_restrict_resultleft) + (dst_negative_scale_table_restrict_resultleft)) * S ((dst_negative_code_table_restrict_resultleft) + (dst_negative_scale_table_restrict_resultleft)) + ((dst_negative_scale_table_restrict_resultleft) + (dst_negative_scale_table_restrict_resultleft)))) * S ((((dst_positive_code_table_restrict_resultleft) + (dst_positive_scale_table_restrict_resultleft)) * S ((dst_positive_code_table_restrict_resultleft) + (dst_positive_scale_table_restrict_resultleft)) + ((dst_positive_scale_table_restrict_resultleft) + (dst_positive_scale_table_restrict_resultleft))) + (((dst_negative_code_table_restrict_resultleft) + (dst_negative_scale_table_restrict_resultleft)) * S ((dst_negative_code_table_restrict_resultleft) + (dst_negative_scale_table_restrict_resultleft)) + ((dst_negative_scale_table_restrict_resultleft) + (dst_negative_scale_table_restrict_resultleft)))) + ((((dst_negative_code_table_restrict_resultleft) + (dst_negative_scale_table_restrict_resultleft)) * S ((dst_negative_code_table_restrict_resultleft) + (dst_negative_scale_table_restrict_resultleft)) + ((dst_negative_scale_table_restrict_resultleft) + (dst_negative_scale_table_restrict_resultleft))) + (((dst_negative_code_table_restrict_resultleft) + (dst_negative_scale_table_restrict_resultleft)) * S ((dst_negative_code_table_restrict_resultleft) + (dst_negative_scale_table_restrict_resultleft)) + ((dst_negative_scale_table_restrict_resultleft) + (dst_negative_scale_table_restrict_resultleft)))))) /\ (forall dst_index_table_restrict_resultleft. (exists pvs_le_gap_table_restrict_resultleftdomain. pvs_le_gap_table_restrict_resultleftdomain + (dst_index_table_restrict_resultleft) = (J)) -> exists dst_positive_table_restrict_resultleft dst_negative_table_restrict_resultleft dst_value_table_restrict_resultleft. ((((exists ff_h_pvs_table_restrict_resultleftentrypositive. ff_h_pvs_table_restrict_resultleftentrypositive + S (dst_positive_table_restrict_resultleft) = S ((S (dst_index_table_restrict_resultleft)) * dst_positive_scale_table_restrict_resultleft)) /\ exists ff_q_pvs_table_restrict_resultleftentrypositive. dst_positive_code_table_restrict_resultleft = ff_q_pvs_table_restrict_resultleftentrypositive * S ((S (dst_index_table_restrict_resultleft)) * dst_positive_scale_table_restrict_resultleft) + (dst_positive_table_restrict_resultleft))) /\ (((((exists ff_h_pvs_table_restrict_resultleftentrynegative. ff_h_pvs_table_restrict_resultleftentrynegative + S (dst_negative_table_restrict_resultleft) = S ((S (dst_index_table_restrict_resultleft)) * dst_negative_scale_table_restrict_resultleft)) /\ exists ff_q_pvs_table_restrict_resultleftentrynegative. dst_negative_code_table_restrict_resultleft = ff_q_pvs_table_restrict_resultleftentrynegative * S ((S (dst_index_table_restrict_resultleft)) * dst_negative_scale_table_restrict_resultleft) + (dst_negative_table_restrict_resultleft))) /\ (exists ge_balance_positive_table_restrict_resultleftentryvalue ge_balance_negative_table_restrict_resultleftentryvalue. (((((dst_value_table_restrict_resultleft) = 2 * (ge_balance_positive_table_restrict_resultleftentryvalue) /\ (ge_balance_negative_table_restrict_resultleftentryvalue) = 0) \/ exists ge_signed_half_table_restrict_resultleftentryvaluedecode. (((dst_value_table_restrict_resultleft) = 2 * ge_signed_half_table_restrict_resultleftentryvaluedecode + 1 /\ (ge_balance_positive_table_restrict_resultleftentryvalue) = 0) /\ (ge_balance_negative_table_restrict_resultleftentryvalue) = S ge_signed_half_table_restrict_resultleftentryvaluedecode))) /\ ((dst_positive_table_restrict_resultleft) + ge_balance_negative_table_restrict_resultleftentryvalue = (dst_negative_table_restrict_resultleft) + ge_balance_positive_table_restrict_resultleftentryvalue))))))))) /\ (((exists dst_positive_code_table_restrict_resultright dst_positive_scale_table_restrict_resultright dst_negative_code_table_restrict_resultright dst_negative_scale_table_restrict_resultright. (((G) = (((((dst_positive_code_table_restrict_resultright) + (dst_positive_scale_table_restrict_resultright)) * S ((dst_positive_code_table_restrict_resultright) + (dst_positive_scale_table_restrict_resultright)) + ((dst_positive_scale_table_restrict_resultright) + (dst_positive_scale_table_restrict_resultright))) + (((dst_negative_code_table_restrict_resultright) + (dst_negative_scale_table_restrict_resultright)) * S ((dst_negative_code_table_restrict_resultright) + (dst_negative_scale_table_restrict_resultright)) + ((dst_negative_scale_table_restrict_resultright) + (dst_negative_scale_table_restrict_resultright)))) * S ((((dst_positive_code_table_restrict_resultright) + (dst_positive_scale_table_restrict_resultright)) * S ((dst_positive_code_table_restrict_resultright) + (dst_positive_scale_table_restrict_resultright)) + ((dst_positive_scale_table_restrict_resultright) + (dst_positive_scale_table_restrict_resultright))) + (((dst_negative_code_table_restrict_resultright) + (dst_negative_scale_table_restrict_resultright)) * S ((dst_negative_code_table_restrict_resultright) + (dst_negative_scale_table_restrict_resultright)) + ((dst_negative_scale_table_restrict_resultright) + (dst_negative_scale_table_restrict_resultright)))) + ((((dst_negative_code_table_restrict_resultright) + (dst_negative_scale_table_restrict_resultright)) * S ((dst_negative_code_table_restrict_resultright) + (dst_negative_scale_table_restrict_resultright)) + ((dst_negative_scale_table_restrict_resultright) + (dst_negative_scale_table_restrict_resultright))) + (((dst_negative_code_table_restrict_resultright) + (dst_negative_scale_table_restrict_resultright)) * S ((dst_negative_code_table_restrict_resultright) + (dst_negative_scale_table_restrict_resultright)) + ((dst_negative_scale_table_restrict_resultright) + (dst_negative_scale_table_restrict_resultright)))))) /\ (forall dst_index_table_restrict_resultright. (exists pvs_le_gap_table_restrict_resultrightdomain. pvs_le_gap_table_restrict_resultrightdomain + (dst_index_table_restrict_resultright) = (J)) -> exists dst_positive_table_restrict_resultright dst_negative_table_restrict_resultright dst_value_table_restrict_resultright. ((((exists ff_h_pvs_table_restrict_resultrightentrypositive. ff_h_pvs_table_restrict_resultrightentrypositive + S (dst_positive_table_restrict_resultright) = S ((S (dst_index_table_restrict_resultright)) * dst_positive_scale_table_restrict_resultright)) /\ exists ff_q_pvs_table_restrict_resultrightentrypositive. dst_positive_code_table_restrict_resultright = ff_q_pvs_table_restrict_resultrightentrypositive * S ((S (dst_index_table_restrict_resultright)) * dst_positive_scale_table_restrict_resultright) + (dst_positive_table_restrict_resultright))) /\ (((((exists ff_h_pvs_table_restrict_resultrightentrynegative. ff_h_pvs_table_restrict_resultrightentrynegative + S (dst_negative_table_restrict_resultright) = S ((S (dst_index_table_restrict_resultright)) * dst_negative_scale_table_restrict_resultright)) /\ exists ff_q_pvs_table_restrict_resultrightentrynegative. dst_negative_code_table_restrict_resultright = ff_q_pvs_table_restrict_resultrightentrynegative * S ((S (dst_index_table_restrict_resultright)) * dst_negative_scale_table_restrict_resultright) + (dst_negative_table_restrict_resultright))) /\ (exists ge_balance_positive_table_restrict_resultrightentryvalue ge_balance_negative_table_restrict_resultrightentryvalue. (((((dst_value_table_restrict_resultright) = 2 * (ge_balance_positive_table_restrict_resultrightentryvalue) /\ (ge_balance_negative_table_restrict_resultrightentryvalue) = 0) \/ exists ge_signed_half_table_restrict_resultrightentryvaluedecode. (((dst_value_table_restrict_resultright) = 2 * ge_signed_half_table_restrict_resultrightentryvaluedecode + 1 /\ (ge_balance_positive_table_restrict_resultrightentryvalue) = 0) /\ (ge_balance_negative_table_restrict_resultrightentryvalue) = S ge_signed_half_table_restrict_resultrightentryvaluedecode))) /\ ((dst_positive_table_restrict_resultright) + ge_balance_negative_table_restrict_resultrightentryvalue = (dst_negative_table_restrict_resultright) + ge_balance_positive_table_restrict_resultrightentryvalue))))))))) /\ (((exists dst_positive_code_table_restrict_resulttable dst_positive_scale_table_restrict_resulttable dst_negative_code_table_restrict_resulttable dst_negative_scale_table_restrict_resulttable. (((H) = (((((dst_positive_code_table_restrict_resulttable) + (dst_positive_scale_table_restrict_resulttable)) * S ((dst_positive_code_table_restrict_resulttable) + (dst_positive_scale_table_restrict_resulttable)) + ((dst_positive_scale_table_restrict_resulttable) + (dst_positive_scale_table_restrict_resulttable))) + (((dst_negative_code_table_restrict_resulttable) + (dst_negative_scale_table_restrict_resulttable)) * S ((dst_negative_code_table_restrict_resulttable) + (dst_negative_scale_table_restrict_resulttable)) + ((dst_negative_scale_table_restrict_resulttable) + (dst_negative_scale_table_restrict_resulttable)))) * S ((((dst_positive_code_table_restrict_resulttable) + (dst_positive_scale_table_restrict_resulttable)) * S ((dst_positive_code_table_restrict_resulttable) + (dst_positive_scale_table_restrict_resulttable)) + ((dst_positive_scale_table_restrict_resulttable) + (dst_positive_scale_table_restrict_resulttable))) + (((dst_negative_code_table_restrict_resulttable) + (dst_negative_scale_table_restrict_resulttable)) * S ((dst_negative_code_table_restrict_resulttable) + (dst_negative_scale_table_restrict_resulttable)) + ((dst_negative_scale_table_restrict_resulttable) + (dst_negative_scale_table_restrict_resulttable)))) + ((((dst_negative_code_table_restrict_resulttable) + (dst_negative_scale_table_restrict_resulttable)) * S ((dst_negative_code_table_restrict_resulttable) + (dst_negative_scale_table_restrict_resulttable)) + ((dst_negative_scale_table_restrict_resulttable) + (dst_negative_scale_table_restrict_resulttable))) + (((dst_negative_code_table_restrict_resulttable) + (dst_negative_scale_table_restrict_resulttable)) * S ((dst_negative_code_table_restrict_resulttable) + (dst_negative_scale_table_restrict_resulttable)) + ((dst_negative_scale_table_restrict_resulttable) + (dst_negative_scale_table_restrict_resulttable)))))) /\ (forall dst_index_table_restrict_resulttable. (exists pvs_le_gap_table_restrict_resulttabledomain. pvs_le_gap_table_restrict_resulttabledomain + (dst_index_table_restrict_resulttable) = (J)) -> exists dst_positive_table_restrict_resulttable dst_negative_table_restrict_resulttable dst_value_table_restrict_resulttable. ((((exists ff_h_pvs_table_restrict_resulttableentrypositive. ff_h_pvs_table_restrict_resulttableentrypositive + S (dst_positive_table_restrict_resulttable) = S ((S (dst_index_table_restrict_resulttable)) * dst_positive_scale_table_restrict_resulttable)) /\ exists ff_q_pvs_table_restrict_resulttableentrypositive. dst_positive_code_table_restrict_resulttable = ff_q_pvs_table_restrict_resulttableentrypositive * S ((S (dst_index_table_restrict_resulttable)) * dst_positive_scale_table_restrict_resulttable) + (dst_positive_table_restrict_resulttable))) /\ (((((exists ff_h_pvs_table_restrict_resulttableentrynegative. ff_h_pvs_table_restrict_resulttableentrynegative + S (dst_negative_table_restrict_resulttable) = S ((S (dst_index_table_restrict_resulttable)) * dst_negative_scale_table_restrict_resulttable)) /\ exists ff_q_pvs_table_restrict_resulttableentrynegative. dst_negative_code_table_restrict_resulttable = ff_q_pvs_table_restrict_resulttableentrynegative * S ((S (dst_index_table_restrict_resulttable)) * dst_negative_scale_table_restrict_resulttable) + (dst_negative_table_restrict_resulttable))) /\ (exists ge_balance_positive_table_restrict_resulttableentryvalue ge_balance_negative_table_restrict_resulttableentryvalue. (((((dst_value_table_restrict_resulttable) = 2 * (ge_balance_positive_table_restrict_resulttableentryvalue) /\ (ge_balance_negative_table_restrict_resulttableentryvalue) = 0) \/ exists ge_signed_half_table_restrict_resulttableentryvaluedecode. (((dst_value_table_restrict_resulttable) = 2 * ge_signed_half_table_restrict_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_table_restrict_resulttableentryvalue) = 0) /\ (ge_balance_negative_table_restrict_resulttableentryvalue) = S ge_signed_half_table_restrict_resulttableentryvaluedecode))) /\ ((dst_positive_table_restrict_resulttable) + ge_balance_negative_table_restrict_resulttableentryvalue = (dst_negative_table_restrict_resulttable) + ge_balance_positive_table_restrict_resulttableentryvalue))))))))) /\ (forall dc_input_table_restrict_result dc_output_table_restrict_result. ~(dc_input_table_restrict_result=0) -> (exists pvs_le_gap_table_restrict_resultdomain. pvs_le_gap_table_restrict_resultdomain + (dc_input_table_restrict_result) = (J)) -> (exists dst_positive_code_table_restrict_resultlookup dst_positive_scale_table_restrict_resultlookup dst_negative_code_table_restrict_resultlookup dst_negative_scale_table_restrict_resultlookup dst_positive_table_restrict_resultlookup dst_negative_table_restrict_resultlookup. (((H) = (((((dst_positive_code_table_restrict_resultlookup) + (dst_positive_scale_table_restrict_resultlookup)) * S ((dst_positive_code_table_restrict_resultlookup) + (dst_positive_scale_table_restrict_resultlookup)) + ((dst_positive_scale_table_restrict_resultlookup) + (dst_positive_scale_table_restrict_resultlookup))) + (((dst_negative_code_table_restrict_resultlookup) + (dst_negative_scale_table_restrict_resultlookup)) * S ((dst_negative_code_table_restrict_resultlookup) + (dst_negative_scale_table_restrict_resultlookup)) + ((dst_negative_scale_table_restrict_resultlookup) + (dst_negative_scale_table_restrict_resultlookup)))) * S ((((dst_positive_code_table_restrict_resultlookup) + (dst_positive_scale_table_restrict_resultlookup)) * S ((dst_positive_code_table_restrict_resultlookup) + (dst_positive_scale_table_restrict_resultlookup)) + ((dst_positive_scale_table_restrict_resultlookup) + (dst_positive_scale_table_restrict_resultlookup))) + (((dst_negative_code_table_restrict_resultlookup) + (dst_negative_scale_table_restrict_resultlookup)) * S ((dst_negative_code_table_restrict_resultlookup) + (dst_negative_scale_table_restrict_resultlookup)) + ((dst_negative_scale_table_restrict_resultlookup) + (dst_negative_scale_table_restrict_resultlookup)))) + ((((dst_negative_code_table_restrict_resultlookup) + (dst_negative_scale_table_restrict_resultlookup)) * S ((dst_negative_code_table_restrict_resultlookup) + (dst_negative_scale_table_restrict_resultlookup)) + ((dst_negative_scale_table_restrict_resultlookup) + (dst_negative_scale_table_restrict_resultlookup))) + (((dst_negative_code_table_restrict_resultlookup) + (dst_negative_scale_table_restrict_resultlookup)) * S ((dst_negative_code_table_restrict_resultlookup) + (dst_negative_scale_table_restrict_resultlookup)) + ((dst_negative_scale_table_restrict_resultlookup) + (dst_negative_scale_table_restrict_resultlookup)))))) /\ (((((exists ff_h_pvs_table_restrict_resultlookuppositive. ff_h_pvs_table_restrict_resultlookuppositive + S (dst_positive_table_restrict_resultlookup) = S ((S (dc_input_table_restrict_result)) * dst_positive_scale_table_restrict_resultlookup)) /\ exists ff_q_pvs_table_restrict_resultlookuppositive. dst_positive_code_table_restrict_resultlookup = ff_q_pvs_table_restrict_resultlookuppositive * S ((S (dc_input_table_restrict_result)) * dst_positive_scale_table_restrict_resultlookup) + (dst_positive_table_restrict_resultlookup))) /\ (((((exists ff_h_pvs_table_restrict_resultlookupnegative. ff_h_pvs_table_restrict_resultlookupnegative + S (dst_negative_table_restrict_resultlookup) = S ((S (dc_input_table_restrict_result)) * dst_negative_scale_table_restrict_resultlookup)) /\ exists ff_q_pvs_table_restrict_resultlookupnegative. dst_negative_code_table_restrict_resultlookup = ff_q_pvs_table_restrict_resultlookupnegative * S ((S (dc_input_table_restrict_result)) * dst_negative_scale_table_restrict_resultlookup) + (dst_negative_table_restrict_resultlookup))) /\ (exists ge_balance_positive_table_restrict_resultlookupvalue ge_balance_negative_table_restrict_resultlookupvalue. (((((dc_output_table_restrict_result) = 2 * (ge_balance_positive_table_restrict_resultlookupvalue) /\ (ge_balance_negative_table_restrict_resultlookupvalue) = 0) \/ exists ge_signed_half_table_restrict_resultlookupvaluedecode. (((dc_output_table_restrict_result) = 2 * ge_signed_half_table_restrict_resultlookupvaluedecode + 1 /\ (ge_balance_positive_table_restrict_resultlookupvalue) = 0) /\ (ge_balance_negative_table_restrict_resultlookupvalue) = S ge_signed_half_table_restrict_resultlookupvaluedecode))) /\ ((dst_positive_table_restrict_resultlookup) + ge_balance_negative_table_restrict_resultlookupvalue = (dst_negative_table_restrict_resultlookup) + ge_balance_positive_table_restrict_resultlookupvalue))))))))) -> (((~((dc_input_table_restrict_result)=0)) /\ (exists dc_mask_table_restrict_resultvalue. ((((exists dst_positive_code_table_restrict_resultvaluemasktable dst_positive_scale_table_restrict_resultvaluemasktable dst_negative_code_table_restrict_resultvaluemasktable dst_negative_scale_table_restrict_resultvaluemasktable. (((dc_mask_table_restrict_resultvalue) = (((((dst_positive_code_table_restrict_resultvaluemasktable) + (dst_positive_scale_table_restrict_resultvaluemasktable)) * S ((dst_positive_code_table_restrict_resultvaluemasktable) + (dst_positive_scale_table_restrict_resultvaluemasktable)) + ((dst_positive_scale_table_restrict_resultvaluemasktable) + (dst_positive_scale_table_restrict_resultvaluemasktable))) + (((dst_negative_code_table_restrict_resultvaluemasktable) + (dst_negative_scale_table_restrict_resultvaluemasktable)) * S ((dst_negative_code_table_restrict_resultvaluemasktable) + (dst_negative_scale_table_restrict_resultvaluemasktable)) + ((dst_negative_scale_table_restrict_resultvaluemasktable) + (dst_negative_scale_table_restrict_resultvaluemasktable)))) * S ((((dst_positive_code_table_restrict_resultvaluemasktable) + (dst_positive_scale_table_restrict_resultvaluemasktable)) * S ((dst_positive_code_table_restrict_resultvaluemasktable) + (dst_positive_scale_table_restrict_resultvaluemasktable)) + ((dst_positive_scale_table_restrict_resultvaluemasktable) + (dst_positive_scale_table_restrict_resultvaluemasktable))) + (((dst_negative_code_table_restrict_resultvaluemasktable) + (dst_negative_scale_table_restrict_resultvaluemasktable)) * S ((dst_negative_code_table_restrict_resultvaluemasktable) + (dst_negative_scale_table_restrict_resultvaluemasktable)) + ((dst_negative_scale_table_restrict_resultvaluemasktable) + (dst_negative_scale_table_restrict_resultvaluemasktable)))) + ((((dst_negative_code_table_restrict_resultvaluemasktable) + (dst_negative_scale_table_restrict_resultvaluemasktable)) * S ((dst_negative_code_table_restrict_resultvaluemasktable) + (dst_negative_scale_table_restrict_resultvaluemasktable)) + ((dst_negative_scale_table_restrict_resultvaluemasktable) + (dst_negative_scale_table_restrict_resultvaluemasktable))) + (((dst_negative_code_table_restrict_resultvaluemasktable) + (dst_negative_scale_table_restrict_resultvaluemasktable)) * S ((dst_negative_code_table_restrict_resultvaluemasktable) + (dst_negative_scale_table_restrict_resultvaluemasktable)) + ((dst_negative_scale_table_restrict_resultvaluemasktable) + (dst_negative_scale_table_restrict_resultvaluemasktable)))))) /\ (forall dst_index_table_restrict_resultvaluemasktable. (exists pvs_le_gap_table_restrict_resultvaluemasktabledomain. pvs_le_gap_table_restrict_resultvaluemasktabledomain + (dst_index_table_restrict_resultvaluemasktable) = (dc_input_table_restrict_result)) -> exists dst_positive_table_restrict_resultvaluemasktable dst_negative_table_restrict_resultvaluemasktable dst_value_table_restrict_resultvaluemasktable. ((((exists ff_h_pvs_table_restrict_resultvaluemasktableentrypositive. ff_h_pvs_table_restrict_resultvaluemasktableentrypositive + S (dst_positive_table_restrict_resultvaluemasktable) = S ((S (dst_index_table_restrict_resultvaluemasktable)) * dst_positive_scale_table_restrict_resultvaluemasktable)) /\ exists ff_q_pvs_table_restrict_resultvaluemasktableentrypositive. dst_positive_code_table_restrict_resultvaluemasktable = ff_q_pvs_table_restrict_resultvaluemasktableentrypositive * S ((S (dst_index_table_restrict_resultvaluemasktable)) * dst_positive_scale_table_restrict_resultvaluemasktable) + (dst_positive_table_restrict_resultvaluemasktable))) /\ (((((exists ff_h_pvs_table_restrict_resultvaluemasktableentrynegative. ff_h_pvs_table_restrict_resultvaluemasktableentrynegative + S (dst_negative_table_restrict_resultvaluemasktable) = S ((S (dst_index_table_restrict_resultvaluemasktable)) * dst_negative_scale_table_restrict_resultvaluemasktable)) /\ exists ff_q_pvs_table_restrict_resultvaluemasktableentrynegative. dst_negative_code_table_restrict_resultvaluemasktable = ff_q_pvs_table_restrict_resultvaluemasktableentrynegative * S ((S (dst_index_table_restrict_resultvaluemasktable)) * dst_negative_scale_table_restrict_resultvaluemasktable) + (dst_negative_table_restrict_resultvaluemasktable))) /\ (exists ge_balance_positive_table_restrict_resultvaluemasktableentryvalue ge_balance_negative_table_restrict_resultvaluemasktableentryvalue. (((((dst_value_table_restrict_resultvaluemasktable) = 2 * (ge_balance_positive_table_restrict_resultvaluemasktableentryvalue) /\ (ge_balance_negative_table_restrict_resultvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_table_restrict_resultvaluemasktableentryvaluedecode. (((dst_value_table_restrict_resultvaluemasktable) = 2 * ge_signed_half_table_restrict_resultvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_table_restrict_resultvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_table_restrict_resultvaluemasktableentryvalue) = S ge_signed_half_table_restrict_resultvaluemasktableentryvaluedecode))) /\ ((dst_positive_table_restrict_resultvaluemasktable) + ge_balance_negative_table_restrict_resultvaluemasktableentryvalue = (dst_negative_table_restrict_resultvaluemasktable) + ge_balance_positive_table_restrict_resultvaluemasktableentryvalue))))))))) /\ (forall dc_index_table_restrict_resultvaluemask dc_value_table_restrict_resultvaluemask. (exists pvs_le_gap_table_restrict_resultvaluemaskdomain. pvs_le_gap_table_restrict_resultvaluemaskdomain + (dc_index_table_restrict_resultvaluemask) = (dc_input_table_restrict_result)) -> (exists dst_positive_code_table_restrict_resultvaluemasklookup dst_positive_scale_table_restrict_resultvaluemasklookup dst_negative_code_table_restrict_resultvaluemasklookup dst_negative_scale_table_restrict_resultvaluemasklookup dst_positive_table_restrict_resultvaluemasklookup dst_negative_table_restrict_resultvaluemasklookup. (((dc_mask_table_restrict_resultvalue) = (((((dst_positive_code_table_restrict_resultvaluemasklookup) + (dst_positive_scale_table_restrict_resultvaluemasklookup)) * S ((dst_positive_code_table_restrict_resultvaluemasklookup) + (dst_positive_scale_table_restrict_resultvaluemasklookup)) + ((dst_positive_scale_table_restrict_resultvaluemasklookup) + (dst_positive_scale_table_restrict_resultvaluemasklookup))) + (((dst_negative_code_table_restrict_resultvaluemasklookup) + (dst_negative_scale_table_restrict_resultvaluemasklookup)) * S ((dst_negative_code_table_restrict_resultvaluemasklookup) + (dst_negative_scale_table_restrict_resultvaluemasklookup)) + ((dst_negative_scale_table_restrict_resultvaluemasklookup) + (dst_negative_scale_table_restrict_resultvaluemasklookup)))) * S ((((dst_positive_code_table_restrict_resultvaluemasklookup) + (dst_positive_scale_table_restrict_resultvaluemasklookup)) * S ((dst_positive_code_table_restrict_resultvaluemasklookup) + (dst_positive_scale_table_restrict_resultvaluemasklookup)) + ((dst_positive_scale_table_restrict_resultvaluemasklookup) + (dst_positive_scale_table_restrict_resultvaluemasklookup))) + (((dst_negative_code_table_restrict_resultvaluemasklookup) + (dst_negative_scale_table_restrict_resultvaluemasklookup)) * S ((dst_negative_code_table_restrict_resultvaluemasklookup) + (dst_negative_scale_table_restrict_resultvaluemasklookup)) + ((dst_negative_scale_table_restrict_resultvaluemasklookup) + (dst_negative_scale_table_restrict_resultvaluemasklookup)))) + ((((dst_negative_code_table_restrict_resultvaluemasklookup) + (dst_negative_scale_table_restrict_resultvaluemasklookup)) * S ((dst_negative_code_table_restrict_resultvaluemasklookup) + (dst_negative_scale_table_restrict_resultvaluemasklookup)) + ((dst_negative_scale_table_restrict_resultvaluemasklookup) + (dst_negative_scale_table_restrict_resultvaluemasklookup))) + (((dst_negative_code_table_restrict_resultvaluemasklookup) + (dst_negative_scale_table_restrict_resultvaluemasklookup)) * S ((dst_negative_code_table_restrict_resultvaluemasklookup) + (dst_negative_scale_table_restrict_resultvaluemasklookup)) + ((dst_negative_scale_table_restrict_resultvaluemasklookup) + (dst_negative_scale_table_restrict_resultvaluemasklookup)))))) /\ (((((exists ff_h_pvs_table_restrict_resultvaluemasklookuppositive. ff_h_pvs_table_restrict_resultvaluemasklookuppositive + S (dst_positive_table_restrict_resultvaluemasklookup) = S ((S (dc_index_table_restrict_resultvaluemask)) * dst_positive_scale_table_restrict_resultvaluemasklookup)) /\ exists ff_q_pvs_table_restrict_resultvaluemasklookuppositive. dst_positive_code_table_restrict_resultvaluemasklookup = ff_q_pvs_table_restrict_resultvaluemasklookuppositive * S ((S (dc_index_table_restrict_resultvaluemask)) * dst_positive_scale_table_restrict_resultvaluemasklookup) + (dst_positive_table_restrict_resultvaluemasklookup))) /\ (((((exists ff_h_pvs_table_restrict_resultvaluemasklookupnegative. ff_h_pvs_table_restrict_resultvaluemasklookupnegative + S (dst_negative_table_restrict_resultvaluemasklookup) = S ((S (dc_index_table_restrict_resultvaluemask)) * dst_negative_scale_table_restrict_resultvaluemasklookup)) /\ exists ff_q_pvs_table_restrict_resultvaluemasklookupnegative. dst_negative_code_table_restrict_resultvaluemasklookup = ff_q_pvs_table_restrict_resultvaluemasklookupnegative * S ((S (dc_index_table_restrict_resultvaluemask)) * dst_negative_scale_table_restrict_resultvaluemasklookup) + (dst_negative_table_restrict_resultvaluemasklookup))) /\ (exists ge_balance_positive_table_restrict_resultvaluemasklookupvalue ge_balance_negative_table_restrict_resultvaluemasklookupvalue. (((((dc_value_table_restrict_resultvaluemask) = 2 * (ge_balance_positive_table_restrict_resultvaluemasklookupvalue) /\ (ge_balance_negative_table_restrict_resultvaluemasklookupvalue) = 0) \/ exists ge_signed_half_table_restrict_resultvaluemasklookupvaluedecode. (((dc_value_table_restrict_resultvaluemask) = 2 * ge_signed_half_table_restrict_resultvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_table_restrict_resultvaluemasklookupvalue) = 0) /\ (ge_balance_negative_table_restrict_resultvaluemasklookupvalue) = S ge_signed_half_table_restrict_resultvaluemasklookupvaluedecode))) /\ ((dst_positive_table_restrict_resultvaluemasklookup) + ge_balance_negative_table_restrict_resultvaluemasklookupvalue = (dst_negative_table_restrict_resultvaluemasklookup) + ge_balance_positive_table_restrict_resultvaluemasklookupvalue))))))))) -> ((((~((dc_index_table_restrict_resultvaluemask)=0)) /\ (exists dc_quotient_table_restrict_resultvaluemaskentry dc_left_table_restrict_resultvaluemaskentry dc_right_table_restrict_resultvaluemaskentry. (((dc_input_table_restrict_result)=(dc_index_table_restrict_resultvaluemask)*dc_quotient_table_restrict_resultvaluemaskentry) /\ (((exists dst_positive_code_table_restrict_resultvaluemaskentryleft dst_positive_scale_table_restrict_resultvaluemaskentryleft dst_negative_code_table_restrict_resultvaluemaskentryleft dst_negative_scale_table_restrict_resultvaluemaskentryleft dst_positive_table_restrict_resultvaluemaskentryleft dst_negative_table_restrict_resultvaluemaskentryleft. (((F) = (((((dst_positive_code_table_restrict_resultvaluemaskentryleft) + (dst_positive_scale_table_restrict_resultvaluemaskentryleft)) * S ((dst_positive_code_table_restrict_resultvaluemaskentryleft) + (dst_positive_scale_table_restrict_resultvaluemaskentryleft)) + ((dst_positive_scale_table_restrict_resultvaluemaskentryleft) + (dst_positive_scale_table_restrict_resultvaluemaskentryleft))) + (((dst_negative_code_table_restrict_resultvaluemaskentryleft) + (dst_negative_scale_table_restrict_resultvaluemaskentryleft)) * S ((dst_negative_code_table_restrict_resultvaluemaskentryleft) + (dst_negative_scale_table_restrict_resultvaluemaskentryleft)) + ((dst_negative_scale_table_restrict_resultvaluemaskentryleft) + (dst_negative_scale_table_restrict_resultvaluemaskentryleft)))) * S ((((dst_positive_code_table_restrict_resultvaluemaskentryleft) + (dst_positive_scale_table_restrict_resultvaluemaskentryleft)) * S ((dst_positive_code_table_restrict_resultvaluemaskentryleft) + (dst_positive_scale_table_restrict_resultvaluemaskentryleft)) + ((dst_positive_scale_table_restrict_resultvaluemaskentryleft) + (dst_positive_scale_table_restrict_resultvaluemaskentryleft))) + (((dst_negative_code_table_restrict_resultvaluemaskentryleft) + (dst_negative_scale_table_restrict_resultvaluemaskentryleft)) * S ((dst_negative_code_table_restrict_resultvaluemaskentryleft) + (dst_negative_scale_table_restrict_resultvaluemaskentryleft)) + ((dst_negative_scale_table_restrict_resultvaluemaskentryleft) + (dst_negative_scale_table_restrict_resultvaluemaskentryleft)))) + ((((dst_negative_code_table_restrict_resultvaluemaskentryleft) + (dst_negative_scale_table_restrict_resultvaluemaskentryleft)) * S ((dst_negative_code_table_restrict_resultvaluemaskentryleft) + (dst_negative_scale_table_restrict_resultvaluemaskentryleft)) + ((dst_negative_scale_table_restrict_resultvaluemaskentryleft) + (dst_negative_scale_table_restrict_resultvaluemaskentryleft))) + (((dst_negative_code_table_restrict_resultvaluemaskentryleft) + (dst_negative_scale_table_restrict_resultvaluemaskentryleft)) * S ((dst_negative_code_table_restrict_resultvaluemaskentryleft) + (dst_negative_scale_table_restrict_resultvaluemaskentryleft)) + ((dst_negative_scale_table_restrict_resultvaluemaskentryleft) + (dst_negative_scale_table_restrict_resultvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_table_restrict_resultvaluemaskentryleftpositive. ff_h_pvs_table_restrict_resultvaluemaskentryleftpositive + S (dst_positive_table_restrict_resultvaluemaskentryleft) = S ((S (dc_index_table_restrict_resultvaluemask)) * dst_positive_scale_table_restrict_resultvaluemaskentryleft)) /\ exists ff_q_pvs_table_restrict_resultvaluemaskentryleftpositive. dst_positive_code_table_restrict_resultvaluemaskentryleft = ff_q_pvs_table_restrict_resultvaluemaskentryleftpositive * S ((S (dc_index_table_restrict_resultvaluemask)) * dst_positive_scale_table_restrict_resultvaluemaskentryleft) + (dst_positive_table_restrict_resultvaluemaskentryleft))) /\ (((((exists ff_h_pvs_table_restrict_resultvaluemaskentryleftnegative. ff_h_pvs_table_restrict_resultvaluemaskentryleftnegative + S (dst_negative_table_restrict_resultvaluemaskentryleft) = S ((S (dc_index_table_restrict_resultvaluemask)) * dst_negative_scale_table_restrict_resultvaluemaskentryleft)) /\ exists ff_q_pvs_table_restrict_resultvaluemaskentryleftnegative. dst_negative_code_table_restrict_resultvaluemaskentryleft = ff_q_pvs_table_restrict_resultvaluemaskentryleftnegative * S ((S (dc_index_table_restrict_resultvaluemask)) * dst_negative_scale_table_restrict_resultvaluemaskentryleft) + (dst_negative_table_restrict_resultvaluemaskentryleft))) /\ (exists ge_balance_positive_table_restrict_resultvaluemaskentryleftvalue ge_balance_negative_table_restrict_resultvaluemaskentryleftvalue. (((((dc_left_table_restrict_resultvaluemaskentry) = 2 * (ge_balance_positive_table_restrict_resultvaluemaskentryleftvalue) /\ (ge_balance_negative_table_restrict_resultvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_table_restrict_resultvaluemaskentryleftvaluedecode. (((dc_left_table_restrict_resultvaluemaskentry) = 2 * ge_signed_half_table_restrict_resultvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_table_restrict_resultvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_table_restrict_resultvaluemaskentryleftvalue) = S ge_signed_half_table_restrict_resultvaluemaskentryleftvaluedecode))) /\ ((dst_positive_table_restrict_resultvaluemaskentryleft) + ge_balance_negative_table_restrict_resultvaluemaskentryleftvalue = (dst_negative_table_restrict_resultvaluemaskentryleft) + ge_balance_positive_table_restrict_resultvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_table_restrict_resultvaluemaskentryright dst_positive_scale_table_restrict_resultvaluemaskentryright dst_negative_code_table_restrict_resultvaluemaskentryright dst_negative_scale_table_restrict_resultvaluemaskentryright dst_positive_table_restrict_resultvaluemaskentryright dst_negative_table_restrict_resultvaluemaskentryright. (((G) = (((((dst_positive_code_table_restrict_resultvaluemaskentryright) + (dst_positive_scale_table_restrict_resultvaluemaskentryright)) * S ((dst_positive_code_table_restrict_resultvaluemaskentryright) + (dst_positive_scale_table_restrict_resultvaluemaskentryright)) + ((dst_positive_scale_table_restrict_resultvaluemaskentryright) + (dst_positive_scale_table_restrict_resultvaluemaskentryright))) + (((dst_negative_code_table_restrict_resultvaluemaskentryright) + (dst_negative_scale_table_restrict_resultvaluemaskentryright)) * S ((dst_negative_code_table_restrict_resultvaluemaskentryright) + (dst_negative_scale_table_restrict_resultvaluemaskentryright)) + ((dst_negative_scale_table_restrict_resultvaluemaskentryright) + (dst_negative_scale_table_restrict_resultvaluemaskentryright)))) * S ((((dst_positive_code_table_restrict_resultvaluemaskentryright) + (dst_positive_scale_table_restrict_resultvaluemaskentryright)) * S ((dst_positive_code_table_restrict_resultvaluemaskentryright) + (dst_positive_scale_table_restrict_resultvaluemaskentryright)) + ((dst_positive_scale_table_restrict_resultvaluemaskentryright) + (dst_positive_scale_table_restrict_resultvaluemaskentryright))) + (((dst_negative_code_table_restrict_resultvaluemaskentryright) + (dst_negative_scale_table_restrict_resultvaluemaskentryright)) * S ((dst_negative_code_table_restrict_resultvaluemaskentryright) + (dst_negative_scale_table_restrict_resultvaluemaskentryright)) + ((dst_negative_scale_table_restrict_resultvaluemaskentryright) + (dst_negative_scale_table_restrict_resultvaluemaskentryright)))) + ((((dst_negative_code_table_restrict_resultvaluemaskentryright) + (dst_negative_scale_table_restrict_resultvaluemaskentryright)) * S ((dst_negative_code_table_restrict_resultvaluemaskentryright) + (dst_negative_scale_table_restrict_resultvaluemaskentryright)) + ((dst_negative_scale_table_restrict_resultvaluemaskentryright) + (dst_negative_scale_table_restrict_resultvaluemaskentryright))) + (((dst_negative_code_table_restrict_resultvaluemaskentryright) + (dst_negative_scale_table_restrict_resultvaluemaskentryright)) * S ((dst_negative_code_table_restrict_resultvaluemaskentryright) + (dst_negative_scale_table_restrict_resultvaluemaskentryright)) + ((dst_negative_scale_table_restrict_resultvaluemaskentryright) + (dst_negative_scale_table_restrict_resultvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_table_restrict_resultvaluemaskentryrightpositive. ff_h_pvs_table_restrict_resultvaluemaskentryrightpositive + S (dst_positive_table_restrict_resultvaluemaskentryright) = S ((S (dc_quotient_table_restrict_resultvaluemaskentry)) * dst_positive_scale_table_restrict_resultvaluemaskentryright)) /\ exists ff_q_pvs_table_restrict_resultvaluemaskentryrightpositive. dst_positive_code_table_restrict_resultvaluemaskentryright = ff_q_pvs_table_restrict_resultvaluemaskentryrightpositive * S ((S (dc_quotient_table_restrict_resultvaluemaskentry)) * dst_positive_scale_table_restrict_resultvaluemaskentryright) + (dst_positive_table_restrict_resultvaluemaskentryright))) /\ (((((exists ff_h_pvs_table_restrict_resultvaluemaskentryrightnegative. ff_h_pvs_table_restrict_resultvaluemaskentryrightnegative + S (dst_negative_table_restrict_resultvaluemaskentryright) = S ((S (dc_quotient_table_restrict_resultvaluemaskentry)) * dst_negative_scale_table_restrict_resultvaluemaskentryright)) /\ exists ff_q_pvs_table_restrict_resultvaluemaskentryrightnegative. dst_negative_code_table_restrict_resultvaluemaskentryright = ff_q_pvs_table_restrict_resultvaluemaskentryrightnegative * S ((S (dc_quotient_table_restrict_resultvaluemaskentry)) * dst_negative_scale_table_restrict_resultvaluemaskentryright) + (dst_negative_table_restrict_resultvaluemaskentryright))) /\ (exists ge_balance_positive_table_restrict_resultvaluemaskentryrightvalue ge_balance_negative_table_restrict_resultvaluemaskentryrightvalue. (((((dc_right_table_restrict_resultvaluemaskentry) = 2 * (ge_balance_positive_table_restrict_resultvaluemaskentryrightvalue) /\ (ge_balance_negative_table_restrict_resultvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_table_restrict_resultvaluemaskentryrightvaluedecode. (((dc_right_table_restrict_resultvaluemaskentry) = 2 * ge_signed_half_table_restrict_resultvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_table_restrict_resultvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_table_restrict_resultvaluemaskentryrightvalue) = S ge_signed_half_table_restrict_resultvaluemaskentryrightvaluedecode))) /\ ((dst_positive_table_restrict_resultvaluemaskentryright) + ge_balance_negative_table_restrict_resultvaluemaskentryrightvalue = (dst_negative_table_restrict_resultvaluemaskentryright) + ge_balance_positive_table_restrict_resultvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_table_restrict_resultvaluemaskentryproduct sto_an_table_restrict_resultvaluemaskentryproduct sto_bp_table_restrict_resultvaluemaskentryproduct sto_bn_table_restrict_resultvaluemaskentryproduct sto_cp_table_restrict_resultvaluemaskentryproduct sto_cn_table_restrict_resultvaluemaskentryproduct. (((((dc_left_table_restrict_resultvaluemaskentry) = 2 * (sto_ap_table_restrict_resultvaluemaskentryproduct) /\ (sto_an_table_restrict_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_restrict_resultvaluemaskentryproductleft. (((dc_left_table_restrict_resultvaluemaskentry) = 2 * ge_signed_half_table_restrict_resultvaluemaskentryproductleft + 1 /\ (sto_ap_table_restrict_resultvaluemaskentryproduct) = 0) /\ (sto_an_table_restrict_resultvaluemaskentryproduct) = S ge_signed_half_table_restrict_resultvaluemaskentryproductleft))) /\ ((((((dc_right_table_restrict_resultvaluemaskentry) = 2 * (sto_bp_table_restrict_resultvaluemaskentryproduct) /\ (sto_bn_table_restrict_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_restrict_resultvaluemaskentryproductright. (((dc_right_table_restrict_resultvaluemaskentry) = 2 * ge_signed_half_table_restrict_resultvaluemaskentryproductright + 1 /\ (sto_bp_table_restrict_resultvaluemaskentryproduct) = 0) /\ (sto_bn_table_restrict_resultvaluemaskentryproduct) = S ge_signed_half_table_restrict_resultvaluemaskentryproductright))) /\ ((((((dc_value_table_restrict_resultvaluemask) = 2 * (sto_cp_table_restrict_resultvaluemaskentryproduct) /\ (sto_cn_table_restrict_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_restrict_resultvaluemaskentryproductoutput. (((dc_value_table_restrict_resultvaluemask) = 2 * ge_signed_half_table_restrict_resultvaluemaskentryproductoutput + 1 /\ (sto_cp_table_restrict_resultvaluemaskentryproduct) = 0) /\ (sto_cn_table_restrict_resultvaluemaskentryproduct) = S ge_signed_half_table_restrict_resultvaluemaskentryproductoutput))) /\ ((sto_ap_table_restrict_resultvaluemaskentryproduct * sto_bp_table_restrict_resultvaluemaskentryproduct + sto_an_table_restrict_resultvaluemaskentryproduct * sto_bn_table_restrict_resultvaluemaskentryproduct) + sto_cn_table_restrict_resultvaluemaskentryproduct = (sto_ap_table_restrict_resultvaluemaskentryproduct * sto_bn_table_restrict_resultvaluemaskentryproduct + sto_an_table_restrict_resultvaluemaskentryproduct * sto_bp_table_restrict_resultvaluemaskentryproduct) + sto_cp_table_restrict_resultvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_table_restrict_resultvaluemask)=0 \/ ~(exists pvs_factor_table_restrict_resultvaluemaskentrynondivisor. (dc_input_table_restrict_result) = (dc_index_table_restrict_resultvaluemask) * pvs_factor_table_restrict_resultvaluemaskentrynondivisor)) /\ ((dc_value_table_restrict_resultvaluemask)=0))))))) /\ (exists dst_positive_code_table_restrict_resultvaluefold dst_positive_scale_table_restrict_resultvaluefold dst_negative_code_table_restrict_resultvaluefold dst_negative_scale_table_restrict_resultvaluefold dst_positive_sum_table_restrict_resultvaluefold dst_negative_sum_table_restrict_resultvaluefold. (((dc_mask_table_restrict_resultvalue) = (((((dst_positive_code_table_restrict_resultvaluefold) + (dst_positive_scale_table_restrict_resultvaluefold)) * S ((dst_positive_code_table_restrict_resultvaluefold) + (dst_positive_scale_table_restrict_resultvaluefold)) + ((dst_positive_scale_table_restrict_resultvaluefold) + (dst_positive_scale_table_restrict_resultvaluefold))) + (((dst_negative_code_table_restrict_resultvaluefold) + (dst_negative_scale_table_restrict_resultvaluefold)) * S ((dst_negative_code_table_restrict_resultvaluefold) + (dst_negative_scale_table_restrict_resultvaluefold)) + ((dst_negative_scale_table_restrict_resultvaluefold) + (dst_negative_scale_table_restrict_resultvaluefold)))) * S ((((dst_positive_code_table_restrict_resultvaluefold) + (dst_positive_scale_table_restrict_resultvaluefold)) * S ((dst_positive_code_table_restrict_resultvaluefold) + (dst_positive_scale_table_restrict_resultvaluefold)) + ((dst_positive_scale_table_restrict_resultvaluefold) + (dst_positive_scale_table_restrict_resultvaluefold))) + (((dst_negative_code_table_restrict_resultvaluefold) + (dst_negative_scale_table_restrict_resultvaluefold)) * S ((dst_negative_code_table_restrict_resultvaluefold) + (dst_negative_scale_table_restrict_resultvaluefold)) + ((dst_negative_scale_table_restrict_resultvaluefold) + (dst_negative_scale_table_restrict_resultvaluefold)))) + ((((dst_negative_code_table_restrict_resultvaluefold) + (dst_negative_scale_table_restrict_resultvaluefold)) * S ((dst_negative_code_table_restrict_resultvaluefold) + (dst_negative_scale_table_restrict_resultvaluefold)) + ((dst_negative_scale_table_restrict_resultvaluefold) + (dst_negative_scale_table_restrict_resultvaluefold))) + (((dst_negative_code_table_restrict_resultvaluefold) + (dst_negative_scale_table_restrict_resultvaluefold)) * S ((dst_negative_code_table_restrict_resultvaluefold) + (dst_negative_scale_table_restrict_resultvaluefold)) + ((dst_negative_scale_table_restrict_resultvaluefold) + (dst_negative_scale_table_restrict_resultvaluefold)))))) /\ (((exists fs_u_dst_table_restrict_resultvaluefoldpositive fs_v_dst_table_restrict_resultvaluefoldpositive. ((((exists fs_h_dst_table_restrict_resultvaluefoldpositive_body_start. fs_h_dst_table_restrict_resultvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_table_restrict_resultvaluefoldpositive)) /\ exists fs_q_dst_table_restrict_resultvaluefoldpositive_body_start. fs_u_dst_table_restrict_resultvaluefoldpositive = fs_q_dst_table_restrict_resultvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_table_restrict_resultvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_table_restrict_resultvaluefoldpositive_body_terminal. fs_h_dst_table_restrict_resultvaluefoldpositive_body_terminal + S (dst_positive_sum_table_restrict_resultvaluefold) = S ((S (S (dc_input_table_restrict_result))) * fs_v_dst_table_restrict_resultvaluefoldpositive)) /\ exists fs_q_dst_table_restrict_resultvaluefoldpositive_body_terminal. fs_u_dst_table_restrict_resultvaluefoldpositive = fs_q_dst_table_restrict_resultvaluefoldpositive_body_terminal * S ((S (S (dc_input_table_restrict_result))) * fs_v_dst_table_restrict_resultvaluefoldpositive) + (dst_positive_sum_table_restrict_resultvaluefold))) /\ forall fs_i_dst_table_restrict_resultvaluefoldpositive_body_steps. (exists fs_lt_dst_table_restrict_resultvaluefoldpositive_body_steps_bound. fs_lt_dst_table_restrict_resultvaluefoldpositive_body_steps_bound + S fs_i_dst_table_restrict_resultvaluefoldpositive_body_steps = S (dc_input_table_restrict_result)) -> exists fs_a_dst_table_restrict_resultvaluefoldpositive_body_steps fs_r_dst_table_restrict_resultvaluefoldpositive_body_steps fs_s_dst_table_restrict_resultvaluefoldpositive_body_steps. ((((exists fs_h_dst_table_restrict_resultvaluefoldpositive_body_steps_summand. fs_h_dst_table_restrict_resultvaluefoldpositive_body_steps_summand + S (fs_a_dst_table_restrict_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_restrict_resultvaluefoldpositive_body_steps)) * dst_positive_scale_table_restrict_resultvaluefold)) /\ exists fs_q_dst_table_restrict_resultvaluefoldpositive_body_steps_summand. dst_positive_code_table_restrict_resultvaluefold = fs_q_dst_table_restrict_resultvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_table_restrict_resultvaluefoldpositive_body_steps)) * dst_positive_scale_table_restrict_resultvaluefold) + (fs_a_dst_table_restrict_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_restrict_resultvaluefoldpositive_body_steps_partial. fs_h_dst_table_restrict_resultvaluefoldpositive_body_steps_partial + S (fs_r_dst_table_restrict_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_restrict_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_restrict_resultvaluefoldpositive)) /\ exists fs_q_dst_table_restrict_resultvaluefoldpositive_body_steps_partial. fs_u_dst_table_restrict_resultvaluefoldpositive = fs_q_dst_table_restrict_resultvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_table_restrict_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_restrict_resultvaluefoldpositive) + (fs_r_dst_table_restrict_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_restrict_resultvaluefoldpositive_body_steps_successor. fs_h_dst_table_restrict_resultvaluefoldpositive_body_steps_successor + S (fs_s_dst_table_restrict_resultvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_table_restrict_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_restrict_resultvaluefoldpositive)) /\ exists fs_q_dst_table_restrict_resultvaluefoldpositive_body_steps_successor. fs_u_dst_table_restrict_resultvaluefoldpositive = fs_q_dst_table_restrict_resultvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_table_restrict_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_restrict_resultvaluefoldpositive) + (fs_s_dst_table_restrict_resultvaluefoldpositive_body_steps))) /\ fs_s_dst_table_restrict_resultvaluefoldpositive_body_steps = fs_r_dst_table_restrict_resultvaluefoldpositive_body_steps + fs_a_dst_table_restrict_resultvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_table_restrict_resultvaluefoldnegative fs_v_dst_table_restrict_resultvaluefoldnegative. ((((exists fs_h_dst_table_restrict_resultvaluefoldnegative_body_start. fs_h_dst_table_restrict_resultvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_table_restrict_resultvaluefoldnegative)) /\ exists fs_q_dst_table_restrict_resultvaluefoldnegative_body_start. fs_u_dst_table_restrict_resultvaluefoldnegative = fs_q_dst_table_restrict_resultvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_table_restrict_resultvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_table_restrict_resultvaluefoldnegative_body_terminal. fs_h_dst_table_restrict_resultvaluefoldnegative_body_terminal + S (dst_negative_sum_table_restrict_resultvaluefold) = S ((S (S (dc_input_table_restrict_result))) * fs_v_dst_table_restrict_resultvaluefoldnegative)) /\ exists fs_q_dst_table_restrict_resultvaluefoldnegative_body_terminal. fs_u_dst_table_restrict_resultvaluefoldnegative = fs_q_dst_table_restrict_resultvaluefoldnegative_body_terminal * S ((S (S (dc_input_table_restrict_result))) * fs_v_dst_table_restrict_resultvaluefoldnegative) + (dst_negative_sum_table_restrict_resultvaluefold))) /\ forall fs_i_dst_table_restrict_resultvaluefoldnegative_body_steps. (exists fs_lt_dst_table_restrict_resultvaluefoldnegative_body_steps_bound. fs_lt_dst_table_restrict_resultvaluefoldnegative_body_steps_bound + S fs_i_dst_table_restrict_resultvaluefoldnegative_body_steps = S (dc_input_table_restrict_result)) -> exists fs_a_dst_table_restrict_resultvaluefoldnegative_body_steps fs_r_dst_table_restrict_resultvaluefoldnegative_body_steps fs_s_dst_table_restrict_resultvaluefoldnegative_body_steps. ((((exists fs_h_dst_table_restrict_resultvaluefoldnegative_body_steps_summand. fs_h_dst_table_restrict_resultvaluefoldnegative_body_steps_summand + S (fs_a_dst_table_restrict_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_restrict_resultvaluefoldnegative_body_steps)) * dst_negative_scale_table_restrict_resultvaluefold)) /\ exists fs_q_dst_table_restrict_resultvaluefoldnegative_body_steps_summand. dst_negative_code_table_restrict_resultvaluefold = fs_q_dst_table_restrict_resultvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_table_restrict_resultvaluefoldnegative_body_steps)) * dst_negative_scale_table_restrict_resultvaluefold) + (fs_a_dst_table_restrict_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_restrict_resultvaluefoldnegative_body_steps_partial. fs_h_dst_table_restrict_resultvaluefoldnegative_body_steps_partial + S (fs_r_dst_table_restrict_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_restrict_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_restrict_resultvaluefoldnegative)) /\ exists fs_q_dst_table_restrict_resultvaluefoldnegative_body_steps_partial. fs_u_dst_table_restrict_resultvaluefoldnegative = fs_q_dst_table_restrict_resultvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_table_restrict_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_restrict_resultvaluefoldnegative) + (fs_r_dst_table_restrict_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_restrict_resultvaluefoldnegative_body_steps_successor. fs_h_dst_table_restrict_resultvaluefoldnegative_body_steps_successor + S (fs_s_dst_table_restrict_resultvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_table_restrict_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_restrict_resultvaluefoldnegative)) /\ exists fs_q_dst_table_restrict_resultvaluefoldnegative_body_steps_successor. fs_u_dst_table_restrict_resultvaluefoldnegative = fs_q_dst_table_restrict_resultvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_table_restrict_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_restrict_resultvaluefoldnegative) + (fs_s_dst_table_restrict_resultvaluefoldnegative_body_steps))) /\ fs_s_dst_table_restrict_resultvaluefoldnegative_body_steps = fs_r_dst_table_restrict_resultvaluefoldnegative_body_steps + fs_a_dst_table_restrict_resultvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_table_restrict_resultvaluefoldresult ge_balance_negative_table_restrict_resultvaluefoldresult. (((((dc_output_table_restrict_result) = 2 * (ge_balance_positive_table_restrict_resultvaluefoldresult) /\ (ge_balance_negative_table_restrict_resultvaluefoldresult) = 0) \/ exists ge_signed_half_table_restrict_resultvaluefoldresultdecode. (((dc_output_table_restrict_result) = 2 * ge_signed_half_table_restrict_resultvaluefoldresultdecode + 1 /\ (ge_balance_positive_table_restrict_resultvaluefoldresult) = 0) /\ (ge_balance_negative_table_restrict_resultvaluefoldresult) = S ge_signed_half_table_restrict_resultvaluefoldresultdecode))) /\ ((dst_positive_sum_table_restrict_resultvaluefold) + ge_balance_negative_table_restrict_resultvaluefoldresult = (dst_negative_sum_table_restrict_resultvaluefold) + ge_balance_positive_table_restrict_resultvaluefoldresult))))))))))))))))))))Complete tactic proof in conservative notation
All 47 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
47 script commands · 10 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
01Fix variables and assumptionsL1–7
02Separate the logical casesL8–11
03Use earlier factsL12–17
04Separate the logical casesL18–18
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L18
split
05Use earlier factsL19–24
06Separate the logical casesL25–25
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L25
split
07Use earlier factsL26–31
Instantiate or apply named facts and discharge the corresponding proof obligations.
08Fix variables and assumptionsL32–36
09Use earlier factsL37–46
Instantiate or apply named facts and discharge the corresponding proof obligations.
10Use earlier factsL47–47
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L47
exact hz
Original defined command ledger · 47 lines
- 0001
intro N - 0002
intro J - 0003
intro F - 0004
intro G - 0005
intro H - 0006
intro hc - 0007
intro hJN - 0008
cases hc - 0009
cases hc_right - 0010
cases hc_right_right - 0011
split - 0012
specialize divisor_signed_table_restrict (N) - 0013
specialize divisor_signed_table_restrict (J) - 0014
specialize divisor_signed_table_restrict (F) - 0015
apply divisor_signed_table_restrict - 0016
exact hc_left - 0017
exact hJN - 0018
split - 0019
specialize divisor_signed_table_restrict (N) - 0020
specialize divisor_signed_table_restrict (J) - 0021
specialize divisor_signed_table_restrict (G) - 0022
apply divisor_signed_table_restrict - 0023
exact hc_right_left - 0024
exact hJN - 0025
split - 0026
specialize divisor_signed_table_restrict (N) - 0027
specialize divisor_signed_table_restrict (J) - 0028
specialize divisor_signed_table_restrict (H) - 0029
apply divisor_signed_table_restrict - 0030
exact hc_right_right_left - 0031
exact hJN - 0032
intro n - 0033
intro z - 0034
intro hn - 0035
intro hnJ - 0036
intro hz - 0037
specialize hc_right_right_right (n) - 0038
specialize hc_right_right_right (z) - 0039
apply hc_right_right_right - 0040
exact hn - 0041
specialize le_trans (n) - 0042
specialize le_trans (J) - 0043
specialize le_trans (N) - 0044
apply le_trans - 0045
exact hnJ - 0046
exact hJN - 0047
exact hz