jordan_enumeration_cardinality_unique

Exact expanded first-order arithmetic statement

forall k n A B C D u E F G H v. (((forall jt_i_cardinality_left. (exists jt_gap_cardinality_leftsoundindex. jt_gap_cardinality_leftsoundindex+S (jt_i_cardinality_left)=(u)) -> exists jt_b_cardinality_left jt_c_cardinality_left. ((((((exists fs_h_jt_cardinality_leftsoundcode. fs_h_jt_cardinality_leftsoundcode + S (jt_b_cardinality_left) = S ((S (jt_i_cardinality_left)) * B)) /\ exists fs_q_jt_cardinality_leftsoundcode. A = fs_q_jt_cardinality_leftsoundcode * S ((S (jt_i_cardinality_left)) * B) + (jt_b_cardinality_left))) /\ (((exists fs_h_jt_cardinality_leftsoundscale. fs_h_jt_cardinality_leftsoundscale + S (jt_c_cardinality_left) = S ((S (jt_i_cardinality_left)) * D)) /\ exists fs_q_jt_cardinality_leftsoundscale. C = fs_q_jt_cardinality_leftsoundscale * S ((S (jt_i_cardinality_left)) * D) + (jt_c_cardinality_left))))) /\ (((forall jt_index_cardinality_leftbound. (exists jt_gap_cardinality_leftboundindex. jt_gap_cardinality_leftboundindex+S (jt_index_cardinality_leftbound)=(k)) -> exists jt_value_cardinality_leftbound. ((((exists fs_h_jt_cardinality_leftboundat. fs_h_jt_cardinality_leftboundat + S (jt_value_cardinality_leftbound) = S ((S (jt_index_cardinality_leftbound)) * jt_c_cardinality_left)) /\ exists fs_q_jt_cardinality_leftboundat. jt_b_cardinality_left = fs_q_jt_cardinality_leftboundat * S ((S (jt_index_cardinality_leftbound)) * jt_c_cardinality_left) + (jt_value_cardinality_leftbound))) /\ (exists jt_gap_cardinality_leftboundvalue. jt_gap_cardinality_leftboundvalue+S (jt_value_cardinality_leftbound)=(n)))) /\ (forall jt_divisor_cardinality_leftprimitive. (exists jt_factor_cardinality_leftprimitivemodulus. (n)=(jt_divisor_cardinality_leftprimitive)*jt_factor_cardinality_leftprimitivemodulus) -> (forall jt_index_cardinality_leftprimitivecoordinates jt_value_cardinality_leftprimitivecoordinates. (exists jt_gap_cardinality_leftprimitivecoordinatesindex. jt_gap_cardinality_leftprimitivecoordinatesindex+S (jt_index_cardinality_leftprimitivecoordinates)=(k)) -> (((exists fs_h_jt_cardinality_leftprimitivecoordinatesat. fs_h_jt_cardinality_leftprimitivecoordinatesat + S (jt_value_cardinality_leftprimitivecoordinates) = S ((S (jt_index_cardinality_leftprimitivecoordinates)) * jt_c_cardinality_left)) /\ exists fs_q_jt_cardinality_leftprimitivecoordinatesat. jt_b_cardinality_left = fs_q_jt_cardinality_leftprimitivecoordinatesat * S ((S (jt_index_cardinality_leftprimitivecoordinates)) * jt_c_cardinality_left) + (jt_value_cardinality_leftprimitivecoordinates))) -> (exists jt_factor_cardinality_leftprimitivecoordinatesdivides. (jt_value_cardinality_leftprimitivecoordinates)=(jt_divisor_cardinality_leftprimitive)*jt_factor_cardinality_leftprimitivecoordinatesdivides)) -> jt_divisor_cardinality_leftprimitive=1))))) /\ (((forall jt_b_cardinality_left jt_c_cardinality_left. (forall jt_index_cardinality_leftinputbound. (exists jt_gap_cardinality_leftinputboundindex. jt_gap_cardinality_leftinputboundindex+S (jt_index_cardinality_leftinputbound)=(k)) -> exists jt_value_cardinality_leftinputbound. ((((exists fs_h_jt_cardinality_leftinputboundat. fs_h_jt_cardinality_leftinputboundat + S (jt_value_cardinality_leftinputbound) = S ((S (jt_index_cardinality_leftinputbound)) * jt_c_cardinality_left)) /\ exists fs_q_jt_cardinality_leftinputboundat. jt_b_cardinality_left = fs_q_jt_cardinality_leftinputboundat * S ((S (jt_index_cardinality_leftinputbound)) * jt_c_cardinality_left) + (jt_value_cardinality_leftinputbound))) /\ (exists jt_gap_cardinality_leftinputboundvalue. jt_gap_cardinality_leftinputboundvalue+S (jt_value_cardinality_leftinputbound)=(n)))) -> (forall jt_divisor_cardinality_leftinputprimitive. (exists jt_factor_cardinality_leftinputprimitivemodulus. (n)=(jt_divisor_cardinality_leftinputprimitive)*jt_factor_cardinality_leftinputprimitivemodulus) -> (forall jt_index_cardinality_leftinputprimitivecoordinates jt_value_cardinality_leftinputprimitivecoordinates. (exists jt_gap_cardinality_leftinputprimitivecoordinatesindex. jt_gap_cardinality_leftinputprimitivecoordinatesindex+S (jt_index_cardinality_leftinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_cardinality_leftinputprimitivecoordinatesat. fs_h_jt_cardinality_leftinputprimitivecoordinatesat + S (jt_value_cardinality_leftinputprimitivecoordinates) = S ((S (jt_index_cardinality_leftinputprimitivecoordinates)) * jt_c_cardinality_left)) /\ exists fs_q_jt_cardinality_leftinputprimitivecoordinatesat. jt_b_cardinality_left = fs_q_jt_cardinality_leftinputprimitivecoordinatesat * S ((S (jt_index_cardinality_leftinputprimitivecoordinates)) * jt_c_cardinality_left) + (jt_value_cardinality_leftinputprimitivecoordinates))) -> (exists jt_factor_cardinality_leftinputprimitivecoordinatesdivides. (jt_value_cardinality_leftinputprimitivecoordinates)=(jt_divisor_cardinality_leftinputprimitive)*jt_factor_cardinality_leftinputprimitivecoordinatesdivides)) -> jt_divisor_cardinality_leftinputprimitive=1) -> exists jt_i_cardinality_left jt_d_cardinality_left jt_e_cardinality_left. ((exists jt_gap_cardinality_leftcompleteindex. jt_gap_cardinality_leftcompleteindex+S (jt_i_cardinality_left)=(u)) /\ (((((((exists fs_h_jt_cardinality_leftcompletecode. fs_h_jt_cardinality_leftcompletecode + S (jt_d_cardinality_left) = S ((S (jt_i_cardinality_left)) * B)) /\ exists fs_q_jt_cardinality_leftcompletecode. A = fs_q_jt_cardinality_leftcompletecode * S ((S (jt_i_cardinality_left)) * B) + (jt_d_cardinality_left))) /\ (((exists fs_h_jt_cardinality_leftcompletescale. fs_h_jt_cardinality_leftcompletescale + S (jt_e_cardinality_left) = S ((S (jt_i_cardinality_left)) * D)) /\ exists fs_q_jt_cardinality_leftcompletescale. C = fs_q_jt_cardinality_leftcompletescale * S ((S (jt_i_cardinality_left)) * D) + (jt_e_cardinality_left))))) /\ (forall jt_index_cardinality_leftrepresented jt_left_cardinality_leftrepresented jt_right_cardinality_leftrepresented. (exists jt_gap_cardinality_leftrepresentedindex. jt_gap_cardinality_leftrepresentedindex+S (jt_index_cardinality_leftrepresented)=(k)) -> (((exists fs_h_jt_cardinality_leftrepresentedleft. fs_h_jt_cardinality_leftrepresentedleft + S (jt_left_cardinality_leftrepresented) = S ((S (jt_index_cardinality_leftrepresented)) * jt_c_cardinality_left)) /\ exists fs_q_jt_cardinality_leftrepresentedleft. jt_b_cardinality_left = fs_q_jt_cardinality_leftrepresentedleft * S ((S (jt_index_cardinality_leftrepresented)) * jt_c_cardinality_left) + (jt_left_cardinality_leftrepresented))) -> (((exists fs_h_jt_cardinality_leftrepresentedright. fs_h_jt_cardinality_leftrepresentedright + S (jt_right_cardinality_leftrepresented) = S ((S (jt_index_cardinality_leftrepresented)) * jt_e_cardinality_left)) /\ exists fs_q_jt_cardinality_leftrepresentedright. jt_d_cardinality_left = fs_q_jt_cardinality_leftrepresentedright * S ((S (jt_index_cardinality_leftrepresented)) * jt_e_cardinality_left) + (jt_right_cardinality_leftrepresented))) -> jt_left_cardinality_leftrepresented=jt_right_cardinality_leftrepresented))))) /\ (forall jt_i_cardinality_left jt_h_cardinality_left jt_b_cardinality_left jt_c_cardinality_left jt_d_cardinality_left jt_e_cardinality_left. (exists jt_gap_cardinality_leftfirstindex. jt_gap_cardinality_leftfirstindex+S (jt_i_cardinality_left)=(u)) -> (exists jt_gap_cardinality_leftsecondindex. jt_gap_cardinality_leftsecondindex+S (jt_h_cardinality_left)=(u)) -> (((((exists fs_h_jt_cardinality_leftfirstcode. fs_h_jt_cardinality_leftfirstcode + S (jt_b_cardinality_left) = S ((S (jt_i_cardinality_left)) * B)) /\ exists fs_q_jt_cardinality_leftfirstcode. A = fs_q_jt_cardinality_leftfirstcode * S ((S (jt_i_cardinality_left)) * B) + (jt_b_cardinality_left))) /\ (((exists fs_h_jt_cardinality_leftfirstscale. fs_h_jt_cardinality_leftfirstscale + S (jt_c_cardinality_left) = S ((S (jt_i_cardinality_left)) * D)) /\ exists fs_q_jt_cardinality_leftfirstscale. C = fs_q_jt_cardinality_leftfirstscale * S ((S (jt_i_cardinality_left)) * D) + (jt_c_cardinality_left))))) -> (((((exists fs_h_jt_cardinality_leftsecondcode. fs_h_jt_cardinality_leftsecondcode + S (jt_d_cardinality_left) = S ((S (jt_h_cardinality_left)) * B)) /\ exists fs_q_jt_cardinality_leftsecondcode. A = fs_q_jt_cardinality_leftsecondcode * S ((S (jt_h_cardinality_left)) * B) + (jt_d_cardinality_left))) /\ (((exists fs_h_jt_cardinality_leftsecondscale. fs_h_jt_cardinality_leftsecondscale + S (jt_e_cardinality_left) = S ((S (jt_h_cardinality_left)) * D)) /\ exists fs_q_jt_cardinality_leftsecondscale. C = fs_q_jt_cardinality_leftsecondscale * S ((S (jt_h_cardinality_left)) * D) + (jt_e_cardinality_left))))) -> (forall jt_index_cardinality_leftsame jt_left_cardinality_leftsame jt_right_cardinality_leftsame. (exists jt_gap_cardinality_leftsameindex. jt_gap_cardinality_leftsameindex+S (jt_index_cardinality_leftsame)=(k)) -> (((exists fs_h_jt_cardinality_leftsameleft. fs_h_jt_cardinality_leftsameleft + S (jt_left_cardinality_leftsame) = S ((S (jt_index_cardinality_leftsame)) * jt_c_cardinality_left)) /\ exists fs_q_jt_cardinality_leftsameleft. jt_b_cardinality_left = fs_q_jt_cardinality_leftsameleft * S ((S (jt_index_cardinality_leftsame)) * jt_c_cardinality_left) + (jt_left_cardinality_leftsame))) -> (((exists fs_h_jt_cardinality_leftsameright. fs_h_jt_cardinality_leftsameright + S (jt_right_cardinality_leftsame) = S ((S (jt_index_cardinality_leftsame)) * jt_e_cardinality_left)) /\ exists fs_q_jt_cardinality_leftsameright. jt_d_cardinality_left = fs_q_jt_cardinality_leftsameright * S ((S (jt_index_cardinality_leftsame)) * jt_e_cardinality_left) + (jt_right_cardinality_leftsame))) -> jt_left_cardinality_leftsame=jt_right_cardinality_leftsame) -> jt_i_cardinality_left=jt_h_cardinality_left))))) -> (((forall jt_i_cardinality_right. (exists jt_gap_cardinality_rightsoundindex. jt_gap_cardinality_rightsoundindex+S (jt_i_cardinality_right)=(v)) -> exists jt_b_cardinality_right jt_c_cardinality_right. ((((((exists fs_h_jt_cardinality_rightsoundcode. fs_h_jt_cardinality_rightsoundcode + S (jt_b_cardinality_right) = S ((S (jt_i_cardinality_right)) * F)) /\ exists fs_q_jt_cardinality_rightsoundcode. E = fs_q_jt_cardinality_rightsoundcode * S ((S (jt_i_cardinality_right)) * F) + (jt_b_cardinality_right))) /\ (((exists fs_h_jt_cardinality_rightsoundscale. fs_h_jt_cardinality_rightsoundscale + S (jt_c_cardinality_right) = S ((S (jt_i_cardinality_right)) * H)) /\ exists fs_q_jt_cardinality_rightsoundscale. G = fs_q_jt_cardinality_rightsoundscale * S ((S (jt_i_cardinality_right)) * H) + (jt_c_cardinality_right))))) /\ (((forall jt_index_cardinality_rightbound. (exists jt_gap_cardinality_rightboundindex. jt_gap_cardinality_rightboundindex+S (jt_index_cardinality_rightbound)=(k)) -> exists jt_value_cardinality_rightbound. ((((exists fs_h_jt_cardinality_rightboundat. fs_h_jt_cardinality_rightboundat + S (jt_value_cardinality_rightbound) = S ((S (jt_index_cardinality_rightbound)) * jt_c_cardinality_right)) /\ exists fs_q_jt_cardinality_rightboundat. jt_b_cardinality_right = fs_q_jt_cardinality_rightboundat * S ((S (jt_index_cardinality_rightbound)) * jt_c_cardinality_right) + (jt_value_cardinality_rightbound))) /\ (exists jt_gap_cardinality_rightboundvalue. jt_gap_cardinality_rightboundvalue+S (jt_value_cardinality_rightbound)=(n)))) /\ (forall jt_divisor_cardinality_rightprimitive. (exists jt_factor_cardinality_rightprimitivemodulus. (n)=(jt_divisor_cardinality_rightprimitive)*jt_factor_cardinality_rightprimitivemodulus) -> (forall jt_index_cardinality_rightprimitivecoordinates jt_value_cardinality_rightprimitivecoordinates. (exists jt_gap_cardinality_rightprimitivecoordinatesindex. jt_gap_cardinality_rightprimitivecoordinatesindex+S (jt_index_cardinality_rightprimitivecoordinates)=(k)) -> (((exists fs_h_jt_cardinality_rightprimitivecoordinatesat. fs_h_jt_cardinality_rightprimitivecoordinatesat + S (jt_value_cardinality_rightprimitivecoordinates) = S ((S (jt_index_cardinality_rightprimitivecoordinates)) * jt_c_cardinality_right)) /\ exists fs_q_jt_cardinality_rightprimitivecoordinatesat. jt_b_cardinality_right = fs_q_jt_cardinality_rightprimitivecoordinatesat * S ((S (jt_index_cardinality_rightprimitivecoordinates)) * jt_c_cardinality_right) + (jt_value_cardinality_rightprimitivecoordinates))) -> (exists jt_factor_cardinality_rightprimitivecoordinatesdivides. (jt_value_cardinality_rightprimitivecoordinates)=(jt_divisor_cardinality_rightprimitive)*jt_factor_cardinality_rightprimitivecoordinatesdivides)) -> jt_divisor_cardinality_rightprimitive=1))))) /\ (((forall jt_b_cardinality_right jt_c_cardinality_right. (forall jt_index_cardinality_rightinputbound. (exists jt_gap_cardinality_rightinputboundindex. jt_gap_cardinality_rightinputboundindex+S (jt_index_cardinality_rightinputbound)=(k)) -> exists jt_value_cardinality_rightinputbound. ((((exists fs_h_jt_cardinality_rightinputboundat. fs_h_jt_cardinality_rightinputboundat + S (jt_value_cardinality_rightinputbound) = S ((S (jt_index_cardinality_rightinputbound)) * jt_c_cardinality_right)) /\ exists fs_q_jt_cardinality_rightinputboundat. jt_b_cardinality_right = fs_q_jt_cardinality_rightinputboundat * S ((S (jt_index_cardinality_rightinputbound)) * jt_c_cardinality_right) + (jt_value_cardinality_rightinputbound))) /\ (exists jt_gap_cardinality_rightinputboundvalue. jt_gap_cardinality_rightinputboundvalue+S (jt_value_cardinality_rightinputbound)=(n)))) -> (forall jt_divisor_cardinality_rightinputprimitive. (exists jt_factor_cardinality_rightinputprimitivemodulus. (n)=(jt_divisor_cardinality_rightinputprimitive)*jt_factor_cardinality_rightinputprimitivemodulus) -> (forall jt_index_cardinality_rightinputprimitivecoordinates jt_value_cardinality_rightinputprimitivecoordinates. (exists jt_gap_cardinality_rightinputprimitivecoordinatesindex. jt_gap_cardinality_rightinputprimitivecoordinatesindex+S (jt_index_cardinality_rightinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_cardinality_rightinputprimitivecoordinatesat. fs_h_jt_cardinality_rightinputprimitivecoordinatesat + S (jt_value_cardinality_rightinputprimitivecoordinates) = S ((S (jt_index_cardinality_rightinputprimitivecoordinates)) * jt_c_cardinality_right)) /\ exists fs_q_jt_cardinality_rightinputprimitivecoordinatesat. jt_b_cardinality_right = fs_q_jt_cardinality_rightinputprimitivecoordinatesat * S ((S (jt_index_cardinality_rightinputprimitivecoordinates)) * jt_c_cardinality_right) + (jt_value_cardinality_rightinputprimitivecoordinates))) -> (exists jt_factor_cardinality_rightinputprimitivecoordinatesdivides. (jt_value_cardinality_rightinputprimitivecoordinates)=(jt_divisor_cardinality_rightinputprimitive)*jt_factor_cardinality_rightinputprimitivecoordinatesdivides)) -> jt_divisor_cardinality_rightinputprimitive=1) -> exists jt_i_cardinality_right jt_d_cardinality_right jt_e_cardinality_right. ((exists jt_gap_cardinality_rightcompleteindex. jt_gap_cardinality_rightcompleteindex+S (jt_i_cardinality_right)=(v)) /\ (((((((exists fs_h_jt_cardinality_rightcompletecode. fs_h_jt_cardinality_rightcompletecode + S (jt_d_cardinality_right) = S ((S (jt_i_cardinality_right)) * F)) /\ exists fs_q_jt_cardinality_rightcompletecode. E = fs_q_jt_cardinality_rightcompletecode * S ((S (jt_i_cardinality_right)) * F) + (jt_d_cardinality_right))) /\ (((exists fs_h_jt_cardinality_rightcompletescale. fs_h_jt_cardinality_rightcompletescale + S (jt_e_cardinality_right) = S ((S (jt_i_cardinality_right)) * H)) /\ exists fs_q_jt_cardinality_rightcompletescale. G = fs_q_jt_cardinality_rightcompletescale * S ((S (jt_i_cardinality_right)) * H) + (jt_e_cardinality_right))))) /\ (forall jt_index_cardinality_rightrepresented jt_left_cardinality_rightrepresented jt_right_cardinality_rightrepresented. (exists jt_gap_cardinality_rightrepresentedindex. jt_gap_cardinality_rightrepresentedindex+S (jt_index_cardinality_rightrepresented)=(k)) -> (((exists fs_h_jt_cardinality_rightrepresentedleft. fs_h_jt_cardinality_rightrepresentedleft + S (jt_left_cardinality_rightrepresented) = S ((S (jt_index_cardinality_rightrepresented)) * jt_c_cardinality_right)) /\ exists fs_q_jt_cardinality_rightrepresentedleft. jt_b_cardinality_right = fs_q_jt_cardinality_rightrepresentedleft * S ((S (jt_index_cardinality_rightrepresented)) * jt_c_cardinality_right) + (jt_left_cardinality_rightrepresented))) -> (((exists fs_h_jt_cardinality_rightrepresentedright. fs_h_jt_cardinality_rightrepresentedright + S (jt_right_cardinality_rightrepresented) = S ((S (jt_index_cardinality_rightrepresented)) * jt_e_cardinality_right)) /\ exists fs_q_jt_cardinality_rightrepresentedright. jt_d_cardinality_right = fs_q_jt_cardinality_rightrepresentedright * S ((S (jt_index_cardinality_rightrepresented)) * jt_e_cardinality_right) + (jt_right_cardinality_rightrepresented))) -> jt_left_cardinality_rightrepresented=jt_right_cardinality_rightrepresented))))) /\ (forall jt_i_cardinality_right jt_h_cardinality_right jt_b_cardinality_right jt_c_cardinality_right jt_d_cardinality_right jt_e_cardinality_right. (exists jt_gap_cardinality_rightfirstindex. jt_gap_cardinality_rightfirstindex+S (jt_i_cardinality_right)=(v)) -> (exists jt_gap_cardinality_rightsecondindex. jt_gap_cardinality_rightsecondindex+S (jt_h_cardinality_right)=(v)) -> (((((exists fs_h_jt_cardinality_rightfirstcode. fs_h_jt_cardinality_rightfirstcode + S (jt_b_cardinality_right) = S ((S (jt_i_cardinality_right)) * F)) /\ exists fs_q_jt_cardinality_rightfirstcode. E = fs_q_jt_cardinality_rightfirstcode * S ((S (jt_i_cardinality_right)) * F) + (jt_b_cardinality_right))) /\ (((exists fs_h_jt_cardinality_rightfirstscale. fs_h_jt_cardinality_rightfirstscale + S (jt_c_cardinality_right) = S ((S (jt_i_cardinality_right)) * H)) /\ exists fs_q_jt_cardinality_rightfirstscale. G = fs_q_jt_cardinality_rightfirstscale * S ((S (jt_i_cardinality_right)) * H) + (jt_c_cardinality_right))))) -> (((((exists fs_h_jt_cardinality_rightsecondcode. fs_h_jt_cardinality_rightsecondcode + S (jt_d_cardinality_right) = S ((S (jt_h_cardinality_right)) * F)) /\ exists fs_q_jt_cardinality_rightsecondcode. E = fs_q_jt_cardinality_rightsecondcode * S ((S (jt_h_cardinality_right)) * F) + (jt_d_cardinality_right))) /\ (((exists fs_h_jt_cardinality_rightsecondscale. fs_h_jt_cardinality_rightsecondscale + S (jt_e_cardinality_right) = S ((S (jt_h_cardinality_right)) * H)) /\ exists fs_q_jt_cardinality_rightsecondscale. G = fs_q_jt_cardinality_rightsecondscale * S ((S (jt_h_cardinality_right)) * H) + (jt_e_cardinality_right))))) -> (forall jt_index_cardinality_rightsame jt_left_cardinality_rightsame jt_right_cardinality_rightsame. (exists jt_gap_cardinality_rightsameindex. jt_gap_cardinality_rightsameindex+S (jt_index_cardinality_rightsame)=(k)) -> (((exists fs_h_jt_cardinality_rightsameleft. fs_h_jt_cardinality_rightsameleft + S (jt_left_cardinality_rightsame) = S ((S (jt_index_cardinality_rightsame)) * jt_c_cardinality_right)) /\ exists fs_q_jt_cardinality_rightsameleft. jt_b_cardinality_right = fs_q_jt_cardinality_rightsameleft * S ((S (jt_index_cardinality_rightsame)) * jt_c_cardinality_right) + (jt_left_cardinality_rightsame))) -> (((exists fs_h_jt_cardinality_rightsameright. fs_h_jt_cardinality_rightsameright + S (jt_right_cardinality_rightsame) = S ((S (jt_index_cardinality_rightsame)) * jt_e_cardinality_right)) /\ exists fs_q_jt_cardinality_rightsameright. jt_d_cardinality_right = fs_q_jt_cardinality_rightsameright * S ((S (jt_index_cardinality_rightsame)) * jt_e_cardinality_right) + (jt_right_cardinality_rightsame))) -> jt_left_cardinality_rightsame=jt_right_cardinality_rightsame) -> jt_i_cardinality_right=jt_h_cardinality_right))))) -> (u=v)