jordan_enumeration_reduce_primitive

Exact expanded first-order arithmetic statement

forall n k A B C D j b c. ~(n=0) -> (((forall jt_i_reduceenum. (exists jt_gap_reduceenumsoundindex. jt_gap_reduceenumsoundindex+S (jt_i_reduceenum)=(j)) -> exists jt_b_reduceenum jt_c_reduceenum. ((((((exists fs_h_jt_reduceenumsoundcode. fs_h_jt_reduceenumsoundcode + S (jt_b_reduceenum) = S ((S (jt_i_reduceenum)) * B)) /\ exists fs_q_jt_reduceenumsoundcode. A = fs_q_jt_reduceenumsoundcode * S ((S (jt_i_reduceenum)) * B) + (jt_b_reduceenum))) /\ (((exists fs_h_jt_reduceenumsoundscale. fs_h_jt_reduceenumsoundscale + S (jt_c_reduceenum) = S ((S (jt_i_reduceenum)) * D)) /\ exists fs_q_jt_reduceenumsoundscale. C = fs_q_jt_reduceenumsoundscale * S ((S (jt_i_reduceenum)) * D) + (jt_c_reduceenum))))) /\ (((forall jt_index_reduceenumbound. (exists jt_gap_reduceenumboundindex. jt_gap_reduceenumboundindex+S (jt_index_reduceenumbound)=(k)) -> exists jt_value_reduceenumbound. ((((exists fs_h_jt_reduceenumboundat. fs_h_jt_reduceenumboundat + S (jt_value_reduceenumbound) = S ((S (jt_index_reduceenumbound)) * jt_c_reduceenum)) /\ exists fs_q_jt_reduceenumboundat. jt_b_reduceenum = fs_q_jt_reduceenumboundat * S ((S (jt_index_reduceenumbound)) * jt_c_reduceenum) + (jt_value_reduceenumbound))) /\ (exists jt_gap_reduceenumboundvalue. jt_gap_reduceenumboundvalue+S (jt_value_reduceenumbound)=(n)))) /\ (forall jt_divisor_reduceenumprimitive. (exists jt_factor_reduceenumprimitivemodulus. (n)=(jt_divisor_reduceenumprimitive)*jt_factor_reduceenumprimitivemodulus) -> (forall jt_index_reduceenumprimitivecoordinates jt_value_reduceenumprimitivecoordinates. (exists jt_gap_reduceenumprimitivecoordinatesindex. jt_gap_reduceenumprimitivecoordinatesindex+S (jt_index_reduceenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_reduceenumprimitivecoordinatesat. fs_h_jt_reduceenumprimitivecoordinatesat + S (jt_value_reduceenumprimitivecoordinates) = S ((S (jt_index_reduceenumprimitivecoordinates)) * jt_c_reduceenum)) /\ exists fs_q_jt_reduceenumprimitivecoordinatesat. jt_b_reduceenum = fs_q_jt_reduceenumprimitivecoordinatesat * S ((S (jt_index_reduceenumprimitivecoordinates)) * jt_c_reduceenum) + (jt_value_reduceenumprimitivecoordinates))) -> (exists jt_factor_reduceenumprimitivecoordinatesdivides. (jt_value_reduceenumprimitivecoordinates)=(jt_divisor_reduceenumprimitive)*jt_factor_reduceenumprimitivecoordinatesdivides)) -> jt_divisor_reduceenumprimitive=1))))) /\ (((forall jt_b_reduceenum jt_c_reduceenum. (forall jt_index_reduceenuminputbound. (exists jt_gap_reduceenuminputboundindex. jt_gap_reduceenuminputboundindex+S (jt_index_reduceenuminputbound)=(k)) -> exists jt_value_reduceenuminputbound. ((((exists fs_h_jt_reduceenuminputboundat. fs_h_jt_reduceenuminputboundat + S (jt_value_reduceenuminputbound) = S ((S (jt_index_reduceenuminputbound)) * jt_c_reduceenum)) /\ exists fs_q_jt_reduceenuminputboundat. jt_b_reduceenum = fs_q_jt_reduceenuminputboundat * S ((S (jt_index_reduceenuminputbound)) * jt_c_reduceenum) + (jt_value_reduceenuminputbound))) /\ (exists jt_gap_reduceenuminputboundvalue. jt_gap_reduceenuminputboundvalue+S (jt_value_reduceenuminputbound)=(n)))) -> (forall jt_divisor_reduceenuminputprimitive. (exists jt_factor_reduceenuminputprimitivemodulus. (n)=(jt_divisor_reduceenuminputprimitive)*jt_factor_reduceenuminputprimitivemodulus) -> (forall jt_index_reduceenuminputprimitivecoordinates jt_value_reduceenuminputprimitivecoordinates. (exists jt_gap_reduceenuminputprimitivecoordinatesindex. jt_gap_reduceenuminputprimitivecoordinatesindex+S (jt_index_reduceenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_reduceenuminputprimitivecoordinatesat. fs_h_jt_reduceenuminputprimitivecoordinatesat + S (jt_value_reduceenuminputprimitivecoordinates) = S ((S (jt_index_reduceenuminputprimitivecoordinates)) * jt_c_reduceenum)) /\ exists fs_q_jt_reduceenuminputprimitivecoordinatesat. jt_b_reduceenum = fs_q_jt_reduceenuminputprimitivecoordinatesat * S ((S (jt_index_reduceenuminputprimitivecoordinates)) * jt_c_reduceenum) + (jt_value_reduceenuminputprimitivecoordinates))) -> (exists jt_factor_reduceenuminputprimitivecoordinatesdivides. (jt_value_reduceenuminputprimitivecoordinates)=(jt_divisor_reduceenuminputprimitive)*jt_factor_reduceenuminputprimitivecoordinatesdivides)) -> jt_divisor_reduceenuminputprimitive=1) -> exists jt_i_reduceenum jt_d_reduceenum jt_e_reduceenum. ((exists jt_gap_reduceenumcompleteindex. jt_gap_reduceenumcompleteindex+S (jt_i_reduceenum)=(j)) /\ (((((((exists fs_h_jt_reduceenumcompletecode. fs_h_jt_reduceenumcompletecode + S (jt_d_reduceenum) = S ((S (jt_i_reduceenum)) * B)) /\ exists fs_q_jt_reduceenumcompletecode. A = fs_q_jt_reduceenumcompletecode * S ((S (jt_i_reduceenum)) * B) + (jt_d_reduceenum))) /\ (((exists fs_h_jt_reduceenumcompletescale. fs_h_jt_reduceenumcompletescale + S (jt_e_reduceenum) = S ((S (jt_i_reduceenum)) * D)) /\ exists fs_q_jt_reduceenumcompletescale. C = fs_q_jt_reduceenumcompletescale * S ((S (jt_i_reduceenum)) * D) + (jt_e_reduceenum))))) /\ (forall jt_index_reduceenumrepresented jt_left_reduceenumrepresented jt_right_reduceenumrepresented. (exists jt_gap_reduceenumrepresentedindex. jt_gap_reduceenumrepresentedindex+S (jt_index_reduceenumrepresented)=(k)) -> (((exists fs_h_jt_reduceenumrepresentedleft. fs_h_jt_reduceenumrepresentedleft + S (jt_left_reduceenumrepresented) = S ((S (jt_index_reduceenumrepresented)) * jt_c_reduceenum)) /\ exists fs_q_jt_reduceenumrepresentedleft. jt_b_reduceenum = fs_q_jt_reduceenumrepresentedleft * S ((S (jt_index_reduceenumrepresented)) * jt_c_reduceenum) + (jt_left_reduceenumrepresented))) -> (((exists fs_h_jt_reduceenumrepresentedright. fs_h_jt_reduceenumrepresentedright + S (jt_right_reduceenumrepresented) = S ((S (jt_index_reduceenumrepresented)) * jt_e_reduceenum)) /\ exists fs_q_jt_reduceenumrepresentedright. jt_d_reduceenum = fs_q_jt_reduceenumrepresentedright * S ((S (jt_index_reduceenumrepresented)) * jt_e_reduceenum) + (jt_right_reduceenumrepresented))) -> jt_left_reduceenumrepresented=jt_right_reduceenumrepresented))))) /\ (forall jt_i_reduceenum jt_h_reduceenum jt_b_reduceenum jt_c_reduceenum jt_d_reduceenum jt_e_reduceenum. (exists jt_gap_reduceenumfirstindex. jt_gap_reduceenumfirstindex+S (jt_i_reduceenum)=(j)) -> (exists jt_gap_reduceenumsecondindex. jt_gap_reduceenumsecondindex+S (jt_h_reduceenum)=(j)) -> (((((exists fs_h_jt_reduceenumfirstcode. fs_h_jt_reduceenumfirstcode + S (jt_b_reduceenum) = S ((S (jt_i_reduceenum)) * B)) /\ exists fs_q_jt_reduceenumfirstcode. A = fs_q_jt_reduceenumfirstcode * S ((S (jt_i_reduceenum)) * B) + (jt_b_reduceenum))) /\ (((exists fs_h_jt_reduceenumfirstscale. fs_h_jt_reduceenumfirstscale + S (jt_c_reduceenum) = S ((S (jt_i_reduceenum)) * D)) /\ exists fs_q_jt_reduceenumfirstscale. C = fs_q_jt_reduceenumfirstscale * S ((S (jt_i_reduceenum)) * D) + (jt_c_reduceenum))))) -> (((((exists fs_h_jt_reduceenumsecondcode. fs_h_jt_reduceenumsecondcode + S (jt_d_reduceenum) = S ((S (jt_h_reduceenum)) * B)) /\ exists fs_q_jt_reduceenumsecondcode. A = fs_q_jt_reduceenumsecondcode * S ((S (jt_h_reduceenum)) * B) + (jt_d_reduceenum))) /\ (((exists fs_h_jt_reduceenumsecondscale. fs_h_jt_reduceenumsecondscale + S (jt_e_reduceenum) = S ((S (jt_h_reduceenum)) * D)) /\ exists fs_q_jt_reduceenumsecondscale. C = fs_q_jt_reduceenumsecondscale * S ((S (jt_h_reduceenum)) * D) + (jt_e_reduceenum))))) -> (forall jt_index_reduceenumsame jt_left_reduceenumsame jt_right_reduceenumsame. (exists jt_gap_reduceenumsameindex. jt_gap_reduceenumsameindex+S (jt_index_reduceenumsame)=(k)) -> (((exists fs_h_jt_reduceenumsameleft. fs_h_jt_reduceenumsameleft + S (jt_left_reduceenumsame) = S ((S (jt_index_reduceenumsame)) * jt_c_reduceenum)) /\ exists fs_q_jt_reduceenumsameleft. jt_b_reduceenum = fs_q_jt_reduceenumsameleft * S ((S (jt_index_reduceenumsame)) * jt_c_reduceenum) + (jt_left_reduceenumsame))) -> (((exists fs_h_jt_reduceenumsameright. fs_h_jt_reduceenumsameright + S (jt_right_reduceenumsame) = S ((S (jt_index_reduceenumsame)) * jt_e_reduceenum)) /\ exists fs_q_jt_reduceenumsameright. jt_d_reduceenum = fs_q_jt_reduceenumsameright * S ((S (jt_index_reduceenumsame)) * jt_e_reduceenum) + (jt_right_reduceenumsame))) -> jt_left_reduceenumsame=jt_right_reduceenumsame) -> jt_i_reduceenum=jt_h_reduceenum))))) -> (forall jt_divisor_reduceinput. (exists jt_factor_reduceinputmodulus. (n)=(jt_divisor_reduceinput)*jt_factor_reduceinputmodulus) -> (forall jt_index_reduceinputcoordinates jt_value_reduceinputcoordinates. (exists jt_gap_reduceinputcoordinatesindex. jt_gap_reduceinputcoordinatesindex+S (jt_index_reduceinputcoordinates)=(k)) -> (((exists fs_h_jt_reduceinputcoordinatesat. fs_h_jt_reduceinputcoordinatesat + S (jt_value_reduceinputcoordinates) = S ((S (jt_index_reduceinputcoordinates)) * c)) /\ exists fs_q_jt_reduceinputcoordinatesat. b = fs_q_jt_reduceinputcoordinatesat * S ((S (jt_index_reduceinputcoordinates)) * c) + (jt_value_reduceinputcoordinates))) -> (exists jt_factor_reduceinputcoordinatesdivides. (jt_value_reduceinputcoordinates)=(jt_divisor_reduceinput)*jt_factor_reduceinputcoordinatesdivides)) -> jt_divisor_reduceinput=1) -> exists i d e. ((exists jt_gap_reduceindex. jt_gap_reduceindex+S (i)=(j)) /\ (((((((exists fs_h_jt_reduceentrycode. fs_h_jt_reduceentrycode + S (d) = S ((S (i)) * B)) /\ exists fs_q_jt_reduceentrycode. A = fs_q_jt_reduceentrycode * S ((S (i)) * B) + (d))) /\ (((exists fs_h_jt_reduceentryscale. fs_h_jt_reduceentryscale + S (e) = S ((S (i)) * D)) /\ exists fs_q_jt_reduceentryscale. C = fs_q_jt_reduceentryscale * S ((S (i)) * D) + (e))))) /\ (forall jt_index_reduceresult jt_left_reduceresult jt_right_reduceresult. (exists jt_gap_reduceresultindex. jt_gap_reduceresultindex+S (jt_index_reduceresult)=(k)) -> (((exists fs_h_jt_reduceresultleft. fs_h_jt_reduceresultleft + S (jt_left_reduceresult) = S ((S (jt_index_reduceresult)) * c)) /\ exists fs_q_jt_reduceresultleft. b = fs_q_jt_reduceresultleft * S ((S (jt_index_reduceresult)) * c) + (jt_left_reduceresult))) -> (((exists fs_h_jt_reduceresultright. fs_h_jt_reduceresultright + S (jt_right_reduceresult) = S ((S (jt_index_reduceresult)) * e)) /\ exists fs_q_jt_reduceresultright. d = fs_q_jt_reduceresultright * S ((S (jt_index_reduceresult)) * e) + (jt_right_reduceresult))) -> (exists jt_left_reduceresultmod jt_right_reduceresultmod. (jt_left_reduceresult)+(n)*jt_left_reduceresultmod=(jt_right_reduceresult)+(n)*jt_right_reduceresultmod)))))