jordan_tuple_scan_empty

Exact expanded first-order arithmetic statement

forall k n c B C D E. ((forall jt_i_scanempty. (exists jt_gap_scanemptysoundindex. jt_gap_scanemptysoundindex+S (jt_i_scanempty)=(0)) -> exists jt_b_scanempty jt_e_scanempty. ((((((exists fs_h_jt_scanemptysoundcode. fs_h_jt_scanemptysoundcode + S (jt_b_scanempty) = S ((S (jt_i_scanempty)) * C)) /\ exists fs_q_jt_scanemptysoundcode. B = fs_q_jt_scanemptysoundcode * S ((S (jt_i_scanempty)) * C) + (jt_b_scanempty))) /\ (((exists fs_h_jt_scanemptysoundscale. fs_h_jt_scanemptysoundscale + S (jt_e_scanempty) = S ((S (jt_i_scanempty)) * E)) /\ exists fs_q_jt_scanemptysoundscale. D = fs_q_jt_scanemptysoundscale * S ((S (jt_i_scanempty)) * E) + (jt_e_scanempty))))) /\ (((forall jt_index_scanemptybound. (exists jt_gap_scanemptyboundindex. jt_gap_scanemptyboundindex+S (jt_index_scanemptybound)=(k)) -> exists jt_value_scanemptybound. ((((exists fs_h_jt_scanemptyboundat. fs_h_jt_scanemptyboundat + S (jt_value_scanemptybound) = S ((S (jt_index_scanemptybound)) * jt_e_scanempty)) /\ exists fs_q_jt_scanemptyboundat. jt_b_scanempty = fs_q_jt_scanemptyboundat * S ((S (jt_index_scanemptybound)) * jt_e_scanempty) + (jt_value_scanemptybound))) /\ (exists jt_gap_scanemptyboundvalue. jt_gap_scanemptyboundvalue+S (jt_value_scanemptybound)=(n)))) /\ (forall jt_divisor_scanemptyprimitive. (exists jt_factor_scanemptyprimitivemodulus. (n)=(jt_divisor_scanemptyprimitive)*jt_factor_scanemptyprimitivemodulus) -> (forall jt_index_scanemptyprimitivecoordinates jt_value_scanemptyprimitivecoordinates. (exists jt_gap_scanemptyprimitivecoordinatesindex. jt_gap_scanemptyprimitivecoordinatesindex+S (jt_index_scanemptyprimitivecoordinates)=(k)) -> (((exists fs_h_jt_scanemptyprimitivecoordinatesat. fs_h_jt_scanemptyprimitivecoordinatesat + S (jt_value_scanemptyprimitivecoordinates) = S ((S (jt_index_scanemptyprimitivecoordinates)) * jt_e_scanempty)) /\ exists fs_q_jt_scanemptyprimitivecoordinatesat. jt_b_scanempty = fs_q_jt_scanemptyprimitivecoordinatesat * S ((S (jt_index_scanemptyprimitivecoordinates)) * jt_e_scanempty) + (jt_value_scanemptyprimitivecoordinates))) -> (exists jt_factor_scanemptyprimitivecoordinatesdivides. (jt_value_scanemptyprimitivecoordinates)=(jt_divisor_scanemptyprimitive)*jt_factor_scanemptyprimitivecoordinatesdivides)) -> jt_divisor_scanemptyprimitive=1))))) /\ (((forall jt_i_scanempty jt_h_scanempty jt_b_scanempty jt_e_scanempty jt_d_scanempty jt_f_scanempty. (exists jt_gap_scanemptyfirstindex. jt_gap_scanemptyfirstindex+S (jt_i_scanempty)=(0)) -> (exists jt_gap_scanemptysecondindex. jt_gap_scanemptysecondindex+S (jt_h_scanempty)=(0)) -> (((((exists fs_h_jt_scanemptyfirstcode. fs_h_jt_scanemptyfirstcode + S (jt_b_scanempty) = S ((S (jt_i_scanempty)) * C)) /\ exists fs_q_jt_scanemptyfirstcode. B = fs_q_jt_scanemptyfirstcode * S ((S (jt_i_scanempty)) * C) + (jt_b_scanempty))) /\ (((exists fs_h_jt_scanemptyfirstscale. fs_h_jt_scanemptyfirstscale + S (jt_e_scanempty) = S ((S (jt_i_scanempty)) * E)) /\ exists fs_q_jt_scanemptyfirstscale. D = fs_q_jt_scanemptyfirstscale * S ((S (jt_i_scanempty)) * E) + (jt_e_scanempty))))) -> (((((exists fs_h_jt_scanemptysecondcode. fs_h_jt_scanemptysecondcode + S (jt_d_scanempty) = S ((S (jt_h_scanempty)) * C)) /\ exists fs_q_jt_scanemptysecondcode. B = fs_q_jt_scanemptysecondcode * S ((S (jt_h_scanempty)) * C) + (jt_d_scanempty))) /\ (((exists fs_h_jt_scanemptysecondscale. fs_h_jt_scanemptysecondscale + S (jt_f_scanempty) = S ((S (jt_h_scanempty)) * E)) /\ exists fs_q_jt_scanemptysecondscale. D = fs_q_jt_scanemptysecondscale * S ((S (jt_h_scanempty)) * E) + (jt_f_scanempty))))) -> (forall jt_index_scanemptysame jt_left_scanemptysame jt_right_scanemptysame. (exists jt_gap_scanemptysameindex. jt_gap_scanemptysameindex+S (jt_index_scanemptysame)=(k)) -> (((exists fs_h_jt_scanemptysameleft. fs_h_jt_scanemptysameleft + S (jt_left_scanemptysame) = S ((S (jt_index_scanemptysame)) * jt_e_scanempty)) /\ exists fs_q_jt_scanemptysameleft. jt_b_scanempty = fs_q_jt_scanemptysameleft * S ((S (jt_index_scanemptysame)) * jt_e_scanempty) + (jt_left_scanemptysame))) -> (((exists fs_h_jt_scanemptysameright. fs_h_jt_scanemptysameright + S (jt_right_scanemptysame) = S ((S (jt_index_scanemptysame)) * jt_f_scanempty)) /\ exists fs_q_jt_scanemptysameright. jt_d_scanempty = fs_q_jt_scanemptysameright * S ((S (jt_index_scanemptysame)) * jt_f_scanempty) + (jt_right_scanemptysame))) -> jt_left_scanemptysame=jt_right_scanemptysame) -> jt_i_scanempty=jt_h_scanempty) /\ (forall jt_z_scanempty. (exists jt_gap_scanemptycodeindex. jt_gap_scanemptycodeindex+S (jt_z_scanempty)=(0)) -> (forall jt_index_scanemptyinputbound. (exists jt_gap_scanemptyinputboundindex. jt_gap_scanemptyinputboundindex+S (jt_index_scanemptyinputbound)=(k)) -> exists jt_value_scanemptyinputbound. ((((exists fs_h_jt_scanemptyinputboundat. fs_h_jt_scanemptyinputboundat + S (jt_value_scanemptyinputbound) = S ((S (jt_index_scanemptyinputbound)) * c)) /\ exists fs_q_jt_scanemptyinputboundat. jt_z_scanempty = fs_q_jt_scanemptyinputboundat * S ((S (jt_index_scanemptyinputbound)) * c) + (jt_value_scanemptyinputbound))) /\ (exists jt_gap_scanemptyinputboundvalue. jt_gap_scanemptyinputboundvalue+S (jt_value_scanemptyinputbound)=(n)))) -> (forall jt_divisor_scanemptyinputprimitive. (exists jt_factor_scanemptyinputprimitivemodulus. (n)=(jt_divisor_scanemptyinputprimitive)*jt_factor_scanemptyinputprimitivemodulus) -> (forall jt_index_scanemptyinputprimitivecoordinates jt_value_scanemptyinputprimitivecoordinates. (exists jt_gap_scanemptyinputprimitivecoordinatesindex. jt_gap_scanemptyinputprimitivecoordinatesindex+S (jt_index_scanemptyinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_scanemptyinputprimitivecoordinatesat. fs_h_jt_scanemptyinputprimitivecoordinatesat + S (jt_value_scanemptyinputprimitivecoordinates) = S ((S (jt_index_scanemptyinputprimitivecoordinates)) * c)) /\ exists fs_q_jt_scanemptyinputprimitivecoordinatesat. jt_z_scanempty = fs_q_jt_scanemptyinputprimitivecoordinatesat * S ((S (jt_index_scanemptyinputprimitivecoordinates)) * c) + (jt_value_scanemptyinputprimitivecoordinates))) -> (exists jt_factor_scanemptyinputprimitivecoordinatesdivides. (jt_value_scanemptyinputprimitivecoordinates)=(jt_divisor_scanemptyinputprimitive)*jt_factor_scanemptyinputprimitivecoordinatesdivides)) -> jt_divisor_scanemptyinputprimitive=1) -> (exists jt_index_scanemptylisted jt_code_scanemptylisted jt_scale_scanemptylisted. ((exists jt_gap_scanemptylistedindex. jt_gap_scanemptylistedindex+S (jt_index_scanemptylisted)=(0)) /\ (((((((exists fs_h_jt_scanemptylistedcode. fs_h_jt_scanemptylistedcode + S (jt_code_scanemptylisted) = S ((S (jt_index_scanemptylisted)) * C)) /\ exists fs_q_jt_scanemptylistedcode. B = fs_q_jt_scanemptylistedcode * S ((S (jt_index_scanemptylisted)) * C) + (jt_code_scanemptylisted))) /\ (((exists fs_h_jt_scanemptylistedscale. fs_h_jt_scanemptylistedscale + S (jt_scale_scanemptylisted) = S ((S (jt_index_scanemptylisted)) * E)) /\ exists fs_q_jt_scanemptylistedscale. D = fs_q_jt_scanemptylistedscale * S ((S (jt_index_scanemptylisted)) * E) + (jt_scale_scanemptylisted))))) /\ (forall jt_index_scanemptylistedequal jt_left_scanemptylistedequal jt_right_scanemptylistedequal. (exists jt_gap_scanemptylistedequalindex. jt_gap_scanemptylistedequalindex+S (jt_index_scanemptylistedequal)=(k)) -> (((exists fs_h_jt_scanemptylistedequalleft. fs_h_jt_scanemptylistedequalleft + S (jt_left_scanemptylistedequal) = S ((S (jt_index_scanemptylistedequal)) * c)) /\ exists fs_q_jt_scanemptylistedequalleft. jt_z_scanempty = fs_q_jt_scanemptylistedequalleft * S ((S (jt_index_scanemptylistedequal)) * c) + (jt_left_scanemptylistedequal))) -> (((exists fs_h_jt_scanemptylistedequalright. fs_h_jt_scanemptylistedequalright + S (jt_right_scanemptylistedequal) = S ((S (jt_index_scanemptylistedequal)) * jt_scale_scanemptylisted)) /\ exists fs_q_jt_scanemptylistedequalright. jt_code_scanemptylisted = fs_q_jt_scanemptylistedequalright * S ((S (jt_index_scanemptylistedequal)) * jt_scale_scanemptylisted) + (jt_right_scanemptylistedequal))) -> jt_left_scanemptylistedequal=jt_right_scanemptylistedequal)))))))))