signed_prefix_sum_pointwise_add

Exact expanded first-order arithmetic statement

forall l F G H a b c. (((exists dst_positive_code_linearity_pointwiseleft_table dst_positive_scale_linearity_pointwiseleft_table dst_negative_code_linearity_pointwiseleft_table dst_negative_scale_linearity_pointwiseleft_table. (((F) = (((((dst_positive_code_linearity_pointwiseleft_table) + (dst_positive_scale_linearity_pointwiseleft_table)) * S ((dst_positive_code_linearity_pointwiseleft_table) + (dst_positive_scale_linearity_pointwiseleft_table)) + ((dst_positive_scale_linearity_pointwiseleft_table) + (dst_positive_scale_linearity_pointwiseleft_table))) + (((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) * S ((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) + ((dst_negative_scale_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)))) * S ((((dst_positive_code_linearity_pointwiseleft_table) + (dst_positive_scale_linearity_pointwiseleft_table)) * S ((dst_positive_code_linearity_pointwiseleft_table) + (dst_positive_scale_linearity_pointwiseleft_table)) + ((dst_positive_scale_linearity_pointwiseleft_table) + (dst_positive_scale_linearity_pointwiseleft_table))) + (((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) * S ((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) + ((dst_negative_scale_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)))) + ((((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) * S ((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) + ((dst_negative_scale_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table))) + (((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) * S ((dst_negative_code_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)) + ((dst_negative_scale_linearity_pointwiseleft_table) + (dst_negative_scale_linearity_pointwiseleft_table)))))) /\ (forall dst_index_linearity_pointwiseleft_table. (exists pvs_le_gap_linearity_pointwiseleft_tabledomain. pvs_le_gap_linearity_pointwiseleft_tabledomain + (dst_index_linearity_pointwiseleft_table) = (l)) -> exists dst_positive_linearity_pointwiseleft_table dst_negative_linearity_pointwiseleft_table dst_value_linearity_pointwiseleft_table. ((((exists ff_h_pvs_linearity_pointwiseleft_tableentrypositive. ff_h_pvs_linearity_pointwiseleft_tableentrypositive + S (dst_positive_linearity_pointwiseleft_table) = S ((S (dst_index_linearity_pointwiseleft_table)) * dst_positive_scale_linearity_pointwiseleft_table)) /\ exists ff_q_pvs_linearity_pointwiseleft_tableentrypositive. dst_positive_code_linearity_pointwiseleft_table = ff_q_pvs_linearity_pointwiseleft_tableentrypositive * S ((S (dst_index_linearity_pointwiseleft_table)) * dst_positive_scale_linearity_pointwiseleft_table) + (dst_positive_linearity_pointwiseleft_table))) /\ (((((exists ff_h_pvs_linearity_pointwiseleft_tableentrynegative. ff_h_pvs_linearity_pointwiseleft_tableentrynegative + S (dst_negative_linearity_pointwiseleft_table) = S ((S (dst_index_linearity_pointwiseleft_table)) * dst_negative_scale_linearity_pointwiseleft_table)) /\ exists ff_q_pvs_linearity_pointwiseleft_tableentrynegative. dst_negative_code_linearity_pointwiseleft_table = ff_q_pvs_linearity_pointwiseleft_tableentrynegative * S ((S (dst_index_linearity_pointwiseleft_table)) * dst_negative_scale_linearity_pointwiseleft_table) + (dst_negative_linearity_pointwiseleft_table))) /\ (exists ge_balance_positive_linearity_pointwiseleft_tableentryvalue ge_balance_negative_linearity_pointwiseleft_tableentryvalue. (((((dst_value_linearity_pointwiseleft_table) = 2 * (ge_balance_positive_linearity_pointwiseleft_tableentryvalue) /\ (ge_balance_negative_linearity_pointwiseleft_tableentryvalue) = 0) \/ exists ge_signed_half_linearity_pointwiseleft_tableentryvaluedecode. (((dst_value_linearity_pointwiseleft_table) = 2 * ge_signed_half_linearity_pointwiseleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_linearity_pointwiseleft_tableentryvalue) = 0) /\ (ge_balance_negative_linearity_pointwiseleft_tableentryvalue) = S ge_signed_half_linearity_pointwiseleft_tableentryvaluedecode))) /\ ((dst_positive_linearity_pointwiseleft_table) + ge_balance_negative_linearity_pointwiseleft_tableentryvalue = (dst_negative_linearity_pointwiseleft_table) + ge_balance_positive_linearity_pointwiseleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_linearity_pointwiseright_table dst_positive_scale_linearity_pointwiseright_table dst_negative_code_linearity_pointwiseright_table dst_negative_scale_linearity_pointwiseright_table. (((G) = (((((dst_positive_code_linearity_pointwiseright_table) + (dst_positive_scale_linearity_pointwiseright_table)) * S ((dst_positive_code_linearity_pointwiseright_table) + (dst_positive_scale_linearity_pointwiseright_table)) + ((dst_positive_scale_linearity_pointwiseright_table) + (dst_positive_scale_linearity_pointwiseright_table))) + (((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) * S ((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) + ((dst_negative_scale_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)))) * S ((((dst_positive_code_linearity_pointwiseright_table) + (dst_positive_scale_linearity_pointwiseright_table)) * S ((dst_positive_code_linearity_pointwiseright_table) + (dst_positive_scale_linearity_pointwiseright_table)) + ((dst_positive_scale_linearity_pointwiseright_table) + (dst_positive_scale_linearity_pointwiseright_table))) + (((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) * S ((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) + ((dst_negative_scale_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)))) + ((((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) * S ((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) + ((dst_negative_scale_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table))) + (((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) * S ((dst_negative_code_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)) + ((dst_negative_scale_linearity_pointwiseright_table) + (dst_negative_scale_linearity_pointwiseright_table)))))) /\ (forall dst_index_linearity_pointwiseright_table. (exists pvs_le_gap_linearity_pointwiseright_tabledomain. pvs_le_gap_linearity_pointwiseright_tabledomain + (dst_index_linearity_pointwiseright_table) = (l)) -> exists dst_positive_linearity_pointwiseright_table dst_negative_linearity_pointwiseright_table dst_value_linearity_pointwiseright_table. ((((exists ff_h_pvs_linearity_pointwiseright_tableentrypositive. ff_h_pvs_linearity_pointwiseright_tableentrypositive + S (dst_positive_linearity_pointwiseright_table) = S ((S (dst_index_linearity_pointwiseright_table)) * dst_positive_scale_linearity_pointwiseright_table)) /\ exists ff_q_pvs_linearity_pointwiseright_tableentrypositive. dst_positive_code_linearity_pointwiseright_table = ff_q_pvs_linearity_pointwiseright_tableentrypositive * S ((S (dst_index_linearity_pointwiseright_table)) * dst_positive_scale_linearity_pointwiseright_table) + (dst_positive_linearity_pointwiseright_table))) /\ (((((exists ff_h_pvs_linearity_pointwiseright_tableentrynegative. ff_h_pvs_linearity_pointwiseright_tableentrynegative + S (dst_negative_linearity_pointwiseright_table) = S ((S (dst_index_linearity_pointwiseright_table)) * dst_negative_scale_linearity_pointwiseright_table)) /\ exists ff_q_pvs_linearity_pointwiseright_tableentrynegative. dst_negative_code_linearity_pointwiseright_table = ff_q_pvs_linearity_pointwiseright_tableentrynegative * S ((S (dst_index_linearity_pointwiseright_table)) * dst_negative_scale_linearity_pointwiseright_table) + (dst_negative_linearity_pointwiseright_table))) /\ (exists ge_balance_positive_linearity_pointwiseright_tableentryvalue ge_balance_negative_linearity_pointwiseright_tableentryvalue. (((((dst_value_linearity_pointwiseright_table) = 2 * (ge_balance_positive_linearity_pointwiseright_tableentryvalue) /\ (ge_balance_negative_linearity_pointwiseright_tableentryvalue) = 0) \/ exists ge_signed_half_linearity_pointwiseright_tableentryvaluedecode. (((dst_value_linearity_pointwiseright_table) = 2 * ge_signed_half_linearity_pointwiseright_tableentryvaluedecode + 1 /\ (ge_balance_positive_linearity_pointwiseright_tableentryvalue) = 0) /\ (ge_balance_negative_linearity_pointwiseright_tableentryvalue) = S ge_signed_half_linearity_pointwiseright_tableentryvaluedecode))) /\ ((dst_positive_linearity_pointwiseright_table) + ge_balance_negative_linearity_pointwiseright_tableentryvalue = (dst_negative_linearity_pointwiseright_table) + ge_balance_positive_linearity_pointwiseright_tableentryvalue))))))))) /\ (((exists dst_positive_code_linearity_pointwiseoutput_table dst_positive_scale_linearity_pointwiseoutput_table dst_negative_code_linearity_pointwiseoutput_table dst_negative_scale_linearity_pointwiseoutput_table. (((H) = (((((dst_positive_code_linearity_pointwiseoutput_table) + (dst_positive_scale_linearity_pointwiseoutput_table)) * S ((dst_positive_code_linearity_pointwiseoutput_table) + (dst_positive_scale_linearity_pointwiseoutput_table)) + ((dst_positive_scale_linearity_pointwiseoutput_table) + (dst_positive_scale_linearity_pointwiseoutput_table))) + (((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) * S ((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) + ((dst_negative_scale_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)))) * S ((((dst_positive_code_linearity_pointwiseoutput_table) + (dst_positive_scale_linearity_pointwiseoutput_table)) * S ((dst_positive_code_linearity_pointwiseoutput_table) + (dst_positive_scale_linearity_pointwiseoutput_table)) + ((dst_positive_scale_linearity_pointwiseoutput_table) + (dst_positive_scale_linearity_pointwiseoutput_table))) + (((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) * S ((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) + ((dst_negative_scale_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)))) + ((((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) * S ((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) + ((dst_negative_scale_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table))) + (((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) * S ((dst_negative_code_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)) + ((dst_negative_scale_linearity_pointwiseoutput_table) + (dst_negative_scale_linearity_pointwiseoutput_table)))))) /\ (forall dst_index_linearity_pointwiseoutput_table. (exists pvs_le_gap_linearity_pointwiseoutput_tabledomain. pvs_le_gap_linearity_pointwiseoutput_tabledomain + (dst_index_linearity_pointwiseoutput_table) = (l)) -> exists dst_positive_linearity_pointwiseoutput_table dst_negative_linearity_pointwiseoutput_table dst_value_linearity_pointwiseoutput_table. ((((exists ff_h_pvs_linearity_pointwiseoutput_tableentrypositive. ff_h_pvs_linearity_pointwiseoutput_tableentrypositive + S (dst_positive_linearity_pointwiseoutput_table) = S ((S (dst_index_linearity_pointwiseoutput_table)) * dst_positive_scale_linearity_pointwiseoutput_table)) /\ exists ff_q_pvs_linearity_pointwiseoutput_tableentrypositive. dst_positive_code_linearity_pointwiseoutput_table = ff_q_pvs_linearity_pointwiseoutput_tableentrypositive * S ((S (dst_index_linearity_pointwiseoutput_table)) * dst_positive_scale_linearity_pointwiseoutput_table) + (dst_positive_linearity_pointwiseoutput_table))) /\ (((((exists ff_h_pvs_linearity_pointwiseoutput_tableentrynegative. ff_h_pvs_linearity_pointwiseoutput_tableentrynegative + S (dst_negative_linearity_pointwiseoutput_table) = S ((S (dst_index_linearity_pointwiseoutput_table)) * dst_negative_scale_linearity_pointwiseoutput_table)) /\ exists ff_q_pvs_linearity_pointwiseoutput_tableentrynegative. dst_negative_code_linearity_pointwiseoutput_table = ff_q_pvs_linearity_pointwiseoutput_tableentrynegative * S ((S (dst_index_linearity_pointwiseoutput_table)) * dst_negative_scale_linearity_pointwiseoutput_table) + (dst_negative_linearity_pointwiseoutput_table))) /\ (exists ge_balance_positive_linearity_pointwiseoutput_tableentryvalue ge_balance_negative_linearity_pointwiseoutput_tableentryvalue. (((((dst_value_linearity_pointwiseoutput_table) = 2 * (ge_balance_positive_linearity_pointwiseoutput_tableentryvalue) /\ (ge_balance_negative_linearity_pointwiseoutput_tableentryvalue) = 0) \/ exists ge_signed_half_linearity_pointwiseoutput_tableentryvaluedecode. (((dst_value_linearity_pointwiseoutput_table) = 2 * ge_signed_half_linearity_pointwiseoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_linearity_pointwiseoutput_tableentryvalue) = 0) /\ (ge_balance_negative_linearity_pointwiseoutput_tableentryvalue) = S ge_signed_half_linearity_pointwiseoutput_tableentryvaluedecode))) /\ ((dst_positive_linearity_pointwiseoutput_table) + ge_balance_negative_linearity_pointwiseoutput_tableentryvalue = (dst_negative_linearity_pointwiseoutput_table) + ge_balance_positive_linearity_pointwiseoutput_tableentryvalue))))))))) /\ (forall sto_index_linearity_pointwiseentries. (exists pvs_gap_linearity_pointwiseentriesbound. pvs_gap_linearity_pointwiseentriesbound + S (sto_index_linearity_pointwiseentries) = (l)) -> exists sto_left_linearity_pointwiseentries sto_right_linearity_pointwiseentries sto_output_linearity_pointwiseentries. ((exists dst_positive_code_linearity_pointwiseentriesentryleft dst_positive_scale_linearity_pointwiseentriesentryleft dst_negative_code_linearity_pointwiseentriesentryleft dst_negative_scale_linearity_pointwiseentriesentryleft dst_positive_linearity_pointwiseentriesentryleft dst_negative_linearity_pointwiseentriesentryleft. (((F) = (((((dst_positive_code_linearity_pointwiseentriesentryleft) + (dst_positive_scale_linearity_pointwiseentriesentryleft)) * S ((dst_positive_code_linearity_pointwiseentriesentryleft) + (dst_positive_scale_linearity_pointwiseentriesentryleft)) + ((dst_positive_scale_linearity_pointwiseentriesentryleft) + (dst_positive_scale_linearity_pointwiseentriesentryleft))) + (((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) * S ((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) + ((dst_negative_scale_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)))) * S ((((dst_positive_code_linearity_pointwiseentriesentryleft) + (dst_positive_scale_linearity_pointwiseentriesentryleft)) * S ((dst_positive_code_linearity_pointwiseentriesentryleft) + (dst_positive_scale_linearity_pointwiseentriesentryleft)) + ((dst_positive_scale_linearity_pointwiseentriesentryleft) + (dst_positive_scale_linearity_pointwiseentriesentryleft))) + (((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) * S ((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) + ((dst_negative_scale_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)))) + ((((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) * S ((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) + ((dst_negative_scale_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft))) + (((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) * S ((dst_negative_code_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)) + ((dst_negative_scale_linearity_pointwiseentriesentryleft) + (dst_negative_scale_linearity_pointwiseentriesentryleft)))))) /\ (((((exists ff_h_pvs_linearity_pointwiseentriesentryleftpositive. ff_h_pvs_linearity_pointwiseentriesentryleftpositive + S (dst_positive_linearity_pointwiseentriesentryleft) = S ((S (sto_index_linearity_pointwiseentries)) * dst_positive_scale_linearity_pointwiseentriesentryleft)) /\ exists ff_q_pvs_linearity_pointwiseentriesentryleftpositive. dst_positive_code_linearity_pointwiseentriesentryleft = ff_q_pvs_linearity_pointwiseentriesentryleftpositive * S ((S (sto_index_linearity_pointwiseentries)) * dst_positive_scale_linearity_pointwiseentriesentryleft) + (dst_positive_linearity_pointwiseentriesentryleft))) /\ (((((exists ff_h_pvs_linearity_pointwiseentriesentryleftnegative. ff_h_pvs_linearity_pointwiseentriesentryleftnegative + S (dst_negative_linearity_pointwiseentriesentryleft) = S ((S (sto_index_linearity_pointwiseentries)) * dst_negative_scale_linearity_pointwiseentriesentryleft)) /\ exists ff_q_pvs_linearity_pointwiseentriesentryleftnegative. dst_negative_code_linearity_pointwiseentriesentryleft = ff_q_pvs_linearity_pointwiseentriesentryleftnegative * S ((S (sto_index_linearity_pointwiseentries)) * dst_negative_scale_linearity_pointwiseentriesentryleft) + (dst_negative_linearity_pointwiseentriesentryleft))) /\ (exists ge_balance_positive_linearity_pointwiseentriesentryleftvalue ge_balance_negative_linearity_pointwiseentriesentryleftvalue. (((((sto_left_linearity_pointwiseentries) = 2 * (ge_balance_positive_linearity_pointwiseentriesentryleftvalue) /\ (ge_balance_negative_linearity_pointwiseentriesentryleftvalue) = 0) \/ exists ge_signed_half_linearity_pointwiseentriesentryleftvaluedecode. (((sto_left_linearity_pointwiseentries) = 2 * ge_signed_half_linearity_pointwiseentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_linearity_pointwiseentriesentryleftvalue) = 0) /\ (ge_balance_negative_linearity_pointwiseentriesentryleftvalue) = S ge_signed_half_linearity_pointwiseentriesentryleftvaluedecode))) /\ ((dst_positive_linearity_pointwiseentriesentryleft) + ge_balance_negative_linearity_pointwiseentriesentryleftvalue = (dst_negative_linearity_pointwiseentriesentryleft) + ge_balance_positive_linearity_pointwiseentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_linearity_pointwiseentriesentryright dst_positive_scale_linearity_pointwiseentriesentryright dst_negative_code_linearity_pointwiseentriesentryright dst_negative_scale_linearity_pointwiseentriesentryright dst_positive_linearity_pointwiseentriesentryright dst_negative_linearity_pointwiseentriesentryright. (((G) = (((((dst_positive_code_linearity_pointwiseentriesentryright) + (dst_positive_scale_linearity_pointwiseentriesentryright)) * S ((dst_positive_code_linearity_pointwiseentriesentryright) + (dst_positive_scale_linearity_pointwiseentriesentryright)) + ((dst_positive_scale_linearity_pointwiseentriesentryright) + (dst_positive_scale_linearity_pointwiseentriesentryright))) + (((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) * S ((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) + ((dst_negative_scale_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)))) * S ((((dst_positive_code_linearity_pointwiseentriesentryright) + (dst_positive_scale_linearity_pointwiseentriesentryright)) * S ((dst_positive_code_linearity_pointwiseentriesentryright) + (dst_positive_scale_linearity_pointwiseentriesentryright)) + ((dst_positive_scale_linearity_pointwiseentriesentryright) + (dst_positive_scale_linearity_pointwiseentriesentryright))) + (((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) * S ((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) + ((dst_negative_scale_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)))) + ((((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) * S ((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) + ((dst_negative_scale_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright))) + (((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) * S ((dst_negative_code_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)) + ((dst_negative_scale_linearity_pointwiseentriesentryright) + (dst_negative_scale_linearity_pointwiseentriesentryright)))))) /\ (((((exists ff_h_pvs_linearity_pointwiseentriesentryrightpositive. ff_h_pvs_linearity_pointwiseentriesentryrightpositive + S (dst_positive_linearity_pointwiseentriesentryright) = S ((S (sto_index_linearity_pointwiseentries)) * dst_positive_scale_linearity_pointwiseentriesentryright)) /\ exists ff_q_pvs_linearity_pointwiseentriesentryrightpositive. dst_positive_code_linearity_pointwiseentriesentryright = ff_q_pvs_linearity_pointwiseentriesentryrightpositive * S ((S (sto_index_linearity_pointwiseentries)) * dst_positive_scale_linearity_pointwiseentriesentryright) + (dst_positive_linearity_pointwiseentriesentryright))) /\ (((((exists ff_h_pvs_linearity_pointwiseentriesentryrightnegative. ff_h_pvs_linearity_pointwiseentriesentryrightnegative + S (dst_negative_linearity_pointwiseentriesentryright) = S ((S (sto_index_linearity_pointwiseentries)) * dst_negative_scale_linearity_pointwiseentriesentryright)) /\ exists ff_q_pvs_linearity_pointwiseentriesentryrightnegative. dst_negative_code_linearity_pointwiseentriesentryright = ff_q_pvs_linearity_pointwiseentriesentryrightnegative * S ((S (sto_index_linearity_pointwiseentries)) * dst_negative_scale_linearity_pointwiseentriesentryright) + (dst_negative_linearity_pointwiseentriesentryright))) /\ (exists ge_balance_positive_linearity_pointwiseentriesentryrightvalue ge_balance_negative_linearity_pointwiseentriesentryrightvalue. (((((sto_right_linearity_pointwiseentries) = 2 * (ge_balance_positive_linearity_pointwiseentriesentryrightvalue) /\ (ge_balance_negative_linearity_pointwiseentriesentryrightvalue) = 0) \/ exists ge_signed_half_linearity_pointwiseentriesentryrightvaluedecode. (((sto_right_linearity_pointwiseentries) = 2 * ge_signed_half_linearity_pointwiseentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_linearity_pointwiseentriesentryrightvalue) = 0) /\ (ge_balance_negative_linearity_pointwiseentriesentryrightvalue) = S ge_signed_half_linearity_pointwiseentriesentryrightvaluedecode))) /\ ((dst_positive_linearity_pointwiseentriesentryright) + ge_balance_negative_linearity_pointwiseentriesentryrightvalue = (dst_negative_linearity_pointwiseentriesentryright) + ge_balance_positive_linearity_pointwiseentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_linearity_pointwiseentriesentryoutput dst_positive_scale_linearity_pointwiseentriesentryoutput dst_negative_code_linearity_pointwiseentriesentryoutput dst_negative_scale_linearity_pointwiseentriesentryoutput dst_positive_linearity_pointwiseentriesentryoutput dst_negative_linearity_pointwiseentriesentryoutput. (((H) = (((((dst_positive_code_linearity_pointwiseentriesentryoutput) + (dst_positive_scale_linearity_pointwiseentriesentryoutput)) * S ((dst_positive_code_linearity_pointwiseentriesentryoutput) + (dst_positive_scale_linearity_pointwiseentriesentryoutput)) + ((dst_positive_scale_linearity_pointwiseentriesentryoutput) + (dst_positive_scale_linearity_pointwiseentriesentryoutput))) + (((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) * S ((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) + ((dst_negative_scale_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)))) * S ((((dst_positive_code_linearity_pointwiseentriesentryoutput) + (dst_positive_scale_linearity_pointwiseentriesentryoutput)) * S ((dst_positive_code_linearity_pointwiseentriesentryoutput) + (dst_positive_scale_linearity_pointwiseentriesentryoutput)) + ((dst_positive_scale_linearity_pointwiseentriesentryoutput) + (dst_positive_scale_linearity_pointwiseentriesentryoutput))) + (((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) * S ((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) + ((dst_negative_scale_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)))) + ((((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) * S ((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) + ((dst_negative_scale_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput))) + (((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) * S ((dst_negative_code_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)) + ((dst_negative_scale_linearity_pointwiseentriesentryoutput) + (dst_negative_scale_linearity_pointwiseentriesentryoutput)))))) /\ (((((exists ff_h_pvs_linearity_pointwiseentriesentryoutputpositive. ff_h_pvs_linearity_pointwiseentriesentryoutputpositive + S (dst_positive_linearity_pointwiseentriesentryoutput) = S ((S (sto_index_linearity_pointwiseentries)) * dst_positive_scale_linearity_pointwiseentriesentryoutput)) /\ exists ff_q_pvs_linearity_pointwiseentriesentryoutputpositive. dst_positive_code_linearity_pointwiseentriesentryoutput = ff_q_pvs_linearity_pointwiseentriesentryoutputpositive * S ((S (sto_index_linearity_pointwiseentries)) * dst_positive_scale_linearity_pointwiseentriesentryoutput) + (dst_positive_linearity_pointwiseentriesentryoutput))) /\ (((((exists ff_h_pvs_linearity_pointwiseentriesentryoutputnegative. ff_h_pvs_linearity_pointwiseentriesentryoutputnegative + S (dst_negative_linearity_pointwiseentriesentryoutput) = S ((S (sto_index_linearity_pointwiseentries)) * dst_negative_scale_linearity_pointwiseentriesentryoutput)) /\ exists ff_q_pvs_linearity_pointwiseentriesentryoutputnegative. dst_negative_code_linearity_pointwiseentriesentryoutput = ff_q_pvs_linearity_pointwiseentriesentryoutputnegative * S ((S (sto_index_linearity_pointwiseentries)) * dst_negative_scale_linearity_pointwiseentriesentryoutput) + (dst_negative_linearity_pointwiseentriesentryoutput))) /\ (exists ge_balance_positive_linearity_pointwiseentriesentryoutputvalue ge_balance_negative_linearity_pointwiseentriesentryoutputvalue. (((((sto_output_linearity_pointwiseentries) = 2 * (ge_balance_positive_linearity_pointwiseentriesentryoutputvalue) /\ (ge_balance_negative_linearity_pointwiseentriesentryoutputvalue) = 0) \/ exists ge_signed_half_linearity_pointwiseentriesentryoutputvaluedecode. (((sto_output_linearity_pointwiseentries) = 2 * ge_signed_half_linearity_pointwiseentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_linearity_pointwiseentriesentryoutputvalue) = 0) /\ (ge_balance_negative_linearity_pointwiseentriesentryoutputvalue) = S ge_signed_half_linearity_pointwiseentriesentryoutputvaluedecode))) /\ ((dst_positive_linearity_pointwiseentriesentryoutput) + ge_balance_negative_linearity_pointwiseentriesentryoutputvalue = (dst_negative_linearity_pointwiseentriesentryoutput) + ge_balance_positive_linearity_pointwiseentriesentryoutputvalue))))))))) /\ (exists dsa_ap_linearity_pointwiseentriesentryoperation dsa_an_linearity_pointwiseentriesentryoperation dsa_bp_linearity_pointwiseentriesentryoperation dsa_bn_linearity_pointwiseentriesentryoperation dsa_cp_linearity_pointwiseentriesentryoperation dsa_cn_linearity_pointwiseentriesentryoperation. (((((sto_left_linearity_pointwiseentries) = 2 * (dsa_ap_linearity_pointwiseentriesentryoperation) /\ (dsa_an_linearity_pointwiseentriesentryoperation) = 0) \/ exists ge_signed_half_linearity_pointwiseentriesentryoperationleft. (((sto_left_linearity_pointwiseentries) = 2 * ge_signed_half_linearity_pointwiseentriesentryoperationleft + 1 /\ (dsa_ap_linearity_pointwiseentriesentryoperation) = 0) /\ (dsa_an_linearity_pointwiseentriesentryoperation) = S ge_signed_half_linearity_pointwiseentriesentryoperationleft))) /\ ((((((sto_right_linearity_pointwiseentries) = 2 * (dsa_bp_linearity_pointwiseentriesentryoperation) /\ (dsa_bn_linearity_pointwiseentriesentryoperation) = 0) \/ exists ge_signed_half_linearity_pointwiseentriesentryoperationright. (((sto_right_linearity_pointwiseentries) = 2 * ge_signed_half_linearity_pointwiseentriesentryoperationright + 1 /\ (dsa_bp_linearity_pointwiseentriesentryoperation) = 0) /\ (dsa_bn_linearity_pointwiseentriesentryoperation) = S ge_signed_half_linearity_pointwiseentriesentryoperationright))) /\ ((((((sto_output_linearity_pointwiseentries) = 2 * (dsa_cp_linearity_pointwiseentriesentryoperation) /\ (dsa_cn_linearity_pointwiseentriesentryoperation) = 0) \/ exists ge_signed_half_linearity_pointwiseentriesentryoperationoutput. (((sto_output_linearity_pointwiseentries) = 2 * ge_signed_half_linearity_pointwiseentriesentryoperationoutput + 1 /\ (dsa_cp_linearity_pointwiseentriesentryoperation) = 0) /\ (dsa_cn_linearity_pointwiseentriesentryoperation) = S ge_signed_half_linearity_pointwiseentriesentryoperationoutput))) /\ ((dsa_ap_linearity_pointwiseentriesentryoperation + dsa_bp_linearity_pointwiseentriesentryoperation) + dsa_cn_linearity_pointwiseentriesentryoperation = (dsa_an_linearity_pointwiseentriesentryoperation + dsa_bn_linearity_pointwiseentriesentryoperation) + dsa_cp_linearity_pointwiseentriesentryoperation))))))))))))))))))) -> (exists dst_positive_code_linearity_first dst_positive_scale_linearity_first dst_negative_code_linearity_first dst_negative_scale_linearity_first dst_positive_sum_linearity_first dst_negative_sum_linearity_first. (((F) = (((((dst_positive_code_linearity_first) + (dst_positive_scale_linearity_first)) * S ((dst_positive_code_linearity_first) + (dst_positive_scale_linearity_first)) + ((dst_positive_scale_linearity_first) + (dst_positive_scale_linearity_first))) + (((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) * S ((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) + ((dst_negative_scale_linearity_first) + (dst_negative_scale_linearity_first)))) * S ((((dst_positive_code_linearity_first) + (dst_positive_scale_linearity_first)) * S ((dst_positive_code_linearity_first) + (dst_positive_scale_linearity_first)) + ((dst_positive_scale_linearity_first) + (dst_positive_scale_linearity_first))) + (((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) * S ((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) + ((dst_negative_scale_linearity_first) + (dst_negative_scale_linearity_first)))) + ((((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) * S ((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) + ((dst_negative_scale_linearity_first) + (dst_negative_scale_linearity_first))) + (((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) * S ((dst_negative_code_linearity_first) + (dst_negative_scale_linearity_first)) + ((dst_negative_scale_linearity_first) + (dst_negative_scale_linearity_first)))))) /\ (((exists fs_u_dst_linearity_firstpositive fs_v_dst_linearity_firstpositive. ((((exists fs_h_dst_linearity_firstpositive_body_start. fs_h_dst_linearity_firstpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_linearity_firstpositive)) /\ exists fs_q_dst_linearity_firstpositive_body_start. fs_u_dst_linearity_firstpositive = fs_q_dst_linearity_firstpositive_body_start * S ((S (0)) * fs_v_dst_linearity_firstpositive) + (0))) /\ ((((exists fs_h_dst_linearity_firstpositive_body_terminal. fs_h_dst_linearity_firstpositive_body_terminal + S (dst_positive_sum_linearity_first) = S ((S (l)) * fs_v_dst_linearity_firstpositive)) /\ exists fs_q_dst_linearity_firstpositive_body_terminal. fs_u_dst_linearity_firstpositive = fs_q_dst_linearity_firstpositive_body_terminal * S ((S (l)) * fs_v_dst_linearity_firstpositive) + (dst_positive_sum_linearity_first))) /\ forall fs_i_dst_linearity_firstpositive_body_steps. (exists fs_lt_dst_linearity_firstpositive_body_steps_bound. fs_lt_dst_linearity_firstpositive_body_steps_bound + S fs_i_dst_linearity_firstpositive_body_steps = l) -> exists fs_a_dst_linearity_firstpositive_body_steps fs_r_dst_linearity_firstpositive_body_steps fs_s_dst_linearity_firstpositive_body_steps. ((((exists fs_h_dst_linearity_firstpositive_body_steps_summand. fs_h_dst_linearity_firstpositive_body_steps_summand + S (fs_a_dst_linearity_firstpositive_body_steps) = S ((S (fs_i_dst_linearity_firstpositive_body_steps)) * dst_positive_scale_linearity_first)) /\ exists fs_q_dst_linearity_firstpositive_body_steps_summand. dst_positive_code_linearity_first = fs_q_dst_linearity_firstpositive_body_steps_summand * S ((S (fs_i_dst_linearity_firstpositive_body_steps)) * dst_positive_scale_linearity_first) + (fs_a_dst_linearity_firstpositive_body_steps))) /\ ((((exists fs_h_dst_linearity_firstpositive_body_steps_partial. fs_h_dst_linearity_firstpositive_body_steps_partial + S (fs_r_dst_linearity_firstpositive_body_steps) = S ((S (fs_i_dst_linearity_firstpositive_body_steps)) * fs_v_dst_linearity_firstpositive)) /\ exists fs_q_dst_linearity_firstpositive_body_steps_partial. fs_u_dst_linearity_firstpositive = fs_q_dst_linearity_firstpositive_body_steps_partial * S ((S (fs_i_dst_linearity_firstpositive_body_steps)) * fs_v_dst_linearity_firstpositive) + (fs_r_dst_linearity_firstpositive_body_steps))) /\ ((((exists fs_h_dst_linearity_firstpositive_body_steps_successor. fs_h_dst_linearity_firstpositive_body_steps_successor + S (fs_s_dst_linearity_firstpositive_body_steps) = S ((S (S fs_i_dst_linearity_firstpositive_body_steps)) * fs_v_dst_linearity_firstpositive)) /\ exists fs_q_dst_linearity_firstpositive_body_steps_successor. fs_u_dst_linearity_firstpositive = fs_q_dst_linearity_firstpositive_body_steps_successor * S ((S (S fs_i_dst_linearity_firstpositive_body_steps)) * fs_v_dst_linearity_firstpositive) + (fs_s_dst_linearity_firstpositive_body_steps))) /\ fs_s_dst_linearity_firstpositive_body_steps = fs_r_dst_linearity_firstpositive_body_steps + fs_a_dst_linearity_firstpositive_body_steps)))))) /\ (((exists fs_u_dst_linearity_firstnegative fs_v_dst_linearity_firstnegative. ((((exists fs_h_dst_linearity_firstnegative_body_start. fs_h_dst_linearity_firstnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_linearity_firstnegative)) /\ exists fs_q_dst_linearity_firstnegative_body_start. fs_u_dst_linearity_firstnegative = fs_q_dst_linearity_firstnegative_body_start * S ((S (0)) * fs_v_dst_linearity_firstnegative) + (0))) /\ ((((exists fs_h_dst_linearity_firstnegative_body_terminal. fs_h_dst_linearity_firstnegative_body_terminal + S (dst_negative_sum_linearity_first) = S ((S (l)) * fs_v_dst_linearity_firstnegative)) /\ exists fs_q_dst_linearity_firstnegative_body_terminal. fs_u_dst_linearity_firstnegative = fs_q_dst_linearity_firstnegative_body_terminal * S ((S (l)) * fs_v_dst_linearity_firstnegative) + (dst_negative_sum_linearity_first))) /\ forall fs_i_dst_linearity_firstnegative_body_steps. (exists fs_lt_dst_linearity_firstnegative_body_steps_bound. fs_lt_dst_linearity_firstnegative_body_steps_bound + S fs_i_dst_linearity_firstnegative_body_steps = l) -> exists fs_a_dst_linearity_firstnegative_body_steps fs_r_dst_linearity_firstnegative_body_steps fs_s_dst_linearity_firstnegative_body_steps. ((((exists fs_h_dst_linearity_firstnegative_body_steps_summand. fs_h_dst_linearity_firstnegative_body_steps_summand + S (fs_a_dst_linearity_firstnegative_body_steps) = S ((S (fs_i_dst_linearity_firstnegative_body_steps)) * dst_negative_scale_linearity_first)) /\ exists fs_q_dst_linearity_firstnegative_body_steps_summand. dst_negative_code_linearity_first = fs_q_dst_linearity_firstnegative_body_steps_summand * S ((S (fs_i_dst_linearity_firstnegative_body_steps)) * dst_negative_scale_linearity_first) + (fs_a_dst_linearity_firstnegative_body_steps))) /\ ((((exists fs_h_dst_linearity_firstnegative_body_steps_partial. fs_h_dst_linearity_firstnegative_body_steps_partial + S (fs_r_dst_linearity_firstnegative_body_steps) = S ((S (fs_i_dst_linearity_firstnegative_body_steps)) * fs_v_dst_linearity_firstnegative)) /\ exists fs_q_dst_linearity_firstnegative_body_steps_partial. fs_u_dst_linearity_firstnegative = fs_q_dst_linearity_firstnegative_body_steps_partial * S ((S (fs_i_dst_linearity_firstnegative_body_steps)) * fs_v_dst_linearity_firstnegative) + (fs_r_dst_linearity_firstnegative_body_steps))) /\ ((((exists fs_h_dst_linearity_firstnegative_body_steps_successor. fs_h_dst_linearity_firstnegative_body_steps_successor + S (fs_s_dst_linearity_firstnegative_body_steps) = S ((S (S fs_i_dst_linearity_firstnegative_body_steps)) * fs_v_dst_linearity_firstnegative)) /\ exists fs_q_dst_linearity_firstnegative_body_steps_successor. fs_u_dst_linearity_firstnegative = fs_q_dst_linearity_firstnegative_body_steps_successor * S ((S (S fs_i_dst_linearity_firstnegative_body_steps)) * fs_v_dst_linearity_firstnegative) + (fs_s_dst_linearity_firstnegative_body_steps))) /\ fs_s_dst_linearity_firstnegative_body_steps = fs_r_dst_linearity_firstnegative_body_steps + fs_a_dst_linearity_firstnegative_body_steps)))))) /\ (exists ge_balance_positive_linearity_firstresult ge_balance_negative_linearity_firstresult. (((((a) = 2 * (ge_balance_positive_linearity_firstresult) /\ (ge_balance_negative_linearity_firstresult) = 0) \/ exists ge_signed_half_linearity_firstresultdecode. (((a) = 2 * ge_signed_half_linearity_firstresultdecode + 1 /\ (ge_balance_positive_linearity_firstresult) = 0) /\ (ge_balance_negative_linearity_firstresult) = S ge_signed_half_linearity_firstresultdecode))) /\ ((dst_positive_sum_linearity_first) + ge_balance_negative_linearity_firstresult = (dst_negative_sum_linearity_first) + ge_balance_positive_linearity_firstresult))))))))) -> (exists dst_positive_code_linearity_second dst_positive_scale_linearity_second dst_negative_code_linearity_second dst_negative_scale_linearity_second dst_positive_sum_linearity_second dst_negative_sum_linearity_second. (((G) = (((((dst_positive_code_linearity_second) + (dst_positive_scale_linearity_second)) * S ((dst_positive_code_linearity_second) + (dst_positive_scale_linearity_second)) + ((dst_positive_scale_linearity_second) + (dst_positive_scale_linearity_second))) + (((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) * S ((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) + ((dst_negative_scale_linearity_second) + (dst_negative_scale_linearity_second)))) * S ((((dst_positive_code_linearity_second) + (dst_positive_scale_linearity_second)) * S ((dst_positive_code_linearity_second) + (dst_positive_scale_linearity_second)) + ((dst_positive_scale_linearity_second) + (dst_positive_scale_linearity_second))) + (((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) * S ((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) + ((dst_negative_scale_linearity_second) + (dst_negative_scale_linearity_second)))) + ((((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) * S ((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) + ((dst_negative_scale_linearity_second) + (dst_negative_scale_linearity_second))) + (((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) * S ((dst_negative_code_linearity_second) + (dst_negative_scale_linearity_second)) + ((dst_negative_scale_linearity_second) + (dst_negative_scale_linearity_second)))))) /\ (((exists fs_u_dst_linearity_secondpositive fs_v_dst_linearity_secondpositive. ((((exists fs_h_dst_linearity_secondpositive_body_start. fs_h_dst_linearity_secondpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_linearity_secondpositive)) /\ exists fs_q_dst_linearity_secondpositive_body_start. fs_u_dst_linearity_secondpositive = fs_q_dst_linearity_secondpositive_body_start * S ((S (0)) * fs_v_dst_linearity_secondpositive) + (0))) /\ ((((exists fs_h_dst_linearity_secondpositive_body_terminal. fs_h_dst_linearity_secondpositive_body_terminal + S (dst_positive_sum_linearity_second) = S ((S (l)) * fs_v_dst_linearity_secondpositive)) /\ exists fs_q_dst_linearity_secondpositive_body_terminal. fs_u_dst_linearity_secondpositive = fs_q_dst_linearity_secondpositive_body_terminal * S ((S (l)) * fs_v_dst_linearity_secondpositive) + (dst_positive_sum_linearity_second))) /\ forall fs_i_dst_linearity_secondpositive_body_steps. (exists fs_lt_dst_linearity_secondpositive_body_steps_bound. fs_lt_dst_linearity_secondpositive_body_steps_bound + S fs_i_dst_linearity_secondpositive_body_steps = l) -> exists fs_a_dst_linearity_secondpositive_body_steps fs_r_dst_linearity_secondpositive_body_steps fs_s_dst_linearity_secondpositive_body_steps. ((((exists fs_h_dst_linearity_secondpositive_body_steps_summand. fs_h_dst_linearity_secondpositive_body_steps_summand + S (fs_a_dst_linearity_secondpositive_body_steps) = S ((S (fs_i_dst_linearity_secondpositive_body_steps)) * dst_positive_scale_linearity_second)) /\ exists fs_q_dst_linearity_secondpositive_body_steps_summand. dst_positive_code_linearity_second = fs_q_dst_linearity_secondpositive_body_steps_summand * S ((S (fs_i_dst_linearity_secondpositive_body_steps)) * dst_positive_scale_linearity_second) + (fs_a_dst_linearity_secondpositive_body_steps))) /\ ((((exists fs_h_dst_linearity_secondpositive_body_steps_partial. fs_h_dst_linearity_secondpositive_body_steps_partial + S (fs_r_dst_linearity_secondpositive_body_steps) = S ((S (fs_i_dst_linearity_secondpositive_body_steps)) * fs_v_dst_linearity_secondpositive)) /\ exists fs_q_dst_linearity_secondpositive_body_steps_partial. fs_u_dst_linearity_secondpositive = fs_q_dst_linearity_secondpositive_body_steps_partial * S ((S (fs_i_dst_linearity_secondpositive_body_steps)) * fs_v_dst_linearity_secondpositive) + (fs_r_dst_linearity_secondpositive_body_steps))) /\ ((((exists fs_h_dst_linearity_secondpositive_body_steps_successor. fs_h_dst_linearity_secondpositive_body_steps_successor + S (fs_s_dst_linearity_secondpositive_body_steps) = S ((S (S fs_i_dst_linearity_secondpositive_body_steps)) * fs_v_dst_linearity_secondpositive)) /\ exists fs_q_dst_linearity_secondpositive_body_steps_successor. fs_u_dst_linearity_secondpositive = fs_q_dst_linearity_secondpositive_body_steps_successor * S ((S (S fs_i_dst_linearity_secondpositive_body_steps)) * fs_v_dst_linearity_secondpositive) + (fs_s_dst_linearity_secondpositive_body_steps))) /\ fs_s_dst_linearity_secondpositive_body_steps = fs_r_dst_linearity_secondpositive_body_steps + fs_a_dst_linearity_secondpositive_body_steps)))))) /\ (((exists fs_u_dst_linearity_secondnegative fs_v_dst_linearity_secondnegative. ((((exists fs_h_dst_linearity_secondnegative_body_start. fs_h_dst_linearity_secondnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_linearity_secondnegative)) /\ exists fs_q_dst_linearity_secondnegative_body_start. fs_u_dst_linearity_secondnegative = fs_q_dst_linearity_secondnegative_body_start * S ((S (0)) * fs_v_dst_linearity_secondnegative) + (0))) /\ ((((exists fs_h_dst_linearity_secondnegative_body_terminal. fs_h_dst_linearity_secondnegative_body_terminal + S (dst_negative_sum_linearity_second) = S ((S (l)) * fs_v_dst_linearity_secondnegative)) /\ exists fs_q_dst_linearity_secondnegative_body_terminal. fs_u_dst_linearity_secondnegative = fs_q_dst_linearity_secondnegative_body_terminal * S ((S (l)) * fs_v_dst_linearity_secondnegative) + (dst_negative_sum_linearity_second))) /\ forall fs_i_dst_linearity_secondnegative_body_steps. (exists fs_lt_dst_linearity_secondnegative_body_steps_bound. fs_lt_dst_linearity_secondnegative_body_steps_bound + S fs_i_dst_linearity_secondnegative_body_steps = l) -> exists fs_a_dst_linearity_secondnegative_body_steps fs_r_dst_linearity_secondnegative_body_steps fs_s_dst_linearity_secondnegative_body_steps. ((((exists fs_h_dst_linearity_secondnegative_body_steps_summand. fs_h_dst_linearity_secondnegative_body_steps_summand + S (fs_a_dst_linearity_secondnegative_body_steps) = S ((S (fs_i_dst_linearity_secondnegative_body_steps)) * dst_negative_scale_linearity_second)) /\ exists fs_q_dst_linearity_secondnegative_body_steps_summand. dst_negative_code_linearity_second = fs_q_dst_linearity_secondnegative_body_steps_summand * S ((S (fs_i_dst_linearity_secondnegative_body_steps)) * dst_negative_scale_linearity_second) + (fs_a_dst_linearity_secondnegative_body_steps))) /\ ((((exists fs_h_dst_linearity_secondnegative_body_steps_partial. fs_h_dst_linearity_secondnegative_body_steps_partial + S (fs_r_dst_linearity_secondnegative_body_steps) = S ((S (fs_i_dst_linearity_secondnegative_body_steps)) * fs_v_dst_linearity_secondnegative)) /\ exists fs_q_dst_linearity_secondnegative_body_steps_partial. fs_u_dst_linearity_secondnegative = fs_q_dst_linearity_secondnegative_body_steps_partial * S ((S (fs_i_dst_linearity_secondnegative_body_steps)) * fs_v_dst_linearity_secondnegative) + (fs_r_dst_linearity_secondnegative_body_steps))) /\ ((((exists fs_h_dst_linearity_secondnegative_body_steps_successor. fs_h_dst_linearity_secondnegative_body_steps_successor + S (fs_s_dst_linearity_secondnegative_body_steps) = S ((S (S fs_i_dst_linearity_secondnegative_body_steps)) * fs_v_dst_linearity_secondnegative)) /\ exists fs_q_dst_linearity_secondnegative_body_steps_successor. fs_u_dst_linearity_secondnegative = fs_q_dst_linearity_secondnegative_body_steps_successor * S ((S (S fs_i_dst_linearity_secondnegative_body_steps)) * fs_v_dst_linearity_secondnegative) + (fs_s_dst_linearity_secondnegative_body_steps))) /\ fs_s_dst_linearity_secondnegative_body_steps = fs_r_dst_linearity_secondnegative_body_steps + fs_a_dst_linearity_secondnegative_body_steps)))))) /\ (exists ge_balance_positive_linearity_secondresult ge_balance_negative_linearity_secondresult. (((((b) = 2 * (ge_balance_positive_linearity_secondresult) /\ (ge_balance_negative_linearity_secondresult) = 0) \/ exists ge_signed_half_linearity_secondresultdecode. (((b) = 2 * ge_signed_half_linearity_secondresultdecode + 1 /\ (ge_balance_positive_linearity_secondresult) = 0) /\ (ge_balance_negative_linearity_secondresult) = S ge_signed_half_linearity_secondresultdecode))) /\ ((dst_positive_sum_linearity_second) + ge_balance_negative_linearity_secondresult = (dst_negative_sum_linearity_second) + ge_balance_positive_linearity_secondresult))))))))) -> (exists dst_positive_code_linearity_output dst_positive_scale_linearity_output dst_negative_code_linearity_output dst_negative_scale_linearity_output dst_positive_sum_linearity_output dst_negative_sum_linearity_output. (((H) = (((((dst_positive_code_linearity_output) + (dst_positive_scale_linearity_output)) * S ((dst_positive_code_linearity_output) + (dst_positive_scale_linearity_output)) + ((dst_positive_scale_linearity_output) + (dst_positive_scale_linearity_output))) + (((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) * S ((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) + ((dst_negative_scale_linearity_output) + (dst_negative_scale_linearity_output)))) * S ((((dst_positive_code_linearity_output) + (dst_positive_scale_linearity_output)) * S ((dst_positive_code_linearity_output) + (dst_positive_scale_linearity_output)) + ((dst_positive_scale_linearity_output) + (dst_positive_scale_linearity_output))) + (((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) * S ((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) + ((dst_negative_scale_linearity_output) + (dst_negative_scale_linearity_output)))) + ((((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) * S ((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) + ((dst_negative_scale_linearity_output) + (dst_negative_scale_linearity_output))) + (((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) * S ((dst_negative_code_linearity_output) + (dst_negative_scale_linearity_output)) + ((dst_negative_scale_linearity_output) + (dst_negative_scale_linearity_output)))))) /\ (((exists fs_u_dst_linearity_outputpositive fs_v_dst_linearity_outputpositive. ((((exists fs_h_dst_linearity_outputpositive_body_start. fs_h_dst_linearity_outputpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_linearity_outputpositive)) /\ exists fs_q_dst_linearity_outputpositive_body_start. fs_u_dst_linearity_outputpositive = fs_q_dst_linearity_outputpositive_body_start * S ((S (0)) * fs_v_dst_linearity_outputpositive) + (0))) /\ ((((exists fs_h_dst_linearity_outputpositive_body_terminal. fs_h_dst_linearity_outputpositive_body_terminal + S (dst_positive_sum_linearity_output) = S ((S (l)) * fs_v_dst_linearity_outputpositive)) /\ exists fs_q_dst_linearity_outputpositive_body_terminal. fs_u_dst_linearity_outputpositive = fs_q_dst_linearity_outputpositive_body_terminal * S ((S (l)) * fs_v_dst_linearity_outputpositive) + (dst_positive_sum_linearity_output))) /\ forall fs_i_dst_linearity_outputpositive_body_steps. (exists fs_lt_dst_linearity_outputpositive_body_steps_bound. fs_lt_dst_linearity_outputpositive_body_steps_bound + S fs_i_dst_linearity_outputpositive_body_steps = l) -> exists fs_a_dst_linearity_outputpositive_body_steps fs_r_dst_linearity_outputpositive_body_steps fs_s_dst_linearity_outputpositive_body_steps. ((((exists fs_h_dst_linearity_outputpositive_body_steps_summand. fs_h_dst_linearity_outputpositive_body_steps_summand + S (fs_a_dst_linearity_outputpositive_body_steps) = S ((S (fs_i_dst_linearity_outputpositive_body_steps)) * dst_positive_scale_linearity_output)) /\ exists fs_q_dst_linearity_outputpositive_body_steps_summand. dst_positive_code_linearity_output = fs_q_dst_linearity_outputpositive_body_steps_summand * S ((S (fs_i_dst_linearity_outputpositive_body_steps)) * dst_positive_scale_linearity_output) + (fs_a_dst_linearity_outputpositive_body_steps))) /\ ((((exists fs_h_dst_linearity_outputpositive_body_steps_partial. fs_h_dst_linearity_outputpositive_body_steps_partial + S (fs_r_dst_linearity_outputpositive_body_steps) = S ((S (fs_i_dst_linearity_outputpositive_body_steps)) * fs_v_dst_linearity_outputpositive)) /\ exists fs_q_dst_linearity_outputpositive_body_steps_partial. fs_u_dst_linearity_outputpositive = fs_q_dst_linearity_outputpositive_body_steps_partial * S ((S (fs_i_dst_linearity_outputpositive_body_steps)) * fs_v_dst_linearity_outputpositive) + (fs_r_dst_linearity_outputpositive_body_steps))) /\ ((((exists fs_h_dst_linearity_outputpositive_body_steps_successor. fs_h_dst_linearity_outputpositive_body_steps_successor + S (fs_s_dst_linearity_outputpositive_body_steps) = S ((S (S fs_i_dst_linearity_outputpositive_body_steps)) * fs_v_dst_linearity_outputpositive)) /\ exists fs_q_dst_linearity_outputpositive_body_steps_successor. fs_u_dst_linearity_outputpositive = fs_q_dst_linearity_outputpositive_body_steps_successor * S ((S (S fs_i_dst_linearity_outputpositive_body_steps)) * fs_v_dst_linearity_outputpositive) + (fs_s_dst_linearity_outputpositive_body_steps))) /\ fs_s_dst_linearity_outputpositive_body_steps = fs_r_dst_linearity_outputpositive_body_steps + fs_a_dst_linearity_outputpositive_body_steps)))))) /\ (((exists fs_u_dst_linearity_outputnegative fs_v_dst_linearity_outputnegative. ((((exists fs_h_dst_linearity_outputnegative_body_start. fs_h_dst_linearity_outputnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_linearity_outputnegative)) /\ exists fs_q_dst_linearity_outputnegative_body_start. fs_u_dst_linearity_outputnegative = fs_q_dst_linearity_outputnegative_body_start * S ((S (0)) * fs_v_dst_linearity_outputnegative) + (0))) /\ ((((exists fs_h_dst_linearity_outputnegative_body_terminal. fs_h_dst_linearity_outputnegative_body_terminal + S (dst_negative_sum_linearity_output) = S ((S (l)) * fs_v_dst_linearity_outputnegative)) /\ exists fs_q_dst_linearity_outputnegative_body_terminal. fs_u_dst_linearity_outputnegative = fs_q_dst_linearity_outputnegative_body_terminal * S ((S (l)) * fs_v_dst_linearity_outputnegative) + (dst_negative_sum_linearity_output))) /\ forall fs_i_dst_linearity_outputnegative_body_steps. (exists fs_lt_dst_linearity_outputnegative_body_steps_bound. fs_lt_dst_linearity_outputnegative_body_steps_bound + S fs_i_dst_linearity_outputnegative_body_steps = l) -> exists fs_a_dst_linearity_outputnegative_body_steps fs_r_dst_linearity_outputnegative_body_steps fs_s_dst_linearity_outputnegative_body_steps. ((((exists fs_h_dst_linearity_outputnegative_body_steps_summand. fs_h_dst_linearity_outputnegative_body_steps_summand + S (fs_a_dst_linearity_outputnegative_body_steps) = S ((S (fs_i_dst_linearity_outputnegative_body_steps)) * dst_negative_scale_linearity_output)) /\ exists fs_q_dst_linearity_outputnegative_body_steps_summand. dst_negative_code_linearity_output = fs_q_dst_linearity_outputnegative_body_steps_summand * S ((S (fs_i_dst_linearity_outputnegative_body_steps)) * dst_negative_scale_linearity_output) + (fs_a_dst_linearity_outputnegative_body_steps))) /\ ((((exists fs_h_dst_linearity_outputnegative_body_steps_partial. fs_h_dst_linearity_outputnegative_body_steps_partial + S (fs_r_dst_linearity_outputnegative_body_steps) = S ((S (fs_i_dst_linearity_outputnegative_body_steps)) * fs_v_dst_linearity_outputnegative)) /\ exists fs_q_dst_linearity_outputnegative_body_steps_partial. fs_u_dst_linearity_outputnegative = fs_q_dst_linearity_outputnegative_body_steps_partial * S ((S (fs_i_dst_linearity_outputnegative_body_steps)) * fs_v_dst_linearity_outputnegative) + (fs_r_dst_linearity_outputnegative_body_steps))) /\ ((((exists fs_h_dst_linearity_outputnegative_body_steps_successor. fs_h_dst_linearity_outputnegative_body_steps_successor + S (fs_s_dst_linearity_outputnegative_body_steps) = S ((S (S fs_i_dst_linearity_outputnegative_body_steps)) * fs_v_dst_linearity_outputnegative)) /\ exists fs_q_dst_linearity_outputnegative_body_steps_successor. fs_u_dst_linearity_outputnegative = fs_q_dst_linearity_outputnegative_body_steps_successor * S ((S (S fs_i_dst_linearity_outputnegative_body_steps)) * fs_v_dst_linearity_outputnegative) + (fs_s_dst_linearity_outputnegative_body_steps))) /\ fs_s_dst_linearity_outputnegative_body_steps = fs_r_dst_linearity_outputnegative_body_steps + fs_a_dst_linearity_outputnegative_body_steps)))))) /\ (exists ge_balance_positive_linearity_outputresult ge_balance_negative_linearity_outputresult. (((((c) = 2 * (ge_balance_positive_linearity_outputresult) /\ (ge_balance_negative_linearity_outputresult) = 0) \/ exists ge_signed_half_linearity_outputresultdecode. (((c) = 2 * ge_signed_half_linearity_outputresultdecode + 1 /\ (ge_balance_positive_linearity_outputresult) = 0) /\ (ge_balance_negative_linearity_outputresult) = S ge_signed_half_linearity_outputresultdecode))) /\ ((dst_positive_sum_linearity_output) + ge_balance_negative_linearity_outputresult = (dst_negative_sum_linearity_output) + ge_balance_positive_linearity_outputresult))))))))) -> (exists dsa_ap_linearity_result dsa_an_linearity_result dsa_bp_linearity_result dsa_bn_linearity_result dsa_cp_linearity_result dsa_cn_linearity_result. (((((a) = 2 * (dsa_ap_linearity_result) /\ (dsa_an_linearity_result) = 0) \/ exists ge_signed_half_linearity_resultleft. (((a) = 2 * ge_signed_half_linearity_resultleft + 1 /\ (dsa_ap_linearity_result) = 0) /\ (dsa_an_linearity_result) = S ge_signed_half_linearity_resultleft))) /\ ((((((b) = 2 * (dsa_bp_linearity_result) /\ (dsa_bn_linearity_result) = 0) \/ exists ge_signed_half_linearity_resultright. (((b) = 2 * ge_signed_half_linearity_resultright + 1 /\ (dsa_bp_linearity_result) = 0) /\ (dsa_bn_linearity_result) = S ge_signed_half_linearity_resultright))) /\ ((((((c) = 2 * (dsa_cp_linearity_result) /\ (dsa_cn_linearity_result) = 0) \/ exists ge_signed_half_linearity_resultoutput. (((c) = 2 * ge_signed_half_linearity_resultoutput + 1 /\ (dsa_cp_linearity_result) = 0) /\ (dsa_cn_linearity_result) = S ge_signed_half_linearity_resultoutput))) /\ ((dsa_ap_linearity_result + dsa_bp_linearity_result) + dsa_cn_linearity_result = (dsa_an_linearity_result + dsa_bn_linearity_result) + dsa_cp_linearity_result)))))))