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

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

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

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

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

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

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

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

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

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

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

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

d_IsCommutativeMonoid_150 ∷ p → p → () Source #

d_IsCommutativeRing_152 ∷ p → p → p → p → p → () Source #

d_IsCommutativeSemigroup_154 ∷ p → () Source #

d_IsCommutativeSemiring_156 ∷ p → p → p → p → () Source #

d_IsGroup_162 ∷ p → p → p → () Source #

d_IsMagma_182 ∷ p → () Source #

d_IsMonoid_188 ∷ p → p → () Source #

d_IsRing_204 ∷ p → p → p → p → p → () Source #

d_IsSemigroup_210 ∷ p → () Source #

d_IsSemiring_214 ∷ p → p → p → p → () Source #

d_comm_230 ∷ T_IsAbelianGroup_1132 → Integer → Integer → T__'8801'__12 Source #

d_isGroup_252 ∷ T_IsAbelianGroup_1132 → T_IsGroup_1036 Source #

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

d_isMonoid_536 ∷ T_IsCommutativeMonoid_736 → T_IsMonoid_686 Source #

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

d_isRing_654 ∷ T_IsCommutativeRing_2796 → T_IsRing_2650 Source #

d_comm_688 ∷ T_IsCommutativeSemigroup_548 → Integer → Integer → T__'8801'__12 Source #

d_isSemigroup_698 ∷ T_IsCommutativeSemigroup_548 → T_IsSemigroup_472 Source #

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

d_isSemiring_790 ∷ T_IsCommutativeSemiring_1678 → T_IsSemiring_1570 Source #

d_inverse_918 ∷ T_IsGroup_1036 → T_Σ_14 Source #

d_isMonoid_932 ∷ T_IsGroup_1036 → T_IsMonoid_686 Source #

d_'8315''185''45'cong_954 ∷ T_IsGroup_1036 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_isEquivalence_1482 ∷ T_IsMagma_176 → T_IsEquivalence_26 Source #

d_'8729''45'cong_1496 ∷ T_IsMagma_176 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1592 ∷ T_IsMonoid_686 → T_Σ_14 Source #

d_isSemigroup_1604 ∷ T_IsMonoid_686 → T_IsSemigroup_472 Source #

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

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

d_'42''45'identity_2118 ∷ T_IsRing_2650 → T_Σ_14 Source #

d_'43''45'isAbelianGroup_2146 ∷ T_IsRing_2650 → T_IsAbelianGroup_1132 Source #

d_distrib_2176 ∷ T_IsRing_2650 → T_Σ_14 Source #

d_assoc_2336 ∷ T_IsSemigroup_472 → Integer → Integer → Integer → T__'8801'__12 Source #

d_isMagma_2340 ∷ T_IsSemigroup_472 → T_IsMagma_176 Source #

d_isSemiringWithoutAnnihilatingZero_2454 ∷ T_IsSemiring_1570 → T_IsSemiringWithoutAnnihilatingZero_1468 Source #

d_zero_2468 ∷ T_IsSemiring_1570 → T_Σ_14 Source #

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

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

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

d_Morphism_2658 ∷ () Source #

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

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

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

d_Morphism_2668 ∷ () Source #

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

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

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

d__'8799'__2692 ∷ Integer → Integer → T_Dec_20 Source #

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

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

d_drop'8255''43''8804''43'_2714 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__22 Source #

du_drop'8255''43''8804''43'_2714 ∷ T__'8804'__26 → T__'8804'__22 Source #

d_drop'8255''45''8804''45'_2718 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__22 Source #

du_drop'8255''45''8804''45'_2718 ∷ T__'8804'__26 → T__'8804'__22 Source #

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

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

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

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

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

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

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

d__'8804''63'__2772 ∷ Integer → Integer → T_Dec_20 Source #

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

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

d_'8804''45'isTotalPreorder_2802 ∷ T_IsTotalPreorder_124 Source #

d_'8804''45'isPartialOrder_2804 ∷ T_IsPartialOrder_174 Source #

