jordan_enumeration_complete

Exact expanded first-order arithmetic statement

forall k n A B C D j b c. (((forall jt_i_completeenum. (exists jt_gap_completeenumsoundindex. jt_gap_completeenumsoundindex+S (jt_i_completeenum)=(j)) -> exists jt_b_completeenum jt_c_completeenum. ((((((exists fs_h_jt_completeenumsoundcode. fs_h_jt_completeenumsoundcode + S (jt_b_completeenum) = S ((S (jt_i_completeenum)) * B)) /\ exists fs_q_jt_completeenumsoundcode. A = fs_q_jt_completeenumsoundcode * S ((S (jt_i_completeenum)) * B) + (jt_b_completeenum))) /\ (((exists fs_h_jt_completeenumsoundscale. fs_h_jt_completeenumsoundscale + S (jt_c_completeenum) = S ((S (jt_i_completeenum)) * D)) /\ exists fs_q_jt_completeenumsoundscale. C = fs_q_jt_completeenumsoundscale * S ((S (jt_i_completeenum)) * D) + (jt_c_completeenum))))) /\ (((forall jt_index_completeenumbound. (exists jt_gap_completeenumboundindex. jt_gap_completeenumboundindex+S (jt_index_completeenumbound)=(k)) -> exists jt_value_completeenumbound. ((((exists fs_h_jt_completeenumboundat. fs_h_jt_completeenumboundat + S (jt_value_completeenumbound) = S ((S (jt_index_completeenumbound)) * jt_c_completeenum)) /\ exists fs_q_jt_completeenumboundat. jt_b_completeenum = fs_q_jt_completeenumboundat * S ((S (jt_index_completeenumbound)) * jt_c_completeenum) + (jt_value_completeenumbound))) /\ (exists jt_gap_completeenumboundvalue. jt_gap_completeenumboundvalue+S (jt_value_completeenumbound)=(n)))) /\ (forall jt_divisor_completeenumprimitive. (exists jt_factor_completeenumprimitivemodulus. (n)=(jt_divisor_completeenumprimitive)*jt_factor_completeenumprimitivemodulus) -> (forall jt_index_completeenumprimitivecoordinates jt_value_completeenumprimitivecoordinates. (exists jt_gap_completeenumprimitivecoordinatesindex. jt_gap_completeenumprimitivecoordinatesindex+S (jt_index_completeenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_completeenumprimitivecoordinatesat. fs_h_jt_completeenumprimitivecoordinatesat + S (jt_value_completeenumprimitivecoordinates) = S ((S (jt_index_completeenumprimitivecoordinates)) * jt_c_completeenum)) /\ exists fs_q_jt_completeenumprimitivecoordinatesat. jt_b_completeenum = fs_q_jt_completeenumprimitivecoordinatesat * S ((S (jt_index_completeenumprimitivecoordinates)) * jt_c_completeenum) + (jt_value_completeenumprimitivecoordinates))) -> (exists jt_factor_completeenumprimitivecoordinatesdivides. (jt_value_completeenumprimitivecoordinates)=(jt_divisor_completeenumprimitive)*jt_factor_completeenumprimitivecoordinatesdivides)) -> jt_divisor_completeenumprimitive=1))))) /\ (((forall jt_b_completeenum jt_c_completeenum. (forall jt_index_completeenuminputbound. (exists jt_gap_completeenuminputboundindex. jt_gap_completeenuminputboundindex+S (jt_index_completeenuminputbound)=(k)) -> exists jt_value_completeenuminputbound. ((((exists fs_h_jt_completeenuminputboundat. fs_h_jt_completeenuminputboundat + S (jt_value_completeenuminputbound) = S ((S (jt_index_completeenuminputbound)) * jt_c_completeenum)) /\ exists fs_q_jt_completeenuminputboundat. jt_b_completeenum = fs_q_jt_completeenuminputboundat * S ((S (jt_index_completeenuminputbound)) * jt_c_completeenum) + (jt_value_completeenuminputbound))) /\ (exists jt_gap_completeenuminputboundvalue. jt_gap_completeenuminputboundvalue+S (jt_value_completeenuminputbound)=(n)))) -> (forall jt_divisor_completeenuminputprimitive. (exists jt_factor_completeenuminputprimitivemodulus. (n)=(jt_divisor_completeenuminputprimitive)*jt_factor_completeenuminputprimitivemodulus) -> (forall jt_index_completeenuminputprimitivecoordinates jt_value_completeenuminputprimitivecoordinates. (exists jt_gap_completeenuminputprimitivecoordinatesindex. jt_gap_completeenuminputprimitivecoordinatesindex+S (jt_index_completeenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_completeenuminputprimitivecoordinatesat. fs_h_jt_completeenuminputprimitivecoordinatesat + S (jt_value_completeenuminputprimitivecoordinates) = S ((S (jt_index_completeenuminputprimitivecoordinates)) * jt_c_completeenum)) /\ exists fs_q_jt_completeenuminputprimitivecoordinatesat. jt_b_completeenum = fs_q_jt_completeenuminputprimitivecoordinatesat * S ((S (jt_index_completeenuminputprimitivecoordinates)) * jt_c_completeenum) + (jt_value_completeenuminputprimitivecoordinates))) -> (exists jt_factor_completeenuminputprimitivecoordinatesdivides. (jt_value_completeenuminputprimitivecoordinates)=(jt_divisor_completeenuminputprimitive)*jt_factor_completeenuminputprimitivecoordinatesdivides)) -> jt_divisor_completeenuminputprimitive=1) -> exists jt_i_completeenum jt_d_completeenum jt_e_completeenum. ((exists jt_gap_completeenumcompleteindex. jt_gap_completeenumcompleteindex+S (jt_i_completeenum)=(j)) /\ (((((((exists fs_h_jt_completeenumcompletecode. fs_h_jt_completeenumcompletecode + S (jt_d_completeenum) = S ((S (jt_i_completeenum)) * B)) /\ exists fs_q_jt_completeenumcompletecode. A = fs_q_jt_completeenumcompletecode * S ((S (jt_i_completeenum)) * B) + (jt_d_completeenum))) /\ (((exists fs_h_jt_completeenumcompletescale. fs_h_jt_completeenumcompletescale + S (jt_e_completeenum) = S ((S (jt_i_completeenum)) * D)) /\ exists fs_q_jt_completeenumcompletescale. C = fs_q_jt_completeenumcompletescale * S ((S (jt_i_completeenum)) * D) + (jt_e_completeenum))))) /\ (forall jt_index_completeenumrepresented jt_left_completeenumrepresented jt_right_completeenumrepresented. (exists jt_gap_completeenumrepresentedindex. jt_gap_completeenumrepresentedindex+S (jt_index_completeenumrepresented)=(k)) -> (((exists fs_h_jt_completeenumrepresentedleft. fs_h_jt_completeenumrepresentedleft + S (jt_left_completeenumrepresented) = S ((S (jt_index_completeenumrepresented)) * jt_c_completeenum)) /\ exists fs_q_jt_completeenumrepresentedleft. jt_b_completeenum = fs_q_jt_completeenumrepresentedleft * S ((S (jt_index_completeenumrepresented)) * jt_c_completeenum) + (jt_left_completeenumrepresented))) -> (((exists fs_h_jt_completeenumrepresentedright. fs_h_jt_completeenumrepresentedright + S (jt_right_completeenumrepresented) = S ((S (jt_index_completeenumrepresented)) * jt_e_completeenum)) /\ exists fs_q_jt_completeenumrepresentedright. jt_d_completeenum = fs_q_jt_completeenumrepresentedright * S ((S (jt_index_completeenumrepresented)) * jt_e_completeenum) + (jt_right_completeenumrepresented))) -> jt_left_completeenumrepresented=jt_right_completeenumrepresented))))) /\ (forall jt_i_completeenum jt_h_completeenum jt_b_completeenum jt_c_completeenum jt_d_completeenum jt_e_completeenum. (exists jt_gap_completeenumfirstindex. jt_gap_completeenumfirstindex+S (jt_i_completeenum)=(j)) -> (exists jt_gap_completeenumsecondindex. jt_gap_completeenumsecondindex+S (jt_h_completeenum)=(j)) -> (((((exists fs_h_jt_completeenumfirstcode. fs_h_jt_completeenumfirstcode + S (jt_b_completeenum) = S ((S (jt_i_completeenum)) * B)) /\ exists fs_q_jt_completeenumfirstcode. A = fs_q_jt_completeenumfirstcode * S ((S (jt_i_completeenum)) * B) + (jt_b_completeenum))) /\ (((exists fs_h_jt_completeenumfirstscale. fs_h_jt_completeenumfirstscale + S (jt_c_completeenum) = S ((S (jt_i_completeenum)) * D)) /\ exists fs_q_jt_completeenumfirstscale. C = fs_q_jt_completeenumfirstscale * S ((S (jt_i_completeenum)) * D) + (jt_c_completeenum))))) -> (((((exists fs_h_jt_completeenumsecondcode. fs_h_jt_completeenumsecondcode + S (jt_d_completeenum) = S ((S (jt_h_completeenum)) * B)) /\ exists fs_q_jt_completeenumsecondcode. A = fs_q_jt_completeenumsecondcode * S ((S (jt_h_completeenum)) * B) + (jt_d_completeenum))) /\ (((exists fs_h_jt_completeenumsecondscale. fs_h_jt_completeenumsecondscale + S (jt_e_completeenum) = S ((S (jt_h_completeenum)) * D)) /\ exists fs_q_jt_completeenumsecondscale. C = fs_q_jt_completeenumsecondscale * S ((S (jt_h_completeenum)) * D) + (jt_e_completeenum))))) -> (forall jt_index_completeenumsame jt_left_completeenumsame jt_right_completeenumsame. (exists jt_gap_completeenumsameindex. jt_gap_completeenumsameindex+S (jt_index_completeenumsame)=(k)) -> (((exists fs_h_jt_completeenumsameleft. fs_h_jt_completeenumsameleft + S (jt_left_completeenumsame) = S ((S (jt_index_completeenumsame)) * jt_c_completeenum)) /\ exists fs_q_jt_completeenumsameleft. jt_b_completeenum = fs_q_jt_completeenumsameleft * S ((S (jt_index_completeenumsame)) * jt_c_completeenum) + (jt_left_completeenumsame))) -> (((exists fs_h_jt_completeenumsameright. fs_h_jt_completeenumsameright + S (jt_right_completeenumsame) = S ((S (jt_index_completeenumsame)) * jt_e_completeenum)) /\ exists fs_q_jt_completeenumsameright. jt_d_completeenum = fs_q_jt_completeenumsameright * S ((S (jt_index_completeenumsame)) * jt_e_completeenum) + (jt_right_completeenumsame))) -> jt_left_completeenumsame=jt_right_completeenumsame) -> jt_i_completeenum=jt_h_completeenum))))) -> (forall jt_index_completebound. (exists jt_gap_completeboundindex. jt_gap_completeboundindex+S (jt_index_completebound)=(k)) -> exists jt_value_completebound. ((((exists fs_h_jt_completeboundat. fs_h_jt_completeboundat + S (jt_value_completebound) = S ((S (jt_index_completebound)) * c)) /\ exists fs_q_jt_completeboundat. b = fs_q_jt_completeboundat * S ((S (jt_index_completebound)) * c) + (jt_value_completebound))) /\ (exists jt_gap_completeboundvalue. jt_gap_completeboundvalue+S (jt_value_completebound)=(n)))) -> (forall jt_divisor_completeprimitive. (exists jt_factor_completeprimitivemodulus. (n)=(jt_divisor_completeprimitive)*jt_factor_completeprimitivemodulus) -> (forall jt_index_completeprimitivecoordinates jt_value_completeprimitivecoordinates. (exists jt_gap_completeprimitivecoordinatesindex. jt_gap_completeprimitivecoordinatesindex+S (jt_index_completeprimitivecoordinates)=(k)) -> (((exists fs_h_jt_completeprimitivecoordinatesat. fs_h_jt_completeprimitivecoordinatesat + S (jt_value_completeprimitivecoordinates) = S ((S (jt_index_completeprimitivecoordinates)) * c)) /\ exists fs_q_jt_completeprimitivecoordinatesat. b = fs_q_jt_completeprimitivecoordinatesat * S ((S (jt_index_completeprimitivecoordinates)) * c) + (jt_value_completeprimitivecoordinates))) -> (exists jt_factor_completeprimitivecoordinatesdivides. (jt_value_completeprimitivecoordinates)=(jt_divisor_completeprimitive)*jt_factor_completeprimitivecoordinatesdivides)) -> jt_divisor_completeprimitive=1) -> (exists jt_index_completelisted jt_code_completelisted jt_scale_completelisted. ((exists jt_gap_completelistedindex. jt_gap_completelistedindex+S (jt_index_completelisted)=(j)) /\ (((((((exists fs_h_jt_completelistedcode. fs_h_jt_completelistedcode + S (jt_code_completelisted) = S ((S (jt_index_completelisted)) * B)) /\ exists fs_q_jt_completelistedcode. A = fs_q_jt_completelistedcode * S ((S (jt_index_completelisted)) * B) + (jt_code_completelisted))) /\ (((exists fs_h_jt_completelistedscale. fs_h_jt_completelistedscale + S (jt_scale_completelisted) = S ((S (jt_index_completelisted)) * D)) /\ exists fs_q_jt_completelistedscale. C = fs_q_jt_completelistedscale * S ((S (jt_index_completelisted)) * D) + (jt_scale_completelisted))))) /\ (forall jt_index_completelistedequal jt_left_completelistedequal jt_right_completelistedequal. (exists jt_gap_completelistedequalindex. jt_gap_completelistedequalindex+S (jt_index_completelistedequal)=(k)) -> (((exists fs_h_jt_completelistedequalleft. fs_h_jt_completelistedequalleft + S (jt_left_completelistedequal) = S ((S (jt_index_completelistedequal)) * c)) /\ exists fs_q_jt_completelistedequalleft. b = fs_q_jt_completelistedequalleft * S ((S (jt_index_completelistedequal)) * c) + (jt_left_completelistedequal))) -> (((exists fs_h_jt_completelistedequalright. fs_h_jt_completelistedequalright + S (jt_right_completelistedequal) = S ((S (jt_index_completelistedequal)) * jt_scale_completelisted)) /\ exists fs_q_jt_completelistedequalright. jt_code_completelisted = fs_q_jt_completelistedequalright * S ((S (jt_index_completelistedequal)) * jt_scale_completelisted) + (jt_right_completelistedequal))) -> jt_left_completelistedequal=jt_right_completelistedequal)))))