jordan_enumeration_actual_value

Exact expanded first-order arithmetic statement

forall k n A B C D j i b c. (((forall jt_i_actualenum. (exists jt_gap_actualenumsoundindex. jt_gap_actualenumsoundindex+S (jt_i_actualenum)=(j)) -> exists jt_b_actualenum jt_c_actualenum. ((((((exists fs_h_jt_actualenumsoundcode. fs_h_jt_actualenumsoundcode + S (jt_b_actualenum) = S ((S (jt_i_actualenum)) * B)) /\ exists fs_q_jt_actualenumsoundcode. A = fs_q_jt_actualenumsoundcode * S ((S (jt_i_actualenum)) * B) + (jt_b_actualenum))) /\ (((exists fs_h_jt_actualenumsoundscale. fs_h_jt_actualenumsoundscale + S (jt_c_actualenum) = S ((S (jt_i_actualenum)) * D)) /\ exists fs_q_jt_actualenumsoundscale. C = fs_q_jt_actualenumsoundscale * S ((S (jt_i_actualenum)) * D) + (jt_c_actualenum))))) /\ (((forall jt_index_actualenumbound. (exists jt_gap_actualenumboundindex. jt_gap_actualenumboundindex+S (jt_index_actualenumbound)=(k)) -> exists jt_value_actualenumbound. ((((exists fs_h_jt_actualenumboundat. fs_h_jt_actualenumboundat + S (jt_value_actualenumbound) = S ((S (jt_index_actualenumbound)) * jt_c_actualenum)) /\ exists fs_q_jt_actualenumboundat. jt_b_actualenum = fs_q_jt_actualenumboundat * S ((S (jt_index_actualenumbound)) * jt_c_actualenum) + (jt_value_actualenumbound))) /\ (exists jt_gap_actualenumboundvalue. jt_gap_actualenumboundvalue+S (jt_value_actualenumbound)=(n)))) /\ (forall jt_divisor_actualenumprimitive. (exists jt_factor_actualenumprimitivemodulus. (n)=(jt_divisor_actualenumprimitive)*jt_factor_actualenumprimitivemodulus) -> (forall jt_index_actualenumprimitivecoordinates jt_value_actualenumprimitivecoordinates. (exists jt_gap_actualenumprimitivecoordinatesindex. jt_gap_actualenumprimitivecoordinatesindex+S (jt_index_actualenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_actualenumprimitivecoordinatesat. fs_h_jt_actualenumprimitivecoordinatesat + S (jt_value_actualenumprimitivecoordinates) = S ((S (jt_index_actualenumprimitivecoordinates)) * jt_c_actualenum)) /\ exists fs_q_jt_actualenumprimitivecoordinatesat. jt_b_actualenum = fs_q_jt_actualenumprimitivecoordinatesat * S ((S (jt_index_actualenumprimitivecoordinates)) * jt_c_actualenum) + (jt_value_actualenumprimitivecoordinates))) -> (exists jt_factor_actualenumprimitivecoordinatesdivides. (jt_value_actualenumprimitivecoordinates)=(jt_divisor_actualenumprimitive)*jt_factor_actualenumprimitivecoordinatesdivides)) -> jt_divisor_actualenumprimitive=1))))) /\ (((forall jt_b_actualenum jt_c_actualenum. (forall jt_index_actualenuminputbound. (exists jt_gap_actualenuminputboundindex. jt_gap_actualenuminputboundindex+S (jt_index_actualenuminputbound)=(k)) -> exists jt_value_actualenuminputbound. ((((exists fs_h_jt_actualenuminputboundat. fs_h_jt_actualenuminputboundat + S (jt_value_actualenuminputbound) = S ((S (jt_index_actualenuminputbound)) * jt_c_actualenum)) /\ exists fs_q_jt_actualenuminputboundat. jt_b_actualenum = fs_q_jt_actualenuminputboundat * S ((S (jt_index_actualenuminputbound)) * jt_c_actualenum) + (jt_value_actualenuminputbound))) /\ (exists jt_gap_actualenuminputboundvalue. jt_gap_actualenuminputboundvalue+S (jt_value_actualenuminputbound)=(n)))) -> (forall jt_divisor_actualenuminputprimitive. (exists jt_factor_actualenuminputprimitivemodulus. (n)=(jt_divisor_actualenuminputprimitive)*jt_factor_actualenuminputprimitivemodulus) -> (forall jt_index_actualenuminputprimitivecoordinates jt_value_actualenuminputprimitivecoordinates. (exists jt_gap_actualenuminputprimitivecoordinatesindex. jt_gap_actualenuminputprimitivecoordinatesindex+S (jt_index_actualenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_actualenuminputprimitivecoordinatesat. fs_h_jt_actualenuminputprimitivecoordinatesat + S (jt_value_actualenuminputprimitivecoordinates) = S ((S (jt_index_actualenuminputprimitivecoordinates)) * jt_c_actualenum)) /\ exists fs_q_jt_actualenuminputprimitivecoordinatesat. jt_b_actualenum = fs_q_jt_actualenuminputprimitivecoordinatesat * S ((S (jt_index_actualenuminputprimitivecoordinates)) * jt_c_actualenum) + (jt_value_actualenuminputprimitivecoordinates))) -> (exists jt_factor_actualenuminputprimitivecoordinatesdivides. (jt_value_actualenuminputprimitivecoordinates)=(jt_divisor_actualenuminputprimitive)*jt_factor_actualenuminputprimitivecoordinatesdivides)) -> jt_divisor_actualenuminputprimitive=1) -> exists jt_i_actualenum jt_d_actualenum jt_e_actualenum. ((exists jt_gap_actualenumcompleteindex. jt_gap_actualenumcompleteindex+S (jt_i_actualenum)=(j)) /\ (((((((exists fs_h_jt_actualenumcompletecode. fs_h_jt_actualenumcompletecode + S (jt_d_actualenum) = S ((S (jt_i_actualenum)) * B)) /\ exists fs_q_jt_actualenumcompletecode. A = fs_q_jt_actualenumcompletecode * S ((S (jt_i_actualenum)) * B) + (jt_d_actualenum))) /\ (((exists fs_h_jt_actualenumcompletescale. fs_h_jt_actualenumcompletescale + S (jt_e_actualenum) = S ((S (jt_i_actualenum)) * D)) /\ exists fs_q_jt_actualenumcompletescale. C = fs_q_jt_actualenumcompletescale * S ((S (jt_i_actualenum)) * D) + (jt_e_actualenum))))) /\ (forall jt_index_actualenumrepresented jt_left_actualenumrepresented jt_right_actualenumrepresented. (exists jt_gap_actualenumrepresentedindex. jt_gap_actualenumrepresentedindex+S (jt_index_actualenumrepresented)=(k)) -> (((exists fs_h_jt_actualenumrepresentedleft. fs_h_jt_actualenumrepresentedleft + S (jt_left_actualenumrepresented) = S ((S (jt_index_actualenumrepresented)) * jt_c_actualenum)) /\ exists fs_q_jt_actualenumrepresentedleft. jt_b_actualenum = fs_q_jt_actualenumrepresentedleft * S ((S (jt_index_actualenumrepresented)) * jt_c_actualenum) + (jt_left_actualenumrepresented))) -> (((exists fs_h_jt_actualenumrepresentedright. fs_h_jt_actualenumrepresentedright + S (jt_right_actualenumrepresented) = S ((S (jt_index_actualenumrepresented)) * jt_e_actualenum)) /\ exists fs_q_jt_actualenumrepresentedright. jt_d_actualenum = fs_q_jt_actualenumrepresentedright * S ((S (jt_index_actualenumrepresented)) * jt_e_actualenum) + (jt_right_actualenumrepresented))) -> jt_left_actualenumrepresented=jt_right_actualenumrepresented))))) /\ (forall jt_i_actualenum jt_h_actualenum jt_b_actualenum jt_c_actualenum jt_d_actualenum jt_e_actualenum. (exists jt_gap_actualenumfirstindex. jt_gap_actualenumfirstindex+S (jt_i_actualenum)=(j)) -> (exists jt_gap_actualenumsecondindex. jt_gap_actualenumsecondindex+S (jt_h_actualenum)=(j)) -> (((((exists fs_h_jt_actualenumfirstcode. fs_h_jt_actualenumfirstcode + S (jt_b_actualenum) = S ((S (jt_i_actualenum)) * B)) /\ exists fs_q_jt_actualenumfirstcode. A = fs_q_jt_actualenumfirstcode * S ((S (jt_i_actualenum)) * B) + (jt_b_actualenum))) /\ (((exists fs_h_jt_actualenumfirstscale. fs_h_jt_actualenumfirstscale + S (jt_c_actualenum) = S ((S (jt_i_actualenum)) * D)) /\ exists fs_q_jt_actualenumfirstscale. C = fs_q_jt_actualenumfirstscale * S ((S (jt_i_actualenum)) * D) + (jt_c_actualenum))))) -> (((((exists fs_h_jt_actualenumsecondcode. fs_h_jt_actualenumsecondcode + S (jt_d_actualenum) = S ((S (jt_h_actualenum)) * B)) /\ exists fs_q_jt_actualenumsecondcode. A = fs_q_jt_actualenumsecondcode * S ((S (jt_h_actualenum)) * B) + (jt_d_actualenum))) /\ (((exists fs_h_jt_actualenumsecondscale. fs_h_jt_actualenumsecondscale + S (jt_e_actualenum) = S ((S (jt_h_actualenum)) * D)) /\ exists fs_q_jt_actualenumsecondscale. C = fs_q_jt_actualenumsecondscale * S ((S (jt_h_actualenum)) * D) + (jt_e_actualenum))))) -> (forall jt_index_actualenumsame jt_left_actualenumsame jt_right_actualenumsame. (exists jt_gap_actualenumsameindex. jt_gap_actualenumsameindex+S (jt_index_actualenumsame)=(k)) -> (((exists fs_h_jt_actualenumsameleft. fs_h_jt_actualenumsameleft + S (jt_left_actualenumsame) = S ((S (jt_index_actualenumsame)) * jt_c_actualenum)) /\ exists fs_q_jt_actualenumsameleft. jt_b_actualenum = fs_q_jt_actualenumsameleft * S ((S (jt_index_actualenumsame)) * jt_c_actualenum) + (jt_left_actualenumsame))) -> (((exists fs_h_jt_actualenumsameright. fs_h_jt_actualenumsameright + S (jt_right_actualenumsame) = S ((S (jt_index_actualenumsame)) * jt_e_actualenum)) /\ exists fs_q_jt_actualenumsameright. jt_d_actualenum = fs_q_jt_actualenumsameright * S ((S (jt_index_actualenumsame)) * jt_e_actualenum) + (jt_right_actualenumsame))) -> jt_left_actualenumsame=jt_right_actualenumsame) -> jt_i_actualenum=jt_h_actualenum))))) -> (exists jt_gap_actualindex. jt_gap_actualindex+S (i)=(j)) -> (((((exists fs_h_jt_actualentrycode. fs_h_jt_actualentrycode + S (b) = S ((S (i)) * B)) /\ exists fs_q_jt_actualentrycode. A = fs_q_jt_actualentrycode * S ((S (i)) * B) + (b))) /\ (((exists fs_h_jt_actualentryscale. fs_h_jt_actualentryscale + S (c) = S ((S (i)) * D)) /\ exists fs_q_jt_actualentryscale. C = fs_q_jt_actualentryscale * S ((S (i)) * D) + (c))))) -> ((forall jt_index_actualbound. (exists jt_gap_actualboundindex. jt_gap_actualboundindex+S (jt_index_actualbound)=(k)) -> exists jt_value_actualbound. ((((exists fs_h_jt_actualboundat. fs_h_jt_actualboundat + S (jt_value_actualbound) = S ((S (jt_index_actualbound)) * c)) /\ exists fs_q_jt_actualboundat. b = fs_q_jt_actualboundat * S ((S (jt_index_actualbound)) * c) + (jt_value_actualbound))) /\ (exists jt_gap_actualboundvalue. jt_gap_actualboundvalue+S (jt_value_actualbound)=(n)))) /\ (forall jt_divisor_actualprimitive. (exists jt_factor_actualprimitivemodulus. (n)=(jt_divisor_actualprimitive)*jt_factor_actualprimitivemodulus) -> (forall jt_index_actualprimitivecoordinates jt_value_actualprimitivecoordinates. (exists jt_gap_actualprimitivecoordinatesindex. jt_gap_actualprimitivecoordinatesindex+S (jt_index_actualprimitivecoordinates)=(k)) -> (((exists fs_h_jt_actualprimitivecoordinatesat. fs_h_jt_actualprimitivecoordinatesat + S (jt_value_actualprimitivecoordinates) = S ((S (jt_index_actualprimitivecoordinates)) * c)) /\ exists fs_q_jt_actualprimitivecoordinatesat. b = fs_q_jt_actualprimitivecoordinatesat * S ((S (jt_index_actualprimitivecoordinates)) * c) + (jt_value_actualprimitivecoordinates))) -> (exists jt_factor_actualprimitivecoordinatesdivides. (jt_value_actualprimitivecoordinates)=(jt_divisor_actualprimitive)*jt_factor_actualprimitivecoordinatesdivides)) -> jt_divisor_actualprimitive=1))