d_'8804''45'isTotalOrder_2806 ∷ T_IsTotalOrder_404 Source #

d_'8804''45'isDecTotalOrder_2808 ∷ T_IsDecTotalOrder_460 Source #

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

d_'8804''45'totalPreorder_2812 ∷ T_TotalPreorder_222 Source #

d_'8804''45'poset_2814 ∷ T_Poset_314 Source #

d_'8804''45'totalOrder_2816 ∷ T_TotalOrder_764 Source #

d_'8804''45'decTotalOrder_2818 ∷ T_DecTotalOrder_866 Source #

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

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

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

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

d_drop'8255''43''60''43'_2834 ∷ Integer → Integer → T__'60'__50 → T__'8804'__22 Source #

du_drop'8255''43''60''43'_2834 ∷ T__'60'__50 → T__'8804'__22 Source #

d_drop'8255''45''60''45'_2838 ∷ Integer → Integer → T__'60'__50 → T__'8804'__22 Source #

du_drop'8255''45''60''45'_2838 ∷ T__'60'__50 → T__'8804'__22 Source #

d_'43''8814'0_2842 ∷ Integer → T__'60'__50 → T_Irrelevant_20 Source #

d_'43''8814''45'_2844 ∷ Integer → Integer → T__'60'__50 → T_Irrelevant_20 Source #

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

du_'60''8658''8804'_2846 ∷ T__'60'__50 → T__'8804'__26 Source #

d_'60''8658''8802'_2852 ∷ Integer → Integer → T__'60'__50 → T__'8801'__12 → T_Irrelevant_20 Source #

d_'60''8658''8817'_2858 ∷ Integer → Integer → T__'60'__50 → T__'8804'__26 → T_Irrelevant_20 Source #

d_'8804''8658''8815'_2864 ∷ Integer → Integer → T__'8804'__26 → T__'60'__50 → T_Irrelevant_20 Source #

d_'8816''8658''62'_2874 ∷ Integer → Integer → (T__'8804'__26 → T_Irrelevant_20) → T__'60'__50 Source #

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

d_'8814''8658''8805'_2900 ∷ Integer → Integer → (T__'60'__50 → T_Irrelevant_20) → T__'8804'__26 Source #

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

d_'62''8658''8816'_2926 ∷ Integer → Integer → T__'60'__50 → T__'8804'__26 → T_Irrelevant_20 Source #

d_'8804''8743''8802''8658''60'_2928 ∷ Integer → Integer → T__'8804'__26 → (T__'8801'__12 → T_Irrelevant_20) → T__'60'__50 Source #

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

d_'8804''8743''8814''8658''8801'_2940 ∷ Integer → Integer → T__'8804'__26 → (T__'60'__50 → T_Irrelevant_20) → T__'8801'__12 Source #

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

d_'60''45'asym_2952 ∷ Integer → Integer → T__'60'__50 → T__'60'__50 → T_Irrelevant_20 Source #

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

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

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

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

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

du_'60''45'trans_2986 ∷ T__'60'__50 → T__'60'__50 → T__'60'__50 Source #

d_'60''45'cmp_2992 ∷ Integer → Integer → T_Tri_158 Source #

d__'60''63'__3082 ∷ Integer → Integer → T_Dec_20 Source #

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

d_'60''45'isStrictPartialOrder_3110 ∷ T_IsStrictPartialOrder_290 Source #

d_'60''45'isStrictTotalOrder_3116 ∷ T_IsStrictTotalOrder_534 Source #

d_'60''45'strictPartialOrder_3118 ∷ T_StrictPartialOrder_556 Source #

d_'60''45'strictTotalOrder_3120 ∷ T_StrictTotalOrder_1036 Source #

d_i'8814'i_3122 ∷ Integer → T__'60'__50 → T_Irrelevant_20 Source #

d_'62''45'irrefl_3124 ∷ Integer → Integer → T__'8801'__12 → T__'60'__50 → T_Irrelevant_20 Source #

