Documentation

d__Absorbs__8 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d__DistributesOver__10 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d__DistributesOver'691'__12 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d__DistributesOver'737'__14 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d__IdempotentOn__16 ∷ (Integer → Integer → Integer) → Integer → () Source #

d__MiddleFourExchange__18 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_Absorptive_20 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_AlmostCancellative_22 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_AlmostLeftCancellative_24 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_AlmostRightCancellative_26 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_Alternative_28 ∷ (Integer → Integer → Integer) → () Source #

d_Associative_30 ∷ (Integer → Integer → Integer) → () Source #

d_Cancellative_32 ∷ (Integer → Integer → Integer) → () Source #

d_Commutative_34 ∷ (Integer → Integer → Integer) → () Source #

d_Congruent'8321'_36 ∷ (Integer → Integer) → () Source #

d_Congruent'8322'_38 ∷ (Integer → Integer → Integer) → () Source #

d_Conical_40 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_Flexible_42 ∷ (Integer → Integer → Integer) → () Source #

d_Idempotent_44 ∷ (Integer → Integer → Integer) → () Source #

d_IdempotentFun_46 ∷ (Integer → Integer) → () Source #

d_Identical_48 ∷ (Integer → Integer → Integer) → () Source #

d_Identity_50 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_Interchangable_52 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_Inverse_54 ∷ Integer → (Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_Invertible_56 ∷ Integer → (Integer → Integer → Integer) → Integer → () Source #

d_Involutive_58 ∷ (Integer → Integer) → () Source #

d_LeftAlternative_60 ∷ (Integer → Integer → Integer) → () Source #

d_LeftBol_62 ∷ (Integer → Integer → Integer) → () Source #

d_LeftCancellative_64 ∷ (Integer → Integer → Integer) → () Source #

d_LeftCongruent_66 ∷ (Integer → Integer → Integer) → () Source #

d_LeftConical_68 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_LeftDivides_70 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_LeftDivides'691'_72 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_LeftDivides'737'_74 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_LeftIdentity_76 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_LeftInverse_78 ∷ Integer → (Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_LeftInvertible_80 ∷ Integer → (Integer → Integer → Integer) → Integer → () Source #

d_LeftSemimedial_82 ∷ (Integer → Integer → Integer) → () Source #

d_LeftZero_84 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_Medial_86 ∷ (Integer → Integer → Integer) → () Source #

d_MiddleBol_88 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_RightAlternative_90 ∷ (Integer → Integer → Integer) → () Source #

d_RightBol_92 ∷ (Integer → Integer → Integer) → () Source #

d_RightCancellative_94 ∷ (Integer → Integer → Integer) → () Source #

d_RightCongruent_96 ∷ (Integer → Integer → Integer) → () Source #

d_RightConical_98 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_RightDivides_100 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_RightDivides'691'_102 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_RightDivides'737'_104 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_RightIdentity_106 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_RightInverse_108 ∷ Integer → (Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_RightInvertible_110 ∷ Integer → (Integer → Integer → Integer) → Integer → () Source #

d_RightSemimedial_112 ∷ (Integer → Integer → Integer) → () Source #

d_RightZero_114 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_Selective_116 ∷ (Integer → Integer → Integer) → () Source #

d_SelfInverse_118 ∷ (Integer → Integer) → () Source #

d_Semimedial_120 ∷ (Integer → Integer → Integer) → () Source #

d_StarDestructive_122 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → () Source #

d_StarExpansive_124 ∷ Integer → (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → () Source #

d_StarLeftDestructive_126 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → () Source #

d_StarLeftExpansive_128 ∷ Integer → (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → () Source #

d_StarRightDestructive_130 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → () Source #

d_StarRightExpansive_132 ∷ Integer → (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → () Source #

d_Zero_134 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_IsAbelianGroup_138 ∷ p → p → p → () Source #

d_IsAlternativeMagma_142 ∷ p → () Source #

d_IsBand_146 ∷ p → () Source #

d_IsCancellativeCommutativeSemiring_150 ∷ p → p → p → p → () Source #

d_IsCommutativeBand_154 ∷ p → () Source #

d_IsCommutativeMagma_158 ∷ p → () Source #

d_IsCommutativeMonoid_162 ∷ p → p → () Source #

d_IsCommutativeRing_166 ∷ p → p → p → p → p → () Source #

d_IsCommutativeSemigroup_170 ∷ p → () Source #

d_IsCommutativeSemiring_174 ∷ p → p → p → p → () Source #

d_IsCommutativeSemiringWithoutOne_178 ∷ p → p → p → () Source #

d_IsFlexibleMagma_182 ∷ p → () Source #

d_IsGroup_186 ∷ p → p → p → () Source #

d_IsIdempotentCommutativeMonoid_190 ∷ p → p → () Source #

d_IsIdempotentMagma_194 ∷ p → () Source #

d_IsIdempotentMonoid_198 ∷ p → p → () Source #

d_IsIdempotentSemiring_202 ∷ p → p → p → p → () Source #

d_IsInvertibleMagma_206 ∷ p → p → p → () Source #

d_IsInvertibleUnitalMagma_210 ∷ p → p → p → () Source #

d_IsKleeneAlgebra_214 ∷ p → p → p → p → p → () Source #

d_IsLeftBolLoop_218 ∷ p → p → p → p → () Source #

d_IsLoop_222 ∷ p → p → p → p → () Source #

d_IsMagma_226 ∷ p → () Source #

d_IsMedialMagma_230 ∷ p → () Source #

d_IsMiddleBolLoop_234 ∷ p → p → p → p → () Source #

d_IsMonoid_238 ∷ p → p → () Source #

d_IsMoufangLoop_242 ∷ p → p → p → p → () Source #

d_IsNearSemiring_246 ∷ p → p → p → () Source #

d_IsNearring_250 ∷ p → p → p → p → p → () Source #

d_IsNonAssociativeRing_254 ∷ p → p → p → p → p → () Source #

d_IsQuasigroup_258 ∷ p → p → p → () Source #

d_IsQuasiring_262 ∷ p → p → p → p → () Source #

d_IsRightBolLoop_266 ∷ p → p → p → p → () Source #

d_IsRing_270 ∷ p → p → p → p → p → () Source #

d_IsRingWithoutOne_274 ∷ p → p → p → p → () Source #

d_IsSelectiveMagma_278 ∷ p → () Source #

d_IsSemigroup_282 ∷ p → () Source #

d_IsSemimedialMagma_286 ∷ p → () Source #

d_IsSemiring_290 ∷ p → p → p → p → () Source #

d_IsSemiringWithoutAnnihilatingZero_294 ∷ p → p → p → p → () Source #

d_IsSemiringWithoutOne_298 ∷ p → p → p → () Source #

d_IsSuccessorSet_302 ∷ p → p → () Source #

d_IsUnitalMagma_306 ∷ p → p → () Source #

d__'47''47'__312 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → Integer → Integer → Integer Source #

du__'47''47'__312 ∷ (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → Integer Source #

d_assoc_314 ∷ T_IsAbelianGroup_1172 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_316 ∷ T_IsAbelianGroup_1172 → Integer → Integer → T__'8801'__12 Source #

d_identity_318 ∷ T_IsAbelianGroup_1172 → T_Σ_14 Source #

d_identity'691'_320 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → Integer → T__'8801'__12 Source #

d_identity'737'_322 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → Integer → T__'8801'__12 Source #

d_inverse_324 ∷ T_IsAbelianGroup_1172 → T_Σ_14 Source #

d_inverse'691'_326 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → Integer → T__'8801'__12 Source #

d_inverse'737'_328 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → Integer → T__'8801'__12 Source #

d_isCommutativeMagma_330 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_330 ∷ T_IsAbelianGroup_1172 → T_IsCommutativeMagma_214 Source #

d_isCommutativeMonoid_332 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → T_IsCommutativeMonoid_764 Source #

d_isCommutativeSemigroup_334 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_334 ∷ T_IsAbelianGroup_1172 → T_IsCommutativeSemigroup_568 Source #

d_isEquivalence_336 ∷ T_IsAbelianGroup_1172 → T_IsEquivalence_28 Source #

d_isGroup_338 ∷ T_IsAbelianGroup_1172 → T_IsGroup_1074 Source #

d_isInvertibleMagma_340 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → T_IsInvertibleMagma_958 Source #

du_isInvertibleMagma_340 ∷ T_IsAbelianGroup_1172 → T_IsInvertibleMagma_958 Source #

d_isInvertibleUnitalMagma_342 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → T_IsInvertibleUnitalMagma_1012 Source #

du_isInvertibleUnitalMagma_342 ∷ T_IsAbelianGroup_1172 → T_IsInvertibleUnitalMagma_1012 Source #

d_isMagma_344 ∷ T_IsAbelianGroup_1172 → T_IsMagma_178 Source #

d_isMonoid_346 ∷ T_IsAbelianGroup_1172 → T_IsMonoid_712 Source #

d_isPartialEquivalence_348 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_348 ∷ T_IsAbelianGroup_1172 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_350 ∷ T_IsAbelianGroup_1172 → T_IsSemigroup_488 Source #

d_isUnitalMagma_352 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_352 ∷ T_IsAbelianGroup_1172 → T_IsUnitalMagma_666 Source #

d_refl_354 ∷ T_IsAbelianGroup_1172 → Integer → T__'8801'__12 Source #

d_reflexive_356 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_358 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → T_Setoid_46 Source #

du_setoid_358 ∷ T_IsAbelianGroup_1172 → T_Setoid_46 Source #

d_sym_360 ∷ T_IsAbelianGroup_1172 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_362 ∷ T_IsAbelianGroup_1172 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_unique'691''45''8315''185'_364 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_unique'737''45''8315''185'_366 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8315''185''45'cong_368 ∷ T_IsAbelianGroup_1172 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_370 ∷ T_IsAbelianGroup_1172 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_372 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_374 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsAbelianGroup_1172 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_alter_378 ∷ T_IsAlternativeMagma_290 → T_Σ_14 Source #

d_alternative'691'_380 ∷ (Integer → Integer → Integer) → T_IsAlternativeMagma_290 → Integer → Integer → T__'8801'__12 Source #

d_alternative'737'_382 ∷ (Integer → Integer → Integer) → T_IsAlternativeMagma_290 → Integer → Integer → T__'8801'__12 Source #

d_isEquivalence_384 ∷ T_IsAlternativeMagma_290 → T_IsEquivalence_28 Source #

d_isMagma_386 ∷ T_IsAlternativeMagma_290 → T_IsMagma_178 Source #

d_isPartialEquivalence_388 ∷ (Integer → Integer → Integer) → T_IsAlternativeMagma_290 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_388 ∷ T_IsAlternativeMagma_290 → T_IsPartialEquivalence_16 Source #

d_refl_390 ∷ T_IsAlternativeMagma_290 → Integer → T__'8801'__12 Source #

d_reflexive_392 ∷ (Integer → Integer → Integer) → T_IsAlternativeMagma_290 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_394 ∷ (Integer → Integer → Integer) → T_IsAlternativeMagma_290 → T_Setoid_46 Source #

du_setoid_394 ∷ T_IsAlternativeMagma_290 → T_Setoid_46 Source #

d_sym_396 ∷ T_IsAlternativeMagma_290 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_398 ∷ T_IsAlternativeMagma_290 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_400 ∷ T_IsAlternativeMagma_290 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_402 ∷ (Integer → Integer → Integer) → T_IsAlternativeMagma_290 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_404 ∷ (Integer → Integer → Integer) → T_IsAlternativeMagma_290 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_408 ∷ T_IsBand_526 → Integer → Integer → Integer → T__'8801'__12 Source #

d_idem_410 ∷ T_IsBand_526 → Integer → T__'8801'__12 Source #

d_isEquivalence_412 ∷ T_IsBand_526 → T_IsEquivalence_28 Source #

d_isMagma_414 ∷ T_IsBand_526 → T_IsMagma_178 Source #

d_isPartialEquivalence_416 ∷ (Integer → Integer → Integer) → T_IsBand_526 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_416 ∷ T_IsBand_526 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_418 ∷ T_IsBand_526 → T_IsSemigroup_488 Source #

d_refl_420 ∷ T_IsBand_526 → Integer → T__'8801'__12 Source #

d_reflexive_422 ∷ (Integer → Integer → Integer) → T_IsBand_526 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_424 ∷ (Integer → Integer → Integer) → T_IsBand_526 → T_Setoid_46 Source #

du_setoid_424 ∷ T_IsBand_526 → T_Setoid_46 Source #

d_sym_426 ∷ T_IsBand_526 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_428 ∷ T_IsBand_526 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_430 ∷ T_IsBand_526 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_432 ∷ (Integer → Integer → Integer) → T_IsBand_526 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_434 ∷ (Integer → Integer → Integer) → T_IsBand_526 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'42''45'assoc_438 ∷ T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'cancel'691''45'nonZero_440 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → Integer → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 → T__'8801'__12 Source #

d_'42''45'cancel'737''45'nonZero_442 ∷ T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → Integer → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 → T__'8801'__12 Source #

d_'42''45'comm_444 ∷ T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → T__'8801'__12 Source #

d_'42''45'cong_446 ∷ T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_448 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_450 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'42''45'identity_452 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_Σ_14 Source #

d_identity'691'_454 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → Integer → T__'8801'__12 Source #

d_identity'737'_456 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → Integer → T__'8801'__12 Source #

d_isCommutativeMagma_458 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_458 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeMagma_214 Source #

d_'42''45'isCommutativeMonoid_460 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeMonoid_764 Source #

du_'42''45'isCommutativeMonoid_460 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeMonoid_764 Source #

d_'42''45'isCommutativeSemigroup_462 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeSemigroup_568 Source #

du_'42''45'isCommutativeSemigroup_462 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeSemigroup_568 Source #

d_'42''45'isMagma_464 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → T_IsMagma_178 Source #

du_'42''45'isMagma_464 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsMagma_178 Source #

d_'42''45'isMonoid_466 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → T_IsMonoid_712 Source #

du_'42''45'isMonoid_466 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsMonoid_712 Source #

d_'42''45'isSemigroup_468 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → T_IsSemigroup_488 Source #

du_'42''45'isSemigroup_468 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsSemigroup_488 Source #

d_assoc_470 ∷ T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_472 ∷ T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_474 ∷ T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_476 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_478 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_identity_480 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_Σ_14 Source #

d_identity'691'_482 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → Integer → T__'8801'__12 Source #

d_identity'737'_484 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → Integer → T__'8801'__12 Source #

d_isCommutativeMagma_486 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_486 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeMagma_214 Source #

d_'43''45'isCommutativeMonoid_488 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeMonoid_764 Source #

d_isCommutativeSemigroup_490 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_490 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeSemigroup_568 Source #

d_isMagma_492 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsMagma_178 Source #

d_isMonoid_494 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsMonoid_712 Source #

d_isSemigroup_496 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsSemigroup_488 Source #

d_isUnitalMagma_498 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_498 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsUnitalMagma_666 Source #

d_distrib_500 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_Σ_14 Source #

d_distrib'691'_502 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → Integer → T__'8801'__12 Source #

d_distrib'737'_504 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → Integer → T__'8801'__12 Source #

d_isCommutativeSemiring_506 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeSemiring_1750 Source #

d_isCommutativeSemiringWithoutOne_508 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeSemiringWithoutOne_1438 Source #

du_isCommutativeSemiringWithoutOne_508 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeSemiringWithoutOne_1438 Source #

d_isEquivalence_510 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsEquivalence_28 Source #

d_isNearSemiring_512 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → T_IsNearSemiring_1260 Source #

du_isNearSemiring_512 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsNearSemiring_1260 Source #

d_isPartialEquivalence_514 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_514 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsPartialEquivalence_16 Source #

d_isSemiring_516 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsSemiring_1640 Source #

d_isSemiringWithoutAnnihilatingZero_518 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsSemiringWithoutAnnihilatingZero_1536 Source #

d_isSemiringWithoutOne_520 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → T_IsSemiringWithoutOne_1342 Source #

du_isSemiringWithoutOne_520 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsSemiringWithoutOne_1342 Source #

d_refl_522 ∷ T_IsCancellativeCommutativeSemiring_1872 → Integer → T__'8801'__12 Source #

d_reflexive_524 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_526 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → T_Setoid_46 Source #

du_setoid_526 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_Setoid_46 Source #

d_sym_528 ∷ T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_530 ∷ T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_zero_532 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_Σ_14 Source #

d_zero'691'_534 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → Integer → T__'8801'__12 Source #

d_zero'737'_536 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → Integer → T__'8801'__12 Source #

d_assoc_540 ∷ T_IsCommutativeBand_612 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_542 ∷ T_IsCommutativeBand_612 → Integer → Integer → T__'8801'__12 Source #

d_idem_544 ∷ T_IsCommutativeBand_612 → Integer → T__'8801'__12 Source #

d_isBand_546 ∷ T_IsCommutativeBand_612 → T_IsBand_526 Source #

d_isCommutativeMagma_548 ∷ (Integer → Integer → Integer) → T_IsCommutativeBand_612 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_548 ∷ T_IsCommutativeBand_612 → T_IsCommutativeMagma_214 Source #

d_isCommutativeSemigroup_550 ∷ (Integer → Integer → Integer) → T_IsCommutativeBand_612 → T_IsCommutativeSemigroup_568 Source #

d_isEquivalence_552 ∷ T_IsCommutativeBand_612 → T_IsEquivalence_28 Source #

d_isMagma_554 ∷ T_IsCommutativeBand_612 → T_IsMagma_178 Source #

d_isPartialEquivalence_556 ∷ (Integer → Integer → Integer) → T_IsCommutativeBand_612 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_556 ∷ T_IsCommutativeBand_612 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_558 ∷ T_IsCommutativeBand_612 → T_IsSemigroup_488 Source #

d_refl_560 ∷ T_IsCommutativeBand_612 → Integer → T__'8801'__12 Source #

d_reflexive_562 ∷ (Integer → Integer → Integer) → T_IsCommutativeBand_612 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_564 ∷ (Integer → Integer → Integer) → T_IsCommutativeBand_612 → T_Setoid_46 Source #

du_setoid_564 ∷ T_IsCommutativeBand_612 → T_Setoid_46 Source #

d_sym_566 ∷ T_IsCommutativeBand_612 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_568 ∷ T_IsCommutativeBand_612 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_570 ∷ T_IsCommutativeBand_612 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_572 ∷ (Integer → Integer → Integer) → T_IsCommutativeBand_612 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_574 ∷ (Integer → Integer → Integer) → T_IsCommutativeBand_612 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_comm_578 ∷ T_IsCommutativeMagma_214 → Integer → Integer → T__'8801'__12 Source #

d_isEquivalence_580 ∷ T_IsCommutativeMagma_214 → T_IsEquivalence_28 Source #

d_isMagma_582 ∷ T_IsCommutativeMagma_214 → T_IsMagma_178 Source #

d_isPartialEquivalence_584 ∷ (Integer → Integer → Integer) → T_IsCommutativeMagma_214 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_584 ∷ T_IsCommutativeMagma_214 → T_IsPartialEquivalence_16 Source #

d_refl_586 ∷ T_IsCommutativeMagma_214 → Integer → T__'8801'__12 Source #

d_reflexive_588 ∷ (Integer → Integer → Integer) → T_IsCommutativeMagma_214 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_590 ∷ (Integer → Integer → Integer) → T_IsCommutativeMagma_214 → T_Setoid_46 Source #

du_setoid_590 ∷ T_IsCommutativeMagma_214 → T_Setoid_46 Source #

d_sym_592 ∷ T_IsCommutativeMagma_214 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_594 ∷ T_IsCommutativeMagma_214 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_596 ∷ T_IsCommutativeMagma_214 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_598 ∷ (Integer → Integer → Integer) → T_IsCommutativeMagma_214 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_600 ∷ (Integer → Integer → Integer) → T_IsCommutativeMagma_214 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_604 ∷ T_IsCommutativeMonoid_764 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_606 ∷ T_IsCommutativeMonoid_764 → Integer → Integer → T__'8801'__12 Source #

d_identity_608 ∷ T_IsCommutativeMonoid_764 → T_Σ_14 Source #

d_identity'691'_610 ∷ (Integer → Integer → Integer) → Integer → T_IsCommutativeMonoid_764 → Integer → T__'8801'__12 Source #

d_identity'737'_612 ∷ (Integer → Integer → Integer) → Integer → T_IsCommutativeMonoid_764 → Integer → T__'8801'__12 Source #

d_isCommutativeMagma_614 ∷ (Integer → Integer → Integer) → Integer → T_IsCommutativeMonoid_764 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_614 ∷ T_IsCommutativeMonoid_764 → T_IsCommutativeMagma_214 Source #

d_isCommutativeSemigroup_616 ∷ (Integer → Integer → Integer) → Integer → T_IsCommutativeMonoid_764 → T_IsCommutativeSemigroup_568 Source #

d_isEquivalence_618 ∷ T_IsCommutativeMonoid_764 → T_IsEquivalence_28 Source #

d_isMagma_620 ∷ T_IsCommutativeMonoid_764 → T_IsMagma_178 Source #

d_isMonoid_622 ∷ T_IsCommutativeMonoid_764 → T_IsMonoid_712 Source #

d_isPartialEquivalence_624 ∷ (Integer → Integer → Integer) → Integer → T_IsCommutativeMonoid_764 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_624 ∷ T_IsCommutativeMonoid_764 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_626 ∷ T_IsCommutativeMonoid_764 → T_IsSemigroup_488 Source #

d_isUnitalMagma_628 ∷ (Integer → Integer → Integer) → Integer → T_IsCommutativeMonoid_764 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_628 ∷ T_IsCommutativeMonoid_764 → T_IsUnitalMagma_666 Source #

d_refl_630 ∷ T_IsCommutativeMonoid_764 → Integer → T__'8801'__12 Source #

d_reflexive_632 ∷ (Integer → Integer → Integer) → Integer → T_IsCommutativeMonoid_764 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_634 ∷ (Integer → Integer → Integer) → Integer → T_IsCommutativeMonoid_764 → T_Setoid_46 Source #

du_setoid_634 ∷ T_IsCommutativeMonoid_764 → T_Setoid_46 Source #

d_sym_636 ∷ T_IsCommutativeMonoid_764 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_638 ∷ T_IsCommutativeMonoid_764 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_640 ∷ T_IsCommutativeMonoid_764 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_642 ∷ (Integer → Integer → Integer) → Integer → T_IsCommutativeMonoid_764 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_644 ∷ (Integer → Integer → Integer) → Integer → T_IsCommutativeMonoid_764 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d__'47''47'__648 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → Integer Source #

du__'47''47'__648 ∷ (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → Integer Source #

d_'42''45'assoc_650 ∷ T_IsCommutativeRing_2888 → Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'comm_652 ∷ T_IsCommutativeRing_2888 → Integer → Integer → T__'8801'__12 Source #

d_'42''45'cong_654 ∷ T_IsCommutativeRing_2888 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_656 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_658 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'42''45'identity_660 ∷ T_IsCommutativeRing_2888 → T_Σ_14 Source #

d_identity'691'_662 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → T__'8801'__12 Source #

d_identity'737'_664 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → T__'8801'__12 Source #

d_isCommutativeMagma_666 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_666 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → T_IsCommutativeRing_2888 → T_IsCommutativeMagma_214 Source #

d_'42''45'isCommutativeMonoid_668 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsCommutativeMonoid_764 Source #

du_'42''45'isCommutativeMonoid_668 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → T_IsCommutativeRing_2888 → T_IsCommutativeMonoid_764 Source #

d_'42''45'isCommutativeSemigroup_670 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsCommutativeSemigroup_568 Source #

du_'42''45'isCommutativeSemigroup_670 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → T_IsCommutativeRing_2888 → T_IsCommutativeSemigroup_568 Source #

d_'42''45'isMagma_672 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsMagma_178 Source #

du_'42''45'isMagma_672 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → T_IsCommutativeRing_2888 → T_IsMagma_178 Source #

d_'42''45'isMonoid_674 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsMonoid_712 Source #

du_'42''45'isMonoid_674 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → T_IsCommutativeRing_2888 → T_IsMonoid_712 Source #

d_'42''45'isSemigroup_676 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsSemigroup_488 Source #

du_'42''45'isSemigroup_676 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → T_IsCommutativeRing_2888 → T_IsSemigroup_488 Source #

d_assoc_678 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_680 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_682 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_684 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_686 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_identity_688 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_Σ_14 Source #

du_identity_688 ∷ T_IsCommutativeRing_2888 → T_Σ_14 Source #

d_identity'691'_690 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → T__'8801'__12 Source #

d_identity'737'_692 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → T__'8801'__12 Source #

d_'43''45'isAbelianGroup_694 ∷ T_IsCommutativeRing_2888 → T_IsAbelianGroup_1172 Source #

d_isCommutativeMagma_696 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_696 ∷ T_IsCommutativeRing_2888 → T_IsCommutativeMagma_214 Source #

d_isCommutativeMonoid_698 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsCommutativeMonoid_764 Source #

du_isCommutativeMonoid_698 ∷ T_IsCommutativeRing_2888 → T_IsCommutativeMonoid_764 Source #

d_isCommutativeSemigroup_700 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_700 ∷ T_IsCommutativeRing_2888 → T_IsCommutativeSemigroup_568 Source #

d_isGroup_702 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsGroup_1074 Source #

du_isGroup_702 ∷ T_IsCommutativeRing_2888 → T_IsGroup_1074 Source #

d_isInvertibleMagma_704 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsInvertibleMagma_958 Source #

du_isInvertibleMagma_704 ∷ T_IsCommutativeRing_2888 → T_IsInvertibleMagma_958 Source #

d_isInvertibleUnitalMagma_706 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsInvertibleUnitalMagma_1012 Source #

du_isInvertibleUnitalMagma_706 ∷ T_IsCommutativeRing_2888 → T_IsInvertibleUnitalMagma_1012 Source #

d_isMagma_708 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsMagma_178 Source #

du_isMagma_708 ∷ T_IsCommutativeRing_2888 → T_IsMagma_178 Source #

d_isMonoid_710 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsMonoid_712 Source #

du_isMonoid_710 ∷ T_IsCommutativeRing_2888 → T_IsMonoid_712 Source #

d_isSemigroup_712 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsSemigroup_488 Source #

du_isSemigroup_712 ∷ T_IsCommutativeRing_2888 → T_IsSemigroup_488 Source #

d_isUnitalMagma_714 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_714 ∷ T_IsCommutativeRing_2888 → T_IsUnitalMagma_666 Source #

d_'8315''185''45'cong_716 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_inverse_718 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_Σ_14 Source #

du_inverse_718 ∷ T_IsCommutativeRing_2888 → T_Σ_14 Source #

d_inverse'691'_720 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → T__'8801'__12 Source #

d_inverse'737'_722 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → T__'8801'__12 Source #

d_distrib_724 ∷ T_IsCommutativeRing_2888 → T_Σ_14 Source #

d_distrib'691'_726 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → Integer → T__'8801'__12 Source #

d_distrib'737'_728 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → Integer → T__'8801'__12 Source #

d_isCommutativeSemiring_730 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsCommutativeSemiring_1750 Source #

d_isCommutativeSemiringWithoutOne_732 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsCommutativeSemiringWithoutOne_1438 Source #

du_isCommutativeSemiringWithoutOne_732 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → T_IsCommutativeRing_2888 → T_IsCommutativeSemiringWithoutOne_1438 Source #

d_isEquivalence_734 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsEquivalence_28 Source #

du_isEquivalence_734 ∷ T_IsCommutativeRing_2888 → T_IsEquivalence_28 Source #

d_isNearSemiring_736 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsNearSemiring_1260 Source #

du_isNearSemiring_736 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → T_IsCommutativeRing_2888 → T_IsNearSemiring_1260 Source #

d_isPartialEquivalence_738 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_738 ∷ T_IsCommutativeRing_2888 → T_IsPartialEquivalence_16 Source #

d_isRing_740 ∷ T_IsCommutativeRing_2888 → T_IsRing_2740 Source #

d_isRingWithoutOne_742 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsRingWithoutOne_2368 Source #

du_isRingWithoutOne_742 ∷ T_IsCommutativeRing_2888 → T_IsRingWithoutOne_2368 Source #

d_isSemiring_744 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsSemiring_1640 Source #

du_isSemiring_744 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → T_IsCommutativeRing_2888 → T_IsSemiring_1640 Source #

d_isSemiringWithoutAnnihilatingZero_746 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsSemiringWithoutAnnihilatingZero_1536 Source #

du_isSemiringWithoutAnnihilatingZero_746 ∷ T_IsCommutativeRing_2888 → T_IsSemiringWithoutAnnihilatingZero_1536 Source #

d_isSemiringWithoutOne_748 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_IsSemiringWithoutOne_1342 Source #

du_isSemiringWithoutOne_748 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → T_IsCommutativeRing_2888 → T_IsSemiringWithoutOne_1342 Source #

d_refl_750 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → T__'8801'__12 Source #

d_reflexive_752 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_754 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_Setoid_46 Source #

du_setoid_754 ∷ T_IsCommutativeRing_2888 → T_Setoid_46 Source #

d_sym_756 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_758 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_unique'691''45''8315''185'_760 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_unique'737''45''8315''185'_762 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_zero_764 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_Σ_14 Source #

du_zero_764 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → T_IsCommutativeRing_2888 → T_Σ_14 Source #

d_zero'691'_766 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → T__'8801'__12 Source #

d_zero'737'_768 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → T__'8801'__12 Source #

d_assoc_772 ∷ T_IsCommutativeSemigroup_568 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_774 ∷ T_IsCommutativeSemigroup_568 → Integer → Integer → T__'8801'__12 Source #

d_isCommutativeMagma_776 ∷ (Integer → Integer → Integer) → T_IsCommutativeSemigroup_568 → T_IsCommutativeMagma_214 Source #

d_isEquivalence_778 ∷ T_IsCommutativeSemigroup_568 → T_IsEquivalence_28 Source #

d_isMagma_780 ∷ T_IsCommutativeSemigroup_568 → T_IsMagma_178 Source #

d_isPartialEquivalence_782 ∷ (Integer → Integer → Integer) → T_IsCommutativeSemigroup_568 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_782 ∷ T_IsCommutativeSemigroup_568 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_784 ∷ T_IsCommutativeSemigroup_568 → T_IsSemigroup_488 Source #

d_refl_786 ∷ T_IsCommutativeSemigroup_568 → Integer → T__'8801'__12 Source #

d_reflexive_788 ∷ (Integer → Integer → Integer) → T_IsCommutativeSemigroup_568 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_790 ∷ (Integer → Integer → Integer) → T_IsCommutativeSemigroup_568 → T_Setoid_46 Source #

du_setoid_790 ∷ T_IsCommutativeSemigroup_568 → T_Setoid_46 Source #

d_sym_792 ∷ T_IsCommutativeSemigroup_568 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_794 ∷ T_IsCommutativeSemigroup_568 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_796 ∷ T_IsCommutativeSemigroup_568 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_798 ∷ (Integer → Integer → Integer) → T_IsCommutativeSemigroup_568 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_800 ∷ (Integer → Integer → Integer) → T_IsCommutativeSemigroup_568 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'42''45'assoc_804 ∷ T_IsCommutativeSemiring_1750 → Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'comm_806 ∷ T_IsCommutativeSemiring_1750 → Integer → Integer → T__'8801'__12 Source #

d_'42''45'cong_808 ∷ T_IsCommutativeSemiring_1750 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_810 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_812 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'42''45'identity_814 ∷ T_IsCommutativeSemiring_1750 → T_Σ_14 Source #

d_identity'691'_816 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → Integer → T__'8801'__12 Source #

d_identity'737'_818 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → Integer → T__'8801'__12 Source #

d_isCommutativeMagma_820 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_820 ∷ T_IsCommutativeSemiring_1750 → T_IsCommutativeMagma_214 Source #

d_'42''45'isCommutativeMonoid_822 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → T_IsCommutativeMonoid_764 Source #

d_'42''45'isCommutativeSemigroup_824 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → T_IsCommutativeSemigroup_568 Source #

du_'42''45'isCommutativeSemigroup_824 ∷ T_IsCommutativeSemiring_1750 → T_IsCommutativeSemigroup_568 Source #

d_'42''45'isMagma_826 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → T_IsMagma_178 Source #

du_'42''45'isMagma_826 ∷ T_IsCommutativeSemiring_1750 → T_IsMagma_178 Source #

d_'42''45'isMonoid_828 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → T_IsMonoid_712 Source #

du_'42''45'isMonoid_828 ∷ T_IsCommutativeSemiring_1750 → T_IsMonoid_712 Source #

d_'42''45'isSemigroup_830 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → T_IsSemigroup_488 Source #

du_'42''45'isSemigroup_830 ∷ T_IsCommutativeSemiring_1750 → T_IsSemigroup_488 Source #

d_assoc_832 ∷ T_IsCommutativeSemiring_1750 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_834 ∷ T_IsCommutativeSemiring_1750 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_836 ∷ T_IsCommutativeSemiring_1750 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_838 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_840 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_identity_842 ∷ T_IsCommutativeSemiring_1750 → T_Σ_14 Source #

d_identity'691'_844 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → Integer → T__'8801'__12 Source #

d_identity'737'_846 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → Integer → T__'8801'__12 Source #

d_isCommutativeMagma_848 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_848 ∷ T_IsCommutativeSemiring_1750 → T_IsCommutativeMagma_214 Source #

d_'43''45'isCommutativeMonoid_850 ∷ T_IsCommutativeSemiring_1750 → T_IsCommutativeMonoid_764 Source #

d_isCommutativeSemigroup_852 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_852 ∷ T_IsCommutativeSemiring_1750 → T_IsCommutativeSemigroup_568 Source #

d_isMagma_854 ∷ T_IsCommutativeSemiring_1750 → T_IsMagma_178 Source #

d_isMonoid_856 ∷ T_IsCommutativeSemiring_1750 → T_IsMonoid_712 Source #

d_isSemigroup_858 ∷ T_IsCommutativeSemiring_1750 → T_IsSemigroup_488 Source #

d_isUnitalMagma_860 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_860 ∷ T_IsCommutativeSemiring_1750 → T_IsUnitalMagma_666 Source #

d_distrib_862 ∷ T_IsCommutativeSemiring_1750 → T_Σ_14 Source #

d_distrib'691'_864 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → Integer → Integer → Integer → T__'8801'__12 Source #

d_distrib'737'_866 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → Integer → Integer → Integer → T__'8801'__12 Source #

d_isCommutativeSemiringWithoutOne_868 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → T_IsCommutativeSemiringWithoutOne_1438 Source #

d_isEquivalence_870 ∷ T_IsCommutativeSemiring_1750 → T_IsEquivalence_28 Source #

d_isNearSemiring_872 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → T_IsNearSemiring_1260 Source #

du_isNearSemiring_872 ∷ T_IsCommutativeSemiring_1750 → T_IsNearSemiring_1260 Source #

d_isPartialEquivalence_874 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_874 ∷ T_IsCommutativeSemiring_1750 → T_IsPartialEquivalence_16 Source #

d_isSemiring_876 ∷ T_IsCommutativeSemiring_1750 → T_IsSemiring_1640 Source #

d_isSemiringWithoutAnnihilatingZero_878 ∷ T_IsCommutativeSemiring_1750 → T_IsSemiringWithoutAnnihilatingZero_1536 Source #

d_isSemiringWithoutOne_880 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → T_IsSemiringWithoutOne_1342 Source #

du_isSemiringWithoutOne_880 ∷ T_IsCommutativeSemiring_1750 → T_IsSemiringWithoutOne_1342 Source #

d_refl_882 ∷ T_IsCommutativeSemiring_1750 → Integer → T__'8801'__12 Source #

d_reflexive_884 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_886 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → T_Setoid_46 Source #

du_setoid_886 ∷ T_IsCommutativeSemiring_1750 → T_Setoid_46 Source #

d_sym_888 ∷ T_IsCommutativeSemiring_1750 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_890 ∷ T_IsCommutativeSemiring_1750 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_zero_892 ∷ T_IsCommutativeSemiring_1750 → T_Σ_14 Source #

d_zero'691'_894 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → Integer → T__'8801'__12 Source #

d_zero'737'_896 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → Integer → T__'8801'__12 Source #

d_'42''45'assoc_900 ∷ T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'comm_902 ∷ T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → T__'8801'__12 Source #

d_'42''45'cong_904 ∷ T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_906 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_908 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_isCommutativeMagma_910 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_910 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsCommutativeMagma_214 Source #

d_'42''45'isCommutativeSemigroup_912 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → T_IsCommutativeSemigroup_568 Source #

d_'42''45'isMagma_914 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → T_IsMagma_178 Source #

du_'42''45'isMagma_914 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsMagma_178 Source #

d_'42''45'isSemigroup_916 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → T_IsSemigroup_488 Source #

du_'42''45'isSemigroup_916 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsSemigroup_488 Source #

d_assoc_918 ∷ T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_920 ∷ T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_922 ∷ T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_924 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_926 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_identity_928 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_Σ_14 Source #

d_identity'691'_930 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → Integer → T__'8801'__12 Source #

d_identity'737'_932 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → Integer → T__'8801'__12 Source #

d_isCommutativeMagma_934 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_934 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsCommutativeMagma_214 Source #

d_'43''45'isCommutativeMonoid_936 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsCommutativeMonoid_764 Source #

d_isCommutativeSemigroup_938 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_938 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsCommutativeSemigroup_568 Source #

d_isMonoid_940 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsMonoid_712 Source #

d_distrib_942 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_Σ_14 Source #

d_distrib'691'_944 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → Integer → T__'8801'__12 Source #

d_distrib'737'_946 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → Integer → T__'8801'__12 Source #

d_isEquivalence_948 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsEquivalence_28 Source #

d_isNearSemiring_950 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → T_IsNearSemiring_1260 Source #

du_isNearSemiring_950 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsNearSemiring_1260 Source #

d_isPartialEquivalence_952 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_952 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsPartialEquivalence_16 Source #

d_isSemiringWithoutOne_954 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsSemiringWithoutOne_1342 Source #

d_refl_956 ∷ T_IsCommutativeSemiringWithoutOne_1438 → Integer → T__'8801'__12 Source #

d_reflexive_958 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_960 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → T_Setoid_46 Source #

du_setoid_960 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_Setoid_46 Source #

d_sym_962 ∷ T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_964 ∷ T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_zero_966 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_Σ_14 Source #

d_zero'691'_968 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → Integer → T__'8801'__12 Source #

d_zero'737'_970 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → Integer → T__'8801'__12 Source #

d_flex_974 ∷ T_IsFlexibleMagma_332 → Integer → Integer → T__'8801'__12 Source #

d_isEquivalence_976 ∷ T_IsFlexibleMagma_332 → T_IsEquivalence_28 Source #

d_isMagma_978 ∷ T_IsFlexibleMagma_332 → T_IsMagma_178 Source #

d_isPartialEquivalence_980 ∷ (Integer → Integer → Integer) → T_IsFlexibleMagma_332 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_980 ∷ T_IsFlexibleMagma_332 → T_IsPartialEquivalence_16 Source #

d_refl_982 ∷ T_IsFlexibleMagma_332 → Integer → T__'8801'__12 Source #

d_reflexive_984 ∷ (Integer → Integer → Integer) → T_IsFlexibleMagma_332 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_986 ∷ (Integer → Integer → Integer) → T_IsFlexibleMagma_332 → T_Setoid_46 Source #

du_setoid_986 ∷ T_IsFlexibleMagma_332 → T_Setoid_46 Source #

d_sym_988 ∷ T_IsFlexibleMagma_332 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_990 ∷ T_IsFlexibleMagma_332 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_992 ∷ T_IsFlexibleMagma_332 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_994 ∷ (Integer → Integer → Integer) → T_IsFlexibleMagma_332 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_996 ∷ (Integer → Integer → Integer) → T_IsFlexibleMagma_332 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d__'45'__1000 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → Integer → Integer → Integer Source #

d__'47''47'__1002 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → Integer → Integer → Integer Source #

d__'92''92'__1004 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → Integer → Integer → Integer Source #

d_assoc_1006 ∷ T_IsGroup_1074 → Integer → Integer → Integer → T__'8801'__12 Source #

d_identity_1008 ∷ T_IsGroup_1074 → T_Σ_14 Source #

d_identity'691'_1010 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → Integer → T__'8801'__12 Source #

d_identity'737'_1012 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → Integer → T__'8801'__12 Source #

d_inverse_1014 ∷ T_IsGroup_1074 → T_Σ_14 Source #

d_inverse'691'_1016 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → Integer → T__'8801'__12 Source #

d_inverse'737'_1018 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → Integer → T__'8801'__12 Source #

d_isEquivalence_1020 ∷ T_IsGroup_1074 → T_IsEquivalence_28 Source #

d_isInvertibleMagma_1022 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → T_IsInvertibleMagma_958 Source #

d_isInvertibleUnitalMagma_1024 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → T_IsInvertibleUnitalMagma_1012 Source #

d_isMagma_1026 ∷ T_IsGroup_1074 → T_IsMagma_178 Source #

d_isMonoid_1028 ∷ T_IsGroup_1074 → T_IsMonoid_712 Source #

d_isPartialEquivalence_1030 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1030 ∷ T_IsGroup_1074 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1032 ∷ T_IsGroup_1074 → T_IsSemigroup_488 Source #

d_isUnitalMagma_1034 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_1034 ∷ T_IsGroup_1074 → T_IsUnitalMagma_666 Source #

d_refl_1036 ∷ T_IsGroup_1074 → Integer → T__'8801'__12 Source #

d_reflexive_1038 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_1040 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → T_Setoid_46 Source #

du_setoid_1040 ∷ T_IsGroup_1074 → T_Setoid_46 Source #

d_sym_1042 ∷ T_IsGroup_1074 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_1044 ∷ T_IsGroup_1074 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_unique'691''45''8315''185'_1046 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_unique'737''45''8315''185'_1048 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8315''185''45'cong_1050 ∷ T_IsGroup_1074 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_1052 ∷ T_IsGroup_1074 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_1054 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_1056 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsGroup_1074 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_1060 ∷ T_IsIdempotentCommutativeMonoid_884 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_1062 ∷ T_IsIdempotentCommutativeMonoid_884 → Integer → Integer → T__'8801'__12 Source #

d_idem_1064 ∷ T_IsIdempotentCommutativeMonoid_884 → Integer → T__'8801'__12 Source #

d_identity_1066 ∷ T_IsIdempotentCommutativeMonoid_884 → T_Σ_14 Source #

d_identity'691'_1068 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentCommutativeMonoid_884 → Integer → T__'8801'__12 Source #

d_identity'737'_1070 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentCommutativeMonoid_884 → Integer → T__'8801'__12 Source #

d_isBand_1072 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentCommutativeMonoid_884 → T_IsBand_526 Source #

du_isBand_1072 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsBand_526 Source #

d_isCommutativeBand_1074 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeBand_612 Source #

d_isCommutativeMagma_1076 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_1076 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeMagma_214 Source #

d_isCommutativeMonoid_1078 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeMonoid_764 Source #

d_isCommutativeSemigroup_1080 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_1080 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeSemigroup_568 Source #

d_isEquivalence_1082 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsEquivalence_28 Source #

d_isIdempotentMonoid_1084 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentCommutativeMonoid_884 → T_IsIdempotentMonoid_826 Source #

d_isMagma_1086 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsMagma_178 Source #

d_isMonoid_1088 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsMonoid_712 Source #

d_isPartialEquivalence_1090 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentCommutativeMonoid_884 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1090 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1092 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsSemigroup_488 Source #

d_isUnitalMagma_1094 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentCommutativeMonoid_884 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_1094 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsUnitalMagma_666 Source #

d_refl_1096 ∷ T_IsIdempotentCommutativeMonoid_884 → Integer → T__'8801'__12 Source #

d_reflexive_1098 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentCommutativeMonoid_884 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_1100 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentCommutativeMonoid_884 → T_Setoid_46 Source #

du_setoid_1100 ∷ T_IsIdempotentCommutativeMonoid_884 → T_Setoid_46 Source #

d_sym_1102 ∷ T_IsIdempotentCommutativeMonoid_884 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_1104 ∷ T_IsIdempotentCommutativeMonoid_884 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_1106 ∷ T_IsIdempotentCommutativeMonoid_884 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_1108 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentCommutativeMonoid_884 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_1110 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentCommutativeMonoid_884 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_idem_1114 ∷ T_IsIdempotentMagma_252 → Integer → T__'8801'__12 Source #

d_isEquivalence_1116 ∷ T_IsIdempotentMagma_252 → T_IsEquivalence_28 Source #

d_isMagma_1118 ∷ T_IsIdempotentMagma_252 → T_IsMagma_178 Source #

d_isPartialEquivalence_1120 ∷ (Integer → Integer → Integer) → T_IsIdempotentMagma_252 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1120 ∷ T_IsIdempotentMagma_252 → T_IsPartialEquivalence_16 Source #

d_refl_1122 ∷ T_IsIdempotentMagma_252 → Integer → T__'8801'__12 Source #

d_reflexive_1124 ∷ (Integer → Integer → Integer) → T_IsIdempotentMagma_252 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_1126 ∷ (Integer → Integer → Integer) → T_IsIdempotentMagma_252 → T_Setoid_46 Source #

du_setoid_1126 ∷ T_IsIdempotentMagma_252 → T_Setoid_46 Source #

d_sym_1128 ∷ T_IsIdempotentMagma_252 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_1130 ∷ T_IsIdempotentMagma_252 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_1132 ∷ T_IsIdempotentMagma_252 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_1134 ∷ (Integer → Integer → Integer) → T_IsIdempotentMagma_252 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_1136 ∷ (Integer → Integer → Integer) → T_IsIdempotentMagma_252 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_1140 ∷ T_IsIdempotentMonoid_826 → Integer → Integer → Integer → T__'8801'__12 Source #

d_idem_1142 ∷ T_IsIdempotentMonoid_826 → Integer → T__'8801'__12 Source #

d_identity_1144 ∷ T_IsIdempotentMonoid_826 → T_Σ_14 Source #

d_identity'691'_1146 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentMonoid_826 → Integer → T__'8801'__12 Source #

d_identity'737'_1148 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentMonoid_826 → Integer → T__'8801'__12 Source #

d_isBand_1150 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentMonoid_826 → T_IsBand_526 Source #

d_isEquivalence_1152 ∷ T_IsIdempotentMonoid_826 → T_IsEquivalence_28 Source #

d_isMagma_1154 ∷ T_IsIdempotentMonoid_826 → T_IsMagma_178 Source #

d_isMonoid_1156 ∷ T_IsIdempotentMonoid_826 → T_IsMonoid_712 Source #

d_isPartialEquivalence_1158 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentMonoid_826 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1158 ∷ T_IsIdempotentMonoid_826 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1160 ∷ T_IsIdempotentMonoid_826 → T_IsSemigroup_488 Source #

d_isUnitalMagma_1162 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentMonoid_826 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_1162 ∷ T_IsIdempotentMonoid_826 → T_IsUnitalMagma_666 Source #

d_refl_1164 ∷ T_IsIdempotentMonoid_826 → Integer → T__'8801'__12 Source #

d_reflexive_1166 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentMonoid_826 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_1168 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentMonoid_826 → T_Setoid_46 Source #

du_setoid_1168 ∷ T_IsIdempotentMonoid_826 → T_Setoid_46 Source #

d_sym_1170 ∷ T_IsIdempotentMonoid_826 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_1172 ∷ T_IsIdempotentMonoid_826 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_1174 ∷ T_IsIdempotentMonoid_826 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_1176 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentMonoid_826 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_1178 ∷ (Integer → Integer → Integer) → Integer → T_IsIdempotentMonoid_826 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'42''45'assoc_1182 ∷ T_IsIdempotentSemiring_1998 → Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'cong_1184 ∷ T_IsIdempotentSemiring_1998 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_1186 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_1188 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'42''45'identity_1190 ∷ T_IsIdempotentSemiring_1998 → T_Σ_14 Source #

d_identity'691'_1192 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → Integer → T__'8801'__12 Source #

d_identity'737'_1194 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → Integer → T__'8801'__12 Source #

d_'42''45'isMagma_1196 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → T_IsMagma_178 Source #

du_'42''45'isMagma_1196 ∷ T_IsIdempotentSemiring_1998 → T_IsMagma_178 Source #

d_'42''45'isMonoid_1198 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → T_IsMonoid_712 Source #

du_'42''45'isMonoid_1198 ∷ T_IsIdempotentSemiring_1998 → T_IsMonoid_712 Source #

d_'42''45'isSemigroup_1200 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → T_IsSemigroup_488 Source #

du_'42''45'isSemigroup_1200 ∷ T_IsIdempotentSemiring_1998 → T_IsSemigroup_488 Source #

d_assoc_1202 ∷ T_IsIdempotentSemiring_1998 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_1204 ∷ T_IsIdempotentSemiring_1998 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_1206 ∷ T_IsIdempotentSemiring_1998 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_1208 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_1210 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'43''45'idem_1212 ∷ T_IsIdempotentSemiring_1998 → Integer → T__'8801'__12 Source #

d_identity_1214 ∷ T_IsIdempotentSemiring_1998 → T_Σ_14 Source #

d_identity'691'_1216 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → Integer → T__'8801'__12 Source #

d_identity'737'_1218 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → Integer → T__'8801'__12 Source #

d_isBand_1220 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → T_IsBand_526 Source #

du_isBand_1220 ∷ T_IsIdempotentSemiring_1998 → T_IsBand_526 Source #

d_isCommutativeBand_1222 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → T_IsCommutativeBand_612 Source #

du_isCommutativeBand_1222 ∷ T_IsIdempotentSemiring_1998 → T_IsCommutativeBand_612 Source #

d_isCommutativeMagma_1224 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → T_IsCommutativeMagma_214 Source #

du_isCommutativeMagma_1224 ∷ T_IsIdempotentSemiring_1998 → T_IsCommutativeMagma_214 Source #

d_'43''45'isCommutativeMonoid_1226 ∷ T_IsIdempotentSemiring_1998 → T_IsCommutativeMonoid_764 Source #

d_isCommutativeSemigroup_1228 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → T_IsCommutativeSemigroup_568 Source #

du_isCommutativeSemigroup_1228 ∷ T_IsIdempotentSemiring_1998 → T_IsCommutativeSemigroup_568 Source #

d_'43''45'isIdempotentCommutativeMonoid_1230 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → T_IsIdempotentCommutativeMonoid_884 Source #

d_isIdempotentMonoid_1232 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → T_IsIdempotentMonoid_826 Source #

du_isIdempotentMonoid_1232 ∷ T_IsIdempotentSemiring_1998 → T_IsIdempotentMonoid_826 Source #

d_isMagma_1234 ∷ T_IsIdempotentSemiring_1998 → T_IsMagma_178 Source #

d_isMonoid_1236 ∷ T_IsIdempotentSemiring_1998 → T_IsMonoid_712 Source #

d_isSemigroup_1238 ∷ T_IsIdempotentSemiring_1998 → T_IsSemigroup_488 Source #

d_isUnitalMagma_1240 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → T_IsUnitalMagma_666 Source #

du_isUnitalMagma_1240 ∷ T_IsIdempotentSemiring_1998 → T_IsUnitalMagma_666 Source #

d_distrib_1242 ∷ T_IsIdempotentSemiring_1998 → T_Σ_14 Source #

d_distrib'691'_1244 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → Integer → Integer → Integer → T__'8801'__12 Source #

d_distrib'737'_1246 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → Integer → Integer → Integer → T__'8801'__12 Source #

d_isEquivalence_1248 ∷ T_IsIdempotentSemiring_1998 → T_IsEquivalence_28 Source #

d_isNearSemiring_1250 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → T_IsNearSemiring_1260 Source #

du_isNearSemiring_1250 ∷ T_IsIdempotentSemiring_1998 → T_IsNearSemiring_1260 Source #

d_isPartialEquivalence_1252 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1252 ∷ T_IsIdempotentSemiring_1998 → T_IsPartialEquivalence_16 Source #

d_isSemiring_1254 ∷ T_IsIdempotentSemiring_1998 → T_IsSemiring_1640 Source #

d_isSemiringWithoutAnnihilatingZero_1256 ∷ T_IsIdempotentSemiring_1998 → T_IsSemiringWithoutAnnihilatingZero_1536 Source #

d_isSemiringWithoutOne_1258 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → T_IsSemiringWithoutOne_1342 Source #

du_isSemiringWithoutOne_1258 ∷ T_IsIdempotentSemiring_1998 → T_IsSemiringWithoutOne_1342 Source #

d_refl_1260 ∷ T_IsIdempotentSemiring_1998 → Integer → T__'8801'__12 Source #

d_reflexive_1262 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_1264 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → T_Setoid_46 Source #

du_setoid_1264 ∷ T_IsIdempotentSemiring_1998 → T_Setoid_46 Source #

d_sym_1266 ∷ T_IsIdempotentSemiring_1998 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_1268 ∷ T_IsIdempotentSemiring_1998 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_zero_1270 ∷ T_IsIdempotentSemiring_1998 → T_Σ_14 Source #

d_zero'691'_1272 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → Integer → T__'8801'__12 Source #

d_zero'737'_1274 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsIdempotentSemiring_1998 → Integer → T__'8801'__12 Source #

d_inverse_1278 ∷ T_IsInvertibleMagma_958 → T_Σ_14 Source #

d_inverse'691'_1280 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleMagma_958 → Integer → T__'8801'__12 Source #

d_inverse'737'_1282 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleMagma_958 → Integer → T__'8801'__12 Source #

d_isEquivalence_1284 ∷ T_IsInvertibleMagma_958 → T_IsEquivalence_28 Source #

d_isMagma_1286 ∷ T_IsInvertibleMagma_958 → T_IsMagma_178 Source #

d_isPartialEquivalence_1288 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleMagma_958 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1288 ∷ T_IsInvertibleMagma_958 → T_IsPartialEquivalence_16 Source #

d_refl_1290 ∷ T_IsInvertibleMagma_958 → Integer → T__'8801'__12 Source #

d_reflexive_1292 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleMagma_958 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_1294 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleMagma_958 → T_Setoid_46 Source #

du_setoid_1294 ∷ T_IsInvertibleMagma_958 → T_Setoid_46 Source #

d_sym_1296 ∷ T_IsInvertibleMagma_958 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_1298 ∷ T_IsInvertibleMagma_958 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8315''185''45'cong_1300 ∷ T_IsInvertibleMagma_958 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_1302 ∷ T_IsInvertibleMagma_958 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_1304 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleMagma_958 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_1306 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleMagma_958 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1310 ∷ T_IsInvertibleUnitalMagma_1012 → T_Σ_14 Source #

d_identity'691'_1312 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleUnitalMagma_1012 → Integer → T__'8801'__12 Source #

d_identity'737'_1314 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleUnitalMagma_1012 → Integer → T__'8801'__12 Source #

d_inverse_1316 ∷ T_IsInvertibleUnitalMagma_1012 → T_Σ_14 Source #

d_inverse'691'_1318 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleUnitalMagma_1012 → Integer → T__'8801'__12 Source #

d_inverse'737'_1320 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleUnitalMagma_1012 → Integer → T__'8801'__12 Source #

d_isEquivalence_1322 ∷ T_IsInvertibleUnitalMagma_1012 → T_IsEquivalence_28 Source #

d_isInvertibleMagma_1324 ∷ T_IsInvertibleUnitalMagma_1012 → T_IsInvertibleMagma_958 Source #

d_isMagma_1326 ∷ T_IsInvertibleUnitalMagma_1012 → T_IsMagma_178 Source #

d_isPartialEquivalence_1328 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleUnitalMagma_1012 → T_IsPartialEquivalence_16 Source #

du_isPartialEquivalence_1328 ∷ T_IsInvertibleUnitalMagma_1012 → T_IsPartialEquivalence_16 Source #

d_isUnitalMagma_1330 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleUnitalMagma_1012 → T_IsUnitalMagma_666 Source #

d_refl_1332 ∷ T_IsInvertibleUnitalMagma_1012 → Integer → T__'8801'__12 Source #

d_reflexive_1334 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleUnitalMagma_1012 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_setoid_1336 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleUnitalMagma_1012 → T_Setoid_46 Source #

du_setoid_1336 ∷ T_IsInvertibleUnitalMagma_1012 → T_Setoid_46 Source #

d_sym_1338 ∷ T_IsInvertibleUnitalMagma_1012 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_trans_1340 ∷ T_IsInvertibleUnitalMagma_1012 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8315''185''45'cong_1342 ∷ T_IsInvertibleUnitalMagma_1012 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_1344 ∷ T_IsInvertibleUnitalMagma_1012 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'691'_1346 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleUnitalMagma_1012 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong'737'_1348 ∷ (Integer → Integer → Integer) → Integer → (Integer → Integer) → T_IsInvertibleUnitalMagma_1012 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'42''45'assoc_1352 ∷ T_IsKleeneAlgebra_2122 → Integer → Integer → Integer → T__'8801'__12 Source #