Definition in prerequisite notation
S a ≤ bOnly definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists h. h + S a = bThe 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
DivRem(n,d,q,r)Product(b,c,l,z)Repeat(b,c,a,l)CanonicalModularResidue(m,a,r)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)JordanTupleRepresentatives(k,n,c,T)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
JT0011 · jordan_tuple_all_divisible_extendJT0014 · jordan_tuple_primitive_bounded_decidableJT0015 · jordan_primitive_tuple_decidableJT0018 · jordan_tuple_equal_extendJT001C · jordan_tuple_listed_decidableJT001F · jordan_tuple_equal_entryJT0020 · jordan_tuple_bounded_transportJT0023 · jordan_tuple_scan_skipJT0024 · jordan_tuple_scan_completeJT0026 · jordan_tuple_scan_appendJT0028 · jordan_tuple_representatives_existsJT002B · jordan_crt_tuple_extendJT0034 · jordan_rectangle_width_nonzeroJT0035 · jordan_rectangle_quotient_boundJT0036 · jordan_rectangle_flat_boundJT0037 · jordan_rectangle_pair_uniqueJT003D · jordan_enumeration_actual_valueJT003F · jordan_enumeration_distinctJT0040 · jordan_rectangle_crt_appendJT0041 · jordan_rectangle_crt_successorJT0043 · 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_enumerationJT004D · 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