jordan_enumeration_index_map_exists

Exact expanded first-order arithmetic statement

forall q k n A B C D u E F G H v. (((forall jt_i_exists_source. (exists jt_gap_exists_sourcesoundindex. jt_gap_exists_sourcesoundindex+S (jt_i_exists_source)=(u)) -> exists jt_b_exists_source jt_c_exists_source. ((((((exists fs_h_jt_exists_sourcesoundcode. fs_h_jt_exists_sourcesoundcode + S (jt_b_exists_source) = S ((S (jt_i_exists_source)) * B)) /\ exists fs_q_jt_exists_sourcesoundcode. A = fs_q_jt_exists_sourcesoundcode * S ((S (jt_i_exists_source)) * B) + (jt_b_exists_source))) /\ (((exists fs_h_jt_exists_sourcesoundscale. fs_h_jt_exists_sourcesoundscale + S (jt_c_exists_source) = S ((S (jt_i_exists_source)) * D)) /\ exists fs_q_jt_exists_sourcesoundscale. C = fs_q_jt_exists_sourcesoundscale * S ((S (jt_i_exists_source)) * D) + (jt_c_exists_source))))) /\ (((forall jt_index_exists_sourcebound. (exists jt_gap_exists_sourceboundindex. jt_gap_exists_sourceboundindex+S (jt_index_exists_sourcebound)=(k)) -> exists jt_value_exists_sourcebound. ((((exists fs_h_jt_exists_sourceboundat. fs_h_jt_exists_sourceboundat + S (jt_value_exists_sourcebound) = S ((S (jt_index_exists_sourcebound)) * jt_c_exists_source)) /\ exists fs_q_jt_exists_sourceboundat. jt_b_exists_source = fs_q_jt_exists_sourceboundat * S ((S (jt_index_exists_sourcebound)) * jt_c_exists_source) + (jt_value_exists_sourcebound))) /\ (exists jt_gap_exists_sourceboundvalue. jt_gap_exists_sourceboundvalue+S (jt_value_exists_sourcebound)=(n)))) /\ (forall jt_divisor_exists_sourceprimitive. (exists jt_factor_exists_sourceprimitivemodulus. (n)=(jt_divisor_exists_sourceprimitive)*jt_factor_exists_sourceprimitivemodulus) -> (forall jt_index_exists_sourceprimitivecoordinates jt_value_exists_sourceprimitivecoordinates. (exists jt_gap_exists_sourceprimitivecoordinatesindex. jt_gap_exists_sourceprimitivecoordinatesindex+S (jt_index_exists_sourceprimitivecoordinates)=(k)) -> (((exists fs_h_jt_exists_sourceprimitivecoordinatesat. fs_h_jt_exists_sourceprimitivecoordinatesat + S (jt_value_exists_sourceprimitivecoordinates) = S ((S (jt_index_exists_sourceprimitivecoordinates)) * jt_c_exists_source)) /\ exists fs_q_jt_exists_sourceprimitivecoordinatesat. jt_b_exists_source = fs_q_jt_exists_sourceprimitivecoordinatesat * S ((S (jt_index_exists_sourceprimitivecoordinates)) * jt_c_exists_source) + (jt_value_exists_sourceprimitivecoordinates))) -> (exists jt_factor_exists_sourceprimitivecoordinatesdivides. (jt_value_exists_sourceprimitivecoordinates)=(jt_divisor_exists_sourceprimitive)*jt_factor_exists_sourceprimitivecoordinatesdivides)) -> jt_divisor_exists_sourceprimitive=1))))) /\ (((forall jt_b_exists_source jt_c_exists_source. (forall jt_index_exists_sourceinputbound. (exists jt_gap_exists_sourceinputboundindex. jt_gap_exists_sourceinputboundindex+S (jt_index_exists_sourceinputbound)=(k)) -> exists jt_value_exists_sourceinputbound. ((((exists fs_h_jt_exists_sourceinputboundat. fs_h_jt_exists_sourceinputboundat + S (jt_value_exists_sourceinputbound) = S ((S (jt_index_exists_sourceinputbound)) * jt_c_exists_source)) /\ exists fs_q_jt_exists_sourceinputboundat. jt_b_exists_source = fs_q_jt_exists_sourceinputboundat * S ((S (jt_index_exists_sourceinputbound)) * jt_c_exists_source) + (jt_value_exists_sourceinputbound))) /\ (exists jt_gap_exists_sourceinputboundvalue. jt_gap_exists_sourceinputboundvalue+S (jt_value_exists_sourceinputbound)=(n)))) -> (forall jt_divisor_exists_sourceinputprimitive. (exists jt_factor_exists_sourceinputprimitivemodulus. (n)=(jt_divisor_exists_sourceinputprimitive)*jt_factor_exists_sourceinputprimitivemodulus) -> (forall jt_index_exists_sourceinputprimitivecoordinates jt_value_exists_sourceinputprimitivecoordinates. (exists jt_gap_exists_sourceinputprimitivecoordinatesindex. jt_gap_exists_sourceinputprimitivecoordinatesindex+S (jt_index_exists_sourceinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_exists_sourceinputprimitivecoordinatesat. fs_h_jt_exists_sourceinputprimitivecoordinatesat + S (jt_value_exists_sourceinputprimitivecoordinates) = S ((S (jt_index_exists_sourceinputprimitivecoordinates)) * jt_c_exists_source)) /\ exists fs_q_jt_exists_sourceinputprimitivecoordinatesat. jt_b_exists_source = fs_q_jt_exists_sourceinputprimitivecoordinatesat * S ((S (jt_index_exists_sourceinputprimitivecoordinates)) * jt_c_exists_source) + (jt_value_exists_sourceinputprimitivecoordinates))) -> (exists jt_factor_exists_sourceinputprimitivecoordinatesdivides. (jt_value_exists_sourceinputprimitivecoordinates)=(jt_divisor_exists_sourceinputprimitive)*jt_factor_exists_sourceinputprimitivecoordinatesdivides)) -> jt_divisor_exists_sourceinputprimitive=1) -> exists jt_i_exists_source jt_d_exists_source jt_e_exists_source. ((exists jt_gap_exists_sourcecompleteindex. jt_gap_exists_sourcecompleteindex+S (jt_i_exists_source)=(u)) /\ (((((((exists fs_h_jt_exists_sourcecompletecode. fs_h_jt_exists_sourcecompletecode + S (jt_d_exists_source) = S ((S (jt_i_exists_source)) * B)) /\ exists fs_q_jt_exists_sourcecompletecode. A = fs_q_jt_exists_sourcecompletecode * S ((S (jt_i_exists_source)) * B) + (jt_d_exists_source))) /\ (((exists fs_h_jt_exists_sourcecompletescale. fs_h_jt_exists_sourcecompletescale + S (jt_e_exists_source) = S ((S (jt_i_exists_source)) * D)) /\ exists fs_q_jt_exists_sourcecompletescale. C = fs_q_jt_exists_sourcecompletescale * S ((S (jt_i_exists_source)) * D) + (jt_e_exists_source))))) /\ (forall jt_index_exists_sourcerepresented jt_left_exists_sourcerepresented jt_right_exists_sourcerepresented. (exists jt_gap_exists_sourcerepresentedindex. jt_gap_exists_sourcerepresentedindex+S (jt_index_exists_sourcerepresented)=(k)) -> (((exists fs_h_jt_exists_sourcerepresentedleft. fs_h_jt_exists_sourcerepresentedleft + S (jt_left_exists_sourcerepresented) = S ((S (jt_index_exists_sourcerepresented)) * jt_c_exists_source)) /\ exists fs_q_jt_exists_sourcerepresentedleft. jt_b_exists_source = fs_q_jt_exists_sourcerepresentedleft * S ((S (jt_index_exists_sourcerepresented)) * jt_c_exists_source) + (jt_left_exists_sourcerepresented))) -> (((exists fs_h_jt_exists_sourcerepresentedright. fs_h_jt_exists_sourcerepresentedright + S (jt_right_exists_sourcerepresented) = S ((S (jt_index_exists_sourcerepresented)) * jt_e_exists_source)) /\ exists fs_q_jt_exists_sourcerepresentedright. jt_d_exists_source = fs_q_jt_exists_sourcerepresentedright * S ((S (jt_index_exists_sourcerepresented)) * jt_e_exists_source) + (jt_right_exists_sourcerepresented))) -> jt_left_exists_sourcerepresented=jt_right_exists_sourcerepresented))))) /\ (forall jt_i_exists_source jt_h_exists_source jt_b_exists_source jt_c_exists_source jt_d_exists_source jt_e_exists_source. (exists jt_gap_exists_sourcefirstindex. jt_gap_exists_sourcefirstindex+S (jt_i_exists_source)=(u)) -> (exists jt_gap_exists_sourcesecondindex. jt_gap_exists_sourcesecondindex+S (jt_h_exists_source)=(u)) -> (((((exists fs_h_jt_exists_sourcefirstcode. fs_h_jt_exists_sourcefirstcode + S (jt_b_exists_source) = S ((S (jt_i_exists_source)) * B)) /\ exists fs_q_jt_exists_sourcefirstcode. A = fs_q_jt_exists_sourcefirstcode * S ((S (jt_i_exists_source)) * B) + (jt_b_exists_source))) /\ (((exists fs_h_jt_exists_sourcefirstscale. fs_h_jt_exists_sourcefirstscale + S (jt_c_exists_source) = S ((S (jt_i_exists_source)) * D)) /\ exists fs_q_jt_exists_sourcefirstscale. C = fs_q_jt_exists_sourcefirstscale * S ((S (jt_i_exists_source)) * D) + (jt_c_exists_source))))) -> (((((exists fs_h_jt_exists_sourcesecondcode. fs_h_jt_exists_sourcesecondcode + S (jt_d_exists_source) = S ((S (jt_h_exists_source)) * B)) /\ exists fs_q_jt_exists_sourcesecondcode. A = fs_q_jt_exists_sourcesecondcode * S ((S (jt_h_exists_source)) * B) + (jt_d_exists_source))) /\ (((exists fs_h_jt_exists_sourcesecondscale. fs_h_jt_exists_sourcesecondscale + S (jt_e_exists_source) = S ((S (jt_h_exists_source)) * D)) /\ exists fs_q_jt_exists_sourcesecondscale. C = fs_q_jt_exists_sourcesecondscale * S ((S (jt_h_exists_source)) * D) + (jt_e_exists_source))))) -> (forall jt_index_exists_sourcesame jt_left_exists_sourcesame jt_right_exists_sourcesame. (exists jt_gap_exists_sourcesameindex. jt_gap_exists_sourcesameindex+S (jt_index_exists_sourcesame)=(k)) -> (((exists fs_h_jt_exists_sourcesameleft. fs_h_jt_exists_sourcesameleft + S (jt_left_exists_sourcesame) = S ((S (jt_index_exists_sourcesame)) * jt_c_exists_source)) /\ exists fs_q_jt_exists_sourcesameleft. jt_b_exists_source = fs_q_jt_exists_sourcesameleft * S ((S (jt_index_exists_sourcesame)) * jt_c_exists_source) + (jt_left_exists_sourcesame))) -> (((exists fs_h_jt_exists_sourcesameright. fs_h_jt_exists_sourcesameright + S (jt_right_exists_sourcesame) = S ((S (jt_index_exists_sourcesame)) * jt_e_exists_source)) /\ exists fs_q_jt_exists_sourcesameright. jt_d_exists_source = fs_q_jt_exists_sourcesameright * S ((S (jt_index_exists_sourcesame)) * jt_e_exists_source) + (jt_right_exists_sourcesame))) -> jt_left_exists_sourcesame=jt_right_exists_sourcesame) -> jt_i_exists_source=jt_h_exists_source))))) -> (((forall jt_i_exists_target. (exists jt_gap_exists_targetsoundindex. jt_gap_exists_targetsoundindex+S (jt_i_exists_target)=(v)) -> exists jt_b_exists_target jt_c_exists_target. ((((((exists fs_h_jt_exists_targetsoundcode. fs_h_jt_exists_targetsoundcode + S (jt_b_exists_target) = S ((S (jt_i_exists_target)) * F)) /\ exists fs_q_jt_exists_targetsoundcode. E = fs_q_jt_exists_targetsoundcode * S ((S (jt_i_exists_target)) * F) + (jt_b_exists_target))) /\ (((exists fs_h_jt_exists_targetsoundscale. fs_h_jt_exists_targetsoundscale + S (jt_c_exists_target) = S ((S (jt_i_exists_target)) * H)) /\ exists fs_q_jt_exists_targetsoundscale. G = fs_q_jt_exists_targetsoundscale * S ((S (jt_i_exists_target)) * H) + (jt_c_exists_target))))) /\ (((forall jt_index_exists_targetbound. (exists jt_gap_exists_targetboundindex. jt_gap_exists_targetboundindex+S (jt_index_exists_targetbound)=(k)) -> exists jt_value_exists_targetbound. ((((exists fs_h_jt_exists_targetboundat. fs_h_jt_exists_targetboundat + S (jt_value_exists_targetbound) = S ((S (jt_index_exists_targetbound)) * jt_c_exists_target)) /\ exists fs_q_jt_exists_targetboundat. jt_b_exists_target = fs_q_jt_exists_targetboundat * S ((S (jt_index_exists_targetbound)) * jt_c_exists_target) + (jt_value_exists_targetbound))) /\ (exists jt_gap_exists_targetboundvalue. jt_gap_exists_targetboundvalue+S (jt_value_exists_targetbound)=(n)))) /\ (forall jt_divisor_exists_targetprimitive. (exists jt_factor_exists_targetprimitivemodulus. (n)=(jt_divisor_exists_targetprimitive)*jt_factor_exists_targetprimitivemodulus) -> (forall jt_index_exists_targetprimitivecoordinates jt_value_exists_targetprimitivecoordinates. (exists jt_gap_exists_targetprimitivecoordinatesindex. jt_gap_exists_targetprimitivecoordinatesindex+S (jt_index_exists_targetprimitivecoordinates)=(k)) -> (((exists fs_h_jt_exists_targetprimitivecoordinatesat. fs_h_jt_exists_targetprimitivecoordinatesat + S (jt_value_exists_targetprimitivecoordinates) = S ((S (jt_index_exists_targetprimitivecoordinates)) * jt_c_exists_target)) /\ exists fs_q_jt_exists_targetprimitivecoordinatesat. jt_b_exists_target = fs_q_jt_exists_targetprimitivecoordinatesat * S ((S (jt_index_exists_targetprimitivecoordinates)) * jt_c_exists_target) + (jt_value_exists_targetprimitivecoordinates))) -> (exists jt_factor_exists_targetprimitivecoordinatesdivides. (jt_value_exists_targetprimitivecoordinates)=(jt_divisor_exists_targetprimitive)*jt_factor_exists_targetprimitivecoordinatesdivides)) -> jt_divisor_exists_targetprimitive=1))))) /\ (((forall jt_b_exists_target jt_c_exists_target. (forall jt_index_exists_targetinputbound. (exists jt_gap_exists_targetinputboundindex. jt_gap_exists_targetinputboundindex+S (jt_index_exists_targetinputbound)=(k)) -> exists jt_value_exists_targetinputbound. ((((exists fs_h_jt_exists_targetinputboundat. fs_h_jt_exists_targetinputboundat + S (jt_value_exists_targetinputbound) = S ((S (jt_index_exists_targetinputbound)) * jt_c_exists_target)) /\ exists fs_q_jt_exists_targetinputboundat. jt_b_exists_target = fs_q_jt_exists_targetinputboundat * S ((S (jt_index_exists_targetinputbound)) * jt_c_exists_target) + (jt_value_exists_targetinputbound))) /\ (exists jt_gap_exists_targetinputboundvalue. jt_gap_exists_targetinputboundvalue+S (jt_value_exists_targetinputbound)=(n)))) -> (forall jt_divisor_exists_targetinputprimitive. (exists jt_factor_exists_targetinputprimitivemodulus. (n)=(jt_divisor_exists_targetinputprimitive)*jt_factor_exists_targetinputprimitivemodulus) -> (forall jt_index_exists_targetinputprimitivecoordinates jt_value_exists_targetinputprimitivecoordinates. (exists jt_gap_exists_targetinputprimitivecoordinatesindex. jt_gap_exists_targetinputprimitivecoordinatesindex+S (jt_index_exists_targetinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_exists_targetinputprimitivecoordinatesat. fs_h_jt_exists_targetinputprimitivecoordinatesat + S (jt_value_exists_targetinputprimitivecoordinates) = S ((S (jt_index_exists_targetinputprimitivecoordinates)) * jt_c_exists_target)) /\ exists fs_q_jt_exists_targetinputprimitivecoordinatesat. jt_b_exists_target = fs_q_jt_exists_targetinputprimitivecoordinatesat * S ((S (jt_index_exists_targetinputprimitivecoordinates)) * jt_c_exists_target) + (jt_value_exists_targetinputprimitivecoordinates))) -> (exists jt_factor_exists_targetinputprimitivecoordinatesdivides. (jt_value_exists_targetinputprimitivecoordinates)=(jt_divisor_exists_targetinputprimitive)*jt_factor_exists_targetinputprimitivecoordinatesdivides)) -> jt_divisor_exists_targetinputprimitive=1) -> exists jt_i_exists_target jt_d_exists_target jt_e_exists_target. ((exists jt_gap_exists_targetcompleteindex. jt_gap_exists_targetcompleteindex+S (jt_i_exists_target)=(v)) /\ (((((((exists fs_h_jt_exists_targetcompletecode. fs_h_jt_exists_targetcompletecode + S (jt_d_exists_target) = S ((S (jt_i_exists_target)) * F)) /\ exists fs_q_jt_exists_targetcompletecode. E = fs_q_jt_exists_targetcompletecode * S ((S (jt_i_exists_target)) * F) + (jt_d_exists_target))) /\ (((exists fs_h_jt_exists_targetcompletescale. fs_h_jt_exists_targetcompletescale + S (jt_e_exists_target) = S ((S (jt_i_exists_target)) * H)) /\ exists fs_q_jt_exists_targetcompletescale. G = fs_q_jt_exists_targetcompletescale * S ((S (jt_i_exists_target)) * H) + (jt_e_exists_target))))) /\ (forall jt_index_exists_targetrepresented jt_left_exists_targetrepresented jt_right_exists_targetrepresented. (exists jt_gap_exists_targetrepresentedindex. jt_gap_exists_targetrepresentedindex+S (jt_index_exists_targetrepresented)=(k)) -> (((exists fs_h_jt_exists_targetrepresentedleft. fs_h_jt_exists_targetrepresentedleft + S (jt_left_exists_targetrepresented) = S ((S (jt_index_exists_targetrepresented)) * jt_c_exists_target)) /\ exists fs_q_jt_exists_targetrepresentedleft. jt_b_exists_target = fs_q_jt_exists_targetrepresentedleft * S ((S (jt_index_exists_targetrepresented)) * jt_c_exists_target) + (jt_left_exists_targetrepresented))) -> (((exists fs_h_jt_exists_targetrepresentedright. fs_h_jt_exists_targetrepresentedright + S (jt_right_exists_targetrepresented) = S ((S (jt_index_exists_targetrepresented)) * jt_e_exists_target)) /\ exists fs_q_jt_exists_targetrepresentedright. jt_d_exists_target = fs_q_jt_exists_targetrepresentedright * S ((S (jt_index_exists_targetrepresented)) * jt_e_exists_target) + (jt_right_exists_targetrepresented))) -> jt_left_exists_targetrepresented=jt_right_exists_targetrepresented))))) /\ (forall jt_i_exists_target jt_h_exists_target jt_b_exists_target jt_c_exists_target jt_d_exists_target jt_e_exists_target. (exists jt_gap_exists_targetfirstindex. jt_gap_exists_targetfirstindex+S (jt_i_exists_target)=(v)) -> (exists jt_gap_exists_targetsecondindex. jt_gap_exists_targetsecondindex+S (jt_h_exists_target)=(v)) -> (((((exists fs_h_jt_exists_targetfirstcode. fs_h_jt_exists_targetfirstcode + S (jt_b_exists_target) = S ((S (jt_i_exists_target)) * F)) /\ exists fs_q_jt_exists_targetfirstcode. E = fs_q_jt_exists_targetfirstcode * S ((S (jt_i_exists_target)) * F) + (jt_b_exists_target))) /\ (((exists fs_h_jt_exists_targetfirstscale. fs_h_jt_exists_targetfirstscale + S (jt_c_exists_target) = S ((S (jt_i_exists_target)) * H)) /\ exists fs_q_jt_exists_targetfirstscale. G = fs_q_jt_exists_targetfirstscale * S ((S (jt_i_exists_target)) * H) + (jt_c_exists_target))))) -> (((((exists fs_h_jt_exists_targetsecondcode. fs_h_jt_exists_targetsecondcode + S (jt_d_exists_target) = S ((S (jt_h_exists_target)) * F)) /\ exists fs_q_jt_exists_targetsecondcode. E = fs_q_jt_exists_targetsecondcode * S ((S (jt_h_exists_target)) * F) + (jt_d_exists_target))) /\ (((exists fs_h_jt_exists_targetsecondscale. fs_h_jt_exists_targetsecondscale + S (jt_e_exists_target) = S ((S (jt_h_exists_target)) * H)) /\ exists fs_q_jt_exists_targetsecondscale. G = fs_q_jt_exists_targetsecondscale * S ((S (jt_h_exists_target)) * H) + (jt_e_exists_target))))) -> (forall jt_index_exists_targetsame jt_left_exists_targetsame jt_right_exists_targetsame. (exists jt_gap_exists_targetsameindex. jt_gap_exists_targetsameindex+S (jt_index_exists_targetsame)=(k)) -> (((exists fs_h_jt_exists_targetsameleft. fs_h_jt_exists_targetsameleft + S (jt_left_exists_targetsame) = S ((S (jt_index_exists_targetsame)) * jt_c_exists_target)) /\ exists fs_q_jt_exists_targetsameleft. jt_b_exists_target = fs_q_jt_exists_targetsameleft * S ((S (jt_index_exists_targetsame)) * jt_c_exists_target) + (jt_left_exists_targetsame))) -> (((exists fs_h_jt_exists_targetsameright. fs_h_jt_exists_targetsameright + S (jt_right_exists_targetsame) = S ((S (jt_index_exists_targetsame)) * jt_e_exists_target)) /\ exists fs_q_jt_exists_targetsameright. jt_d_exists_target = fs_q_jt_exists_targetsameright * S ((S (jt_index_exists_targetsame)) * jt_e_exists_target) + (jt_right_exists_targetsame))) -> jt_left_exists_targetsame=jt_right_exists_targetsame) -> jt_i_exists_target=jt_h_exists_target))))) -> (exists jt_gap_exists_bound. jt_gap_exists_bound+(q)=(u)) -> (exists Z W. forall jt_index_exists_map. (exists jt_gap_exists_mapindex. jt_gap_exists_mapindex+S (jt_index_exists_map)=(q)) -> exists jt_image_exists_map. ((((exists fs_h_jt_exists_mapat. fs_h_jt_exists_mapat + S (jt_image_exists_map) = S ((S (jt_index_exists_map)) * W)) /\ exists fs_q_jt_exists_mapat. Z = fs_q_jt_exists_mapat * S ((S (jt_index_exists_map)) * W) + (jt_image_exists_map))) /\ (((exists jt_gap_exists_mapbound. jt_gap_exists_mapbound+S (jt_image_exists_map)=(v)) /\ (forall jt_b_exists_mapmatch jt_c_exists_mapmatch jt_d_exists_mapmatch jt_e_exists_mapmatch. (((((exists fs_h_jt_exists_mapmatchleftcode. fs_h_jt_exists_mapmatchleftcode + S (jt_b_exists_mapmatch) = S ((S (jt_index_exists_map)) * B)) /\ exists fs_q_jt_exists_mapmatchleftcode. A = fs_q_jt_exists_mapmatchleftcode * S ((S (jt_index_exists_map)) * B) + (jt_b_exists_mapmatch))) /\ (((exists fs_h_jt_exists_mapmatchleftscale. fs_h_jt_exists_mapmatchleftscale + S (jt_c_exists_mapmatch) = S ((S (jt_index_exists_map)) * D)) /\ exists fs_q_jt_exists_mapmatchleftscale. C = fs_q_jt_exists_mapmatchleftscale * S ((S (jt_index_exists_map)) * D) + (jt_c_exists_mapmatch))))) -> (((((exists fs_h_jt_exists_mapmatchrightcode. fs_h_jt_exists_mapmatchrightcode + S (jt_d_exists_mapmatch) = S ((S (jt_image_exists_map)) * F)) /\ exists fs_q_jt_exists_mapmatchrightcode. E = fs_q_jt_exists_mapmatchrightcode * S ((S (jt_image_exists_map)) * F) + (jt_d_exists_mapmatch))) /\ (((exists fs_h_jt_exists_mapmatchrightscale. fs_h_jt_exists_mapmatchrightscale + S (jt_e_exists_mapmatch) = S ((S (jt_image_exists_map)) * H)) /\ exists fs_q_jt_exists_mapmatchrightscale. G = fs_q_jt_exists_mapmatchrightscale * S ((S (jt_image_exists_map)) * H) + (jt_e_exists_mapmatch))))) -> (forall jt_index_exists_mapmatchequal jt_left_exists_mapmatchequal jt_right_exists_mapmatchequal. (exists jt_gap_exists_mapmatchequalindex. jt_gap_exists_mapmatchequalindex+S (jt_index_exists_mapmatchequal)=(k)) -> (((exists fs_h_jt_exists_mapmatchequalleft. fs_h_jt_exists_mapmatchequalleft + S (jt_left_exists_mapmatchequal) = S ((S (jt_index_exists_mapmatchequal)) * jt_c_exists_mapmatch)) /\ exists fs_q_jt_exists_mapmatchequalleft. jt_b_exists_mapmatch = fs_q_jt_exists_mapmatchequalleft * S ((S (jt_index_exists_mapmatchequal)) * jt_c_exists_mapmatch) + (jt_left_exists_mapmatchequal))) -> (((exists fs_h_jt_exists_mapmatchequalright. fs_h_jt_exists_mapmatchequalright + S (jt_right_exists_mapmatchequal) = S ((S (jt_index_exists_mapmatchequal)) * jt_e_exists_mapmatch)) /\ exists fs_q_jt_exists_mapmatchequalright. jt_d_exists_mapmatch = fs_q_jt_exists_mapmatchequalright * S ((S (jt_index_exists_mapmatchequal)) * jt_e_exists_mapmatch) + (jt_right_exists_mapmatchequal))) -> jt_left_exists_mapmatchequal=jt_right_exists_mapmatchequal))))))