jordan_totient_from_complete_scan

Exact expanded first-order arithmetic statement

forall k n c T B C D E j. ~(k=0) -> ~(n=0) -> (forall jt_code_jordanbox jt_scale_jordanbox. (forall jt_index_jordanboxbound. (exists jt_gap_jordanboxboundindex. jt_gap_jordanboxboundindex+S (jt_index_jordanboxbound)=(k)) -> exists jt_value_jordanboxbound. ((((exists fs_h_jt_jordanboxboundat. fs_h_jt_jordanboxboundat + S (jt_value_jordanboxbound) = S ((S (jt_index_jordanboxbound)) * jt_scale_jordanbox)) /\ exists fs_q_jt_jordanboxboundat. jt_code_jordanbox = fs_q_jt_jordanboxboundat * S ((S (jt_index_jordanboxbound)) * jt_scale_jordanbox) + (jt_value_jordanboxbound))) /\ (exists jt_gap_jordanboxboundvalue. jt_gap_jordanboxboundvalue+S (jt_value_jordanboxbound)=(n)))) -> exists jt_representative_jordanbox. ((exists jt_gap_jordanboxindex. jt_gap_jordanboxindex+S (jt_representative_jordanbox)=(T)) /\ (forall jt_index_jordanboxequal jt_left_jordanboxequal jt_right_jordanboxequal. (exists jt_gap_jordanboxequalindex. jt_gap_jordanboxequalindex+S (jt_index_jordanboxequal)=(k)) -> (((exists fs_h_jt_jordanboxequalleft. fs_h_jt_jordanboxequalleft + S (jt_left_jordanboxequal) = S ((S (jt_index_jordanboxequal)) * jt_scale_jordanbox)) /\ exists fs_q_jt_jordanboxequalleft. jt_code_jordanbox = fs_q_jt_jordanboxequalleft * S ((S (jt_index_jordanboxequal)) * jt_scale_jordanbox) + (jt_left_jordanboxequal))) -> (((exists fs_h_jt_jordanboxequalright. fs_h_jt_jordanboxequalright + S (jt_right_jordanboxequal) = S ((S (jt_index_jordanboxequal)) * c)) /\ exists fs_q_jt_jordanboxequalright. jt_representative_jordanbox = fs_q_jt_jordanboxequalright * S ((S (jt_index_jordanboxequal)) * c) + (jt_right_jordanboxequal))) -> jt_left_jordanboxequal=jt_right_jordanboxequal))) -> (((forall jt_i_jordanscan. (exists jt_gap_jordanscansoundindex. jt_gap_jordanscansoundindex+S (jt_i_jordanscan)=(j)) -> exists jt_b_jordanscan jt_e_jordanscan. ((((((exists fs_h_jt_jordanscansoundcode. fs_h_jt_jordanscansoundcode + S (jt_b_jordanscan) = S ((S (jt_i_jordanscan)) * C)) /\ exists fs_q_jt_jordanscansoundcode. B = fs_q_jt_jordanscansoundcode * S ((S (jt_i_jordanscan)) * C) + (jt_b_jordanscan))) /\ (((exists fs_h_jt_jordanscansoundscale. fs_h_jt_jordanscansoundscale + S (jt_e_jordanscan) = S ((S (jt_i_jordanscan)) * E)) /\ exists fs_q_jt_jordanscansoundscale. D = fs_q_jt_jordanscansoundscale * S ((S (jt_i_jordanscan)) * E) + (jt_e_jordanscan))))) /\ (((forall jt_index_jordanscanbound. (exists jt_gap_jordanscanboundindex. jt_gap_jordanscanboundindex+S (jt_index_jordanscanbound)=(k)) -> exists jt_value_jordanscanbound. ((((exists fs_h_jt_jordanscanboundat. fs_h_jt_jordanscanboundat + S (jt_value_jordanscanbound) = S ((S (jt_index_jordanscanbound)) * jt_e_jordanscan)) /\ exists fs_q_jt_jordanscanboundat. jt_b_jordanscan = fs_q_jt_jordanscanboundat * S ((S (jt_index_jordanscanbound)) * jt_e_jordanscan) + (jt_value_jordanscanbound))) /\ (exists jt_gap_jordanscanboundvalue. jt_gap_jordanscanboundvalue+S (jt_value_jordanscanbound)=(n)))) /\ (forall jt_divisor_jordanscanprimitive. (exists jt_factor_jordanscanprimitivemodulus. (n)=(jt_divisor_jordanscanprimitive)*jt_factor_jordanscanprimitivemodulus) -> (forall jt_index_jordanscanprimitivecoordinates jt_value_jordanscanprimitivecoordinates. (exists jt_gap_jordanscanprimitivecoordinatesindex. jt_gap_jordanscanprimitivecoordinatesindex+S (jt_index_jordanscanprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jordanscanprimitivecoordinatesat. fs_h_jt_jordanscanprimitivecoordinatesat + S (jt_value_jordanscanprimitivecoordinates) = S ((S (jt_index_jordanscanprimitivecoordinates)) * jt_e_jordanscan)) /\ exists fs_q_jt_jordanscanprimitivecoordinatesat. jt_b_jordanscan = fs_q_jt_jordanscanprimitivecoordinatesat * S ((S (jt_index_jordanscanprimitivecoordinates)) * jt_e_jordanscan) + (jt_value_jordanscanprimitivecoordinates))) -> (exists jt_factor_jordanscanprimitivecoordinatesdivides. (jt_value_jordanscanprimitivecoordinates)=(jt_divisor_jordanscanprimitive)*jt_factor_jordanscanprimitivecoordinatesdivides)) -> jt_divisor_jordanscanprimitive=1))))) /\ (((forall jt_i_jordanscan jt_h_jordanscan jt_b_jordanscan jt_e_jordanscan jt_d_jordanscan jt_f_jordanscan. (exists jt_gap_jordanscanfirstindex. jt_gap_jordanscanfirstindex+S (jt_i_jordanscan)=(j)) -> (exists jt_gap_jordanscansecondindex. jt_gap_jordanscansecondindex+S (jt_h_jordanscan)=(j)) -> (((((exists fs_h_jt_jordanscanfirstcode. fs_h_jt_jordanscanfirstcode + S (jt_b_jordanscan) = S ((S (jt_i_jordanscan)) * C)) /\ exists fs_q_jt_jordanscanfirstcode. B = fs_q_jt_jordanscanfirstcode * S ((S (jt_i_jordanscan)) * C) + (jt_b_jordanscan))) /\ (((exists fs_h_jt_jordanscanfirstscale. fs_h_jt_jordanscanfirstscale + S (jt_e_jordanscan) = S ((S (jt_i_jordanscan)) * E)) /\ exists fs_q_jt_jordanscanfirstscale. D = fs_q_jt_jordanscanfirstscale * S ((S (jt_i_jordanscan)) * E) + (jt_e_jordanscan))))) -> (((((exists fs_h_jt_jordanscansecondcode. fs_h_jt_jordanscansecondcode + S (jt_d_jordanscan) = S ((S (jt_h_jordanscan)) * C)) /\ exists fs_q_jt_jordanscansecondcode. B = fs_q_jt_jordanscansecondcode * S ((S (jt_h_jordanscan)) * C) + (jt_d_jordanscan))) /\ (((exists fs_h_jt_jordanscansecondscale. fs_h_jt_jordanscansecondscale + S (jt_f_jordanscan) = S ((S (jt_h_jordanscan)) * E)) /\ exists fs_q_jt_jordanscansecondscale. D = fs_q_jt_jordanscansecondscale * S ((S (jt_h_jordanscan)) * E) + (jt_f_jordanscan))))) -> (forall jt_index_jordanscansame jt_left_jordanscansame jt_right_jordanscansame. (exists jt_gap_jordanscansameindex. jt_gap_jordanscansameindex+S (jt_index_jordanscansame)=(k)) -> (((exists fs_h_jt_jordanscansameleft. fs_h_jt_jordanscansameleft + S (jt_left_jordanscansame) = S ((S (jt_index_jordanscansame)) * jt_e_jordanscan)) /\ exists fs_q_jt_jordanscansameleft. jt_b_jordanscan = fs_q_jt_jordanscansameleft * S ((S (jt_index_jordanscansame)) * jt_e_jordanscan) + (jt_left_jordanscansame))) -> (((exists fs_h_jt_jordanscansameright. fs_h_jt_jordanscansameright + S (jt_right_jordanscansame) = S ((S (jt_index_jordanscansame)) * jt_f_jordanscan)) /\ exists fs_q_jt_jordanscansameright. jt_d_jordanscan = fs_q_jt_jordanscansameright * S ((S (jt_index_jordanscansame)) * jt_f_jordanscan) + (jt_right_jordanscansame))) -> jt_left_jordanscansame=jt_right_jordanscansame) -> jt_i_jordanscan=jt_h_jordanscan) /\ (forall jt_z_jordanscan. (exists jt_gap_jordanscancodeindex. jt_gap_jordanscancodeindex+S (jt_z_jordanscan)=(T)) -> (forall jt_index_jordanscaninputbound. (exists jt_gap_jordanscaninputboundindex. jt_gap_jordanscaninputboundindex+S (jt_index_jordanscaninputbound)=(k)) -> exists jt_value_jordanscaninputbound. ((((exists fs_h_jt_jordanscaninputboundat. fs_h_jt_jordanscaninputboundat + S (jt_value_jordanscaninputbound) = S ((S (jt_index_jordanscaninputbound)) * c)) /\ exists fs_q_jt_jordanscaninputboundat. jt_z_jordanscan = fs_q_jt_jordanscaninputboundat * S ((S (jt_index_jordanscaninputbound)) * c) + (jt_value_jordanscaninputbound))) /\ (exists jt_gap_jordanscaninputboundvalue. jt_gap_jordanscaninputboundvalue+S (jt_value_jordanscaninputbound)=(n)))) -> (forall jt_divisor_jordanscaninputprimitive. (exists jt_factor_jordanscaninputprimitivemodulus. (n)=(jt_divisor_jordanscaninputprimitive)*jt_factor_jordanscaninputprimitivemodulus) -> (forall jt_index_jordanscaninputprimitivecoordinates jt_value_jordanscaninputprimitivecoordinates. (exists jt_gap_jordanscaninputprimitivecoordinatesindex. jt_gap_jordanscaninputprimitivecoordinatesindex+S (jt_index_jordanscaninputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jordanscaninputprimitivecoordinatesat. fs_h_jt_jordanscaninputprimitivecoordinatesat + S (jt_value_jordanscaninputprimitivecoordinates) = S ((S (jt_index_jordanscaninputprimitivecoordinates)) * c)) /\ exists fs_q_jt_jordanscaninputprimitivecoordinatesat. jt_z_jordanscan = fs_q_jt_jordanscaninputprimitivecoordinatesat * S ((S (jt_index_jordanscaninputprimitivecoordinates)) * c) + (jt_value_jordanscaninputprimitivecoordinates))) -> (exists jt_factor_jordanscaninputprimitivecoordinatesdivides. (jt_value_jordanscaninputprimitivecoordinates)=(jt_divisor_jordanscaninputprimitive)*jt_factor_jordanscaninputprimitivecoordinatesdivides)) -> jt_divisor_jordanscaninputprimitive=1) -> (exists jt_index_jordanscanlisted jt_code_jordanscanlisted jt_scale_jordanscanlisted. ((exists jt_gap_jordanscanlistedindex. jt_gap_jordanscanlistedindex+S (jt_index_jordanscanlisted)=(j)) /\ (((((((exists fs_h_jt_jordanscanlistedcode. fs_h_jt_jordanscanlistedcode + S (jt_code_jordanscanlisted) = S ((S (jt_index_jordanscanlisted)) * C)) /\ exists fs_q_jt_jordanscanlistedcode. B = fs_q_jt_jordanscanlistedcode * S ((S (jt_index_jordanscanlisted)) * C) + (jt_code_jordanscanlisted))) /\ (((exists fs_h_jt_jordanscanlistedscale. fs_h_jt_jordanscanlistedscale + S (jt_scale_jordanscanlisted) = S ((S (jt_index_jordanscanlisted)) * E)) /\ exists fs_q_jt_jordanscanlistedscale. D = fs_q_jt_jordanscanlistedscale * S ((S (jt_index_jordanscanlisted)) * E) + (jt_scale_jordanscanlisted))))) /\ (forall jt_index_jordanscanlistedequal jt_left_jordanscanlistedequal jt_right_jordanscanlistedequal. (exists jt_gap_jordanscanlistedequalindex. jt_gap_jordanscanlistedequalindex+S (jt_index_jordanscanlistedequal)=(k)) -> (((exists fs_h_jt_jordanscanlistedequalleft. fs_h_jt_jordanscanlistedequalleft + S (jt_left_jordanscanlistedequal) = S ((S (jt_index_jordanscanlistedequal)) * c)) /\ exists fs_q_jt_jordanscanlistedequalleft. jt_z_jordanscan = fs_q_jt_jordanscanlistedequalleft * S ((S (jt_index_jordanscanlistedequal)) * c) + (jt_left_jordanscanlistedequal))) -> (((exists fs_h_jt_jordanscanlistedequalright. fs_h_jt_jordanscanlistedequalright + S (jt_right_jordanscanlistedequal) = S ((S (jt_index_jordanscanlistedequal)) * jt_scale_jordanscanlisted)) /\ exists fs_q_jt_jordanscanlistedequalright. jt_code_jordanscanlisted = fs_q_jt_jordanscanlistedequalright * S ((S (jt_index_jordanscanlistedequal)) * jt_scale_jordanscanlisted) + (jt_right_jordanscanlistedequal))) -> jt_left_jordanscanlistedequal=jt_right_jordanscanlistedequal)))))))))) -> (((~((k)=0)) /\ (((~((n)=0)) /\ (exists jt_codes_jordancount jt_code_scale_jordancount jt_scales_jordancount jt_scale_scale_jordancount. ((forall jt_i_jordancountenum. (exists jt_gap_jordancountenumsoundindex. jt_gap_jordancountenumsoundindex+S (jt_i_jordancountenum)=(j)) -> exists jt_b_jordancountenum jt_c_jordancountenum. ((((((exists fs_h_jt_jordancountenumsoundcode. fs_h_jt_jordancountenumsoundcode + S (jt_b_jordancountenum) = S ((S (jt_i_jordancountenum)) * jt_code_scale_jordancount)) /\ exists fs_q_jt_jordancountenumsoundcode. jt_codes_jordancount = fs_q_jt_jordancountenumsoundcode * S ((S (jt_i_jordancountenum)) * jt_code_scale_jordancount) + (jt_b_jordancountenum))) /\ (((exists fs_h_jt_jordancountenumsoundscale. fs_h_jt_jordancountenumsoundscale + S (jt_c_jordancountenum) = S ((S (jt_i_jordancountenum)) * jt_scale_scale_jordancount)) /\ exists fs_q_jt_jordancountenumsoundscale. jt_scales_jordancount = fs_q_jt_jordancountenumsoundscale * S ((S (jt_i_jordancountenum)) * jt_scale_scale_jordancount) + (jt_c_jordancountenum))))) /\ (((forall jt_index_jordancountenumbound. (exists jt_gap_jordancountenumboundindex. jt_gap_jordancountenumboundindex+S (jt_index_jordancountenumbound)=(k)) -> exists jt_value_jordancountenumbound. ((((exists fs_h_jt_jordancountenumboundat. fs_h_jt_jordancountenumboundat + S (jt_value_jordancountenumbound) = S ((S (jt_index_jordancountenumbound)) * jt_c_jordancountenum)) /\ exists fs_q_jt_jordancountenumboundat. jt_b_jordancountenum = fs_q_jt_jordancountenumboundat * S ((S (jt_index_jordancountenumbound)) * jt_c_jordancountenum) + (jt_value_jordancountenumbound))) /\ (exists jt_gap_jordancountenumboundvalue. jt_gap_jordancountenumboundvalue+S (jt_value_jordancountenumbound)=(n)))) /\ (forall jt_divisor_jordancountenumprimitive. (exists jt_factor_jordancountenumprimitivemodulus. (n)=(jt_divisor_jordancountenumprimitive)*jt_factor_jordancountenumprimitivemodulus) -> (forall jt_index_jordancountenumprimitivecoordinates jt_value_jordancountenumprimitivecoordinates. (exists jt_gap_jordancountenumprimitivecoordinatesindex. jt_gap_jordancountenumprimitivecoordinatesindex+S (jt_index_jordancountenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jordancountenumprimitivecoordinatesat. fs_h_jt_jordancountenumprimitivecoordinatesat + S (jt_value_jordancountenumprimitivecoordinates) = S ((S (jt_index_jordancountenumprimitivecoordinates)) * jt_c_jordancountenum)) /\ exists fs_q_jt_jordancountenumprimitivecoordinatesat. jt_b_jordancountenum = fs_q_jt_jordancountenumprimitivecoordinatesat * S ((S (jt_index_jordancountenumprimitivecoordinates)) * jt_c_jordancountenum) + (jt_value_jordancountenumprimitivecoordinates))) -> (exists jt_factor_jordancountenumprimitivecoordinatesdivides. (jt_value_jordancountenumprimitivecoordinates)=(jt_divisor_jordancountenumprimitive)*jt_factor_jordancountenumprimitivecoordinatesdivides)) -> jt_divisor_jordancountenumprimitive=1))))) /\ (((forall jt_b_jordancountenum jt_c_jordancountenum. (forall jt_index_jordancountenuminputbound. (exists jt_gap_jordancountenuminputboundindex. jt_gap_jordancountenuminputboundindex+S (jt_index_jordancountenuminputbound)=(k)) -> exists jt_value_jordancountenuminputbound. ((((exists fs_h_jt_jordancountenuminputboundat. fs_h_jt_jordancountenuminputboundat + S (jt_value_jordancountenuminputbound) = S ((S (jt_index_jordancountenuminputbound)) * jt_c_jordancountenum)) /\ exists fs_q_jt_jordancountenuminputboundat. jt_b_jordancountenum = fs_q_jt_jordancountenuminputboundat * S ((S (jt_index_jordancountenuminputbound)) * jt_c_jordancountenum) + (jt_value_jordancountenuminputbound))) /\ (exists jt_gap_jordancountenuminputboundvalue. jt_gap_jordancountenuminputboundvalue+S (jt_value_jordancountenuminputbound)=(n)))) -> (forall jt_divisor_jordancountenuminputprimitive. (exists jt_factor_jordancountenuminputprimitivemodulus. (n)=(jt_divisor_jordancountenuminputprimitive)*jt_factor_jordancountenuminputprimitivemodulus) -> (forall jt_index_jordancountenuminputprimitivecoordinates jt_value_jordancountenuminputprimitivecoordinates. (exists jt_gap_jordancountenuminputprimitivecoordinatesindex. jt_gap_jordancountenuminputprimitivecoordinatesindex+S (jt_index_jordancountenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jordancountenuminputprimitivecoordinatesat. fs_h_jt_jordancountenuminputprimitivecoordinatesat + S (jt_value_jordancountenuminputprimitivecoordinates) = S ((S (jt_index_jordancountenuminputprimitivecoordinates)) * jt_c_jordancountenum)) /\ exists fs_q_jt_jordancountenuminputprimitivecoordinatesat. jt_b_jordancountenum = fs_q_jt_jordancountenuminputprimitivecoordinatesat * S ((S (jt_index_jordancountenuminputprimitivecoordinates)) * jt_c_jordancountenum) + (jt_value_jordancountenuminputprimitivecoordinates))) -> (exists jt_factor_jordancountenuminputprimitivecoordinatesdivides. (jt_value_jordancountenuminputprimitivecoordinates)=(jt_divisor_jordancountenuminputprimitive)*jt_factor_jordancountenuminputprimitivecoordinatesdivides)) -> jt_divisor_jordancountenuminputprimitive=1) -> exists jt_i_jordancountenum jt_d_jordancountenum jt_e_jordancountenum. ((exists jt_gap_jordancountenumcompleteindex. jt_gap_jordancountenumcompleteindex+S (jt_i_jordancountenum)=(j)) /\ (((((((exists fs_h_jt_jordancountenumcompletecode. fs_h_jt_jordancountenumcompletecode + S (jt_d_jordancountenum) = S ((S (jt_i_jordancountenum)) * jt_code_scale_jordancount)) /\ exists fs_q_jt_jordancountenumcompletecode. jt_codes_jordancount = fs_q_jt_jordancountenumcompletecode * S ((S (jt_i_jordancountenum)) * jt_code_scale_jordancount) + (jt_d_jordancountenum))) /\ (((exists fs_h_jt_jordancountenumcompletescale. fs_h_jt_jordancountenumcompletescale + S (jt_e_jordancountenum) = S ((S (jt_i_jordancountenum)) * jt_scale_scale_jordancount)) /\ exists fs_q_jt_jordancountenumcompletescale. jt_scales_jordancount = fs_q_jt_jordancountenumcompletescale * S ((S (jt_i_jordancountenum)) * jt_scale_scale_jordancount) + (jt_e_jordancountenum))))) /\ (forall jt_index_jordancountenumrepresented jt_left_jordancountenumrepresented jt_right_jordancountenumrepresented. (exists jt_gap_jordancountenumrepresentedindex. jt_gap_jordancountenumrepresentedindex+S (jt_index_jordancountenumrepresented)=(k)) -> (((exists fs_h_jt_jordancountenumrepresentedleft. fs_h_jt_jordancountenumrepresentedleft + S (jt_left_jordancountenumrepresented) = S ((S (jt_index_jordancountenumrepresented)) * jt_c_jordancountenum)) /\ exists fs_q_jt_jordancountenumrepresentedleft. jt_b_jordancountenum = fs_q_jt_jordancountenumrepresentedleft * S ((S (jt_index_jordancountenumrepresented)) * jt_c_jordancountenum) + (jt_left_jordancountenumrepresented))) -> (((exists fs_h_jt_jordancountenumrepresentedright. fs_h_jt_jordancountenumrepresentedright + S (jt_right_jordancountenumrepresented) = S ((S (jt_index_jordancountenumrepresented)) * jt_e_jordancountenum)) /\ exists fs_q_jt_jordancountenumrepresentedright. jt_d_jordancountenum = fs_q_jt_jordancountenumrepresentedright * S ((S (jt_index_jordancountenumrepresented)) * jt_e_jordancountenum) + (jt_right_jordancountenumrepresented))) -> jt_left_jordancountenumrepresented=jt_right_jordancountenumrepresented))))) /\ (forall jt_i_jordancountenum jt_h_jordancountenum jt_b_jordancountenum jt_c_jordancountenum jt_d_jordancountenum jt_e_jordancountenum. (exists jt_gap_jordancountenumfirstindex. jt_gap_jordancountenumfirstindex+S (jt_i_jordancountenum)=(j)) -> (exists jt_gap_jordancountenumsecondindex. jt_gap_jordancountenumsecondindex+S (jt_h_jordancountenum)=(j)) -> (((((exists fs_h_jt_jordancountenumfirstcode. fs_h_jt_jordancountenumfirstcode + S (jt_b_jordancountenum) = S ((S (jt_i_jordancountenum)) * jt_code_scale_jordancount)) /\ exists fs_q_jt_jordancountenumfirstcode. jt_codes_jordancount = fs_q_jt_jordancountenumfirstcode * S ((S (jt_i_jordancountenum)) * jt_code_scale_jordancount) + (jt_b_jordancountenum))) /\ (((exists fs_h_jt_jordancountenumfirstscale. fs_h_jt_jordancountenumfirstscale + S (jt_c_jordancountenum) = S ((S (jt_i_jordancountenum)) * jt_scale_scale_jordancount)) /\ exists fs_q_jt_jordancountenumfirstscale. jt_scales_jordancount = fs_q_jt_jordancountenumfirstscale * S ((S (jt_i_jordancountenum)) * jt_scale_scale_jordancount) + (jt_c_jordancountenum))))) -> (((((exists fs_h_jt_jordancountenumsecondcode. fs_h_jt_jordancountenumsecondcode + S (jt_d_jordancountenum) = S ((S (jt_h_jordancountenum)) * jt_code_scale_jordancount)) /\ exists fs_q_jt_jordancountenumsecondcode. jt_codes_jordancount = fs_q_jt_jordancountenumsecondcode * S ((S (jt_h_jordancountenum)) * jt_code_scale_jordancount) + (jt_d_jordancountenum))) /\ (((exists fs_h_jt_jordancountenumsecondscale. fs_h_jt_jordancountenumsecondscale + S (jt_e_jordancountenum) = S ((S (jt_h_jordancountenum)) * jt_scale_scale_jordancount)) /\ exists fs_q_jt_jordancountenumsecondscale. jt_scales_jordancount = fs_q_jt_jordancountenumsecondscale * S ((S (jt_h_jordancountenum)) * jt_scale_scale_jordancount) + (jt_e_jordancountenum))))) -> (forall jt_index_jordancountenumsame jt_left_jordancountenumsame jt_right_jordancountenumsame. (exists jt_gap_jordancountenumsameindex. jt_gap_jordancountenumsameindex+S (jt_index_jordancountenumsame)=(k)) -> (((exists fs_h_jt_jordancountenumsameleft. fs_h_jt_jordancountenumsameleft + S (jt_left_jordancountenumsame) = S ((S (jt_index_jordancountenumsame)) * jt_c_jordancountenum)) /\ exists fs_q_jt_jordancountenumsameleft. jt_b_jordancountenum = fs_q_jt_jordancountenumsameleft * S ((S (jt_index_jordancountenumsame)) * jt_c_jordancountenum) + (jt_left_jordancountenumsame))) -> (((exists fs_h_jt_jordancountenumsameright. fs_h_jt_jordancountenumsameright + S (jt_right_jordancountenumsame) = S ((S (jt_index_jordancountenumsame)) * jt_e_jordancountenum)) /\ exists fs_q_jt_jordancountenumsameright. jt_d_jordancountenum = fs_q_jt_jordancountenumsameright * S ((S (jt_index_jordancountenumsame)) * jt_e_jordancountenum) + (jt_right_jordancountenumsame))) -> jt_left_jordancountenumsame=jt_right_jordancountenumsame) -> jt_i_jordancountenum=jt_h_jordancountenum)))))))))