RegistryUniquenessVariantMC

Complete selected asymmetric reference profile. Definitions and supplied fixtures are distinct from the three teaching specializations; review and qualification are stated in the bound evidence and release.

Package reference-profile, input revision 2. Exact prepared source; CC0 1.0.

This is a definition inventory. Start with the learning chapters for the contract and its assumptions.

DefectBodyRegistryUniquenessVariant · operator

reference-profile · input revision 2 · CC0 1.0

DefectBodyRegistryUniquenessVariant(catalog) ==
 IF ~IsFunctionValueSA(catalog) THEN FALSE
 ELSE IF ~IsFiniteSet(DOMAIN catalog) THEN FALSE
 ELSE IF ~(\A key \in DOMAIN catalog : IsNaturalValueSA(key)) THEN FALSE
 ELSE IF ~(DOMAIN catalog \subseteq Nat \ {0}) THEN FALSE
 ELSE IF ~(\A key \in DOMAIN catalog : RowValidSA(catalog[key])) THEN FALSE
 ELSE \A a,b \in DOMAIN catalog :
   TRUE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: IsFunctionValueSA, IsNaturalValueSA, RowValidSA