jordan_enumeration_index_map_bounded_injective

Exact expanded first-order arithmetic statement

forall k n A B C D u E F G H v Z W. (((forall jt_i_injective_source. (exists jt_gap_injective_sourcesoundindex. jt_gap_injective_sourcesoundindex+S (jt_i_injective_source)=(u)) -> exists jt_b_injective_source jt_c_injective_source. ((((((exists fs_h_jt_injective_sourcesoundcode. fs_h_jt_injective_sourcesoundcode + S (jt_b_injective_source) = S ((S (jt_i_injective_source)) * B)) /\ exists fs_q_jt_injective_sourcesoundcode. A = fs_q_jt_injective_sourcesoundcode * S ((S (jt_i_injective_source)) * B) + (jt_b_injective_source))) /\ (((exists fs_h_jt_injective_sourcesoundscale. fs_h_jt_injective_sourcesoundscale + S (jt_c_injective_source) = S ((S (jt_i_injective_source)) * D)) /\ exists fs_q_jt_injective_sourcesoundscale. C = fs_q_jt_injective_sourcesoundscale * S ((S (jt_i_injective_source)) * D) + (jt_c_injective_source))))) /\ (((forall jt_index_injective_sourcebound. (exists jt_gap_injective_sourceboundindex. jt_gap_injective_sourceboundindex+S (jt_index_injective_sourcebound)=(k)) -> exists jt_value_injective_sourcebound. ((((exists fs_h_jt_injective_sourceboundat. fs_h_jt_injective_sourceboundat + S (jt_value_injective_sourcebound) = S ((S (jt_index_injective_sourcebound)) * jt_c_injective_source)) /\ exists fs_q_jt_injective_sourceboundat. jt_b_injective_source = fs_q_jt_injective_sourceboundat * S ((S (jt_index_injective_sourcebound)) * jt_c_injective_source) + (jt_value_injective_sourcebound))) /\ (exists jt_gap_injective_sourceboundvalue. jt_gap_injective_sourceboundvalue+S (jt_value_injective_sourcebound)=(n)))) /\ (forall jt_divisor_injective_sourceprimitive. (exists jt_factor_injective_sourceprimitivemodulus. (n)=(jt_divisor_injective_sourceprimitive)*jt_factor_injective_sourceprimitivemodulus) -> (forall jt_index_injective_sourceprimitivecoordinates jt_value_injective_sourceprimitivecoordinates. (exists jt_gap_injective_sourceprimitivecoordinatesindex. jt_gap_injective_sourceprimitivecoordinatesindex+S (jt_index_injective_sourceprimitivecoordinates)=(k)) -> (((exists fs_h_jt_injective_sourceprimitivecoordinatesat. fs_h_jt_injective_sourceprimitivecoordinatesat + S (jt_value_injective_sourceprimitivecoordinates) = S ((S (jt_index_injective_sourceprimitivecoordinates)) * jt_c_injective_source)) /\ exists fs_q_jt_injective_sourceprimitivecoordinatesat. jt_b_injective_source = fs_q_jt_injective_sourceprimitivecoordinatesat * S ((S (jt_index_injective_sourceprimitivecoordinates)) * jt_c_injective_source) + (jt_value_injective_sourceprimitivecoordinates))) -> (exists jt_factor_injective_sourceprimitivecoordinatesdivides. (jt_value_injective_sourceprimitivecoordinates)=(jt_divisor_injective_sourceprimitive)*jt_factor_injective_sourceprimitivecoordinatesdivides)) -> jt_divisor_injective_sourceprimitive=1))))) /\ (((forall jt_b_injective_source jt_c_injective_source. (forall jt_index_injective_sourceinputbound. (exists jt_gap_injective_sourceinputboundindex. jt_gap_injective_sourceinputboundindex+S (jt_index_injective_sourceinputbound)=(k)) -> exists jt_value_injective_sourceinputbound. ((((exists fs_h_jt_injective_sourceinputboundat. fs_h_jt_injective_sourceinputboundat + S (jt_value_injective_sourceinputbound) = S ((S (jt_index_injective_sourceinputbound)) * jt_c_injective_source)) /\ exists fs_q_jt_injective_sourceinputboundat. jt_b_injective_source = fs_q_jt_injective_sourceinputboundat * S ((S (jt_index_injective_sourceinputbound)) * jt_c_injective_source) + (jt_value_injective_sourceinputbound))) /\ (exists jt_gap_injective_sourceinputboundvalue. jt_gap_injective_sourceinputboundvalue+S (jt_value_injective_sourceinputbound)=(n)))) -> (forall jt_divisor_injective_sourceinputprimitive. (exists jt_factor_injective_sourceinputprimitivemodulus. (n)=(jt_divisor_injective_sourceinputprimitive)*jt_factor_injective_sourceinputprimitivemodulus) -> (forall jt_index_injective_sourceinputprimitivecoordinates jt_value_injective_sourceinputprimitivecoordinates. (exists jt_gap_injective_sourceinputprimitivecoordinatesindex. jt_gap_injective_sourceinputprimitivecoordinatesindex+S (jt_index_injective_sourceinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_injective_sourceinputprimitivecoordinatesat. fs_h_jt_injective_sourceinputprimitivecoordinatesat + S (jt_value_injective_sourceinputprimitivecoordinates) = S ((S (jt_index_injective_sourceinputprimitivecoordinates)) * jt_c_injective_source)) /\ exists fs_q_jt_injective_sourceinputprimitivecoordinatesat. jt_b_injective_source = fs_q_jt_injective_sourceinputprimitivecoordinatesat * S ((S (jt_index_injective_sourceinputprimitivecoordinates)) * jt_c_injective_source) + (jt_value_injective_sourceinputprimitivecoordinates))) -> (exists jt_factor_injective_sourceinputprimitivecoordinatesdivides. (jt_value_injective_sourceinputprimitivecoordinates)=(jt_divisor_injective_sourceinputprimitive)*jt_factor_injective_sourceinputprimitivecoordinatesdivides)) -> jt_divisor_injective_sourceinputprimitive=1) -> exists jt_i_injective_source jt_d_injective_source jt_e_injective_source. ((exists jt_gap_injective_sourcecompleteindex. jt_gap_injective_sourcecompleteindex+S (jt_i_injective_source)=(u)) /\ (((((((exists fs_h_jt_injective_sourcecompletecode. fs_h_jt_injective_sourcecompletecode + S (jt_d_injective_source) = S ((S (jt_i_injective_source)) * B)) /\ exists fs_q_jt_injective_sourcecompletecode. A = fs_q_jt_injective_sourcecompletecode * S ((S (jt_i_injective_source)) * B) + (jt_d_injective_source))) /\ (((exists fs_h_jt_injective_sourcecompletescale. fs_h_jt_injective_sourcecompletescale + S (jt_e_injective_source) = S ((S (jt_i_injective_source)) * D)) /\ exists fs_q_jt_injective_sourcecompletescale. C = fs_q_jt_injective_sourcecompletescale * S ((S (jt_i_injective_source)) * D) + (jt_e_injective_source))))) /\ (forall jt_index_injective_sourcerepresented jt_left_injective_sourcerepresented jt_right_injective_sourcerepresented. (exists jt_gap_injective_sourcerepresentedindex. jt_gap_injective_sourcerepresentedindex+S (jt_index_injective_sourcerepresented)=(k)) -> (((exists fs_h_jt_injective_sourcerepresentedleft. fs_h_jt_injective_sourcerepresentedleft + S (jt_left_injective_sourcerepresented) = S ((S (jt_index_injective_sourcerepresented)) * jt_c_injective_source)) /\ exists fs_q_jt_injective_sourcerepresentedleft. jt_b_injective_source = fs_q_jt_injective_sourcerepresentedleft * S ((S (jt_index_injective_sourcerepresented)) * jt_c_injective_source) + (jt_left_injective_sourcerepresented))) -> (((exists fs_h_jt_injective_sourcerepresentedright. fs_h_jt_injective_sourcerepresentedright + S (jt_right_injective_sourcerepresented) = S ((S (jt_index_injective_sourcerepresented)) * jt_e_injective_source)) /\ exists fs_q_jt_injective_sourcerepresentedright. jt_d_injective_source = fs_q_jt_injective_sourcerepresentedright * S ((S (jt_index_injective_sourcerepresented)) * jt_e_injective_source) + (jt_right_injective_sourcerepresented))) -> jt_left_injective_sourcerepresented=jt_right_injective_sourcerepresented))))) /\ (forall jt_i_injective_source jt_h_injective_source jt_b_injective_source jt_c_injective_source jt_d_injective_source jt_e_injective_source. (exists jt_gap_injective_sourcefirstindex. jt_gap_injective_sourcefirstindex+S (jt_i_injective_source)=(u)) -> (exists jt_gap_injective_sourcesecondindex. jt_gap_injective_sourcesecondindex+S (jt_h_injective_source)=(u)) -> (((((exists fs_h_jt_injective_sourcefirstcode. fs_h_jt_injective_sourcefirstcode + S (jt_b_injective_source) = S ((S (jt_i_injective_source)) * B)) /\ exists fs_q_jt_injective_sourcefirstcode. A = fs_q_jt_injective_sourcefirstcode * S ((S (jt_i_injective_source)) * B) + (jt_b_injective_source))) /\ (((exists fs_h_jt_injective_sourcefirstscale. fs_h_jt_injective_sourcefirstscale + S (jt_c_injective_source) = S ((S (jt_i_injective_source)) * D)) /\ exists fs_q_jt_injective_sourcefirstscale. C = fs_q_jt_injective_sourcefirstscale * S ((S (jt_i_injective_source)) * D) + (jt_c_injective_source))))) -> (((((exists fs_h_jt_injective_sourcesecondcode. fs_h_jt_injective_sourcesecondcode + S (jt_d_injective_source) = S ((S (jt_h_injective_source)) * B)) /\ exists fs_q_jt_injective_sourcesecondcode. A = fs_q_jt_injective_sourcesecondcode * S ((S (jt_h_injective_source)) * B) + (jt_d_injective_source))) /\ (((exists fs_h_jt_injective_sourcesecondscale. fs_h_jt_injective_sourcesecondscale + S (jt_e_injective_source) = S ((S (jt_h_injective_source)) * D)) /\ exists fs_q_jt_injective_sourcesecondscale. C = fs_q_jt_injective_sourcesecondscale * S ((S (jt_h_injective_source)) * D) + (jt_e_injective_source))))) -> (forall jt_index_injective_sourcesame jt_left_injective_sourcesame jt_right_injective_sourcesame. (exists jt_gap_injective_sourcesameindex. jt_gap_injective_sourcesameindex+S (jt_index_injective_sourcesame)=(k)) -> (((exists fs_h_jt_injective_sourcesameleft. fs_h_jt_injective_sourcesameleft + S (jt_left_injective_sourcesame) = S ((S (jt_index_injective_sourcesame)) * jt_c_injective_source)) /\ exists fs_q_jt_injective_sourcesameleft. jt_b_injective_source = fs_q_jt_injective_sourcesameleft * S ((S (jt_index_injective_sourcesame)) * jt_c_injective_source) + (jt_left_injective_sourcesame))) -> (((exists fs_h_jt_injective_sourcesameright. fs_h_jt_injective_sourcesameright + S (jt_right_injective_sourcesame) = S ((S (jt_index_injective_sourcesame)) * jt_e_injective_source)) /\ exists fs_q_jt_injective_sourcesameright. jt_d_injective_source = fs_q_jt_injective_sourcesameright * S ((S (jt_index_injective_sourcesame)) * jt_e_injective_source) + (jt_right_injective_sourcesame))) -> jt_left_injective_sourcesame=jt_right_injective_sourcesame) -> jt_i_injective_source=jt_h_injective_source))))) -> (((forall jt_i_injective_target. (exists jt_gap_injective_targetsoundindex. jt_gap_injective_targetsoundindex+S (jt_i_injective_target)=(v)) -> exists jt_b_injective_target jt_c_injective_target. ((((((exists fs_h_jt_injective_targetsoundcode. fs_h_jt_injective_targetsoundcode + S (jt_b_injective_target) = S ((S (jt_i_injective_target)) * F)) /\ exists fs_q_jt_injective_targetsoundcode. E = fs_q_jt_injective_targetsoundcode * S ((S (jt_i_injective_target)) * F) + (jt_b_injective_target))) /\ (((exists fs_h_jt_injective_targetsoundscale. fs_h_jt_injective_targetsoundscale + S (jt_c_injective_target) = S ((S (jt_i_injective_target)) * H)) /\ exists fs_q_jt_injective_targetsoundscale. G = fs_q_jt_injective_targetsoundscale * S ((S (jt_i_injective_target)) * H) + (jt_c_injective_target))))) /\ (((forall jt_index_injective_targetbound. (exists jt_gap_injective_targetboundindex. jt_gap_injective_targetboundindex+S (jt_index_injective_targetbound)=(k)) -> exists jt_value_injective_targetbound. ((((exists fs_h_jt_injective_targetboundat. fs_h_jt_injective_targetboundat + S (jt_value_injective_targetbound) = S ((S (jt_index_injective_targetbound)) * jt_c_injective_target)) /\ exists fs_q_jt_injective_targetboundat. jt_b_injective_target = fs_q_jt_injective_targetboundat * S ((S (jt_index_injective_targetbound)) * jt_c_injective_target) + (jt_value_injective_targetbound))) /\ (exists jt_gap_injective_targetboundvalue. jt_gap_injective_targetboundvalue+S (jt_value_injective_targetbound)=(n)))) /\ (forall jt_divisor_injective_targetprimitive. (exists jt_factor_injective_targetprimitivemodulus. (n)=(jt_divisor_injective_targetprimitive)*jt_factor_injective_targetprimitivemodulus) -> (forall jt_index_injective_targetprimitivecoordinates jt_value_injective_targetprimitivecoordinates. (exists jt_gap_injective_targetprimitivecoordinatesindex. jt_gap_injective_targetprimitivecoordinatesindex+S (jt_index_injective_targetprimitivecoordinates)=(k)) -> (((exists fs_h_jt_injective_targetprimitivecoordinatesat. fs_h_jt_injective_targetprimitivecoordinatesat + S (jt_value_injective_targetprimitivecoordinates) = S ((S (jt_index_injective_targetprimitivecoordinates)) * jt_c_injective_target)) /\ exists fs_q_jt_injective_targetprimitivecoordinatesat. jt_b_injective_target = fs_q_jt_injective_targetprimitivecoordinatesat * S ((S (jt_index_injective_targetprimitivecoordinates)) * jt_c_injective_target) + (jt_value_injective_targetprimitivecoordinates))) -> (exists jt_factor_injective_targetprimitivecoordinatesdivides. (jt_value_injective_targetprimitivecoordinates)=(jt_divisor_injective_targetprimitive)*jt_factor_injective_targetprimitivecoordinatesdivides)) -> jt_divisor_injective_targetprimitive=1))))) /\ (((forall jt_b_injective_target jt_c_injective_target. (forall jt_index_injective_targetinputbound. (exists jt_gap_injective_targetinputboundindex. jt_gap_injective_targetinputboundindex+S (jt_index_injective_targetinputbound)=(k)) -> exists jt_value_injective_targetinputbound. ((((exists fs_h_jt_injective_targetinputboundat. fs_h_jt_injective_targetinputboundat + S (jt_value_injective_targetinputbound) = S ((S (jt_index_injective_targetinputbound)) * jt_c_injective_target)) /\ exists fs_q_jt_injective_targetinputboundat. jt_b_injective_target = fs_q_jt_injective_targetinputboundat * S ((S (jt_index_injective_targetinputbound)) * jt_c_injective_target) + (jt_value_injective_targetinputbound))) /\ (exists jt_gap_injective_targetinputboundvalue. jt_gap_injective_targetinputboundvalue+S (jt_value_injective_targetinputbound)=(n)))) -> (forall jt_divisor_injective_targetinputprimitive. (exists jt_factor_injective_targetinputprimitivemodulus. (n)=(jt_divisor_injective_targetinputprimitive)*jt_factor_injective_targetinputprimitivemodulus) -> (forall jt_index_injective_targetinputprimitivecoordinates jt_value_injective_targetinputprimitivecoordinates. (exists jt_gap_injective_targetinputprimitivecoordinatesindex. jt_gap_injective_targetinputprimitivecoordinatesindex+S (jt_index_injective_targetinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_injective_targetinputprimitivecoordinatesat. fs_h_jt_injective_targetinputprimitivecoordinatesat + S (jt_value_injective_targetinputprimitivecoordinates) = S ((S (jt_index_injective_targetinputprimitivecoordinates)) * jt_c_injective_target)) /\ exists fs_q_jt_injective_targetinputprimitivecoordinatesat. jt_b_injective_target = fs_q_jt_injective_targetinputprimitivecoordinatesat * S ((S (jt_index_injective_targetinputprimitivecoordinates)) * jt_c_injective_target) + (jt_value_injective_targetinputprimitivecoordinates))) -> (exists jt_factor_injective_targetinputprimitivecoordinatesdivides. (jt_value_injective_targetinputprimitivecoordinates)=(jt_divisor_injective_targetinputprimitive)*jt_factor_injective_targetinputprimitivecoordinatesdivides)) -> jt_divisor_injective_targetinputprimitive=1) -> exists jt_i_injective_target jt_d_injective_target jt_e_injective_target. ((exists jt_gap_injective_targetcompleteindex. jt_gap_injective_targetcompleteindex+S (jt_i_injective_target)=(v)) /\ (((((((exists fs_h_jt_injective_targetcompletecode. fs_h_jt_injective_targetcompletecode + S (jt_d_injective_target) = S ((S (jt_i_injective_target)) * F)) /\ exists fs_q_jt_injective_targetcompletecode. E = fs_q_jt_injective_targetcompletecode * S ((S (jt_i_injective_target)) * F) + (jt_d_injective_target))) /\ (((exists fs_h_jt_injective_targetcompletescale. fs_h_jt_injective_targetcompletescale + S (jt_e_injective_target) = S ((S (jt_i_injective_target)) * H)) /\ exists fs_q_jt_injective_targetcompletescale. G = fs_q_jt_injective_targetcompletescale * S ((S (jt_i_injective_target)) * H) + (jt_e_injective_target))))) /\ (forall jt_index_injective_targetrepresented jt_left_injective_targetrepresented jt_right_injective_targetrepresented. (exists jt_gap_injective_targetrepresentedindex. jt_gap_injective_targetrepresentedindex+S (jt_index_injective_targetrepresented)=(k)) -> (((exists fs_h_jt_injective_targetrepresentedleft. fs_h_jt_injective_targetrepresentedleft + S (jt_left_injective_targetrepresented) = S ((S (jt_index_injective_targetrepresented)) * jt_c_injective_target)) /\ exists fs_q_jt_injective_targetrepresentedleft. jt_b_injective_target = fs_q_jt_injective_targetrepresentedleft * S ((S (jt_index_injective_targetrepresented)) * jt_c_injective_target) + (jt_left_injective_targetrepresented))) -> (((exists fs_h_jt_injective_targetrepresentedright. fs_h_jt_injective_targetrepresentedright + S (jt_right_injective_targetrepresented) = S ((S (jt_index_injective_targetrepresented)) * jt_e_injective_target)) /\ exists fs_q_jt_injective_targetrepresentedright. jt_d_injective_target = fs_q_jt_injective_targetrepresentedright * S ((S (jt_index_injective_targetrepresented)) * jt_e_injective_target) + (jt_right_injective_targetrepresented))) -> jt_left_injective_targetrepresented=jt_right_injective_targetrepresented))))) /\ (forall jt_i_injective_target jt_h_injective_target jt_b_injective_target jt_c_injective_target jt_d_injective_target jt_e_injective_target. (exists jt_gap_injective_targetfirstindex. jt_gap_injective_targetfirstindex+S (jt_i_injective_target)=(v)) -> (exists jt_gap_injective_targetsecondindex. jt_gap_injective_targetsecondindex+S (jt_h_injective_target)=(v)) -> (((((exists fs_h_jt_injective_targetfirstcode. fs_h_jt_injective_targetfirstcode + S (jt_b_injective_target) = S ((S (jt_i_injective_target)) * F)) /\ exists fs_q_jt_injective_targetfirstcode. E = fs_q_jt_injective_targetfirstcode * S ((S (jt_i_injective_target)) * F) + (jt_b_injective_target))) /\ (((exists fs_h_jt_injective_targetfirstscale. fs_h_jt_injective_targetfirstscale + S (jt_c_injective_target) = S ((S (jt_i_injective_target)) * H)) /\ exists fs_q_jt_injective_targetfirstscale. G = fs_q_jt_injective_targetfirstscale * S ((S (jt_i_injective_target)) * H) + (jt_c_injective_target))))) -> (((((exists fs_h_jt_injective_targetsecondcode. fs_h_jt_injective_targetsecondcode + S (jt_d_injective_target) = S ((S (jt_h_injective_target)) * F)) /\ exists fs_q_jt_injective_targetsecondcode. E = fs_q_jt_injective_targetsecondcode * S ((S (jt_h_injective_target)) * F) + (jt_d_injective_target))) /\ (((exists fs_h_jt_injective_targetsecondscale. fs_h_jt_injective_targetsecondscale + S (jt_e_injective_target) = S ((S (jt_h_injective_target)) * H)) /\ exists fs_q_jt_injective_targetsecondscale. G = fs_q_jt_injective_targetsecondscale * S ((S (jt_h_injective_target)) * H) + (jt_e_injective_target))))) -> (forall jt_index_injective_targetsame jt_left_injective_targetsame jt_right_injective_targetsame. (exists jt_gap_injective_targetsameindex. jt_gap_injective_targetsameindex+S (jt_index_injective_targetsame)=(k)) -> (((exists fs_h_jt_injective_targetsameleft. fs_h_jt_injective_targetsameleft + S (jt_left_injective_targetsame) = S ((S (jt_index_injective_targetsame)) * jt_c_injective_target)) /\ exists fs_q_jt_injective_targetsameleft. jt_b_injective_target = fs_q_jt_injective_targetsameleft * S ((S (jt_index_injective_targetsame)) * jt_c_injective_target) + (jt_left_injective_targetsame))) -> (((exists fs_h_jt_injective_targetsameright. fs_h_jt_injective_targetsameright + S (jt_right_injective_targetsame) = S ((S (jt_index_injective_targetsame)) * jt_e_injective_target)) /\ exists fs_q_jt_injective_targetsameright. jt_d_injective_target = fs_q_jt_injective_targetsameright * S ((S (jt_index_injective_targetsame)) * jt_e_injective_target) + (jt_right_injective_targetsame))) -> jt_left_injective_targetsame=jt_right_injective_targetsame) -> jt_i_injective_target=jt_h_injective_target))))) -> (forall jt_index_injective_map. (exists jt_gap_injective_mapindex. jt_gap_injective_mapindex+S (jt_index_injective_map)=(u)) -> exists jt_image_injective_map. ((((exists fs_h_jt_injective_mapat. fs_h_jt_injective_mapat + S (jt_image_injective_map) = S ((S (jt_index_injective_map)) * W)) /\ exists fs_q_jt_injective_mapat. Z = fs_q_jt_injective_mapat * S ((S (jt_index_injective_map)) * W) + (jt_image_injective_map))) /\ (((exists jt_gap_injective_mapbound. jt_gap_injective_mapbound+S (jt_image_injective_map)=(v)) /\ (forall jt_b_injective_mapmatch jt_c_injective_mapmatch jt_d_injective_mapmatch jt_e_injective_mapmatch. (((((exists fs_h_jt_injective_mapmatchleftcode. fs_h_jt_injective_mapmatchleftcode + S (jt_b_injective_mapmatch) = S ((S (jt_index_injective_map)) * B)) /\ exists fs_q_jt_injective_mapmatchleftcode. A = fs_q_jt_injective_mapmatchleftcode * S ((S (jt_index_injective_map)) * B) + (jt_b_injective_mapmatch))) /\ (((exists fs_h_jt_injective_mapmatchleftscale. fs_h_jt_injective_mapmatchleftscale + S (jt_c_injective_mapmatch) = S ((S (jt_index_injective_map)) * D)) /\ exists fs_q_jt_injective_mapmatchleftscale. C = fs_q_jt_injective_mapmatchleftscale * S ((S (jt_index_injective_map)) * D) + (jt_c_injective_mapmatch))))) -> (((((exists fs_h_jt_injective_mapmatchrightcode. fs_h_jt_injective_mapmatchrightcode + S (jt_d_injective_mapmatch) = S ((S (jt_image_injective_map)) * F)) /\ exists fs_q_jt_injective_mapmatchrightcode. E = fs_q_jt_injective_mapmatchrightcode * S ((S (jt_image_injective_map)) * F) + (jt_d_injective_mapmatch))) /\ (((exists fs_h_jt_injective_mapmatchrightscale. fs_h_jt_injective_mapmatchrightscale + S (jt_e_injective_mapmatch) = S ((S (jt_image_injective_map)) * H)) /\ exists fs_q_jt_injective_mapmatchrightscale. G = fs_q_jt_injective_mapmatchrightscale * S ((S (jt_image_injective_map)) * H) + (jt_e_injective_mapmatch))))) -> (forall jt_index_injective_mapmatchequal jt_left_injective_mapmatchequal jt_right_injective_mapmatchequal. (exists jt_gap_injective_mapmatchequalindex. jt_gap_injective_mapmatchequalindex+S (jt_index_injective_mapmatchequal)=(k)) -> (((exists fs_h_jt_injective_mapmatchequalleft. fs_h_jt_injective_mapmatchequalleft + S (jt_left_injective_mapmatchequal) = S ((S (jt_index_injective_mapmatchequal)) * jt_c_injective_mapmatch)) /\ exists fs_q_jt_injective_mapmatchequalleft. jt_b_injective_mapmatch = fs_q_jt_injective_mapmatchequalleft * S ((S (jt_index_injective_mapmatchequal)) * jt_c_injective_mapmatch) + (jt_left_injective_mapmatchequal))) -> (((exists fs_h_jt_injective_mapmatchequalright. fs_h_jt_injective_mapmatchequalright + S (jt_right_injective_mapmatchequal) = S ((S (jt_index_injective_mapmatchequal)) * jt_e_injective_mapmatch)) /\ exists fs_q_jt_injective_mapmatchequalright. jt_d_injective_mapmatch = fs_q_jt_injective_mapmatchequalright * S ((S (jt_index_injective_mapmatchequal)) * jt_e_injective_mapmatch) + (jt_right_injective_mapmatchequal))) -> jt_left_injective_mapmatchequal=jt_right_injective_mapmatchequal)))))) -> (((forall jt_index_injective_bound. (exists jt_gap_injective_boundindex. jt_gap_injective_boundindex+S (jt_index_injective_bound)=(u)) -> exists jt_value_injective_bound. ((((exists fs_h_jt_injective_boundat. fs_h_jt_injective_boundat + S (jt_value_injective_bound) = S ((S (jt_index_injective_bound)) * W)) /\ exists fs_q_jt_injective_boundat. Z = fs_q_jt_injective_boundat * S ((S (jt_index_injective_bound)) * W) + (jt_value_injective_bound))) /\ (exists jt_gap_injective_boundvalue. jt_gap_injective_boundvalue+S (jt_value_injective_bound)=(v)))) /\ (forall fp_i_jordan_injective fp_j_jordan_injective fp_value_jordan_injective. (exists fp_gap_jordan_injective_i. fp_gap_jordan_injective_i + S fp_i_jordan_injective = u) -> (exists fp_gap_jordan_injective_j. fp_gap_jordan_injective_j + S fp_j_jordan_injective = u) -> (((exists ff_h_jordan_injective_left. ff_h_jordan_injective_left + S (fp_value_jordan_injective) = S ((S (fp_i_jordan_injective)) * W)) /\ exists ff_q_jordan_injective_left. Z = ff_q_jordan_injective_left * S ((S (fp_i_jordan_injective)) * W) + (fp_value_jordan_injective))) -> (((exists ff_h_jordan_injective_right. ff_h_jordan_injective_right + S (fp_value_jordan_injective) = S ((S (fp_j_jordan_injective)) * W)) /\ exists ff_q_jordan_injective_right. Z = ff_q_jordan_injective_right * S ((S (fp_j_jordan_injective)) * W) + (fp_value_jordan_injective))) -> fp_i_jordan_injective = fp_j_jordan_injective)))