d__IsRelatedTo__3130 ∷ p → p → () Source #

d__'8718'_3132 ∷ Integer → T__IsRelatedTo__78 Source #

d_'60''45'go_3134 ∷ Integer → Integer → Integer → T__'60'__50 → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

d_IsEquality_3136 ∷ p → p → p → () Source #

d_IsEquality'63'_3138 ∷ Integer → Integer → T__IsRelatedTo__78 → T_Dec_20 Source #

d_IsStrict_3140 ∷ p → p → p → () Source #

d_IsStrict'63'_3142 ∷ Integer → Integer → T__IsRelatedTo__78 → T_Dec_20 Source #

d_begin__3144 ∷ Integer → Integer → T__IsRelatedTo__78 → T__'8804'__26 Source #

d_begin'45'contradiction__3146 ∷ Integer → T__IsRelatedTo__78 → AgdaAny → T_Level_18 → () → AgdaAny Source #

d_begin__3148 ∷ Integer → Integer → T__IsRelatedTo__78 → AgdaAny → T__'8801'__12 Source #

d_begin__3150 ∷ Integer → Integer → T__IsRelatedTo__78 → AgdaAny → T__'60'__50 Source #

d_eqRelation_3152 ∷ T_SubRelation_60 Source #

d_extractEquality_3156 ∷ Integer → Integer → T__IsRelatedTo__78 → T_IsEquality_208 → T__'8801'__12 Source #

d_extractStrict_3158 ∷ Integer → Integer → T__IsRelatedTo__78 → T_IsStrict_172 → T__'60'__50 Source #

d_start_3166 ∷ Integer → Integer → T__IsRelatedTo__78 → T__'8804'__26 Source #

d_step'45''60'_3168 ∷ Integer → Integer → Integer → T__IsRelatedTo__78 → T__'60'__50 → T__IsRelatedTo__78 Source #

d_step'45''8801'_3170 ∷ Integer → Integer → Integer → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #

d_step'45''8801''45''8739'_3172 ∷ Integer → Integer → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

du_step'45''8801''45''8739'_3172 ∷ T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

d_step'45''8801''45''10216'_3174 ∷ Integer → Integer → Integer → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #

d_step'45''8801''45''10217'_3176 ∷ Integer → Integer → Integer → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #

d_step'45''8801''728'_3178 ∷ Integer → Integer → Integer → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #

d_step'45''8804'_3180 ∷ Integer → Integer → Integer → T__IsRelatedTo__78 → T__'8804'__26 → T__IsRelatedTo__78 Source #

d_stop_3182 ∷ Integer → T__IsRelatedTo__78 Source #

d_strictRelation_3186 ∷ T_SubRelation_60 Source #

d_'8776''45'go_3188 ∷ Integer → Integer → Integer → T__'8801'__12 → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

d_'8801''45'go_3190 ∷ Integer → Integer → Integer → T__'8801'__12 → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

du_'8801''45'go_3190 ∷ T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

d_'8804''45'go_3192 ∷ Integer → Integer → Integer → T__'8804'__26 → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

d_positive'8315''185'_3212 ∷ Integer → T_Positive_134 → T__'60'__50 Source #

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

d_negative'8315''185'_3218 ∷ Integer → T_Negative_164 → T__'60'__50 Source #

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

d_nonPositive'8315''185'_3224 ∷ Integer → T_NonPositive_154 → T__'8804'__26 Source #

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

d_nonNegative'8315''185'_3230 ∷ Integer → T_NonNegative_144 → T__'8804'__26 Source #

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

d_negative'60'positive_3238 ∷ Integer → Integer → T_Negative_164 → T_Positive_134 → T__'60'__50 Source #

du_negative'60'positive_3238 ∷ T__'60'__50 Source #

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

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

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

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

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

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

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

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

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

d_'8739'i'8739''8801'0'8658'i'8801'0_3340 ∷ Integer → T__'8801'__12 → T__'8801'__12 Source #

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

