Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
The full finite signed G007 theorem includes the reverse equivalence and actual witnesses at N=0. The divisor-transform premise covers every required positive quotient. F(0), G(0) and H(0) are unrestricted; only the historical Möbius witness retains its separate zero convention. Full G009 multiplicative closure is admitted in Alpha v32; G091 prime-power fields remain open.
Exact theorem in conservative defined notation
∀ N. ∀ F. ∀ G. ∀ U. ConstantOneTable(N,U) → DirichletTable(N,F,U,G) → DivisorTransform(N,F,G)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall N F G U. (((exists dst_positive_code_transform_reverse_onetable dst_positive_scale_transform_reverse_onetable dst_negative_code_transform_reverse_onetable dst_negative_scale_transform_reverse_onetable. (((U) = (((((dst_positive_code_transform_reverse_onetable) + (dst_positive_scale_transform_reverse_onetable)) * S ((dst_positive_code_transform_reverse_onetable) + (dst_positive_scale_transform_reverse_onetable)) + ((dst_positive_scale_transform_reverse_onetable) + (dst_positive_scale_transform_reverse_onetable))) + (((dst_negative_code_transform_reverse_onetable) + (dst_negative_scale_transform_reverse_onetable)) * S ((dst_negative_code_transform_reverse_onetable) + (dst_negative_scale_transform_reverse_onetable)) + ((dst_negative_scale_transform_reverse_onetable) + (dst_negative_scale_transform_reverse_onetable)))) * S ((((dst_positive_code_transform_reverse_onetable) + (dst_positive_scale_transform_reverse_onetable)) * S ((dst_positive_code_transform_reverse_onetable) + (dst_positive_scale_transform_reverse_onetable)) + ((dst_positive_scale_transform_reverse_onetable) + (dst_positive_scale_transform_reverse_onetable))) + (((dst_negative_code_transform_reverse_onetable) + (dst_negative_scale_transform_reverse_onetable)) * S ((dst_negative_code_transform_reverse_onetable) + (dst_negative_scale_transform_reverse_onetable)) + ((dst_negative_scale_transform_reverse_onetable) + (dst_negative_scale_transform_reverse_onetable)))) + ((((dst_negative_code_transform_reverse_onetable) + (dst_negative_scale_transform_reverse_onetable)) * S ((dst_negative_code_transform_reverse_onetable) + (dst_negative_scale_transform_reverse_onetable)) + ((dst_negative_scale_transform_reverse_onetable) + (dst_negative_scale_transform_reverse_onetable))) + (((dst_negative_code_transform_reverse_onetable) + (dst_negative_scale_transform_reverse_onetable)) * S ((dst_negative_code_transform_reverse_onetable) + (dst_negative_scale_transform_reverse_onetable)) + ((dst_negative_scale_transform_reverse_onetable) + (dst_negative_scale_transform_reverse_onetable)))))) /\ (forall dst_index_transform_reverse_onetable. (exists pvs_le_gap_transform_reverse_onetabledomain. pvs_le_gap_transform_reverse_onetabledomain + (dst_index_transform_reverse_onetable) = (N)) -> exists dst_positive_transform_reverse_onetable dst_negative_transform_reverse_onetable dst_value_transform_reverse_onetable. ((((exists ff_h_pvs_transform_reverse_onetableentrypositive. ff_h_pvs_transform_reverse_onetableentrypositive + S (dst_positive_transform_reverse_onetable) = S ((S (dst_index_transform_reverse_onetable)) * dst_positive_scale_transform_reverse_onetable)) /\ exists ff_q_pvs_transform_reverse_onetableentrypositive. dst_positive_code_transform_reverse_onetable = ff_q_pvs_transform_reverse_onetableentrypositive * S ((S (dst_index_transform_reverse_onetable)) * dst_positive_scale_transform_reverse_onetable) + (dst_positive_transform_reverse_onetable))) /\ (((((exists ff_h_pvs_transform_reverse_onetableentrynegative. ff_h_pvs_transform_reverse_onetableentrynegative + S (dst_negative_transform_reverse_onetable) = S ((S (dst_index_transform_reverse_onetable)) * dst_negative_scale_transform_reverse_onetable)) /\ exists ff_q_pvs_transform_reverse_onetableentrynegative. dst_negative_code_transform_reverse_onetable = ff_q_pvs_transform_reverse_onetableentrynegative * S ((S (dst_index_transform_reverse_onetable)) * dst_negative_scale_transform_reverse_onetable) + (dst_negative_transform_reverse_onetable))) /\ (exists ge_balance_positive_transform_reverse_onetableentryvalue ge_balance_negative_transform_reverse_onetableentryvalue. (((((dst_value_transform_reverse_onetable) = 2 * (ge_balance_positive_transform_reverse_onetableentryvalue) /\ (ge_balance_negative_transform_reverse_onetableentryvalue) = 0) \/ exists ge_signed_half_transform_reverse_onetableentryvaluedecode. (((dst_value_transform_reverse_onetable) = 2 * ge_signed_half_transform_reverse_onetableentryvaluedecode + 1 /\ (ge_balance_positive_transform_reverse_onetableentryvalue) = 0) /\ (ge_balance_negative_transform_reverse_onetableentryvalue) = S ge_signed_half_transform_reverse_onetableentryvaluedecode))) /\ ((dst_positive_transform_reverse_onetable) + ge_balance_negative_transform_reverse_onetableentryvalue = (dst_negative_transform_reverse_onetable) + ge_balance_positive_transform_reverse_onetableentryvalue))))))))) /\ (forall du_index_transform_reverse_one du_value_transform_reverse_one. ~(du_index_transform_reverse_one=0) -> (exists pvs_le_gap_transform_reverse_onebound. pvs_le_gap_transform_reverse_onebound + (du_index_transform_reverse_one) = (N)) -> (exists dst_positive_code_transform_reverse_oneentry dst_positive_scale_transform_reverse_oneentry dst_negative_code_transform_reverse_oneentry dst_negative_scale_transform_reverse_oneentry dst_positive_transform_reverse_oneentry dst_negative_transform_reverse_oneentry. (((U) = (((((dst_positive_code_transform_reverse_oneentry) + (dst_positive_scale_transform_reverse_oneentry)) * S ((dst_positive_code_transform_reverse_oneentry) + (dst_positive_scale_transform_reverse_oneentry)) + ((dst_positive_scale_transform_reverse_oneentry) + (dst_positive_scale_transform_reverse_oneentry))) + (((dst_negative_code_transform_reverse_oneentry) + (dst_negative_scale_transform_reverse_oneentry)) * S ((dst_negative_code_transform_reverse_oneentry) + (dst_negative_scale_transform_reverse_oneentry)) + ((dst_negative_scale_transform_reverse_oneentry) + (dst_negative_scale_transform_reverse_oneentry)))) * S ((((dst_positive_code_transform_reverse_oneentry) + (dst_positive_scale_transform_reverse_oneentry)) * S ((dst_positive_code_transform_reverse_oneentry) + (dst_positive_scale_transform_reverse_oneentry)) + ((dst_positive_scale_transform_reverse_oneentry) + (dst_positive_scale_transform_reverse_oneentry))) + (((dst_negative_code_transform_reverse_oneentry) + (dst_negative_scale_transform_reverse_oneentry)) * S ((dst_negative_code_transform_reverse_oneentry) + (dst_negative_scale_transform_reverse_oneentry)) + ((dst_negative_scale_transform_reverse_oneentry) + (dst_negative_scale_transform_reverse_oneentry)))) + ((((dst_negative_code_transform_reverse_oneentry) + (dst_negative_scale_transform_reverse_oneentry)) * S ((dst_negative_code_transform_reverse_oneentry) + (dst_negative_scale_transform_reverse_oneentry)) + ((dst_negative_scale_transform_reverse_oneentry) + (dst_negative_scale_transform_reverse_oneentry))) + (((dst_negative_code_transform_reverse_oneentry) + (dst_negative_scale_transform_reverse_oneentry)) * S ((dst_negative_code_transform_reverse_oneentry) + (dst_negative_scale_transform_reverse_oneentry)) + ((dst_negative_scale_transform_reverse_oneentry) + (dst_negative_scale_transform_reverse_oneentry)))))) /\ (((((exists ff_h_pvs_transform_reverse_oneentrypositive. ff_h_pvs_transform_reverse_oneentrypositive + S (dst_positive_transform_reverse_oneentry) = S ((S (du_index_transform_reverse_one)) * dst_positive_scale_transform_reverse_oneentry)) /\ exists ff_q_pvs_transform_reverse_oneentrypositive. dst_positive_code_transform_reverse_oneentry = ff_q_pvs_transform_reverse_oneentrypositive * S ((S (du_index_transform_reverse_one)) * dst_positive_scale_transform_reverse_oneentry) + (dst_positive_transform_reverse_oneentry))) /\ (((((exists ff_h_pvs_transform_reverse_oneentrynegative. ff_h_pvs_transform_reverse_oneentrynegative + S (dst_negative_transform_reverse_oneentry) = S ((S (du_index_transform_reverse_one)) * dst_negative_scale_transform_reverse_oneentry)) /\ exists ff_q_pvs_transform_reverse_oneentrynegative. dst_negative_code_transform_reverse_oneentry = ff_q_pvs_transform_reverse_oneentrynegative * S ((S (du_index_transform_reverse_one)) * dst_negative_scale_transform_reverse_oneentry) + (dst_negative_transform_reverse_oneentry))) /\ (exists ge_balance_positive_transform_reverse_oneentryvalue ge_balance_negative_transform_reverse_oneentryvalue. (((((du_value_transform_reverse_one) = 2 * (ge_balance_positive_transform_reverse_oneentryvalue) /\ (ge_balance_negative_transform_reverse_oneentryvalue) = 0) \/ exists ge_signed_half_transform_reverse_oneentryvaluedecode. (((du_value_transform_reverse_one) = 2 * ge_signed_half_transform_reverse_oneentryvaluedecode + 1 /\ (ge_balance_positive_transform_reverse_oneentryvalue) = 0) /\ (ge_balance_negative_transform_reverse_oneentryvalue) = S ge_signed_half_transform_reverse_oneentryvaluedecode))) /\ ((dst_positive_transform_reverse_oneentry) + ge_balance_negative_transform_reverse_oneentryvalue = (dst_negative_transform_reverse_oneentry) + ge_balance_positive_transform_reverse_oneentryvalue))))))))) -> du_value_transform_reverse_one=2))) -> (((exists dst_positive_code_transform_reverse_sourceleft dst_positive_scale_transform_reverse_sourceleft dst_negative_code_transform_reverse_sourceleft dst_negative_scale_transform_reverse_sourceleft. (((F) = (((((dst_positive_code_transform_reverse_sourceleft) + (dst_positive_scale_transform_reverse_sourceleft)) * S ((dst_positive_code_transform_reverse_sourceleft) + (dst_positive_scale_transform_reverse_sourceleft)) + ((dst_positive_scale_transform_reverse_sourceleft) + (dst_positive_scale_transform_reverse_sourceleft))) + (((dst_negative_code_transform_reverse_sourceleft) + (dst_negative_scale_transform_reverse_sourceleft)) * S ((dst_negative_code_transform_reverse_sourceleft) + (dst_negative_scale_transform_reverse_sourceleft)) + ((dst_negative_scale_transform_reverse_sourceleft) + (dst_negative_scale_transform_reverse_sourceleft)))) * S ((((dst_positive_code_transform_reverse_sourceleft) + (dst_positive_scale_transform_reverse_sourceleft)) * S ((dst_positive_code_transform_reverse_sourceleft) + (dst_positive_scale_transform_reverse_sourceleft)) + ((dst_positive_scale_transform_reverse_sourceleft) + (dst_positive_scale_transform_reverse_sourceleft))) + (((dst_negative_code_transform_reverse_sourceleft) + (dst_negative_scale_transform_reverse_sourceleft)) * S ((dst_negative_code_transform_reverse_sourceleft) + (dst_negative_scale_transform_reverse_sourceleft)) + ((dst_negative_scale_transform_reverse_sourceleft) + (dst_negative_scale_transform_reverse_sourceleft)))) + ((((dst_negative_code_transform_reverse_sourceleft) + (dst_negative_scale_transform_reverse_sourceleft)) * S ((dst_negative_code_transform_reverse_sourceleft) + (dst_negative_scale_transform_reverse_sourceleft)) + ((dst_negative_scale_transform_reverse_sourceleft) + (dst_negative_scale_transform_reverse_sourceleft))) + (((dst_negative_code_transform_reverse_sourceleft) + (dst_negative_scale_transform_reverse_sourceleft)) * S ((dst_negative_code_transform_reverse_sourceleft) + (dst_negative_scale_transform_reverse_sourceleft)) + ((dst_negative_scale_transform_reverse_sourceleft) + (dst_negative_scale_transform_reverse_sourceleft)))))) /\ (forall dst_index_transform_reverse_sourceleft. (exists pvs_le_gap_transform_reverse_sourceleftdomain. pvs_le_gap_transform_reverse_sourceleftdomain + (dst_index_transform_reverse_sourceleft) = (N)) -> exists dst_positive_transform_reverse_sourceleft dst_negative_transform_reverse_sourceleft dst_value_transform_reverse_sourceleft. ((((exists ff_h_pvs_transform_reverse_sourceleftentrypositive. ff_h_pvs_transform_reverse_sourceleftentrypositive + S (dst_positive_transform_reverse_sourceleft) = S ((S (dst_index_transform_reverse_sourceleft)) * dst_positive_scale_transform_reverse_sourceleft)) /\ exists ff_q_pvs_transform_reverse_sourceleftentrypositive. dst_positive_code_transform_reverse_sourceleft = ff_q_pvs_transform_reverse_sourceleftentrypositive * S ((S (dst_index_transform_reverse_sourceleft)) * dst_positive_scale_transform_reverse_sourceleft) + (dst_positive_transform_reverse_sourceleft))) /\ (((((exists ff_h_pvs_transform_reverse_sourceleftentrynegative. ff_h_pvs_transform_reverse_sourceleftentrynegative + S (dst_negative_transform_reverse_sourceleft) = S ((S (dst_index_transform_reverse_sourceleft)) * dst_negative_scale_transform_reverse_sourceleft)) /\ exists ff_q_pvs_transform_reverse_sourceleftentrynegative. dst_negative_code_transform_reverse_sourceleft = ff_q_pvs_transform_reverse_sourceleftentrynegative * S ((S (dst_index_transform_reverse_sourceleft)) * dst_negative_scale_transform_reverse_sourceleft) + (dst_negative_transform_reverse_sourceleft))) /\ (exists ge_balance_positive_transform_reverse_sourceleftentryvalue ge_balance_negative_transform_reverse_sourceleftentryvalue. (((((dst_value_transform_reverse_sourceleft) = 2 * (ge_balance_positive_transform_reverse_sourceleftentryvalue) /\ (ge_balance_negative_transform_reverse_sourceleftentryvalue) = 0) \/ exists ge_signed_half_transform_reverse_sourceleftentryvaluedecode. (((dst_value_transform_reverse_sourceleft) = 2 * ge_signed_half_transform_reverse_sourceleftentryvaluedecode + 1 /\ (ge_balance_positive_transform_reverse_sourceleftentryvalue) = 0) /\ (ge_balance_negative_transform_reverse_sourceleftentryvalue) = S ge_signed_half_transform_reverse_sourceleftentryvaluedecode))) /\ ((dst_positive_transform_reverse_sourceleft) + ge_balance_negative_transform_reverse_sourceleftentryvalue = (dst_negative_transform_reverse_sourceleft) + ge_balance_positive_transform_reverse_sourceleftentryvalue))))))))) /\ (((exists dst_positive_code_transform_reverse_sourceright dst_positive_scale_transform_reverse_sourceright dst_negative_code_transform_reverse_sourceright dst_negative_scale_transform_reverse_sourceright. (((U) = (((((dst_positive_code_transform_reverse_sourceright) + (dst_positive_scale_transform_reverse_sourceright)) * S ((dst_positive_code_transform_reverse_sourceright) + (dst_positive_scale_transform_reverse_sourceright)) + ((dst_positive_scale_transform_reverse_sourceright) + (dst_positive_scale_transform_reverse_sourceright))) + (((dst_negative_code_transform_reverse_sourceright) + (dst_negative_scale_transform_reverse_sourceright)) * S ((dst_negative_code_transform_reverse_sourceright) + (dst_negative_scale_transform_reverse_sourceright)) + ((dst_negative_scale_transform_reverse_sourceright) + (dst_negative_scale_transform_reverse_sourceright)))) * S ((((dst_positive_code_transform_reverse_sourceright) + (dst_positive_scale_transform_reverse_sourceright)) * S ((dst_positive_code_transform_reverse_sourceright) + (dst_positive_scale_transform_reverse_sourceright)) + ((dst_positive_scale_transform_reverse_sourceright) + (dst_positive_scale_transform_reverse_sourceright))) + (((dst_negative_code_transform_reverse_sourceright) + (dst_negative_scale_transform_reverse_sourceright)) * S ((dst_negative_code_transform_reverse_sourceright) + (dst_negative_scale_transform_reverse_sourceright)) + ((dst_negative_scale_transform_reverse_sourceright) + (dst_negative_scale_transform_reverse_sourceright)))) + ((((dst_negative_code_transform_reverse_sourceright) + (dst_negative_scale_transform_reverse_sourceright)) * S ((dst_negative_code_transform_reverse_sourceright) + (dst_negative_scale_transform_reverse_sourceright)) + ((dst_negative_scale_transform_reverse_sourceright) + (dst_negative_scale_transform_reverse_sourceright))) + (((dst_negative_code_transform_reverse_sourceright) + (dst_negative_scale_transform_reverse_sourceright)) * S ((dst_negative_code_transform_reverse_sourceright) + (dst_negative_scale_transform_reverse_sourceright)) + ((dst_negative_scale_transform_reverse_sourceright) + (dst_negative_scale_transform_reverse_sourceright)))))) /\ (forall dst_index_transform_reverse_sourceright. (exists pvs_le_gap_transform_reverse_sourcerightdomain. pvs_le_gap_transform_reverse_sourcerightdomain + (dst_index_transform_reverse_sourceright) = (N)) -> exists dst_positive_transform_reverse_sourceright dst_negative_transform_reverse_sourceright dst_value_transform_reverse_sourceright. ((((exists ff_h_pvs_transform_reverse_sourcerightentrypositive. ff_h_pvs_transform_reverse_sourcerightentrypositive + S (dst_positive_transform_reverse_sourceright) = S ((S (dst_index_transform_reverse_sourceright)) * dst_positive_scale_transform_reverse_sourceright)) /\ exists ff_q_pvs_transform_reverse_sourcerightentrypositive. dst_positive_code_transform_reverse_sourceright = ff_q_pvs_transform_reverse_sourcerightentrypositive * S ((S (dst_index_transform_reverse_sourceright)) * dst_positive_scale_transform_reverse_sourceright) + (dst_positive_transform_reverse_sourceright))) /\ (((((exists ff_h_pvs_transform_reverse_sourcerightentrynegative. ff_h_pvs_transform_reverse_sourcerightentrynegative + S (dst_negative_transform_reverse_sourceright) = S ((S (dst_index_transform_reverse_sourceright)) * dst_negative_scale_transform_reverse_sourceright)) /\ exists ff_q_pvs_transform_reverse_sourcerightentrynegative. dst_negative_code_transform_reverse_sourceright = ff_q_pvs_transform_reverse_sourcerightentrynegative * S ((S (dst_index_transform_reverse_sourceright)) * dst_negative_scale_transform_reverse_sourceright) + (dst_negative_transform_reverse_sourceright))) /\ (exists ge_balance_positive_transform_reverse_sourcerightentryvalue ge_balance_negative_transform_reverse_sourcerightentryvalue. (((((dst_value_transform_reverse_sourceright) = 2 * (ge_balance_positive_transform_reverse_sourcerightentryvalue) /\ (ge_balance_negative_transform_reverse_sourcerightentryvalue) = 0) \/ exists ge_signed_half_transform_reverse_sourcerightentryvaluedecode. (((dst_value_transform_reverse_sourceright) = 2 * ge_signed_half_transform_reverse_sourcerightentryvaluedecode + 1 /\ (ge_balance_positive_transform_reverse_sourcerightentryvalue) = 0) /\ (ge_balance_negative_transform_reverse_sourcerightentryvalue) = S ge_signed_half_transform_reverse_sourcerightentryvaluedecode))) /\ ((dst_positive_transform_reverse_sourceright) + ge_balance_negative_transform_reverse_sourcerightentryvalue = (dst_negative_transform_reverse_sourceright) + ge_balance_positive_transform_reverse_sourcerightentryvalue))))))))) /\ (((exists dst_positive_code_transform_reverse_sourcetable dst_positive_scale_transform_reverse_sourcetable dst_negative_code_transform_reverse_sourcetable dst_negative_scale_transform_reverse_sourcetable. (((G) = (((((dst_positive_code_transform_reverse_sourcetable) + (dst_positive_scale_transform_reverse_sourcetable)) * S ((dst_positive_code_transform_reverse_sourcetable) + (dst_positive_scale_transform_reverse_sourcetable)) + ((dst_positive_scale_transform_reverse_sourcetable) + (dst_positive_scale_transform_reverse_sourcetable))) + (((dst_negative_code_transform_reverse_sourcetable) + (dst_negative_scale_transform_reverse_sourcetable)) * S ((dst_negative_code_transform_reverse_sourcetable) + (dst_negative_scale_transform_reverse_sourcetable)) + ((dst_negative_scale_transform_reverse_sourcetable) + (dst_negative_scale_transform_reverse_sourcetable)))) * S ((((dst_positive_code_transform_reverse_sourcetable) + (dst_positive_scale_transform_reverse_sourcetable)) * S ((dst_positive_code_transform_reverse_sourcetable) + (dst_positive_scale_transform_reverse_sourcetable)) + ((dst_positive_scale_transform_reverse_sourcetable) + (dst_positive_scale_transform_reverse_sourcetable))) + (((dst_negative_code_transform_reverse_sourcetable) + (dst_negative_scale_transform_reverse_sourcetable)) * S ((dst_negative_code_transform_reverse_sourcetable) + (dst_negative_scale_transform_reverse_sourcetable)) + ((dst_negative_scale_transform_reverse_sourcetable) + (dst_negative_scale_transform_reverse_sourcetable)))) + ((((dst_negative_code_transform_reverse_sourcetable) + (dst_negative_scale_transform_reverse_sourcetable)) * S ((dst_negative_code_transform_reverse_sourcetable) + (dst_negative_scale_transform_reverse_sourcetable)) + ((dst_negative_scale_transform_reverse_sourcetable) + (dst_negative_scale_transform_reverse_sourcetable))) + (((dst_negative_code_transform_reverse_sourcetable) + (dst_negative_scale_transform_reverse_sourcetable)) * S ((dst_negative_code_transform_reverse_sourcetable) + (dst_negative_scale_transform_reverse_sourcetable)) + ((dst_negative_scale_transform_reverse_sourcetable) + (dst_negative_scale_transform_reverse_sourcetable)))))) /\ (forall dst_index_transform_reverse_sourcetable. (exists pvs_le_gap_transform_reverse_sourcetabledomain. pvs_le_gap_transform_reverse_sourcetabledomain + (dst_index_transform_reverse_sourcetable) = (N)) -> exists dst_positive_transform_reverse_sourcetable dst_negative_transform_reverse_sourcetable dst_value_transform_reverse_sourcetable. ((((exists ff_h_pvs_transform_reverse_sourcetableentrypositive. ff_h_pvs_transform_reverse_sourcetableentrypositive + S (dst_positive_transform_reverse_sourcetable) = S ((S (dst_index_transform_reverse_sourcetable)) * dst_positive_scale_transform_reverse_sourcetable)) /\ exists ff_q_pvs_transform_reverse_sourcetableentrypositive. dst_positive_code_transform_reverse_sourcetable = ff_q_pvs_transform_reverse_sourcetableentrypositive * S ((S (dst_index_transform_reverse_sourcetable)) * dst_positive_scale_transform_reverse_sourcetable) + (dst_positive_transform_reverse_sourcetable))) /\ (((((exists ff_h_pvs_transform_reverse_sourcetableentrynegative. ff_h_pvs_transform_reverse_sourcetableentrynegative + S (dst_negative_transform_reverse_sourcetable) = S ((S (dst_index_transform_reverse_sourcetable)) * dst_negative_scale_transform_reverse_sourcetable)) /\ exists ff_q_pvs_transform_reverse_sourcetableentrynegative. dst_negative_code_transform_reverse_sourcetable = ff_q_pvs_transform_reverse_sourcetableentrynegative * S ((S (dst_index_transform_reverse_sourcetable)) * dst_negative_scale_transform_reverse_sourcetable) + (dst_negative_transform_reverse_sourcetable))) /\ (exists ge_balance_positive_transform_reverse_sourcetableentryvalue ge_balance_negative_transform_reverse_sourcetableentryvalue. (((((dst_value_transform_reverse_sourcetable) = 2 * (ge_balance_positive_transform_reverse_sourcetableentryvalue) /\ (ge_balance_negative_transform_reverse_sourcetableentryvalue) = 0) \/ exists ge_signed_half_transform_reverse_sourcetableentryvaluedecode. (((dst_value_transform_reverse_sourcetable) = 2 * ge_signed_half_transform_reverse_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_transform_reverse_sourcetableentryvalue) = 0) /\ (ge_balance_negative_transform_reverse_sourcetableentryvalue) = S ge_signed_half_transform_reverse_sourcetableentryvaluedecode))) /\ ((dst_positive_transform_reverse_sourcetable) + ge_balance_negative_transform_reverse_sourcetableentryvalue = (dst_negative_transform_reverse_sourcetable) + ge_balance_positive_transform_reverse_sourcetableentryvalue))))))))) /\ (forall dc_input_transform_reverse_source dc_output_transform_reverse_source. ~(dc_input_transform_reverse_source=0) -> (exists pvs_le_gap_transform_reverse_sourcedomain. pvs_le_gap_transform_reverse_sourcedomain + (dc_input_transform_reverse_source) = (N)) -> (exists dst_positive_code_transform_reverse_sourcelookup dst_positive_scale_transform_reverse_sourcelookup dst_negative_code_transform_reverse_sourcelookup dst_negative_scale_transform_reverse_sourcelookup dst_positive_transform_reverse_sourcelookup dst_negative_transform_reverse_sourcelookup. (((G) = (((((dst_positive_code_transform_reverse_sourcelookup) + (dst_positive_scale_transform_reverse_sourcelookup)) * S ((dst_positive_code_transform_reverse_sourcelookup) + (dst_positive_scale_transform_reverse_sourcelookup)) + ((dst_positive_scale_transform_reverse_sourcelookup) + (dst_positive_scale_transform_reverse_sourcelookup))) + (((dst_negative_code_transform_reverse_sourcelookup) + (dst_negative_scale_transform_reverse_sourcelookup)) * S ((dst_negative_code_transform_reverse_sourcelookup) + (dst_negative_scale_transform_reverse_sourcelookup)) + ((dst_negative_scale_transform_reverse_sourcelookup) + (dst_negative_scale_transform_reverse_sourcelookup)))) * S ((((dst_positive_code_transform_reverse_sourcelookup) + (dst_positive_scale_transform_reverse_sourcelookup)) * S ((dst_positive_code_transform_reverse_sourcelookup) + (dst_positive_scale_transform_reverse_sourcelookup)) + ((dst_positive_scale_transform_reverse_sourcelookup) + (dst_positive_scale_transform_reverse_sourcelookup))) + (((dst_negative_code_transform_reverse_sourcelookup) + (dst_negative_scale_transform_reverse_sourcelookup)) * S ((dst_negative_code_transform_reverse_sourcelookup) + (dst_negative_scale_transform_reverse_sourcelookup)) + ((dst_negative_scale_transform_reverse_sourcelookup) + (dst_negative_scale_transform_reverse_sourcelookup)))) + ((((dst_negative_code_transform_reverse_sourcelookup) + (dst_negative_scale_transform_reverse_sourcelookup)) * S ((dst_negative_code_transform_reverse_sourcelookup) + (dst_negative_scale_transform_reverse_sourcelookup)) + ((dst_negative_scale_transform_reverse_sourcelookup) + (dst_negative_scale_transform_reverse_sourcelookup))) + (((dst_negative_code_transform_reverse_sourcelookup) + (dst_negative_scale_transform_reverse_sourcelookup)) * S ((dst_negative_code_transform_reverse_sourcelookup) + (dst_negative_scale_transform_reverse_sourcelookup)) + ((dst_negative_scale_transform_reverse_sourcelookup) + (dst_negative_scale_transform_reverse_sourcelookup)))))) /\ (((((exists ff_h_pvs_transform_reverse_sourcelookuppositive. ff_h_pvs_transform_reverse_sourcelookuppositive + S (dst_positive_transform_reverse_sourcelookup) = S ((S (dc_input_transform_reverse_source)) * dst_positive_scale_transform_reverse_sourcelookup)) /\ exists ff_q_pvs_transform_reverse_sourcelookuppositive. dst_positive_code_transform_reverse_sourcelookup = ff_q_pvs_transform_reverse_sourcelookuppositive * S ((S (dc_input_transform_reverse_source)) * dst_positive_scale_transform_reverse_sourcelookup) + (dst_positive_transform_reverse_sourcelookup))) /\ (((((exists ff_h_pvs_transform_reverse_sourcelookupnegative. ff_h_pvs_transform_reverse_sourcelookupnegative + S (dst_negative_transform_reverse_sourcelookup) = S ((S (dc_input_transform_reverse_source)) * dst_negative_scale_transform_reverse_sourcelookup)) /\ exists ff_q_pvs_transform_reverse_sourcelookupnegative. dst_negative_code_transform_reverse_sourcelookup = ff_q_pvs_transform_reverse_sourcelookupnegative * S ((S (dc_input_transform_reverse_source)) * dst_negative_scale_transform_reverse_sourcelookup) + (dst_negative_transform_reverse_sourcelookup))) /\ (exists ge_balance_positive_transform_reverse_sourcelookupvalue ge_balance_negative_transform_reverse_sourcelookupvalue. (((((dc_output_transform_reverse_source) = 2 * (ge_balance_positive_transform_reverse_sourcelookupvalue) /\ (ge_balance_negative_transform_reverse_sourcelookupvalue) = 0) \/ exists ge_signed_half_transform_reverse_sourcelookupvaluedecode. (((dc_output_transform_reverse_source) = 2 * ge_signed_half_transform_reverse_sourcelookupvaluedecode + 1 /\ (ge_balance_positive_transform_reverse_sourcelookupvalue) = 0) /\ (ge_balance_negative_transform_reverse_sourcelookupvalue) = S ge_signed_half_transform_reverse_sourcelookupvaluedecode))) /\ ((dst_positive_transform_reverse_sourcelookup) + ge_balance_negative_transform_reverse_sourcelookupvalue = (dst_negative_transform_reverse_sourcelookup) + ge_balance_positive_transform_reverse_sourcelookupvalue))))))))) -> (((~((dc_input_transform_reverse_source)=0)) /\ (exists dc_mask_transform_reverse_sourcevalue. ((((exists dst_positive_code_transform_reverse_sourcevaluemasktable dst_positive_scale_transform_reverse_sourcevaluemasktable dst_negative_code_transform_reverse_sourcevaluemasktable dst_negative_scale_transform_reverse_sourcevaluemasktable. (((dc_mask_transform_reverse_sourcevalue) = (((((dst_positive_code_transform_reverse_sourcevaluemasktable) + (dst_positive_scale_transform_reverse_sourcevaluemasktable)) * S ((dst_positive_code_transform_reverse_sourcevaluemasktable) + (dst_positive_scale_transform_reverse_sourcevaluemasktable)) + ((dst_positive_scale_transform_reverse_sourcevaluemasktable) + (dst_positive_scale_transform_reverse_sourcevaluemasktable))) + (((dst_negative_code_transform_reverse_sourcevaluemasktable) + (dst_negative_scale_transform_reverse_sourcevaluemasktable)) * S ((dst_negative_code_transform_reverse_sourcevaluemasktable) + (dst_negative_scale_transform_reverse_sourcevaluemasktable)) + ((dst_negative_scale_transform_reverse_sourcevaluemasktable) + (dst_negative_scale_transform_reverse_sourcevaluemasktable)))) * S ((((dst_positive_code_transform_reverse_sourcevaluemasktable) + (dst_positive_scale_transform_reverse_sourcevaluemasktable)) * S ((dst_positive_code_transform_reverse_sourcevaluemasktable) + (dst_positive_scale_transform_reverse_sourcevaluemasktable)) + ((dst_positive_scale_transform_reverse_sourcevaluemasktable) + (dst_positive_scale_transform_reverse_sourcevaluemasktable))) + (((dst_negative_code_transform_reverse_sourcevaluemasktable) + (dst_negative_scale_transform_reverse_sourcevaluemasktable)) * S ((dst_negative_code_transform_reverse_sourcevaluemasktable) + (dst_negative_scale_transform_reverse_sourcevaluemasktable)) + ((dst_negative_scale_transform_reverse_sourcevaluemasktable) + (dst_negative_scale_transform_reverse_sourcevaluemasktable)))) + ((((dst_negative_code_transform_reverse_sourcevaluemasktable) + (dst_negative_scale_transform_reverse_sourcevaluemasktable)) * S ((dst_negative_code_transform_reverse_sourcevaluemasktable) + (dst_negative_scale_transform_reverse_sourcevaluemasktable)) + ((dst_negative_scale_transform_reverse_sourcevaluemasktable) + (dst_negative_scale_transform_reverse_sourcevaluemasktable))) + (((dst_negative_code_transform_reverse_sourcevaluemasktable) + (dst_negative_scale_transform_reverse_sourcevaluemasktable)) * S ((dst_negative_code_transform_reverse_sourcevaluemasktable) + (dst_negative_scale_transform_reverse_sourcevaluemasktable)) + ((dst_negative_scale_transform_reverse_sourcevaluemasktable) + (dst_negative_scale_transform_reverse_sourcevaluemasktable)))))) /\ (forall dst_index_transform_reverse_sourcevaluemasktable. (exists pvs_le_gap_transform_reverse_sourcevaluemasktabledomain. pvs_le_gap_transform_reverse_sourcevaluemasktabledomain + (dst_index_transform_reverse_sourcevaluemasktable) = (dc_input_transform_reverse_source)) -> exists dst_positive_transform_reverse_sourcevaluemasktable dst_negative_transform_reverse_sourcevaluemasktable dst_value_transform_reverse_sourcevaluemasktable. ((((exists ff_h_pvs_transform_reverse_sourcevaluemasktableentrypositive. ff_h_pvs_transform_reverse_sourcevaluemasktableentrypositive + S (dst_positive_transform_reverse_sourcevaluemasktable) = S ((S (dst_index_transform_reverse_sourcevaluemasktable)) * dst_positive_scale_transform_reverse_sourcevaluemasktable)) /\ exists ff_q_pvs_transform_reverse_sourcevaluemasktableentrypositive. dst_positive_code_transform_reverse_sourcevaluemasktable = ff_q_pvs_transform_reverse_sourcevaluemasktableentrypositive * S ((S (dst_index_transform_reverse_sourcevaluemasktable)) * dst_positive_scale_transform_reverse_sourcevaluemasktable) + (dst_positive_transform_reverse_sourcevaluemasktable))) /\ (((((exists ff_h_pvs_transform_reverse_sourcevaluemasktableentrynegative. ff_h_pvs_transform_reverse_sourcevaluemasktableentrynegative + S (dst_negative_transform_reverse_sourcevaluemasktable) = S ((S (dst_index_transform_reverse_sourcevaluemasktable)) * dst_negative_scale_transform_reverse_sourcevaluemasktable)) /\ exists ff_q_pvs_transform_reverse_sourcevaluemasktableentrynegative. dst_negative_code_transform_reverse_sourcevaluemasktable = ff_q_pvs_transform_reverse_sourcevaluemasktableentrynegative * S ((S (dst_index_transform_reverse_sourcevaluemasktable)) * dst_negative_scale_transform_reverse_sourcevaluemasktable) + (dst_negative_transform_reverse_sourcevaluemasktable))) /\ (exists ge_balance_positive_transform_reverse_sourcevaluemasktableentryvalue ge_balance_negative_transform_reverse_sourcevaluemasktableentryvalue. (((((dst_value_transform_reverse_sourcevaluemasktable) = 2 * (ge_balance_positive_transform_reverse_sourcevaluemasktableentryvalue) /\ (ge_balance_negative_transform_reverse_sourcevaluemasktableentryvalue) = 0) \/ exists ge_signed_half_transform_reverse_sourcevaluemasktableentryvaluedecode. (((dst_value_transform_reverse_sourcevaluemasktable) = 2 * ge_signed_half_transform_reverse_sourcevaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_transform_reverse_sourcevaluemasktableentryvalue) = 0) /\ (ge_balance_negative_transform_reverse_sourcevaluemasktableentryvalue) = S ge_signed_half_transform_reverse_sourcevaluemasktableentryvaluedecode))) /\ ((dst_positive_transform_reverse_sourcevaluemasktable) + ge_balance_negative_transform_reverse_sourcevaluemasktableentryvalue = (dst_negative_transform_reverse_sourcevaluemasktable) + ge_balance_positive_transform_reverse_sourcevaluemasktableentryvalue))))))))) /\ (forall dc_index_transform_reverse_sourcevaluemask dc_value_transform_reverse_sourcevaluemask. (exists pvs_le_gap_transform_reverse_sourcevaluemaskdomain. pvs_le_gap_transform_reverse_sourcevaluemaskdomain + (dc_index_transform_reverse_sourcevaluemask) = (dc_input_transform_reverse_source)) -> (exists dst_positive_code_transform_reverse_sourcevaluemasklookup dst_positive_scale_transform_reverse_sourcevaluemasklookup dst_negative_code_transform_reverse_sourcevaluemasklookup dst_negative_scale_transform_reverse_sourcevaluemasklookup dst_positive_transform_reverse_sourcevaluemasklookup dst_negative_transform_reverse_sourcevaluemasklookup. (((dc_mask_transform_reverse_sourcevalue) = (((((dst_positive_code_transform_reverse_sourcevaluemasklookup) + (dst_positive_scale_transform_reverse_sourcevaluemasklookup)) * S ((dst_positive_code_transform_reverse_sourcevaluemasklookup) + (dst_positive_scale_transform_reverse_sourcevaluemasklookup)) + ((dst_positive_scale_transform_reverse_sourcevaluemasklookup) + (dst_positive_scale_transform_reverse_sourcevaluemasklookup))) + (((dst_negative_code_transform_reverse_sourcevaluemasklookup) + (dst_negative_scale_transform_reverse_sourcevaluemasklookup)) * S ((dst_negative_code_transform_reverse_sourcevaluemasklookup) + (dst_negative_scale_transform_reverse_sourcevaluemasklookup)) + ((dst_negative_scale_transform_reverse_sourcevaluemasklookup) + (dst_negative_scale_transform_reverse_sourcevaluemasklookup)))) * S ((((dst_positive_code_transform_reverse_sourcevaluemasklookup) + (dst_positive_scale_transform_reverse_sourcevaluemasklookup)) * S ((dst_positive_code_transform_reverse_sourcevaluemasklookup) + (dst_positive_scale_transform_reverse_sourcevaluemasklookup)) + ((dst_positive_scale_transform_reverse_sourcevaluemasklookup) + (dst_positive_scale_transform_reverse_sourcevaluemasklookup))) + (((dst_negative_code_transform_reverse_sourcevaluemasklookup) + (dst_negative_scale_transform_reverse_sourcevaluemasklookup)) * S ((dst_negative_code_transform_reverse_sourcevaluemasklookup) + (dst_negative_scale_transform_reverse_sourcevaluemasklookup)) + ((dst_negative_scale_transform_reverse_sourcevaluemasklookup) + (dst_negative_scale_transform_reverse_sourcevaluemasklookup)))) + ((((dst_negative_code_transform_reverse_sourcevaluemasklookup) + (dst_negative_scale_transform_reverse_sourcevaluemasklookup)) * S ((dst_negative_code_transform_reverse_sourcevaluemasklookup) + (dst_negative_scale_transform_reverse_sourcevaluemasklookup)) + ((dst_negative_scale_transform_reverse_sourcevaluemasklookup) + (dst_negative_scale_transform_reverse_sourcevaluemasklookup))) + (((dst_negative_code_transform_reverse_sourcevaluemasklookup) + (dst_negative_scale_transform_reverse_sourcevaluemasklookup)) * S ((dst_negative_code_transform_reverse_sourcevaluemasklookup) + (dst_negative_scale_transform_reverse_sourcevaluemasklookup)) + ((dst_negative_scale_transform_reverse_sourcevaluemasklookup) + (dst_negative_scale_transform_reverse_sourcevaluemasklookup)))))) /\ (((((exists ff_h_pvs_transform_reverse_sourcevaluemasklookuppositive. ff_h_pvs_transform_reverse_sourcevaluemasklookuppositive + S (dst_positive_transform_reverse_sourcevaluemasklookup) = S ((S (dc_index_transform_reverse_sourcevaluemask)) * dst_positive_scale_transform_reverse_sourcevaluemasklookup)) /\ exists ff_q_pvs_transform_reverse_sourcevaluemasklookuppositive. dst_positive_code_transform_reverse_sourcevaluemasklookup = ff_q_pvs_transform_reverse_sourcevaluemasklookuppositive * S ((S (dc_index_transform_reverse_sourcevaluemask)) * dst_positive_scale_transform_reverse_sourcevaluemasklookup) + (dst_positive_transform_reverse_sourcevaluemasklookup))) /\ (((((exists ff_h_pvs_transform_reverse_sourcevaluemasklookupnegative. ff_h_pvs_transform_reverse_sourcevaluemasklookupnegative + S (dst_negative_transform_reverse_sourcevaluemasklookup) = S ((S (dc_index_transform_reverse_sourcevaluemask)) * dst_negative_scale_transform_reverse_sourcevaluemasklookup)) /\ exists ff_q_pvs_transform_reverse_sourcevaluemasklookupnegative. dst_negative_code_transform_reverse_sourcevaluemasklookup = ff_q_pvs_transform_reverse_sourcevaluemasklookupnegative * S ((S (dc_index_transform_reverse_sourcevaluemask)) * dst_negative_scale_transform_reverse_sourcevaluemasklookup) + (dst_negative_transform_reverse_sourcevaluemasklookup))) /\ (exists ge_balance_positive_transform_reverse_sourcevaluemasklookupvalue ge_balance_negative_transform_reverse_sourcevaluemasklookupvalue. (((((dc_value_transform_reverse_sourcevaluemask) = 2 * (ge_balance_positive_transform_reverse_sourcevaluemasklookupvalue) /\ (ge_balance_negative_transform_reverse_sourcevaluemasklookupvalue) = 0) \/ exists ge_signed_half_transform_reverse_sourcevaluemasklookupvaluedecode. (((dc_value_transform_reverse_sourcevaluemask) = 2 * ge_signed_half_transform_reverse_sourcevaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_transform_reverse_sourcevaluemasklookupvalue) = 0) /\ (ge_balance_negative_transform_reverse_sourcevaluemasklookupvalue) = S ge_signed_half_transform_reverse_sourcevaluemasklookupvaluedecode))) /\ ((dst_positive_transform_reverse_sourcevaluemasklookup) + ge_balance_negative_transform_reverse_sourcevaluemasklookupvalue = (dst_negative_transform_reverse_sourcevaluemasklookup) + ge_balance_positive_transform_reverse_sourcevaluemasklookupvalue))))))))) -> ((((~((dc_index_transform_reverse_sourcevaluemask)=0)) /\ (exists dc_quotient_transform_reverse_sourcevaluemaskentry dc_left_transform_reverse_sourcevaluemaskentry dc_right_transform_reverse_sourcevaluemaskentry. (((dc_input_transform_reverse_source)=(dc_index_transform_reverse_sourcevaluemask)*dc_quotient_transform_reverse_sourcevaluemaskentry) /\ (((exists dst_positive_code_transform_reverse_sourcevaluemaskentryleft dst_positive_scale_transform_reverse_sourcevaluemaskentryleft dst_negative_code_transform_reverse_sourcevaluemaskentryleft dst_negative_scale_transform_reverse_sourcevaluemaskentryleft dst_positive_transform_reverse_sourcevaluemaskentryleft dst_negative_transform_reverse_sourcevaluemaskentryleft. (((F) = (((((dst_positive_code_transform_reverse_sourcevaluemaskentryleft) + (dst_positive_scale_transform_reverse_sourcevaluemaskentryleft)) * S ((dst_positive_code_transform_reverse_sourcevaluemaskentryleft) + (dst_positive_scale_transform_reverse_sourcevaluemaskentryleft)) + ((dst_positive_scale_transform_reverse_sourcevaluemaskentryleft) + (dst_positive_scale_transform_reverse_sourcevaluemaskentryleft))) + (((dst_negative_code_transform_reverse_sourcevaluemaskentryleft) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryleft)) * S ((dst_negative_code_transform_reverse_sourcevaluemaskentryleft) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryleft)) + ((dst_negative_scale_transform_reverse_sourcevaluemaskentryleft) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryleft)))) * S ((((dst_positive_code_transform_reverse_sourcevaluemaskentryleft) + (dst_positive_scale_transform_reverse_sourcevaluemaskentryleft)) * S ((dst_positive_code_transform_reverse_sourcevaluemaskentryleft) + (dst_positive_scale_transform_reverse_sourcevaluemaskentryleft)) + ((dst_positive_scale_transform_reverse_sourcevaluemaskentryleft) + (dst_positive_scale_transform_reverse_sourcevaluemaskentryleft))) + (((dst_negative_code_transform_reverse_sourcevaluemaskentryleft) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryleft)) * S ((dst_negative_code_transform_reverse_sourcevaluemaskentryleft) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryleft)) + ((dst_negative_scale_transform_reverse_sourcevaluemaskentryleft) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryleft)))) + ((((dst_negative_code_transform_reverse_sourcevaluemaskentryleft) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryleft)) * S ((dst_negative_code_transform_reverse_sourcevaluemaskentryleft) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryleft)) + ((dst_negative_scale_transform_reverse_sourcevaluemaskentryleft) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryleft))) + (((dst_negative_code_transform_reverse_sourcevaluemaskentryleft) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryleft)) * S ((dst_negative_code_transform_reverse_sourcevaluemaskentryleft) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryleft)) + ((dst_negative_scale_transform_reverse_sourcevaluemaskentryleft) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_transform_reverse_sourcevaluemaskentryleftpositive. ff_h_pvs_transform_reverse_sourcevaluemaskentryleftpositive + S (dst_positive_transform_reverse_sourcevaluemaskentryleft) = S ((S (dc_index_transform_reverse_sourcevaluemask)) * dst_positive_scale_transform_reverse_sourcevaluemaskentryleft)) /\ exists ff_q_pvs_transform_reverse_sourcevaluemaskentryleftpositive. dst_positive_code_transform_reverse_sourcevaluemaskentryleft = ff_q_pvs_transform_reverse_sourcevaluemaskentryleftpositive * S ((S (dc_index_transform_reverse_sourcevaluemask)) * dst_positive_scale_transform_reverse_sourcevaluemaskentryleft) + (dst_positive_transform_reverse_sourcevaluemaskentryleft))) /\ (((((exists ff_h_pvs_transform_reverse_sourcevaluemaskentryleftnegative. ff_h_pvs_transform_reverse_sourcevaluemaskentryleftnegative + S (dst_negative_transform_reverse_sourcevaluemaskentryleft) = S ((S (dc_index_transform_reverse_sourcevaluemask)) * dst_negative_scale_transform_reverse_sourcevaluemaskentryleft)) /\ exists ff_q_pvs_transform_reverse_sourcevaluemaskentryleftnegative. dst_negative_code_transform_reverse_sourcevaluemaskentryleft = ff_q_pvs_transform_reverse_sourcevaluemaskentryleftnegative * S ((S (dc_index_transform_reverse_sourcevaluemask)) * dst_negative_scale_transform_reverse_sourcevaluemaskentryleft) + (dst_negative_transform_reverse_sourcevaluemaskentryleft))) /\ (exists ge_balance_positive_transform_reverse_sourcevaluemaskentryleftvalue ge_balance_negative_transform_reverse_sourcevaluemaskentryleftvalue. (((((dc_left_transform_reverse_sourcevaluemaskentry) = 2 * (ge_balance_positive_transform_reverse_sourcevaluemaskentryleftvalue) /\ (ge_balance_negative_transform_reverse_sourcevaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_transform_reverse_sourcevaluemaskentryleftvaluedecode. (((dc_left_transform_reverse_sourcevaluemaskentry) = 2 * ge_signed_half_transform_reverse_sourcevaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_transform_reverse_sourcevaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_transform_reverse_sourcevaluemaskentryleftvalue) = S ge_signed_half_transform_reverse_sourcevaluemaskentryleftvaluedecode))) /\ ((dst_positive_transform_reverse_sourcevaluemaskentryleft) + ge_balance_negative_transform_reverse_sourcevaluemaskentryleftvalue = (dst_negative_transform_reverse_sourcevaluemaskentryleft) + ge_balance_positive_transform_reverse_sourcevaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_transform_reverse_sourcevaluemaskentryright dst_positive_scale_transform_reverse_sourcevaluemaskentryright dst_negative_code_transform_reverse_sourcevaluemaskentryright dst_negative_scale_transform_reverse_sourcevaluemaskentryright dst_positive_transform_reverse_sourcevaluemaskentryright dst_negative_transform_reverse_sourcevaluemaskentryright. (((U) = (((((dst_positive_code_transform_reverse_sourcevaluemaskentryright) + (dst_positive_scale_transform_reverse_sourcevaluemaskentryright)) * S ((dst_positive_code_transform_reverse_sourcevaluemaskentryright) + (dst_positive_scale_transform_reverse_sourcevaluemaskentryright)) + ((dst_positive_scale_transform_reverse_sourcevaluemaskentryright) + (dst_positive_scale_transform_reverse_sourcevaluemaskentryright))) + (((dst_negative_code_transform_reverse_sourcevaluemaskentryright) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryright)) * S ((dst_negative_code_transform_reverse_sourcevaluemaskentryright) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryright)) + ((dst_negative_scale_transform_reverse_sourcevaluemaskentryright) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryright)))) * S ((((dst_positive_code_transform_reverse_sourcevaluemaskentryright) + (dst_positive_scale_transform_reverse_sourcevaluemaskentryright)) * S ((dst_positive_code_transform_reverse_sourcevaluemaskentryright) + (dst_positive_scale_transform_reverse_sourcevaluemaskentryright)) + ((dst_positive_scale_transform_reverse_sourcevaluemaskentryright) + (dst_positive_scale_transform_reverse_sourcevaluemaskentryright))) + (((dst_negative_code_transform_reverse_sourcevaluemaskentryright) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryright)) * S ((dst_negative_code_transform_reverse_sourcevaluemaskentryright) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryright)) + ((dst_negative_scale_transform_reverse_sourcevaluemaskentryright) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryright)))) + ((((dst_negative_code_transform_reverse_sourcevaluemaskentryright) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryright)) * S ((dst_negative_code_transform_reverse_sourcevaluemaskentryright) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryright)) + ((dst_negative_scale_transform_reverse_sourcevaluemaskentryright) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryright))) + (((dst_negative_code_transform_reverse_sourcevaluemaskentryright) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryright)) * S ((dst_negative_code_transform_reverse_sourcevaluemaskentryright) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryright)) + ((dst_negative_scale_transform_reverse_sourcevaluemaskentryright) + (dst_negative_scale_transform_reverse_sourcevaluemaskentryright)))))) /\ (((((exists ff_h_pvs_transform_reverse_sourcevaluemaskentryrightpositive. ff_h_pvs_transform_reverse_sourcevaluemaskentryrightpositive + S (dst_positive_transform_reverse_sourcevaluemaskentryright) = S ((S (dc_quotient_transform_reverse_sourcevaluemaskentry)) * dst_positive_scale_transform_reverse_sourcevaluemaskentryright)) /\ exists ff_q_pvs_transform_reverse_sourcevaluemaskentryrightpositive. dst_positive_code_transform_reverse_sourcevaluemaskentryright = ff_q_pvs_transform_reverse_sourcevaluemaskentryrightpositive * S ((S (dc_quotient_transform_reverse_sourcevaluemaskentry)) * dst_positive_scale_transform_reverse_sourcevaluemaskentryright) + (dst_positive_transform_reverse_sourcevaluemaskentryright))) /\ (((((exists ff_h_pvs_transform_reverse_sourcevaluemaskentryrightnegative. ff_h_pvs_transform_reverse_sourcevaluemaskentryrightnegative + S (dst_negative_transform_reverse_sourcevaluemaskentryright) = S ((S (dc_quotient_transform_reverse_sourcevaluemaskentry)) * dst_negative_scale_transform_reverse_sourcevaluemaskentryright)) /\ exists ff_q_pvs_transform_reverse_sourcevaluemaskentryrightnegative. dst_negative_code_transform_reverse_sourcevaluemaskentryright = ff_q_pvs_transform_reverse_sourcevaluemaskentryrightnegative * S ((S (dc_quotient_transform_reverse_sourcevaluemaskentry)) * dst_negative_scale_transform_reverse_sourcevaluemaskentryright) + (dst_negative_transform_reverse_sourcevaluemaskentryright))) /\ (exists ge_balance_positive_transform_reverse_sourcevaluemaskentryrightvalue ge_balance_negative_transform_reverse_sourcevaluemaskentryrightvalue. (((((dc_right_transform_reverse_sourcevaluemaskentry) = 2 * (ge_balance_positive_transform_reverse_sourcevaluemaskentryrightvalue) /\ (ge_balance_negative_transform_reverse_sourcevaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_transform_reverse_sourcevaluemaskentryrightvaluedecode. (((dc_right_transform_reverse_sourcevaluemaskentry) = 2 * ge_signed_half_transform_reverse_sourcevaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_transform_reverse_sourcevaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_transform_reverse_sourcevaluemaskentryrightvalue) = S ge_signed_half_transform_reverse_sourcevaluemaskentryrightvaluedecode))) /\ ((dst_positive_transform_reverse_sourcevaluemaskentryright) + ge_balance_negative_transform_reverse_sourcevaluemaskentryrightvalue = (dst_negative_transform_reverse_sourcevaluemaskentryright) + ge_balance_positive_transform_reverse_sourcevaluemaskentryrightvalue))))))))) /\ (exists sto_ap_transform_reverse_sourcevaluemaskentryproduct sto_an_transform_reverse_sourcevaluemaskentryproduct sto_bp_transform_reverse_sourcevaluemaskentryproduct sto_bn_transform_reverse_sourcevaluemaskentryproduct sto_cp_transform_reverse_sourcevaluemaskentryproduct sto_cn_transform_reverse_sourcevaluemaskentryproduct. (((((dc_left_transform_reverse_sourcevaluemaskentry) = 2 * (sto_ap_transform_reverse_sourcevaluemaskentryproduct) /\ (sto_an_transform_reverse_sourcevaluemaskentryproduct) = 0) \/ exists ge_signed_half_transform_reverse_sourcevaluemaskentryproductleft. (((dc_left_transform_reverse_sourcevaluemaskentry) = 2 * ge_signed_half_transform_reverse_sourcevaluemaskentryproductleft + 1 /\ (sto_ap_transform_reverse_sourcevaluemaskentryproduct) = 0) /\ (sto_an_transform_reverse_sourcevaluemaskentryproduct) = S ge_signed_half_transform_reverse_sourcevaluemaskentryproductleft))) /\ ((((((dc_right_transform_reverse_sourcevaluemaskentry) = 2 * (sto_bp_transform_reverse_sourcevaluemaskentryproduct) /\ (sto_bn_transform_reverse_sourcevaluemaskentryproduct) = 0) \/ exists ge_signed_half_transform_reverse_sourcevaluemaskentryproductright. (((dc_right_transform_reverse_sourcevaluemaskentry) = 2 * ge_signed_half_transform_reverse_sourcevaluemaskentryproductright + 1 /\ (sto_bp_transform_reverse_sourcevaluemaskentryproduct) = 0) /\ (sto_bn_transform_reverse_sourcevaluemaskentryproduct) = S ge_signed_half_transform_reverse_sourcevaluemaskentryproductright))) /\ ((((((dc_value_transform_reverse_sourcevaluemask) = 2 * (sto_cp_transform_reverse_sourcevaluemaskentryproduct) /\ (sto_cn_transform_reverse_sourcevaluemaskentryproduct) = 0) \/ exists ge_signed_half_transform_reverse_sourcevaluemaskentryproductoutput. (((dc_value_transform_reverse_sourcevaluemask) = 2 * ge_signed_half_transform_reverse_sourcevaluemaskentryproductoutput + 1 /\ (sto_cp_transform_reverse_sourcevaluemaskentryproduct) = 0) /\ (sto_cn_transform_reverse_sourcevaluemaskentryproduct) = S ge_signed_half_transform_reverse_sourcevaluemaskentryproductoutput))) /\ ((sto_ap_transform_reverse_sourcevaluemaskentryproduct * sto_bp_transform_reverse_sourcevaluemaskentryproduct + sto_an_transform_reverse_sourcevaluemaskentryproduct * sto_bn_transform_reverse_sourcevaluemaskentryproduct) + sto_cn_transform_reverse_sourcevaluemaskentryproduct = (sto_ap_transform_reverse_sourcevaluemaskentryproduct * sto_bn_transform_reverse_sourcevaluemaskentryproduct + sto_an_transform_reverse_sourcevaluemaskentryproduct * sto_bp_transform_reverse_sourcevaluemaskentryproduct) + sto_cp_transform_reverse_sourcevaluemaskentryproduct))))))))))))))) \/ ((((dc_index_transform_reverse_sourcevaluemask)=0 \/ ~(exists pvs_factor_transform_reverse_sourcevaluemaskentrynondivisor. (dc_input_transform_reverse_source) = (dc_index_transform_reverse_sourcevaluemask) * pvs_factor_transform_reverse_sourcevaluemaskentrynondivisor)) /\ ((dc_value_transform_reverse_sourcevaluemask)=0))))))) /\ (exists dst_positive_code_transform_reverse_sourcevaluefold dst_positive_scale_transform_reverse_sourcevaluefold dst_negative_code_transform_reverse_sourcevaluefold dst_negative_scale_transform_reverse_sourcevaluefold dst_positive_sum_transform_reverse_sourcevaluefold dst_negative_sum_transform_reverse_sourcevaluefold. (((dc_mask_transform_reverse_sourcevalue) = (((((dst_positive_code_transform_reverse_sourcevaluefold) + (dst_positive_scale_transform_reverse_sourcevaluefold)) * S ((dst_positive_code_transform_reverse_sourcevaluefold) + (dst_positive_scale_transform_reverse_sourcevaluefold)) + ((dst_positive_scale_transform_reverse_sourcevaluefold) + (dst_positive_scale_transform_reverse_sourcevaluefold))) + (((dst_negative_code_transform_reverse_sourcevaluefold) + (dst_negative_scale_transform_reverse_sourcevaluefold)) * S ((dst_negative_code_transform_reverse_sourcevaluefold) + (dst_negative_scale_transform_reverse_sourcevaluefold)) + ((dst_negative_scale_transform_reverse_sourcevaluefold) + (dst_negative_scale_transform_reverse_sourcevaluefold)))) * S ((((dst_positive_code_transform_reverse_sourcevaluefold) + (dst_positive_scale_transform_reverse_sourcevaluefold)) * S ((dst_positive_code_transform_reverse_sourcevaluefold) + (dst_positive_scale_transform_reverse_sourcevaluefold)) + ((dst_positive_scale_transform_reverse_sourcevaluefold) + (dst_positive_scale_transform_reverse_sourcevaluefold))) + (((dst_negative_code_transform_reverse_sourcevaluefold) + (dst_negative_scale_transform_reverse_sourcevaluefold)) * S ((dst_negative_code_transform_reverse_sourcevaluefold) + (dst_negative_scale_transform_reverse_sourcevaluefold)) + ((dst_negative_scale_transform_reverse_sourcevaluefold) + (dst_negative_scale_transform_reverse_sourcevaluefold)))) + ((((dst_negative_code_transform_reverse_sourcevaluefold) + (dst_negative_scale_transform_reverse_sourcevaluefold)) * S ((dst_negative_code_transform_reverse_sourcevaluefold) + (dst_negative_scale_transform_reverse_sourcevaluefold)) + ((dst_negative_scale_transform_reverse_sourcevaluefold) + (dst_negative_scale_transform_reverse_sourcevaluefold))) + (((dst_negative_code_transform_reverse_sourcevaluefold) + (dst_negative_scale_transform_reverse_sourcevaluefold)) * S ((dst_negative_code_transform_reverse_sourcevaluefold) + (dst_negative_scale_transform_reverse_sourcevaluefold)) + ((dst_negative_scale_transform_reverse_sourcevaluefold) + (dst_negative_scale_transform_reverse_sourcevaluefold)))))) /\ (((exists fs_u_dst_transform_reverse_sourcevaluefoldpositive fs_v_dst_transform_reverse_sourcevaluefoldpositive. ((((exists fs_h_dst_transform_reverse_sourcevaluefoldpositive_body_start. fs_h_dst_transform_reverse_sourcevaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_transform_reverse_sourcevaluefoldpositive)) /\ exists fs_q_dst_transform_reverse_sourcevaluefoldpositive_body_start. fs_u_dst_transform_reverse_sourcevaluefoldpositive = fs_q_dst_transform_reverse_sourcevaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_transform_reverse_sourcevaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_transform_reverse_sourcevaluefoldpositive_body_terminal. fs_h_dst_transform_reverse_sourcevaluefoldpositive_body_terminal + S (dst_positive_sum_transform_reverse_sourcevaluefold) = S ((S (S (dc_input_transform_reverse_source))) * fs_v_dst_transform_reverse_sourcevaluefoldpositive)) /\ exists fs_q_dst_transform_reverse_sourcevaluefoldpositive_body_terminal. fs_u_dst_transform_reverse_sourcevaluefoldpositive = fs_q_dst_transform_reverse_sourcevaluefoldpositive_body_terminal * S ((S (S (dc_input_transform_reverse_source))) * fs_v_dst_transform_reverse_sourcevaluefoldpositive) + (dst_positive_sum_transform_reverse_sourcevaluefold))) /\ forall fs_i_dst_transform_reverse_sourcevaluefoldpositive_body_steps. (exists fs_lt_dst_transform_reverse_sourcevaluefoldpositive_body_steps_bound. fs_lt_dst_transform_reverse_sourcevaluefoldpositive_body_steps_bound + S fs_i_dst_transform_reverse_sourcevaluefoldpositive_body_steps = S (dc_input_transform_reverse_source)) -> exists fs_a_dst_transform_reverse_sourcevaluefoldpositive_body_steps fs_r_dst_transform_reverse_sourcevaluefoldpositive_body_steps fs_s_dst_transform_reverse_sourcevaluefoldpositive_body_steps. ((((exists fs_h_dst_transform_reverse_sourcevaluefoldpositive_body_steps_summand. fs_h_dst_transform_reverse_sourcevaluefoldpositive_body_steps_summand + S (fs_a_dst_transform_reverse_sourcevaluefoldpositive_body_steps) = S ((S (fs_i_dst_transform_reverse_sourcevaluefoldpositive_body_steps)) * dst_positive_scale_transform_reverse_sourcevaluefold)) /\ exists fs_q_dst_transform_reverse_sourcevaluefoldpositive_body_steps_summand. dst_positive_code_transform_reverse_sourcevaluefold = fs_q_dst_transform_reverse_sourcevaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_transform_reverse_sourcevaluefoldpositive_body_steps)) * dst_positive_scale_transform_reverse_sourcevaluefold) + (fs_a_dst_transform_reverse_sourcevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_transform_reverse_sourcevaluefoldpositive_body_steps_partial. fs_h_dst_transform_reverse_sourcevaluefoldpositive_body_steps_partial + S (fs_r_dst_transform_reverse_sourcevaluefoldpositive_body_steps) = S ((S (fs_i_dst_transform_reverse_sourcevaluefoldpositive_body_steps)) * fs_v_dst_transform_reverse_sourcevaluefoldpositive)) /\ exists fs_q_dst_transform_reverse_sourcevaluefoldpositive_body_steps_partial. fs_u_dst_transform_reverse_sourcevaluefoldpositive = fs_q_dst_transform_reverse_sourcevaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_transform_reverse_sourcevaluefoldpositive_body_steps)) * fs_v_dst_transform_reverse_sourcevaluefoldpositive) + (fs_r_dst_transform_reverse_sourcevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_transform_reverse_sourcevaluefoldpositive_body_steps_successor. fs_h_dst_transform_reverse_sourcevaluefoldpositive_body_steps_successor + S (fs_s_dst_transform_reverse_sourcevaluefoldpositive_body_steps) = S ((S (S fs_i_dst_transform_reverse_sourcevaluefoldpositive_body_steps)) * fs_v_dst_transform_reverse_sourcevaluefoldpositive)) /\ exists fs_q_dst_transform_reverse_sourcevaluefoldpositive_body_steps_successor. fs_u_dst_transform_reverse_sourcevaluefoldpositive = fs_q_dst_transform_reverse_sourcevaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_transform_reverse_sourcevaluefoldpositive_body_steps)) * fs_v_dst_transform_reverse_sourcevaluefoldpositive) + (fs_s_dst_transform_reverse_sourcevaluefoldpositive_body_steps))) /\ fs_s_dst_transform_reverse_sourcevaluefoldpositive_body_steps = fs_r_dst_transform_reverse_sourcevaluefoldpositive_body_steps + fs_a_dst_transform_reverse_sourcevaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_transform_reverse_sourcevaluefoldnegative fs_v_dst_transform_reverse_sourcevaluefoldnegative. ((((exists fs_h_dst_transform_reverse_sourcevaluefoldnegative_body_start. fs_h_dst_transform_reverse_sourcevaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_transform_reverse_sourcevaluefoldnegative)) /\ exists fs_q_dst_transform_reverse_sourcevaluefoldnegative_body_start. fs_u_dst_transform_reverse_sourcevaluefoldnegative = fs_q_dst_transform_reverse_sourcevaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_transform_reverse_sourcevaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_transform_reverse_sourcevaluefoldnegative_body_terminal. fs_h_dst_transform_reverse_sourcevaluefoldnegative_body_terminal + S (dst_negative_sum_transform_reverse_sourcevaluefold) = S ((S (S (dc_input_transform_reverse_source))) * fs_v_dst_transform_reverse_sourcevaluefoldnegative)) /\ exists fs_q_dst_transform_reverse_sourcevaluefoldnegative_body_terminal. fs_u_dst_transform_reverse_sourcevaluefoldnegative = fs_q_dst_transform_reverse_sourcevaluefoldnegative_body_terminal * S ((S (S (dc_input_transform_reverse_source))) * fs_v_dst_transform_reverse_sourcevaluefoldnegative) + (dst_negative_sum_transform_reverse_sourcevaluefold))) /\ forall fs_i_dst_transform_reverse_sourcevaluefoldnegative_body_steps. (exists fs_lt_dst_transform_reverse_sourcevaluefoldnegative_body_steps_bound. fs_lt_dst_transform_reverse_sourcevaluefoldnegative_body_steps_bound + S fs_i_dst_transform_reverse_sourcevaluefoldnegative_body_steps = S (dc_input_transform_reverse_source)) -> exists fs_a_dst_transform_reverse_sourcevaluefoldnegative_body_steps fs_r_dst_transform_reverse_sourcevaluefoldnegative_body_steps fs_s_dst_transform_reverse_sourcevaluefoldnegative_body_steps. ((((exists fs_h_dst_transform_reverse_sourcevaluefoldnegative_body_steps_summand. fs_h_dst_transform_reverse_sourcevaluefoldnegative_body_steps_summand + S (fs_a_dst_transform_reverse_sourcevaluefoldnegative_body_steps) = S ((S (fs_i_dst_transform_reverse_sourcevaluefoldnegative_body_steps)) * dst_negative_scale_transform_reverse_sourcevaluefold)) /\ exists fs_q_dst_transform_reverse_sourcevaluefoldnegative_body_steps_summand. dst_negative_code_transform_reverse_sourcevaluefold = fs_q_dst_transform_reverse_sourcevaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_transform_reverse_sourcevaluefoldnegative_body_steps)) * dst_negative_scale_transform_reverse_sourcevaluefold) + (fs_a_dst_transform_reverse_sourcevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_transform_reverse_sourcevaluefoldnegative_body_steps_partial. fs_h_dst_transform_reverse_sourcevaluefoldnegative_body_steps_partial + S (fs_r_dst_transform_reverse_sourcevaluefoldnegative_body_steps) = S ((S (fs_i_dst_transform_reverse_sourcevaluefoldnegative_body_steps)) * fs_v_dst_transform_reverse_sourcevaluefoldnegative)) /\ exists fs_q_dst_transform_reverse_sourcevaluefoldnegative_body_steps_partial. fs_u_dst_transform_reverse_sourcevaluefoldnegative = fs_q_dst_transform_reverse_sourcevaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_transform_reverse_sourcevaluefoldnegative_body_steps)) * fs_v_dst_transform_reverse_sourcevaluefoldnegative) + (fs_r_dst_transform_reverse_sourcevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_transform_reverse_sourcevaluefoldnegative_body_steps_successor. fs_h_dst_transform_reverse_sourcevaluefoldnegative_body_steps_successor + S (fs_s_dst_transform_reverse_sourcevaluefoldnegative_body_steps) = S ((S (S fs_i_dst_transform_reverse_sourcevaluefoldnegative_body_steps)) * fs_v_dst_transform_reverse_sourcevaluefoldnegative)) /\ exists fs_q_dst_transform_reverse_sourcevaluefoldnegative_body_steps_successor. fs_u_dst_transform_reverse_sourcevaluefoldnegative = fs_q_dst_transform_reverse_sourcevaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_transform_reverse_sourcevaluefoldnegative_body_steps)) * fs_v_dst_transform_reverse_sourcevaluefoldnegative) + (fs_s_dst_transform_reverse_sourcevaluefoldnegative_body_steps))) /\ fs_s_dst_transform_reverse_sourcevaluefoldnegative_body_steps = fs_r_dst_transform_reverse_sourcevaluefoldnegative_body_steps + fs_a_dst_transform_reverse_sourcevaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_transform_reverse_sourcevaluefoldresult ge_balance_negative_transform_reverse_sourcevaluefoldresult. (((((dc_output_transform_reverse_source) = 2 * (ge_balance_positive_transform_reverse_sourcevaluefoldresult) /\ (ge_balance_negative_transform_reverse_sourcevaluefoldresult) = 0) \/ exists ge_signed_half_transform_reverse_sourcevaluefoldresultdecode. (((dc_output_transform_reverse_source) = 2 * ge_signed_half_transform_reverse_sourcevaluefoldresultdecode + 1 /\ (ge_balance_positive_transform_reverse_sourcevaluefoldresult) = 0) /\ (ge_balance_negative_transform_reverse_sourcevaluefoldresult) = S ge_signed_half_transform_reverse_sourcevaluefoldresultdecode))) /\ ((dst_positive_sum_transform_reverse_sourcevaluefold) + ge_balance_negative_transform_reverse_sourcevaluefoldresult = (dst_negative_sum_transform_reverse_sourcevaluefold) + ge_balance_positive_transform_reverse_sourcevaluefoldresult)))))))))))))))))))) -> (forall mi_index_transform_reverse_result mi_value_transform_reverse_result. ~(mi_index_transform_reverse_result=0) -> (exists pvs_le_gap_transform_reverse_resultbound. pvs_le_gap_transform_reverse_resultbound + (mi_index_transform_reverse_result) = (N)) -> (exists dst_positive_code_transform_reverse_resultentry dst_positive_scale_transform_reverse_resultentry dst_negative_code_transform_reverse_resultentry dst_negative_scale_transform_reverse_resultentry dst_positive_transform_reverse_resultentry dst_negative_transform_reverse_resultentry. (((G) = (((((dst_positive_code_transform_reverse_resultentry) + (dst_positive_scale_transform_reverse_resultentry)) * S ((dst_positive_code_transform_reverse_resultentry) + (dst_positive_scale_transform_reverse_resultentry)) + ((dst_positive_scale_transform_reverse_resultentry) + (dst_positive_scale_transform_reverse_resultentry))) + (((dst_negative_code_transform_reverse_resultentry) + (dst_negative_scale_transform_reverse_resultentry)) * S ((dst_negative_code_transform_reverse_resultentry) + (dst_negative_scale_transform_reverse_resultentry)) + ((dst_negative_scale_transform_reverse_resultentry) + (dst_negative_scale_transform_reverse_resultentry)))) * S ((((dst_positive_code_transform_reverse_resultentry) + (dst_positive_scale_transform_reverse_resultentry)) * S ((dst_positive_code_transform_reverse_resultentry) + (dst_positive_scale_transform_reverse_resultentry)) + ((dst_positive_scale_transform_reverse_resultentry) + (dst_positive_scale_transform_reverse_resultentry))) + (((dst_negative_code_transform_reverse_resultentry) + (dst_negative_scale_transform_reverse_resultentry)) * S ((dst_negative_code_transform_reverse_resultentry) + (dst_negative_scale_transform_reverse_resultentry)) + ((dst_negative_scale_transform_reverse_resultentry) + (dst_negative_scale_transform_reverse_resultentry)))) + ((((dst_negative_code_transform_reverse_resultentry) + (dst_negative_scale_transform_reverse_resultentry)) * S ((dst_negative_code_transform_reverse_resultentry) + (dst_negative_scale_transform_reverse_resultentry)) + ((dst_negative_scale_transform_reverse_resultentry) + (dst_negative_scale_transform_reverse_resultentry))) + (((dst_negative_code_transform_reverse_resultentry) + (dst_negative_scale_transform_reverse_resultentry)) * S ((dst_negative_code_transform_reverse_resultentry) + (dst_negative_scale_transform_reverse_resultentry)) + ((dst_negative_scale_transform_reverse_resultentry) + (dst_negative_scale_transform_reverse_resultentry)))))) /\ (((((exists ff_h_pvs_transform_reverse_resultentrypositive. ff_h_pvs_transform_reverse_resultentrypositive + S (dst_positive_transform_reverse_resultentry) = S ((S (mi_index_transform_reverse_result)) * dst_positive_scale_transform_reverse_resultentry)) /\ exists ff_q_pvs_transform_reverse_resultentrypositive. dst_positive_code_transform_reverse_resultentry = ff_q_pvs_transform_reverse_resultentrypositive * S ((S (mi_index_transform_reverse_result)) * dst_positive_scale_transform_reverse_resultentry) + (dst_positive_transform_reverse_resultentry))) /\ (((((exists ff_h_pvs_transform_reverse_resultentrynegative. ff_h_pvs_transform_reverse_resultentrynegative + S (dst_negative_transform_reverse_resultentry) = S ((S (mi_index_transform_reverse_result)) * dst_negative_scale_transform_reverse_resultentry)) /\ exists ff_q_pvs_transform_reverse_resultentrynegative. dst_negative_code_transform_reverse_resultentry = ff_q_pvs_transform_reverse_resultentrynegative * S ((S (mi_index_transform_reverse_result)) * dst_negative_scale_transform_reverse_resultentry) + (dst_negative_transform_reverse_resultentry))) /\ (exists ge_balance_positive_transform_reverse_resultentryvalue ge_balance_negative_transform_reverse_resultentryvalue. (((((mi_value_transform_reverse_result) = 2 * (ge_balance_positive_transform_reverse_resultentryvalue) /\ (ge_balance_negative_transform_reverse_resultentryvalue) = 0) \/ exists ge_signed_half_transform_reverse_resultentryvaluedecode. (((mi_value_transform_reverse_result) = 2 * ge_signed_half_transform_reverse_resultentryvaluedecode + 1 /\ (ge_balance_positive_transform_reverse_resultentryvalue) = 0) /\ (ge_balance_negative_transform_reverse_resultentryvalue) = S ge_signed_half_transform_reverse_resultentryvaluedecode))) /\ ((dst_positive_transform_reverse_resultentry) + ge_balance_negative_transform_reverse_resultentryvalue = (dst_negative_transform_reverse_resultentry) + ge_balance_positive_transform_reverse_resultentryvalue))))))))) -> (((~((mi_index_transform_reverse_result)=0)) /\ (exists dm_mask_table_transform_reverse_resultsum. ((((exists dst_positive_code_transform_reverse_resultsummasktable dst_positive_scale_transform_reverse_resultsummasktable dst_negative_code_transform_reverse_resultsummasktable dst_negative_scale_transform_reverse_resultsummasktable. (((dm_mask_table_transform_reverse_resultsum) = (((((dst_positive_code_transform_reverse_resultsummasktable) + (dst_positive_scale_transform_reverse_resultsummasktable)) * S ((dst_positive_code_transform_reverse_resultsummasktable) + (dst_positive_scale_transform_reverse_resultsummasktable)) + ((dst_positive_scale_transform_reverse_resultsummasktable) + (dst_positive_scale_transform_reverse_resultsummasktable))) + (((dst_negative_code_transform_reverse_resultsummasktable) + (dst_negative_scale_transform_reverse_resultsummasktable)) * S ((dst_negative_code_transform_reverse_resultsummasktable) + (dst_negative_scale_transform_reverse_resultsummasktable)) + ((dst_negative_scale_transform_reverse_resultsummasktable) + (dst_negative_scale_transform_reverse_resultsummasktable)))) * S ((((dst_positive_code_transform_reverse_resultsummasktable) + (dst_positive_scale_transform_reverse_resultsummasktable)) * S ((dst_positive_code_transform_reverse_resultsummasktable) + (dst_positive_scale_transform_reverse_resultsummasktable)) + ((dst_positive_scale_transform_reverse_resultsummasktable) + (dst_positive_scale_transform_reverse_resultsummasktable))) + (((dst_negative_code_transform_reverse_resultsummasktable) + (dst_negative_scale_transform_reverse_resultsummasktable)) * S ((dst_negative_code_transform_reverse_resultsummasktable) + (dst_negative_scale_transform_reverse_resultsummasktable)) + ((dst_negative_scale_transform_reverse_resultsummasktable) + (dst_negative_scale_transform_reverse_resultsummasktable)))) + ((((dst_negative_code_transform_reverse_resultsummasktable) + (dst_negative_scale_transform_reverse_resultsummasktable)) * S ((dst_negative_code_transform_reverse_resultsummasktable) + (dst_negative_scale_transform_reverse_resultsummasktable)) + ((dst_negative_scale_transform_reverse_resultsummasktable) + (dst_negative_scale_transform_reverse_resultsummasktable))) + (((dst_negative_code_transform_reverse_resultsummasktable) + (dst_negative_scale_transform_reverse_resultsummasktable)) * S ((dst_negative_code_transform_reverse_resultsummasktable) + (dst_negative_scale_transform_reverse_resultsummasktable)) + ((dst_negative_scale_transform_reverse_resultsummasktable) + (dst_negative_scale_transform_reverse_resultsummasktable)))))) /\ (forall dst_index_transform_reverse_resultsummasktable. (exists pvs_le_gap_transform_reverse_resultsummasktabledomain. pvs_le_gap_transform_reverse_resultsummasktabledomain + (dst_index_transform_reverse_resultsummasktable) = (mi_index_transform_reverse_result)) -> exists dst_positive_transform_reverse_resultsummasktable dst_negative_transform_reverse_resultsummasktable dst_value_transform_reverse_resultsummasktable. ((((exists ff_h_pvs_transform_reverse_resultsummasktableentrypositive. ff_h_pvs_transform_reverse_resultsummasktableentrypositive + S (dst_positive_transform_reverse_resultsummasktable) = S ((S (dst_index_transform_reverse_resultsummasktable)) * dst_positive_scale_transform_reverse_resultsummasktable)) /\ exists ff_q_pvs_transform_reverse_resultsummasktableentrypositive. dst_positive_code_transform_reverse_resultsummasktable = ff_q_pvs_transform_reverse_resultsummasktableentrypositive * S ((S (dst_index_transform_reverse_resultsummasktable)) * dst_positive_scale_transform_reverse_resultsummasktable) + (dst_positive_transform_reverse_resultsummasktable))) /\ (((((exists ff_h_pvs_transform_reverse_resultsummasktableentrynegative. ff_h_pvs_transform_reverse_resultsummasktableentrynegative + S (dst_negative_transform_reverse_resultsummasktable) = S ((S (dst_index_transform_reverse_resultsummasktable)) * dst_negative_scale_transform_reverse_resultsummasktable)) /\ exists ff_q_pvs_transform_reverse_resultsummasktableentrynegative. dst_negative_code_transform_reverse_resultsummasktable = ff_q_pvs_transform_reverse_resultsummasktableentrynegative * S ((S (dst_index_transform_reverse_resultsummasktable)) * dst_negative_scale_transform_reverse_resultsummasktable) + (dst_negative_transform_reverse_resultsummasktable))) /\ (exists ge_balance_positive_transform_reverse_resultsummasktableentryvalue ge_balance_negative_transform_reverse_resultsummasktableentryvalue. (((((dst_value_transform_reverse_resultsummasktable) = 2 * (ge_balance_positive_transform_reverse_resultsummasktableentryvalue) /\ (ge_balance_negative_transform_reverse_resultsummasktableentryvalue) = 0) \/ exists ge_signed_half_transform_reverse_resultsummasktableentryvaluedecode. (((dst_value_transform_reverse_resultsummasktable) = 2 * ge_signed_half_transform_reverse_resultsummasktableentryvaluedecode + 1 /\ (ge_balance_positive_transform_reverse_resultsummasktableentryvalue) = 0) /\ (ge_balance_negative_transform_reverse_resultsummasktableentryvalue) = S ge_signed_half_transform_reverse_resultsummasktableentryvaluedecode))) /\ ((dst_positive_transform_reverse_resultsummasktable) + ge_balance_negative_transform_reverse_resultsummasktableentryvalue = (dst_negative_transform_reverse_resultsummasktable) + ge_balance_positive_transform_reverse_resultsummasktableentryvalue))))))))) /\ (forall dm_index_transform_reverse_resultsummask dm_value_transform_reverse_resultsummask. (exists pvs_le_gap_transform_reverse_resultsummaskdomain. pvs_le_gap_transform_reverse_resultsummaskdomain + (dm_index_transform_reverse_resultsummask) = (mi_index_transform_reverse_result)) -> (exists dst_positive_code_transform_reverse_resultsummasklookup dst_positive_scale_transform_reverse_resultsummasklookup dst_negative_code_transform_reverse_resultsummasklookup dst_negative_scale_transform_reverse_resultsummasklookup dst_positive_transform_reverse_resultsummasklookup dst_negative_transform_reverse_resultsummasklookup. (((dm_mask_table_transform_reverse_resultsum) = (((((dst_positive_code_transform_reverse_resultsummasklookup) + (dst_positive_scale_transform_reverse_resultsummasklookup)) * S ((dst_positive_code_transform_reverse_resultsummasklookup) + (dst_positive_scale_transform_reverse_resultsummasklookup)) + ((dst_positive_scale_transform_reverse_resultsummasklookup) + (dst_positive_scale_transform_reverse_resultsummasklookup))) + (((dst_negative_code_transform_reverse_resultsummasklookup) + (dst_negative_scale_transform_reverse_resultsummasklookup)) * S ((dst_negative_code_transform_reverse_resultsummasklookup) + (dst_negative_scale_transform_reverse_resultsummasklookup)) + ((dst_negative_scale_transform_reverse_resultsummasklookup) + (dst_negative_scale_transform_reverse_resultsummasklookup)))) * S ((((dst_positive_code_transform_reverse_resultsummasklookup) + (dst_positive_scale_transform_reverse_resultsummasklookup)) * S ((dst_positive_code_transform_reverse_resultsummasklookup) + (dst_positive_scale_transform_reverse_resultsummasklookup)) + ((dst_positive_scale_transform_reverse_resultsummasklookup) + (dst_positive_scale_transform_reverse_resultsummasklookup))) + (((dst_negative_code_transform_reverse_resultsummasklookup) + (dst_negative_scale_transform_reverse_resultsummasklookup)) * S ((dst_negative_code_transform_reverse_resultsummasklookup) + (dst_negative_scale_transform_reverse_resultsummasklookup)) + ((dst_negative_scale_transform_reverse_resultsummasklookup) + (dst_negative_scale_transform_reverse_resultsummasklookup)))) + ((((dst_negative_code_transform_reverse_resultsummasklookup) + (dst_negative_scale_transform_reverse_resultsummasklookup)) * S ((dst_negative_code_transform_reverse_resultsummasklookup) + (dst_negative_scale_transform_reverse_resultsummasklookup)) + ((dst_negative_scale_transform_reverse_resultsummasklookup) + (dst_negative_scale_transform_reverse_resultsummasklookup))) + (((dst_negative_code_transform_reverse_resultsummasklookup) + (dst_negative_scale_transform_reverse_resultsummasklookup)) * S ((dst_negative_code_transform_reverse_resultsummasklookup) + (dst_negative_scale_transform_reverse_resultsummasklookup)) + ((dst_negative_scale_transform_reverse_resultsummasklookup) + (dst_negative_scale_transform_reverse_resultsummasklookup)))))) /\ (((((exists ff_h_pvs_transform_reverse_resultsummasklookuppositive. ff_h_pvs_transform_reverse_resultsummasklookuppositive + S (dst_positive_transform_reverse_resultsummasklookup) = S ((S (dm_index_transform_reverse_resultsummask)) * dst_positive_scale_transform_reverse_resultsummasklookup)) /\ exists ff_q_pvs_transform_reverse_resultsummasklookuppositive. dst_positive_code_transform_reverse_resultsummasklookup = ff_q_pvs_transform_reverse_resultsummasklookuppositive * S ((S (dm_index_transform_reverse_resultsummask)) * dst_positive_scale_transform_reverse_resultsummasklookup) + (dst_positive_transform_reverse_resultsummasklookup))) /\ (((((exists ff_h_pvs_transform_reverse_resultsummasklookupnegative. ff_h_pvs_transform_reverse_resultsummasklookupnegative + S (dst_negative_transform_reverse_resultsummasklookup) = S ((S (dm_index_transform_reverse_resultsummask)) * dst_negative_scale_transform_reverse_resultsummasklookup)) /\ exists ff_q_pvs_transform_reverse_resultsummasklookupnegative. dst_negative_code_transform_reverse_resultsummasklookup = ff_q_pvs_transform_reverse_resultsummasklookupnegative * S ((S (dm_index_transform_reverse_resultsummask)) * dst_negative_scale_transform_reverse_resultsummasklookup) + (dst_negative_transform_reverse_resultsummasklookup))) /\ (exists ge_balance_positive_transform_reverse_resultsummasklookupvalue ge_balance_negative_transform_reverse_resultsummasklookupvalue. (((((dm_value_transform_reverse_resultsummask) = 2 * (ge_balance_positive_transform_reverse_resultsummasklookupvalue) /\ (ge_balance_negative_transform_reverse_resultsummasklookupvalue) = 0) \/ exists ge_signed_half_transform_reverse_resultsummasklookupvaluedecode. (((dm_value_transform_reverse_resultsummask) = 2 * ge_signed_half_transform_reverse_resultsummasklookupvaluedecode + 1 /\ (ge_balance_positive_transform_reverse_resultsummasklookupvalue) = 0) /\ (ge_balance_negative_transform_reverse_resultsummasklookupvalue) = S ge_signed_half_transform_reverse_resultsummasklookupvaluedecode))) /\ ((dst_positive_transform_reverse_resultsummasklookup) + ge_balance_negative_transform_reverse_resultsummasklookupvalue = (dst_negative_transform_reverse_resultsummasklookup) + ge_balance_positive_transform_reverse_resultsummasklookupvalue))))))))) -> ((((~((dm_index_transform_reverse_resultsummask)=0)) /\ (exists dm_quotient_transform_reverse_resultsummaskentry. (((mi_index_transform_reverse_result)=(dm_index_transform_reverse_resultsummask)*dm_quotient_transform_reverse_resultsummaskentry) /\ (exists dst_positive_code_transform_reverse_resultsummaskentryinput dst_positive_scale_transform_reverse_resultsummaskentryinput dst_negative_code_transform_reverse_resultsummaskentryinput dst_negative_scale_transform_reverse_resultsummaskentryinput dst_positive_transform_reverse_resultsummaskentryinput dst_negative_transform_reverse_resultsummaskentryinput. (((F) = (((((dst_positive_code_transform_reverse_resultsummaskentryinput) + (dst_positive_scale_transform_reverse_resultsummaskentryinput)) * S ((dst_positive_code_transform_reverse_resultsummaskentryinput) + (dst_positive_scale_transform_reverse_resultsummaskentryinput)) + ((dst_positive_scale_transform_reverse_resultsummaskentryinput) + (dst_positive_scale_transform_reverse_resultsummaskentryinput))) + (((dst_negative_code_transform_reverse_resultsummaskentryinput) + (dst_negative_scale_transform_reverse_resultsummaskentryinput)) * S ((dst_negative_code_transform_reverse_resultsummaskentryinput) + (dst_negative_scale_transform_reverse_resultsummaskentryinput)) + ((dst_negative_scale_transform_reverse_resultsummaskentryinput) + (dst_negative_scale_transform_reverse_resultsummaskentryinput)))) * S ((((dst_positive_code_transform_reverse_resultsummaskentryinput) + (dst_positive_scale_transform_reverse_resultsummaskentryinput)) * S ((dst_positive_code_transform_reverse_resultsummaskentryinput) + (dst_positive_scale_transform_reverse_resultsummaskentryinput)) + ((dst_positive_scale_transform_reverse_resultsummaskentryinput) + (dst_positive_scale_transform_reverse_resultsummaskentryinput))) + (((dst_negative_code_transform_reverse_resultsummaskentryinput) + (dst_negative_scale_transform_reverse_resultsummaskentryinput)) * S ((dst_negative_code_transform_reverse_resultsummaskentryinput) + (dst_negative_scale_transform_reverse_resultsummaskentryinput)) + ((dst_negative_scale_transform_reverse_resultsummaskentryinput) + (dst_negative_scale_transform_reverse_resultsummaskentryinput)))) + ((((dst_negative_code_transform_reverse_resultsummaskentryinput) + (dst_negative_scale_transform_reverse_resultsummaskentryinput)) * S ((dst_negative_code_transform_reverse_resultsummaskentryinput) + (dst_negative_scale_transform_reverse_resultsummaskentryinput)) + ((dst_negative_scale_transform_reverse_resultsummaskentryinput) + (dst_negative_scale_transform_reverse_resultsummaskentryinput))) + (((dst_negative_code_transform_reverse_resultsummaskentryinput) + (dst_negative_scale_transform_reverse_resultsummaskentryinput)) * S ((dst_negative_code_transform_reverse_resultsummaskentryinput) + (dst_negative_scale_transform_reverse_resultsummaskentryinput)) + ((dst_negative_scale_transform_reverse_resultsummaskentryinput) + (dst_negative_scale_transform_reverse_resultsummaskentryinput)))))) /\ (((((exists ff_h_pvs_transform_reverse_resultsummaskentryinputpositive. ff_h_pvs_transform_reverse_resultsummaskentryinputpositive + S (dst_positive_transform_reverse_resultsummaskentryinput) = S ((S (dm_index_transform_reverse_resultsummask)) * dst_positive_scale_transform_reverse_resultsummaskentryinput)) /\ exists ff_q_pvs_transform_reverse_resultsummaskentryinputpositive. dst_positive_code_transform_reverse_resultsummaskentryinput = ff_q_pvs_transform_reverse_resultsummaskentryinputpositive * S ((S (dm_index_transform_reverse_resultsummask)) * dst_positive_scale_transform_reverse_resultsummaskentryinput) + (dst_positive_transform_reverse_resultsummaskentryinput))) /\ (((((exists ff_h_pvs_transform_reverse_resultsummaskentryinputnegative. ff_h_pvs_transform_reverse_resultsummaskentryinputnegative + S (dst_negative_transform_reverse_resultsummaskentryinput) = S ((S (dm_index_transform_reverse_resultsummask)) * dst_negative_scale_transform_reverse_resultsummaskentryinput)) /\ exists ff_q_pvs_transform_reverse_resultsummaskentryinputnegative. dst_negative_code_transform_reverse_resultsummaskentryinput = ff_q_pvs_transform_reverse_resultsummaskentryinputnegative * S ((S (dm_index_transform_reverse_resultsummask)) * dst_negative_scale_transform_reverse_resultsummaskentryinput) + (dst_negative_transform_reverse_resultsummaskentryinput))) /\ (exists ge_balance_positive_transform_reverse_resultsummaskentryinputvalue ge_balance_negative_transform_reverse_resultsummaskentryinputvalue. (((((dm_value_transform_reverse_resultsummask) = 2 * (ge_balance_positive_transform_reverse_resultsummaskentryinputvalue) /\ (ge_balance_negative_transform_reverse_resultsummaskentryinputvalue) = 0) \/ exists ge_signed_half_transform_reverse_resultsummaskentryinputvaluedecode. (((dm_value_transform_reverse_resultsummask) = 2 * ge_signed_half_transform_reverse_resultsummaskentryinputvaluedecode + 1 /\ (ge_balance_positive_transform_reverse_resultsummaskentryinputvalue) = 0) /\ (ge_balance_negative_transform_reverse_resultsummaskentryinputvalue) = S ge_signed_half_transform_reverse_resultsummaskentryinputvaluedecode))) /\ ((dst_positive_transform_reverse_resultsummaskentryinput) + ge_balance_negative_transform_reverse_resultsummaskentryinputvalue = (dst_negative_transform_reverse_resultsummaskentryinput) + ge_balance_positive_transform_reverse_resultsummaskentryinputvalue))))))))))))) \/ ((((dm_index_transform_reverse_resultsummask)=0 \/ ~(exists pvs_factor_transform_reverse_resultsummaskentrynondivisor. (mi_index_transform_reverse_result) = (dm_index_transform_reverse_resultsummask) * pvs_factor_transform_reverse_resultsummaskentrynondivisor)) /\ ((dm_value_transform_reverse_resultsummask)=0))))))) /\ (exists dst_positive_code_transform_reverse_resultsumfold dst_positive_scale_transform_reverse_resultsumfold dst_negative_code_transform_reverse_resultsumfold dst_negative_scale_transform_reverse_resultsumfold dst_positive_sum_transform_reverse_resultsumfold dst_negative_sum_transform_reverse_resultsumfold. (((dm_mask_table_transform_reverse_resultsum) = (((((dst_positive_code_transform_reverse_resultsumfold) + (dst_positive_scale_transform_reverse_resultsumfold)) * S ((dst_positive_code_transform_reverse_resultsumfold) + (dst_positive_scale_transform_reverse_resultsumfold)) + ((dst_positive_scale_transform_reverse_resultsumfold) + (dst_positive_scale_transform_reverse_resultsumfold))) + (((dst_negative_code_transform_reverse_resultsumfold) + (dst_negative_scale_transform_reverse_resultsumfold)) * S ((dst_negative_code_transform_reverse_resultsumfold) + (dst_negative_scale_transform_reverse_resultsumfold)) + ((dst_negative_scale_transform_reverse_resultsumfold) + (dst_negative_scale_transform_reverse_resultsumfold)))) * S ((((dst_positive_code_transform_reverse_resultsumfold) + (dst_positive_scale_transform_reverse_resultsumfold)) * S ((dst_positive_code_transform_reverse_resultsumfold) + (dst_positive_scale_transform_reverse_resultsumfold)) + ((dst_positive_scale_transform_reverse_resultsumfold) + (dst_positive_scale_transform_reverse_resultsumfold))) + (((dst_negative_code_transform_reverse_resultsumfold) + (dst_negative_scale_transform_reverse_resultsumfold)) * S ((dst_negative_code_transform_reverse_resultsumfold) + (dst_negative_scale_transform_reverse_resultsumfold)) + ((dst_negative_scale_transform_reverse_resultsumfold) + (dst_negative_scale_transform_reverse_resultsumfold)))) + ((((dst_negative_code_transform_reverse_resultsumfold) + (dst_negative_scale_transform_reverse_resultsumfold)) * S ((dst_negative_code_transform_reverse_resultsumfold) + (dst_negative_scale_transform_reverse_resultsumfold)) + ((dst_negative_scale_transform_reverse_resultsumfold) + (dst_negative_scale_transform_reverse_resultsumfold))) + (((dst_negative_code_transform_reverse_resultsumfold) + (dst_negative_scale_transform_reverse_resultsumfold)) * S ((dst_negative_code_transform_reverse_resultsumfold) + (dst_negative_scale_transform_reverse_resultsumfold)) + ((dst_negative_scale_transform_reverse_resultsumfold) + (dst_negative_scale_transform_reverse_resultsumfold)))))) /\ (((exists fs_u_dst_transform_reverse_resultsumfoldpositive fs_v_dst_transform_reverse_resultsumfoldpositive. ((((exists fs_h_dst_transform_reverse_resultsumfoldpositive_body_start. fs_h_dst_transform_reverse_resultsumfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_transform_reverse_resultsumfoldpositive)) /\ exists fs_q_dst_transform_reverse_resultsumfoldpositive_body_start. fs_u_dst_transform_reverse_resultsumfoldpositive = fs_q_dst_transform_reverse_resultsumfoldpositive_body_start * S ((S (0)) * fs_v_dst_transform_reverse_resultsumfoldpositive) + (0))) /\ ((((exists fs_h_dst_transform_reverse_resultsumfoldpositive_body_terminal. fs_h_dst_transform_reverse_resultsumfoldpositive_body_terminal + S (dst_positive_sum_transform_reverse_resultsumfold) = S ((S (S (mi_index_transform_reverse_result))) * fs_v_dst_transform_reverse_resultsumfoldpositive)) /\ exists fs_q_dst_transform_reverse_resultsumfoldpositive_body_terminal. fs_u_dst_transform_reverse_resultsumfoldpositive = fs_q_dst_transform_reverse_resultsumfoldpositive_body_terminal * S ((S (S (mi_index_transform_reverse_result))) * fs_v_dst_transform_reverse_resultsumfoldpositive) + (dst_positive_sum_transform_reverse_resultsumfold))) /\ forall fs_i_dst_transform_reverse_resultsumfoldpositive_body_steps. (exists fs_lt_dst_transform_reverse_resultsumfoldpositive_body_steps_bound. fs_lt_dst_transform_reverse_resultsumfoldpositive_body_steps_bound + S fs_i_dst_transform_reverse_resultsumfoldpositive_body_steps = S (mi_index_transform_reverse_result)) -> exists fs_a_dst_transform_reverse_resultsumfoldpositive_body_steps fs_r_dst_transform_reverse_resultsumfoldpositive_body_steps fs_s_dst_transform_reverse_resultsumfoldpositive_body_steps. ((((exists fs_h_dst_transform_reverse_resultsumfoldpositive_body_steps_summand. fs_h_dst_transform_reverse_resultsumfoldpositive_body_steps_summand + S (fs_a_dst_transform_reverse_resultsumfoldpositive_body_steps) = S ((S (fs_i_dst_transform_reverse_resultsumfoldpositive_body_steps)) * dst_positive_scale_transform_reverse_resultsumfold)) /\ exists fs_q_dst_transform_reverse_resultsumfoldpositive_body_steps_summand. dst_positive_code_transform_reverse_resultsumfold = fs_q_dst_transform_reverse_resultsumfoldpositive_body_steps_summand * S ((S (fs_i_dst_transform_reverse_resultsumfoldpositive_body_steps)) * dst_positive_scale_transform_reverse_resultsumfold) + (fs_a_dst_transform_reverse_resultsumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_transform_reverse_resultsumfoldpositive_body_steps_partial. fs_h_dst_transform_reverse_resultsumfoldpositive_body_steps_partial + S (fs_r_dst_transform_reverse_resultsumfoldpositive_body_steps) = S ((S (fs_i_dst_transform_reverse_resultsumfoldpositive_body_steps)) * fs_v_dst_transform_reverse_resultsumfoldpositive)) /\ exists fs_q_dst_transform_reverse_resultsumfoldpositive_body_steps_partial. fs_u_dst_transform_reverse_resultsumfoldpositive = fs_q_dst_transform_reverse_resultsumfoldpositive_body_steps_partial * S ((S (fs_i_dst_transform_reverse_resultsumfoldpositive_body_steps)) * fs_v_dst_transform_reverse_resultsumfoldpositive) + (fs_r_dst_transform_reverse_resultsumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_transform_reverse_resultsumfoldpositive_body_steps_successor. fs_h_dst_transform_reverse_resultsumfoldpositive_body_steps_successor + S (fs_s_dst_transform_reverse_resultsumfoldpositive_body_steps) = S ((S (S fs_i_dst_transform_reverse_resultsumfoldpositive_body_steps)) * fs_v_dst_transform_reverse_resultsumfoldpositive)) /\ exists fs_q_dst_transform_reverse_resultsumfoldpositive_body_steps_successor. fs_u_dst_transform_reverse_resultsumfoldpositive = fs_q_dst_transform_reverse_resultsumfoldpositive_body_steps_successor * S ((S (S fs_i_dst_transform_reverse_resultsumfoldpositive_body_steps)) * fs_v_dst_transform_reverse_resultsumfoldpositive) + (fs_s_dst_transform_reverse_resultsumfoldpositive_body_steps))) /\ fs_s_dst_transform_reverse_resultsumfoldpositive_body_steps = fs_r_dst_transform_reverse_resultsumfoldpositive_body_steps + fs_a_dst_transform_reverse_resultsumfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_transform_reverse_resultsumfoldnegative fs_v_dst_transform_reverse_resultsumfoldnegative. ((((exists fs_h_dst_transform_reverse_resultsumfoldnegative_body_start. fs_h_dst_transform_reverse_resultsumfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_transform_reverse_resultsumfoldnegative)) /\ exists fs_q_dst_transform_reverse_resultsumfoldnegative_body_start. fs_u_dst_transform_reverse_resultsumfoldnegative = fs_q_dst_transform_reverse_resultsumfoldnegative_body_start * S ((S (0)) * fs_v_dst_transform_reverse_resultsumfoldnegative) + (0))) /\ ((((exists fs_h_dst_transform_reverse_resultsumfoldnegative_body_terminal. fs_h_dst_transform_reverse_resultsumfoldnegative_body_terminal + S (dst_negative_sum_transform_reverse_resultsumfold) = S ((S (S (mi_index_transform_reverse_result))) * fs_v_dst_transform_reverse_resultsumfoldnegative)) /\ exists fs_q_dst_transform_reverse_resultsumfoldnegative_body_terminal. fs_u_dst_transform_reverse_resultsumfoldnegative = fs_q_dst_transform_reverse_resultsumfoldnegative_body_terminal * S ((S (S (mi_index_transform_reverse_result))) * fs_v_dst_transform_reverse_resultsumfoldnegative) + (dst_negative_sum_transform_reverse_resultsumfold))) /\ forall fs_i_dst_transform_reverse_resultsumfoldnegative_body_steps. (exists fs_lt_dst_transform_reverse_resultsumfoldnegative_body_steps_bound. fs_lt_dst_transform_reverse_resultsumfoldnegative_body_steps_bound + S fs_i_dst_transform_reverse_resultsumfoldnegative_body_steps = S (mi_index_transform_reverse_result)) -> exists fs_a_dst_transform_reverse_resultsumfoldnegative_body_steps fs_r_dst_transform_reverse_resultsumfoldnegative_body_steps fs_s_dst_transform_reverse_resultsumfoldnegative_body_steps. ((((exists fs_h_dst_transform_reverse_resultsumfoldnegative_body_steps_summand. fs_h_dst_transform_reverse_resultsumfoldnegative_body_steps_summand + S (fs_a_dst_transform_reverse_resultsumfoldnegative_body_steps) = S ((S (fs_i_dst_transform_reverse_resultsumfoldnegative_body_steps)) * dst_negative_scale_transform_reverse_resultsumfold)) /\ exists fs_q_dst_transform_reverse_resultsumfoldnegative_body_steps_summand. dst_negative_code_transform_reverse_resultsumfold = fs_q_dst_transform_reverse_resultsumfoldnegative_body_steps_summand * S ((S (fs_i_dst_transform_reverse_resultsumfoldnegative_body_steps)) * dst_negative_scale_transform_reverse_resultsumfold) + (fs_a_dst_transform_reverse_resultsumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_transform_reverse_resultsumfoldnegative_body_steps_partial. fs_h_dst_transform_reverse_resultsumfoldnegative_body_steps_partial + S (fs_r_dst_transform_reverse_resultsumfoldnegative_body_steps) = S ((S (fs_i_dst_transform_reverse_resultsumfoldnegative_body_steps)) * fs_v_dst_transform_reverse_resultsumfoldnegative)) /\ exists fs_q_dst_transform_reverse_resultsumfoldnegative_body_steps_partial. fs_u_dst_transform_reverse_resultsumfoldnegative = fs_q_dst_transform_reverse_resultsumfoldnegative_body_steps_partial * S ((S (fs_i_dst_transform_reverse_resultsumfoldnegative_body_steps)) * fs_v_dst_transform_reverse_resultsumfoldnegative) + (fs_r_dst_transform_reverse_resultsumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_transform_reverse_resultsumfoldnegative_body_steps_successor. fs_h_dst_transform_reverse_resultsumfoldnegative_body_steps_successor + S (fs_s_dst_transform_reverse_resultsumfoldnegative_body_steps) = S ((S (S fs_i_dst_transform_reverse_resultsumfoldnegative_body_steps)) * fs_v_dst_transform_reverse_resultsumfoldnegative)) /\ exists fs_q_dst_transform_reverse_resultsumfoldnegative_body_steps_successor. fs_u_dst_transform_reverse_resultsumfoldnegative = fs_q_dst_transform_reverse_resultsumfoldnegative_body_steps_successor * S ((S (S fs_i_dst_transform_reverse_resultsumfoldnegative_body_steps)) * fs_v_dst_transform_reverse_resultsumfoldnegative) + (fs_s_dst_transform_reverse_resultsumfoldnegative_body_steps))) /\ fs_s_dst_transform_reverse_resultsumfoldnegative_body_steps = fs_r_dst_transform_reverse_resultsumfoldnegative_body_steps + fs_a_dst_transform_reverse_resultsumfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_transform_reverse_resultsumfoldresult ge_balance_negative_transform_reverse_resultsumfoldresult. (((((mi_value_transform_reverse_result) = 2 * (ge_balance_positive_transform_reverse_resultsumfoldresult) /\ (ge_balance_negative_transform_reverse_resultsumfoldresult) = 0) \/ exists ge_signed_half_transform_reverse_resultsumfoldresultdecode. (((mi_value_transform_reverse_result) = 2 * ge_signed_half_transform_reverse_resultsumfoldresultdecode + 1 /\ (ge_balance_positive_transform_reverse_resultsumfoldresult) = 0) /\ (ge_balance_negative_transform_reverse_resultsumfoldresult) = S ge_signed_half_transform_reverse_resultsumfoldresultdecode))) /\ ((dst_positive_sum_transform_reverse_resultsumfold) + ge_balance_negative_transform_reverse_resultsumfoldresult = (dst_negative_sum_transform_reverse_resultsumfold) + ge_balance_positive_transform_reverse_resultsumfoldresult))))))))))))))Complete tactic proof in conservative notation
All 33 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
33 script commands · 7 reading checkpoints · 1 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–6
02Separate the logical casesL7–9
03Fix variables and assumptionsL10–14
04Establish hiL15–24
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet constant one sum iff.
- L15
have hi : (DirichletSum(F,U,n,z) → DivisorSum(F,n,z)) ∧ (DivisorSum(F,n,z) → DirichletSum(F,U,n,z))Definitions: DirichletSum(F,U,n,z)DivisorSum(F,n,z)Original native command in the exact edition - L16
specialize dirichlet_constant_one_sum_iff (N) - L17
specialize dirichlet_constant_one_sum_iff (F) - L18
specialize dirichlet_constant_one_sum_iff (U) - L19
specialize dirichlet_constant_one_sum_iff (n) - L20
specialize dirichlet_constant_one_sum_iff (z) - L21
apply dirichlet_constant_one_sum_iff - L22
exact hc_left - L23
exact hU - L24
exact hn
05Use earlier factsL25–25
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L25
exact hbound
06Separate the logical casesL26–26
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L26
cases hi
Original defined command ledger · 33 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro U - 0005
intro hU - 0006
intro hc - 0007
cases hc - 0008
cases hc_right - 0009
cases hc_right_right - 0010
intro n - 0011
intro z - 0012
intro hn - 0013
intro hbound - 0014
intro hz - 0015
have hi : (DirichletSum(F,U,n,z) → DivisorSum(F,n,z)) ∧ (DivisorSum(F,n,z) → DirichletSum(F,U,n,z)) - 0016
specialize dirichlet_constant_one_sum_iff (N) - 0017
specialize dirichlet_constant_one_sum_iff (F) - 0018
specialize dirichlet_constant_one_sum_iff (U) - 0019
specialize dirichlet_constant_one_sum_iff (n) - 0020
specialize dirichlet_constant_one_sum_iff (z) - 0021
apply dirichlet_constant_one_sum_iff - 0022
exact hc_left - 0023
exact hU - 0024
exact hn - 0025
exact hbound - 0026
cases hi - 0027
apply hi_left - 0028
specialize hc_right_right_right (n) - 0029
specialize hc_right_right_right (z) - 0030
apply hc_right_right_right - 0031
exact hn - 0032
exact hbound - 0033
exact hz