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

d_Identity_40 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_LeftIdentity_52 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_LeftZero_56 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_RightIdentity_62 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_RightZero_66 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_Zero_70 ∷ Integer → (Integer → Integer → Integer) → () Source #

d_IsAbelianGroup_74 ∷ p → p → p → () Source #

d_IsBand_76 ∷ p → () Source #

d_IsCancellativeCommutativeSemiring_82 ∷ p → p → p → p → () Source #

d_IsCommutativeMagma_84 ∷ p → () Source #

d_IsCommutativeMonoid_86 ∷ p → p → () Source #

d_IsCommutativeRing_88 ∷ p → p → p → p → p → () Source #

d_IsCommutativeSemigroup_90 ∷ p → () Source #

d_IsCommutativeSemiring_92 ∷ p → p → p → p → () Source #

d_IsCommutativeSemiringWithoutOne_94 ∷ p → p → p → () Source #

d_IsGroup_98 ∷ p → p → p → () Source #

d_IsIdempotentCommutativeMonoid_100 ∷ p → p → () Source #

d_IsMagma_104 ∷ p → () Source #

d_IsMonoid_106 ∷ p → p → () Source #

d_IsNearSemiring_108 ∷ p → p → p → () Source #

d_IsRing_110 ∷ p → p → p → p → p → () Source #

d_IsSelectiveMagma_112 ∷ p → () Source #

d_IsSemigroup_114 ∷ p → () Source #

d_IsSemilattice_116 ∷ p → () Source #

d_IsSemiring_118 ∷ p → p → p → p → () Source #

d_IsSemiringWithoutAnnihilatingZero_120 ∷ p → p → p → p → () Source #

d_IsSemiringWithoutOne_122 ∷ p → p → p → () Source #

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

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

d_identity_132 ∷ T_IsAbelianGroup_662 → T_Σ_14 Source #

d_inverse_138 ∷ T_IsAbelianGroup_662 → T_Σ_14 Source #

d_isEquivalence_150 ∷ T_IsAbelianGroup_662 → T_IsEquivalence_26 Source #

d_isGroup_152 ∷ T_IsAbelianGroup_662 → T_IsGroup_580 Source #

d_isMagma_154 ∷ T_IsAbelianGroup_662 → T_IsMagma_86 Source #

d_isMonoid_156 ∷ T_IsAbelianGroup_662 → T_IsMonoid_358 Source #

d_isSemigroup_160 ∷ T_IsAbelianGroup_662 → T_IsSemigroup_194 Source #

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

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

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

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

d_isEquivalence_190 ∷ T_IsBand_230 → T_IsEquivalence_26 Source #

d_isMagma_192 ∷ T_IsBand_230 → T_IsMagma_86 Source #

d_isSemigroup_196 ∷ T_IsBand_230 → T_IsSemigroup_194 Source #

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

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

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

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

d_identity_276 ∷ T_IsIdempotentCommutativeMonoid_464 → T_Σ_14 Source #

d_isCommutativeMonoid_284 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeMonoid_406 Source #

d_isEquivalence_288 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsEquivalence_26 Source #

d_isMagma_290 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMagma_86 Source #

d_isMonoid_292 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMonoid_358 Source #

d_isSemigroup_296 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsSemigroup_194 Source #

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

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

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

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

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

d_identity_328 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

d_isMagma_340 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsMagma_86 Source #

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

d_isSemigroup_344 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemigroup_194 Source #

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

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

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

d_identity_356 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

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

d_isMagma_368 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsMagma_86 Source #

d_isMonoid_370 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsMonoid_358 Source #

d_isSemigroup_372 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemigroup_194 Source #

d_distrib_374 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

d_isCommutativeSemiring_380 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeSemiring_1344 Source #

d_isEquivalence_384 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsEquivalence_26 Source #

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

du_isNearSemiring_386 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsNearSemiring_876 Source #

d_isSemiring_390 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemiring_1238 Source #

d_isSemiringWithoutAnnihilatingZero_392 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

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

du_isSemiringWithoutOne_394 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemiringWithoutOne_952 Source #

d_zero_406 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

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

d_isEquivalence_416 ∷ T_IsCommutativeMagma_122 → T_IsEquivalence_26 Source #

d_isMagma_418 ∷ T_IsCommutativeMagma_122 → T_IsMagma_86 Source #

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

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

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

d_identity_444 ∷ T_IsCommutativeMonoid_406 → T_Σ_14 Source #

d_isEquivalence_454 ∷ T_IsCommutativeMonoid_406 → T_IsEquivalence_26 Source #

d_isMagma_456 ∷ T_IsCommutativeMonoid_406 → T_IsMagma_86 Source #

d_isMonoid_458 ∷ T_IsCommutativeMonoid_406 → T_IsMonoid_358 Source #

d_isSemigroup_462 ∷ T_IsCommutativeMonoid_406 → T_IsSemigroup_194 Source #

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

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

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

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

d_identity_494 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_isMagma_506 ∷ T_IsCommutativeRing_1720 → T_IsMagma_86 Source #

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

d_isSemigroup_510 ∷ T_IsCommutativeRing_1720 → T_IsSemigroup_194 Source #

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

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

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

d_identity_522 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

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

d_isGroup_536 ∷ T_IsCommutativeRing_1720 → T_IsGroup_580 Source #

d_isMagma_538 ∷ T_IsCommutativeRing_1720 → T_IsMagma_86 Source #

d_isMonoid_540 ∷ T_IsCommutativeRing_1720 → T_IsMonoid_358 Source #

d_isSemigroup_542 ∷ T_IsCommutativeRing_1720 → T_IsSemigroup_194 Source #

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

d_inverse_546 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_distrib_552 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_isEquivalence_562 ∷ T_IsCommutativeRing_1720 → T_IsEquivalence_26 Source #

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

du_isNearSemiring_564 ∷ T_IsCommutativeRing_1720 → T_IsNearSemiring_876 Source #

d_isRing_568 ∷ T_IsCommutativeRing_1720 → T_IsRing_1584 Source #

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

du_isSemiring_570 ∷ T_IsCommutativeRing_1720 → T_IsSemiring_1238 Source #

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

du_isSemiringWithoutOne_574 ∷ T_IsCommutativeRing_1720 → T_IsSemiringWithoutOne_952 Source #

d_zero_590 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

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

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

d_isEquivalence_604 ∷ T_IsCommutativeSemigroup_270 → T_IsEquivalence_26 Source #

d_isMagma_606 ∷ T_IsCommutativeSemigroup_270 → T_IsMagma_86 Source #

d_isSemigroup_610 ∷ T_IsCommutativeSemigroup_270 → T_IsSemigroup_194 Source #

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

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

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

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

d_identity_640 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

d_isMagma_652 ∷ T_IsCommutativeSemiring_1344 → T_IsMagma_86 Source #

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

d_isSemigroup_656 ∷ T_IsCommutativeSemiring_1344 → T_IsSemigroup_194 Source #

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

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

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

d_identity_668 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

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

d_isMagma_680 ∷ T_IsCommutativeSemiring_1344 → T_IsMagma_86 Source #

d_isMonoid_682 ∷ T_IsCommutativeSemiring_1344 → T_IsMonoid_358 Source #

d_isSemigroup_684 ∷ T_IsCommutativeSemiring_1344 → T_IsSemigroup_194 Source #