d_0'8804'i'8658''43''8739'i'8739''8801'i_3350 ∷ Integer → T__'8804'__26 → T__'8801'__12 Source #

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

du_'43''8739'i'8739''8801'i'8658'0'8804'i_3352 ∷ T__'8804'__26 Source #

d_'43''8739'i'8739''8801'i'8846''43''8739'i'8739''8801''45'i_3358 ∷ Integer → T__'8846'__30 Source #

d_'8739'm'8861'n'8739''8804'm'8852'n_3368 ∷ Integer → Integer → T__'8804'__22 Source #

d_'8739'i'43'j'8739''8804''8739'i'8739''43''8739'j'8739'_3398 ∷ Integer → Integer → T__'8804'__22 Source #

d_'8739'i'45'j'8739''8804''8739'i'8739''43''8739'j'8739'_3436 ∷ Integer → Integer → T__'8804'__22 Source #

d_'9667''45'nonZero_3454 ∷ T_Sign_6 → Integer → T_NonZero_112 → T_NonZero_112 Source #

du_'9667''45'nonZero_3454 ∷ T_Sign_6 → T_NonZero_112 Source #

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

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

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

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

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

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

d_sign'7522''9667''8739'i'8739''8801'i_3506 ∷ Integer → T__'8801'__12 Source #

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

d_sign'45'cong'8242'_3532 ∷ T_Sign_6 → Integer → T_Sign_6 → Integer → T__'8801'__12 → T__'8846'__30 Source #

du_sign'45'cong'8242'_3532 ∷ T_Sign_6 → Integer → T__'8846'__30 Source #

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

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

d_'43''9667''45'mono'45''60'_3600 ∷ Integer → Integer → T__'8804'__22 → T__'60'__50 Source #

du_'43''9667''45'mono'45''60'_3600 ∷ Integer → T__'8804'__22 → T__'60'__50 Source #

d_'43''9667''45'cancel'45''60'_3612 ∷ Integer → Integer → T__'60'__50 → T__'8804'__22 Source #

du_'43''9667''45'cancel'45''60'_3612 ∷ Integer → T__'60'__50 → T__'8804'__22 Source #

d_neg'9667''45'cancel'45''60'_3626 ∷ Integer → Integer → T__'60'__50 → T__'8804'__22 Source #

du_neg'9667''45'cancel'45''60'_3626 ∷ Integer → T__'60'__50 → T__'8804'__22 Source #

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

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

d_'43''9667''8814''45''9667'_3644 ∷ Integer → Integer → T__'60'__50 → T_Irrelevant_20 Source #

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

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

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

d_'8854''45''8805'_3704 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #

d_'8804''45''8854'_3732 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #

d_'8854''45''8804'_3746 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #

d_'8854''45''60'_3782 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #

d_'8854''45''8816'_3784 ∷ Integer → Integer → (T__'8804'__22 → T_Irrelevant_20) → T__'8801'__12 Source #

d_'8739''8854''8739''45''8804'_3786 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #

d_'8739''8854''8739''45''60'_3798 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #

d_'8739''8854''8739''45''8816'_3810 ∷ Integer → Integer → (T__'8804'__22 → T_Irrelevant_20) → T__'8801'__12 Source #

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

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

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

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

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

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

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

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

du_m'8854'1'43'n'60'm_3942 ∷ Integer → Integer → T__'60'__50 Source #

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

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

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

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

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

d_sign'45''8854''45''60'_4006 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #

d_sign'45''8854''45''8816'_4018 ∷ Integer → Integer → (T__'8804'__22 → T_Irrelevant_20) → T__'8801'__12 Source #

d_'8854''45'mono'691''45''8805''45''8804'_4024 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__26 Source #

d_'8854''45'mono'737''45''8804'_4056 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__26 Source #

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

d_'8854''45'mono'737''45''60'_4114 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'60'__50 Source #

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

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

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

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

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

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

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

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

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

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

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

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

d_'43''45'isMagma_4424 ∷ T_IsMagma_176 Source #

