Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Definition in prerequisite notation
MultiplicativePrefix(N,F) ∧ (MultiplicativePrefix(N,G) ∧ (¬m = 0 ∧ (¬n = 0 ∧ (Le(m · n,N) ∧ (Coprime(m,n) ∧ (DirichletPrefix(F,G,m,m,A) ∧ (DirichletPrefix(F,G,n,n,B) ∧ (SignedCartesianProduct(A,B,T,S m,S n) ∧ (DirichletPrefix(F,G,m · n,m · n,Q) ∧ DivisorPairIndexMap(S n,S m · S n,r,s))))))))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((((~(((N))=0)) /\ (((exists dst_positive_code_g009_definitionFtable dst_positive_scale_g009_definitionFtable dst_negative_code_g009_definitionFtable dst_negative_scale_g009_definitionFtable. ((((F)) = (((((dst_positive_code_g009_definitionFtable) + (dst_positive_scale_g009_definitionFtable)) * S ((dst_positive_code_g009_definitionFtable) + (dst_positive_scale_g009_definitionFtable)) + ((dst_positive_scale_g009_definitionFtable) + (dst_positive_scale_g009_definitionFtable))) + (((dst_negative_code_g009_definitionFtable) + (dst_negative_scale_g009_definitionFtable)) * S ((dst_negative_code_g009_definitionFtable) + (dst_negative_scale_g009_definitionFtable)) + ((dst_negative_scale_g009_definitionFtable) + (dst_negative_scale_g009_definitionFtable)))) * S ((((dst_positive_code_g009_definitionFtable) + (dst_positive_scale_g009_definitionFtable)) * S ((dst_positive_code_g009_definitionFtable) + (dst_positive_scale_g009_definitionFtable)) + ((dst_positive_scale_g009_definitionFtable) + (dst_positive_scale_g009_definitionFtable))) + (((dst_negative_code_g009_definitionFtable) + (dst_negative_scale_g009_definitionFtable)) * S ((dst_negative_code_g009_definitionFtable) + (dst_negative_scale_g009_definitionFtable)) + ((dst_negative_scale_g009_definitionFtable) + (dst_negative_scale_g009_definitionFtable)))) + ((((dst_negative_code_g009_definitionFtable) + (dst_negative_scale_g009_definitionFtable)) * S ((dst_negative_code_g009_definitionFtable) + (dst_negative_scale_g009_definitionFtable)) + ((dst_negative_scale_g009_definitionFtable) + (dst_negative_scale_g009_definitionFtable))) + (((dst_negative_code_g009_definitionFtable) + (dst_negative_scale_g009_definitionFtable)) * S ((dst_negative_code_g009_definitionFtable) + (dst_negative_scale_g009_definitionFtable)) + ((dst_negative_scale_g009_definitionFtable) + (dst_negative_scale_g009_definitionFtable)))))) /\ (forall dst_index_g009_definitionFtable. (exists pvs_le_gap_g009_definitionFtabledomain. pvs_le_gap_g009_definitionFtabledomain + (dst_index_g009_definitionFtable) = ((N))) -> exists dst_positive_g009_definitionFtable dst_negative_g009_definitionFtable dst_value_g009_definitionFtable. ((((exists ff_h_pvs_g009_definitionFtableentrypositive. ff_h_pvs_g009_definitionFtableentrypositive + S (dst_positive_g009_definitionFtable) = S ((S (dst_index_g009_definitionFtable)) * dst_positive_scale_g009_definitionFtable)) /\ exists ff_q_pvs_g009_definitionFtableentrypositive. dst_positive_code_g009_definitionFtable = ff_q_pvs_g009_definitionFtableentrypositive * S ((S (dst_index_g009_definitionFtable)) * dst_positive_scale_g009_definitionFtable) + (dst_positive_g009_definitionFtable))) /\ (((((exists ff_h_pvs_g009_definitionFtableentrynegative. ff_h_pvs_g009_definitionFtableentrynegative + S (dst_negative_g009_definitionFtable) = S ((S (dst_index_g009_definitionFtable)) * dst_negative_scale_g009_definitionFtable)) /\ exists ff_q_pvs_g009_definitionFtableentrynegative. dst_negative_code_g009_definitionFtable = ff_q_pvs_g009_definitionFtableentrynegative * S ((S (dst_index_g009_definitionFtable)) * dst_negative_scale_g009_definitionFtable) + (dst_negative_g009_definitionFtable))) /\ (exists ge_balance_positive_g009_definitionFtableentryvalue ge_balance_negative_g009_definitionFtableentryvalue. (((((dst_value_g009_definitionFtable) = 2 * (ge_balance_positive_g009_definitionFtableentryvalue) /\ (ge_balance_negative_g009_definitionFtableentryvalue) = 0) \/ exists ge_signed_half_g009_definitionFtableentryvaluedecode. (((dst_value_g009_definitionFtable) = 2 * ge_signed_half_g009_definitionFtableentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitionFtableentryvalue) = 0) /\ (ge_balance_negative_g009_definitionFtableentryvalue) = S ge_signed_half_g009_definitionFtableentryvaluedecode))) /\ ((dst_positive_g009_definitionFtable) + ge_balance_negative_g009_definitionFtableentryvalue = (dst_negative_g009_definitionFtable) + ge_balance_positive_g009_definitionFtableentryvalue))))))))) /\ (((exists dst_positive_code_g009_definitionFone dst_positive_scale_g009_definitionFone dst_negative_code_g009_definitionFone dst_negative_scale_g009_definitionFone dst_positive_g009_definitionFone dst_negative_g009_definitionFone. ((((F)) = (((((dst_positive_code_g009_definitionFone) + (dst_positive_scale_g009_definitionFone)) * S ((dst_positive_code_g009_definitionFone) + (dst_positive_scale_g009_definitionFone)) + ((dst_positive_scale_g009_definitionFone) + (dst_positive_scale_g009_definitionFone))) + (((dst_negative_code_g009_definitionFone) + (dst_negative_scale_g009_definitionFone)) * S ((dst_negative_code_g009_definitionFone) + (dst_negative_scale_g009_definitionFone)) + ((dst_negative_scale_g009_definitionFone) + (dst_negative_scale_g009_definitionFone)))) * S ((((dst_positive_code_g009_definitionFone) + (dst_positive_scale_g009_definitionFone)) * S ((dst_positive_code_g009_definitionFone) + (dst_positive_scale_g009_definitionFone)) + ((dst_positive_scale_g009_definitionFone) + (dst_positive_scale_g009_definitionFone))) + (((dst_negative_code_g009_definitionFone) + (dst_negative_scale_g009_definitionFone)) * S ((dst_negative_code_g009_definitionFone) + (dst_negative_scale_g009_definitionFone)) + ((dst_negative_scale_g009_definitionFone) + (dst_negative_scale_g009_definitionFone)))) + ((((dst_negative_code_g009_definitionFone) + (dst_negative_scale_g009_definitionFone)) * S ((dst_negative_code_g009_definitionFone) + (dst_negative_scale_g009_definitionFone)) + ((dst_negative_scale_g009_definitionFone) + (dst_negative_scale_g009_definitionFone))) + (((dst_negative_code_g009_definitionFone) + (dst_negative_scale_g009_definitionFone)) * S ((dst_negative_code_g009_definitionFone) + (dst_negative_scale_g009_definitionFone)) + ((dst_negative_scale_g009_definitionFone) + (dst_negative_scale_g009_definitionFone)))))) /\ (((((exists ff_h_pvs_g009_definitionFonepositive. ff_h_pvs_g009_definitionFonepositive + S (dst_positive_g009_definitionFone) = S ((S (1)) * dst_positive_scale_g009_definitionFone)) /\ exists ff_q_pvs_g009_definitionFonepositive. dst_positive_code_g009_definitionFone = ff_q_pvs_g009_definitionFonepositive * S ((S (1)) * dst_positive_scale_g009_definitionFone) + (dst_positive_g009_definitionFone))) /\ (((((exists ff_h_pvs_g009_definitionFonenegative. ff_h_pvs_g009_definitionFonenegative + S (dst_negative_g009_definitionFone) = S ((S (1)) * dst_negative_scale_g009_definitionFone)) /\ exists ff_q_pvs_g009_definitionFonenegative. dst_negative_code_g009_definitionFone = ff_q_pvs_g009_definitionFonenegative * S ((S (1)) * dst_negative_scale_g009_definitionFone) + (dst_negative_g009_definitionFone))) /\ (exists ge_balance_positive_g009_definitionFonevalue ge_balance_negative_g009_definitionFonevalue. (((((2) = 2 * (ge_balance_positive_g009_definitionFonevalue) /\ (ge_balance_negative_g009_definitionFonevalue) = 0) \/ exists ge_signed_half_g009_definitionFonevaluedecode. (((2) = 2 * ge_signed_half_g009_definitionFonevaluedecode + 1 /\ (ge_balance_positive_g009_definitionFonevalue) = 0) /\ (ge_balance_negative_g009_definitionFonevalue) = S ge_signed_half_g009_definitionFonevaluedecode))) /\ ((dst_positive_g009_definitionFone) + ge_balance_negative_g009_definitionFonevalue = (dst_negative_g009_definitionFone) + ge_balance_positive_g009_definitionFonevalue))))))))) /\ (forall mp_a_g009_definitionF mp_b_g009_definitionF mp_x_g009_definitionF mp_y_g009_definitionF mp_z_g009_definitionF. ~(mp_a_g009_definitionF=0) -> ~(mp_b_g009_definitionF=0) -> (exists pvs_le_gap_g009_definitionFbound. pvs_le_gap_g009_definitionFbound + (mp_a_g009_definitionF*mp_b_g009_definitionF) = ((N))) -> (forall frp_divisor_g009_definitionFcoprime. (exists frp_left_factor_g009_definitionFcoprime. mp_a_g009_definitionF = frp_divisor_g009_definitionFcoprime * frp_left_factor_g009_definitionFcoprime) -> (exists frp_right_factor_g009_definitionFcoprime. mp_b_g009_definitionF = frp_divisor_g009_definitionFcoprime * frp_right_factor_g009_definitionFcoprime) -> frp_divisor_g009_definitionFcoprime = 1) -> (exists dst_positive_code_g009_definitionFfirst dst_positive_scale_g009_definitionFfirst dst_negative_code_g009_definitionFfirst dst_negative_scale_g009_definitionFfirst dst_positive_g009_definitionFfirst dst_negative_g009_definitionFfirst. ((((F)) = (((((dst_positive_code_g009_definitionFfirst) + (dst_positive_scale_g009_definitionFfirst)) * S ((dst_positive_code_g009_definitionFfirst) + (dst_positive_scale_g009_definitionFfirst)) + ((dst_positive_scale_g009_definitionFfirst) + (dst_positive_scale_g009_definitionFfirst))) + (((dst_negative_code_g009_definitionFfirst) + (dst_negative_scale_g009_definitionFfirst)) * S ((dst_negative_code_g009_definitionFfirst) + (dst_negative_scale_g009_definitionFfirst)) + ((dst_negative_scale_g009_definitionFfirst) + (dst_negative_scale_g009_definitionFfirst)))) * S ((((dst_positive_code_g009_definitionFfirst) + (dst_positive_scale_g009_definitionFfirst)) * S ((dst_positive_code_g009_definitionFfirst) + (dst_positive_scale_g009_definitionFfirst)) + ((dst_positive_scale_g009_definitionFfirst) + (dst_positive_scale_g009_definitionFfirst))) + (((dst_negative_code_g009_definitionFfirst) + (dst_negative_scale_g009_definitionFfirst)) * S ((dst_negative_code_g009_definitionFfirst) + (dst_negative_scale_g009_definitionFfirst)) + ((dst_negative_scale_g009_definitionFfirst) + (dst_negative_scale_g009_definitionFfirst)))) + ((((dst_negative_code_g009_definitionFfirst) + (dst_negative_scale_g009_definitionFfirst)) * S ((dst_negative_code_g009_definitionFfirst) + (dst_negative_scale_g009_definitionFfirst)) + ((dst_negative_scale_g009_definitionFfirst) + (dst_negative_scale_g009_definitionFfirst))) + (((dst_negative_code_g009_definitionFfirst) + (dst_negative_scale_g009_definitionFfirst)) * S ((dst_negative_code_g009_definitionFfirst) + (dst_negative_scale_g009_definitionFfirst)) + ((dst_negative_scale_g009_definitionFfirst) + (dst_negative_scale_g009_definitionFfirst)))))) /\ (((((exists ff_h_pvs_g009_definitionFfirstpositive. ff_h_pvs_g009_definitionFfirstpositive + S (dst_positive_g009_definitionFfirst) = S ((S (mp_a_g009_definitionF)) * dst_positive_scale_g009_definitionFfirst)) /\ exists ff_q_pvs_g009_definitionFfirstpositive. dst_positive_code_g009_definitionFfirst = ff_q_pvs_g009_definitionFfirstpositive * S ((S (mp_a_g009_definitionF)) * dst_positive_scale_g009_definitionFfirst) + (dst_positive_g009_definitionFfirst))) /\ (((((exists ff_h_pvs_g009_definitionFfirstnegative. ff_h_pvs_g009_definitionFfirstnegative + S (dst_negative_g009_definitionFfirst) = S ((S (mp_a_g009_definitionF)) * dst_negative_scale_g009_definitionFfirst)) /\ exists ff_q_pvs_g009_definitionFfirstnegative. dst_negative_code_g009_definitionFfirst = ff_q_pvs_g009_definitionFfirstnegative * S ((S (mp_a_g009_definitionF)) * dst_negative_scale_g009_definitionFfirst) + (dst_negative_g009_definitionFfirst))) /\ (exists ge_balance_positive_g009_definitionFfirstvalue ge_balance_negative_g009_definitionFfirstvalue. (((((mp_x_g009_definitionF) = 2 * (ge_balance_positive_g009_definitionFfirstvalue) /\ (ge_balance_negative_g009_definitionFfirstvalue) = 0) \/ exists ge_signed_half_g009_definitionFfirstvaluedecode. (((mp_x_g009_definitionF) = 2 * ge_signed_half_g009_definitionFfirstvaluedecode + 1 /\ (ge_balance_positive_g009_definitionFfirstvalue) = 0) /\ (ge_balance_negative_g009_definitionFfirstvalue) = S ge_signed_half_g009_definitionFfirstvaluedecode))) /\ ((dst_positive_g009_definitionFfirst) + ge_balance_negative_g009_definitionFfirstvalue = (dst_negative_g009_definitionFfirst) + ge_balance_positive_g009_definitionFfirstvalue))))))))) -> (exists dst_positive_code_g009_definitionFsecond dst_positive_scale_g009_definitionFsecond dst_negative_code_g009_definitionFsecond dst_negative_scale_g009_definitionFsecond dst_positive_g009_definitionFsecond dst_negative_g009_definitionFsecond. ((((F)) = (((((dst_positive_code_g009_definitionFsecond) + (dst_positive_scale_g009_definitionFsecond)) * S ((dst_positive_code_g009_definitionFsecond) + (dst_positive_scale_g009_definitionFsecond)) + ((dst_positive_scale_g009_definitionFsecond) + (dst_positive_scale_g009_definitionFsecond))) + (((dst_negative_code_g009_definitionFsecond) + (dst_negative_scale_g009_definitionFsecond)) * S ((dst_negative_code_g009_definitionFsecond) + (dst_negative_scale_g009_definitionFsecond)) + ((dst_negative_scale_g009_definitionFsecond) + (dst_negative_scale_g009_definitionFsecond)))) * S ((((dst_positive_code_g009_definitionFsecond) + (dst_positive_scale_g009_definitionFsecond)) * S ((dst_positive_code_g009_definitionFsecond) + (dst_positive_scale_g009_definitionFsecond)) + ((dst_positive_scale_g009_definitionFsecond) + (dst_positive_scale_g009_definitionFsecond))) + (((dst_negative_code_g009_definitionFsecond) + (dst_negative_scale_g009_definitionFsecond)) * S ((dst_negative_code_g009_definitionFsecond) + (dst_negative_scale_g009_definitionFsecond)) + ((dst_negative_scale_g009_definitionFsecond) + (dst_negative_scale_g009_definitionFsecond)))) + ((((dst_negative_code_g009_definitionFsecond) + (dst_negative_scale_g009_definitionFsecond)) * S ((dst_negative_code_g009_definitionFsecond) + (dst_negative_scale_g009_definitionFsecond)) + ((dst_negative_scale_g009_definitionFsecond) + (dst_negative_scale_g009_definitionFsecond))) + (((dst_negative_code_g009_definitionFsecond) + (dst_negative_scale_g009_definitionFsecond)) * S ((dst_negative_code_g009_definitionFsecond) + (dst_negative_scale_g009_definitionFsecond)) + ((dst_negative_scale_g009_definitionFsecond) + (dst_negative_scale_g009_definitionFsecond)))))) /\ (((((exists ff_h_pvs_g009_definitionFsecondpositive. ff_h_pvs_g009_definitionFsecondpositive + S (dst_positive_g009_definitionFsecond) = S ((S (mp_b_g009_definitionF)) * dst_positive_scale_g009_definitionFsecond)) /\ exists ff_q_pvs_g009_definitionFsecondpositive. dst_positive_code_g009_definitionFsecond = ff_q_pvs_g009_definitionFsecondpositive * S ((S (mp_b_g009_definitionF)) * dst_positive_scale_g009_definitionFsecond) + (dst_positive_g009_definitionFsecond))) /\ (((((exists ff_h_pvs_g009_definitionFsecondnegative. ff_h_pvs_g009_definitionFsecondnegative + S (dst_negative_g009_definitionFsecond) = S ((S (mp_b_g009_definitionF)) * dst_negative_scale_g009_definitionFsecond)) /\ exists ff_q_pvs_g009_definitionFsecondnegative. dst_negative_code_g009_definitionFsecond = ff_q_pvs_g009_definitionFsecondnegative * S ((S (mp_b_g009_definitionF)) * dst_negative_scale_g009_definitionFsecond) + (dst_negative_g009_definitionFsecond))) /\ (exists ge_balance_positive_g009_definitionFsecondvalue ge_balance_negative_g009_definitionFsecondvalue. (((((mp_y_g009_definitionF) = 2 * (ge_balance_positive_g009_definitionFsecondvalue) /\ (ge_balance_negative_g009_definitionFsecondvalue) = 0) \/ exists ge_signed_half_g009_definitionFsecondvaluedecode. (((mp_y_g009_definitionF) = 2 * ge_signed_half_g009_definitionFsecondvaluedecode + 1 /\ (ge_balance_positive_g009_definitionFsecondvalue) = 0) /\ (ge_balance_negative_g009_definitionFsecondvalue) = S ge_signed_half_g009_definitionFsecondvaluedecode))) /\ ((dst_positive_g009_definitionFsecond) + ge_balance_negative_g009_definitionFsecondvalue = (dst_negative_g009_definitionFsecond) + ge_balance_positive_g009_definitionFsecondvalue))))))))) -> (exists dst_positive_code_g009_definitionFproduct dst_positive_scale_g009_definitionFproduct dst_negative_code_g009_definitionFproduct dst_negative_scale_g009_definitionFproduct dst_positive_g009_definitionFproduct dst_negative_g009_definitionFproduct. ((((F)) = (((((dst_positive_code_g009_definitionFproduct) + (dst_positive_scale_g009_definitionFproduct)) * S ((dst_positive_code_g009_definitionFproduct) + (dst_positive_scale_g009_definitionFproduct)) + ((dst_positive_scale_g009_definitionFproduct) + (dst_positive_scale_g009_definitionFproduct))) + (((dst_negative_code_g009_definitionFproduct) + (dst_negative_scale_g009_definitionFproduct)) * S ((dst_negative_code_g009_definitionFproduct) + (dst_negative_scale_g009_definitionFproduct)) + ((dst_negative_scale_g009_definitionFproduct) + (dst_negative_scale_g009_definitionFproduct)))) * S ((((dst_positive_code_g009_definitionFproduct) + (dst_positive_scale_g009_definitionFproduct)) * S ((dst_positive_code_g009_definitionFproduct) + (dst_positive_scale_g009_definitionFproduct)) + ((dst_positive_scale_g009_definitionFproduct) + (dst_positive_scale_g009_definitionFproduct))) + (((dst_negative_code_g009_definitionFproduct) + (dst_negative_scale_g009_definitionFproduct)) * S ((dst_negative_code_g009_definitionFproduct) + (dst_negative_scale_g009_definitionFproduct)) + ((dst_negative_scale_g009_definitionFproduct) + (dst_negative_scale_g009_definitionFproduct)))) + ((((dst_negative_code_g009_definitionFproduct) + (dst_negative_scale_g009_definitionFproduct)) * S ((dst_negative_code_g009_definitionFproduct) + (dst_negative_scale_g009_definitionFproduct)) + ((dst_negative_scale_g009_definitionFproduct) + (dst_negative_scale_g009_definitionFproduct))) + (((dst_negative_code_g009_definitionFproduct) + (dst_negative_scale_g009_definitionFproduct)) * S ((dst_negative_code_g009_definitionFproduct) + (dst_negative_scale_g009_definitionFproduct)) + ((dst_negative_scale_g009_definitionFproduct) + (dst_negative_scale_g009_definitionFproduct)))))) /\ (((((exists ff_h_pvs_g009_definitionFproductpositive. ff_h_pvs_g009_definitionFproductpositive + S (dst_positive_g009_definitionFproduct) = S ((S (mp_a_g009_definitionF*mp_b_g009_definitionF)) * dst_positive_scale_g009_definitionFproduct)) /\ exists ff_q_pvs_g009_definitionFproductpositive. dst_positive_code_g009_definitionFproduct = ff_q_pvs_g009_definitionFproductpositive * S ((S (mp_a_g009_definitionF*mp_b_g009_definitionF)) * dst_positive_scale_g009_definitionFproduct) + (dst_positive_g009_definitionFproduct))) /\ (((((exists ff_h_pvs_g009_definitionFproductnegative. ff_h_pvs_g009_definitionFproductnegative + S (dst_negative_g009_definitionFproduct) = S ((S (mp_a_g009_definitionF*mp_b_g009_definitionF)) * dst_negative_scale_g009_definitionFproduct)) /\ exists ff_q_pvs_g009_definitionFproductnegative. dst_negative_code_g009_definitionFproduct = ff_q_pvs_g009_definitionFproductnegative * S ((S (mp_a_g009_definitionF*mp_b_g009_definitionF)) * dst_negative_scale_g009_definitionFproduct) + (dst_negative_g009_definitionFproduct))) /\ (exists ge_balance_positive_g009_definitionFproductvalue ge_balance_negative_g009_definitionFproductvalue. (((((mp_z_g009_definitionF) = 2 * (ge_balance_positive_g009_definitionFproductvalue) /\ (ge_balance_negative_g009_definitionFproductvalue) = 0) \/ exists ge_signed_half_g009_definitionFproductvaluedecode. (((mp_z_g009_definitionF) = 2 * ge_signed_half_g009_definitionFproductvaluedecode + 1 /\ (ge_balance_positive_g009_definitionFproductvalue) = 0) /\ (ge_balance_negative_g009_definitionFproductvalue) = S ge_signed_half_g009_definitionFproductvaluedecode))) /\ ((dst_positive_g009_definitionFproduct) + ge_balance_negative_g009_definitionFproductvalue = (dst_negative_g009_definitionFproduct) + ge_balance_positive_g009_definitionFproductvalue))))))))) -> (exists sto_ap_g009_definitionFlaw sto_an_g009_definitionFlaw sto_bp_g009_definitionFlaw sto_bn_g009_definitionFlaw sto_cp_g009_definitionFlaw sto_cn_g009_definitionFlaw. (((((mp_x_g009_definitionF) = 2 * (sto_ap_g009_definitionFlaw) /\ (sto_an_g009_definitionFlaw) = 0) \/ exists ge_signed_half_g009_definitionFlawleft. (((mp_x_g009_definitionF) = 2 * ge_signed_half_g009_definitionFlawleft + 1 /\ (sto_ap_g009_definitionFlaw) = 0) /\ (sto_an_g009_definitionFlaw) = S ge_signed_half_g009_definitionFlawleft))) /\ ((((((mp_y_g009_definitionF) = 2 * (sto_bp_g009_definitionFlaw) /\ (sto_bn_g009_definitionFlaw) = 0) \/ exists ge_signed_half_g009_definitionFlawright. (((mp_y_g009_definitionF) = 2 * ge_signed_half_g009_definitionFlawright + 1 /\ (sto_bp_g009_definitionFlaw) = 0) /\ (sto_bn_g009_definitionFlaw) = S ge_signed_half_g009_definitionFlawright))) /\ ((((((mp_z_g009_definitionF) = 2 * (sto_cp_g009_definitionFlaw) /\ (sto_cn_g009_definitionFlaw) = 0) \/ exists ge_signed_half_g009_definitionFlawoutput. (((mp_z_g009_definitionF) = 2 * ge_signed_half_g009_definitionFlawoutput + 1 /\ (sto_cp_g009_definitionFlaw) = 0) /\ (sto_cn_g009_definitionFlaw) = S ge_signed_half_g009_definitionFlawoutput))) /\ ((sto_ap_g009_definitionFlaw * sto_bp_g009_definitionFlaw + sto_an_g009_definitionFlaw * sto_bn_g009_definitionFlaw) + sto_cn_g009_definitionFlaw = (sto_ap_g009_definitionFlaw * sto_bn_g009_definitionFlaw + sto_an_g009_definitionFlaw * sto_bp_g009_definitionFlaw) + sto_cp_g009_definitionFlaw)))))))))))))) /\ (((((~(((N))=0)) /\ (((exists dst_positive_code_g009_definitionGtable dst_positive_scale_g009_definitionGtable dst_negative_code_g009_definitionGtable dst_negative_scale_g009_definitionGtable. ((((G)) = (((((dst_positive_code_g009_definitionGtable) + (dst_positive_scale_g009_definitionGtable)) * S ((dst_positive_code_g009_definitionGtable) + (dst_positive_scale_g009_definitionGtable)) + ((dst_positive_scale_g009_definitionGtable) + (dst_positive_scale_g009_definitionGtable))) + (((dst_negative_code_g009_definitionGtable) + (dst_negative_scale_g009_definitionGtable)) * S ((dst_negative_code_g009_definitionGtable) + (dst_negative_scale_g009_definitionGtable)) + ((dst_negative_scale_g009_definitionGtable) + (dst_negative_scale_g009_definitionGtable)))) * S ((((dst_positive_code_g009_definitionGtable) + (dst_positive_scale_g009_definitionGtable)) * S ((dst_positive_code_g009_definitionGtable) + (dst_positive_scale_g009_definitionGtable)) + ((dst_positive_scale_g009_definitionGtable) + (dst_positive_scale_g009_definitionGtable))) + (((dst_negative_code_g009_definitionGtable) + (dst_negative_scale_g009_definitionGtable)) * S ((dst_negative_code_g009_definitionGtable) + (dst_negative_scale_g009_definitionGtable)) + ((dst_negative_scale_g009_definitionGtable) + (dst_negative_scale_g009_definitionGtable)))) + ((((dst_negative_code_g009_definitionGtable) + (dst_negative_scale_g009_definitionGtable)) * S ((dst_negative_code_g009_definitionGtable) + (dst_negative_scale_g009_definitionGtable)) + ((dst_negative_scale_g009_definitionGtable) + (dst_negative_scale_g009_definitionGtable))) + (((dst_negative_code_g009_definitionGtable) + (dst_negative_scale_g009_definitionGtable)) * S ((dst_negative_code_g009_definitionGtable) + (dst_negative_scale_g009_definitionGtable)) + ((dst_negative_scale_g009_definitionGtable) + (dst_negative_scale_g009_definitionGtable)))))) /\ (forall dst_index_g009_definitionGtable. (exists pvs_le_gap_g009_definitionGtabledomain. pvs_le_gap_g009_definitionGtabledomain + (dst_index_g009_definitionGtable) = ((N))) -> exists dst_positive_g009_definitionGtable dst_negative_g009_definitionGtable dst_value_g009_definitionGtable. ((((exists ff_h_pvs_g009_definitionGtableentrypositive. ff_h_pvs_g009_definitionGtableentrypositive + S (dst_positive_g009_definitionGtable) = S ((S (dst_index_g009_definitionGtable)) * dst_positive_scale_g009_definitionGtable)) /\ exists ff_q_pvs_g009_definitionGtableentrypositive. dst_positive_code_g009_definitionGtable = ff_q_pvs_g009_definitionGtableentrypositive * S ((S (dst_index_g009_definitionGtable)) * dst_positive_scale_g009_definitionGtable) + (dst_positive_g009_definitionGtable))) /\ (((((exists ff_h_pvs_g009_definitionGtableentrynegative. ff_h_pvs_g009_definitionGtableentrynegative + S (dst_negative_g009_definitionGtable) = S ((S (dst_index_g009_definitionGtable)) * dst_negative_scale_g009_definitionGtable)) /\ exists ff_q_pvs_g009_definitionGtableentrynegative. dst_negative_code_g009_definitionGtable = ff_q_pvs_g009_definitionGtableentrynegative * S ((S (dst_index_g009_definitionGtable)) * dst_negative_scale_g009_definitionGtable) + (dst_negative_g009_definitionGtable))) /\ (exists ge_balance_positive_g009_definitionGtableentryvalue ge_balance_negative_g009_definitionGtableentryvalue. (((((dst_value_g009_definitionGtable) = 2 * (ge_balance_positive_g009_definitionGtableentryvalue) /\ (ge_balance_negative_g009_definitionGtableentryvalue) = 0) \/ exists ge_signed_half_g009_definitionGtableentryvaluedecode. (((dst_value_g009_definitionGtable) = 2 * ge_signed_half_g009_definitionGtableentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitionGtableentryvalue) = 0) /\ (ge_balance_negative_g009_definitionGtableentryvalue) = S ge_signed_half_g009_definitionGtableentryvaluedecode))) /\ ((dst_positive_g009_definitionGtable) + ge_balance_negative_g009_definitionGtableentryvalue = (dst_negative_g009_definitionGtable) + ge_balance_positive_g009_definitionGtableentryvalue))))))))) /\ (((exists dst_positive_code_g009_definitionGone dst_positive_scale_g009_definitionGone dst_negative_code_g009_definitionGone dst_negative_scale_g009_definitionGone dst_positive_g009_definitionGone dst_negative_g009_definitionGone. ((((G)) = (((((dst_positive_code_g009_definitionGone) + (dst_positive_scale_g009_definitionGone)) * S ((dst_positive_code_g009_definitionGone) + (dst_positive_scale_g009_definitionGone)) + ((dst_positive_scale_g009_definitionGone) + (dst_positive_scale_g009_definitionGone))) + (((dst_negative_code_g009_definitionGone) + (dst_negative_scale_g009_definitionGone)) * S ((dst_negative_code_g009_definitionGone) + (dst_negative_scale_g009_definitionGone)) + ((dst_negative_scale_g009_definitionGone) + (dst_negative_scale_g009_definitionGone)))) * S ((((dst_positive_code_g009_definitionGone) + (dst_positive_scale_g009_definitionGone)) * S ((dst_positive_code_g009_definitionGone) + (dst_positive_scale_g009_definitionGone)) + ((dst_positive_scale_g009_definitionGone) + (dst_positive_scale_g009_definitionGone))) + (((dst_negative_code_g009_definitionGone) + (dst_negative_scale_g009_definitionGone)) * S ((dst_negative_code_g009_definitionGone) + (dst_negative_scale_g009_definitionGone)) + ((dst_negative_scale_g009_definitionGone) + (dst_negative_scale_g009_definitionGone)))) + ((((dst_negative_code_g009_definitionGone) + (dst_negative_scale_g009_definitionGone)) * S ((dst_negative_code_g009_definitionGone) + (dst_negative_scale_g009_definitionGone)) + ((dst_negative_scale_g009_definitionGone) + (dst_negative_scale_g009_definitionGone))) + (((dst_negative_code_g009_definitionGone) + (dst_negative_scale_g009_definitionGone)) * S ((dst_negative_code_g009_definitionGone) + (dst_negative_scale_g009_definitionGone)) + ((dst_negative_scale_g009_definitionGone) + (dst_negative_scale_g009_definitionGone)))))) /\ (((((exists ff_h_pvs_g009_definitionGonepositive. ff_h_pvs_g009_definitionGonepositive + S (dst_positive_g009_definitionGone) = S ((S (1)) * dst_positive_scale_g009_definitionGone)) /\ exists ff_q_pvs_g009_definitionGonepositive. dst_positive_code_g009_definitionGone = ff_q_pvs_g009_definitionGonepositive * S ((S (1)) * dst_positive_scale_g009_definitionGone) + (dst_positive_g009_definitionGone))) /\ (((((exists ff_h_pvs_g009_definitionGonenegative. ff_h_pvs_g009_definitionGonenegative + S (dst_negative_g009_definitionGone) = S ((S (1)) * dst_negative_scale_g009_definitionGone)) /\ exists ff_q_pvs_g009_definitionGonenegative. dst_negative_code_g009_definitionGone = ff_q_pvs_g009_definitionGonenegative * S ((S (1)) * dst_negative_scale_g009_definitionGone) + (dst_negative_g009_definitionGone))) /\ (exists ge_balance_positive_g009_definitionGonevalue ge_balance_negative_g009_definitionGonevalue. (((((2) = 2 * (ge_balance_positive_g009_definitionGonevalue) /\ (ge_balance_negative_g009_definitionGonevalue) = 0) \/ exists ge_signed_half_g009_definitionGonevaluedecode. (((2) = 2 * ge_signed_half_g009_definitionGonevaluedecode + 1 /\ (ge_balance_positive_g009_definitionGonevalue) = 0) /\ (ge_balance_negative_g009_definitionGonevalue) = S ge_signed_half_g009_definitionGonevaluedecode))) /\ ((dst_positive_g009_definitionGone) + ge_balance_negative_g009_definitionGonevalue = (dst_negative_g009_definitionGone) + ge_balance_positive_g009_definitionGonevalue))))))))) /\ (forall mp_a_g009_definitionG mp_b_g009_definitionG mp_x_g009_definitionG mp_y_g009_definitionG mp_z_g009_definitionG. ~(mp_a_g009_definitionG=0) -> ~(mp_b_g009_definitionG=0) -> (exists pvs_le_gap_g009_definitionGbound. pvs_le_gap_g009_definitionGbound + (mp_a_g009_definitionG*mp_b_g009_definitionG) = ((N))) -> (forall frp_divisor_g009_definitionGcoprime. (exists frp_left_factor_g009_definitionGcoprime. mp_a_g009_definitionG = frp_divisor_g009_definitionGcoprime * frp_left_factor_g009_definitionGcoprime) -> (exists frp_right_factor_g009_definitionGcoprime. mp_b_g009_definitionG = frp_divisor_g009_definitionGcoprime * frp_right_factor_g009_definitionGcoprime) -> frp_divisor_g009_definitionGcoprime = 1) -> (exists dst_positive_code_g009_definitionGfirst dst_positive_scale_g009_definitionGfirst dst_negative_code_g009_definitionGfirst dst_negative_scale_g009_definitionGfirst dst_positive_g009_definitionGfirst dst_negative_g009_definitionGfirst. ((((G)) = (((((dst_positive_code_g009_definitionGfirst) + (dst_positive_scale_g009_definitionGfirst)) * S ((dst_positive_code_g009_definitionGfirst) + (dst_positive_scale_g009_definitionGfirst)) + ((dst_positive_scale_g009_definitionGfirst) + (dst_positive_scale_g009_definitionGfirst))) + (((dst_negative_code_g009_definitionGfirst) + (dst_negative_scale_g009_definitionGfirst)) * S ((dst_negative_code_g009_definitionGfirst) + (dst_negative_scale_g009_definitionGfirst)) + ((dst_negative_scale_g009_definitionGfirst) + (dst_negative_scale_g009_definitionGfirst)))) * S ((((dst_positive_code_g009_definitionGfirst) + (dst_positive_scale_g009_definitionGfirst)) * S ((dst_positive_code_g009_definitionGfirst) + (dst_positive_scale_g009_definitionGfirst)) + ((dst_positive_scale_g009_definitionGfirst) + (dst_positive_scale_g009_definitionGfirst))) + (((dst_negative_code_g009_definitionGfirst) + (dst_negative_scale_g009_definitionGfirst)) * S ((dst_negative_code_g009_definitionGfirst) + (dst_negative_scale_g009_definitionGfirst)) + ((dst_negative_scale_g009_definitionGfirst) + (dst_negative_scale_g009_definitionGfirst)))) + ((((dst_negative_code_g009_definitionGfirst) + (dst_negative_scale_g009_definitionGfirst)) * S ((dst_negative_code_g009_definitionGfirst) + (dst_negative_scale_g009_definitionGfirst)) + ((dst_negative_scale_g009_definitionGfirst) + (dst_negative_scale_g009_definitionGfirst))) + (((dst_negative_code_g009_definitionGfirst) + (dst_negative_scale_g009_definitionGfirst)) * S ((dst_negative_code_g009_definitionGfirst) + (dst_negative_scale_g009_definitionGfirst)) + ((dst_negative_scale_g009_definitionGfirst) + (dst_negative_scale_g009_definitionGfirst)))))) /\ (((((exists ff_h_pvs_g009_definitionGfirstpositive. ff_h_pvs_g009_definitionGfirstpositive + S (dst_positive_g009_definitionGfirst) = S ((S (mp_a_g009_definitionG)) * dst_positive_scale_g009_definitionGfirst)) /\ exists ff_q_pvs_g009_definitionGfirstpositive. dst_positive_code_g009_definitionGfirst = ff_q_pvs_g009_definitionGfirstpositive * S ((S (mp_a_g009_definitionG)) * dst_positive_scale_g009_definitionGfirst) + (dst_positive_g009_definitionGfirst))) /\ (((((exists ff_h_pvs_g009_definitionGfirstnegative. ff_h_pvs_g009_definitionGfirstnegative + S (dst_negative_g009_definitionGfirst) = S ((S (mp_a_g009_definitionG)) * dst_negative_scale_g009_definitionGfirst)) /\ exists ff_q_pvs_g009_definitionGfirstnegative. dst_negative_code_g009_definitionGfirst = ff_q_pvs_g009_definitionGfirstnegative * S ((S (mp_a_g009_definitionG)) * dst_negative_scale_g009_definitionGfirst) + (dst_negative_g009_definitionGfirst))) /\ (exists ge_balance_positive_g009_definitionGfirstvalue ge_balance_negative_g009_definitionGfirstvalue. (((((mp_x_g009_definitionG) = 2 * (ge_balance_positive_g009_definitionGfirstvalue) /\ (ge_balance_negative_g009_definitionGfirstvalue) = 0) \/ exists ge_signed_half_g009_definitionGfirstvaluedecode. (((mp_x_g009_definitionG) = 2 * ge_signed_half_g009_definitionGfirstvaluedecode + 1 /\ (ge_balance_positive_g009_definitionGfirstvalue) = 0) /\ (ge_balance_negative_g009_definitionGfirstvalue) = S ge_signed_half_g009_definitionGfirstvaluedecode))) /\ ((dst_positive_g009_definitionGfirst) + ge_balance_negative_g009_definitionGfirstvalue = (dst_negative_g009_definitionGfirst) + ge_balance_positive_g009_definitionGfirstvalue))))))))) -> (exists dst_positive_code_g009_definitionGsecond dst_positive_scale_g009_definitionGsecond dst_negative_code_g009_definitionGsecond dst_negative_scale_g009_definitionGsecond dst_positive_g009_definitionGsecond dst_negative_g009_definitionGsecond. ((((G)) = (((((dst_positive_code_g009_definitionGsecond) + (dst_positive_scale_g009_definitionGsecond)) * S ((dst_positive_code_g009_definitionGsecond) + (dst_positive_scale_g009_definitionGsecond)) + ((dst_positive_scale_g009_definitionGsecond) + (dst_positive_scale_g009_definitionGsecond))) + (((dst_negative_code_g009_definitionGsecond) + (dst_negative_scale_g009_definitionGsecond)) * S ((dst_negative_code_g009_definitionGsecond) + (dst_negative_scale_g009_definitionGsecond)) + ((dst_negative_scale_g009_definitionGsecond) + (dst_negative_scale_g009_definitionGsecond)))) * S ((((dst_positive_code_g009_definitionGsecond) + (dst_positive_scale_g009_definitionGsecond)) * S ((dst_positive_code_g009_definitionGsecond) + (dst_positive_scale_g009_definitionGsecond)) + ((dst_positive_scale_g009_definitionGsecond) + (dst_positive_scale_g009_definitionGsecond))) + (((dst_negative_code_g009_definitionGsecond) + (dst_negative_scale_g009_definitionGsecond)) * S ((dst_negative_code_g009_definitionGsecond) + (dst_negative_scale_g009_definitionGsecond)) + ((dst_negative_scale_g009_definitionGsecond) + (dst_negative_scale_g009_definitionGsecond)))) + ((((dst_negative_code_g009_definitionGsecond) + (dst_negative_scale_g009_definitionGsecond)) * S ((dst_negative_code_g009_definitionGsecond) + (dst_negative_scale_g009_definitionGsecond)) + ((dst_negative_scale_g009_definitionGsecond) + (dst_negative_scale_g009_definitionGsecond))) + (((dst_negative_code_g009_definitionGsecond) + (dst_negative_scale_g009_definitionGsecond)) * S ((dst_negative_code_g009_definitionGsecond) + (dst_negative_scale_g009_definitionGsecond)) + ((dst_negative_scale_g009_definitionGsecond) + (dst_negative_scale_g009_definitionGsecond)))))) /\ (((((exists ff_h_pvs_g009_definitionGsecondpositive. ff_h_pvs_g009_definitionGsecondpositive + S (dst_positive_g009_definitionGsecond) = S ((S (mp_b_g009_definitionG)) * dst_positive_scale_g009_definitionGsecond)) /\ exists ff_q_pvs_g009_definitionGsecondpositive. dst_positive_code_g009_definitionGsecond = ff_q_pvs_g009_definitionGsecondpositive * S ((S (mp_b_g009_definitionG)) * dst_positive_scale_g009_definitionGsecond) + (dst_positive_g009_definitionGsecond))) /\ (((((exists ff_h_pvs_g009_definitionGsecondnegative. ff_h_pvs_g009_definitionGsecondnegative + S (dst_negative_g009_definitionGsecond) = S ((S (mp_b_g009_definitionG)) * dst_negative_scale_g009_definitionGsecond)) /\ exists ff_q_pvs_g009_definitionGsecondnegative. dst_negative_code_g009_definitionGsecond = ff_q_pvs_g009_definitionGsecondnegative * S ((S (mp_b_g009_definitionG)) * dst_negative_scale_g009_definitionGsecond) + (dst_negative_g009_definitionGsecond))) /\ (exists ge_balance_positive_g009_definitionGsecondvalue ge_balance_negative_g009_definitionGsecondvalue. (((((mp_y_g009_definitionG) = 2 * (ge_balance_positive_g009_definitionGsecondvalue) /\ (ge_balance_negative_g009_definitionGsecondvalue) = 0) \/ exists ge_signed_half_g009_definitionGsecondvaluedecode. (((mp_y_g009_definitionG) = 2 * ge_signed_half_g009_definitionGsecondvaluedecode + 1 /\ (ge_balance_positive_g009_definitionGsecondvalue) = 0) /\ (ge_balance_negative_g009_definitionGsecondvalue) = S ge_signed_half_g009_definitionGsecondvaluedecode))) /\ ((dst_positive_g009_definitionGsecond) + ge_balance_negative_g009_definitionGsecondvalue = (dst_negative_g009_definitionGsecond) + ge_balance_positive_g009_definitionGsecondvalue))))))))) -> (exists dst_positive_code_g009_definitionGproduct dst_positive_scale_g009_definitionGproduct dst_negative_code_g009_definitionGproduct dst_negative_scale_g009_definitionGproduct dst_positive_g009_definitionGproduct dst_negative_g009_definitionGproduct. ((((G)) = (((((dst_positive_code_g009_definitionGproduct) + (dst_positive_scale_g009_definitionGproduct)) * S ((dst_positive_code_g009_definitionGproduct) + (dst_positive_scale_g009_definitionGproduct)) + ((dst_positive_scale_g009_definitionGproduct) + (dst_positive_scale_g009_definitionGproduct))) + (((dst_negative_code_g009_definitionGproduct) + (dst_negative_scale_g009_definitionGproduct)) * S ((dst_negative_code_g009_definitionGproduct) + (dst_negative_scale_g009_definitionGproduct)) + ((dst_negative_scale_g009_definitionGproduct) + (dst_negative_scale_g009_definitionGproduct)))) * S ((((dst_positive_code_g009_definitionGproduct) + (dst_positive_scale_g009_definitionGproduct)) * S ((dst_positive_code_g009_definitionGproduct) + (dst_positive_scale_g009_definitionGproduct)) + ((dst_positive_scale_g009_definitionGproduct) + (dst_positive_scale_g009_definitionGproduct))) + (((dst_negative_code_g009_definitionGproduct) + (dst_negative_scale_g009_definitionGproduct)) * S ((dst_negative_code_g009_definitionGproduct) + (dst_negative_scale_g009_definitionGproduct)) + ((dst_negative_scale_g009_definitionGproduct) + (dst_negative_scale_g009_definitionGproduct)))) + ((((dst_negative_code_g009_definitionGproduct) + (dst_negative_scale_g009_definitionGproduct)) * S ((dst_negative_code_g009_definitionGproduct) + (dst_negative_scale_g009_definitionGproduct)) + ((dst_negative_scale_g009_definitionGproduct) + (dst_negative_scale_g009_definitionGproduct))) + (((dst_negative_code_g009_definitionGproduct) + (dst_negative_scale_g009_definitionGproduct)) * S ((dst_negative_code_g009_definitionGproduct) + (dst_negative_scale_g009_definitionGproduct)) + ((dst_negative_scale_g009_definitionGproduct) + (dst_negative_scale_g009_definitionGproduct)))))) /\ (((((exists ff_h_pvs_g009_definitionGproductpositive. ff_h_pvs_g009_definitionGproductpositive + S (dst_positive_g009_definitionGproduct) = S ((S (mp_a_g009_definitionG*mp_b_g009_definitionG)) * dst_positive_scale_g009_definitionGproduct)) /\ exists ff_q_pvs_g009_definitionGproductpositive. dst_positive_code_g009_definitionGproduct = ff_q_pvs_g009_definitionGproductpositive * S ((S (mp_a_g009_definitionG*mp_b_g009_definitionG)) * dst_positive_scale_g009_definitionGproduct) + (dst_positive_g009_definitionGproduct))) /\ (((((exists ff_h_pvs_g009_definitionGproductnegative. ff_h_pvs_g009_definitionGproductnegative + S (dst_negative_g009_definitionGproduct) = S ((S (mp_a_g009_definitionG*mp_b_g009_definitionG)) * dst_negative_scale_g009_definitionGproduct)) /\ exists ff_q_pvs_g009_definitionGproductnegative. dst_negative_code_g009_definitionGproduct = ff_q_pvs_g009_definitionGproductnegative * S ((S (mp_a_g009_definitionG*mp_b_g009_definitionG)) * dst_negative_scale_g009_definitionGproduct) + (dst_negative_g009_definitionGproduct))) /\ (exists ge_balance_positive_g009_definitionGproductvalue ge_balance_negative_g009_definitionGproductvalue. (((((mp_z_g009_definitionG) = 2 * (ge_balance_positive_g009_definitionGproductvalue) /\ (ge_balance_negative_g009_definitionGproductvalue) = 0) \/ exists ge_signed_half_g009_definitionGproductvaluedecode. (((mp_z_g009_definitionG) = 2 * ge_signed_half_g009_definitionGproductvaluedecode + 1 /\ (ge_balance_positive_g009_definitionGproductvalue) = 0) /\ (ge_balance_negative_g009_definitionGproductvalue) = S ge_signed_half_g009_definitionGproductvaluedecode))) /\ ((dst_positive_g009_definitionGproduct) + ge_balance_negative_g009_definitionGproductvalue = (dst_negative_g009_definitionGproduct) + ge_balance_positive_g009_definitionGproductvalue))))))))) -> (exists sto_ap_g009_definitionGlaw sto_an_g009_definitionGlaw sto_bp_g009_definitionGlaw sto_bn_g009_definitionGlaw sto_cp_g009_definitionGlaw sto_cn_g009_definitionGlaw. (((((mp_x_g009_definitionG) = 2 * (sto_ap_g009_definitionGlaw) /\ (sto_an_g009_definitionGlaw) = 0) \/ exists ge_signed_half_g009_definitionGlawleft. (((mp_x_g009_definitionG) = 2 * ge_signed_half_g009_definitionGlawleft + 1 /\ (sto_ap_g009_definitionGlaw) = 0) /\ (sto_an_g009_definitionGlaw) = S ge_signed_half_g009_definitionGlawleft))) /\ ((((((mp_y_g009_definitionG) = 2 * (sto_bp_g009_definitionGlaw) /\ (sto_bn_g009_definitionGlaw) = 0) \/ exists ge_signed_half_g009_definitionGlawright. (((mp_y_g009_definitionG) = 2 * ge_signed_half_g009_definitionGlawright + 1 /\ (sto_bp_g009_definitionGlaw) = 0) /\ (sto_bn_g009_definitionGlaw) = S ge_signed_half_g009_definitionGlawright))) /\ ((((((mp_z_g009_definitionG) = 2 * (sto_cp_g009_definitionGlaw) /\ (sto_cn_g009_definitionGlaw) = 0) \/ exists ge_signed_half_g009_definitionGlawoutput. (((mp_z_g009_definitionG) = 2 * ge_signed_half_g009_definitionGlawoutput + 1 /\ (sto_cp_g009_definitionGlaw) = 0) /\ (sto_cn_g009_definitionGlaw) = S ge_signed_half_g009_definitionGlawoutput))) /\ ((sto_ap_g009_definitionGlaw * sto_bp_g009_definitionGlaw + sto_an_g009_definitionGlaw * sto_bn_g009_definitionGlaw) + sto_cn_g009_definitionGlaw = (sto_ap_g009_definitionGlaw * sto_bn_g009_definitionGlaw + sto_an_g009_definitionGlaw * sto_bp_g009_definitionGlaw) + sto_cp_g009_definitionGlaw)))))))))))))) /\ (((~(((m))=0)) /\ (((~(((n))=0)) /\ (((exists pvs_le_gap_g009_definitionbound. pvs_le_gap_g009_definitionbound + (((m))*((n))) = ((N))) /\ (((forall sfd_common_divisor_g009_definitioncoprime. (exists pvs_factor_g009_definitioncoprimeleft. ((m)) = (sfd_common_divisor_g009_definitioncoprime) * pvs_factor_g009_definitioncoprimeleft) -> (exists pvs_factor_g009_definitioncoprimeright. ((n)) = (sfd_common_divisor_g009_definitioncoprime) * pvs_factor_g009_definitioncoprimeright) -> sfd_common_divisor_g009_definitioncoprime = 1) /\ (((((exists dst_positive_code_g009_definitionlefttable dst_positive_scale_g009_definitionlefttable dst_negative_code_g009_definitionlefttable dst_negative_scale_g009_definitionlefttable. ((((A)) = (((((dst_positive_code_g009_definitionlefttable) + (dst_positive_scale_g009_definitionlefttable)) * S ((dst_positive_code_g009_definitionlefttable) + (dst_positive_scale_g009_definitionlefttable)) + ((dst_positive_scale_g009_definitionlefttable) + (dst_positive_scale_g009_definitionlefttable))) + (((dst_negative_code_g009_definitionlefttable) + (dst_negative_scale_g009_definitionlefttable)) * S ((dst_negative_code_g009_definitionlefttable) + (dst_negative_scale_g009_definitionlefttable)) + ((dst_negative_scale_g009_definitionlefttable) + (dst_negative_scale_g009_definitionlefttable)))) * S ((((dst_positive_code_g009_definitionlefttable) + (dst_positive_scale_g009_definitionlefttable)) * S ((dst_positive_code_g009_definitionlefttable) + (dst_positive_scale_g009_definitionlefttable)) + ((dst_positive_scale_g009_definitionlefttable) + (dst_positive_scale_g009_definitionlefttable))) + (((dst_negative_code_g009_definitionlefttable) + (dst_negative_scale_g009_definitionlefttable)) * S ((dst_negative_code_g009_definitionlefttable) + (dst_negative_scale_g009_definitionlefttable)) + ((dst_negative_scale_g009_definitionlefttable) + (dst_negative_scale_g009_definitionlefttable)))) + ((((dst_negative_code_g009_definitionlefttable) + (dst_negative_scale_g009_definitionlefttable)) * S ((dst_negative_code_g009_definitionlefttable) + (dst_negative_scale_g009_definitionlefttable)) + ((dst_negative_scale_g009_definitionlefttable) + (dst_negative_scale_g009_definitionlefttable))) + (((dst_negative_code_g009_definitionlefttable) + (dst_negative_scale_g009_definitionlefttable)) * S ((dst_negative_code_g009_definitionlefttable) + (dst_negative_scale_g009_definitionlefttable)) + ((dst_negative_scale_g009_definitionlefttable) + (dst_negative_scale_g009_definitionlefttable)))))) /\ (forall dst_index_g009_definitionlefttable. (exists pvs_le_gap_g009_definitionlefttabledomain. pvs_le_gap_g009_definitionlefttabledomain + (dst_index_g009_definitionlefttable) = ((m))) -> exists dst_positive_g009_definitionlefttable dst_negative_g009_definitionlefttable dst_value_g009_definitionlefttable. ((((exists ff_h_pvs_g009_definitionlefttableentrypositive. ff_h_pvs_g009_definitionlefttableentrypositive + S (dst_positive_g009_definitionlefttable) = S ((S (dst_index_g009_definitionlefttable)) * dst_positive_scale_g009_definitionlefttable)) /\ exists ff_q_pvs_g009_definitionlefttableentrypositive. dst_positive_code_g009_definitionlefttable = ff_q_pvs_g009_definitionlefttableentrypositive * S ((S (dst_index_g009_definitionlefttable)) * dst_positive_scale_g009_definitionlefttable) + (dst_positive_g009_definitionlefttable))) /\ (((((exists ff_h_pvs_g009_definitionlefttableentrynegative. ff_h_pvs_g009_definitionlefttableentrynegative + S (dst_negative_g009_definitionlefttable) = S ((S (dst_index_g009_definitionlefttable)) * dst_negative_scale_g009_definitionlefttable)) /\ exists ff_q_pvs_g009_definitionlefttableentrynegative. dst_negative_code_g009_definitionlefttable = ff_q_pvs_g009_definitionlefttableentrynegative * S ((S (dst_index_g009_definitionlefttable)) * dst_negative_scale_g009_definitionlefttable) + (dst_negative_g009_definitionlefttable))) /\ (exists ge_balance_positive_g009_definitionlefttableentryvalue ge_balance_negative_g009_definitionlefttableentryvalue. (((((dst_value_g009_definitionlefttable) = 2 * (ge_balance_positive_g009_definitionlefttableentryvalue) /\ (ge_balance_negative_g009_definitionlefttableentryvalue) = 0) \/ exists ge_signed_half_g009_definitionlefttableentryvaluedecode. (((dst_value_g009_definitionlefttable) = 2 * ge_signed_half_g009_definitionlefttableentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitionlefttableentryvalue) = 0) /\ (ge_balance_negative_g009_definitionlefttableentryvalue) = S ge_signed_half_g009_definitionlefttableentryvaluedecode))) /\ ((dst_positive_g009_definitionlefttable) + ge_balance_negative_g009_definitionlefttableentryvalue = (dst_negative_g009_definitionlefttable) + ge_balance_positive_g009_definitionlefttableentryvalue))))))))) /\ (forall dc_index_g009_definitionleft dc_value_g009_definitionleft. (exists pvs_le_gap_g009_definitionleftdomain. pvs_le_gap_g009_definitionleftdomain + (dc_index_g009_definitionleft) = ((m))) -> (exists dst_positive_code_g009_definitionleftlookup dst_positive_scale_g009_definitionleftlookup dst_negative_code_g009_definitionleftlookup dst_negative_scale_g009_definitionleftlookup dst_positive_g009_definitionleftlookup dst_negative_g009_definitionleftlookup. ((((A)) = (((((dst_positive_code_g009_definitionleftlookup) + (dst_positive_scale_g009_definitionleftlookup)) * S ((dst_positive_code_g009_definitionleftlookup) + (dst_positive_scale_g009_definitionleftlookup)) + ((dst_positive_scale_g009_definitionleftlookup) + (dst_positive_scale_g009_definitionleftlookup))) + (((dst_negative_code_g009_definitionleftlookup) + (dst_negative_scale_g009_definitionleftlookup)) * S ((dst_negative_code_g009_definitionleftlookup) + (dst_negative_scale_g009_definitionleftlookup)) + ((dst_negative_scale_g009_definitionleftlookup) + (dst_negative_scale_g009_definitionleftlookup)))) * S ((((dst_positive_code_g009_definitionleftlookup) + (dst_positive_scale_g009_definitionleftlookup)) * S ((dst_positive_code_g009_definitionleftlookup) + (dst_positive_scale_g009_definitionleftlookup)) + ((dst_positive_scale_g009_definitionleftlookup) + (dst_positive_scale_g009_definitionleftlookup))) + (((dst_negative_code_g009_definitionleftlookup) + (dst_negative_scale_g009_definitionleftlookup)) * S ((dst_negative_code_g009_definitionleftlookup) + (dst_negative_scale_g009_definitionleftlookup)) + ((dst_negative_scale_g009_definitionleftlookup) + (dst_negative_scale_g009_definitionleftlookup)))) + ((((dst_negative_code_g009_definitionleftlookup) + (dst_negative_scale_g009_definitionleftlookup)) * S ((dst_negative_code_g009_definitionleftlookup) + (dst_negative_scale_g009_definitionleftlookup)) + ((dst_negative_scale_g009_definitionleftlookup) + (dst_negative_scale_g009_definitionleftlookup))) + (((dst_negative_code_g009_definitionleftlookup) + (dst_negative_scale_g009_definitionleftlookup)) * S ((dst_negative_code_g009_definitionleftlookup) + (dst_negative_scale_g009_definitionleftlookup)) + ((dst_negative_scale_g009_definitionleftlookup) + (dst_negative_scale_g009_definitionleftlookup)))))) /\ (((((exists ff_h_pvs_g009_definitionleftlookuppositive. ff_h_pvs_g009_definitionleftlookuppositive + S (dst_positive_g009_definitionleftlookup) = S ((S (dc_index_g009_definitionleft)) * dst_positive_scale_g009_definitionleftlookup)) /\ exists ff_q_pvs_g009_definitionleftlookuppositive. dst_positive_code_g009_definitionleftlookup = ff_q_pvs_g009_definitionleftlookuppositive * S ((S (dc_index_g009_definitionleft)) * dst_positive_scale_g009_definitionleftlookup) + (dst_positive_g009_definitionleftlookup))) /\ (((((exists ff_h_pvs_g009_definitionleftlookupnegative. ff_h_pvs_g009_definitionleftlookupnegative + S (dst_negative_g009_definitionleftlookup) = S ((S (dc_index_g009_definitionleft)) * dst_negative_scale_g009_definitionleftlookup)) /\ exists ff_q_pvs_g009_definitionleftlookupnegative. dst_negative_code_g009_definitionleftlookup = ff_q_pvs_g009_definitionleftlookupnegative * S ((S (dc_index_g009_definitionleft)) * dst_negative_scale_g009_definitionleftlookup) + (dst_negative_g009_definitionleftlookup))) /\ (exists ge_balance_positive_g009_definitionleftlookupvalue ge_balance_negative_g009_definitionleftlookupvalue. (((((dc_value_g009_definitionleft) = 2 * (ge_balance_positive_g009_definitionleftlookupvalue) /\ (ge_balance_negative_g009_definitionleftlookupvalue) = 0) \/ exists ge_signed_half_g009_definitionleftlookupvaluedecode. (((dc_value_g009_definitionleft) = 2 * ge_signed_half_g009_definitionleftlookupvaluedecode + 1 /\ (ge_balance_positive_g009_definitionleftlookupvalue) = 0) /\ (ge_balance_negative_g009_definitionleftlookupvalue) = S ge_signed_half_g009_definitionleftlookupvaluedecode))) /\ ((dst_positive_g009_definitionleftlookup) + ge_balance_negative_g009_definitionleftlookupvalue = (dst_negative_g009_definitionleftlookup) + ge_balance_positive_g009_definitionleftlookupvalue))))))))) -> ((((~((dc_index_g009_definitionleft)=0)) /\ (exists dc_quotient_g009_definitionleftentry dc_left_g009_definitionleftentry dc_right_g009_definitionleftentry. ((((m))=(dc_index_g009_definitionleft)*dc_quotient_g009_definitionleftentry) /\ (((exists dst_positive_code_g009_definitionleftentryleft dst_positive_scale_g009_definitionleftentryleft dst_negative_code_g009_definitionleftentryleft dst_negative_scale_g009_definitionleftentryleft dst_positive_g009_definitionleftentryleft dst_negative_g009_definitionleftentryleft. ((((F)) = (((((dst_positive_code_g009_definitionleftentryleft) + (dst_positive_scale_g009_definitionleftentryleft)) * S ((dst_positive_code_g009_definitionleftentryleft) + (dst_positive_scale_g009_definitionleftentryleft)) + ((dst_positive_scale_g009_definitionleftentryleft) + (dst_positive_scale_g009_definitionleftentryleft))) + (((dst_negative_code_g009_definitionleftentryleft) + (dst_negative_scale_g009_definitionleftentryleft)) * S ((dst_negative_code_g009_definitionleftentryleft) + (dst_negative_scale_g009_definitionleftentryleft)) + ((dst_negative_scale_g009_definitionleftentryleft) + (dst_negative_scale_g009_definitionleftentryleft)))) * S ((((dst_positive_code_g009_definitionleftentryleft) + (dst_positive_scale_g009_definitionleftentryleft)) * S ((dst_positive_code_g009_definitionleftentryleft) + (dst_positive_scale_g009_definitionleftentryleft)) + ((dst_positive_scale_g009_definitionleftentryleft) + (dst_positive_scale_g009_definitionleftentryleft))) + (((dst_negative_code_g009_definitionleftentryleft) + (dst_negative_scale_g009_definitionleftentryleft)) * S ((dst_negative_code_g009_definitionleftentryleft) + (dst_negative_scale_g009_definitionleftentryleft)) + ((dst_negative_scale_g009_definitionleftentryleft) + (dst_negative_scale_g009_definitionleftentryleft)))) + ((((dst_negative_code_g009_definitionleftentryleft) + (dst_negative_scale_g009_definitionleftentryleft)) * S ((dst_negative_code_g009_definitionleftentryleft) + (dst_negative_scale_g009_definitionleftentryleft)) + ((dst_negative_scale_g009_definitionleftentryleft) + (dst_negative_scale_g009_definitionleftentryleft))) + (((dst_negative_code_g009_definitionleftentryleft) + (dst_negative_scale_g009_definitionleftentryleft)) * S ((dst_negative_code_g009_definitionleftentryleft) + (dst_negative_scale_g009_definitionleftentryleft)) + ((dst_negative_scale_g009_definitionleftentryleft) + (dst_negative_scale_g009_definitionleftentryleft)))))) /\ (((((exists ff_h_pvs_g009_definitionleftentryleftpositive. ff_h_pvs_g009_definitionleftentryleftpositive + S (dst_positive_g009_definitionleftentryleft) = S ((S (dc_index_g009_definitionleft)) * dst_positive_scale_g009_definitionleftentryleft)) /\ exists ff_q_pvs_g009_definitionleftentryleftpositive. dst_positive_code_g009_definitionleftentryleft = ff_q_pvs_g009_definitionleftentryleftpositive * S ((S (dc_index_g009_definitionleft)) * dst_positive_scale_g009_definitionleftentryleft) + (dst_positive_g009_definitionleftentryleft))) /\ (((((exists ff_h_pvs_g009_definitionleftentryleftnegative. ff_h_pvs_g009_definitionleftentryleftnegative + S (dst_negative_g009_definitionleftentryleft) = S ((S (dc_index_g009_definitionleft)) * dst_negative_scale_g009_definitionleftentryleft)) /\ exists ff_q_pvs_g009_definitionleftentryleftnegative. dst_negative_code_g009_definitionleftentryleft = ff_q_pvs_g009_definitionleftentryleftnegative * S ((S (dc_index_g009_definitionleft)) * dst_negative_scale_g009_definitionleftentryleft) + (dst_negative_g009_definitionleftentryleft))) /\ (exists ge_balance_positive_g009_definitionleftentryleftvalue ge_balance_negative_g009_definitionleftentryleftvalue. (((((dc_left_g009_definitionleftentry) = 2 * (ge_balance_positive_g009_definitionleftentryleftvalue) /\ (ge_balance_negative_g009_definitionleftentryleftvalue) = 0) \/ exists ge_signed_half_g009_definitionleftentryleftvaluedecode. (((dc_left_g009_definitionleftentry) = 2 * ge_signed_half_g009_definitionleftentryleftvaluedecode + 1 /\ (ge_balance_positive_g009_definitionleftentryleftvalue) = 0) /\ (ge_balance_negative_g009_definitionleftentryleftvalue) = S ge_signed_half_g009_definitionleftentryleftvaluedecode))) /\ ((dst_positive_g009_definitionleftentryleft) + ge_balance_negative_g009_definitionleftentryleftvalue = (dst_negative_g009_definitionleftentryleft) + ge_balance_positive_g009_definitionleftentryleftvalue))))))))) /\ (((exists dst_positive_code_g009_definitionleftentryright dst_positive_scale_g009_definitionleftentryright dst_negative_code_g009_definitionleftentryright dst_negative_scale_g009_definitionleftentryright dst_positive_g009_definitionleftentryright dst_negative_g009_definitionleftentryright. ((((G)) = (((((dst_positive_code_g009_definitionleftentryright) + (dst_positive_scale_g009_definitionleftentryright)) * S ((dst_positive_code_g009_definitionleftentryright) + (dst_positive_scale_g009_definitionleftentryright)) + ((dst_positive_scale_g009_definitionleftentryright) + (dst_positive_scale_g009_definitionleftentryright))) + (((dst_negative_code_g009_definitionleftentryright) + (dst_negative_scale_g009_definitionleftentryright)) * S ((dst_negative_code_g009_definitionleftentryright) + (dst_negative_scale_g009_definitionleftentryright)) + ((dst_negative_scale_g009_definitionleftentryright) + (dst_negative_scale_g009_definitionleftentryright)))) * S ((((dst_positive_code_g009_definitionleftentryright) + (dst_positive_scale_g009_definitionleftentryright)) * S ((dst_positive_code_g009_definitionleftentryright) + (dst_positive_scale_g009_definitionleftentryright)) + ((dst_positive_scale_g009_definitionleftentryright) + (dst_positive_scale_g009_definitionleftentryright))) + (((dst_negative_code_g009_definitionleftentryright) + (dst_negative_scale_g009_definitionleftentryright)) * S ((dst_negative_code_g009_definitionleftentryright) + (dst_negative_scale_g009_definitionleftentryright)) + ((dst_negative_scale_g009_definitionleftentryright) + (dst_negative_scale_g009_definitionleftentryright)))) + ((((dst_negative_code_g009_definitionleftentryright) + (dst_negative_scale_g009_definitionleftentryright)) * S ((dst_negative_code_g009_definitionleftentryright) + (dst_negative_scale_g009_definitionleftentryright)) + ((dst_negative_scale_g009_definitionleftentryright) + (dst_negative_scale_g009_definitionleftentryright))) + (((dst_negative_code_g009_definitionleftentryright) + (dst_negative_scale_g009_definitionleftentryright)) * S ((dst_negative_code_g009_definitionleftentryright) + (dst_negative_scale_g009_definitionleftentryright)) + ((dst_negative_scale_g009_definitionleftentryright) + (dst_negative_scale_g009_definitionleftentryright)))))) /\ (((((exists ff_h_pvs_g009_definitionleftentryrightpositive. ff_h_pvs_g009_definitionleftentryrightpositive + S (dst_positive_g009_definitionleftentryright) = S ((S (dc_quotient_g009_definitionleftentry)) * dst_positive_scale_g009_definitionleftentryright)) /\ exists ff_q_pvs_g009_definitionleftentryrightpositive. dst_positive_code_g009_definitionleftentryright = ff_q_pvs_g009_definitionleftentryrightpositive * S ((S (dc_quotient_g009_definitionleftentry)) * dst_positive_scale_g009_definitionleftentryright) + (dst_positive_g009_definitionleftentryright))) /\ (((((exists ff_h_pvs_g009_definitionleftentryrightnegative. ff_h_pvs_g009_definitionleftentryrightnegative + S (dst_negative_g009_definitionleftentryright) = S ((S (dc_quotient_g009_definitionleftentry)) * dst_negative_scale_g009_definitionleftentryright)) /\ exists ff_q_pvs_g009_definitionleftentryrightnegative. dst_negative_code_g009_definitionleftentryright = ff_q_pvs_g009_definitionleftentryrightnegative * S ((S (dc_quotient_g009_definitionleftentry)) * dst_negative_scale_g009_definitionleftentryright) + (dst_negative_g009_definitionleftentryright))) /\ (exists ge_balance_positive_g009_definitionleftentryrightvalue ge_balance_negative_g009_definitionleftentryrightvalue. (((((dc_right_g009_definitionleftentry) = 2 * (ge_balance_positive_g009_definitionleftentryrightvalue) /\ (ge_balance_negative_g009_definitionleftentryrightvalue) = 0) \/ exists ge_signed_half_g009_definitionleftentryrightvaluedecode. (((dc_right_g009_definitionleftentry) = 2 * ge_signed_half_g009_definitionleftentryrightvaluedecode + 1 /\ (ge_balance_positive_g009_definitionleftentryrightvalue) = 0) /\ (ge_balance_negative_g009_definitionleftentryrightvalue) = S ge_signed_half_g009_definitionleftentryrightvaluedecode))) /\ ((dst_positive_g009_definitionleftentryright) + ge_balance_negative_g009_definitionleftentryrightvalue = (dst_negative_g009_definitionleftentryright) + ge_balance_positive_g009_definitionleftentryrightvalue))))))))) /\ (exists sto_ap_g009_definitionleftentryproduct sto_an_g009_definitionleftentryproduct sto_bp_g009_definitionleftentryproduct sto_bn_g009_definitionleftentryproduct sto_cp_g009_definitionleftentryproduct sto_cn_g009_definitionleftentryproduct. (((((dc_left_g009_definitionleftentry) = 2 * (sto_ap_g009_definitionleftentryproduct) /\ (sto_an_g009_definitionleftentryproduct) = 0) \/ exists ge_signed_half_g009_definitionleftentryproductleft. (((dc_left_g009_definitionleftentry) = 2 * ge_signed_half_g009_definitionleftentryproductleft + 1 /\ (sto_ap_g009_definitionleftentryproduct) = 0) /\ (sto_an_g009_definitionleftentryproduct) = S ge_signed_half_g009_definitionleftentryproductleft))) /\ ((((((dc_right_g009_definitionleftentry) = 2 * (sto_bp_g009_definitionleftentryproduct) /\ (sto_bn_g009_definitionleftentryproduct) = 0) \/ exists ge_signed_half_g009_definitionleftentryproductright. (((dc_right_g009_definitionleftentry) = 2 * ge_signed_half_g009_definitionleftentryproductright + 1 /\ (sto_bp_g009_definitionleftentryproduct) = 0) /\ (sto_bn_g009_definitionleftentryproduct) = S ge_signed_half_g009_definitionleftentryproductright))) /\ ((((((dc_value_g009_definitionleft) = 2 * (sto_cp_g009_definitionleftentryproduct) /\ (sto_cn_g009_definitionleftentryproduct) = 0) \/ exists ge_signed_half_g009_definitionleftentryproductoutput. (((dc_value_g009_definitionleft) = 2 * ge_signed_half_g009_definitionleftentryproductoutput + 1 /\ (sto_cp_g009_definitionleftentryproduct) = 0) /\ (sto_cn_g009_definitionleftentryproduct) = S ge_signed_half_g009_definitionleftentryproductoutput))) /\ ((sto_ap_g009_definitionleftentryproduct * sto_bp_g009_definitionleftentryproduct + sto_an_g009_definitionleftentryproduct * sto_bn_g009_definitionleftentryproduct) + sto_cn_g009_definitionleftentryproduct = (sto_ap_g009_definitionleftentryproduct * sto_bn_g009_definitionleftentryproduct + sto_an_g009_definitionleftentryproduct * sto_bp_g009_definitionleftentryproduct) + sto_cp_g009_definitionleftentryproduct))))))))))))))) \/ ((((dc_index_g009_definitionleft)=0 \/ ~(exists pvs_factor_g009_definitionleftentrynondivisor. ((m)) = (dc_index_g009_definitionleft) * pvs_factor_g009_definitionleftentrynondivisor)) /\ ((dc_value_g009_definitionleft)=0))))))) /\ (((((exists dst_positive_code_g009_definitionrighttable dst_positive_scale_g009_definitionrighttable dst_negative_code_g009_definitionrighttable dst_negative_scale_g009_definitionrighttable. ((((B)) = (((((dst_positive_code_g009_definitionrighttable) + (dst_positive_scale_g009_definitionrighttable)) * S ((dst_positive_code_g009_definitionrighttable) + (dst_positive_scale_g009_definitionrighttable)) + ((dst_positive_scale_g009_definitionrighttable) + (dst_positive_scale_g009_definitionrighttable))) + (((dst_negative_code_g009_definitionrighttable) + (dst_negative_scale_g009_definitionrighttable)) * S ((dst_negative_code_g009_definitionrighttable) + (dst_negative_scale_g009_definitionrighttable)) + ((dst_negative_scale_g009_definitionrighttable) + (dst_negative_scale_g009_definitionrighttable)))) * S ((((dst_positive_code_g009_definitionrighttable) + (dst_positive_scale_g009_definitionrighttable)) * S ((dst_positive_code_g009_definitionrighttable) + (dst_positive_scale_g009_definitionrighttable)) + ((dst_positive_scale_g009_definitionrighttable) + (dst_positive_scale_g009_definitionrighttable))) + (((dst_negative_code_g009_definitionrighttable) + (dst_negative_scale_g009_definitionrighttable)) * S ((dst_negative_code_g009_definitionrighttable) + (dst_negative_scale_g009_definitionrighttable)) + ((dst_negative_scale_g009_definitionrighttable) + (dst_negative_scale_g009_definitionrighttable)))) + ((((dst_negative_code_g009_definitionrighttable) + (dst_negative_scale_g009_definitionrighttable)) * S ((dst_negative_code_g009_definitionrighttable) + (dst_negative_scale_g009_definitionrighttable)) + ((dst_negative_scale_g009_definitionrighttable) + (dst_negative_scale_g009_definitionrighttable))) + (((dst_negative_code_g009_definitionrighttable) + (dst_negative_scale_g009_definitionrighttable)) * S ((dst_negative_code_g009_definitionrighttable) + (dst_negative_scale_g009_definitionrighttable)) + ((dst_negative_scale_g009_definitionrighttable) + (dst_negative_scale_g009_definitionrighttable)))))) /\ (forall dst_index_g009_definitionrighttable. (exists pvs_le_gap_g009_definitionrighttabledomain. pvs_le_gap_g009_definitionrighttabledomain + (dst_index_g009_definitionrighttable) = ((n))) -> exists dst_positive_g009_definitionrighttable dst_negative_g009_definitionrighttable dst_value_g009_definitionrighttable. ((((exists ff_h_pvs_g009_definitionrighttableentrypositive. ff_h_pvs_g009_definitionrighttableentrypositive + S (dst_positive_g009_definitionrighttable) = S ((S (dst_index_g009_definitionrighttable)) * dst_positive_scale_g009_definitionrighttable)) /\ exists ff_q_pvs_g009_definitionrighttableentrypositive. dst_positive_code_g009_definitionrighttable = ff_q_pvs_g009_definitionrighttableentrypositive * S ((S (dst_index_g009_definitionrighttable)) * dst_positive_scale_g009_definitionrighttable) + (dst_positive_g009_definitionrighttable))) /\ (((((exists ff_h_pvs_g009_definitionrighttableentrynegative. ff_h_pvs_g009_definitionrighttableentrynegative + S (dst_negative_g009_definitionrighttable) = S ((S (dst_index_g009_definitionrighttable)) * dst_negative_scale_g009_definitionrighttable)) /\ exists ff_q_pvs_g009_definitionrighttableentrynegative. dst_negative_code_g009_definitionrighttable = ff_q_pvs_g009_definitionrighttableentrynegative * S ((S (dst_index_g009_definitionrighttable)) * dst_negative_scale_g009_definitionrighttable) + (dst_negative_g009_definitionrighttable))) /\ (exists ge_balance_positive_g009_definitionrighttableentryvalue ge_balance_negative_g009_definitionrighttableentryvalue. (((((dst_value_g009_definitionrighttable) = 2 * (ge_balance_positive_g009_definitionrighttableentryvalue) /\ (ge_balance_negative_g009_definitionrighttableentryvalue) = 0) \/ exists ge_signed_half_g009_definitionrighttableentryvaluedecode. (((dst_value_g009_definitionrighttable) = 2 * ge_signed_half_g009_definitionrighttableentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitionrighttableentryvalue) = 0) /\ (ge_balance_negative_g009_definitionrighttableentryvalue) = S ge_signed_half_g009_definitionrighttableentryvaluedecode))) /\ ((dst_positive_g009_definitionrighttable) + ge_balance_negative_g009_definitionrighttableentryvalue = (dst_negative_g009_definitionrighttable) + ge_balance_positive_g009_definitionrighttableentryvalue))))))))) /\ (forall dc_index_g009_definitionright dc_value_g009_definitionright. (exists pvs_le_gap_g009_definitionrightdomain. pvs_le_gap_g009_definitionrightdomain + (dc_index_g009_definitionright) = ((n))) -> (exists dst_positive_code_g009_definitionrightlookup dst_positive_scale_g009_definitionrightlookup dst_negative_code_g009_definitionrightlookup dst_negative_scale_g009_definitionrightlookup dst_positive_g009_definitionrightlookup dst_negative_g009_definitionrightlookup. ((((B)) = (((((dst_positive_code_g009_definitionrightlookup) + (dst_positive_scale_g009_definitionrightlookup)) * S ((dst_positive_code_g009_definitionrightlookup) + (dst_positive_scale_g009_definitionrightlookup)) + ((dst_positive_scale_g009_definitionrightlookup) + (dst_positive_scale_g009_definitionrightlookup))) + (((dst_negative_code_g009_definitionrightlookup) + (dst_negative_scale_g009_definitionrightlookup)) * S ((dst_negative_code_g009_definitionrightlookup) + (dst_negative_scale_g009_definitionrightlookup)) + ((dst_negative_scale_g009_definitionrightlookup) + (dst_negative_scale_g009_definitionrightlookup)))) * S ((((dst_positive_code_g009_definitionrightlookup) + (dst_positive_scale_g009_definitionrightlookup)) * S ((dst_positive_code_g009_definitionrightlookup) + (dst_positive_scale_g009_definitionrightlookup)) + ((dst_positive_scale_g009_definitionrightlookup) + (dst_positive_scale_g009_definitionrightlookup))) + (((dst_negative_code_g009_definitionrightlookup) + (dst_negative_scale_g009_definitionrightlookup)) * S ((dst_negative_code_g009_definitionrightlookup) + (dst_negative_scale_g009_definitionrightlookup)) + ((dst_negative_scale_g009_definitionrightlookup) + (dst_negative_scale_g009_definitionrightlookup)))) + ((((dst_negative_code_g009_definitionrightlookup) + (dst_negative_scale_g009_definitionrightlookup)) * S ((dst_negative_code_g009_definitionrightlookup) + (dst_negative_scale_g009_definitionrightlookup)) + ((dst_negative_scale_g009_definitionrightlookup) + (dst_negative_scale_g009_definitionrightlookup))) + (((dst_negative_code_g009_definitionrightlookup) + (dst_negative_scale_g009_definitionrightlookup)) * S ((dst_negative_code_g009_definitionrightlookup) + (dst_negative_scale_g009_definitionrightlookup)) + ((dst_negative_scale_g009_definitionrightlookup) + (dst_negative_scale_g009_definitionrightlookup)))))) /\ (((((exists ff_h_pvs_g009_definitionrightlookuppositive. ff_h_pvs_g009_definitionrightlookuppositive + S (dst_positive_g009_definitionrightlookup) = S ((S (dc_index_g009_definitionright)) * dst_positive_scale_g009_definitionrightlookup)) /\ exists ff_q_pvs_g009_definitionrightlookuppositive. dst_positive_code_g009_definitionrightlookup = ff_q_pvs_g009_definitionrightlookuppositive * S ((S (dc_index_g009_definitionright)) * dst_positive_scale_g009_definitionrightlookup) + (dst_positive_g009_definitionrightlookup))) /\ (((((exists ff_h_pvs_g009_definitionrightlookupnegative. ff_h_pvs_g009_definitionrightlookupnegative + S (dst_negative_g009_definitionrightlookup) = S ((S (dc_index_g009_definitionright)) * dst_negative_scale_g009_definitionrightlookup)) /\ exists ff_q_pvs_g009_definitionrightlookupnegative. dst_negative_code_g009_definitionrightlookup = ff_q_pvs_g009_definitionrightlookupnegative * S ((S (dc_index_g009_definitionright)) * dst_negative_scale_g009_definitionrightlookup) + (dst_negative_g009_definitionrightlookup))) /\ (exists ge_balance_positive_g009_definitionrightlookupvalue ge_balance_negative_g009_definitionrightlookupvalue. (((((dc_value_g009_definitionright) = 2 * (ge_balance_positive_g009_definitionrightlookupvalue) /\ (ge_balance_negative_g009_definitionrightlookupvalue) = 0) \/ exists ge_signed_half_g009_definitionrightlookupvaluedecode. (((dc_value_g009_definitionright) = 2 * ge_signed_half_g009_definitionrightlookupvaluedecode + 1 /\ (ge_balance_positive_g009_definitionrightlookupvalue) = 0) /\ (ge_balance_negative_g009_definitionrightlookupvalue) = S ge_signed_half_g009_definitionrightlookupvaluedecode))) /\ ((dst_positive_g009_definitionrightlookup) + ge_balance_negative_g009_definitionrightlookupvalue = (dst_negative_g009_definitionrightlookup) + ge_balance_positive_g009_definitionrightlookupvalue))))))))) -> ((((~((dc_index_g009_definitionright)=0)) /\ (exists dc_quotient_g009_definitionrightentry dc_left_g009_definitionrightentry dc_right_g009_definitionrightentry. ((((n))=(dc_index_g009_definitionright)*dc_quotient_g009_definitionrightentry) /\ (((exists dst_positive_code_g009_definitionrightentryleft dst_positive_scale_g009_definitionrightentryleft dst_negative_code_g009_definitionrightentryleft dst_negative_scale_g009_definitionrightentryleft dst_positive_g009_definitionrightentryleft dst_negative_g009_definitionrightentryleft. ((((F)) = (((((dst_positive_code_g009_definitionrightentryleft) + (dst_positive_scale_g009_definitionrightentryleft)) * S ((dst_positive_code_g009_definitionrightentryleft) + (dst_positive_scale_g009_definitionrightentryleft)) + ((dst_positive_scale_g009_definitionrightentryleft) + (dst_positive_scale_g009_definitionrightentryleft))) + (((dst_negative_code_g009_definitionrightentryleft) + (dst_negative_scale_g009_definitionrightentryleft)) * S ((dst_negative_code_g009_definitionrightentryleft) + (dst_negative_scale_g009_definitionrightentryleft)) + ((dst_negative_scale_g009_definitionrightentryleft) + (dst_negative_scale_g009_definitionrightentryleft)))) * S ((((dst_positive_code_g009_definitionrightentryleft) + (dst_positive_scale_g009_definitionrightentryleft)) * S ((dst_positive_code_g009_definitionrightentryleft) + (dst_positive_scale_g009_definitionrightentryleft)) + ((dst_positive_scale_g009_definitionrightentryleft) + (dst_positive_scale_g009_definitionrightentryleft))) + (((dst_negative_code_g009_definitionrightentryleft) + (dst_negative_scale_g009_definitionrightentryleft)) * S ((dst_negative_code_g009_definitionrightentryleft) + (dst_negative_scale_g009_definitionrightentryleft)) + ((dst_negative_scale_g009_definitionrightentryleft) + (dst_negative_scale_g009_definitionrightentryleft)))) + ((((dst_negative_code_g009_definitionrightentryleft) + (dst_negative_scale_g009_definitionrightentryleft)) * S ((dst_negative_code_g009_definitionrightentryleft) + (dst_negative_scale_g009_definitionrightentryleft)) + ((dst_negative_scale_g009_definitionrightentryleft) + (dst_negative_scale_g009_definitionrightentryleft))) + (((dst_negative_code_g009_definitionrightentryleft) + (dst_negative_scale_g009_definitionrightentryleft)) * S ((dst_negative_code_g009_definitionrightentryleft) + (dst_negative_scale_g009_definitionrightentryleft)) + ((dst_negative_scale_g009_definitionrightentryleft) + (dst_negative_scale_g009_definitionrightentryleft)))))) /\ (((((exists ff_h_pvs_g009_definitionrightentryleftpositive. ff_h_pvs_g009_definitionrightentryleftpositive + S (dst_positive_g009_definitionrightentryleft) = S ((S (dc_index_g009_definitionright)) * dst_positive_scale_g009_definitionrightentryleft)) /\ exists ff_q_pvs_g009_definitionrightentryleftpositive. dst_positive_code_g009_definitionrightentryleft = ff_q_pvs_g009_definitionrightentryleftpositive * S ((S (dc_index_g009_definitionright)) * dst_positive_scale_g009_definitionrightentryleft) + (dst_positive_g009_definitionrightentryleft))) /\ (((((exists ff_h_pvs_g009_definitionrightentryleftnegative. ff_h_pvs_g009_definitionrightentryleftnegative + S (dst_negative_g009_definitionrightentryleft) = S ((S (dc_index_g009_definitionright)) * dst_negative_scale_g009_definitionrightentryleft)) /\ exists ff_q_pvs_g009_definitionrightentryleftnegative. dst_negative_code_g009_definitionrightentryleft = ff_q_pvs_g009_definitionrightentryleftnegative * S ((S (dc_index_g009_definitionright)) * dst_negative_scale_g009_definitionrightentryleft) + (dst_negative_g009_definitionrightentryleft))) /\ (exists ge_balance_positive_g009_definitionrightentryleftvalue ge_balance_negative_g009_definitionrightentryleftvalue. (((((dc_left_g009_definitionrightentry) = 2 * (ge_balance_positive_g009_definitionrightentryleftvalue) /\ (ge_balance_negative_g009_definitionrightentryleftvalue) = 0) \/ exists ge_signed_half_g009_definitionrightentryleftvaluedecode. (((dc_left_g009_definitionrightentry) = 2 * ge_signed_half_g009_definitionrightentryleftvaluedecode + 1 /\ (ge_balance_positive_g009_definitionrightentryleftvalue) = 0) /\ (ge_balance_negative_g009_definitionrightentryleftvalue) = S ge_signed_half_g009_definitionrightentryleftvaluedecode))) /\ ((dst_positive_g009_definitionrightentryleft) + ge_balance_negative_g009_definitionrightentryleftvalue = (dst_negative_g009_definitionrightentryleft) + ge_balance_positive_g009_definitionrightentryleftvalue))))))))) /\ (((exists dst_positive_code_g009_definitionrightentryright dst_positive_scale_g009_definitionrightentryright dst_negative_code_g009_definitionrightentryright dst_negative_scale_g009_definitionrightentryright dst_positive_g009_definitionrightentryright dst_negative_g009_definitionrightentryright. ((((G)) = (((((dst_positive_code_g009_definitionrightentryright) + (dst_positive_scale_g009_definitionrightentryright)) * S ((dst_positive_code_g009_definitionrightentryright) + (dst_positive_scale_g009_definitionrightentryright)) + ((dst_positive_scale_g009_definitionrightentryright) + (dst_positive_scale_g009_definitionrightentryright))) + (((dst_negative_code_g009_definitionrightentryright) + (dst_negative_scale_g009_definitionrightentryright)) * S ((dst_negative_code_g009_definitionrightentryright) + (dst_negative_scale_g009_definitionrightentryright)) + ((dst_negative_scale_g009_definitionrightentryright) + (dst_negative_scale_g009_definitionrightentryright)))) * S ((((dst_positive_code_g009_definitionrightentryright) + (dst_positive_scale_g009_definitionrightentryright)) * S ((dst_positive_code_g009_definitionrightentryright) + (dst_positive_scale_g009_definitionrightentryright)) + ((dst_positive_scale_g009_definitionrightentryright) + (dst_positive_scale_g009_definitionrightentryright))) + (((dst_negative_code_g009_definitionrightentryright) + (dst_negative_scale_g009_definitionrightentryright)) * S ((dst_negative_code_g009_definitionrightentryright) + (dst_negative_scale_g009_definitionrightentryright)) + ((dst_negative_scale_g009_definitionrightentryright) + (dst_negative_scale_g009_definitionrightentryright)))) + ((((dst_negative_code_g009_definitionrightentryright) + (dst_negative_scale_g009_definitionrightentryright)) * S ((dst_negative_code_g009_definitionrightentryright) + (dst_negative_scale_g009_definitionrightentryright)) + ((dst_negative_scale_g009_definitionrightentryright) + (dst_negative_scale_g009_definitionrightentryright))) + (((dst_negative_code_g009_definitionrightentryright) + (dst_negative_scale_g009_definitionrightentryright)) * S ((dst_negative_code_g009_definitionrightentryright) + (dst_negative_scale_g009_definitionrightentryright)) + ((dst_negative_scale_g009_definitionrightentryright) + (dst_negative_scale_g009_definitionrightentryright)))))) /\ (((((exists ff_h_pvs_g009_definitionrightentryrightpositive. ff_h_pvs_g009_definitionrightentryrightpositive + S (dst_positive_g009_definitionrightentryright) = S ((S (dc_quotient_g009_definitionrightentry)) * dst_positive_scale_g009_definitionrightentryright)) /\ exists ff_q_pvs_g009_definitionrightentryrightpositive. dst_positive_code_g009_definitionrightentryright = ff_q_pvs_g009_definitionrightentryrightpositive * S ((S (dc_quotient_g009_definitionrightentry)) * dst_positive_scale_g009_definitionrightentryright) + (dst_positive_g009_definitionrightentryright))) /\ (((((exists ff_h_pvs_g009_definitionrightentryrightnegative. ff_h_pvs_g009_definitionrightentryrightnegative + S (dst_negative_g009_definitionrightentryright) = S ((S (dc_quotient_g009_definitionrightentry)) * dst_negative_scale_g009_definitionrightentryright)) /\ exists ff_q_pvs_g009_definitionrightentryrightnegative. dst_negative_code_g009_definitionrightentryright = ff_q_pvs_g009_definitionrightentryrightnegative * S ((S (dc_quotient_g009_definitionrightentry)) * dst_negative_scale_g009_definitionrightentryright) + (dst_negative_g009_definitionrightentryright))) /\ (exists ge_balance_positive_g009_definitionrightentryrightvalue ge_balance_negative_g009_definitionrightentryrightvalue. (((((dc_right_g009_definitionrightentry) = 2 * (ge_balance_positive_g009_definitionrightentryrightvalue) /\ (ge_balance_negative_g009_definitionrightentryrightvalue) = 0) \/ exists ge_signed_half_g009_definitionrightentryrightvaluedecode. (((dc_right_g009_definitionrightentry) = 2 * ge_signed_half_g009_definitionrightentryrightvaluedecode + 1 /\ (ge_balance_positive_g009_definitionrightentryrightvalue) = 0) /\ (ge_balance_negative_g009_definitionrightentryrightvalue) = S ge_signed_half_g009_definitionrightentryrightvaluedecode))) /\ ((dst_positive_g009_definitionrightentryright) + ge_balance_negative_g009_definitionrightentryrightvalue = (dst_negative_g009_definitionrightentryright) + ge_balance_positive_g009_definitionrightentryrightvalue))))))))) /\ (exists sto_ap_g009_definitionrightentryproduct sto_an_g009_definitionrightentryproduct sto_bp_g009_definitionrightentryproduct sto_bn_g009_definitionrightentryproduct sto_cp_g009_definitionrightentryproduct sto_cn_g009_definitionrightentryproduct. (((((dc_left_g009_definitionrightentry) = 2 * (sto_ap_g009_definitionrightentryproduct) /\ (sto_an_g009_definitionrightentryproduct) = 0) \/ exists ge_signed_half_g009_definitionrightentryproductleft. (((dc_left_g009_definitionrightentry) = 2 * ge_signed_half_g009_definitionrightentryproductleft + 1 /\ (sto_ap_g009_definitionrightentryproduct) = 0) /\ (sto_an_g009_definitionrightentryproduct) = S ge_signed_half_g009_definitionrightentryproductleft))) /\ ((((((dc_right_g009_definitionrightentry) = 2 * (sto_bp_g009_definitionrightentryproduct) /\ (sto_bn_g009_definitionrightentryproduct) = 0) \/ exists ge_signed_half_g009_definitionrightentryproductright. (((dc_right_g009_definitionrightentry) = 2 * ge_signed_half_g009_definitionrightentryproductright + 1 /\ (sto_bp_g009_definitionrightentryproduct) = 0) /\ (sto_bn_g009_definitionrightentryproduct) = S ge_signed_half_g009_definitionrightentryproductright))) /\ ((((((dc_value_g009_definitionright) = 2 * (sto_cp_g009_definitionrightentryproduct) /\ (sto_cn_g009_definitionrightentryproduct) = 0) \/ exists ge_signed_half_g009_definitionrightentryproductoutput. (((dc_value_g009_definitionright) = 2 * ge_signed_half_g009_definitionrightentryproductoutput + 1 /\ (sto_cp_g009_definitionrightentryproduct) = 0) /\ (sto_cn_g009_definitionrightentryproduct) = S ge_signed_half_g009_definitionrightentryproductoutput))) /\ ((sto_ap_g009_definitionrightentryproduct * sto_bp_g009_definitionrightentryproduct + sto_an_g009_definitionrightentryproduct * sto_bn_g009_definitionrightentryproduct) + sto_cn_g009_definitionrightentryproduct = (sto_ap_g009_definitionrightentryproduct * sto_bn_g009_definitionrightentryproduct + sto_an_g009_definitionrightentryproduct * sto_bp_g009_definitionrightentryproduct) + sto_cp_g009_definitionrightentryproduct))))))))))))))) \/ ((((dc_index_g009_definitionright)=0 \/ ~(exists pvs_factor_g009_definitionrightentrynondivisor. ((n)) = (dc_index_g009_definitionright) * pvs_factor_g009_definitionrightentrynondivisor)) /\ ((dc_value_g009_definitionright)=0))))))) /\ (((((exists dst_positive_code_g009_definitioncartesianF dst_positive_scale_g009_definitioncartesianF dst_negative_code_g009_definitioncartesianF dst_negative_scale_g009_definitioncartesianF. ((((A)) = (((((dst_positive_code_g009_definitioncartesianF) + (dst_positive_scale_g009_definitioncartesianF)) * S ((dst_positive_code_g009_definitioncartesianF) + (dst_positive_scale_g009_definitioncartesianF)) + ((dst_positive_scale_g009_definitioncartesianF) + (dst_positive_scale_g009_definitioncartesianF))) + (((dst_negative_code_g009_definitioncartesianF) + (dst_negative_scale_g009_definitioncartesianF)) * S ((dst_negative_code_g009_definitioncartesianF) + (dst_negative_scale_g009_definitioncartesianF)) + ((dst_negative_scale_g009_definitioncartesianF) + (dst_negative_scale_g009_definitioncartesianF)))) * S ((((dst_positive_code_g009_definitioncartesianF) + (dst_positive_scale_g009_definitioncartesianF)) * S ((dst_positive_code_g009_definitioncartesianF) + (dst_positive_scale_g009_definitioncartesianF)) + ((dst_positive_scale_g009_definitioncartesianF) + (dst_positive_scale_g009_definitioncartesianF))) + (((dst_negative_code_g009_definitioncartesianF) + (dst_negative_scale_g009_definitioncartesianF)) * S ((dst_negative_code_g009_definitioncartesianF) + (dst_negative_scale_g009_definitioncartesianF)) + ((dst_negative_scale_g009_definitioncartesianF) + (dst_negative_scale_g009_definitioncartesianF)))) + ((((dst_negative_code_g009_definitioncartesianF) + (dst_negative_scale_g009_definitioncartesianF)) * S ((dst_negative_code_g009_definitioncartesianF) + (dst_negative_scale_g009_definitioncartesianF)) + ((dst_negative_scale_g009_definitioncartesianF) + (dst_negative_scale_g009_definitioncartesianF))) + (((dst_negative_code_g009_definitioncartesianF) + (dst_negative_scale_g009_definitioncartesianF)) * S ((dst_negative_code_g009_definitioncartesianF) + (dst_negative_scale_g009_definitioncartesianF)) + ((dst_negative_scale_g009_definitioncartesianF) + (dst_negative_scale_g009_definitioncartesianF)))))) /\ (forall dst_index_g009_definitioncartesianF. (exists pvs_le_gap_g009_definitioncartesianFdomain. pvs_le_gap_g009_definitioncartesianFdomain + (dst_index_g009_definitioncartesianF) = (0)) -> exists dst_positive_g009_definitioncartesianF dst_negative_g009_definitioncartesianF dst_value_g009_definitioncartesianF. ((((exists ff_h_pvs_g009_definitioncartesianFentrypositive. ff_h_pvs_g009_definitioncartesianFentrypositive + S (dst_positive_g009_definitioncartesianF) = S ((S (dst_index_g009_definitioncartesianF)) * dst_positive_scale_g009_definitioncartesianF)) /\ exists ff_q_pvs_g009_definitioncartesianFentrypositive. dst_positive_code_g009_definitioncartesianF = ff_q_pvs_g009_definitioncartesianFentrypositive * S ((S (dst_index_g009_definitioncartesianF)) * dst_positive_scale_g009_definitioncartesianF) + (dst_positive_g009_definitioncartesianF))) /\ (((((exists ff_h_pvs_g009_definitioncartesianFentrynegative. ff_h_pvs_g009_definitioncartesianFentrynegative + S (dst_negative_g009_definitioncartesianF) = S ((S (dst_index_g009_definitioncartesianF)) * dst_negative_scale_g009_definitioncartesianF)) /\ exists ff_q_pvs_g009_definitioncartesianFentrynegative. dst_negative_code_g009_definitioncartesianF = ff_q_pvs_g009_definitioncartesianFentrynegative * S ((S (dst_index_g009_definitioncartesianF)) * dst_negative_scale_g009_definitioncartesianF) + (dst_negative_g009_definitioncartesianF))) /\ (exists ge_balance_positive_g009_definitioncartesianFentryvalue ge_balance_negative_g009_definitioncartesianFentryvalue. (((((dst_value_g009_definitioncartesianF) = 2 * (ge_balance_positive_g009_definitioncartesianFentryvalue) /\ (ge_balance_negative_g009_definitioncartesianFentryvalue) = 0) \/ exists ge_signed_half_g009_definitioncartesianFentryvaluedecode. (((dst_value_g009_definitioncartesianF) = 2 * ge_signed_half_g009_definitioncartesianFentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitioncartesianFentryvalue) = 0) /\ (ge_balance_negative_g009_definitioncartesianFentryvalue) = S ge_signed_half_g009_definitioncartesianFentryvaluedecode))) /\ ((dst_positive_g009_definitioncartesianF) + ge_balance_negative_g009_definitioncartesianFentryvalue = (dst_negative_g009_definitioncartesianF) + ge_balance_positive_g009_definitioncartesianFentryvalue))))))))) /\ (((exists dst_positive_code_g009_definitioncartesianG dst_positive_scale_g009_definitioncartesianG dst_negative_code_g009_definitioncartesianG dst_negative_scale_g009_definitioncartesianG. ((((B)) = (((((dst_positive_code_g009_definitioncartesianG) + (dst_positive_scale_g009_definitioncartesianG)) * S ((dst_positive_code_g009_definitioncartesianG) + (dst_positive_scale_g009_definitioncartesianG)) + ((dst_positive_scale_g009_definitioncartesianG) + (dst_positive_scale_g009_definitioncartesianG))) + (((dst_negative_code_g009_definitioncartesianG) + (dst_negative_scale_g009_definitioncartesianG)) * S ((dst_negative_code_g009_definitioncartesianG) + (dst_negative_scale_g009_definitioncartesianG)) + ((dst_negative_scale_g009_definitioncartesianG) + (dst_negative_scale_g009_definitioncartesianG)))) * S ((((dst_positive_code_g009_definitioncartesianG) + (dst_positive_scale_g009_definitioncartesianG)) * S ((dst_positive_code_g009_definitioncartesianG) + (dst_positive_scale_g009_definitioncartesianG)) + ((dst_positive_scale_g009_definitioncartesianG) + (dst_positive_scale_g009_definitioncartesianG))) + (((dst_negative_code_g009_definitioncartesianG) + (dst_negative_scale_g009_definitioncartesianG)) * S ((dst_negative_code_g009_definitioncartesianG) + (dst_negative_scale_g009_definitioncartesianG)) + ((dst_negative_scale_g009_definitioncartesianG) + (dst_negative_scale_g009_definitioncartesianG)))) + ((((dst_negative_code_g009_definitioncartesianG) + (dst_negative_scale_g009_definitioncartesianG)) * S ((dst_negative_code_g009_definitioncartesianG) + (dst_negative_scale_g009_definitioncartesianG)) + ((dst_negative_scale_g009_definitioncartesianG) + (dst_negative_scale_g009_definitioncartesianG))) + (((dst_negative_code_g009_definitioncartesianG) + (dst_negative_scale_g009_definitioncartesianG)) * S ((dst_negative_code_g009_definitioncartesianG) + (dst_negative_scale_g009_definitioncartesianG)) + ((dst_negative_scale_g009_definitioncartesianG) + (dst_negative_scale_g009_definitioncartesianG)))))) /\ (forall dst_index_g009_definitioncartesianG. (exists pvs_le_gap_g009_definitioncartesianGdomain. pvs_le_gap_g009_definitioncartesianGdomain + (dst_index_g009_definitioncartesianG) = (0)) -> exists dst_positive_g009_definitioncartesianG dst_negative_g009_definitioncartesianG dst_value_g009_definitioncartesianG. ((((exists ff_h_pvs_g009_definitioncartesianGentrypositive. ff_h_pvs_g009_definitioncartesianGentrypositive + S (dst_positive_g009_definitioncartesianG) = S ((S (dst_index_g009_definitioncartesianG)) * dst_positive_scale_g009_definitioncartesianG)) /\ exists ff_q_pvs_g009_definitioncartesianGentrypositive. dst_positive_code_g009_definitioncartesianG = ff_q_pvs_g009_definitioncartesianGentrypositive * S ((S (dst_index_g009_definitioncartesianG)) * dst_positive_scale_g009_definitioncartesianG) + (dst_positive_g009_definitioncartesianG))) /\ (((((exists ff_h_pvs_g009_definitioncartesianGentrynegative. ff_h_pvs_g009_definitioncartesianGentrynegative + S (dst_negative_g009_definitioncartesianG) = S ((S (dst_index_g009_definitioncartesianG)) * dst_negative_scale_g009_definitioncartesianG)) /\ exists ff_q_pvs_g009_definitioncartesianGentrynegative. dst_negative_code_g009_definitioncartesianG = ff_q_pvs_g009_definitioncartesianGentrynegative * S ((S (dst_index_g009_definitioncartesianG)) * dst_negative_scale_g009_definitioncartesianG) + (dst_negative_g009_definitioncartesianG))) /\ (exists ge_balance_positive_g009_definitioncartesianGentryvalue ge_balance_negative_g009_definitioncartesianGentryvalue. (((((dst_value_g009_definitioncartesianG) = 2 * (ge_balance_positive_g009_definitioncartesianGentryvalue) /\ (ge_balance_negative_g009_definitioncartesianGentryvalue) = 0) \/ exists ge_signed_half_g009_definitioncartesianGentryvaluedecode. (((dst_value_g009_definitioncartesianG) = 2 * ge_signed_half_g009_definitioncartesianGentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitioncartesianGentryvalue) = 0) /\ (ge_balance_negative_g009_definitioncartesianGentryvalue) = S ge_signed_half_g009_definitioncartesianGentryvaluedecode))) /\ ((dst_positive_g009_definitioncartesianG) + ge_balance_negative_g009_definitioncartesianGentryvalue = (dst_negative_g009_definitioncartesianG) + ge_balance_positive_g009_definitioncartesianGentryvalue))))))))) /\ (((exists dst_positive_code_g009_definitioncartesianT dst_positive_scale_g009_definitioncartesianT dst_negative_code_g009_definitioncartesianT dst_negative_scale_g009_definitioncartesianT. ((((T)) = (((((dst_positive_code_g009_definitioncartesianT) + (dst_positive_scale_g009_definitioncartesianT)) * S ((dst_positive_code_g009_definitioncartesianT) + (dst_positive_scale_g009_definitioncartesianT)) + ((dst_positive_scale_g009_definitioncartesianT) + (dst_positive_scale_g009_definitioncartesianT))) + (((dst_negative_code_g009_definitioncartesianT) + (dst_negative_scale_g009_definitioncartesianT)) * S ((dst_negative_code_g009_definitioncartesianT) + (dst_negative_scale_g009_definitioncartesianT)) + ((dst_negative_scale_g009_definitioncartesianT) + (dst_negative_scale_g009_definitioncartesianT)))) * S ((((dst_positive_code_g009_definitioncartesianT) + (dst_positive_scale_g009_definitioncartesianT)) * S ((dst_positive_code_g009_definitioncartesianT) + (dst_positive_scale_g009_definitioncartesianT)) + ((dst_positive_scale_g009_definitioncartesianT) + (dst_positive_scale_g009_definitioncartesianT))) + (((dst_negative_code_g009_definitioncartesianT) + (dst_negative_scale_g009_definitioncartesianT)) * S ((dst_negative_code_g009_definitioncartesianT) + (dst_negative_scale_g009_definitioncartesianT)) + ((dst_negative_scale_g009_definitioncartesianT) + (dst_negative_scale_g009_definitioncartesianT)))) + ((((dst_negative_code_g009_definitioncartesianT) + (dst_negative_scale_g009_definitioncartesianT)) * S ((dst_negative_code_g009_definitioncartesianT) + (dst_negative_scale_g009_definitioncartesianT)) + ((dst_negative_scale_g009_definitioncartesianT) + (dst_negative_scale_g009_definitioncartesianT))) + (((dst_negative_code_g009_definitioncartesianT) + (dst_negative_scale_g009_definitioncartesianT)) * S ((dst_negative_code_g009_definitioncartesianT) + (dst_negative_scale_g009_definitioncartesianT)) + ((dst_negative_scale_g009_definitioncartesianT) + (dst_negative_scale_g009_definitioncartesianT)))))) /\ (forall dst_index_g009_definitioncartesianT. (exists pvs_le_gap_g009_definitioncartesianTdomain. pvs_le_gap_g009_definitioncartesianTdomain + (dst_index_g009_definitioncartesianT) = ((S ((m)))*(S ((n))))) -> exists dst_positive_g009_definitioncartesianT dst_negative_g009_definitioncartesianT dst_value_g009_definitioncartesianT. ((((exists ff_h_pvs_g009_definitioncartesianTentrypositive. ff_h_pvs_g009_definitioncartesianTentrypositive + S (dst_positive_g009_definitioncartesianT) = S ((S (dst_index_g009_definitioncartesianT)) * dst_positive_scale_g009_definitioncartesianT)) /\ exists ff_q_pvs_g009_definitioncartesianTentrypositive. dst_positive_code_g009_definitioncartesianT = ff_q_pvs_g009_definitioncartesianTentrypositive * S ((S (dst_index_g009_definitioncartesianT)) * dst_positive_scale_g009_definitioncartesianT) + (dst_positive_g009_definitioncartesianT))) /\ (((((exists ff_h_pvs_g009_definitioncartesianTentrynegative. ff_h_pvs_g009_definitioncartesianTentrynegative + S (dst_negative_g009_definitioncartesianT) = S ((S (dst_index_g009_definitioncartesianT)) * dst_negative_scale_g009_definitioncartesianT)) /\ exists ff_q_pvs_g009_definitioncartesianTentrynegative. dst_negative_code_g009_definitioncartesianT = ff_q_pvs_g009_definitioncartesianTentrynegative * S ((S (dst_index_g009_definitioncartesianT)) * dst_negative_scale_g009_definitioncartesianT) + (dst_negative_g009_definitioncartesianT))) /\ (exists ge_balance_positive_g009_definitioncartesianTentryvalue ge_balance_negative_g009_definitioncartesianTentryvalue. (((((dst_value_g009_definitioncartesianT) = 2 * (ge_balance_positive_g009_definitioncartesianTentryvalue) /\ (ge_balance_negative_g009_definitioncartesianTentryvalue) = 0) \/ exists ge_signed_half_g009_definitioncartesianTentryvaluedecode. (((dst_value_g009_definitioncartesianT) = 2 * ge_signed_half_g009_definitioncartesianTentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitioncartesianTentryvalue) = 0) /\ (ge_balance_negative_g009_definitioncartesianTentryvalue) = S ge_signed_half_g009_definitioncartesianTentryvaluedecode))) /\ ((dst_positive_g009_definitioncartesianT) + ge_balance_negative_g009_definitioncartesianTentryvalue = (dst_negative_g009_definitioncartesianT) + ge_balance_positive_g009_definitioncartesianTentryvalue))))))))) /\ (forall scp_row_g009_definitioncartesian scp_column_g009_definitioncartesian scp_first_g009_definitioncartesian scp_second_g009_definitioncartesian scp_value_g009_definitioncartesian. (exists pvs_gap_g009_definitioncartesianrows. pvs_gap_g009_definitioncartesianrows + S (scp_row_g009_definitioncartesian) = (S ((m)))) -> (exists pvs_gap_g009_definitioncartesiancolumns. pvs_gap_g009_definitioncartesiancolumns + S (scp_column_g009_definitioncartesian) = (S ((n)))) -> (exists dst_positive_code_g009_definitioncartesianfirst dst_positive_scale_g009_definitioncartesianfirst dst_negative_code_g009_definitioncartesianfirst dst_negative_scale_g009_definitioncartesianfirst dst_positive_g009_definitioncartesianfirst dst_negative_g009_definitioncartesianfirst. ((((A)) = (((((dst_positive_code_g009_definitioncartesianfirst) + (dst_positive_scale_g009_definitioncartesianfirst)) * S ((dst_positive_code_g009_definitioncartesianfirst) + (dst_positive_scale_g009_definitioncartesianfirst)) + ((dst_positive_scale_g009_definitioncartesianfirst) + (dst_positive_scale_g009_definitioncartesianfirst))) + (((dst_negative_code_g009_definitioncartesianfirst) + (dst_negative_scale_g009_definitioncartesianfirst)) * S ((dst_negative_code_g009_definitioncartesianfirst) + (dst_negative_scale_g009_definitioncartesianfirst)) + ((dst_negative_scale_g009_definitioncartesianfirst) + (dst_negative_scale_g009_definitioncartesianfirst)))) * S ((((dst_positive_code_g009_definitioncartesianfirst) + (dst_positive_scale_g009_definitioncartesianfirst)) * S ((dst_positive_code_g009_definitioncartesianfirst) + (dst_positive_scale_g009_definitioncartesianfirst)) + ((dst_positive_scale_g009_definitioncartesianfirst) + (dst_positive_scale_g009_definitioncartesianfirst))) + (((dst_negative_code_g009_definitioncartesianfirst) + (dst_negative_scale_g009_definitioncartesianfirst)) * S ((dst_negative_code_g009_definitioncartesianfirst) + (dst_negative_scale_g009_definitioncartesianfirst)) + ((dst_negative_scale_g009_definitioncartesianfirst) + (dst_negative_scale_g009_definitioncartesianfirst)))) + ((((dst_negative_code_g009_definitioncartesianfirst) + (dst_negative_scale_g009_definitioncartesianfirst)) * S ((dst_negative_code_g009_definitioncartesianfirst) + (dst_negative_scale_g009_definitioncartesianfirst)) + ((dst_negative_scale_g009_definitioncartesianfirst) + (dst_negative_scale_g009_definitioncartesianfirst))) + (((dst_negative_code_g009_definitioncartesianfirst) + (dst_negative_scale_g009_definitioncartesianfirst)) * S ((dst_negative_code_g009_definitioncartesianfirst) + (dst_negative_scale_g009_definitioncartesianfirst)) + ((dst_negative_scale_g009_definitioncartesianfirst) + (dst_negative_scale_g009_definitioncartesianfirst)))))) /\ (((((exists ff_h_pvs_g009_definitioncartesianfirstpositive. ff_h_pvs_g009_definitioncartesianfirstpositive + S (dst_positive_g009_definitioncartesianfirst) = S ((S (scp_row_g009_definitioncartesian)) * dst_positive_scale_g009_definitioncartesianfirst)) /\ exists ff_q_pvs_g009_definitioncartesianfirstpositive. dst_positive_code_g009_definitioncartesianfirst = ff_q_pvs_g009_definitioncartesianfirstpositive * S ((S (scp_row_g009_definitioncartesian)) * dst_positive_scale_g009_definitioncartesianfirst) + (dst_positive_g009_definitioncartesianfirst))) /\ (((((exists ff_h_pvs_g009_definitioncartesianfirstnegative. ff_h_pvs_g009_definitioncartesianfirstnegative + S (dst_negative_g009_definitioncartesianfirst) = S ((S (scp_row_g009_definitioncartesian)) * dst_negative_scale_g009_definitioncartesianfirst)) /\ exists ff_q_pvs_g009_definitioncartesianfirstnegative. dst_negative_code_g009_definitioncartesianfirst = ff_q_pvs_g009_definitioncartesianfirstnegative * S ((S (scp_row_g009_definitioncartesian)) * dst_negative_scale_g009_definitioncartesianfirst) + (dst_negative_g009_definitioncartesianfirst))) /\ (exists ge_balance_positive_g009_definitioncartesianfirstvalue ge_balance_negative_g009_definitioncartesianfirstvalue. (((((scp_first_g009_definitioncartesian) = 2 * (ge_balance_positive_g009_definitioncartesianfirstvalue) /\ (ge_balance_negative_g009_definitioncartesianfirstvalue) = 0) \/ exists ge_signed_half_g009_definitioncartesianfirstvaluedecode. (((scp_first_g009_definitioncartesian) = 2 * ge_signed_half_g009_definitioncartesianfirstvaluedecode + 1 /\ (ge_balance_positive_g009_definitioncartesianfirstvalue) = 0) /\ (ge_balance_negative_g009_definitioncartesianfirstvalue) = S ge_signed_half_g009_definitioncartesianfirstvaluedecode))) /\ ((dst_positive_g009_definitioncartesianfirst) + ge_balance_negative_g009_definitioncartesianfirstvalue = (dst_negative_g009_definitioncartesianfirst) + ge_balance_positive_g009_definitioncartesianfirstvalue))))))))) -> (exists dst_positive_code_g009_definitioncartesiansecond dst_positive_scale_g009_definitioncartesiansecond dst_negative_code_g009_definitioncartesiansecond dst_negative_scale_g009_definitioncartesiansecond dst_positive_g009_definitioncartesiansecond dst_negative_g009_definitioncartesiansecond. ((((B)) = (((((dst_positive_code_g009_definitioncartesiansecond) + (dst_positive_scale_g009_definitioncartesiansecond)) * S ((dst_positive_code_g009_definitioncartesiansecond) + (dst_positive_scale_g009_definitioncartesiansecond)) + ((dst_positive_scale_g009_definitioncartesiansecond) + (dst_positive_scale_g009_definitioncartesiansecond))) + (((dst_negative_code_g009_definitioncartesiansecond) + (dst_negative_scale_g009_definitioncartesiansecond)) * S ((dst_negative_code_g009_definitioncartesiansecond) + (dst_negative_scale_g009_definitioncartesiansecond)) + ((dst_negative_scale_g009_definitioncartesiansecond) + (dst_negative_scale_g009_definitioncartesiansecond)))) * S ((((dst_positive_code_g009_definitioncartesiansecond) + (dst_positive_scale_g009_definitioncartesiansecond)) * S ((dst_positive_code_g009_definitioncartesiansecond) + (dst_positive_scale_g009_definitioncartesiansecond)) + ((dst_positive_scale_g009_definitioncartesiansecond) + (dst_positive_scale_g009_definitioncartesiansecond))) + (((dst_negative_code_g009_definitioncartesiansecond) + (dst_negative_scale_g009_definitioncartesiansecond)) * S ((dst_negative_code_g009_definitioncartesiansecond) + (dst_negative_scale_g009_definitioncartesiansecond)) + ((dst_negative_scale_g009_definitioncartesiansecond) + (dst_negative_scale_g009_definitioncartesiansecond)))) + ((((dst_negative_code_g009_definitioncartesiansecond) + (dst_negative_scale_g009_definitioncartesiansecond)) * S ((dst_negative_code_g009_definitioncartesiansecond) + (dst_negative_scale_g009_definitioncartesiansecond)) + ((dst_negative_scale_g009_definitioncartesiansecond) + (dst_negative_scale_g009_definitioncartesiansecond))) + (((dst_negative_code_g009_definitioncartesiansecond) + (dst_negative_scale_g009_definitioncartesiansecond)) * S ((dst_negative_code_g009_definitioncartesiansecond) + (dst_negative_scale_g009_definitioncartesiansecond)) + ((dst_negative_scale_g009_definitioncartesiansecond) + (dst_negative_scale_g009_definitioncartesiansecond)))))) /\ (((((exists ff_h_pvs_g009_definitioncartesiansecondpositive. ff_h_pvs_g009_definitioncartesiansecondpositive + S (dst_positive_g009_definitioncartesiansecond) = S ((S (scp_column_g009_definitioncartesian)) * dst_positive_scale_g009_definitioncartesiansecond)) /\ exists ff_q_pvs_g009_definitioncartesiansecondpositive. dst_positive_code_g009_definitioncartesiansecond = ff_q_pvs_g009_definitioncartesiansecondpositive * S ((S (scp_column_g009_definitioncartesian)) * dst_positive_scale_g009_definitioncartesiansecond) + (dst_positive_g009_definitioncartesiansecond))) /\ (((((exists ff_h_pvs_g009_definitioncartesiansecondnegative. ff_h_pvs_g009_definitioncartesiansecondnegative + S (dst_negative_g009_definitioncartesiansecond) = S ((S (scp_column_g009_definitioncartesian)) * dst_negative_scale_g009_definitioncartesiansecond)) /\ exists ff_q_pvs_g009_definitioncartesiansecondnegative. dst_negative_code_g009_definitioncartesiansecond = ff_q_pvs_g009_definitioncartesiansecondnegative * S ((S (scp_column_g009_definitioncartesian)) * dst_negative_scale_g009_definitioncartesiansecond) + (dst_negative_g009_definitioncartesiansecond))) /\ (exists ge_balance_positive_g009_definitioncartesiansecondvalue ge_balance_negative_g009_definitioncartesiansecondvalue. (((((scp_second_g009_definitioncartesian) = 2 * (ge_balance_positive_g009_definitioncartesiansecondvalue) /\ (ge_balance_negative_g009_definitioncartesiansecondvalue) = 0) \/ exists ge_signed_half_g009_definitioncartesiansecondvaluedecode. (((scp_second_g009_definitioncartesian) = 2 * ge_signed_half_g009_definitioncartesiansecondvaluedecode + 1 /\ (ge_balance_positive_g009_definitioncartesiansecondvalue) = 0) /\ (ge_balance_negative_g009_definitioncartesiansecondvalue) = S ge_signed_half_g009_definitioncartesiansecondvaluedecode))) /\ ((dst_positive_g009_definitioncartesiansecond) + ge_balance_negative_g009_definitioncartesiansecondvalue = (dst_negative_g009_definitioncartesiansecond) + ge_balance_positive_g009_definitioncartesiansecondvalue))))))))) -> (exists dst_positive_code_g009_definitioncartesianentry dst_positive_scale_g009_definitioncartesianentry dst_negative_code_g009_definitioncartesianentry dst_negative_scale_g009_definitioncartesianentry dst_positive_g009_definitioncartesianentry dst_negative_g009_definitioncartesianentry. ((((T)) = (((((dst_positive_code_g009_definitioncartesianentry) + (dst_positive_scale_g009_definitioncartesianentry)) * S ((dst_positive_code_g009_definitioncartesianentry) + (dst_positive_scale_g009_definitioncartesianentry)) + ((dst_positive_scale_g009_definitioncartesianentry) + (dst_positive_scale_g009_definitioncartesianentry))) + (((dst_negative_code_g009_definitioncartesianentry) + (dst_negative_scale_g009_definitioncartesianentry)) * S ((dst_negative_code_g009_definitioncartesianentry) + (dst_negative_scale_g009_definitioncartesianentry)) + ((dst_negative_scale_g009_definitioncartesianentry) + (dst_negative_scale_g009_definitioncartesianentry)))) * S ((((dst_positive_code_g009_definitioncartesianentry) + (dst_positive_scale_g009_definitioncartesianentry)) * S ((dst_positive_code_g009_definitioncartesianentry) + (dst_positive_scale_g009_definitioncartesianentry)) + ((dst_positive_scale_g009_definitioncartesianentry) + (dst_positive_scale_g009_definitioncartesianentry))) + (((dst_negative_code_g009_definitioncartesianentry) + (dst_negative_scale_g009_definitioncartesianentry)) * S ((dst_negative_code_g009_definitioncartesianentry) + (dst_negative_scale_g009_definitioncartesianentry)) + ((dst_negative_scale_g009_definitioncartesianentry) + (dst_negative_scale_g009_definitioncartesianentry)))) + ((((dst_negative_code_g009_definitioncartesianentry) + (dst_negative_scale_g009_definitioncartesianentry)) * S ((dst_negative_code_g009_definitioncartesianentry) + (dst_negative_scale_g009_definitioncartesianentry)) + ((dst_negative_scale_g009_definitioncartesianentry) + (dst_negative_scale_g009_definitioncartesianentry))) + (((dst_negative_code_g009_definitioncartesianentry) + (dst_negative_scale_g009_definitioncartesianentry)) * S ((dst_negative_code_g009_definitioncartesianentry) + (dst_negative_scale_g009_definitioncartesianentry)) + ((dst_negative_scale_g009_definitioncartesianentry) + (dst_negative_scale_g009_definitioncartesianentry)))))) /\ (((((exists ff_h_pvs_g009_definitioncartesianentrypositive. ff_h_pvs_g009_definitioncartesianentrypositive + S (dst_positive_g009_definitioncartesianentry) = S ((S (((S ((n)))*(scp_row_g009_definitioncartesian)+(scp_column_g009_definitioncartesian)))) * dst_positive_scale_g009_definitioncartesianentry)) /\ exists ff_q_pvs_g009_definitioncartesianentrypositive. dst_positive_code_g009_definitioncartesianentry = ff_q_pvs_g009_definitioncartesianentrypositive * S ((S (((S ((n)))*(scp_row_g009_definitioncartesian)+(scp_column_g009_definitioncartesian)))) * dst_positive_scale_g009_definitioncartesianentry) + (dst_positive_g009_definitioncartesianentry))) /\ (((((exists ff_h_pvs_g009_definitioncartesianentrynegative. ff_h_pvs_g009_definitioncartesianentrynegative + S (dst_negative_g009_definitioncartesianentry) = S ((S (((S ((n)))*(scp_row_g009_definitioncartesian)+(scp_column_g009_definitioncartesian)))) * dst_negative_scale_g009_definitioncartesianentry)) /\ exists ff_q_pvs_g009_definitioncartesianentrynegative. dst_negative_code_g009_definitioncartesianentry = ff_q_pvs_g009_definitioncartesianentrynegative * S ((S (((S ((n)))*(scp_row_g009_definitioncartesian)+(scp_column_g009_definitioncartesian)))) * dst_negative_scale_g009_definitioncartesianentry) + (dst_negative_g009_definitioncartesianentry))) /\ (exists ge_balance_positive_g009_definitioncartesianentryvalue ge_balance_negative_g009_definitioncartesianentryvalue. (((((scp_value_g009_definitioncartesian) = 2 * (ge_balance_positive_g009_definitioncartesianentryvalue) /\ (ge_balance_negative_g009_definitioncartesianentryvalue) = 0) \/ exists ge_signed_half_g009_definitioncartesianentryvaluedecode. (((scp_value_g009_definitioncartesian) = 2 * ge_signed_half_g009_definitioncartesianentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitioncartesianentryvalue) = 0) /\ (ge_balance_negative_g009_definitioncartesianentryvalue) = S ge_signed_half_g009_definitioncartesianentryvaluedecode))) /\ ((dst_positive_g009_definitioncartesianentry) + ge_balance_negative_g009_definitioncartesianentryvalue = (dst_negative_g009_definitioncartesianentry) + ge_balance_positive_g009_definitioncartesianentryvalue))))))))) -> (exists sto_ap_g009_definitioncartesianmultiply sto_an_g009_definitioncartesianmultiply sto_bp_g009_definitioncartesianmultiply sto_bn_g009_definitioncartesianmultiply sto_cp_g009_definitioncartesianmultiply sto_cn_g009_definitioncartesianmultiply. (((((scp_first_g009_definitioncartesian) = 2 * (sto_ap_g009_definitioncartesianmultiply) /\ (sto_an_g009_definitioncartesianmultiply) = 0) \/ exists ge_signed_half_g009_definitioncartesianmultiplyleft. (((scp_first_g009_definitioncartesian) = 2 * ge_signed_half_g009_definitioncartesianmultiplyleft + 1 /\ (sto_ap_g009_definitioncartesianmultiply) = 0) /\ (sto_an_g009_definitioncartesianmultiply) = S ge_signed_half_g009_definitioncartesianmultiplyleft))) /\ ((((((scp_second_g009_definitioncartesian) = 2 * (sto_bp_g009_definitioncartesianmultiply) /\ (sto_bn_g009_definitioncartesianmultiply) = 0) \/ exists ge_signed_half_g009_definitioncartesianmultiplyright. (((scp_second_g009_definitioncartesian) = 2 * ge_signed_half_g009_definitioncartesianmultiplyright + 1 /\ (sto_bp_g009_definitioncartesianmultiply) = 0) /\ (sto_bn_g009_definitioncartesianmultiply) = S ge_signed_half_g009_definitioncartesianmultiplyright))) /\ ((((((scp_value_g009_definitioncartesian) = 2 * (sto_cp_g009_definitioncartesianmultiply) /\ (sto_cn_g009_definitioncartesianmultiply) = 0) \/ exists ge_signed_half_g009_definitioncartesianmultiplyoutput. (((scp_value_g009_definitioncartesian) = 2 * ge_signed_half_g009_definitioncartesianmultiplyoutput + 1 /\ (sto_cp_g009_definitioncartesianmultiply) = 0) /\ (sto_cn_g009_definitioncartesianmultiply) = S ge_signed_half_g009_definitioncartesianmultiplyoutput))) /\ ((sto_ap_g009_definitioncartesianmultiply * sto_bp_g009_definitioncartesianmultiply + sto_an_g009_definitioncartesianmultiply * sto_bn_g009_definitioncartesianmultiply) + sto_cn_g009_definitioncartesianmultiply = (sto_ap_g009_definitioncartesianmultiply * sto_bn_g009_definitioncartesianmultiply + sto_an_g009_definitioncartesianmultiply * sto_bp_g009_definitioncartesianmultiply) + sto_cp_g009_definitioncartesianmultiply)))))))))))))) /\ (((((exists dst_positive_code_g009_definitiontargettable dst_positive_scale_g009_definitiontargettable dst_negative_code_g009_definitiontargettable dst_negative_scale_g009_definitiontargettable. ((((Q)) = (((((dst_positive_code_g009_definitiontargettable) + (dst_positive_scale_g009_definitiontargettable)) * S ((dst_positive_code_g009_definitiontargettable) + (dst_positive_scale_g009_definitiontargettable)) + ((dst_positive_scale_g009_definitiontargettable) + (dst_positive_scale_g009_definitiontargettable))) + (((dst_negative_code_g009_definitiontargettable) + (dst_negative_scale_g009_definitiontargettable)) * S ((dst_negative_code_g009_definitiontargettable) + (dst_negative_scale_g009_definitiontargettable)) + ((dst_negative_scale_g009_definitiontargettable) + (dst_negative_scale_g009_definitiontargettable)))) * S ((((dst_positive_code_g009_definitiontargettable) + (dst_positive_scale_g009_definitiontargettable)) * S ((dst_positive_code_g009_definitiontargettable) + (dst_positive_scale_g009_definitiontargettable)) + ((dst_positive_scale_g009_definitiontargettable) + (dst_positive_scale_g009_definitiontargettable))) + (((dst_negative_code_g009_definitiontargettable) + (dst_negative_scale_g009_definitiontargettable)) * S ((dst_negative_code_g009_definitiontargettable) + (dst_negative_scale_g009_definitiontargettable)) + ((dst_negative_scale_g009_definitiontargettable) + (dst_negative_scale_g009_definitiontargettable)))) + ((((dst_negative_code_g009_definitiontargettable) + (dst_negative_scale_g009_definitiontargettable)) * S ((dst_negative_code_g009_definitiontargettable) + (dst_negative_scale_g009_definitiontargettable)) + ((dst_negative_scale_g009_definitiontargettable) + (dst_negative_scale_g009_definitiontargettable))) + (((dst_negative_code_g009_definitiontargettable) + (dst_negative_scale_g009_definitiontargettable)) * S ((dst_negative_code_g009_definitiontargettable) + (dst_negative_scale_g009_definitiontargettable)) + ((dst_negative_scale_g009_definitiontargettable) + (dst_negative_scale_g009_definitiontargettable)))))) /\ (forall dst_index_g009_definitiontargettable. (exists pvs_le_gap_g009_definitiontargettabledomain. pvs_le_gap_g009_definitiontargettabledomain + (dst_index_g009_definitiontargettable) = (((m))*((n)))) -> exists dst_positive_g009_definitiontargettable dst_negative_g009_definitiontargettable dst_value_g009_definitiontargettable. ((((exists ff_h_pvs_g009_definitiontargettableentrypositive. ff_h_pvs_g009_definitiontargettableentrypositive + S (dst_positive_g009_definitiontargettable) = S ((S (dst_index_g009_definitiontargettable)) * dst_positive_scale_g009_definitiontargettable)) /\ exists ff_q_pvs_g009_definitiontargettableentrypositive. dst_positive_code_g009_definitiontargettable = ff_q_pvs_g009_definitiontargettableentrypositive * S ((S (dst_index_g009_definitiontargettable)) * dst_positive_scale_g009_definitiontargettable) + (dst_positive_g009_definitiontargettable))) /\ (((((exists ff_h_pvs_g009_definitiontargettableentrynegative. ff_h_pvs_g009_definitiontargettableentrynegative + S (dst_negative_g009_definitiontargettable) = S ((S (dst_index_g009_definitiontargettable)) * dst_negative_scale_g009_definitiontargettable)) /\ exists ff_q_pvs_g009_definitiontargettableentrynegative. dst_negative_code_g009_definitiontargettable = ff_q_pvs_g009_definitiontargettableentrynegative * S ((S (dst_index_g009_definitiontargettable)) * dst_negative_scale_g009_definitiontargettable) + (dst_negative_g009_definitiontargettable))) /\ (exists ge_balance_positive_g009_definitiontargettableentryvalue ge_balance_negative_g009_definitiontargettableentryvalue. (((((dst_value_g009_definitiontargettable) = 2 * (ge_balance_positive_g009_definitiontargettableentryvalue) /\ (ge_balance_negative_g009_definitiontargettableentryvalue) = 0) \/ exists ge_signed_half_g009_definitiontargettableentryvaluedecode. (((dst_value_g009_definitiontargettable) = 2 * ge_signed_half_g009_definitiontargettableentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitiontargettableentryvalue) = 0) /\ (ge_balance_negative_g009_definitiontargettableentryvalue) = S ge_signed_half_g009_definitiontargettableentryvaluedecode))) /\ ((dst_positive_g009_definitiontargettable) + ge_balance_negative_g009_definitiontargettableentryvalue = (dst_negative_g009_definitiontargettable) + ge_balance_positive_g009_definitiontargettableentryvalue))))))))) /\ (forall dc_index_g009_definitiontarget dc_value_g009_definitiontarget. (exists pvs_le_gap_g009_definitiontargetdomain. pvs_le_gap_g009_definitiontargetdomain + (dc_index_g009_definitiontarget) = (((m))*((n)))) -> (exists dst_positive_code_g009_definitiontargetlookup dst_positive_scale_g009_definitiontargetlookup dst_negative_code_g009_definitiontargetlookup dst_negative_scale_g009_definitiontargetlookup dst_positive_g009_definitiontargetlookup dst_negative_g009_definitiontargetlookup. ((((Q)) = (((((dst_positive_code_g009_definitiontargetlookup) + (dst_positive_scale_g009_definitiontargetlookup)) * S ((dst_positive_code_g009_definitiontargetlookup) + (dst_positive_scale_g009_definitiontargetlookup)) + ((dst_positive_scale_g009_definitiontargetlookup) + (dst_positive_scale_g009_definitiontargetlookup))) + (((dst_negative_code_g009_definitiontargetlookup) + (dst_negative_scale_g009_definitiontargetlookup)) * S ((dst_negative_code_g009_definitiontargetlookup) + (dst_negative_scale_g009_definitiontargetlookup)) + ((dst_negative_scale_g009_definitiontargetlookup) + (dst_negative_scale_g009_definitiontargetlookup)))) * S ((((dst_positive_code_g009_definitiontargetlookup) + (dst_positive_scale_g009_definitiontargetlookup)) * S ((dst_positive_code_g009_definitiontargetlookup) + (dst_positive_scale_g009_definitiontargetlookup)) + ((dst_positive_scale_g009_definitiontargetlookup) + (dst_positive_scale_g009_definitiontargetlookup))) + (((dst_negative_code_g009_definitiontargetlookup) + (dst_negative_scale_g009_definitiontargetlookup)) * S ((dst_negative_code_g009_definitiontargetlookup) + (dst_negative_scale_g009_definitiontargetlookup)) + ((dst_negative_scale_g009_definitiontargetlookup) + (dst_negative_scale_g009_definitiontargetlookup)))) + ((((dst_negative_code_g009_definitiontargetlookup) + (dst_negative_scale_g009_definitiontargetlookup)) * S ((dst_negative_code_g009_definitiontargetlookup) + (dst_negative_scale_g009_definitiontargetlookup)) + ((dst_negative_scale_g009_definitiontargetlookup) + (dst_negative_scale_g009_definitiontargetlookup))) + (((dst_negative_code_g009_definitiontargetlookup) + (dst_negative_scale_g009_definitiontargetlookup)) * S ((dst_negative_code_g009_definitiontargetlookup) + (dst_negative_scale_g009_definitiontargetlookup)) + ((dst_negative_scale_g009_definitiontargetlookup) + (dst_negative_scale_g009_definitiontargetlookup)))))) /\ (((((exists ff_h_pvs_g009_definitiontargetlookuppositive. ff_h_pvs_g009_definitiontargetlookuppositive + S (dst_positive_g009_definitiontargetlookup) = S ((S (dc_index_g009_definitiontarget)) * dst_positive_scale_g009_definitiontargetlookup)) /\ exists ff_q_pvs_g009_definitiontargetlookuppositive. dst_positive_code_g009_definitiontargetlookup = ff_q_pvs_g009_definitiontargetlookuppositive * S ((S (dc_index_g009_definitiontarget)) * dst_positive_scale_g009_definitiontargetlookup) + (dst_positive_g009_definitiontargetlookup))) /\ (((((exists ff_h_pvs_g009_definitiontargetlookupnegative. ff_h_pvs_g009_definitiontargetlookupnegative + S (dst_negative_g009_definitiontargetlookup) = S ((S (dc_index_g009_definitiontarget)) * dst_negative_scale_g009_definitiontargetlookup)) /\ exists ff_q_pvs_g009_definitiontargetlookupnegative. dst_negative_code_g009_definitiontargetlookup = ff_q_pvs_g009_definitiontargetlookupnegative * S ((S (dc_index_g009_definitiontarget)) * dst_negative_scale_g009_definitiontargetlookup) + (dst_negative_g009_definitiontargetlookup))) /\ (exists ge_balance_positive_g009_definitiontargetlookupvalue ge_balance_negative_g009_definitiontargetlookupvalue. (((((dc_value_g009_definitiontarget) = 2 * (ge_balance_positive_g009_definitiontargetlookupvalue) /\ (ge_balance_negative_g009_definitiontargetlookupvalue) = 0) \/ exists ge_signed_half_g009_definitiontargetlookupvaluedecode. (((dc_value_g009_definitiontarget) = 2 * ge_signed_half_g009_definitiontargetlookupvaluedecode + 1 /\ (ge_balance_positive_g009_definitiontargetlookupvalue) = 0) /\ (ge_balance_negative_g009_definitiontargetlookupvalue) = S ge_signed_half_g009_definitiontargetlookupvaluedecode))) /\ ((dst_positive_g009_definitiontargetlookup) + ge_balance_negative_g009_definitiontargetlookupvalue = (dst_negative_g009_definitiontargetlookup) + ge_balance_positive_g009_definitiontargetlookupvalue))))))))) -> ((((~((dc_index_g009_definitiontarget)=0)) /\ (exists dc_quotient_g009_definitiontargetentry dc_left_g009_definitiontargetentry dc_right_g009_definitiontargetentry. (((((m))*((n)))=(dc_index_g009_definitiontarget)*dc_quotient_g009_definitiontargetentry) /\ (((exists dst_positive_code_g009_definitiontargetentryleft dst_positive_scale_g009_definitiontargetentryleft dst_negative_code_g009_definitiontargetentryleft dst_negative_scale_g009_definitiontargetentryleft dst_positive_g009_definitiontargetentryleft dst_negative_g009_definitiontargetentryleft. ((((F)) = (((((dst_positive_code_g009_definitiontargetentryleft) + (dst_positive_scale_g009_definitiontargetentryleft)) * S ((dst_positive_code_g009_definitiontargetentryleft) + (dst_positive_scale_g009_definitiontargetentryleft)) + ((dst_positive_scale_g009_definitiontargetentryleft) + (dst_positive_scale_g009_definitiontargetentryleft))) + (((dst_negative_code_g009_definitiontargetentryleft) + (dst_negative_scale_g009_definitiontargetentryleft)) * S ((dst_negative_code_g009_definitiontargetentryleft) + (dst_negative_scale_g009_definitiontargetentryleft)) + ((dst_negative_scale_g009_definitiontargetentryleft) + (dst_negative_scale_g009_definitiontargetentryleft)))) * S ((((dst_positive_code_g009_definitiontargetentryleft) + (dst_positive_scale_g009_definitiontargetentryleft)) * S ((dst_positive_code_g009_definitiontargetentryleft) + (dst_positive_scale_g009_definitiontargetentryleft)) + ((dst_positive_scale_g009_definitiontargetentryleft) + (dst_positive_scale_g009_definitiontargetentryleft))) + (((dst_negative_code_g009_definitiontargetentryleft) + (dst_negative_scale_g009_definitiontargetentryleft)) * S ((dst_negative_code_g009_definitiontargetentryleft) + (dst_negative_scale_g009_definitiontargetentryleft)) + ((dst_negative_scale_g009_definitiontargetentryleft) + (dst_negative_scale_g009_definitiontargetentryleft)))) + ((((dst_negative_code_g009_definitiontargetentryleft) + (dst_negative_scale_g009_definitiontargetentryleft)) * S ((dst_negative_code_g009_definitiontargetentryleft) + (dst_negative_scale_g009_definitiontargetentryleft)) + ((dst_negative_scale_g009_definitiontargetentryleft) + (dst_negative_scale_g009_definitiontargetentryleft))) + (((dst_negative_code_g009_definitiontargetentryleft) + (dst_negative_scale_g009_definitiontargetentryleft)) * S ((dst_negative_code_g009_definitiontargetentryleft) + (dst_negative_scale_g009_definitiontargetentryleft)) + ((dst_negative_scale_g009_definitiontargetentryleft) + (dst_negative_scale_g009_definitiontargetentryleft)))))) /\ (((((exists ff_h_pvs_g009_definitiontargetentryleftpositive. ff_h_pvs_g009_definitiontargetentryleftpositive + S (dst_positive_g009_definitiontargetentryleft) = S ((S (dc_index_g009_definitiontarget)) * dst_positive_scale_g009_definitiontargetentryleft)) /\ exists ff_q_pvs_g009_definitiontargetentryleftpositive. dst_positive_code_g009_definitiontargetentryleft = ff_q_pvs_g009_definitiontargetentryleftpositive * S ((S (dc_index_g009_definitiontarget)) * dst_positive_scale_g009_definitiontargetentryleft) + (dst_positive_g009_definitiontargetentryleft))) /\ (((((exists ff_h_pvs_g009_definitiontargetentryleftnegative. ff_h_pvs_g009_definitiontargetentryleftnegative + S (dst_negative_g009_definitiontargetentryleft) = S ((S (dc_index_g009_definitiontarget)) * dst_negative_scale_g009_definitiontargetentryleft)) /\ exists ff_q_pvs_g009_definitiontargetentryleftnegative. dst_negative_code_g009_definitiontargetentryleft = ff_q_pvs_g009_definitiontargetentryleftnegative * S ((S (dc_index_g009_definitiontarget)) * dst_negative_scale_g009_definitiontargetentryleft) + (dst_negative_g009_definitiontargetentryleft))) /\ (exists ge_balance_positive_g009_definitiontargetentryleftvalue ge_balance_negative_g009_definitiontargetentryleftvalue. (((((dc_left_g009_definitiontargetentry) = 2 * (ge_balance_positive_g009_definitiontargetentryleftvalue) /\ (ge_balance_negative_g009_definitiontargetentryleftvalue) = 0) \/ exists ge_signed_half_g009_definitiontargetentryleftvaluedecode. (((dc_left_g009_definitiontargetentry) = 2 * ge_signed_half_g009_definitiontargetentryleftvaluedecode + 1 /\ (ge_balance_positive_g009_definitiontargetentryleftvalue) = 0) /\ (ge_balance_negative_g009_definitiontargetentryleftvalue) = S ge_signed_half_g009_definitiontargetentryleftvaluedecode))) /\ ((dst_positive_g009_definitiontargetentryleft) + ge_balance_negative_g009_definitiontargetentryleftvalue = (dst_negative_g009_definitiontargetentryleft) + ge_balance_positive_g009_definitiontargetentryleftvalue))))))))) /\ (((exists dst_positive_code_g009_definitiontargetentryright dst_positive_scale_g009_definitiontargetentryright dst_negative_code_g009_definitiontargetentryright dst_negative_scale_g009_definitiontargetentryright dst_positive_g009_definitiontargetentryright dst_negative_g009_definitiontargetentryright. ((((G)) = (((((dst_positive_code_g009_definitiontargetentryright) + (dst_positive_scale_g009_definitiontargetentryright)) * S ((dst_positive_code_g009_definitiontargetentryright) + (dst_positive_scale_g009_definitiontargetentryright)) + ((dst_positive_scale_g009_definitiontargetentryright) + (dst_positive_scale_g009_definitiontargetentryright))) + (((dst_negative_code_g009_definitiontargetentryright) + (dst_negative_scale_g009_definitiontargetentryright)) * S ((dst_negative_code_g009_definitiontargetentryright) + (dst_negative_scale_g009_definitiontargetentryright)) + ((dst_negative_scale_g009_definitiontargetentryright) + (dst_negative_scale_g009_definitiontargetentryright)))) * S ((((dst_positive_code_g009_definitiontargetentryright) + (dst_positive_scale_g009_definitiontargetentryright)) * S ((dst_positive_code_g009_definitiontargetentryright) + (dst_positive_scale_g009_definitiontargetentryright)) + ((dst_positive_scale_g009_definitiontargetentryright) + (dst_positive_scale_g009_definitiontargetentryright))) + (((dst_negative_code_g009_definitiontargetentryright) + (dst_negative_scale_g009_definitiontargetentryright)) * S ((dst_negative_code_g009_definitiontargetentryright) + (dst_negative_scale_g009_definitiontargetentryright)) + ((dst_negative_scale_g009_definitiontargetentryright) + (dst_negative_scale_g009_definitiontargetentryright)))) + ((((dst_negative_code_g009_definitiontargetentryright) + (dst_negative_scale_g009_definitiontargetentryright)) * S ((dst_negative_code_g009_definitiontargetentryright) + (dst_negative_scale_g009_definitiontargetentryright)) + ((dst_negative_scale_g009_definitiontargetentryright) + (dst_negative_scale_g009_definitiontargetentryright))) + (((dst_negative_code_g009_definitiontargetentryright) + (dst_negative_scale_g009_definitiontargetentryright)) * S ((dst_negative_code_g009_definitiontargetentryright) + (dst_negative_scale_g009_definitiontargetentryright)) + ((dst_negative_scale_g009_definitiontargetentryright) + (dst_negative_scale_g009_definitiontargetentryright)))))) /\ (((((exists ff_h_pvs_g009_definitiontargetentryrightpositive. ff_h_pvs_g009_definitiontargetentryrightpositive + S (dst_positive_g009_definitiontargetentryright) = S ((S (dc_quotient_g009_definitiontargetentry)) * dst_positive_scale_g009_definitiontargetentryright)) /\ exists ff_q_pvs_g009_definitiontargetentryrightpositive. dst_positive_code_g009_definitiontargetentryright = ff_q_pvs_g009_definitiontargetentryrightpositive * S ((S (dc_quotient_g009_definitiontargetentry)) * dst_positive_scale_g009_definitiontargetentryright) + (dst_positive_g009_definitiontargetentryright))) /\ (((((exists ff_h_pvs_g009_definitiontargetentryrightnegative. ff_h_pvs_g009_definitiontargetentryrightnegative + S (dst_negative_g009_definitiontargetentryright) = S ((S (dc_quotient_g009_definitiontargetentry)) * dst_negative_scale_g009_definitiontargetentryright)) /\ exists ff_q_pvs_g009_definitiontargetentryrightnegative. dst_negative_code_g009_definitiontargetentryright = ff_q_pvs_g009_definitiontargetentryrightnegative * S ((S (dc_quotient_g009_definitiontargetentry)) * dst_negative_scale_g009_definitiontargetentryright) + (dst_negative_g009_definitiontargetentryright))) /\ (exists ge_balance_positive_g009_definitiontargetentryrightvalue ge_balance_negative_g009_definitiontargetentryrightvalue. (((((dc_right_g009_definitiontargetentry) = 2 * (ge_balance_positive_g009_definitiontargetentryrightvalue) /\ (ge_balance_negative_g009_definitiontargetentryrightvalue) = 0) \/ exists ge_signed_half_g009_definitiontargetentryrightvaluedecode. (((dc_right_g009_definitiontargetentry) = 2 * ge_signed_half_g009_definitiontargetentryrightvaluedecode + 1 /\ (ge_balance_positive_g009_definitiontargetentryrightvalue) = 0) /\ (ge_balance_negative_g009_definitiontargetentryrightvalue) = S ge_signed_half_g009_definitiontargetentryrightvaluedecode))) /\ ((dst_positive_g009_definitiontargetentryright) + ge_balance_negative_g009_definitiontargetentryrightvalue = (dst_negative_g009_definitiontargetentryright) + ge_balance_positive_g009_definitiontargetentryrightvalue))))))))) /\ (exists sto_ap_g009_definitiontargetentryproduct sto_an_g009_definitiontargetentryproduct sto_bp_g009_definitiontargetentryproduct sto_bn_g009_definitiontargetentryproduct sto_cp_g009_definitiontargetentryproduct sto_cn_g009_definitiontargetentryproduct. (((((dc_left_g009_definitiontargetentry) = 2 * (sto_ap_g009_definitiontargetentryproduct) /\ (sto_an_g009_definitiontargetentryproduct) = 0) \/ exists ge_signed_half_g009_definitiontargetentryproductleft. (((dc_left_g009_definitiontargetentry) = 2 * ge_signed_half_g009_definitiontargetentryproductleft + 1 /\ (sto_ap_g009_definitiontargetentryproduct) = 0) /\ (sto_an_g009_definitiontargetentryproduct) = S ge_signed_half_g009_definitiontargetentryproductleft))) /\ ((((((dc_right_g009_definitiontargetentry) = 2 * (sto_bp_g009_definitiontargetentryproduct) /\ (sto_bn_g009_definitiontargetentryproduct) = 0) \/ exists ge_signed_half_g009_definitiontargetentryproductright. (((dc_right_g009_definitiontargetentry) = 2 * ge_signed_half_g009_definitiontargetentryproductright + 1 /\ (sto_bp_g009_definitiontargetentryproduct) = 0) /\ (sto_bn_g009_definitiontargetentryproduct) = S ge_signed_half_g009_definitiontargetentryproductright))) /\ ((((((dc_value_g009_definitiontarget) = 2 * (sto_cp_g009_definitiontargetentryproduct) /\ (sto_cn_g009_definitiontargetentryproduct) = 0) \/ exists ge_signed_half_g009_definitiontargetentryproductoutput. (((dc_value_g009_definitiontarget) = 2 * ge_signed_half_g009_definitiontargetentryproductoutput + 1 /\ (sto_cp_g009_definitiontargetentryproduct) = 0) /\ (sto_cn_g009_definitiontargetentryproduct) = S ge_signed_half_g009_definitiontargetentryproductoutput))) /\ ((sto_ap_g009_definitiontargetentryproduct * sto_bp_g009_definitiontargetentryproduct + sto_an_g009_definitiontargetentryproduct * sto_bn_g009_definitiontargetentryproduct) + sto_cn_g009_definitiontargetentryproduct = (sto_ap_g009_definitiontargetentryproduct * sto_bn_g009_definitiontargetentryproduct + sto_an_g009_definitiontargetentryproduct * sto_bp_g009_definitiontargetentryproduct) + sto_cp_g009_definitiontargetentryproduct))))))))))))))) \/ ((((dc_index_g009_definitiontarget)=0 \/ ~(exists pvs_factor_g009_definitiontargetentrynondivisor. (((m))*((n))) = (dc_index_g009_definitiontarget) * pvs_factor_g009_definitiontargetentrynondivisor)) /\ ((dc_value_g009_definitiontarget)=0))))))) /\ (((~((S ((n)))=0)) /\ (forall dpi_index_g009_definitionmap dpi_row_g009_definitionmap dpi_column_g009_definitionmap. (exists pvs_gap_g009_definitionmapwindow. pvs_gap_g009_definitionmapwindow + S (dpi_index_g009_definitionmap) = ((S ((m)))*(S ((n))))) -> (exists pvs_gap_g009_definitionmapremainder. pvs_gap_g009_definitionmapremainder + S (dpi_column_g009_definitionmap) = (S ((n)))) -> (dpi_index_g009_definitionmap)=(S ((n)))*(dpi_row_g009_definitionmap)+(dpi_column_g009_definitionmap) -> (((exists ff_h_pvs_g009_definitionmapvalue. ff_h_pvs_g009_definitionmapvalue + S ((dpi_row_g009_definitionmap)*(dpi_column_g009_definitionmap)) = S ((S (dpi_index_g009_definitionmap)) * (s))) /\ exists ff_q_pvs_g009_definitionmapvalue. (r) = ff_q_pvs_g009_definitionmapvalue * S ((S (dpi_index_g009_definitionmap)) * (s)) + ((dpi_row_g009_definitionmap)*(dpi_column_g009_definitionmap))))))))))))))))))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
none
Checked theorems using this definition
MX0051 · dirichlet_coprime_grid_nonzero_coordinatesMX0052 · dirichlet_coprime_grid_support_preservingMX0053 · dirichlet_coprime_grid_support_injectiveMX0054 · dirichlet_coprime_grid_support_coveringMX0055 · dirichlet_coprime_grid_support_reindexMX0056 · dirichlet_coprime_product_data_constructMX0057 · dirichlet_convolution_multiplicative_values