d_distrib_686 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

d_isEquivalence_694 ∷ T_IsCommutativeSemiring_1344 → T_IsEquivalence_26 Source #

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

du_isNearSemiring_696 ∷ T_IsCommutativeSemiring_1344 → T_IsNearSemiring_876 Source #

d_isSemiring_700 ∷ T_IsCommutativeSemiring_1344 → T_IsSemiring_1238 Source #

d_isSemiringWithoutAnnihilatingZero_702 ∷ T_IsCommutativeSemiring_1344 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

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

du_isSemiringWithoutOne_704 ∷ T_IsCommutativeSemiring_1344 → T_IsSemiringWithoutOne_952 Source #

d_zero_716 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

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

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

d_'8729''45'cong_728 ∷ (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_738 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1044 → T_IsMagma_86 Source #

du_isMagma_738 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsMagma_86 Source #

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

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

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

d_'8729''45'cong_746 ∷ (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_752 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

du_identity_752 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

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

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

du_isMagma_764 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsMagma_86 Source #

d_isMonoid_766 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsMonoid_358 Source #

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

du_isSemigroup_768 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsSemigroup_194 Source #

d_distrib_770 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

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

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

du_isEquivalence_774 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsEquivalence_26 Source #

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

du_isNearSemiring_776 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsNearSemiring_876 Source #

d_isSemiringWithoutOne_780 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsSemiringWithoutOne_952 Source #

d_zero_792 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

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

d_identity_850 ∷ T_IsGroup_580 → T_Σ_14 Source #

d_inverse_856 ∷ T_IsGroup_580 → T_Σ_14 Source #

d_isEquivalence_862 ∷ T_IsGroup_580 → T_IsEquivalence_26 Source #

d_isMagma_864 ∷ T_IsGroup_580 → T_IsMagma_86 Source #

d_isMonoid_866 ∷ T_IsGroup_580 → T_IsMonoid_358 Source #

d_isSemigroup_870 ∷ T_IsGroup_580 → T_IsSemigroup_194 Source #

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

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

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

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

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

d_identity_902 ∷ T_IsIdempotentCommutativeMonoid_464 → T_Σ_14 Source #

d_isCommutativeMonoid_910 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeMonoid_406 Source #

d_isEquivalence_914 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsEquivalence_26 Source #

d_isMagma_916 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMagma_86 Source #

d_isMonoid_918 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMonoid_358 Source #

d_isSemigroup_922 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsSemigroup_194 Source #

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

d_isEquivalence_982 ∷ T_IsMagma_86 → T_IsEquivalence_26 Source #

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

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

d_identity_1006 ∷ T_IsMonoid_358 → T_Σ_14 Source #

d_isEquivalence_1012 ∷ T_IsMonoid_358 → T_IsEquivalence_26 Source #

d_isMagma_1014 ∷ T_IsMonoid_358 → T_IsMagma_86 Source #

d_isSemigroup_1018 ∷ T_IsMonoid_358 → T_IsSemigroup_194 Source #

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

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

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

d_isMagma_1046 ∷ T_IsNearSemiring_876 → T_IsMagma_86 Source #

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

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

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

d_identity_1058 ∷ T_IsNearSemiring_876 → T_Σ_14 Source #

d_isMagma_1064 ∷ T_IsNearSemiring_876 → T_IsMagma_86 Source #

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

d_isSemigroup_1068 ∷ T_IsNearSemiring_876 → T_IsSemigroup_194 Source #

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

d_isEquivalence_1072 ∷ T_IsNearSemiring_876 → T_IsEquivalence_26 Source #

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

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

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

d_identity_1100 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_isMagma_1106 ∷ T_IsRing_1584 → T_IsMagma_86 Source #

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

d_isSemigroup_1110 ∷ T_IsRing_1584 → T_IsSemigroup_194 Source #

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

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

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

d_identity_1122 ∷ T_IsRing_1584 → T_Σ_14 Source #

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

d_isGroup_1136 ∷ T_IsRing_1584 → T_IsGroup_580 Source #

d_isMagma_1138 ∷ T_IsRing_1584 → T_IsMagma_86 Source #

d_isMonoid_1140 ∷ T_IsRing_1584 → T_IsMonoid_358 Source #

d_isSemigroup_1142 ∷ T_IsRing_1584 → T_IsSemigroup_194 Source #

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

d_inverse_1146 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_distrib_1152 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_isEquivalence_1158 ∷ T_IsRing_1584 → T_IsEquivalence_26 Source #

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

du_isNearSemiring_1160 ∷ T_IsRing_1584 → T_IsNearSemiring_876 Source #

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

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

du_isSemiringWithoutOne_1168 ∷ T_IsRing_1584 → T_IsSemiringWithoutOne_952 Source #

d_zero_1184 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_isEquivalence_1192 ∷ T_IsSelectiveMagma_158 → T_IsEquivalence_26 Source #

d_isMagma_1194 ∷ T_IsSelectiveMagma_158 → T_IsMagma_86 Source #

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

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

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

d_isEquivalence_1220 ∷ T_IsSemigroup_194 → T_IsEquivalence_26 Source #

d_isMagma_1222 ∷ T_IsSemigroup_194 → T_IsMagma_86 Source #

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

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

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

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

d_isBand_1250 ∷ T_IsSemilattice_312 → T_IsBand_230 Source #

d_isEquivalence_1252 ∷ T_IsSemilattice_312 → T_IsEquivalence_26 Source #

d_isMagma_1254 ∷ T_IsSemilattice_312 → T_IsMagma_86 Source #

d_isSemigroup_1258 ∷ T_IsSemilattice_312 → T_IsSemigroup_194 Source #

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

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

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

d_identity_1286 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

d_isMagma_1292 ∷ T_IsSemiring_1238 → T_IsMagma_86 Source #

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

d_isSemigroup_1296 ∷ T_IsSemiring_1238 → T_IsSemigroup_194 Source #

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

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

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

d_identity_1308 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

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

d_isMagma_1320 ∷ T_IsSemiring_1238 → T_IsMagma_86 Source #

d_isMonoid_1322 ∷ T_IsSemiring_1238 → T_IsMonoid_358 Source #

d_isSemigroup_1324 ∷ T_IsSemiring_1238 → T_IsSemigroup_194 Source #

d_distrib_1326 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

d_isEquivalence_1332 ∷ T_IsSemiring_1238 → T_IsEquivalence_26 Source #

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

du_isNearSemiring_1334 ∷ T_IsSemiring_1238 → T_IsNearSemiring_876 Source #

d_isSemiringWithoutAnnihilatingZero_1338 ∷ T_IsSemiring_1238 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

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

d_zero_1352 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

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

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

d_identity_1368 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_Σ_14 Source #

d_isMagma_1374 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsMagma_86 Source #

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

d_isSemigroup_1378 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsSemigroup_194 Source #

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

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

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

d_identity_1390 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_Σ_14 Source #

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

d_isMagma_1402 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsMagma_86 Source #

d_isMonoid_1404 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsMonoid_358 Source #

d_isSemigroup_1406 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsSemigroup_194 Source #

d_distrib_1408 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_Σ_14 Source #

d_isEquivalence_1414 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsEquivalence_26 Source #

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

d_'8729''45'cong_1432 ∷ (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_1438 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsSemiringWithoutOne_952 → T_IsMagma_86 Source #

du_isMagma_1438 ∷ T_IsSemiringWithoutOne_952 → T_IsMagma_86 Source #

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

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

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

d_'8729''45'cong_1446 ∷ (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_1452 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → Integer → T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

du_identity_1452 ∷ T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

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

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

du_isMagma_1464 ∷ T_IsSemiringWithoutOne_952 → T_IsMagma_86 Source #

d_isMonoid_1466 ∷ T_IsSemiringWithoutOne_952 → T_IsMonoid_358 Source #

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

du_isSemigroup_1468 ∷ T_IsSemiringWithoutOne_952 → T_IsSemigroup_194 Source #

d_distrib_1470 ∷ T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

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

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

du_isEquivalence_1474 ∷ T_IsSemiringWithoutOne_952 → T_IsEquivalence_26 Source #

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

d_zero_1490 ∷ T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

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

d_'8801''7495''8658''8801'_1506 ∷ Integer → Integer → AgdaAny → T__'8801'__12 Source #

d_'8801''8658''8801''7495'_1518 ∷ Integer → Integer → T__'8801'__12 → AgdaAny Source #

du_'8801''8658''8801''7495'_1518 ∷ Integer → AgdaAny Source #

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

d_'8801''45'irrelevant_1534 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8799''45'diag_1542 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8801''45'isDecEquivalence_1544 ∷ T_IsDecEquivalence_44 Source #

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

d_0'8802'1'43'n_1550 ∷ Integer → T__'8801'__12 → T_'8869'_4 Source #

d_1'43'n'8802'0_1554 ∷ Integer → T__'8801'__12 → T_'8869'_4 Source #

d_1'43'n'8802'n_1558 ∷ Integer → T__'8801'__12 → T_'8869'_4 Source #

d_'60''7495''8658''60'_1566 ∷ Integer → Integer → AgdaAny → T__'8804'__18 Source #

du_'60''7495''8658''60'_1566 ∷ Integer → T__'8804'__18 Source #

d_'60''8658''60''7495'_1582 ∷ Integer → Integer → T__'8804'__18 → AgdaAny Source #

du_'60''8658''60''7495'_1582 ∷ T__'8804'__18 → AgdaAny Source #

d_'60''7495''45'reflects'45''60'_1590 ∷ Integer → Integer → T_Reflects_14 Source #

d_'8804''7495''8658''8804'_1600 ∷ Integer → Integer → AgdaAny → T__'8804'__18 Source #

du_'8804''7495''8658''8804'_1600 ∷ Integer → T__'8804'__18 Source #

d_'8804''8658''8804''7495'_1616 ∷ Integer → Integer → T__'8804'__18 → AgdaAny Source #

du_'8804''8658''8804''7495'_1616 ∷ T__'8804'__18 → AgdaAny Source #

d_'8804''7495''45'reflects'45''8804'_1624 ∷ Integer → Integer → T_Reflects_14 Source #

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

du_'8804''45'reflexive_1630 ∷ Integer → T__'8804'__18 Source #

d_'8804''45'refl_1634 ∷ Integer → T__'8804'__18 Source #

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

d_'8804''45'trans_1642 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

du_'8804''45'trans_1642 ∷ T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

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

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

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

d__'8805''63'__1682 ∷ Integer → Integer → T_Dec_32 Source #

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

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

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

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

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

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

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

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

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

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

d_s'8804's'45'injective_1712 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8801'__12 → T__'8801'__12 Source #

d_'8804''45'step_1718 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'8804''45'step_1718 ∷ T__'8804'__18 → T__'8804'__18 Source #

d_n'8804'1'43'n_1724 ∷ Integer → T__'8804'__18 Source #

d_1'43'n'8816'n_1728 ∷ Integer → T__'8804'__18 → T_'8869'_4 Source #

d_n'8804'0'8658'n'8801'0_1734 ∷ Integer → T__'8804'__18 → T__'8801'__12 Source #

d_'60''8658''8804'_1736 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'60''8658''8804'_1736 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'60''8658''8802'_1740 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 → T_'8869'_4 Source #

d_'62''8658''8802'_1744 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 → T_'8869'_4 Source #

d_'8804''8658''8815'_1746 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 → T_'8869'_4 Source #

d_'60''8658''8817'_1752 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 → T_'8869'_4 Source #

d_'60''8658''8815'_1758 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 → T_'8869'_4 Source #

d_'8816''8658''8814'_1764 ∷ Integer → Integer → (T__'8804'__18 → T_'8869'_4) → T__'8804'__18 → T_'8869'_4 Source #

d_'8816''8658''62'_1770 ∷ Integer → Integer → (T__'8804'__18 → T_'8869'_4) → T__'8804'__18 Source #

du_'8816''8658''62'_1770 ∷ Integer → Integer → T__'8804'__18 Source #

d_'8816''8658''8805'_1782 ∷ Integer → Integer → (T__'8804'__18 → T_'8869'_4) → T__'8804'__18 Source #

du_'8816''8658''8805'_1782 ∷ Integer → Integer → T__'8804'__18 Source #

d_'8814''8658''8805'_1784 ∷ Integer → Integer → (T__'8804'__18 → T_'8869'_4) → T__'8804'__18 Source #

du_'8814''8658''8805'_1784 ∷ Integer → Integer → T__'8804'__18 Source #

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

du_'8804''8743''8802''8658''60'_1800 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'8804''8743''8814''8658''8801'_1818 ∷ Integer → Integer → T__'8804'__18 → (T__'8804'__18 → T_'8869'_4) → T__'8801'__12 Source #

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

d_'8805''45''62''45'connex_1846 ∷ Integer → Integer → T__'8846'__30 Source #

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

d_'62''45''8805''45'connex_1850 ∷ Integer → Integer → T__'8846'__30 Source #

d_'60''45'irrefl_1852 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__18 → T_'8869'_4 Source #

d_'60''45'asym_1856 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 → T_'8869'_4 Source #

d_'60''45'trans_1862 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

du_'60''45'trans_1862 ∷ Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'60''45'trans'691'_1868 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

du_'60''45'trans'691'_1868 ∷ T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'60''45'trans'737'_1874 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

du_'60''45'trans'737'_1874 ∷ T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

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

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

d__'62''63'__1918 ∷ Integer → Integer → T_Dec_32 Source #

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

d_'60''45'resp'8322''45''8801'_1922 ∷ T_Σ_14 Source #

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

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

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

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

d_n'8814'n_1938 ∷ Integer → T__'8804'__18 → T_'8869'_4 Source #

d_0'60'1'43'n_1944 ∷ Integer → T__'8804'__18 Source #

du_0'60'1'43'n_1944 ∷ T__'8804'__18 Source #

d_n'60'1'43'n_1948 ∷ Integer → T__'8804'__18 Source #

d_n'60'1'8658'n'8801'0_1954 ∷ Integer → T__'8804'__18 → T__'8801'__12 Source #

d_n'8802'0'8658'n'62'0_1960 ∷ Integer → (T__'8801'__12 → T_'8869'_4) → T__'8804'__18 Source #

du_n'8802'0'8658'n'62'0_1960 ∷ Integer → T__'8804'__18 Source #

d_m'60'n'8658'0'60'n_1970 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_m'60'n'8658'0'60'n_1970 ∷ T__'8804'__18 → T__'8804'__18 Source #

d_m'60'n'8658'n'8802'0_1976 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 → T_'8869'_4 Source #

d_m'60'n'8658'm'8804'1'43'n_1984 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_m'60'n'8658'm'8804'1'43'n_1984 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'8704''91'm'8804'n'8658'm'8802'o'93''8658'n'60'o_1992 ∷ Integer → Integer → (Integer → T__'8804'__18 → T__'8801'__12 → T_'8869'_4) → T__'8804'__18 Source #

du_'8704''91'm'8804'n'8658'm'8802'o'93''8658'n'60'o_1992 ∷ Integer → Integer → T__'8804'__18 Source #

d_rec_2010 ∷ Integer → Integer → (Integer → T__'8804'__18 → T__'8801'__12 → T_'8869'_4) → Integer → T__'8804'__18 → T__'8801'__12 → T_'8869'_4 Source #

d_'8704''91'm'60'n'8658'm'8802'o'93''8658'n'8804'o_2020 ∷ Integer → Integer → (Integer → T__'8804'__18 → T__'8801'__12 → T_'8869'_4) → T__'8804'__18 Source #

du_'8704''91'm'60'n'8658'm'8802'o'93''8658'n'8804'o_2020 ∷ Integer → Integer → T__'8804'__18 Source #

d_rec_2040 ∷ Integer → Integer → (Integer → T__'8804'__18 → T__'8801'__12 → T_'8869'_4) → Integer → T__'8804'__18 → T__'8801'__12 → T_'8869'_4 Source #

d__IsRelatedTo__2048 ∷ p → p → () Source #

d__'8718'_2050 ∷ Integer → T__IsRelatedTo__70 Source #

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

d_IsEquality_2054 ∷ p → p → p → () Source #

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

d_IsStrict_2058 ∷ p → p → p → () Source #

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

d_begin__2062 ∷ Integer → Integer → T__IsRelatedTo__70 → T__'8804'__18 Source #

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

d_begin'45'strict__2066 ∷ Integer → Integer → T__IsRelatedTo__70 → AgdaAny → T__'8804'__18 Source #

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

d_extractStrict_2072 ∷ Integer → Integer → T__IsRelatedTo__70 → T_IsStrict_92 → T__'8804'__18 Source #

d_step'45''60'_2080 ∷ Integer → Integer → Integer → T__IsRelatedTo__70 → T__'8804'__18 → T__IsRelatedTo__70 Source #

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

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

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

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

d_step'45''8804'_2086 ∷ Integer → Integer → Integer → T__IsRelatedTo__70 → T__'8804'__18 → T__IsRelatedTo__70 Source #

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

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

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

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

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

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

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

d_'43''45'cancel'691''45''8801'_2150 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'43''45'cancel'45''8801'_2152 ∷ T_Σ_14 Source #

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

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

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

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

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

d_'43''45'rawMagma_2164 ∷ T_RawMagma_8 Source #

d_'43''45'0'45'rawMonoid_2166 ∷ T_RawMonoid_474 Source #

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

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

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

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

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

d_'8760''45'magma_2178 ∷ T_Magma_36 Source #

d_m'8802'1'43'm'43'n_2184 ∷ Integer → Integer → T__'8801'__12 → T_'8869'_4 Source #

d_m'8802'1'43'n'43'm_2194 ∷ Integer → Integer → T__'8801'__12 → T_'8869'_4 Source #

d_m'43'1'43'n'8802'm_2204 ∷ Integer → Integer → T__'8801'__12 → T_'8869'_4 Source #

d_m'43'1'43'n'8802'0_2212 ∷ Integer → Integer → T__'8801'__12 → T_'8869'_4 Source #

d_m'43'n'8801'0'8658'm'8801'0_2226 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_m'43'n'8801'0'8658'n'8801'0_2234 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'43''45'cancel'737''45''8804'_2242 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'43''45'cancel'737''45''8804'_2242 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'43''45'cancel'691''45''8804'_2250 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'43''45'cancel'691''45''8804'_2250 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'43''45'cancel'45''8804'_2260 ∷ T_Σ_14 Source #

d_'43''45'cancel'737''45''60'_2262 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'43''45'cancel'737''45''60'_2262 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'43''45'cancel'691''45''60'_2272 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'43''45'cancel'691''45''60'_2272 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'43''45'cancel'45''60'_2280 ∷ T_Σ_14 Source #

d_'8804''45'steps'737'_2288 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'8804''45'steps'737'_2288 ∷ T__'8804'__18 → T__'8804'__18 Source #

d_'8804''45'steps'691'_2302 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'8804''45'steps'691'_2302 ∷ T__'8804'__18 → T__'8804'__18 Source #

d_m'8804'm'43'n_2316 ∷ Integer → Integer → T__'8804'__18 Source #

du_m'8804'm'43'n_2316 ∷ Integer → T__'8804'__18 Source #

d_m'8804'n'43'm_2328 ∷ Integer → Integer → T__'8804'__18 Source #

du_m'8804'n'43'm_2328 ∷ Integer → T__'8804'__18 Source #

d_m'8804'n'8658'm'60'n'8744'm'8801'n_2340 ∷ Integer → Integer → T__'8804'__18 → T__'8846'__30 Source #

d_m'43'n'8804'o'8658'm'8804'o_2376 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_m'43'n'8804'o'8658'm'8804'o_2376 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_m'43'n'8804'o'8658'n'8804'o_2390 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_m'43'n'8804'o'8658'n'8804'o_2390 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'43''45'mono'45''8804'_2398 ∷ Integer → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

du_'43''45'mono'45''8804'_2398 ∷ Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'43''45'mono'737''45''8804'_2412 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'43''45'mono'737''45''8804'_2412 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'43''45'mono'691''45''8804'_2422 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'43''45'mono'691''45''8804'_2422 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'43''45'mono'45''60''45''8804'_2428 ∷ Integer → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

du_'43''45'mono'45''60''45''8804'_2428 ∷ T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'43''45'mono'45''8804''45''60'_2438 ∷ Integer → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

du_'43''45'mono'45''8804''45''60'_2438 ∷ Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

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

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

d_'43''45'mono'737''45''60'_2456 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'43''45'mono'737''45''60'_2456 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'43''45'mono'691''45''60'_2464 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'43''45'mono'691''45''60'_2464 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_m'43'1'43'n'8816'm_2476 ∷ Integer → Integer → T__'8804'__18 → T_'8869'_4 Source #

d_m'60'm'43'n_2486 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_m'60'm'43'n_2486 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_m'60'n'43'm_2498 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_m'60'n'43'm_2498 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_m'43'n'8814'n_2514 ∷ Integer → Integer → T__'8804'__18 → T_'8869'_4 Source #

d_m'43'n'8814'm_2528 ∷ Integer → Integer → T__'8804'__18 → T_'8869'_4 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_'42''45'rawMagma_2626 ∷ T_RawMagma_8 Source #

d_'42''45'1'45'rawMonoid_2628 ∷ T_RawMonoid_474 Source #

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

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

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

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

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

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

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

d_'42''45'cancel'691''45''8801'_2650 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'42''45'cancel'737''45''8801'_2668 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

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

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

d_m'42'n'8801'1'8658'm'8801'1_2696 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_m'42'n'8801'1'8658'n'8801'1_2710 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'91'm'42'n'93''42''91'o'42'p'93''8801''91'm'42'o'93''42''91'n'42'p'93'_2726 ∷ Integer → Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'cancel'691''45''8804'_2792 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'42''45'cancel'691''45''8804'_2792 ∷ Integer → T__'8804'__18 Source #

d_'42''45'cancel'737''45''8804'_2808 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'42''45'cancel'737''45''8804'_2808 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'42''45'mono'45''8804'_2824 ∷ Integer → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

du_'42''45'mono'45''8804'_2824 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'42''45'mono'737''45''8804'_2834 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'42''45'mono'737''45''8804'_2834 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'42''45'mono'691''45''8804'_2844 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'42''45'mono'691''45''8804'_2844 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'42''45'mono'45''60'_2850 ∷ Integer → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

du_'42''45'mono'45''60'_2850 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'42''45'mono'737''45''60'_2862 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'42''45'mono'691''45''60'_2874 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'42''45'mono'691''45''60'_2874 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_m'8804'm'42'n_2886 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_m'8804'n'42'm_2898 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_m'60'm'42'n_2910 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'42''45'cancel'691''45''60'_2920 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'42''45'cancel'691''45''60'_2920 ∷ Integer → Integer → Integer → T__'8804'__18 Source #

d_'42''45'cancel'737''45''60'_2936 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'42''45'cancel'45''60'_2952 ∷ T_Σ_14 Source #

d_'94''45'identity'691'_2954 ∷ Integer → T__'8801'__12 Source #

d_'94''45'zero'737'_2958 ∷ Integer → T__'8801'__12 Source #

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

d_'94''45'semigroup'45'morphism_2986 ∷ Integer → T_IsSemigroupMorphism_148 Source #

du_'94''45'semigroup'45'morphism_2986 ∷ T_IsSemigroupMorphism_148 Source #

d_'94''45'monoid'45'morphism_2994 ∷ Integer → T_IsMonoidMorphism_298 Source #

du_'94''45'monoid'45'morphism_2994 ∷ T_IsMonoidMorphism_298 Source #

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

d_m'94'n'8801'0'8658'm'8801'0_3024 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_m'94'n'8801'1'8658'n'8801'0'8744'm'8801'1_3036 ∷ Integer → Integer → T__'8801'__12 → T__'8846'__30 Source #

du_m'94'n'8801'1'8658'n'8801'0'8744'm'8801'1_3036 ∷ Integer → T__'8846'__30 Source #

d_m'8804'n'8658'm'8852'n'8801'n_3050 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

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

d_m'8804'n'8658'm'8851'n'8801'm_3074 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

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

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

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

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

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

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

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

d_x'8851'y'8804'x_3108 ∷ Integer → Integer → T__'8804'__18 Source #

d_x'8804'y'8658'x'8851'z'8804'y_3110 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_x'8804'y'8658'z'8851'x'8804'y_3112 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_x'8804'y'8658'x'8851'z'8804'y_3114 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_x'8804'y'8658'z'8851'x'8804'y_3116 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_x'8804'y'8851'z'8658'x'8804'y_3118 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_x'8804'y'8851'z'8658'x'8804'z_3120 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_x'8851'y'8804'y_3122 ∷ Integer → Integer → T__'8804'__18 Source #

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

d_x'8851'y'8776'y'8658'y'8804'x_3126 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__18 Source #

d_x'8851'y'8804'x_3128 ∷ Integer → Integer → T__'8804'__18 Source #

d_x'8851'y'8804'x'8852'y_3130 ∷ Integer → Integer → T__'8804'__18 Source #

d_x'8851'y'8804'y_3132 ∷ Integer → Integer → T__'8804'__18 Source #

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

d_x'8851'y'8776'y'8658'y'8804'x_3136 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__18 Source #

d_x'8804'y'8851'z'8658'x'8804'y_3138 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_x'8804'y'8851'z'8658'x'8804'z_3140 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

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

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

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

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

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

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

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

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

d_'8851''45'glb_3164 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

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

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

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

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

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

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

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

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

d_'8851''45'mono'45''8804'_3190 ∷ Integer → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'8851''45'mono'691''45''8804'_3194 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'8851''45'mono'737''45''8804'_3196 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_'8851''45'glb_3270 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

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

d_'8851''45'mono'45''8804'_3274 ∷ Integer → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'8851''45'mono'691''45''8804'_3278 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'8851''45'mono'737''45''8804'_3280 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

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

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

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

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

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

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

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

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

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

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

d_'8852''45'identity'737'_3308 ∷ Integer → T__'8801'__12 Source #

d_'8852''45'identity'691'_3310 ∷ Integer → T__'8801'__12 Source #

d_'8852''45'identity_3314 ∷ T_Σ_14 Source #

d_'8852''45'0'45'isMonoid_3316 ∷ T_IsMonoid_358 Source #

d_'8852''45'0'45'isCommutativeMonoid_3318 ∷ T_IsCommutativeMonoid_406 Source #

d_'8852''45'0'45'monoid_3320 ∷ T_Monoid_506 Source #

d_'8852''45'0'45'commutativeMonoid_3322 ∷ T_CommutativeMonoid_582 Source #

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

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

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

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

d_m'60'n'8658'm'60'n'8852'o_3370 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_m'60'n'8658'm'60'o'8852'n_3378 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_m'8852'n'60'o'8658'm'60'o_3386 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_m'8852'n'60'o'8658'm'60'o_3386 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_m'8852'n'60'o'8658'n'60'o_3400 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_m'8852'n'60'o'8658'n'60'o_3400 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'8852''45'mono'45''60'_3408 ∷ Integer → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'8852''45'pres'45''60'm_3416 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'43''45'distrib'737''45''8852'_3426 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'43''45'distrib'691''45''8852'_3438 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'43''45'distrib'45''8852'_3440 ∷ T_Σ_14 Source #

d_m'8852'n'8804'm'43'n_3446 ∷ Integer → Integer → T__'8804'__18 Source #

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

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

d_'42''45'distrib'45''8852'_3500 ∷ T_Σ_14 Source #

d_'8851''45'zero'737'_3502 ∷ Integer → T__'8801'__12 Source #

d_'8851''45'zero'691'_3504 ∷ Integer → T__'8801'__12 Source #

d_'8851''45'zero_3508 ∷ T_Σ_14 Source #

d_'8852''45''8851''45'isSemiringWithoutOne_3510 ∷ T_IsSemiringWithoutOne_952 Source #

d_'8852''45''8851''45'isCommutativeSemiringWithoutOne_3512 ∷ T_IsCommutativeSemiringWithoutOne_1044 Source #

d_'8852''45''8851''45'commutativeSemiringWithoutOne_3514 ∷ T_CommutativeSemiringWithoutOne_1598 Source #

d_m'60'n'8658'm'8851'o'60'n_3522 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_m'60'n'8658'm'8851'o'60'n_3522 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_m'60'n'8658'o'8851'm'60'n_3534 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_m'60'n'8658'o'8851'm'60'n_3534 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_m'60'n'8851'o'8658'm'60'n_3546 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_m'60'n'8851'o'8658'm'60'o_3554 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'8851''45'mono'45''60'_3556 ∷ Integer → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'8851''45'pres'45'm'60'_3564 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'43''45'distrib'737''45''8851'_3574 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'43''45'distrib'691''45''8851'_3586 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'43''45'distrib'45''8851'_3588 ∷ T_Σ_14 Source #

d_m'8851'n'8804'm'43'n_3594 ∷ Integer → Integer → T__'8804'__18 Source #

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

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

d_'42''45'distrib'45''8851'_3648 ∷ T_Σ_14 Source #

d_0'8760'n'8801'0_3650 ∷ Integer → T__'8801'__12 Source #

d_n'8760'n'8801'0_3654 ∷ Integer → T__'8801'__12 Source #

d_pred'91'm'8760'n'93''8801'm'8760''91'1'43'n'93'_3662 ∷ Integer → Integer → T__'8801'__12 Source #

d_m'8760'n'8804'm_3676 ∷ Integer → Integer → T__'8804'__18 Source #

d_m'8814'm'8760'n_3690 ∷ Integer → Integer → T__'8804'__18 → T_'8869'_4 Source #

d_1'43'm'8802'm'8760'n_3702 ∷ Integer → Integer → T__'8801'__12 → T_'8869'_4 Source #

d_'8760''45'mono_3710 ∷ Integer → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'8760''45'mono'737''45''8804'_3728 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'8760''45'mono'691''45''8804'_3740 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'8760''45'mono'691''45''60'_3750 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'8760''45'cancel'691''45''8804'_3772 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

du_'8760''45'cancel'691''45''8804'_3772 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'8760''45'cancel'691''45''60'_3792 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'8760''45'cancel'691''45''60'_3792 ∷ Integer → Integer → T__'8804'__18 Source #

d_'8760''45'cancel'737''45''8801'_3818 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8801'__12 → T__'8801'__12 Source #

d_'8760''45'cancel'691''45''8801'_3840 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8801'__12 → T__'8801'__12 Source #

d_m'8760'n'8801'0'8658'm'8804'n_3854 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__18 Source #

du_m'8760'n'8801'0'8658'm'8804'n_3854 ∷ Integer → T__'8804'__18 Source #

d_m'8804'n'8658'm'8760'n'8801'0_3866 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

d_m'60'n'8658'0'60'n'8760'm_3876 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_m'60'n'8658'0'60'n'8760'm_3876 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_m'8760'n'8802'0'8658'n'60'm_3890 ∷ Integer → Integer → (T__'8801'__12 → T_'8869'_4) → T__'8804'__18 Source #

du_m'8760'n'8802'0'8658'n'60'm_3890 ∷ Integer → Integer → T__'8804'__18 Source #

d_m'62'n'8658'm'8760'n'8802'0_3922 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 → T_'8869'_4 Source #

d_'43''45''8760''45'comm_3934 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

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

d_'43''45''8760''45'assoc_3976 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

d_m'8804'n'43'm'8760'n_3996 ∷ Integer → Integer → T__'8804'__18 Source #

d_m'43'n'8760'n'8801'm_4010 ∷ Integer → Integer → T__'8801'__12 Source #

d_m'43'n'8760'm'8801'n_4022 ∷ Integer → Integer → T__'8801'__12 Source #

d_m'43''91'n'8760'm'93''8801'n_4034 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

d_m'8760'n'43'n'8801'm_4048 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

d_m'8760''91'm'8760'n'93''8801'n_4060 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

d_'91'm'43'n'93''8760''91'm'43'o'93''8801'n'8760'o_4076 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'691''45''8760'_4088 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'737''45''8760'_4108 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'45''8760'_4110 ∷ T_Σ_14 Source #

d_even'8802'odd_4116 ∷ Integer → Integer → T__'8801'__12 → T_'8869'_4 Source #

d_m'8851'n'43'n'8760'm'8801'n_4132 ∷ Integer → Integer → T__'8801'__12 Source #

d_'91'm'8760'n'93''8851''91'n'8760'm'93''8801'0_4146 ∷ Integer → Integer → T__'8801'__12 Source #

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

d_'8760''45'distrib'691''45''8851'_4170 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

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

d_'8760''45'distrib'691''45''8852'_4192 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_pred'45'mono_4200 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_pred'91'n'93''8804'n_4206 ∷ Integer → T__'8804'__18 Source #

d_'8804'pred'8658''8804'_4214 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'8804'pred'8658''8804'_4214 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'8804''8658'pred'8804'_4230 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'8804''8658'pred'8804'_4230 ∷ Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'60''8658''8804'pred_4242 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'60''8658''8804'pred_4242 ∷ T__'8804'__18 → T__'8804'__18 Source #

d_suc'91'pred'91'n'93''93''8801'n_4248 ∷ Integer → (T__'8801'__12 → T_'8869'_4) → T__'8801'__12 Source #

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

d_'8739'm'45'n'8739''8801'0'8658'm'8801'n_4268 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_m'8804'n'8658''8739'n'45'm'8739''8801'n'8760'm_4282 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

d_'8739'm'45'n'8739''8801'm'8760'n'8658'n'8804'm_4292 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__18 Source #

du_'8739'm'45'n'8739''8801'm'8760'n'8658'n'8804'm_4292 ∷ Integer → Integer → T__'8804'__18 Source #

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

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

d_'8739'm'43'n'45'm'43'o'8739''8801''8739'n'45'o'8739'_4330 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_m'8760'n'8804''8739'm'45'n'8739'_4346 ∷ Integer → Integer → T__'8804'__18 Source #

d_'8739'm'45'n'8739''8804'm'8852'n_4376 ∷ Integer → Integer → T__'8804'__18 Source #

d_'8739''45''8739''45'identity'737'_4386 ∷ Integer → T__'8801'__12 Source #

d_'8739''45''8739''45'identity'691'_4390 ∷ Integer → T__'8801'__12 Source #

d_'8739''45''8739''45'identity_4394 ∷ T_Σ_14 Source #

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

d_'8739'm'45'n'8739''8801''91'm'8760'n'93''8744''91'n'8760'm'93'_4410 ∷ Integer → Integer → T__'8846'__30 Source #

d_'42''45'distrib'737''45''8739''45''8739''45'aux_4438 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

d_'42''45'distrib'737''45''8739''45''8739'_4450 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'691''45''8739''45''8739'_4480 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'45''8739''45''8739'_4482 ∷ T_Σ_14 Source #

d_m'8804'n'43''8739'n'45'm'8739'_4488 ∷ Integer → Integer → T__'8804'__18 Source #

d_m'8804'n'43''8739'm'45'n'8739'_4502 ∷ Integer → Integer → T__'8804'__18 Source #

d_m'8804''8739'm'45'n'8739''43'n_4516 ∷ Integer → Integer → T__'8804'__18 Source #

d_'8739''45''8739''45'triangle_4524 ∷ Integer → Integer → Integer → T__'8804'__18 Source #

d_'8739''45''8739''45'isProtoMetric_4552 ∷ T_IsProtoMetric_30 Source #

d_'8739''45''8739''45'isPreMetric_4554 ∷ T_IsPreMetric_96 Source #

d_'8739''45''8739''45'isQuasiSemiMetric_4556 ∷ T_IsQuasiSemiMetric_162 Source #

d_'8739''45''8739''45'isSemiMetric_4558 ∷ T_IsSemiMetric_232 Source #

d_'8739''45''8739''45'isMetric_4560 ∷ T_IsGeneralMetric_308 Source #

d_'8739''45''8739''45'quasiSemiMetric_4562 ∷ T_QuasiSemiMetric_174 Source #

d_'8739''45''8739''45'semiMetric_4564 ∷ T_SemiMetric_266 Source #

d_'8739''45''8739''45'preMetric_4566 ∷ T_PreMetric_90 Source #

d_'8739''45''8739''45'metric_4568 ∷ T_Metric_364 Source #

d_'8970'n'47'2'8971''45'mono_4570 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'8970'n'47'2'8971''45'mono_4570 ∷ T__'8804'__18 → T__'8804'__18 Source #

d_'8968'n'47'2'8969''45'mono_4574 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'8968'n'47'2'8969''45'mono_4574 ∷ T__'8804'__18 → T__'8804'__18 Source #

d_'8970'n'47'2'8971''8804''8968'n'47'2'8969'_4580 ∷ Integer → T__'8804'__18 Source #

d_'8970'n'47'2'8971''43''8968'n'47'2'8969''8801'n_4586 ∷ Integer → T__'8801'__12 Source #

d_'8970'n'47'2'8971''8804'n_4592 ∷ Integer → T__'8804'__18 Source #

d_'8970'n'47'2'8971''60'n_4598 ∷ Integer → T__'8804'__18 Source #

d_'8968'n'47'2'8969''8804'n_4604 ∷ Integer → T__'8804'__18 Source #

d_'8968'n'47'2'8969''60'n_4610 ∷ Integer → T__'8804'__18 Source #

d_'8804''8242''45'trans_4614 ∷ Integer → Integer → Integer → T__'8804''8242'__154 → T__'8804''8242'__154 → T__'8804''8242'__154 Source #

du_'8804''8242''45'trans_4614 ∷ T__'8804''8242'__154 → T__'8804''8242'__154 → T__'8804''8242'__154 Source #

d_z'8804''8242'n_4624 ∷ Integer → T__'8804''8242'__154 Source #

d_s'8804''8242's_4632 ∷ Integer → Integer → T__'8804''8242'__154 → T__'8804''8242'__154 Source #

du_s'8804''8242's_4632 ∷ T__'8804''8242'__154 → T__'8804''8242'__154 Source #

d_'8804''8242''8658''8804'_4636 ∷ Integer → Integer → T__'8804''8242'__154 → T__'8804'__18 Source #

du_'8804''8242''8658''8804'_4636 ∷ Integer → T__'8804''8242'__154 → T__'8804'__18 Source #

d_'8804''8658''8804''8242'_4640 ∷ Integer → Integer → T__'8804'__18 → T__'8804''8242'__154 Source #

du_'8804''8658''8804''8242'_4640 ∷ Integer → T__'8804'__18 → T__'8804''8242'__154 Source #

d_'8804''8242''45'step'45'injective_4652 ∷ Integer → Integer → T__'8804''8242'__154 → T__'8804''8242'__154 → T__'8801'__12 → T__'8801'__12 Source #

d__'8804''8242''63'__4654 ∷ Integer → Integer → T_Dec_32 Source #

d__'60''8242''63'__4660 ∷ Integer → Integer → T_Dec_32 Source #

d__'8805''8242''63'__4666 ∷ Integer → Integer → T_Dec_32 Source #

d__'62''8242''63'__4668 ∷ Integer → Integer → T_Dec_32 Source #

d_m'8804''8242'm'43'n_4674 ∷ Integer → Integer → T__'8804''8242'__154 Source #

d_n'8804''8242'm'43'n_4684 ∷ Integer → Integer → T__'8804''8242'__154 Source #

du_n'8804''8242'm'43'n_4684 ∷ Integer → T__'8804''8242'__154 Source #

d_'8968'n'47'2'8969''8804''8242'n_4694 ∷ Integer → T__'8804''8242'__154 Source #

d_'8970'n'47'2'8971''8804''8242'n_4700 ∷ Integer → T__'8804''8242'__154 Source #

d_m'60''7495'n'8658'1'43'm'43''91'n'45'1'43'm'93''8801'n_4708 ∷ Integer → Integer → AgdaAny → T__'8801'__12 Source #

d_m'60''7495'1'43'm'43'n_4720 ∷ Integer → Integer → AgdaAny Source #

du_m'60''7495'1'43'm'43'n_4720 ∷ Integer → AgdaAny Source #

d_'60''7495''8658''60''8243'_4728 ∷ Integer → Integer → AgdaAny → T__'8804''8243'__188 Source #

du_'60''7495''8658''60''8243'_4728 ∷ Integer → Integer → T__'8804''8243'__188 Source #

d_'60''8243''8658''60''7495'_4740 ∷ Integer → Integer → T__'8804''8243'__188 → AgdaAny Source #

du_'60''8243''8658''60''7495'_4740 ∷ Integer → T__'8804''8243'__188 → AgdaAny Source #

d_'8804''8243''8658''8804'_4744 ∷ Integer → Integer → T__'8804''8243'__188 → T__'8804'__18 Source #

du_'8804''8243''8658''8804'_4744 ∷ Integer → T__'8804''8243'__188 → T__'8804'__18 Source #

d_'8804''8658''8804''8243'_4748 ∷ Integer → Integer → T__'8804'__18 → T__'8804''8243'__188 Source #

du_'8804''8658''8804''8243'_4748 ∷ Integer → Integer → T__'8804''8243'__188 Source #

d__'60''8243''63'__4750 ∷ Integer → Integer → T_Dec_32 Source #

d__'8804''8243''63'__4756 ∷ Integer → Integer → T_Dec_32 Source #

d__'8805''8243''63'__4764 ∷ Integer → Integer → T_Dec_32 Source #

d__'62''8243''63'__4766 ∷ Integer → Integer → T_Dec_32 Source #

d_'8804''8243''45'irrelevant_4768 ∷ Integer → Integer → T__'8804''8243'__188 → T__'8804''8243'__188 → T__'8801'__12 Source #

d_'60''8243''45'irrelevant_4786 ∷ Integer → Integer → T__'8804''8243'__188 → T__'8804''8243'__188 → T__'8801'__12 Source #

d_'62''8243''45'irrelevant_4788 ∷ Integer → Integer → T__'8804''8243'__188 → T__'8804''8243'__188 → T__'8801'__12 Source #

d_'8805''8243''45'irrelevant_4790 ∷ Integer → Integer → T__'8804''8243'__188 → T__'8804''8243'__188 → T__'8801'__12 Source #

d_'8804''8244''8658''8804''8243'_4796 ∷ Integer → Integer → T__'8804''8244'__222 → T__'8804''8243'__188 Source #

d_ind_4808 ∷ Integer → Integer → T__'8804''8244'__222 → T__'8804''8243'__188 Source #

d_m'8804''8244'm'43'k_4816 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8804''8244'__222 Source #

du_m'8804''8244'm'43'k_4816 ∷ Integer → T__'8804''8244'__222 Source #

d_'8804''8243''8658''8804''8244'_4832 ∷ Integer → Integer → T__'8804''8243'__188 → T__'8804''8244'__222 Source #

du_'8804''8243''8658''8804''8244'_4832 ∷ T__'8804''8243'__188 → T__'8804''8244'__222 Source #

d_0'8804''8244'n_4840 ∷ Integer → T__'8804''8244'__222 Source #

d_'60''7495''8658''60''8244'_4848 ∷ Integer → Integer → AgdaAny → T__'8804''8244'__222 Source #

du_'60''7495''8658''60''8244'_4848 ∷ Integer → Integer → T__'8804''8244'__222 Source #

d_'60''8244''8658''60''7495'_4860 ∷ Integer → Integer → T__'8804''8244'__222 → AgdaAny Source #

d__'60''8244''63'__4864 ∷ Integer → Integer → T_Dec_32 Source #

d__'8804''8244''63'__4870 ∷ Integer → Integer → T_Dec_32 Source #

d__'8805''8244''63'__4878 ∷ Integer → Integer → T_Dec_32 Source #

d__'62''8244''63'__4880 ∷ Integer → Integer → T_Dec_32 Source #

d_'8804''8658''8804''8244'_4882 ∷ Integer → Integer → T__'8804'__18 → T__'8804''8244'__222 Source #

du_'8804''8658''8804''8244'_4882 ∷ Integer → Integer → T__'8804''8244'__222 Source #

d_'8804''8244''8658''8804'_4884 ∷ Integer → Integer → T__'8804''8244'__222 → T__'8804'__18 Source #

d_eq'63'_4890 ∷ T_Level_18 → () → T_Injection_88 → AgdaAny → AgdaAny → T_Dec_32 Source #

du_eq'63'_4890 ∷ T_Injection_88 → AgdaAny → AgdaAny → T_Dec_32 Source #

d__'42''45'mono__4894 ∷ Integer → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d__'43''45'mono__4896 ∷ Integer → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

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

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

d_distrib'691''45''42''45''43'_4902 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'42''45'distrib'45''8760''691'_4904 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_cancel'45''43''45'left_4906 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_cancel'45''43''45'left'45''8804'_4908 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_cancel'45''42''45'right_4910 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_cancel'45''42''45'right'45''8804'_4912 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_strictTotalOrder_4914 ∷ T_StrictTotalOrder_864 Source #

d_isCommutativeSemiring_4916 ∷ T_IsCommutativeSemiring_1344 Source #

d_commutativeSemiring_4918 ∷ T_CommutativeSemiring_2094 Source #

d_isDistributiveLattice_4920 ∷ T_IsDistributiveLattice_814 Source #

d_distributiveLattice_4922 ∷ T_DistributiveLattice_1228 Source #

d_'8852''45''8851''45'0'45'isSemiringWithoutOne_4924 ∷ T_IsSemiringWithoutOne_952 Source #

d_'8852''45''8851''45'0'45'isCommutativeSemiringWithoutOne_4926 ∷ T_IsCommutativeSemiringWithoutOne_1044 Source #

d_'8852''45''8851''45'0'45'commutativeSemiringWithoutOne_4928 ∷ T_CommutativeSemiringWithoutOne_1598 Source #

d_'172'i'43'1'43'j'8804'i_4930 ∷ Integer → Integer → T__'8804'__18 → T_'8869'_4 Source #

d_'8804''45'steps_4932 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

du_'8804''45'steps_4932 ∷ T__'8804'__18 → T__'8804'__18 Source #

d_i'8760'k'8760'j'43'j'8760'k'8801'i'43'j'8760'k_4940 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_im'8801'jm'43'n'8658''91'i'8760'j'93'm'8801'n_4976 ∷ Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8804''43''8802''8658''60'_4992 ∷ Integer → Integer → T__'8804'__18 → (T__'8801'__12 → T_'8869'_4) → T__'8804'__18 Source #

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

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

d_i'43'1'43'j'8802'i_4998 ∷ Integer → Integer → T__'8801'__12 → T_'8869'_4 Source #

d_i'43'j'8801'0'8658'i'8801'0_5000 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_i'43'j'8801'0'8658'j'8801'0_5002 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_i'43'1'43'j'8816'i_5004 ∷ Integer → Integer → T__'8804'__18 → T_'8869'_4 Source #

d_i'42'j'8801'0'8658'i'8801'0'8744'j'8801'0_5006 ∷ Integer → Integer → T__'8801'__12 → T__'8846'__30 Source #

d_i'42'j'8801'1'8658'i'8801'1_5008 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_i'42'j'8801'1'8658'j'8801'1_5010 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_i'94'j'8801'0'8658'i'8801'0_5012 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_i'94'j'8801'1'8658'j'8801'0'8744'i'8801'1_5014 ∷ Integer → Integer → T__'8801'__12 → T__'8846'__30 Source #

d_'91'i'43'j'93''8760''91'i'43'k'93''8801'j'8760'k_5016 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_m'8802'0'8658'suc'91'pred'91'm'93''93''8801'm_5018 ∷ Integer → (T__'8801'__12 → T_'8869'_4) → T__'8801'__12 Source #

d_n'8801'm'8658''8739'n'45'm'8739''8801'0_5020 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8739'n'45'm'8739''8801'0'8658'n'8801'm_5022 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_'8739'n'45'm'8739''8801'n'8760'm'8658'm'8804'n_5024 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__18 Source #

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

d_'8739'n'43'm'45'n'43'o'8739''8801''8739'm'45'o'124'_5028 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_'8739'm'43'n'45'm'43'o'8739''8801''8739'n'45'o'124'_5030 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_n'8760'm'8804''8739'n'45'm'8739'_5032 ∷ Integer → Integer → T__'8804'__18 Source #

d_'8739'n'45'm'8739''8804'n'8852'm_5034 ∷ Integer → Integer → T__'8804'__18 Source #

d_n'8804'm'43'n_5040 ∷ Integer → Integer → T__'8804'__18 Source #

du_n'8804'm'43'n_5040 ∷ Integer → T__'8804'__18 Source #

d_n'8804'm'43'n'8760'm_5052 ∷ Integer → Integer → T__'8804'__18 Source #

d_'8739'n'45'm'8739''8801''91'n'8760'm'93''8744''91'm'8760'n'93'_5066 ∷ Integer → Integer → T__'8846'__30 Source #

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

d_n'8760'm'8804'n_5094 ∷ Integer → Integer → T__'8804'__18 Source #

d_'8704''91'm'8804'n'8658'm'8802'o'93''8658'o'60'n_5106 ∷ Integer → Integer → (Integer → T__'8804'__18 → T__'8801'__12 → T_'8869'_4) → T__'8804'__18 Source #

d_'8704''91'm'60'n'8658'm'8802'o'93''8658'o'8804'n_5114 ∷ Integer → Integer → (Integer → T__'8804'__18 → T__'8801'__12 → T_'8869'_4) → T__'8804'__18 Source #

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

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

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

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

d_m'8804'n'8658'n'8852'm'8801'n_5124 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

d_m'8804'n'8658'n'8851'm'8801'm_5126 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

d_n'8852'm'8801'm'8658'n'8804'm_5128 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__18 Source #

d_n'8852'm'8801'n'8658'm'8804'n_5130 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__18 Source #

d_n'8804'm'8852'n_5132 ∷ Integer → Integer → T__'8804'__18 Source #

d_'8852''45'least_5134 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'8851''45'greatest_5136 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'8852''45'pres'45''8804'm_5138 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'8851''45'pres'45'm'8804'_5140 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'8852''45'abs'45''8851'_5142 ∷ Integer → Integer → T__'8801'__12 Source #