d_'43''45'isSemigroup_4426 ∷ T_IsSemigroup_472 Source #

d_'43''45'isCommutativeSemigroup_4428 ∷ T_IsCommutativeSemigroup_548 Source #

d_'43''45'0'45'isMonoid_4430 ∷ T_IsMonoid_686 Source #

d_'43''45'0'45'isCommutativeMonoid_4432 ∷ T_IsCommutativeMonoid_736 Source #

d_'43''45'0'45'isGroup_4434 ∷ T_IsGroup_1036 Source #

d_'43''45'0'45'isAbelianGroup_4436 ∷ T_IsAbelianGroup_1132 Source #

d_'43''45'magma_4438 ∷ T_Magma_68 Source #

d_'43''45'semigroup_4440 ∷ T_Semigroup_536 Source #

d_'43''45'commutativeSemigroup_4442 ∷ T_CommutativeSemigroup_662 Source #

d_'43''45'0'45'monoid_4444 ∷ T_Monoid_882 Source #

d_'43''45'0'45'commutativeMonoid_4446 ∷ T_CommutativeMonoid_962 Source #

d_'43''45'0'45'abelianGroup_4448 ∷ T_AbelianGroup_1636 Source #

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

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

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

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

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

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

d_i'8804'j'8658'i'8804'k'43'j_4578 ∷ Integer → Integer → Integer → T_NonNegative_144 → T__'8804'__26 → T__'8804'__26 Source #

du_i'8804'j'8658'i'8804'k'43'j_4578 ∷ Integer → Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_i'8804'j'43'i_4592 ∷ Integer → Integer → T_NonNegative_144 → T__'8804'__26 Source #

du_i'8804'j'43'i_4592 ∷ Integer → Integer → T__'8804'__26 Source #

d_i'8804'i'43'j_4604 ∷ Integer → Integer → T_NonNegative_144 → T__'8804'__26 Source #

du_i'8804'i'43'j_4604 ∷ Integer → Integer → T__'8804'__26 Source #

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

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

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

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

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

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

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

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

d_'8739'i'45'j'8739''8801''8739'j'45'i'8739'_4758 ∷ Integer → Integer → T__'8801'__12 Source #

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

d_i'8801'j'8658'i'45'j'8801'0_4826 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_i'45'j'8801'0'8658'i'8801'j_4834 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_i'8804'j'8658'i'45'k'8804'j_4852 ∷ Integer → Integer → Integer → T_NonNegative_144 → T__'8804'__26 → T__'8804'__26 Source #

du_i'8804'j'8658'i'45'k'8804'j_4852 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_i'45'j'8804'i_4880 ∷ Integer → Integer → T_NonNegative_144 → T__'8804'__26 Source #

du_i'45'j'8804'i_4880 ∷ Integer → Integer → T__'8804'__26 Source #

d_i'8804'j'8658'i'45'j'8804'0_4886 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_i'45'j'8804'0'8658'i'8804'j_4912 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_i'8804'j'8658'0'8804'j'45'i_4924 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_0'8804'i'45'j'8658'j'8804'i_4936 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_i'8804'j'8658'i'8804'1'43'j_4948 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

d_i'8804'suc'91'i'93'_4952 ∷ Integer → T__'8804'__26 Source #

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

d_i'8802'suc'91'i'93'_4970 ∷ Integer → T__'8801'__12 → T_Irrelevant_20 Source #

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

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

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

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

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

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

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

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

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

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

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

du_i'8804'pred'91'j'93''8658'i'60'j_5094 ∷ Integer → T__'8804'__26 → T__'60'__50 Source #

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

du_i'60'j'8658'i'8804'pred'91'j'93'_5104 ∷ Integer → T__'60'__50 → T__'8804'__26 Source #

d_i'8804'j'8658'pred'91'i'93''8804'j_5116 ∷ Integer → Integer → T__'8804'__26 → T__'8804'__26 Source #

du_i'8804'j'8658'pred'91'i'93''8804'j_5116 ∷ T__'8804'__26 → T__'8804'__26 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

