jordan_tuple_scan_complete

Exact expanded first-order arithmetic statement

forall k n c T B C D E j. (forall jt_code_completebox jt_scale_completebox. (forall jt_index_completeboxbound. (exists jt_gap_completeboxboundindex. jt_gap_completeboxboundindex+S (jt_index_completeboxbound)=(k)) -> exists jt_value_completeboxbound. ((((exists fs_h_jt_completeboxboundat. fs_h_jt_completeboxboundat + S (jt_value_completeboxbound) = S ((S (jt_index_completeboxbound)) * jt_scale_completebox)) /\ exists fs_q_jt_completeboxboundat. jt_code_completebox = fs_q_jt_completeboxboundat * S ((S (jt_index_completeboxbound)) * jt_scale_completebox) + (jt_value_completeboxbound))) /\ (exists jt_gap_completeboxboundvalue. jt_gap_completeboxboundvalue+S (jt_value_completeboxbound)=(n)))) -> exists jt_representative_completebox. ((exists jt_gap_completeboxindex. jt_gap_completeboxindex+S (jt_representative_completebox)=(T)) /\ (forall jt_index_completeboxequal jt_left_completeboxequal jt_right_completeboxequal. (exists jt_gap_completeboxequalindex. jt_gap_completeboxequalindex+S (jt_index_completeboxequal)=(k)) -> (((exists fs_h_jt_completeboxequalleft. fs_h_jt_completeboxequalleft + S (jt_left_completeboxequal) = S ((S (jt_index_completeboxequal)) * jt_scale_completebox)) /\ exists fs_q_jt_completeboxequalleft. jt_code_completebox = fs_q_jt_completeboxequalleft * S ((S (jt_index_completeboxequal)) * jt_scale_completebox) + (jt_left_completeboxequal))) -> (((exists fs_h_jt_completeboxequalright. fs_h_jt_completeboxequalright + S (jt_right_completeboxequal) = S ((S (jt_index_completeboxequal)) * c)) /\ exists fs_q_jt_completeboxequalright. jt_representative_completebox = fs_q_jt_completeboxequalright * S ((S (jt_index_completeboxequal)) * c) + (jt_right_completeboxequal))) -> jt_left_completeboxequal=jt_right_completeboxequal))) -> (((forall jt_i_completescan. (exists jt_gap_completescansoundindex. jt_gap_completescansoundindex+S (jt_i_completescan)=(j)) -> exists jt_b_completescan jt_e_completescan. ((((((exists fs_h_jt_completescansoundcode. fs_h_jt_completescansoundcode + S (jt_b_completescan) = S ((S (jt_i_completescan)) * C)) /\ exists fs_q_jt_completescansoundcode. B = fs_q_jt_completescansoundcode * S ((S (jt_i_completescan)) * C) + (jt_b_completescan))) /\ (((exists fs_h_jt_completescansoundscale. fs_h_jt_completescansoundscale + S (jt_e_completescan) = S ((S (jt_i_completescan)) * E)) /\ exists fs_q_jt_completescansoundscale. D = fs_q_jt_completescansoundscale * S ((S (jt_i_completescan)) * E) + (jt_e_completescan))))) /\ (((forall jt_index_completescanbound. (exists jt_gap_completescanboundindex. jt_gap_completescanboundindex+S (jt_index_completescanbound)=(k)) -> exists jt_value_completescanbound. ((((exists fs_h_jt_completescanboundat. fs_h_jt_completescanboundat + S (jt_value_completescanbound) = S ((S (jt_index_completescanbound)) * jt_e_completescan)) /\ exists fs_q_jt_completescanboundat. jt_b_completescan = fs_q_jt_completescanboundat * S ((S (jt_index_completescanbound)) * jt_e_completescan) + (jt_value_completescanbound))) /\ (exists jt_gap_completescanboundvalue. jt_gap_completescanboundvalue+S (jt_value_completescanbound)=(n)))) /\ (forall jt_divisor_completescanprimitive. (exists jt_factor_completescanprimitivemodulus. (n)=(jt_divisor_completescanprimitive)*jt_factor_completescanprimitivemodulus) -> (forall jt_index_completescanprimitivecoordinates jt_value_completescanprimitivecoordinates. (exists jt_gap_completescanprimitivecoordinatesindex. jt_gap_completescanprimitivecoordinatesindex+S (jt_index_completescanprimitivecoordinates)=(k)) -> (((exists fs_h_jt_completescanprimitivecoordinatesat. fs_h_jt_completescanprimitivecoordinatesat + S (jt_value_completescanprimitivecoordinates) = S ((S (jt_index_completescanprimitivecoordinates)) * jt_e_completescan)) /\ exists fs_q_jt_completescanprimitivecoordinatesat. jt_b_completescan = fs_q_jt_completescanprimitivecoordinatesat * S ((S (jt_index_completescanprimitivecoordinates)) * jt_e_completescan) + (jt_value_completescanprimitivecoordinates))) -> (exists jt_factor_completescanprimitivecoordinatesdivides. (jt_value_completescanprimitivecoordinates)=(jt_divisor_completescanprimitive)*jt_factor_completescanprimitivecoordinatesdivides)) -> jt_divisor_completescanprimitive=1))))) /\ (((forall jt_i_completescan jt_h_completescan jt_b_completescan jt_e_completescan jt_d_completescan jt_f_completescan. (exists jt_gap_completescanfirstindex. jt_gap_completescanfirstindex+S (jt_i_completescan)=(j)) -> (exists jt_gap_completescansecondindex. jt_gap_completescansecondindex+S (jt_h_completescan)=(j)) -> (((((exists fs_h_jt_completescanfirstcode. fs_h_jt_completescanfirstcode + S (jt_b_completescan) = S ((S (jt_i_completescan)) * C)) /\ exists fs_q_jt_completescanfirstcode. B = fs_q_jt_completescanfirstcode * S ((S (jt_i_completescan)) * C) + (jt_b_completescan))) /\ (((exists fs_h_jt_completescanfirstscale. fs_h_jt_completescanfirstscale + S (jt_e_completescan) = S ((S (jt_i_completescan)) * E)) /\ exists fs_q_jt_completescanfirstscale. D = fs_q_jt_completescanfirstscale * S ((S (jt_i_completescan)) * E) + (jt_e_completescan))))) -> (((((exists fs_h_jt_completescansecondcode. fs_h_jt_completescansecondcode + S (jt_d_completescan) = S ((S (jt_h_completescan)) * C)) /\ exists fs_q_jt_completescansecondcode. B = fs_q_jt_completescansecondcode * S ((S (jt_h_completescan)) * C) + (jt_d_completescan))) /\ (((exists fs_h_jt_completescansecondscale. fs_h_jt_completescansecondscale + S (jt_f_completescan) = S ((S (jt_h_completescan)) * E)) /\ exists fs_q_jt_completescansecondscale. D = fs_q_jt_completescansecondscale * S ((S (jt_h_completescan)) * E) + (jt_f_completescan))))) -> (forall jt_index_completescansame jt_left_completescansame jt_right_completescansame. (exists jt_gap_completescansameindex. jt_gap_completescansameindex+S (jt_index_completescansame)=(k)) -> (((exists fs_h_jt_completescansameleft. fs_h_jt_completescansameleft + S (jt_left_completescansame) = S ((S (jt_index_completescansame)) * jt_e_completescan)) /\ exists fs_q_jt_completescansameleft. jt_b_completescan = fs_q_jt_completescansameleft * S ((S (jt_index_completescansame)) * jt_e_completescan) + (jt_left_completescansame))) -> (((exists fs_h_jt_completescansameright. fs_h_jt_completescansameright + S (jt_right_completescansame) = S ((S (jt_index_completescansame)) * jt_f_completescan)) /\ exists fs_q_jt_completescansameright. jt_d_completescan = fs_q_jt_completescansameright * S ((S (jt_index_completescansame)) * jt_f_completescan) + (jt_right_completescansame))) -> jt_left_completescansame=jt_right_completescansame) -> jt_i_completescan=jt_h_completescan) /\ (forall jt_z_completescan. (exists jt_gap_completescancodeindex. jt_gap_completescancodeindex+S (jt_z_completescan)=(T)) -> (forall jt_index_completescaninputbound. (exists jt_gap_completescaninputboundindex. jt_gap_completescaninputboundindex+S (jt_index_completescaninputbound)=(k)) -> exists jt_value_completescaninputbound. ((((exists fs_h_jt_completescaninputboundat. fs_h_jt_completescaninputboundat + S (jt_value_completescaninputbound) = S ((S (jt_index_completescaninputbound)) * c)) /\ exists fs_q_jt_completescaninputboundat. jt_z_completescan = fs_q_jt_completescaninputboundat * S ((S (jt_index_completescaninputbound)) * c) + (jt_value_completescaninputbound))) /\ (exists jt_gap_completescaninputboundvalue. jt_gap_completescaninputboundvalue+S (jt_value_completescaninputbound)=(n)))) -> (forall jt_divisor_completescaninputprimitive. (exists jt_factor_completescaninputprimitivemodulus. (n)=(jt_divisor_completescaninputprimitive)*jt_factor_completescaninputprimitivemodulus) -> (forall jt_index_completescaninputprimitivecoordinates jt_value_completescaninputprimitivecoordinates. (exists jt_gap_completescaninputprimitivecoordinatesindex. jt_gap_completescaninputprimitivecoordinatesindex+S (jt_index_completescaninputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_completescaninputprimitivecoordinatesat. fs_h_jt_completescaninputprimitivecoordinatesat + S (jt_value_completescaninputprimitivecoordinates) = S ((S (jt_index_completescaninputprimitivecoordinates)) * c)) /\ exists fs_q_jt_completescaninputprimitivecoordinatesat. jt_z_completescan = fs_q_jt_completescaninputprimitivecoordinatesat * S ((S (jt_index_completescaninputprimitivecoordinates)) * c) + (jt_value_completescaninputprimitivecoordinates))) -> (exists jt_factor_completescaninputprimitivecoordinatesdivides. (jt_value_completescaninputprimitivecoordinates)=(jt_divisor_completescaninputprimitive)*jt_factor_completescaninputprimitivecoordinatesdivides)) -> jt_divisor_completescaninputprimitive=1) -> (exists jt_index_completescanlisted jt_code_completescanlisted jt_scale_completescanlisted. ((exists jt_gap_completescanlistedindex. jt_gap_completescanlistedindex+S (jt_index_completescanlisted)=(j)) /\ (((((((exists fs_h_jt_completescanlistedcode. fs_h_jt_completescanlistedcode + S (jt_code_completescanlisted) = S ((S (jt_index_completescanlisted)) * C)) /\ exists fs_q_jt_completescanlistedcode. B = fs_q_jt_completescanlistedcode * S ((S (jt_index_completescanlisted)) * C) + (jt_code_completescanlisted))) /\ (((exists fs_h_jt_completescanlistedscale. fs_h_jt_completescanlistedscale + S (jt_scale_completescanlisted) = S ((S (jt_index_completescanlisted)) * E)) /\ exists fs_q_jt_completescanlistedscale. D = fs_q_jt_completescanlistedscale * S ((S (jt_index_completescanlisted)) * E) + (jt_scale_completescanlisted))))) /\ (forall jt_index_completescanlistedequal jt_left_completescanlistedequal jt_right_completescanlistedequal. (exists jt_gap_completescanlistedequalindex. jt_gap_completescanlistedequalindex+S (jt_index_completescanlistedequal)=(k)) -> (((exists fs_h_jt_completescanlistedequalleft. fs_h_jt_completescanlistedequalleft + S (jt_left_completescanlistedequal) = S ((S (jt_index_completescanlistedequal)) * c)) /\ exists fs_q_jt_completescanlistedequalleft. jt_z_completescan = fs_q_jt_completescanlistedequalleft * S ((S (jt_index_completescanlistedequal)) * c) + (jt_left_completescanlistedequal))) -> (((exists fs_h_jt_completescanlistedequalright. fs_h_jt_completescanlistedequalright + S (jt_right_completescanlistedequal) = S ((S (jt_index_completescanlistedequal)) * jt_scale_completescanlisted)) /\ exists fs_q_jt_completescanlistedequalright. jt_code_completescanlisted = fs_q_jt_completescanlistedequalright * S ((S (jt_index_completescanlistedequal)) * jt_scale_completescanlisted) + (jt_right_completescanlistedequal))) -> jt_left_completescanlistedequal=jt_right_completescanlistedequal)))))))))) -> (((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)) * C)) /\ exists fs_q_jt_completeenumsoundcode. B = fs_q_jt_completeenumsoundcode * S ((S (jt_i_completeenum)) * C) + (jt_b_completeenum))) /\ (((exists fs_h_jt_completeenumsoundscale. fs_h_jt_completeenumsoundscale + S (jt_c_completeenum) = S ((S (jt_i_completeenum)) * E)) /\ exists fs_q_jt_completeenumsoundscale. D = fs_q_jt_completeenumsoundscale * S ((S (jt_i_completeenum)) * E) + (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)) * C)) /\ exists fs_q_jt_completeenumcompletecode. B = fs_q_jt_completeenumcompletecode * S ((S (jt_i_completeenum)) * C) + (jt_d_completeenum))) /\ (((exists fs_h_jt_completeenumcompletescale. fs_h_jt_completeenumcompletescale + S (jt_e_completeenum) = S ((S (jt_i_completeenum)) * E)) /\ exists fs_q_jt_completeenumcompletescale. D = fs_q_jt_completeenumcompletescale * S ((S (jt_i_completeenum)) * E) + (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)) * C)) /\ exists fs_q_jt_completeenumfirstcode. B = fs_q_jt_completeenumfirstcode * S ((S (jt_i_completeenum)) * C) + (jt_b_completeenum))) /\ (((exists fs_h_jt_completeenumfirstscale. fs_h_jt_completeenumfirstscale + S (jt_c_completeenum) = S ((S (jt_i_completeenum)) * E)) /\ exists fs_q_jt_completeenumfirstscale. D = fs_q_jt_completeenumfirstscale * S ((S (jt_i_completeenum)) * E) + (jt_c_completeenum))))) -> (((((exists fs_h_jt_completeenumsecondcode. fs_h_jt_completeenumsecondcode + S (jt_d_completeenum) = S ((S (jt_h_completeenum)) * C)) /\ exists fs_q_jt_completeenumsecondcode. B = fs_q_jt_completeenumsecondcode * S ((S (jt_h_completeenum)) * C) + (jt_d_completeenum))) /\ (((exists fs_h_jt_completeenumsecondscale. fs_h_jt_completeenumsecondscale + S (jt_e_completeenum) = S ((S (jt_h_completeenum)) * E)) /\ exists fs_q_jt_completeenumsecondscale. D = fs_q_jt_completeenumsecondscale * S ((S (jt_h_completeenum)) * E) + (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)))))