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_Commutative_32 ∷ (Integer → Integer → Integer) → () Source #

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

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

d_Conical_38 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_Flexible_40 ∷ (Integer → Integer → Integer) → () Source #

d_Idempotent_42 ∷ (Integer → Integer → Integer) → () Source #

d_IdempotentFun_44 ∷ (Integer → Integer) → () Source #

d_Identical_46 ∷ (Integer → Integer → Integer) → () Source #

d_Identity_48 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_Interchangable_50 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_Inverse_52 ∷ Integer → (Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_Invertible_54 ∷ Integer → (Integer → Integer → Integer) → Integer → () Source #

d_Involutive_56 ∷ (Integer → Integer) → () Source #

d_LeftAlternative_58 ∷ (Integer → Integer → Integer) → () Source #

d_LeftBol_60 ∷ (Integer → Integer → Integer) → () Source #

d_LeftCongruent_62 ∷ (Integer → Integer → Integer) → () Source #

d_LeftConical_64 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_LeftDivides_66 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

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

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

d_LeftIdentity_72 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_LeftInverse_74 ∷ Integer → (Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_LeftInvertible_76 ∷ Integer → (Integer → Integer → Integer) → Integer → () Source #

d_LeftSemimedial_78 ∷ (Integer → Integer → Integer) → () Source #

d_LeftZero_80 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_Medial_82 ∷ (Integer → Integer → Integer) → () Source #

d_MiddleBol_84 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_RightAlternative_86 ∷ (Integer → Integer → Integer) → () Source #

d_RightBol_88 ∷ (Integer → Integer → Integer) → () Source #

d_RightCongruent_90 ∷ (Integer → Integer → Integer) → () Source #

d_RightConical_92 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_RightDivides_94 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

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

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

d_RightIdentity_100 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_RightInverse_102 ∷ Integer → (Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_RightInvertible_104 ∷ Integer → (Integer → Integer → Integer) → Integer → () Source #

d_RightSemimedial_106 ∷ (Integer → Integer → Integer) → () Source #

d_RightZero_108 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_Selective_110 ∷ (Integer → Integer → Integer) → () Source #

d_SelfInverse_112 ∷ (Integer → Integer) → () Source #

d_Semimedial_114 ∷ (Integer → Integer → Integer) → () Source #

d_StarDestructive_116 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → () Source #

d_StarExpansive_118 ∷ Integer → (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → () Source #

d_StarLeftDestructive_120 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → () Source #

d_StarLeftExpansive_122 ∷ Integer → (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → () Source #

d_StarRightDestructive_124 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → () Source #

d_StarRightExpansive_126 ∷ Integer → (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → () Source #

d_Zero_128 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_IsAbelianGroup_132 ∷ p → p → p → () Source #

d_IsAlternativeMagma_136 ∷ p → () Source #

d_IsBand_140 ∷ p → () Source #

d_IsCancellativeCommutativeSemiring_144 ∷ p → p → p → p → () Source #

d_IsCommutativeBand_148 ∷ p → () Source #

d_IsCommutativeMagma_152 ∷ p → () Source #

d_IsCommutativeMonoid_156 ∷ p → p → () Source #

d_IsCommutativeRing_160 ∷ p → p → p → p → p → () Source #

d_IsCommutativeSemigroup_164 ∷ p → () Source #

d_IsCommutativeSemiring_168 ∷ p → p → p → p → () Source #

d_IsCommutativeSemiringWithoutOne_172 ∷ p → p → p → () Source #

d_IsFlexibleMagma_176 ∷ p → () Source #

d_IsGroup_180 ∷ p → p → p → () Source #

d_IsIdempotentCommutativeMonoid_184 ∷ p → p → () Source #

d_IsIdempotentMagma_188 ∷ p → () Source #

d_IsIdempotentMonoid_192 ∷ p → p → () Source #

d_IsIdempotentSemiring_196 ∷ p → p → p → p → () Source #

d_IsInvertibleMagma_200 ∷ p → p → p → () Source #

d_IsInvertibleUnitalMagma_204 ∷ p → p → p → () Source #

d_IsKleeneAlgebra_208 ∷ p → p → p → p → p → () Source #

d_IsLeftBolLoop_212 ∷ p → p → p → p → () Source #

d_IsLoop_216 ∷ p → p → p → p → () Source #

d_IsMagma_220 ∷ p → () Source #

d_IsMedialMagma_224 ∷ p → () Source #

d_IsMiddleBolLoop_228 ∷ p → p → p → p → () Source #

d_IsMonoid_232 ∷ p → p → () Source #

d_IsMoufangLoop_236 ∷ p → p → p → p → () Source #

d_IsNearSemiring_240 ∷ p → p → p → () Source #

d_IsNearring_244 ∷ p → p → p → p → p → () Source #

d_IsNonAssociativeRing_248 ∷ p → p → p → p → p → () Source #

d_IsQuasigroup_252 ∷ p → p → p → () Source #

d_IsQuasiring_256 ∷ p → p → p → p → () Source #

d_IsRightBolLoop_260 ∷ p → p → p → p → () Source #

d_IsRing_264 ∷ p → p → p → p → p → () Source #

d_IsRingWithoutOne_268 ∷ p → p → p → p → () Source #

d_IsSelectiveMagma_272 ∷ p → () Source #

d_IsSemigroup_276 ∷ p → () Source #

d_IsSemimedialMagma_280 ∷ p → () Source #

d_IsSemiring_284 ∷ p → p → p → p → () Source #

d_IsSemiringWithoutAnnihilatingZero_288 ∷ p → p → p → p → () Source #

d_IsSemiringWithoutOne_292 ∷ p → p → p → () Source #

d_IsSuccessorSet_296 ∷ p → p → () Source #

d_IsUnitalMagma_300 ∷ p → p → () Source #

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

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

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

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

d_identity_312 ∷ T_IsAbelianGroup_1172 → T_Σ_14 Source #

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

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

d_inverse_318 ∷ T_IsAbelianGroup_1172 → T_Σ_14 Source #

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

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

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

du_isCommutativeMagma_324 ∷ T_IsAbelianGroup_1172 → T_IsCommutativeMagma_214 Source #

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

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

du_isCommutativeSemigroup_328 ∷ T_IsAbelianGroup_1172 → T_IsCommutativeSemigroup_568 Source #

d_isEquivalence_330 ∷ T_IsAbelianGroup_1172 → T_IsEquivalence_28 Source #

d_isGroup_332 ∷ T_IsAbelianGroup_1172 → T_IsGroup_1074 Source #

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

du_isInvertibleMagma_334 ∷ T_IsAbelianGroup_1172 → T_IsInvertibleMagma_958 Source #

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

du_isInvertibleUnitalMagma_336 ∷ T_IsAbelianGroup_1172 → T_IsInvertibleUnitalMagma_1012 Source #

d_isMagma_338 ∷ T_IsAbelianGroup_1172 → T_IsMagma_178 Source #

d_isMonoid_340 ∷ T_IsAbelianGroup_1172 → T_IsMonoid_712 Source #

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

du_isPartialEquivalence_342 ∷ T_IsAbelianGroup_1172 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_344 ∷ T_IsAbelianGroup_1172 → T_IsSemigroup_488 Source #

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

du_isUnitalMagma_346 ∷ T_IsAbelianGroup_1172 → T_IsUnitalMagma_666 Source #

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

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

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

du_setoid_352 ∷ T_IsAbelianGroup_1172 → T_Setoid_46 Source #

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

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

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

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

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

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

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

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

d_alter_372 ∷ T_IsAlternativeMagma_290 → T_Σ_14 Source #

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

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

d_isEquivalence_378 ∷ T_IsAlternativeMagma_290 → T_IsEquivalence_28 Source #

d_isMagma_380 ∷ T_IsAlternativeMagma_290 → T_IsMagma_178 Source #

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

du_isPartialEquivalence_382 ∷ T_IsAlternativeMagma_290 → T_IsPartialEquivalence_16 Source #

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

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

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

du_setoid_388 ∷ T_IsAlternativeMagma_290 → T_Setoid_46 Source #

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

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

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

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

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

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

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

d_isEquivalence_406 ∷ T_IsBand_526 → T_IsEquivalence_28 Source #

d_isMagma_408 ∷ T_IsBand_526 → T_IsMagma_178 Source #

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

du_isPartialEquivalence_410 ∷ T_IsBand_526 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_412 ∷ T_IsBand_526 → T_IsSemigroup_488 Source #

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

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

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

du_setoid_418 ∷ T_IsBand_526 → T_Setoid_46 Source #

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

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

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

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

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

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

d_'42''45'cancel'691''45'nonZero_434 ∷ (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_436 ∷ T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → Integer → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 → T__'8801'__12 Source #

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

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

d_'8729''45'cong'691'_442 ∷ (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'_444 ∷ (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_446 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_Σ_14 Source #

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

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

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

du_isCommutativeMagma_452 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeMagma_214 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

d_'8729''45'cong'691'_470 ∷ (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'_472 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1872 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_identity_474 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_Σ_14 Source #

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

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

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

du_isCommutativeMagma_480 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeMagma_214 Source #

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

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

du_isCommutativeSemigroup_484 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeSemigroup_568 Source #

d_isMagma_486 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsMagma_178 Source #

d_isMonoid_488 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsMonoid_712 Source #

d_isSemigroup_490 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsSemigroup_488 Source #

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

du_isUnitalMagma_492 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsUnitalMagma_666 Source #

d_distrib_494 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_Σ_14 Source #

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

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

d_isCommutativeSemiring_500 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeSemiring_1750 Source #

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

du_isCommutativeSemiringWithoutOne_502 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsCommutativeSemiringWithoutOne_1438 Source #

d_isEquivalence_504 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsEquivalence_28 Source #

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

du_isNearSemiring_506 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsNearSemiring_1260 Source #

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

du_isPartialEquivalence_508 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsPartialEquivalence_16 Source #

d_isSemiring_510 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsSemiring_1640 Source #

d_isSemiringWithoutAnnihilatingZero_512 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsSemiringWithoutAnnihilatingZero_1536 Source #

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

du_isSemiringWithoutOne_514 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_IsSemiringWithoutOne_1342 Source #

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

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

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

du_setoid_520 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_Setoid_46 Source #

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

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

d_zero_526 ∷ T_IsCancellativeCommutativeSemiring_1872 → T_Σ_14 Source #

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

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

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

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

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

d_isBand_540 ∷ T_IsCommutativeBand_612 → T_IsBand_526 Source #

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

du_isCommutativeMagma_542 ∷ T_IsCommutativeBand_612 → T_IsCommutativeMagma_214 Source #

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

d_isEquivalence_546 ∷ T_IsCommutativeBand_612 → T_IsEquivalence_28 Source #

d_isMagma_548 ∷ T_IsCommutativeBand_612 → T_IsMagma_178 Source #

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

du_isPartialEquivalence_550 ∷ T_IsCommutativeBand_612 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_552 ∷ T_IsCommutativeBand_612 → T_IsSemigroup_488 Source #

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

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

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

du_setoid_558 ∷ T_IsCommutativeBand_612 → T_Setoid_46 Source #

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

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

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

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

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

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

d_isEquivalence_574 ∷ T_IsCommutativeMagma_214 → T_IsEquivalence_28 Source #

d_isMagma_576 ∷ T_IsCommutativeMagma_214 → T_IsMagma_178 Source #

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

du_isPartialEquivalence_578 ∷ T_IsCommutativeMagma_214 → T_IsPartialEquivalence_16 Source #

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

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

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

du_setoid_584 ∷ T_IsCommutativeMagma_214 → T_Setoid_46 Source #

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

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

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

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

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

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

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

d_identity_602 ∷ T_IsCommutativeMonoid_764 → T_Σ_14 Source #

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

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

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

du_isCommutativeMagma_608 ∷ T_IsCommutativeMonoid_764 → T_IsCommutativeMagma_214 Source #

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

d_isEquivalence_612 ∷ T_IsCommutativeMonoid_764 → T_IsEquivalence_28 Source #

d_isMagma_614 ∷ T_IsCommutativeMonoid_764 → T_IsMagma_178 Source #

d_isMonoid_616 ∷ T_IsCommutativeMonoid_764 → T_IsMonoid_712 Source #

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

du_isPartialEquivalence_618 ∷ T_IsCommutativeMonoid_764 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_620 ∷ T_IsCommutativeMonoid_764 → T_IsSemigroup_488 Source #

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

du_isUnitalMagma_622 ∷ T_IsCommutativeMonoid_764 → T_IsUnitalMagma_666 Source #

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

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

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

du_setoid_628 ∷ T_IsCommutativeMonoid_764 → T_Setoid_46 Source #

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

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

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

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

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

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

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

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

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

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

d_'8729''45'cong'691'_650 ∷ (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'_652 ∷ (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_654 ∷ T_IsCommutativeRing_2888 → T_Σ_14 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_'8729''45'cong_676 ∷ (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'_678 ∷ (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'_680 ∷ (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_682 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → T_Σ_14 Source #

du_identity_682 ∷ T_IsCommutativeRing_2888 → T_Σ_14 Source #

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

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

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

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

du_isCommutativeMagma_690 ∷ T_IsCommutativeRing_2888 → T_IsCommutativeMagma_214 Source #

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

du_isCommutativeMonoid_692 ∷ T_IsCommutativeRing_2888 → T_IsCommutativeMonoid_764 Source #

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

du_isCommutativeSemigroup_694 ∷ T_IsCommutativeRing_2888 → T_IsCommutativeSemigroup_568 Source #

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

du_isGroup_696 ∷ T_IsCommutativeRing_2888 → T_IsGroup_1074 Source #

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

du_isInvertibleMagma_698 ∷ T_IsCommutativeRing_2888 → T_IsInvertibleMagma_958 Source #

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

du_isInvertibleUnitalMagma_700 ∷ T_IsCommutativeRing_2888 → T_IsInvertibleUnitalMagma_1012 Source #

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

du_isMagma_702 ∷ T_IsCommutativeRing_2888 → T_IsMagma_178 Source #

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

du_isMonoid_704 ∷ T_IsCommutativeRing_2888 → T_IsMonoid_712 Source #

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

du_isSemigroup_706 ∷ T_IsCommutativeRing_2888 → T_IsSemigroup_488 Source #

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

du_isUnitalMagma_708 ∷ T_IsCommutativeRing_2888 → T_IsUnitalMagma_666 Source #

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

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

du_inverse_712 ∷ T_IsCommutativeRing_2888 → T_Σ_14 Source #

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

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

d_distrib_718 ∷ T_IsCommutativeRing_2888 → T_Σ_14 Source #

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

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

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

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

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

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

du_isEquivalence_728 ∷ T_IsCommutativeRing_2888 → T_IsEquivalence_28 Source #

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

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

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

du_isPartialEquivalence_732 ∷ T_IsCommutativeRing_2888 → T_IsPartialEquivalence_16 Source #

d_isRing_734 ∷ T_IsCommutativeRing_2888 → T_IsRing_2740 Source #

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

du_isRingWithoutOne_736 ∷ T_IsCommutativeRing_2888 → T_IsRingWithoutOne_2368 Source #

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

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

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

du_isSemiringWithoutAnnihilatingZero_740 ∷ T_IsCommutativeRing_2888 → T_IsSemiringWithoutAnnihilatingZero_1536 Source #

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

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

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

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

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

du_setoid_748 ∷ T_IsCommutativeRing_2888 → T_Setoid_46 Source #

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

d_trans_752 ∷ (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'_754 ∷ (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'_756 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_2888 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

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

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

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

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

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

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

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

d_isEquivalence_772 ∷ T_IsCommutativeSemigroup_568 → T_IsEquivalence_28 Source #

d_isMagma_774 ∷ T_IsCommutativeSemigroup_568 → T_IsMagma_178 Source #

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

du_isPartialEquivalence_776 ∷ T_IsCommutativeSemigroup_568 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_778 ∷ T_IsCommutativeSemigroup_568 → T_IsSemigroup_488 Source #

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

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

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

du_setoid_784 ∷ T_IsCommutativeSemigroup_568 → T_Setoid_46 Source #

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

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

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

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

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

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

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

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

d_'8729''45'cong'691'_804 ∷ (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'_806 ∷ (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_808 ∷ T_IsCommutativeSemiring_1750 → T_Σ_14 Source #

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

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

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

du_isCommutativeMagma_814 ∷ T_IsCommutativeSemiring_1750 → T_IsCommutativeMagma_214 Source #

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

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

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

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

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

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

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

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

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

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

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

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

d_'8729''45'cong'691'_832 ∷ (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'_834 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1750 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_identity_836 ∷ T_IsCommutativeSemiring_1750 → T_Σ_14 Source #

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

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

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

du_isCommutativeMagma_842 ∷ T_IsCommutativeSemiring_1750 → T_IsCommutativeMagma_214 Source #

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

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

du_isCommutativeSemigroup_846 ∷ T_IsCommutativeSemiring_1750 → T_IsCommutativeSemigroup_568 Source #

d_isMagma_848 ∷ T_IsCommutativeSemiring_1750 → T_IsMagma_178 Source #

d_isMonoid_850 ∷ T_IsCommutativeSemiring_1750 → T_IsMonoid_712 Source #

d_isSemigroup_852 ∷ T_IsCommutativeSemiring_1750 → T_IsSemigroup_488 Source #

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

du_isUnitalMagma_854 ∷ T_IsCommutativeSemiring_1750 → T_IsUnitalMagma_666 Source #

d_distrib_856 ∷ T_IsCommutativeSemiring_1750 → T_Σ_14 Source #

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

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

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

d_isEquivalence_864 ∷ T_IsCommutativeSemiring_1750 → T_IsEquivalence_28 Source #

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

du_isNearSemiring_866 ∷ T_IsCommutativeSemiring_1750 → T_IsNearSemiring_1260 Source #

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

du_isPartialEquivalence_868 ∷ T_IsCommutativeSemiring_1750 → T_IsPartialEquivalence_16 Source #

d_isSemiring_870 ∷ T_IsCommutativeSemiring_1750 → T_IsSemiring_1640 Source #

d_isSemiringWithoutAnnihilatingZero_872 ∷ T_IsCommutativeSemiring_1750 → T_IsSemiringWithoutAnnihilatingZero_1536 Source #

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

du_isSemiringWithoutOne_874 ∷ T_IsCommutativeSemiring_1750 → T_IsSemiringWithoutOne_1342 Source #

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

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

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

du_setoid_880 ∷ T_IsCommutativeSemiring_1750 → T_Setoid_46 Source #

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

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

d_zero_886 ∷ T_IsCommutativeSemiring_1750 → T_Σ_14 Source #

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

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

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

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

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

d_'8729''45'cong'691'_900 ∷ (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'_902 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

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

du_isCommutativeMagma_904 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsCommutativeMagma_214 Source #

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

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

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

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

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

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

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

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

d_'8729''45'cong'691'_918 ∷ (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'_920 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1438 → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_identity_922 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_Σ_14 Source #

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

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

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

du_isCommutativeMagma_928 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsCommutativeMagma_214 Source #

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

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

du_isCommutativeSemigroup_932 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsCommutativeSemigroup_568 Source #

d_isMonoid_934 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsMonoid_712 Source #

d_distrib_936 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_Σ_14 Source #

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

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

d_isEquivalence_942 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsEquivalence_28 Source #

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

du_isNearSemiring_944 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsNearSemiring_1260 Source #

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

du_isPartialEquivalence_946 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsPartialEquivalence_16 Source #

d_isSemiringWithoutOne_948 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_IsSemiringWithoutOne_1342 Source #

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

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

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

du_setoid_954 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_Setoid_46 Source #

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

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

d_zero_960 ∷ T_IsCommutativeSemiringWithoutOne_1438 → T_Σ_14 Source #

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

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

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

d_isEquivalence_970 ∷ T_IsFlexibleMagma_332 → T_IsEquivalence_28 Source #

d_isMagma_972 ∷ T_IsFlexibleMagma_332 → T_IsMagma_178 Source #

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

du_isPartialEquivalence_974 ∷ T_IsFlexibleMagma_332 → T_IsPartialEquivalence_16 Source #

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

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

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

du_setoid_980 ∷ T_IsFlexibleMagma_332 → T_Setoid_46 Source #

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

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

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

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

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

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

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

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

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

d_identity_1002 ∷ T_IsGroup_1074 → T_Σ_14 Source #

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

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

d_inverse_1008 ∷ T_IsGroup_1074 → T_Σ_14 Source #

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

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

d_isEquivalence_1014 ∷ T_IsGroup_1074 → T_IsEquivalence_28 Source #

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

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

d_isMagma_1020 ∷ T_IsGroup_1074 → T_IsMagma_178 Source #

d_isMonoid_1022 ∷ T_IsGroup_1074 → T_IsMonoid_712 Source #

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

du_isPartialEquivalence_1024 ∷ T_IsGroup_1074 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1026 ∷ T_IsGroup_1074 → T_IsSemigroup_488 Source #

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

du_isUnitalMagma_1028 ∷ T_IsGroup_1074 → T_IsUnitalMagma_666 Source #

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

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

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

du_setoid_1034 ∷ T_IsGroup_1074 → T_Setoid_46 Source #

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

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

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

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

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

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

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

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

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

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

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

d_identity_1060 ∷ T_IsIdempotentCommutativeMonoid_884 → T_Σ_14 Source #

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

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

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

du_isBand_1066 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsBand_526 Source #

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

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

du_isCommutativeMagma_1070 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeMagma_214 Source #

d_isCommutativeMonoid_1072 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeMonoid_764 Source #

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

du_isCommutativeSemigroup_1074 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsCommutativeSemigroup_568 Source #

d_isEquivalence_1076 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsEquivalence_28 Source #

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

d_isMagma_1080 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsMagma_178 Source #

d_isMonoid_1082 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsMonoid_712 Source #

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

du_isPartialEquivalence_1084 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1086 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsSemigroup_488 Source #

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

du_isUnitalMagma_1088 ∷ T_IsIdempotentCommutativeMonoid_884 → T_IsUnitalMagma_666 Source #

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

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

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

du_setoid_1094 ∷ T_IsIdempotentCommutativeMonoid_884 → T_Setoid_46 Source #

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

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

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

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

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

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

d_isEquivalence_1110 ∷ T_IsIdempotentMagma_252 → T_IsEquivalence_28 Source #

d_isMagma_1112 ∷ T_IsIdempotentMagma_252 → T_IsMagma_178 Source #

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

du_isPartialEquivalence_1114 ∷ T_IsIdempotentMagma_252 → T_IsPartialEquivalence_16 Source #

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

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

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

du_setoid_1120 ∷ T_IsIdempotentMagma_252 → T_Setoid_46 Source #

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

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

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

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

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

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

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

d_identity_1138 ∷ T_IsIdempotentMonoid_826 → T_Σ_14 Source #

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

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

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

d_isEquivalence_1146 ∷ T_IsIdempotentMonoid_826 → T_IsEquivalence_28 Source #

d_isMagma_1148 ∷ T_IsIdempotentMonoid_826 → T_IsMagma_178 Source #

d_isMonoid_1150 ∷ T_IsIdempotentMonoid_826 → T_IsMonoid_712 Source #

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

du_isPartialEquivalence_1152 ∷ T_IsIdempotentMonoid_826 → T_IsPartialEquivalence_16 Source #

d_isSemigroup_1154 ∷ T_IsIdempotentMonoid_826 → T_IsSemigroup_488 Source #

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

du_isUnitalMagma_1156 ∷ T_IsIdempotentMonoid_826 → T_IsUnitalMagma_666 Source #

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

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

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

du_setoid_1162 ∷ T_IsIdempotentMonoid_826 → T_Setoid_46 Source #

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

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

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

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

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

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

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

d_'8729''45'cong'691'_1180 ∷ (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'_1182 ∷ (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_1184 ∷ T_IsIdempotentSemiring_1998 → T_Σ_14 Source #

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

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

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

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

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

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

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

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

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

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

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

d_'8729''45'cong'691'_1202 ∷ (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'_1204 ∷ (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_1206 ∷ T_IsIdempotentSemiring_1998 → Integer → T__'8801'__12 Source #

d_identity_1208 ∷ T_IsIdempotentSemiring_1998 → T_Σ_14 Source #

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

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

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

du_isBand_1214 ∷ T_IsIdempotentSemiring_1998 → T_IsBand_526 Source #

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

du_isCommutativeBand_1216 ∷ T_IsIdempotentSemiring_1998 → T_IsCommutativeBand_612 Source #

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

du_isCommutativeMagma_1218 ∷ T_IsIdempotentSemiring_1998 → T_IsCommutativeMagma_214 Source #

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

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

du_isCommutativeSemigroup_1222 ∷ T_IsIdempotentSemiring_1998 → T_IsCommutativeSemigroup_568 Source #

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

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

du_isIdempotentMonoid_1226 ∷ T_IsIdempotentSemiring_1998 → T_IsIdempotentMonoid_826 Source #

d_isMagma_1228 ∷ T_IsIdempotentSemiring_1998 → T_IsMagma_178 Source #

d_isMonoid_1230 ∷ T_IsIdempotentSemiring_1998 → T_IsMonoid_712 Source #

d_isSemigroup_1232 ∷ T_IsIdempotentSemiring_1998 → T_IsSemigroup_488 Source #

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

du_isUnitalMagma_1234 ∷ T_IsIdempotentSemiring_1998 → T_IsUnitalMagma_666 Source #

d_distrib_1236 ∷ T_IsIdempotentSemiring_1998 → T_Σ_14 Source #

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

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

d_isEquivalence_1242 ∷ T_IsIdempotentSemiring_1998 → T_IsEquivalence_28 Source #

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

du_isNearSemiring_1244 ∷ T_IsIdempotentSemiring_1998 → T_IsNearSemiring_1260 Source #

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

du_isPartialEquivalence_1246 ∷ T_IsIdempotentSemiring_1998 → T_IsPartialEquivalence_16 Source #

d_isSemiring_1248 ∷ T_IsIdempotentSemiring_1998 → T_IsSemiring_1640 Source #

d_isSemiringWithoutAnnihilatingZero_1250 ∷ T_IsIdempotentSemiring_1998 → T_IsSemiringWithoutAnnihilatingZero_1536 Source #

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

du_isSemiringWithoutOne_1252 ∷ T_IsIdempotentSemiring_1998 → T_IsSemiringWithoutOne_1342 Source #

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

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

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

du_setoid_1258 ∷ T_IsIdempotentSemiring_1998 → T_Setoid_46 Source #

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

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

d_zero_1264 ∷ T_IsIdempotentSemiring_1998 → T_Σ_14 Source #

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

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

d_inverse_1272 ∷ T_IsInvertibleMagma_958 → T_Σ_14 Source #

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

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

d_isEquivalence_1278 ∷ T_IsInvertibleMagma_958 → T_IsEquivalence_28 Source #

d_isMagma_1280 ∷ T_IsInvertibleMagma_958 → T_IsMagma_178 Source #

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

du_isPartialEquivalence_1282 ∷ T_IsInvertibleMagma_958 → T_IsPartialEquivalence_16 Source #

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

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

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

du_setoid_1288 ∷ T_IsInvertibleMagma_958 → T_Setoid_46 Source #

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

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

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

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

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

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

d_identity_1304 ∷ T_IsInvertibleUnitalMagma_1012 → T_Σ_14 Source #

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

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

d_inverse_1310 ∷ T_IsInvertibleUnitalMagma_1012 → T_Σ_14 Source #

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

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

d_isEquivalence_1316 ∷ T_IsInvertibleUnitalMagma_1012 → T_IsEquivalence_28 Source #

d_isInvertibleMagma_1318 ∷ T_IsInvertibleUnitalMagma_1012 → T_IsInvertibleMagma_958 Source #

d_isMagma_1320 ∷ T_IsInvertibleUnitalMagma_1012 → T_IsMagma_178 Source #

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

du_isPartialEquivalence_1322 ∷ T_IsInvertibleUnitalMagma_1012 → T_IsPartialEquivalence_16 Source #

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

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

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

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

du_setoid_1330 ∷ T_IsInvertibleUnitalMagma_1012 → T_Setoid_46 Source #

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

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

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

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

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

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

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

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

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