d_'42''45'isMagma_5612 ∷ T_IsMagma_176 Source #

d_'42''45'isSemigroup_5614 ∷ T_IsSemigroup_472 Source #

d_'42''45'isCommutativeSemigroup_5616 ∷ T_IsCommutativeSemigroup_548 Source #

d_'42''45'1'45'isMonoid_5618 ∷ T_IsMonoid_686 Source #

d_'42''45'1'45'isCommutativeMonoid_5620 ∷ T_IsCommutativeMonoid_736 Source #

d_'43''45''42''45'isSemiring_5622 ∷ T_IsSemiring_1570 Source #

d_'43''45''42''45'isCommutativeSemiring_5624 ∷ T_IsCommutativeSemiring_1678 Source #

d_'43''45''42''45'isRing_5626 ∷ T_IsRing_2650 Source #

d_'43''45''42''45'isCommutativeRing_5628 ∷ T_IsCommutativeRing_2796 Source #

d_'42''45'magma_5630 ∷ T_Magma_68 Source #

d_'42''45'semigroup_5632 ∷ T_Semigroup_536 Source #

d_'42''45'commutativeSemigroup_5634 ∷ T_CommutativeSemigroup_662 Source #

d_'42''45'1'45'monoid_5636 ∷ T_Monoid_882 Source #

d_'42''45'1'45'commutativeMonoid_5638 ∷ T_CommutativeMonoid_962 Source #

d_'43''45''42''45'semiring_5640 ∷ T_Semiring_2280 Source #

d_'43''45''42''45'commutativeSemiring_5642 ∷ T_CommutativeSemiring_2446 Source #

d_'43''45''42''45'ring_5644 ∷ T_Ring_3800 Source #

d_'43''45''42''45'commutativeRing_5646 ∷ T_CommutativeRing_4016 Source #

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

d_sign'45''42'_5658 ∷ Integer → Integer → T_NonZero_112 → T__'8801'__12 Source #

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

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

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

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

d_'45'1'42'i'8801''45'i_5770 ∷ Integer → T__'8801'__12 Source #

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

du_i'42'j'8801'0'8658'i'8801'0'8744'j'8801'0_5780 ∷ Integer → T__'8846'__30 Source #

d_i'42'j'8802'0_5810 ∷ Integer → Integer → T_NonZero_112 → T_NonZero_112 → T_NonZero_112 Source #

du_i'42'j'8802'0_5810 ∷ T_NonZero_112 Source #

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

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

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

d_'94''45'isMagmaHomomorphism_5862 ∷ Integer → T_IsMagmaHomomorphism_176 Source #

du_'94''45'isMagmaHomomorphism_5862 ∷ T_IsMagmaHomomorphism_176 Source #

d_'94''45'isMonoidHomomorphism_5872 ∷ Integer → T_IsMonoidHomomorphism_350 Source #

du_'94''45'isMonoidHomomorphism_5872 ∷ T_IsMonoidHomomorphism_350 Source #

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

d_i'94'n'8801'0'8658'i'8801'0_5908 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

du_'42''45'mono'737''45''60''45'pos_6214 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

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

du_'42''45'mono'691''45''60''45'pos_6246 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

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

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

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

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

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

du_'42''45'mono'737''45''60''45'neg_6326 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

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

du_'42''45'mono'691''45''60''45'neg_6346 ∷ Integer → Integer → Integer → T__'60'__50 → T__'60'__50 Source #

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

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

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

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

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

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

d_'8739'i'42'j'8739''8801''8739'i'8739''42''8739'j'8739'_6428 ∷ Integer → Integer → T__'8801'__12 Source #

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

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

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

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

d_'8851''45'operator_6454 ∷ T_MinOperator_98 Source #

d_'8852''45'operator_6456 ∷ T_MaxOperator_128 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_'8851''45'band_6506 ∷ T_Band_596 Source #

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

d_'8851''45'commutativeSemigroup_6510 ∷ T_CommutativeSemigroup_662 Source #

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

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

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

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

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

