Definition in prerequisite notation
S x ≤ S (S i · c) ∧ (∃ y. b = y · S (S i · c) + x)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((exists ff_h_defined_beta_at. ff_h_defined_beta_at + S (x) = S ((S (i)) * c)) /\ exists ff_q_defined_beta_at. b = ff_q_defined_beta_at * S ((S (i)) * c) + (x))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
none — first-order arithmetic only
Definitions depending on this notation
Product(b,c,l,z)Repeat(b,c,a,l)UniformBetaPrefixBox(c,T,l,B)FiniteMatrixSelector(b,c,l,B)IntegerVectorZero(ab,ac,db,dc,l)BetaPrefixInto(b,c,l,B)BetaPrefixEqual(b,c,d,e,l)FpCoefficientReduction(p,b,c,d,e,l)JordanTupleAllDivisible(d,b,c,k)JordanTupleCongruence(n,b,c,d,e,k)JordanTupleEnumeration(k,n,B,C,D,E,j)JordanTupleListed(b,c,k,B,C,D,E,j)JordanTupleScan(k,n,c,limit,B,C,D,E,j)JordanTupleCRT(m,n,b,c,d,e,f,g,k)JordanRectangleCRT(m,n,k,A,B,C,D,u,E,F,G,H,v,P,Q,R,T,q)
Checked theorems using this definition
JT0003 · jordan_tuple_equal_transJT0004 · jordan_tuple_common_divisor_transportJT000F · jordan_primitive_tuple_congruence_transportJT0011 · jordan_tuple_all_divisible_extendJT0012 · jordan_tuple_all_divisible_decidableJT0018 · jordan_tuple_equal_extendJT0019 · jordan_tuple_equal_decidableJT001C · jordan_tuple_listed_decidableJT001F · jordan_tuple_equal_entryJT0020 · jordan_tuple_bounded_transportJT0021 · jordan_tuple_outer_append_existsJT0026 · jordan_tuple_scan_appendJT002B · jordan_crt_tuple_extendJT002C · jordan_crt_tuple_existsJT002D · jordan_crt_tuple_leftJT002E · jordan_crt_tuple_rightJT0030 · jordan_tuple_congruence_transJT003D · jordan_enumeration_actual_valueJT003F · jordan_enumeration_distinctJT0040 · jordan_rectangle_crt_appendJT0043 · jordan_rectangle_crt_actual_entryJT0044 · jordan_rectangle_crt_pair_valueJT0045 · jordan_enumeration_reduce_primitiveJT0046 · jordan_rectangle_crt_distinctJT0047 · jordan_rectangle_crt_coversJT0048 · jordan_rectangle_crt_enumerationJT004C · jordan_enumeration_position_match_from_entriesJT004D · jordan_enumeration_position_match_existsJT004E · jordan_enumeration_index_map_emptyJT004F · jordan_enumeration_index_map_appendJT0050 · jordan_enumeration_index_map_existsJT0051 · jordan_enumeration_index_map_entryJT0052 · jordan_enumeration_index_map_bounded_injectiveJT0053 · jordan_enumeration_cardinality_leJT0057 · jordan_tuple_bounded_one_entry_zero