jordan_enumeration_distinct

Exact expanded first-order arithmetic statement

forall k n A B C D j i h b c d e. (((forall jt_i_distinctenum. (exists jt_gap_distinctenumsoundindex. jt_gap_distinctenumsoundindex+S (jt_i_distinctenum)=(j)) -> exists jt_b_distinctenum jt_c_distinctenum. ((((((exists fs_h_jt_distinctenumsoundcode. fs_h_jt_distinctenumsoundcode + S (jt_b_distinctenum) = S ((S (jt_i_distinctenum)) * B)) /\ exists fs_q_jt_distinctenumsoundcode. A = fs_q_jt_distinctenumsoundcode * S ((S (jt_i_distinctenum)) * B) + (jt_b_distinctenum))) /\ (((exists fs_h_jt_distinctenumsoundscale. fs_h_jt_distinctenumsoundscale + S (jt_c_distinctenum) = S ((S (jt_i_distinctenum)) * D)) /\ exists fs_q_jt_distinctenumsoundscale. C = fs_q_jt_distinctenumsoundscale * S ((S (jt_i_distinctenum)) * D) + (jt_c_distinctenum))))) /\ (((forall jt_index_distinctenumbound. (exists jt_gap_distinctenumboundindex. jt_gap_distinctenumboundindex+S (jt_index_distinctenumbound)=(k)) -> exists jt_value_distinctenumbound. ((((exists fs_h_jt_distinctenumboundat. fs_h_jt_distinctenumboundat + S (jt_value_distinctenumbound) = S ((S (jt_index_distinctenumbound)) * jt_c_distinctenum)) /\ exists fs_q_jt_distinctenumboundat. jt_b_distinctenum = fs_q_jt_distinctenumboundat * S ((S (jt_index_distinctenumbound)) * jt_c_distinctenum) + (jt_value_distinctenumbound))) /\ (exists jt_gap_distinctenumboundvalue. jt_gap_distinctenumboundvalue+S (jt_value_distinctenumbound)=(n)))) /\ (forall jt_divisor_distinctenumprimitive. (exists jt_factor_distinctenumprimitivemodulus. (n)=(jt_divisor_distinctenumprimitive)*jt_factor_distinctenumprimitivemodulus) -> (forall jt_index_distinctenumprimitivecoordinates jt_value_distinctenumprimitivecoordinates. (exists jt_gap_distinctenumprimitivecoordinatesindex. jt_gap_distinctenumprimitivecoordinatesindex+S (jt_index_distinctenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_distinctenumprimitivecoordinatesat. fs_h_jt_distinctenumprimitivecoordinatesat + S (jt_value_distinctenumprimitivecoordinates) = S ((S (jt_index_distinctenumprimitivecoordinates)) * jt_c_distinctenum)) /\ exists fs_q_jt_distinctenumprimitivecoordinatesat. jt_b_distinctenum = fs_q_jt_distinctenumprimitivecoordinatesat * S ((S (jt_index_distinctenumprimitivecoordinates)) * jt_c_distinctenum) + (jt_value_distinctenumprimitivecoordinates))) -> (exists jt_factor_distinctenumprimitivecoordinatesdivides. (jt_value_distinctenumprimitivecoordinates)=(jt_divisor_distinctenumprimitive)*jt_factor_distinctenumprimitivecoordinatesdivides)) -> jt_divisor_distinctenumprimitive=1))))) /\ (((forall jt_b_distinctenum jt_c_distinctenum. (forall jt_index_distinctenuminputbound. (exists jt_gap_distinctenuminputboundindex. jt_gap_distinctenuminputboundindex+S (jt_index_distinctenuminputbound)=(k)) -> exists jt_value_distinctenuminputbound. ((((exists fs_h_jt_distinctenuminputboundat. fs_h_jt_distinctenuminputboundat + S (jt_value_distinctenuminputbound) = S ((S (jt_index_distinctenuminputbound)) * jt_c_distinctenum)) /\ exists fs_q_jt_distinctenuminputboundat. jt_b_distinctenum = fs_q_jt_distinctenuminputboundat * S ((S (jt_index_distinctenuminputbound)) * jt_c_distinctenum) + (jt_value_distinctenuminputbound))) /\ (exists jt_gap_distinctenuminputboundvalue. jt_gap_distinctenuminputboundvalue+S (jt_value_distinctenuminputbound)=(n)))) -> (forall jt_divisor_distinctenuminputprimitive. (exists jt_factor_distinctenuminputprimitivemodulus. (n)=(jt_divisor_distinctenuminputprimitive)*jt_factor_distinctenuminputprimitivemodulus) -> (forall jt_index_distinctenuminputprimitivecoordinates jt_value_distinctenuminputprimitivecoordinates. (exists jt_gap_distinctenuminputprimitivecoordinatesindex. jt_gap_distinctenuminputprimitivecoordinatesindex+S (jt_index_distinctenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_distinctenuminputprimitivecoordinatesat. fs_h_jt_distinctenuminputprimitivecoordinatesat + S (jt_value_distinctenuminputprimitivecoordinates) = S ((S (jt_index_distinctenuminputprimitivecoordinates)) * jt_c_distinctenum)) /\ exists fs_q_jt_distinctenuminputprimitivecoordinatesat. jt_b_distinctenum = fs_q_jt_distinctenuminputprimitivecoordinatesat * S ((S (jt_index_distinctenuminputprimitivecoordinates)) * jt_c_distinctenum) + (jt_value_distinctenuminputprimitivecoordinates))) -> (exists jt_factor_distinctenuminputprimitivecoordinatesdivides. (jt_value_distinctenuminputprimitivecoordinates)=(jt_divisor_distinctenuminputprimitive)*jt_factor_distinctenuminputprimitivecoordinatesdivides)) -> jt_divisor_distinctenuminputprimitive=1) -> exists jt_i_distinctenum jt_d_distinctenum jt_e_distinctenum. ((exists jt_gap_distinctenumcompleteindex. jt_gap_distinctenumcompleteindex+S (jt_i_distinctenum)=(j)) /\ (((((((exists fs_h_jt_distinctenumcompletecode. fs_h_jt_distinctenumcompletecode + S (jt_d_distinctenum) = S ((S (jt_i_distinctenum)) * B)) /\ exists fs_q_jt_distinctenumcompletecode. A = fs_q_jt_distinctenumcompletecode * S ((S (jt_i_distinctenum)) * B) + (jt_d_distinctenum))) /\ (((exists fs_h_jt_distinctenumcompletescale. fs_h_jt_distinctenumcompletescale + S (jt_e_distinctenum) = S ((S (jt_i_distinctenum)) * D)) /\ exists fs_q_jt_distinctenumcompletescale. C = fs_q_jt_distinctenumcompletescale * S ((S (jt_i_distinctenum)) * D) + (jt_e_distinctenum))))) /\ (forall jt_index_distinctenumrepresented jt_left_distinctenumrepresented jt_right_distinctenumrepresented. (exists jt_gap_distinctenumrepresentedindex. jt_gap_distinctenumrepresentedindex+S (jt_index_distinctenumrepresented)=(k)) -> (((exists fs_h_jt_distinctenumrepresentedleft. fs_h_jt_distinctenumrepresentedleft + S (jt_left_distinctenumrepresented) = S ((S (jt_index_distinctenumrepresented)) * jt_c_distinctenum)) /\ exists fs_q_jt_distinctenumrepresentedleft. jt_b_distinctenum = fs_q_jt_distinctenumrepresentedleft * S ((S (jt_index_distinctenumrepresented)) * jt_c_distinctenum) + (jt_left_distinctenumrepresented))) -> (((exists fs_h_jt_distinctenumrepresentedright. fs_h_jt_distinctenumrepresentedright + S (jt_right_distinctenumrepresented) = S ((S (jt_index_distinctenumrepresented)) * jt_e_distinctenum)) /\ exists fs_q_jt_distinctenumrepresentedright. jt_d_distinctenum = fs_q_jt_distinctenumrepresentedright * S ((S (jt_index_distinctenumrepresented)) * jt_e_distinctenum) + (jt_right_distinctenumrepresented))) -> jt_left_distinctenumrepresented=jt_right_distinctenumrepresented))))) /\ (forall jt_i_distinctenum jt_h_distinctenum jt_b_distinctenum jt_c_distinctenum jt_d_distinctenum jt_e_distinctenum. (exists jt_gap_distinctenumfirstindex. jt_gap_distinctenumfirstindex+S (jt_i_distinctenum)=(j)) -> (exists jt_gap_distinctenumsecondindex. jt_gap_distinctenumsecondindex+S (jt_h_distinctenum)=(j)) -> (((((exists fs_h_jt_distinctenumfirstcode. fs_h_jt_distinctenumfirstcode + S (jt_b_distinctenum) = S ((S (jt_i_distinctenum)) * B)) /\ exists fs_q_jt_distinctenumfirstcode. A = fs_q_jt_distinctenumfirstcode * S ((S (jt_i_distinctenum)) * B) + (jt_b_distinctenum))) /\ (((exists fs_h_jt_distinctenumfirstscale. fs_h_jt_distinctenumfirstscale + S (jt_c_distinctenum) = S ((S (jt_i_distinctenum)) * D)) /\ exists fs_q_jt_distinctenumfirstscale. C = fs_q_jt_distinctenumfirstscale * S ((S (jt_i_distinctenum)) * D) + (jt_c_distinctenum))))) -> (((((exists fs_h_jt_distinctenumsecondcode. fs_h_jt_distinctenumsecondcode + S (jt_d_distinctenum) = S ((S (jt_h_distinctenum)) * B)) /\ exists fs_q_jt_distinctenumsecondcode. A = fs_q_jt_distinctenumsecondcode * S ((S (jt_h_distinctenum)) * B) + (jt_d_distinctenum))) /\ (((exists fs_h_jt_distinctenumsecondscale. fs_h_jt_distinctenumsecondscale + S (jt_e_distinctenum) = S ((S (jt_h_distinctenum)) * D)) /\ exists fs_q_jt_distinctenumsecondscale. C = fs_q_jt_distinctenumsecondscale * S ((S (jt_h_distinctenum)) * D) + (jt_e_distinctenum))))) -> (forall jt_index_distinctenumsame jt_left_distinctenumsame jt_right_distinctenumsame. (exists jt_gap_distinctenumsameindex. jt_gap_distinctenumsameindex+S (jt_index_distinctenumsame)=(k)) -> (((exists fs_h_jt_distinctenumsameleft. fs_h_jt_distinctenumsameleft + S (jt_left_distinctenumsame) = S ((S (jt_index_distinctenumsame)) * jt_c_distinctenum)) /\ exists fs_q_jt_distinctenumsameleft. jt_b_distinctenum = fs_q_jt_distinctenumsameleft * S ((S (jt_index_distinctenumsame)) * jt_c_distinctenum) + (jt_left_distinctenumsame))) -> (((exists fs_h_jt_distinctenumsameright. fs_h_jt_distinctenumsameright + S (jt_right_distinctenumsame) = S ((S (jt_index_distinctenumsame)) * jt_e_distinctenum)) /\ exists fs_q_jt_distinctenumsameright. jt_d_distinctenum = fs_q_jt_distinctenumsameright * S ((S (jt_index_distinctenumsame)) * jt_e_distinctenum) + (jt_right_distinctenumsame))) -> jt_left_distinctenumsame=jt_right_distinctenumsame) -> jt_i_distinctenum=jt_h_distinctenum))))) -> (exists jt_gap_distinctfirst. jt_gap_distinctfirst+S (i)=(j)) -> (exists jt_gap_distinctsecond. jt_gap_distinctsecond+S (h)=(j)) -> (((((exists fs_h_jt_distinctentryfirstcode. fs_h_jt_distinctentryfirstcode + S (b) = S ((S (i)) * B)) /\ exists fs_q_jt_distinctentryfirstcode. A = fs_q_jt_distinctentryfirstcode * S ((S (i)) * B) + (b))) /\ (((exists fs_h_jt_distinctentryfirstscale. fs_h_jt_distinctentryfirstscale + S (c) = S ((S (i)) * D)) /\ exists fs_q_jt_distinctentryfirstscale. C = fs_q_jt_distinctentryfirstscale * S ((S (i)) * D) + (c))))) -> (((((exists fs_h_jt_distinctentrysecondcode. fs_h_jt_distinctentrysecondcode + S (d) = S ((S (h)) * B)) /\ exists fs_q_jt_distinctentrysecondcode. A = fs_q_jt_distinctentrysecondcode * S ((S (h)) * B) + (d))) /\ (((exists fs_h_jt_distinctentrysecondscale. fs_h_jt_distinctentrysecondscale + S (e) = S ((S (h)) * D)) /\ exists fs_q_jt_distinctentrysecondscale. C = fs_q_jt_distinctentrysecondscale * S ((S (h)) * D) + (e))))) -> (forall jt_index_distinctequal jt_left_distinctequal jt_right_distinctequal. (exists jt_gap_distinctequalindex. jt_gap_distinctequalindex+S (jt_index_distinctequal)=(k)) -> (((exists fs_h_jt_distinctequalleft. fs_h_jt_distinctequalleft + S (jt_left_distinctequal) = S ((S (jt_index_distinctequal)) * c)) /\ exists fs_q_jt_distinctequalleft. b = fs_q_jt_distinctequalleft * S ((S (jt_index_distinctequal)) * c) + (jt_left_distinctequal))) -> (((exists fs_h_jt_distinctequalright. fs_h_jt_distinctequalright + S (jt_right_distinctequal) = S ((S (jt_index_distinctequal)) * e)) /\ exists fs_q_jt_distinctequalright. d = fs_q_jt_distinctequalright * S ((S (jt_index_distinctequal)) * e) + (jt_right_distinctequal))) -> jt_left_distinctequal=jt_right_distinctequal) -> i=h