d_'8851''45'isBand_6534 ∷ T_IsBand_508 Source #

d_'8851''45'isCommutativeSemigroup_6536 ∷ T_IsCommutativeSemigroup_548 Source #

d_'8851''45'isMagma_6538 ∷ T_IsMagma_176 Source #

d_'8851''45'isSelectiveMagma_6542 ∷ T_IsSelectiveMagma_436 Source #

d_'8851''45'isSemigroup_6544 ∷ T_IsSemigroup_472 Source #

d_'8851''45'magma_6546 ∷ T_Magma_68 Source #

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

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

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

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

d_'8851''45'selectiveMagma_6560 ∷ T_SelectiveMagma_122 Source #

d_'8851''45'semigroup_6562 ∷ T_Semigroup_536 Source #

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

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

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

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

d_'8851''45'band_6578 ∷ T_Band_596 Source #

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

d_'8851''45'commutativeSemigroup_6582 ∷ T_CommutativeSemigroup_662 Source #

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

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

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

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

d_'8851''45'isBand_6604 ∷ T_IsBand_508 Source #

d_'8851''45'isCommutativeSemigroup_6606 ∷ T_IsCommutativeSemigroup_548 Source #

d_'8851''45'isMagma_6608 ∷ T_IsMagma_176 Source #

d_'8851''45'isSelectiveMagma_6612 ∷ T_IsSelectiveMagma_436 Source #

d_'8851''45'isSemigroup_6614 ∷ T_IsSemigroup_472 Source #

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

d_'8851''45'magma_6618 ∷ T_Magma_68 Source #

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

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

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

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

d_'8851''45'selectiveMagma_6630 ∷ T_SelectiveMagma_122 Source #

d_'8851''45'semigroup_6632 ∷ T_Semigroup_536 Source #

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

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

d_'8851''45'isSemilattice_6646 ∷ T_IsCommutativeBand_590 Source #

d_'8851''45'semilattice_6648 ∷ T_Semilattice_10 Source #

d_'8851''45''8852''45'distributiveLattice_6650 ∷ T_DistributiveLattice_584 Source #

d_'8851''45''8852''45'isDistributiveLattice_6652 ∷ T_IsDistributiveLattice_3036 Source #

d_'8851''45''8852''45'isLattice_6654 ∷ T_IsLattice_2962 Source #

d_'8851''45''8852''45'lattice_6656 ∷ T_Lattice_500 Source #

d_'8851''45'isSemilattice_6658 ∷ T_IsCommutativeBand_590 Source #

d_'8851''45'semilattice_6660 ∷ T_Semilattice_10 Source #

d_'8852''45''8851''45'distributiveLattice_6662 ∷ T_DistributiveLattice_584 Source #

d_'8852''45''8851''45'isDistributiveLattice_6664 ∷ T_IsDistributiveLattice_3036 Source #

d_'8852''45''8851''45'isLattice_6666 ∷ T_IsLattice_2962 Source #

d_'8852''45''8851''45'lattice_6668 ∷ T_Lattice_500 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_n'8814'n_7110 ∷ Integer → T__'60'__50 → T_Irrelevant_20 Source #

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

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

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

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

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

d_'8739'm'43'n'8739''8804''8739'm'8739''43''8739'n'8739'_7122 ∷ Integer → Integer → T__'8804'__22 Source #

d_'8739'm'45'n'8739''8804''8739'm'8739''43''8739'n'8739'_7124 ∷ Integer → Integer → T__'8804'__22 Source #

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

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

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

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

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

d_'8804''45'steps_7136 ∷ Integer → Integer → Integer → T_NonNegative_144 → T__'8804'__26 → T__'8804'__26 Source #

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

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

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

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

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

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

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

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

d_n'8802'1'43'n_7154 ∷ Integer → T__'8801'__12 → T_Irrelevant_20 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_'43''45'isAbelianGroup_7238 ∷ T_IsAbelianGroup_1132 Source #