Documentation

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

d_Commutative_30 ∷ (Integer → Integer → Integer) → () Source #

d_Identity_42 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_Inverse_46 ∷ Integer → (Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_LeftIdentity_56 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_LeftInverse_58 ∷ Integer → (Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_LeftZero_60 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_RightIdentity_68 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_RightInverse_70 ∷ Integer → (Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_RightZero_72 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_Zero_76 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_IsAbelianGroup_80 ∷ p → p → p → () Source #

d_IsBand_82 ∷ p → () Source #

d_IsCancellativeCommutativeSemiring_88 ∷ p → p → p → p → () Source #

d_IsCommutativeMagma_90 ∷ p → () Source #

d_IsCommutativeMonoid_92 ∷ p → p → () Source #

d_IsCommutativeRing_94 ∷ p → p → p → p → p → () Source #

d_IsCommutativeSemigroup_96 ∷ p → () Source #

d_IsCommutativeSemiring_98 ∷ p → p → p → p → () Source #

d_IsCommutativeSemiringWithoutOne_100 ∷ p → p → p → () Source #

d_IsGroup_104 ∷ p → p → p → () Source #

d_IsIdempotentCommutativeMonoid_106 ∷ p → p → () Source #

d_IsMagma_110 ∷ p → () Source #

d_IsMonoid_112 ∷ p → p → () Source #

d_IsNearSemiring_114 ∷ p → p → p → () Source #

d_IsRing_116 ∷ p → p → p → p → p → () Source #

d_IsSelectiveMagma_118 ∷ p → () Source #

d_IsSemigroup_120 ∷ p → () Source #

d_IsSemilattice_122 ∷ p → () Source #

d_IsSemiring_124 ∷ p → p → p → p → () Source #

d_IsSemiringWithoutAnnihilatingZero_126 ∷ p → p → p → p → () Source #

d_IsSemiringWithoutOne_128 ∷ p → p → p → () Source #

d_assoc_134 ∷ T_IsAbelianGroup_662 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_136 ∷ T_IsAbelianGroup_662 → Integer → Integer → T__'8801'__12 Source #

d_identity_138 ∷ T_IsAbelianGroup_662 → T_Σ_14 Source #

d_inverse_144 ∷ T_IsAbelianGroup_662 → T_Σ_14 Source #

d_isEquivalence_156 ∷ T_IsAbelianGroup_662 → T_IsEquivalence_26 Source #

d_isGroup_158 ∷ T_IsAbelianGroup_662 → T_IsGroup_580 Source #

d_isMagma_160 ∷ T_IsAbelianGroup_662 → T_IsMagma_86 Source #

d_isMonoid_162 ∷ T_IsAbelianGroup_662 → T_IsMonoid_358 Source #

d_isSemigroup_166 ∷ T_IsAbelianGroup_662 → T_IsSemigroup_194 Source #

d_'8315''185''45'cong_182 ∷ T_IsAbelianGroup_662 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_184 ∷ T_IsAbelianGroup_662 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_192 ∷ T_IsBand_230 → Integer → Integer → Integer → T__'8801'__12 Source #

d_idem_194 ∷ T_IsBand_230 → Integer → T__'8801'__12 Source #

d_isEquivalence_196 ∷ T_IsBand_230 → T_IsEquivalence_26 Source #

d_isMagma_198 ∷ T_IsBand_230 → T_IsMagma_86 Source #

d_isSemigroup_202 ∷ T_IsBand_230 → T_IsSemigroup_194 Source #

d_'8729''45'cong_214 ∷ T_IsBand_230 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_276 ∷ T_IsIdempotentCommutativeMonoid_464 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_278 ∷ T_IsIdempotentCommutativeMonoid_464 → Integer → Integer → T__'8801'__12 Source #

d_idem_280 ∷ T_IsIdempotentCommutativeMonoid_464 → Integer → T__'8801'__12 Source #

d_identity_282 ∷ T_IsIdempotentCommutativeMonoid_464 → T_Σ_14 Source #

d_isCommutativeMonoid_290 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeMonoid_406 Source #

d_isEquivalence_294 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsEquivalence_26 Source #

d_isMagma_296 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMagma_86 Source #

d_isMonoid_298 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMonoid_358 Source #

d_isSemigroup_302 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsSemigroup_194 Source #

d_'8729''45'cong_314 ∷ T_IsIdempotentCommutativeMonoid_464 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_322 ∷ T_IsCancellativeCommutativeSemiring_1462 → Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'cancel'737''45'nonZero_324 ∷ T_IsCancellativeCommutativeSemiring_1462 → Integer → Integer → Integer → (T__'8801'__12 → T_'8869'_4) → T__'8801'__12 → T__'8801'__12 Source #

d_'42''45'comm_326 ∷ T_IsCancellativeCommutativeSemiring_1462 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_328 ∷ T_IsCancellativeCommutativeSemiring_1462 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_334 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

d_isMagma_346 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsMagma_86 Source #

d_'42''45'isMonoid_348 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsMonoid_358 Source #

d_isSemigroup_350 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemigroup_194 Source #

d_assoc_352 ∷ T_IsCancellativeCommutativeSemiring_1462 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_354 ∷ T_IsCancellativeCommutativeSemiring_1462 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_356 ∷ T_IsCancellativeCommutativeSemiring_1462 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_362 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

d_'43''45'isCommutativeMonoid_370 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeMonoid_406 Source #

d_isMagma_374 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsMagma_86 Source #

d_isMonoid_376 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsMonoid_358 Source #

d_isSemigroup_378 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemigroup_194 Source #

d_distrib_380 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

d_isCommutativeSemiring_386 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeSemiring_1344 Source #

d_isEquivalence_390 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsEquivalence_26 Source #

d_isNearSemiring_392 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1462 → T_IsNearSemiring_876 Source #

du_isNearSemiring_392 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsNearSemiring_876 Source #

d_isSemiring_396 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemiring_1238 Source #

d_isSemiringWithoutAnnihilatingZero_398 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

d_isSemiringWithoutOne_400 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCancellativeCommutativeSemiring_1462 → T_IsSemiringWithoutOne_952 Source #

du_isSemiringWithoutOne_400 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemiringWithoutOne_952 Source #

d_zero_412 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

d_comm_420 ∷ T_IsCommutativeMagma_122 → Integer → Integer → T__'8801'__12 Source #

d_isEquivalence_422 ∷ T_IsCommutativeMagma_122 → T_IsEquivalence_26 Source #

d_isMagma_424 ∷ T_IsCommutativeMagma_122 → T_IsMagma_86 Source #

d_'8729''45'cong_438 ∷ T_IsCommutativeMagma_122 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_446 ∷ T_IsCommutativeMonoid_406 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_448 ∷ T_IsCommutativeMonoid_406 → Integer → Integer → T__'8801'__12 Source #

d_identity_450 ∷ T_IsCommutativeMonoid_406 → T_Σ_14 Source #

d_isEquivalence_460 ∷ T_IsCommutativeMonoid_406 → T_IsEquivalence_26 Source #

d_isMagma_462 ∷ T_IsCommutativeMonoid_406 → T_IsMagma_86 Source #

d_isMonoid_464 ∷ T_IsCommutativeMonoid_406 → T_IsMonoid_358 Source #

d_isSemigroup_468 ∷ T_IsCommutativeMonoid_406 → T_IsSemigroup_194 Source #

d_'8729''45'cong_480 ∷ T_IsCommutativeMonoid_406 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_490 ∷ T_IsCommutativeRing_1720 → Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'comm_492 ∷ T_IsCommutativeRing_1720 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_494 ∷ T_IsCommutativeRing_1720 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_500 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_isMagma_512 ∷ T_IsCommutativeRing_1720 → T_IsMagma_86 Source #

d_'42''45'isMonoid_514 ∷ T_IsCommutativeRing_1720 → T_IsMonoid_358 Source #

d_isSemigroup_516 ∷ T_IsCommutativeRing_1720 → T_IsSemigroup_194 Source #

d_assoc_518 ∷ T_IsCommutativeRing_1720 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_520 ∷ T_IsCommutativeRing_1720 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_522 ∷ T_IsCommutativeRing_1720 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_528 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_'43''45'isAbelianGroup_534 ∷ T_IsCommutativeRing_1720 → T_IsAbelianGroup_662 Source #

d_isGroup_542 ∷ T_IsCommutativeRing_1720 → T_IsGroup_580 Source #

d_isMagma_544 ∷ T_IsCommutativeRing_1720 → T_IsMagma_86 Source #

d_isMonoid_546 ∷ T_IsCommutativeRing_1720 → T_IsMonoid_358 Source #

d_isSemigroup_548 ∷ T_IsCommutativeRing_1720 → T_IsSemigroup_194 Source #

d_'8315''185''45'cong_550 ∷ T_IsCommutativeRing_1720 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_inverse_552 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_distrib_558 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_isEquivalence_568 ∷ T_IsCommutativeRing_1720 → T_IsEquivalence_26 Source #

d_isNearSemiring_570 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_1720 → T_IsNearSemiring_876 Source #

du_isNearSemiring_570 ∷ T_IsCommutativeRing_1720 → T_IsNearSemiring_876 Source #

d_isRing_574 ∷ T_IsCommutativeRing_1720 → T_IsRing_1584 Source #

d_isSemiring_576 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_1720 → T_IsSemiring_1238 Source #

du_isSemiring_576 ∷ T_IsCommutativeRing_1720 → T_IsSemiring_1238 Source #

d_isSemiringWithoutOne_580 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsCommutativeRing_1720 → T_IsSemiringWithoutOne_952 Source #

du_isSemiringWithoutOne_580 ∷ T_IsCommutativeRing_1720 → T_IsSemiringWithoutOne_952 Source #

d_zero_596 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

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

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

d_isEquivalence_610 ∷ T_IsCommutativeSemigroup_270 → T_IsEquivalence_26 Source #

d_isMagma_612 ∷ T_IsCommutativeSemigroup_270 → T_IsMagma_86 Source #

d_isSemigroup_616 ∷ T_IsCommutativeSemigroup_270 → T_IsSemigroup_194 Source #

d_'8729''45'cong_628 ∷ T_IsCommutativeSemigroup_270 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_636 ∷ T_IsCommutativeSemiring_1344 → Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'comm_638 ∷ T_IsCommutativeSemiring_1344 → Integer → Integer → T__'8801'__12 Source #

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

d_identity_646 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

d_isMagma_658 ∷ T_IsCommutativeSemiring_1344 → T_IsMagma_86 Source #

d_'42''45'isMonoid_660 ∷ T_IsCommutativeSemiring_1344 → T_IsMonoid_358 Source #

d_isSemigroup_662 ∷ T_IsCommutativeSemiring_1344 → T_IsSemigroup_194 Source #

d_assoc_664 ∷ T_IsCommutativeSemiring_1344 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_666 ∷ T_IsCommutativeSemiring_1344 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_668 ∷ T_IsCommutativeSemiring_1344 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_674 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

d_'43''45'isCommutativeMonoid_682 ∷ T_IsCommutativeSemiring_1344 → T_IsCommutativeMonoid_406 Source #

d_isMagma_686 ∷ T_IsCommutativeSemiring_1344 → T_IsMagma_86 Source #

d_isMonoid_688 ∷ T_IsCommutativeSemiring_1344 → T_IsMonoid_358 Source #

d_isSemigroup_690 ∷ T_IsCommutativeSemiring_1344 → T_IsSemigroup_194 Source #

d_distrib_692 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

d_isEquivalence_700 ∷ T_IsCommutativeSemiring_1344 → T_IsEquivalence_26 Source #

d_isNearSemiring_702 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1344 → T_IsNearSemiring_876 Source #

du_isNearSemiring_702 ∷ T_IsCommutativeSemiring_1344 → T_IsNearSemiring_876 Source #

d_isSemiring_706 ∷ T_IsCommutativeSemiring_1344 → T_IsSemiring_1238 Source #

d_isSemiringWithoutAnnihilatingZero_708 ∷ T_IsCommutativeSemiring_1344 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

d_isSemiringWithoutOne_710 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsCommutativeSemiring_1344 → T_IsSemiringWithoutOne_952 Source #

du_isSemiringWithoutOne_710 ∷ T_IsCommutativeSemiring_1344 → T_IsSemiringWithoutOne_952 Source #

d_zero_722 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

d_assoc_730 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1044 → Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'comm_732 ∷ T_IsCommutativeSemiringWithoutOne_1044 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_734 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1044 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_isMagma_744 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1044 → T_IsMagma_86 Source #

du_isMagma_744 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsMagma_86 Source #

d_'42''45'isSemigroup_746 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsSemigroup_194 Source #

d_assoc_748 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1044 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_750 ∷ T_IsCommutativeSemiringWithoutOne_1044 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_752 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1044 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_758 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

du_identity_758 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

d_'43''45'isCommutativeMonoid_766 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsCommutativeMonoid_406 Source #

d_isMagma_770 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1044 → T_IsMagma_86 Source #

du_isMagma_770 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsMagma_86 Source #

d_isMonoid_772 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsMonoid_358 Source #

d_isSemigroup_774 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1044 → T_IsSemigroup_194 Source #

du_isSemigroup_774 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsSemigroup_194 Source #

d_distrib_776 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

d_distrib'691'_778 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1044 → Integer → Integer → Integer → T__'8801'__12 Source #

d_isEquivalence_780 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1044 → T_IsEquivalence_26 Source #

du_isEquivalence_780 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsEquivalence_26 Source #

d_isNearSemiring_782 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1044 → T_IsNearSemiring_876 Source #

du_isNearSemiring_782 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsNearSemiring_876 Source #

d_isSemiringWithoutOne_786 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsSemiringWithoutOne_952 Source #

d_zero_798 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

d_assoc_854 ∷ T_IsGroup_580 → Integer → Integer → Integer → T__'8801'__12 Source #

d_identity_856 ∷ T_IsGroup_580 → T_Σ_14 Source #

d_inverse_862 ∷ T_IsGroup_580 → T_Σ_14 Source #

d_isEquivalence_868 ∷ T_IsGroup_580 → T_IsEquivalence_26 Source #

d_isMagma_870 ∷ T_IsGroup_580 → T_IsMagma_86 Source #

d_isMonoid_872 ∷ T_IsGroup_580 → T_IsMonoid_358 Source #

d_isSemigroup_876 ∷ T_IsGroup_580 → T_IsSemigroup_194 Source #

d_'8315''185''45'cong_892 ∷ T_IsGroup_580 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_894 ∷ T_IsGroup_580 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_902 ∷ T_IsIdempotentCommutativeMonoid_464 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_904 ∷ T_IsIdempotentCommutativeMonoid_464 → Integer → Integer → T__'8801'__12 Source #

d_idem_906 ∷ T_IsIdempotentCommutativeMonoid_464 → Integer → T__'8801'__12 Source #

d_identity_908 ∷ T_IsIdempotentCommutativeMonoid_464 → T_Σ_14 Source #

d_isCommutativeMonoid_916 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeMonoid_406 Source #

d_isEquivalence_920 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsEquivalence_26 Source #

d_isMagma_922 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMagma_86 Source #

d_isMonoid_924 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMonoid_358 Source #

d_isSemigroup_928 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsSemigroup_194 Source #

d_'8729''45'cong_940 ∷ T_IsIdempotentCommutativeMonoid_464 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_isEquivalence_988 ∷ T_IsMagma_86 → T_IsEquivalence_26 Source #

d_'8729''45'cong_1002 ∷ T_IsMagma_86 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_1010 ∷ T_IsMonoid_358 → Integer → Integer → Integer → T__'8801'__12 Source #

d_identity_1012 ∷ T_IsMonoid_358 → T_Σ_14 Source #

d_isEquivalence_1018 ∷ T_IsMonoid_358 → T_IsEquivalence_26 Source #

d_isMagma_1020 ∷ T_IsMonoid_358 → T_IsMagma_86 Source #

d_isSemigroup_1024 ∷ T_IsMonoid_358 → T_IsSemigroup_194 Source #

d_'8729''45'cong_1036 ∷ T_IsMonoid_358 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_1044 ∷ T_IsNearSemiring_876 → Integer → Integer → Integer → T__'8801'__12 Source #

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

d_isMagma_1052 ∷ T_IsNearSemiring_876 → T_IsMagma_86 Source #

d_'42''45'isSemigroup_1054 ∷ T_IsNearSemiring_876 → T_IsSemigroup_194 Source #

d_assoc_1056 ∷ T_IsNearSemiring_876 → Integer → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_1058 ∷ T_IsNearSemiring_876 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1064 ∷ T_IsNearSemiring_876 → T_Σ_14 Source #

d_isMagma_1070 ∷ T_IsNearSemiring_876 → T_IsMagma_86 Source #

d_'43''45'isMonoid_1072 ∷ T_IsNearSemiring_876 → T_IsMonoid_358 Source #

d_isSemigroup_1074 ∷ T_IsNearSemiring_876 → T_IsSemigroup_194 Source #

d_distrib'691'_1076 ∷ T_IsNearSemiring_876 → Integer → Integer → Integer → T__'8801'__12 Source #

d_isEquivalence_1078 ∷ T_IsNearSemiring_876 → T_IsEquivalence_26 Source #

d_zero'737'_1092 ∷ T_IsNearSemiring_876 → Integer → T__'8801'__12 Source #

d_assoc_1098 ∷ T_IsRing_1584 → Integer → Integer → Integer → T__'8801'__12 Source #

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

d_identity_1106 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_isMagma_1112 ∷ T_IsRing_1584 → T_IsMagma_86 Source #

d_'42''45'isMonoid_1114 ∷ T_IsRing_1584 → T_IsMonoid_358 Source #

d_isSemigroup_1116 ∷ T_IsRing_1584 → T_IsSemigroup_194 Source #

d_assoc_1118 ∷ T_IsRing_1584 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_1120 ∷ T_IsRing_1584 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_1122 ∷ T_IsRing_1584 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1128 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_'43''45'isAbelianGroup_1134 ∷ T_IsRing_1584 → T_IsAbelianGroup_662 Source #

d_isGroup_1142 ∷ T_IsRing_1584 → T_IsGroup_580 Source #

d_isMagma_1144 ∷ T_IsRing_1584 → T_IsMagma_86 Source #

d_isMonoid_1146 ∷ T_IsRing_1584 → T_IsMonoid_358 Source #

d_isSemigroup_1148 ∷ T_IsRing_1584 → T_IsSemigroup_194 Source #

d_'8315''185''45'cong_1150 ∷ T_IsRing_1584 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_inverse_1152 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_distrib_1158 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_isEquivalence_1164 ∷ T_IsRing_1584 → T_IsEquivalence_26 Source #

d_isNearSemiring_1166 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsRing_1584 → T_IsNearSemiring_876 Source #

du_isNearSemiring_1166 ∷ T_IsRing_1584 → T_IsNearSemiring_876 Source #

d_isSemiring_1170 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsRing_1584 → T_IsSemiring_1238 Source #

d_isSemiringWithoutOne_1174 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer) → Integer → Integer → T_IsRing_1584 → T_IsSemiringWithoutOne_952 Source #

du_isSemiringWithoutOne_1174 ∷ T_IsRing_1584 → T_IsSemiringWithoutOne_952 Source #

d_zero_1190 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_isEquivalence_1198 ∷ T_IsSelectiveMagma_158 → T_IsEquivalence_26 Source #

d_isMagma_1200 ∷ T_IsSelectiveMagma_158 → T_IsMagma_86 Source #

d_sel_1208 ∷ T_IsSelectiveMagma_158 → Integer → Integer → T__'8846'__30 Source #

d_'8729''45'cong_1216 ∷ T_IsSelectiveMagma_158 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_1224 ∷ T_IsSemigroup_194 → Integer → Integer → Integer → T__'8801'__12 Source #

d_isEquivalence_1226 ∷ T_IsSemigroup_194 → T_IsEquivalence_26 Source #

d_isMagma_1228 ∷ T_IsSemigroup_194 → T_IsMagma_86 Source #

d_'8729''45'cong_1242 ∷ T_IsSemigroup_194 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_1250 ∷ T_IsSemilattice_312 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_1252 ∷ T_IsSemilattice_312 → Integer → Integer → T__'8801'__12 Source #

d_idem_1254 ∷ T_IsSemilattice_312 → Integer → T__'8801'__12 Source #

d_isBand_1256 ∷ T_IsSemilattice_312 → T_IsBand_230 Source #

d_isEquivalence_1258 ∷ T_IsSemilattice_312 → T_IsEquivalence_26 Source #

d_isMagma_1260 ∷ T_IsSemilattice_312 → T_IsMagma_86 Source #

d_isSemigroup_1264 ∷ T_IsSemilattice_312 → T_IsSemigroup_194 Source #

d_'8729''45'cong_1276 ∷ T_IsSemilattice_312 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_1284 ∷ T_IsSemiring_1238 → Integer → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_1286 ∷ T_IsSemiring_1238 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1292 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

d_isMagma_1298 ∷ T_IsSemiring_1238 → T_IsMagma_86 Source #

d_'42''45'isMonoid_1300 ∷ T_IsSemiring_1238 → T_IsMonoid_358 Source #

d_isSemigroup_1302 ∷ T_IsSemiring_1238 → T_IsSemigroup_194 Source #

d_assoc_1304 ∷ T_IsSemiring_1238 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_1306 ∷ T_IsSemiring_1238 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_1308 ∷ T_IsSemiring_1238 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1314 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

d_'43''45'isCommutativeMonoid_1322 ∷ T_IsSemiring_1238 → T_IsCommutativeMonoid_406 Source #

d_isMagma_1326 ∷ T_IsSemiring_1238 → T_IsMagma_86 Source #

d_isMonoid_1328 ∷ T_IsSemiring_1238 → T_IsMonoid_358 Source #

d_isSemigroup_1330 ∷ T_IsSemiring_1238 → T_IsSemigroup_194 Source #

d_distrib_1332 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

d_isEquivalence_1338 ∷ T_IsSemiring_1238 → T_IsEquivalence_26 Source #

d_isNearSemiring_1340 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsSemiring_1238 → T_IsNearSemiring_876 Source #

du_isNearSemiring_1340 ∷ T_IsSemiring_1238 → T_IsNearSemiring_876 Source #

d_isSemiringWithoutAnnihilatingZero_1344 ∷ T_IsSemiring_1238 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

d_isSemiringWithoutOne_1346 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → Integer → T_IsSemiring_1238 → T_IsSemiringWithoutOne_952 Source #

d_zero_1358 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

d_assoc_1366 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → Integer → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_1368 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1374 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_Σ_14 Source #

d_isMagma_1380 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsMagma_86 Source #

d_'42''45'isMonoid_1382 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsMonoid_358 Source #

d_isSemigroup_1384 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsSemigroup_194 Source #

d_assoc_1386 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_1388 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_1390 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1396 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_Σ_14 Source #

d_'43''45'isCommutativeMonoid_1404 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsCommutativeMonoid_406 Source #

d_isMagma_1408 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsMagma_86 Source #

d_isMonoid_1410 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsMonoid_358 Source #

d_isSemigroup_1412 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsSemigroup_194 Source #

d_distrib_1414 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_Σ_14 Source #

d_isEquivalence_1420 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsEquivalence_26 Source #

d_assoc_1436 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsSemiringWithoutOne_952 → Integer → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_1438 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsSemiringWithoutOne_952 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_isMagma_1444 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsSemiringWithoutOne_952 → T_IsMagma_86 Source #

du_isMagma_1444 ∷ T_IsSemiringWithoutOne_952 → T_IsMagma_86 Source #

d_'42''45'isSemigroup_1446 ∷ T_IsSemiringWithoutOne_952 → T_IsSemigroup_194 Source #

d_assoc_1448 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsSemiringWithoutOne_952 → Integer → Integer → Integer → T__'8801'__12 Source #

d_comm_1450 ∷ T_IsSemiringWithoutOne_952 → Integer → Integer → T__'8801'__12 Source #

d_'8729''45'cong_1452 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsSemiringWithoutOne_952 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1458 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

du_identity_1458 ∷ T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

d_'43''45'isCommutativeMonoid_1466 ∷ T_IsSemiringWithoutOne_952 → T_IsCommutativeMonoid_406 Source #

d_isMagma_1470 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsSemiringWithoutOne_952 → T_IsMagma_86 Source #

du_isMagma_1470 ∷ T_IsSemiringWithoutOne_952 → T_IsMagma_86 Source #

d_isMonoid_1472 ∷ T_IsSemiringWithoutOne_952 → T_IsMonoid_358 Source #

d_isSemigroup_1474 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsSemiringWithoutOne_952 → T_IsSemigroup_194 Source #

du_isSemigroup_1474 ∷ T_IsSemiringWithoutOne_952 → T_IsSemigroup_194 Source #

d_distrib_1476 ∷ T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

d_distrib'691'_1478 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsSemiringWithoutOne_952 → Integer → Integer → Integer → T__'8801'__12 Source #

d_isEquivalence_1480 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsSemiringWithoutOne_952 → T_IsEquivalence_26 Source #

du_isEquivalence_1480 ∷ T_IsSemiringWithoutOne_952 → T_IsEquivalence_26 Source #

d_isNearSemiring_1482 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsSemiringWithoutOne_952 → T_IsNearSemiring_876 Source #

d_zero_1496 ∷ T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

d_Homomorphic'8320'_1504 ∷ (Integer → Integer) → Integer → Integer → () Source #

d_Homomorphic'8321'_1506 ∷ (Integer → Integer) → (Integer → Integer) → (Integer → Integer) → () Source #

d_Homomorphic'8322'_1508 ∷ (Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_Morphism_1510 ∷ () Source #

d_Homomorphic'8320'_1514 ∷ (Integer → Integer) → Integer → Integer → () Source #

d_Homomorphic'8321'_1516 ∷ (Integer → Integer) → (Integer → Integer) → (Integer → Integer) → () Source #

d_Homomorphic'8322'_1518 ∷ (Integer → Integer) → (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #

d_Morphism_1520 ∷ () Source #

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

d_'45''91'1'43''45'injective_1532 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'43''91'1'43''45'injective_1538 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d__'8799'__1540 ∷ Integer → Integer → T_Dec_32 Source #

d_'8801''45'setoid_1558 ∷ T_Setoid_44 Source #

d_'8801''45'decSetoid_1560 ∷ T_DecSetoid_84 Source #

d_drop'8255''43''8804''43'_1566 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__18 Source #

du_drop'8255''43''8804''43'_1566 ∷ T__'8804'__26 → T__'8804'__18 Source #

d_drop'8255''45''8804''45'_1574 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__18 Source #

du_drop'8255''45''8804''45'_1574 ∷ T__'8804'__26 → T__'8804'__18 Source #

d_'8804''45'reflexive_1578 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__26 Source #

du_'8804''45'reflexive_1578 ∷ Integer → T__'8804'__26 Source #

d_'8804''45'refl_1584 ∷ Integer → T__'8804'__26 Source #

d_'8804''45'trans_1586 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

du_'8804''45'trans_1586 ∷ T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

d_'8804''45'antisym_1600 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8801'__12 Source #

d_'8804''45'total_1610 ∷ Integer → Integer → T__'8846'__30 Source #

d__'8804''63'__1628 ∷ Integer → Integer → T_Dec_32 Source #

d_'8804''45'irrelevant_1646 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8801'__12 Source #

d_'8804''45'isPreorder_1656 ∷ T_IsPreorder_70 Source #

d_'8804''45'isTotalPreorder_1658 ∷ T_IsTotalPreorder_118 Source #

d_'8804''45'isPartialOrder_1660 ∷ T_IsPartialOrder_162 Source #

d_'8804''45'isTotalOrder_1662 ∷ T_IsTotalOrder_384 Source #

d_'8804''45'isDecTotalOrder_1664 ∷ T_IsDecTotalOrder_434 Source #

d_'8804''45'preorder_1666 ∷ T_Preorder_132 Source #

d_'8804''45'totalPreorder_1668 ∷ T_TotalPreorder_204 Source #

d_'8804''45'poset_1670 ∷ T_Poset_282 Source #

d_'8804''45'totalOrder_1672 ∷ T_TotalOrder_652 Source #

d_'8804''45'decTotalOrder_1674 ∷ T_DecTotalOrder_740 Source #

d_'8804''7495''8658''8804'_1680 ∷ Integer → Integer → AgdaAny → T__'8804'__26 Source #

du_'8804''7495''8658''8804'_1680 ∷ Integer → Integer → T__'8804'__26 Source #

d_'8804''8658''8804''7495'_1692 ∷ Integer → Integer → T__'8804'__26 → AgdaAny Source #

du_'8804''8658''8804''7495'_1692 ∷ T__'8804'__26 → AgdaAny Source #

d_drop'8255''43''60''43'_1702 ∷ Integer → Integer → T__'60'__50 → T__'8804'__18 Source #

du_drop'8255''43''60''43'_1702 ∷ T__'60'__50 → T__'8804'__18 Source #

d_drop'8255''45''60''45'_1710 ∷ Integer → Integer → T__'60'__50 → T__'8804'__18 Source #

du_drop'8255''45''60''45'_1710 ∷ T__'60'__50 → T__'8804'__18 Source #

d_'43''8814'0_1716 ∷ Integer → T__'60'__50 → T_'8869'_4 Source #

d_'43''8814''45'_1722 ∷ Integer → Integer → T__'60'__50 → T_'8869'_4 Source #

d_'60''8658''8804'_1724 ∷ Integer → Integer → T__'60'__50 → T__'8804'__26 Source #

d_'60''8658''8802'_1730 ∷ Integer → Integer → T__'60'__50 → T__'8801'__12 → T_'8869'_4 Source #

d_'60''8658''8817'_1736 ∷ Integer → Integer → T__'60'__50 → T__'8804'__26 → T_'8869'_4 Source #

d_'8804''8658''8815'_1742 ∷ Integer → Integer → T__'8804'__26 → T__'60'__50 → T_'8869'_4 Source #

d_'8816''8658''62'_1752 ∷ Integer → Integer → (T__'8804'__26 → T_'8869'_4) → T__'60'__50 Source #

du_'8816''8658''62'_1752 ∷ Integer → Integer → T__'60'__50 Source #

d_'8814''8658''8805'_1778 ∷ Integer → Integer → (T__'60'__50 → T_'8869'_4) → T__'8804'__26 Source #

du_'8814''8658''8805'_1778 ∷ Integer → Integer → T__'8804'__26 Source #

d_'62''8658''8816'_1804 ∷ Integer → Integer → T__'60'__50 → T__'8804'__26 → T_'8869'_4 Source #

d_'8804''8743''8802''8658''60'_1810 ∷ Integer → Integer → T__'8804'__26 → (T__'8801'__12 → T_'8869'_4) → T__'60'__50 Source #

du_'8804''8743''8802''8658''60'_1810 ∷ Integer → Integer → T__'8804'__26 → T__'60'__50 Source #

d_'8804''8743''8814''8658''8801'_1826 ∷ Integer → Integer → T__'8804'__26 → (T__'60'__50 → T_'8869'_4) → T__'8801'__12 Source #

d_'60''45'irrefl_1832 ∷ Integer → Integer → T__'8801'__12 → T__'60'__50 → T_'8869'_4 Source #

d_'60''45'asym_1838 ∷ Integer → Integer → T__'60'__50 → T__'60'__50 → T_'8869'_4 Source #

d_'8804''45''60''45'trans_1844 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'60'__50 → T__'60'__50 Source #

du_'8804''45''60''45'trans_1844 ∷ T__'8804'__26 → T__'60'__50 → T__'60'__50 Source #

d_'60''45''8804''45'trans_1858 ∷ Integer → Integer → Integer → T__'60'__50 → T__'8804'__26 → T__'60'__50 Source #

du_'60''45''8804''45'trans_1858 ∷ T__'60'__50 → T__'8804'__26 → T__'60'__50 Source #

d_'60''45'trans_1872 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 → T__'60'__50 Source #

du_'60''45'trans_1872 ∷ Integer → Integer → T__'60'__50 → T__'60'__50 → T__'60'__50 Source #

d_'60''45'cmp_1878 ∷ Integer → Integer → T_Tri_136 Source #

d__'60''63'__1968 ∷ Integer → Integer → T_Dec_32 Source #

d_'60''45'irrelevant_1986 ∷ Integer → Integer → T__'60'__50 → T__'60'__50 → T__'8801'__12 Source #

d_'60''45'isStrictPartialOrder_1996 ∷ T_IsStrictPartialOrder_266 Source #

d_'60''45'isStrictTotalOrder_2002 ∷ T_IsStrictTotalOrder_502 Source #

d_'60''45'strictPartialOrder_2004 ∷ T_StrictPartialOrder_472 Source #

d_'60''45'strictTotalOrder_2006 ∷ T_StrictTotalOrder_864 Source #

d_n'8814'n_2010 ∷ Integer → T__'60'__50 → T_'8869'_4 Source #

d_'62''45'irrefl_2014 ∷ Integer → Integer → T__'8801'__12 → T__'60'__50 → T_'8869'_4 Source #

d__IsRelatedTo__2020 ∷ p → p → () Source #

d__'8718'_2022 ∷ Integer → T__IsRelatedTo__70 Source #

d__'8801''10216''10217'__2024 ∷ T__IsRelatedTo__70 → T__IsRelatedTo__70 Source #

d_IsEquality_2026 ∷ p → p → p → () Source #

d_IsEquality'63'_2028 ∷ Integer → Integer → T__IsRelatedTo__70 → T_Dec_32 Source #

d_IsStrict_2030 ∷ p → p → p → () Source #

d_IsStrict'63'_2032 ∷ Integer → Integer → T__IsRelatedTo__70 → T_Dec_32 Source #

d_begin__2034 ∷ Integer → Integer → T__IsRelatedTo__70 → T__'8804'__26 Source #

d_begin'45'equality__2036 ∷ Integer → Integer → T__IsRelatedTo__70 → AgdaAny → T__'8801'__12 Source #

d_begin'45'strict__2038 ∷ Integer → Integer → T__IsRelatedTo__70 → AgdaAny → T__'60'__50 Source #

d_extractEquality_2042 ∷ Integer → Integer → T__IsRelatedTo__70 → T_IsEquality_126 → T__'8801'__12 Source #

d_extractStrict_2044 ∷ Integer → Integer → T__IsRelatedTo__70 → T_IsStrict_92 → T__'60'__50 Source #

d_step'45''60'_2052 ∷ Integer → Integer → Integer → T__IsRelatedTo__70 → T__'60'__50 → T__IsRelatedTo__70 Source #

d_step'45''8801'_2054 ∷ Integer → Integer → Integer → T__IsRelatedTo__70 → T__'8801'__12 → T__IsRelatedTo__70 Source #

du_step'45''8801'_2054 ∷ T__IsRelatedTo__70 → T__IsRelatedTo__70 Source #

d_step'45''8801''728'_2056 ∷ Integer → Integer → Integer → T__IsRelatedTo__70 → T__'8801'__12 → T__IsRelatedTo__70 Source #

du_step'45''8801''728'_2056 ∷ T__IsRelatedTo__70 → T__IsRelatedTo__70 Source #

d_step'45''8804'_2058 ∷ Integer → Integer → Integer → T__IsRelatedTo__70 → T__'8804'__26 → T__IsRelatedTo__70 Source #

d_positive'8315''185'_2080 ∷ Integer → AgdaAny → T__'60'__50 Source #

du_positive'8315''185'_2080 ∷ T__'60'__50 Source #

d_nonNegative'8315''185'_2086 ∷ Integer → AgdaAny → T__'8804'__26 Source #

du_nonNegative'8315''185'_2086 ∷ T__'8804'__26 Source #

d_negative'8315''185'_2092 ∷ Integer → AgdaAny → T__'60'__50 Source #

du_negative'8315''185'_2092 ∷ T__'60'__50 Source #

d_nonPositive'8315''185'_2098 ∷ Integer → AgdaAny → T__'8804'__26 Source #

du_nonPositive'8315''185'_2098 ∷ Integer → T__'8804'__26 Source #

d_negative'60'positive_2106 ∷ Integer → Integer → AgdaAny → AgdaAny → T__'60'__50 Source #

du_negative'60'positive_2106 ∷ Integer → T__'60'__50 Source #

d_neg'45'involutive_2114 ∷ Integer → T__'8801'__12 Source #

d_neg'45'injective_2124 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_neg'45''8804''45'pos_2140 ∷ Integer → Integer → T__'8804'__26 Source #

du_neg'45''8804''45'pos_2140 ∷ Integer → T__'8804'__26 Source #

d_neg'45'mono'45''60'_2144 ∷ Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_neg'45'cancel'45''60'_2162 ∷ Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_'8739'n'8739''8801'0'8658'n'8801'0_2188 ∷ Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8739''45'n'8739''8801''8739'n'8739'_2192 ∷ Integer → T__'8801'__12 Source #

d_0'8804'n'8658''43''8739'n'8739''8801'n_2200 ∷ Integer → T__'8804'__26 → T__'8801'__12 Source #

d_'43''8739'n'8739''8801'n'8658'0'8804'n_2206 ∷ Integer → T__'8801'__12 → T__'8804'__26 Source #

du_'43''8739'n'8739''8801'n'8658'0'8804'n_2206 ∷ T__'8804'__26 Source #

d_'43''8739'n'8739''8801'n'8846''43''8739'n'8739''8801''45'n_2212 ∷ Integer → T__'8846'__30 Source #

d_'8739'm'8861'n'8739''8804'm'8852'n_2222 ∷ Integer → Integer → T__'8804'__18 Source #

d_'8739'm'43'n'8739''8804''8739'm'8739''43''8739'n'8739'_2252 ∷ Integer → Integer → T__'8804'__18 Source #

d_'8739'm'45'n'8739''8804''8739'm'8739''43''8739'n'8739'_2290 ∷ Integer → Integer → T__'8804'__18 Source #

d_'9667''45'inverse_2304 ∷ Integer → T__'8801'__12 Source #

d_'9667''45'cong_2314 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'43''9667'n'8801''43'n_2330 ∷ Integer → T__'8801'__12 Source #

d_'45''9667'n'8801''45'n_2334 ∷ Integer → T__'8801'__12 Source #

d_sign'45''9667'_2340 ∷ T_Sign_6 → Integer → T__'8801'__12 Source #

d_abs'45''9667'_2346 ∷ T_Sign_6 → Integer → T__'8801'__12 Source #

d_sign'8345''9667''8739'n'8739''8801'n_2354 ∷ Integer → T__'8801'__12 Source #

d_sign'45'cong_2368 ∷ T_Sign_6 → T_Sign_6 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_abs'45'cong_2392 ∷ T_Sign_6 → T_Sign_6 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8739's'9667'm'8739''42''8739't'9667'n'8739''8801'm'42'n_2416 ∷ T_Sign_6 → T_Sign_6 → Integer → Integer → T__'8801'__12 Source #

d_'9667''45''8801'_2430 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'43''9667''45'mono'45''60'_2448 ∷ Integer → Integer → T__'8804'__18 → T__'60'__50 Source #

du_'43''9667''45'mono'45''60'_2448 ∷ Integer → T__'8804'__18 → T__'60'__50 Source #

d_'43''9667''45'cancel'45''60'_2464 ∷ Integer → Integer → T__'60'__50 → T__'8804'__18 Source #

du_'43''9667''45'cancel'45''60'_2464 ∷ Integer → T__'60'__50 → T__'8804'__18 Source #

d_neg'9667''45'cancel'45''60'_2482 ∷ Integer → Integer → T__'60'__50 → T__'8804'__18 Source #

du_neg'9667''45'cancel'45''60'_2482 ∷ Integer → T__'60'__50 → T__'8804'__18 Source #

d_'45''9667''60''43''9667'_2498 ∷ Integer → Integer → T__'60'__50 Source #

du_'45''9667''60''43''9667'_2498 ∷ Integer → T__'60'__50 Source #

d_'43''9667''8814''45''9667'_2510 ∷ Integer → Integer → T__'60'__50 → T_'8869'_4 Source #

d_n'8854'n'8801'0_2516 ∷ Integer → T__'8801'__12 Source #

d_'91'1'43'm'93''8854''91'1'43'n'93''8801'm'8854'n_2532 ∷ Integer → Integer → T__'8801'__12 Source #

d_'8854''45'swap_2554 ∷ Integer → Integer → T__'8801'__12 Source #

d_'8854''45''8805'_2572 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

d_'8854''45''8804'_2604 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

d_'8854''45''60'_2644 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

d_'8854''45''8816'_2650 ∷ Integer → Integer → (T__'8804'__18 → T_'8869'_4) → T__'8801'__12 Source #

d_'8739''8854''8739''45''60'_2656 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

d_'8739''8854''8739''45''8816'_2672 ∷ Integer → Integer → (T__'8804'__18 → T_'8869'_4) → T__'8801'__12 Source #

d_'45'm'43'n'8801'n'8854'm_2678 ∷ Integer → Integer → T__'8801'__12 Source #

d_m'45'n'8801'm'8854'n_2690 ∷ Integer → Integer → T__'8801'__12 Source #

d_'45''91'n'8854'm'93''8801''45'm'43'n_2704 ∷ Integer → Integer → T__'8801'__12 Source #

d_'8739'm'8854'n'8739''8801''8739'n'8854'm'8739'_2738 ∷ Integer → Integer → T__'8801'__12 Source #

d_'43''45'cancel'737''45''8854'_2754 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_m'8854'n'8804'm_2774 ∷ Integer → Integer → T__'8804'__26 Source #

d_m'8854'n'60'1'43'm_2792 ∷ Integer → Integer → T__'60'__50 Source #

d_m'8854'1'43'n'60'm_2802 ∷ Integer → Integer → T__'60'__50 Source #

d_'45'1'43'm'60'n'8854'm_2818 ∷ Integer → Integer → T__'60'__50 Source #

d_'45''91'1'43'm'93''8804'n'8854'm'43'1_2836 ∷ Integer → Integer → T__'8804'__26 Source #

d_'45'1'43'm'8804'n'8854'm_2852 ∷ Integer → Integer → T__'8804'__26 Source #

d_0'8854'm'8804''43'_2862 ∷ Integer → Integer → T__'8804'__26 Source #

du_0'8854'm'8804''43'_2862 ∷ Integer → T__'8804'__26 Source #

d_sign'45''8854''45''60'_2870 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

d_sign'45''8854''45''8816'_2886 ∷ Integer → Integer → (T__'8804'__18 → T_'8869'_4) → T__'8801'__12 Source #

d_'8854''45'mono'691''45''8805''45''8804'_2892 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__26 Source #

d_'8854''45'mono'737''45''8804'_2924 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__26 Source #

d_'8854''45'mono'691''45''62''45''60'_2954 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'60'__50 Source #

d_'8854''45'mono'737''45''60'_2982 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'60'__50 Source #

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

d_'43''45'identity'737'_3016 ∷ Integer → T__'8801'__12 Source #

d_'43''45'identity'691'_3018 ∷ Integer → T__'8801'__12 Source #

d_'43''45'identity_3020 ∷ T_Σ_14 Source #

d_distrib'737''45''8854''45''43''45'pos_3028 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_distrib'737''45''8854''45''43''45'neg_3048 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_distrib'691''45''8854''45''43''45'pos_3068 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_distrib'691''45''8854''45''43''45'neg_3088 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

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

d_'43''45'inverse'737'_3282 ∷ Integer → T__'8801'__12 Source #

d_'43''45'inverse'691'_3288 ∷ Integer → T__'8801'__12 Source #

d_'43''45'inverse_3290 ∷ T_Σ_14 Source #

d_'43''45'isMagma_3292 ∷ T_IsMagma_86 Source #

d_'43''45'isSemigroup_3294 ∷ T_IsSemigroup_194 Source #

d_'43''45'isCommutativeSemigroup_3296 ∷ T_IsCommutativeSemigroup_270 Source #

d_'43''45'0'45'isMonoid_3298 ∷ T_IsMonoid_358 Source #

d_'43''45'0'45'isCommutativeMonoid_3300 ∷ T_IsCommutativeMonoid_406 Source #

d_'43''45'0'45'isGroup_3302 ∷ T_IsGroup_580 Source #

d_'43''45'isAbelianGroup_3304 ∷ T_IsAbelianGroup_662 Source #

d_'43''45'magma_3306 ∷ T_Magma_36 Source #

d_'43''45'semigroup_3308 ∷ T_Semigroup_206 Source #

d_'43''45'commutativeSemigroup_3310 ∷ T_CommutativeSemigroup_332 Source #

d_'43''45'0'45'monoid_3312 ∷ T_Monoid_506 Source #

d_'43''45'0'45'commutativeMonoid_3314 ∷ T_CommutativeMonoid_582 Source #

d_'43''45'0'45'abelianGroup_3316 ∷ T_AbelianGroup_990 Source #

d_pos'45''43''45'commute_3318 ∷ Integer → Integer → T__'8801'__12 Source #

d_neg'45'distrib'45''43'_3330 ∷ Integer → Integer → T__'8801'__12 Source #

d_'9667''45'distrib'45''43'_3360 ∷ T_Sign_6 → Integer → Integer → T__'8801'__12 Source #

d_'43''45'pos'45'mono'691''45''8804'_3380 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'43''45'neg'45'mono'691''45''8804'_3396 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'43''45'mono'691''45''8804'_3412 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'43''45'mono'737''45''8804'_3422 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'43''45'mono'45''8804'_3440 ∷ Integer → Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

d_'8804''45'steps_3464 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_m'8804'm'43'n_3476 ∷ Integer → Integer → T__'8804'__26 Source #

d_n'8804'm'43'n_3490 ∷ Integer → Integer → T__'8804'__26 Source #

d_'43''45'mono'691''45''60'_3502 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_'43''45'mono'737''45''60'_3530 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_'43''45'mono'45''60'_3548 ∷ Integer → Integer → Integer → Integer → T__'60'__50 → T__'60'__50 → T__'60'__50 Source #

d_'43''45'mono'45''8804''45''60'_3566 ∷ Integer → Integer → Integer → Integer → T__'8804'__26 → T__'60'__50 → T__'60'__50 Source #

d_'43''45'mono'45''60''45''8804'_3578 ∷ Integer → Integer → Integer → Integer → T__'60'__50 → T__'8804'__26 → T__'60'__50 Source #

d_neg'45'minus'45'pos_3594 ∷ Integer → Integer → T__'8801'__12 Source #

d_'43''45'minus'45'telescope_3610 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'91''43'm'93''45''91''43'n'93''8801'm'8854'n_3632 ∷ Integer → Integer → T__'8801'__12 Source #

d_'8739'm'45'n'8739''8801''8739'n'45'm'8739'_3646 ∷ Integer → Integer → T__'8801'__12 Source #

d_m'8801'n'8658'm'45'n'8801'0_3680 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_m'45'n'8801'0'8658'm'8801'n_3688 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8804''45'steps'45'neg_3708 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

du_'8804''45'steps'45'neg_3708 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_neg'45'mono'45''8804'_3730 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

du_neg'45'mono'45''8804'_3730 ∷ Integer → T__'8804'__26 → T__'8804'__26 Source #

d_neg'45'cancel'45''8804'_3740 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_m'45'n'8804'm_3768 ∷ Integer → Integer → T__'8804'__26 Source #

d_m'8804'n'8658'm'45'n'8804'0_3778 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_m'45'n'8804'0'8658'm'8804'n_3808 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_m'8804'n'8658'0'8804'n'45'm_3824 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_0'8804'n'45'm'8658'm'8804'n_3840 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'8804''45'step_3856 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_n'8804'1'43'n_3860 ∷ Integer → T__'8804'__26 Source #

d_suc'45''43'_3868 ∷ Integer → Integer → T__'8801'__12 Source #

d_n'8802'1'43'n_3880 ∷ Integer → T__'8801'__12 → T_'8869'_4 Source #

d_1'45''91'1'43'n'93''8801''45'n_3886 ∷ Integer → T__'8801'__12 Source #

d_suc'45'mono_3890 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_suc'91'i'93''8804'j'8658'i'60'j_3908 ∷ Integer → Integer → T__'8804'__26 → T__'60'__50 Source #

d_i'60'j'8658'suc'91'i'93''8804'j_3932 ∷ Integer → Integer → T__'60'__50 → T__'8804'__26 Source #

d_suc'45'pred_3944 ∷ Integer → T__'8801'__12 Source #

d_pred'45'suc_3954 ∷ Integer → T__'8801'__12 Source #

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

d_pred'45''43'_3982 ∷ Integer → Integer → T__'8801'__12 Source #

d_neg'45'suc_3994 ∷ Integer → T__'8801'__12 Source #

d_minus'45'suc_4002 ∷ Integer → Integer → T__'8801'__12 Source #

d_m'8804'pred'91'n'93''8658'm'60'n_4016 ∷ Integer → Integer → T__'8804'__26 → T__'60'__50 Source #

du_m'8804'pred'91'n'93''8658'm'60'n_4016 ∷ Integer → T__'8804'__26 → T__'60'__50 Source #

d_m'60'n'8658'm'8804'pred'91'n'93'_4034 ∷ Integer → Integer → T__'60'__50 → T__'8804'__26 Source #

du_m'60'n'8658'm'8804'pred'91'n'93'_4034 ∷ Integer → T__'60'__50 → T__'8804'__26 Source #

d_'8804''45'step'45'neg_4050 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

du_'8804''45'step'45'neg_4050 ∷ T__'8804'__26 → T__'8804'__26 Source #

d_pred'45'mono_4056 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

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

d_'42''45'identity'737'_4098 ∷ Integer → T__'8801'__12 Source #

d_'42''45'identity'691'_4112 ∷ Integer → T__'8801'__12 Source #

d_'42''45'identity_4114 ∷ T_Σ_14 Source #

d_'42''45'zero'737'_4116 ∷ Integer → T__'8801'__12 Source #

d_'42''45'zero'691'_4120 ∷ Integer → T__'8801'__12 Source #

d_'42''45'zero_4122 ∷ T_Σ_14 Source #

d_lemma_4130 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

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

d_distrib'45'lemma_4218 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'691''45''43'_4294 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'737''45''43'_4584 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'45''43'_4586 ∷ T_Σ_14 Source #

d_'42''45'isMagma_4588 ∷ T_IsMagma_86 Source #

d_'42''45'isSemigroup_4590 ∷ T_IsSemigroup_194 Source #

d_'42''45'isCommutativeSemigroup_4592 ∷ T_IsCommutativeSemigroup_270 Source #

d_'42''45'1'45'isMonoid_4594 ∷ T_IsMonoid_358 Source #

d_'42''45'1'45'isCommutativeMonoid_4596 ∷ T_IsCommutativeMonoid_406 Source #

d_'43''45''42''45'isSemiring_4598 ∷ T_IsSemiring_1238 Source #

d_'43''45''42''45'isCommutativeSemiring_4600 ∷ T_IsCommutativeSemiring_1344 Source #

d_'43''45''42''45'isRing_4602 ∷ T_IsRing_1584 Source #

d_'43''45''42''45'isCommutativeRing_4604 ∷ T_IsCommutativeRing_1720 Source #

d_'42''45'magma_4606 ∷ T_Magma_36 Source #

d_'42''45'semigroup_4608 ∷ T_Semigroup_206 Source #

d_'42''45'commutativeSemigroup_4610 ∷ T_CommutativeSemigroup_332 Source #

d_'42''45'1'45'monoid_4612 ∷ T_Monoid_506 Source #

d_'42''45'1'45'commutativeMonoid_4614 ∷ T_CommutativeMonoid_582 Source #

d_'43''45''42''45'semiring_4616 ∷ T_Semiring_1932 Source #

d_'43''45''42''45'commutativeSemiring_4618 ∷ T_CommutativeSemiring_2094 Source #

d_'43''45''42''45'ring_4620 ∷ T_Ring_2514 Source #

d_'43''45''42''45'commutativeRing_4622 ∷ T_CommutativeRing_2704 Source #

d_abs'45''42''45'commute_4624 ∷ Integer → Integer → T__'8801'__12 Source #

d_'42''45'cancel'691''45''8801'_4636 ∷ Integer → Integer → Integer → (T__'8801'__12 → T_'8869'_4) → T__'8801'__12 → T__'8801'__12 Source #

d_sign'45'i'8801'sign'45'j_4698 ∷ T_Sign_6 → Integer → Integer → Integer → (T__'8801'__12 → T_'8869'_4) → T__'8801'__12 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'42''45'cancel'737''45''8801'_4810 ∷ Integer → Integer → Integer → (T__'8801'__12 → T_'8869'_4) → T__'8801'__12 → T__'8801'__12 Source #

d_suc'45''42'_4830 ∷ Integer → Integer → T__'8801'__12 Source #

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

d_'45'1'42'n'8801''45'n_4860 ∷ Integer → T__'8801'__12 Source #

d_m'42'n'8801'0'8658'm'8801'0'8744'n'8801'0_4872 ∷ Integer → Integer → T__'8801'__12 → T__'8846'__30 Source #

du_m'42'n'8801'0'8658'm'8801'0'8744'n'8801'0_4872 ∷ Integer → T__'8846'__30 Source #

d_pos'45'distrib'45''42'_4898 ∷ Integer → Integer → T__'8801'__12 Source #

d_neg'45'distrib'737''45''42'_4912 ∷ Integer → Integer → T__'8801'__12 Source #

d_neg'45'distrib'691''45''42'_4928 ∷ Integer → Integer → T__'8801'__12 Source #

d_'9667''45'distrib'45''42'_4946 ∷ T_Sign_6 → T_Sign_6 → Integer → Integer → T__'8801'__12 Source #

d_'42''45'cancel'691''45''8804''45'pos_4978 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

du_'42''45'cancel'691''45''8804''45'pos_4978 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'42''45'cancel'737''45''8804''45'pos_5002 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

du_'42''45'cancel'737''45''8804''45'pos_5002 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'42''45'mono'691''45''8804''45'pos_5022 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'42''45'mono'691''45''8804''45'nonNeg_5044 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'42''45'mono'737''45''8804''45'nonNeg_5066 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'42''45'mono'737''45''8804''45'pos_5088 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'42''45'cancel'737''45''8804''45'neg_5098 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'42''45'cancel'691''45''8804''45'neg_5118 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'42''45'mono'737''45''8804''45'nonPos_5136 ∷ Integer → AgdaAny → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

du_'42''45'mono'737''45''8804''45'nonPos_5136 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'42''45'mono'691''45''8804''45'nonPos_5164 ∷ Integer → AgdaAny → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

du_'42''45'mono'691''45''8804''45'nonPos_5164 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'42''45'mono'737''45''8804''45'neg_5184 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'42''45'mono'691''45''8804''45'neg_5192 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'42''45'mono'737''45''60''45'pos_5200 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_'42''45'mono'691''45''60''45'pos_5230 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_'42''45'cancel'737''45''60''45'nonNeg_5252 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_'42''45'cancel'691''45''60''45'nonNeg_5292 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_'42''45'mono'737''45''60''45'neg_5312 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_'42''45'mono'691''45''60''45'neg_5330 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_'42''45'cancel'737''45''60''45'neg_5350 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_'42''45'cancel'737''45''60''45'nonPos_5370 ∷ Integer → Integer → Integer → AgdaAny → T__'60'__50 → T__'60'__50 Source #

du_'42''45'cancel'737''45''60''45'nonPos_5370 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_'42''45'cancel'691''45''60''45'neg_5394 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_'42''45'cancel'691''45''60''45'nonPos_5414 ∷ Integer → Integer → Integer → AgdaAny → T__'60'__50 → T__'60'__50 Source #

du_'42''45'cancel'691''45''60''45'nonPos_5414 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_'8739'm'42'n'8739''8801''8739'm'8739''42''8739'n'8739'_5442 ∷ Integer → Integer → T__'8801'__12 Source #

d_i'8804'j'8658'i'8851'j'8801'i_5480 ∷ Integer → Integer → T__'8804'__26 → T__'8801'__12 Source #

d_i'8805'j'8658'i'8851'j'8801'j_5490 ∷ Integer → Integer → T__'8804'__26 → T__'8801'__12 Source #

d_i'8804'j'8658'i'8852'j'8801'j_5500 ∷ Integer → Integer → T__'8804'__26 → T__'8801'__12 Source #

d_i'8805'j'8658'i'8852'j'8801'i_5510 ∷ Integer → Integer → T__'8804'__26 → T__'8801'__12 Source #

d_'8851''45'operator_5516 ∷ T_MinOperator_84 Source #

d_'8852''45'operator_5518 ∷ T_MaxOperator_114 Source #

d_antimono'45''8804''45'distrib'45''8851'_5522 ∷ (Integer → Integer) → (Integer → Integer → T__'8801'__12 → T__'8801'__12) → (Integer → Integer → T__'8804'__26 → T__'8804'__26) → Integer → Integer → T__'8801'__12 Source #

d_antimono'45''8804''45'distrib'45''8852'_5524 ∷ (Integer → Integer) → (Integer → Integer → T__'8801'__12 → T__'8801'__12) → (Integer → Integer → T__'8804'__26 → T__'8804'__26) → Integer → Integer → T__'8801'__12 Source #

d_mono'45''8804''45'distrib'45''8851'_5526 ∷ (Integer → Integer) → (Integer → Integer → T__'8801'__12 → T__'8801'__12) → (Integer → Integer → T__'8804'__26 → T__'8804'__26) → Integer → Integer → T__'8801'__12 Source #

d_mono'45''8804''45'distrib'45''8852'_5528 ∷ (Integer → Integer) → (Integer → Integer → T__'8801'__12 → T__'8801'__12) → (Integer → Integer → T__'8804'__26 → T__'8804'__26) → Integer → Integer → T__'8801'__12 Source #

d_x'8851'y'8804'x_5530 ∷ Integer → Integer → T__'8804'__26 Source #

d_x'8804'y'8658'x'8851'z'8804'y_5532 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_x'8804'y'8658'z'8851'x'8804'y_5534 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_x'8804'y'8658'x'8851'z'8804'y_5536 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_x'8804'y'8658'z'8851'x'8804'y_5538 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_x'8804'y'8851'z'8658'x'8804'y_5540 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_x'8804'y'8851'z'8658'x'8804'z_5542 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_x'8851'y'8804'y_5544 ∷ Integer → Integer → T__'8804'__26 Source #

d_x'8851'y'8776'x'8658'x'8804'y_5546 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__26 Source #

d_x'8851'y'8776'y'8658'y'8804'x_5548 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__26 Source #

d_x'8851'y'8804'x_5550 ∷ Integer → Integer → T__'8804'__26 Source #

d_x'8851'y'8804'x'8852'y_5552 ∷ Integer → Integer → T__'8804'__26 Source #

d_x'8851'y'8804'y_5554 ∷ Integer → Integer → T__'8804'__26 Source #

d_x'8851'y'8776'x'8658'x'8804'y_5556 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__26 Source #

d_x'8851'y'8776'y'8658'y'8804'x_5558 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__26 Source #

d_x'8804'y'8851'z'8658'x'8804'y_5560 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_x'8804'y'8851'z'8658'x'8804'z_5562 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'8851''45'absorbs'45''8852'_5564 ∷ Integer → Integer → T__'8801'__12 Source #

d_'8851''45'assoc_5566 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'8851''45'band_5568 ∷ T_Band_266 Source #

d_'8851''45'comm_5570 ∷ Integer → Integer → T__'8801'__12 Source #

d_'8851''45'commutativeSemigroup_5572 ∷ T_CommutativeSemigroup_332 Source #

d_'8851''45'distrib'45''8852'_5580 ∷ T_Σ_14 Source #

d_'8851''45'distrib'691''45''8852'_5582 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'8851''45'distrib'737''45''8852'_5584 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'8851''45'glb_5586 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

d_'8851''45'idem_5588 ∷ Integer → T__'8801'__12 Source #

d_'8851''45'isBand_5596 ∷ T_IsBand_230 Source #

d_'8851''45'isCommutativeSemigroup_5598 ∷ T_IsCommutativeSemigroup_270 Source #

d_'8851''45'isMagma_5600 ∷ T_IsMagma_86 Source #

d_'8851''45'isSelectiveMagma_5604 ∷ T_IsSelectiveMagma_158 Source #

d_'8851''45'isSemigroup_5606 ∷ T_IsSemigroup_194 Source #

d_'8851''45'isSemilattice_5608 ∷ T_IsSemilattice_312 Source #

d_'8851''45'magma_5610 ∷ T_Magma_36 Source #

d_'8851''45'mono'45''8804'_5612 ∷ Integer → Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

d_'8851''45'mono'691''45''8804'_5616 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'8851''45'mono'737''45''8804'_5618 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'8851''45'sel_5622 ∷ Integer → Integer → T__'8846'__30 Source #

d_'8851''45'selectiveMagma_5624 ∷ T_SelectiveMagma_90 Source #

d_'8851''45'semigroup_5626 ∷ T_Semigroup_206 Source #

d_'8851''45'semilattice_5628 ∷ T_Semilattice_402 Source #

d_'8851''45'triangulate_5630 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'8851''45''8852''45'absorptive_5638 ∷ T_Σ_14 Source #

d_'8851''45''8852''45'distributiveLattice_5640 ∷ T_DistributiveLattice_1228 Source #

d_'8851''45''8852''45'isDistributiveLattice_5642 ∷ T_IsDistributiveLattice_814 Source #

d_'8851''45''8852''45'isLattice_5644 ∷ T_IsLattice_740 Source #

d_'8851''45''8852''45'lattice_5646 ∷ T_Lattice_1144 Source #

d_'8852''45'absorbs'45''8851'_5648 ∷ Integer → Integer → T__'8801'__12 Source #

d_'8851''45'assoc_5650 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'8851''45'band_5652 ∷ T_Band_266 Source #

d_'8851''45'comm_5654 ∷ Integer → Integer → T__'8801'__12 Source #

d_'8851''45'commutativeSemigroup_5656 ∷ T_CommutativeSemigroup_332 Source #

d_'8852''45'distrib'45''8851'_5664 ∷ T_Σ_14 Source #

d_'8852''45'distrib'691''45''8851'_5666 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'8852''45'distrib'737''45''8851'_5668 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'8851''45'idem_5670 ∷ Integer → T__'8801'__12 Source #

d_'8851''45'isBand_5678 ∷ T_IsBand_230 Source #

d_'8851''45'isCommutativeSemigroup_5680 ∷ T_IsCommutativeSemigroup_270 Source #

d_'8851''45'isMagma_5682 ∷ T_IsMagma_86 Source #

d_'8851''45'isSelectiveMagma_5686 ∷ T_IsSelectiveMagma_158 Source #

d_'8851''45'isSemigroup_5688 ∷ T_IsSemigroup_194 Source #

d_'8851''45'isSemilattice_5690 ∷ T_IsSemilattice_312 Source #

d_'8851''45'glb_5692 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

d_'8851''45'magma_5694 ∷ T_Magma_36 Source #

d_'8851''45'mono'45''8804'_5696 ∷ Integer → Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

d_'8851''45'mono'691''45''8804'_5700 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'8851''45'mono'737''45''8804'_5702 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'8851''45'sel_5704 ∷ Integer → Integer → T__'8846'__30 Source #

d_'8851''45'selectiveMagma_5706 ∷ T_SelectiveMagma_90 Source #

d_'8851''45'semigroup_5708 ∷ T_Semigroup_206 Source #

d_'8851''45'semilattice_5710 ∷ T_Semilattice_402 Source #

d_'8851''45'triangulate_5712 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'8852''45''8851''45'absorptive_5720 ∷ T_Σ_14 Source #

d_'8852''45''8851''45'distributiveLattice_5722 ∷ T_DistributiveLattice_1228 Source #

d_'8852''45''8851''45'isDistributiveLattice_5724 ∷ T_IsDistributiveLattice_814 Source #

d_'8852''45''8851''45'isLattice_5726 ∷ T_IsLattice_740 Source #

d_'8852''45''8851''45'lattice_5728 ∷ T_Lattice_1144 Source #

d_mono'45''8804''45'distrib'45''8852'_5736 ∷ (Integer → Integer) → (Integer → Integer → T__'8804'__26 → T__'8804'__26) → Integer → Integer → T__'8801'__12 Source #

d_mono'45''8804''45'distrib'45''8851'_5746 ∷ (Integer → Integer) → (Integer → Integer → T__'8804'__26 → T__'8804'__26) → Integer → Integer → T__'8801'__12 Source #

d_antimono'45''8804''45'distrib'45''8851'_5756 ∷ (Integer → Integer) → (Integer → Integer → T__'8804'__26 → T__'8804'__26) → Integer → Integer → T__'8801'__12 Source #

d_antimono'45''8804''45'distrib'45''8852'_5766 ∷ (Integer → Integer) → (Integer → Integer → T__'8804'__26 → T__'8804'__26) → Integer → Integer → T__'8801'__12 Source #

d_mono'45''60''45'distrib'45''8851'_5776 ∷ (Integer → Integer) → (Integer → Integer → T__'60'__50 → T__'60'__50) → Integer → Integer → T__'8801'__12 Source #

d_mono'45''60''45'distrib'45''8852'_5824 ∷ (Integer → Integer) → (Integer → Integer → T__'60'__50 → T__'60'__50) → Integer → Integer → T__'8801'__12 Source #

d_antimono'45''60''45'distrib'45''8852'_5872 ∷ (Integer → Integer) → (Integer → Integer → T__'60'__50 → T__'60'__50) → Integer → Integer → T__'8801'__12 Source #

d_antimono'45''60''45'distrib'45''8851'_5920 ∷ (Integer → Integer) → (Integer → Integer → T__'60'__50 → T__'60'__50) → Integer → Integer → T__'8801'__12 Source #

d_neg'45'distrib'45''8852''45''8851'_5966 ∷ Integer → Integer → T__'8801'__12 Source #

d_neg'45'distrib'45''8851''45''8852'_5972 ∷ Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'737''45''8851''45'nonNeg_5980 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'691''45''8851''45'nonNeg_5990 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'737''45''8851''45'nonPos_6008 ∷ Integer → AgdaAny → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'691''45''8851''45'nonPos_6026 ∷ Integer → AgdaAny → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'737''45''8852''45'nonNeg_6046 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'691''45''8852''45'nonNeg_6060 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'737''45''8852''45'nonPos_6078 ∷ Integer → AgdaAny → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'691''45''8852''45'nonPos_6096 ∷ Integer → AgdaAny → Integer → Integer → T__'8801'__12 Source #

d_inverse'737'_6110 ∷ Integer → T__'8801'__12 Source #

d_inverse'691'_6112 ∷ Integer → T__'8801'__12 Source #

d_distrib'691'_6114 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_isCommutativeSemiring_6116 ∷ T_IsCommutativeSemiring_1344 Source #

d_commutativeRing_6118 ∷ T_CommutativeRing_2704 Source #

d_'42''45''43''45'right'45'mono_6120 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_cancel'45''42''45''43''45'right'45''8804'_6122 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_cancel'45''42''45'right_6124 ∷ Integer → Integer → Integer → (T__'8801'__12 → T_'8869'_4) → T__'8801'__12 → T__'8801'__12 Source #

d_doubleNeg_6126 ∷ Integer → T__'8801'__12 Source #

d_'45''8255'involutive_6128 ∷ Integer → T__'8801'__12 Source #

d_'43''45''8854''45'left'45'cancel_6130 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'8816''8594''62'_6132 ∷ Integer → Integer → (T__'8804'__26 → T_'8869'_4) → T__'60'__50 Source #

d_'8804''45'irrelevance_6134 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8801'__12 Source #

d_'60''45'irrelevance_6136 ∷ Integer → Integer → T__'60'__50 → T__'60'__50 → T__'8801'__12 Source #

d_'45''60''8242''43'_6142 ∷ Integer → Integer → T__'8804'__26 Source #

du_'45''60''8242''43'_6142 ∷ Integer → T__'8804'__26 Source #

d_'60''8242''45'irrefl_6144 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__26 → T_'8869'_4 Source #

d_'62''8242''45'irrefl_6154 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__26 → T_'8869'_4 Source #

d_'60''8242''45'asym_6156 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 → T_'8869'_4 Source #

d_'8804''45''60''8242''45'trans_6174 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

du_'8804''45''60''8242''45'trans_6174 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

d_'60''8242''45''8804''45'trans_6202 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

du_'60''8242''45''8804''45'trans_6202 ∷ T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

d_'60''8242''8658''8804'_6208 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

du_'60''8242''8658''8804'_6208 ∷ Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'60''8242''45'trans_6212 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

du_'60''8242''45'trans_6212 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

d_'60''8242''45'cmp_6224 ∷ Integer → Integer → T_Tri_136 Source #

d_'60''8242''45'isStrictPartialOrder_6318 ∷ T_IsStrictPartialOrder_266 Source #

d_'60''8242''45'strictPartialOrder_6328 ∷ T_StrictPartialOrder_472 Source #

d_'60''8242''45'isStrictTotalOrder_6330 ∷ T_IsStrictTotalOrder_502 Source #

d_'60''8242''45'strictTotalOrder_6334 ∷ T_StrictTotalOrder_864 Source #

d_n'8814''8242'n_6338 ∷ Integer → T__'8804'__26 → T_'8869'_4 Source #

d_'62''8242''8658''8816''8242'_6352 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 → T_'8869'_4 Source #

d_'8816''8658''62''8242'_6364 ∷ Integer → Integer → (T__'8804'__26 → T_'8869'_4) → T__'8804'__26 Source #

du_'8816''8658''62''8242'_6364 ∷ Integer → Integer → T__'8804'__26 Source #

d_'60''8242''45'irrelevant_6410 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8801'__12 Source #

d_'43''45'mono'737''45''60''8242'_6416 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'43''45'mono'691''45''60''8242'_6432 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'43''45'mono'45''60''8242'_6450 ∷ Integer → Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

d_'43''45'mono'45''8804''45''60''8242'_6468 ∷ Integer → Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

d_'43''45'mono'45''60''8242''45''8804'_6482 ∷ Integer → Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 → T__'8804'__26 Source #

d_m'8804'pred'91'n'93''8658'm'60''8242'n_6500 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_m'60''8242'n'8658'm'8804'pred'91'n'93'_6518 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'91'1'43'm'93''42'n'8801'n'43'm'42'n_6530 ∷ Integer → Integer → T__'8801'__12 Source #

d_neg'45'mono'45''60''45''62'_6532 ∷ Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_neg'45'mono'45''8804''45''8805'_6534 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'42''45'mono'691''45''8804''45'non'45'neg_6536 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'42''45'mono'737''45''8804''45'non'45'neg_6538 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_'42''45'cancel'737''45''60''45'non'45'neg_6540 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_'42''45'cancel'691''45''60''45'non'45'neg_6542 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

d_m'8804'n'8658'm'8851'n'8801'm_6544 ∷ Integer → Integer → T__'8804'__26 → T__'8801'__12 Source #

d_m'8851'n'8801'm'8658'm'8804'n_6546 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__26 Source #

d_m'8805'n'8658'm'8851'n'8801'n_6548 ∷ Integer → Integer → T__'8804'__26 → T__'8801'__12 Source #

d_m'8851'n'8801'n'8658'm'8805'n_6550 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__26 Source #

d_m'8851'n'8804'n_6552 ∷ Integer → Integer → T__'8804'__26 Source #

d_m'8851'n'8804'm_6554 ∷ Integer → Integer → T__'8804'__26 Source #

d_m'8804'n'8658'm'8852'n'8801'n_6556 ∷ Integer → Integer → T__'8804'__26 → T__'8801'__12 Source #

d_m'8852'n'8801'n'8658'm'8804'n_6558 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__26 Source #

d_m'8805'n'8658'm'8852'n'8801'm_6560 ∷ Integer → Integer → T__'8804'__26 → T__'8801'__12 Source #

d_m'8852'n'8801'm'8658'm'8805'n_6562 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__26 Source #

d_m'8804'm'8852'n_6564 ∷ Integer → Integer → T__'8804'__26 Source #

d_n'8804'm'8852'n_6566 ∷ Integer → Integer → T__'8804'__26 Source #