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

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

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

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

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

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

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

d_IsCommutativeMonoid_144 ∷ p → p → () Source #

d_IsCommutativeSemigroup_148 ∷ p → () Source #

d_IsCommutativeSemiring_150 ∷ p → p → p → p → () Source #

d_IsCommutativeSemiringWithoutOne_152 ∷ p → p → p → () Source #

d_IsMagma_176 ∷ p → () Source #

d_IsMonoid_182 ∷ p → p → () Source #

d_IsSemigroup_204 ∷ p → () Source #

d_IsSemiring_208 ∷ p → p → p → p → () Source #

d_IsSemiringWithoutOne_212 ∷ p → p → p → () Source #

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

d_isMonoid_530 ∷ T_IsCommutativeMonoid_736 → T_IsMonoid_686 Source #

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

d_isSemigroup_692 ∷ T_IsCommutativeSemigroup_548 → T_IsSemigroup_472 Source #

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

d_isSemiring_784 ∷ T_IsCommutativeSemiring_1678 → T_IsSemiring_1570 Source #

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

d_isSemiringWithoutOne_850 ∷ T_IsCommutativeSemiringWithoutOne_1382 → T_IsSemiringWithoutOne_1298 Source #

d_isEquivalence_1476 ∷ T_IsMagma_176 → T_IsEquivalence_26 Source #

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

d_identity_1586 ∷ T_IsMonoid_686 → T_Σ_14 Source #

d_isSemigroup_1598 ∷ T_IsMonoid_686 → T_IsSemigroup_472 Source #

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

d_isMagma_2334 ∷ T_IsSemigroup_472 → T_IsMagma_176 Source #

d_isSemiringWithoutAnnihilatingZero_2448 ∷ T_IsSemiring_1570 → T_IsSemiringWithoutAnnihilatingZero_1468 Source #

d_zero_2462 ∷ T_IsSemiring_1570 → T_Σ_14 Source #

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

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

d_'43''45'isCommutativeMonoid_2562 ∷ T_IsSemiringWithoutOne_1298 → T_IsCommutativeMonoid_736 Source #

d_distrib_2570 ∷ T_IsSemiringWithoutOne_1298 → T_Σ_14 Source #

d_zero_2590 ∷ T_IsSemiringWithoutOne_1298 → T_Σ_14 Source #

d_nonZero'63'_2652 ∷ Integer → T_Dec_20 Source #

d_nonTrivial'63'_2656 ∷ Integer → T_Dec_20 Source #

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

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

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

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

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

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

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

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

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

d_0'8802'1'43'n_2704 ∷ Integer → T__'8801'__12 → T_Irrelevant_20 Source #

d_1'43'n'8802'0_2706 ∷ Integer → T__'8801'__12 → T_Irrelevant_20 Source #

d_1'43'n'8802'n_2708 ∷ Integer → T__'8801'__12 → T_Irrelevant_20 Source #

d_'60''7495''8658''60'_2716 ∷ Integer → Integer → AgdaAny → T__'8804'__22 Source #

du_'60''7495''8658''60'_2716 ∷ Integer → T__'8804'__22 Source #

d_'60''8658''60''7495'_2728 ∷ Integer → Integer → T__'8804'__22 → AgdaAny Source #

du_'60''8658''60''7495'_2728 ∷ T__'8804'__22 → AgdaAny Source #

d_'60''7495''45'reflects'45''60'_2736 ∷ Integer → Integer → T_Reflects_16 Source #

d_'8804''7495''8658''8804'_2746 ∷ Integer → Integer → AgdaAny → T__'8804'__22 Source #

du_'8804''7495''8658''8804'_2746 ∷ Integer → T__'8804'__22 Source #

d_'8804''8658''8804''7495'_2758 ∷ Integer → Integer → T__'8804'__22 → AgdaAny Source #

du_'8804''8658''8804''7495'_2758 ∷ T__'8804'__22 → AgdaAny Source #

d_'8804''7495''45'reflects'45''8804'_2766 ∷ Integer → Integer → T_Reflects_16 Source #

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

du_'8804''45'reflexive_2772 ∷ Integer → T__'8804'__22 Source #

d_'8804''45'refl_2776 ∷ Integer → T__'8804'__22 Source #

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

d_'8804''45'trans_2784 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

du_'8804''45'trans_2784 ∷ T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

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

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

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

d__'8805''63'__2808 ∷ Integer → Integer → T_Dec_20 Source #

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

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

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

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

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

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

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

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

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

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

d_s'8804's'45'injective_2834 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 → T__'8801'__12 Source #

d_'8804''45'pred_2836 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'8804''45'pred_2836 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_m'8804'n'8658'm'8804'1'43'n_2838 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'8804'n'8658'm'8804'1'43'n_2838 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_n'8804'1'43'n_2844 ∷ Integer → T__'8804'__22 Source #

d_1'43'n'8816'n_2846 ∷ Integer → T__'8804'__22 → T_Irrelevant_20 Source #

d_n'8804'0'8658'n'8801'0_2850 ∷ Integer → T__'8804'__22 → T__'8801'__12 Source #

d_n'8804'1'8658'n'8801'0'8744'n'8801'1_2852 ∷ Integer → T__'8804'__22 → T__'8846'__30 Source #

du_n'8804'1'8658'n'8801'0'8744'n'8801'1_2852 ∷ T__'8804'__22 → T__'8846'__30 Source #

d_'60''8658''8804'_2854 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'60''8658''8804'_2854 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_'60''8658''8802'_2858 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20 Source #

d_'62''8658''8802'_2862 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20 Source #

d_'8804''8658''8815'_2864 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T_Irrelevant_20 Source #

d_'60''8658''8817'_2870 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T_Irrelevant_20 Source #

d_'60''8658''8815'_2876 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T_Irrelevant_20 Source #

d_'8816''8658''8814'_2882 ∷ Integer → Integer → (T__'8804'__22 → T_Irrelevant_20) → T__'8804'__22 → T_Irrelevant_20 Source #

d_'8816''8658''62'_2888 ∷ Integer → Integer → (T__'8804'__22 → T_Irrelevant_20) → T__'8804'__22 Source #

du_'8816''8658''62'_2888 ∷ Integer → Integer → T__'8804'__22 Source #

d_'8816''8658''8805'_2900 ∷ Integer → Integer → (T__'8804'__22 → T_Irrelevant_20) → T__'8804'__22 Source #

du_'8816''8658''8805'_2900 ∷ Integer → Integer → T__'8804'__22 Source #

d_'8814''8658''8805'_2902 ∷ Integer → Integer → (T__'8804'__22 → T_Irrelevant_20) → T__'8804'__22 Source #

du_'8814''8658''8805'_2902 ∷ Integer → Integer → T__'8804'__22 Source #

d_'8804''8743''8802''8658''60'_2918 ∷ Integer → Integer → T__'8804'__22 → (T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 Source #

du_'8804''8743''8802''8658''60'_2918 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'8804''8743''8814''8658''8801'_2936 ∷ Integer → Integer → T__'8804'__22 → (T__'8804'__22 → T_Irrelevant_20) → T__'8801'__12 Source #

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

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

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

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

d_'60''45'irrefl_2970 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__22 → T_Irrelevant_20 Source #

d_'60''45'asym_2974 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T_Irrelevant_20 Source #

d_'60''45'trans_2980 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

du_'60''45'trans_2980 ∷ Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8804''45''60''45'trans_2986 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

du_'8804''45''60''45'trans_2986 ∷ T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'60''45''8804''45'trans_2992 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

du_'60''45''8804''45'trans_2992 ∷ T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

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

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

d__'62''63'__3036 ∷ Integer → Integer → T_Dec_20 Source #

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

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

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

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

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

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

d_s'60's'45'injective_3058 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 → T__'8801'__12 Source #

d_'60''45'pred_3060 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'60''45'pred_3060 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_m'60'n'8658'm'60'1'43'n_3062 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'60'n'8658'm'60'1'43'n_3062 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_n'8814'0_3066 ∷ Integer → T__'8804'__22 → T_Irrelevant_20 Source #

d_n'8814'n_3070 ∷ Integer → T__'8804'__22 → T_Irrelevant_20 Source #

d_0'60'1'43'n_3074 ∷ Integer → T__'8804'__22 Source #

du_0'60'1'43'n_3074 ∷ T__'8804'__22 Source #

d_n'60'1'43'n_3078 ∷ Integer → T__'8804'__22 Source #

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

d_n'62'0'8658'n'8802'0_3086 ∷ Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20 Source #

d_n'8802'0'8658'n'62'0_3090 ∷ Integer → (T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 Source #

du_n'8802'0'8658'n'62'0_3090 ∷ Integer → T__'8804'__22 Source #

d_m'60'n'8658'0'60'n_3096 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'60'n'8658'0'60'n_3096 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_m'60'n'8658'n'8802'0_3098 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20 Source #

d_m'60'n'8658'm'8804'1'43'n_3102 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'60'n'8658'm'8804'1'43'n_3102 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_m'60'1'43'n'8658'm'60'n'8744'm'8801'n_3108 ∷ Integer → Integer → T__'8804'__22 → T__'8846'__30 Source #

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

d_m'60'1'43'n'8658'm'8804'n_3122 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'60'1'43'n'8658'm'8804'n_3122 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_'8704''91'm'8804'n'8658'm'8802'o'93''8658'n'60'o_3132 ∷ Integer → Integer → (Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 Source #

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

d_rec_3150 ∷ Integer → Integer → (Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20) → Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20 Source #

d_'8704''91'm'60'n'8658'm'8802'o'93''8658'n'8804'o_3160 ∷ Integer → Integer → (Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 Source #

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

d_rec_3180 ∷ Integer → Integer → (Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20) → Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20 Source #

d__IsRelatedTo__3188 ∷ p → p → () Source #

d__'8718'_3190 ∷ Integer → T__IsRelatedTo__78 Source #

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

d_IsEquality_3194 ∷ p → p → p → () Source #

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

d_IsStrict_3198 ∷ p → p → p → () Source #

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

d_begin__3202 ∷ Integer → Integer → T__IsRelatedTo__78 → T__'8804'__22 Source #

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

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

d_begin__3208 ∷ Integer → Integer → T__IsRelatedTo__78 → AgdaAny → T__'8804'__22 Source #

d_eqRelation_3210 ∷ T_SubRelation_60 Source #

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

d_extractStrict_3216 ∷ Integer → Integer → T__IsRelatedTo__78 → T_IsStrict_172 → T__'8804'__22 Source #

d_start_3224 ∷ Integer → Integer → T__IsRelatedTo__78 → T__'8804'__22 Source #

d_step'45''60'_3226 ∷ Integer → Integer → Integer → T__IsRelatedTo__78 → T__'8804'__22 → T__IsRelatedTo__78 Source #

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

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

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

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

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

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

d_step'45''8804'_3238 ∷ Integer → Integer → Integer → T__IsRelatedTo__78 → T__'8804'__22 → T__IsRelatedTo__78 Source #

d_stop_3240 ∷ Integer → T__IsRelatedTo__78 Source #

d_strictRelation_3244 ∷ T_SubRelation_60 Source #

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

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

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

d_'8804''45'go_3250 ∷ Integer → Integer → Integer → T__'8804'__22 → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_'8760''45'magma_3336 ∷ T_Magma_68 Source #

d_m'8802'1'43'm'43'n_3342 ∷ Integer → Integer → T__'8801'__12 → T_Irrelevant_20 Source #

d_m'8802'1'43'n'43'm_3352 ∷ Integer → Integer → T__'8801'__12 → T_Irrelevant_20 Source #

d_m'43'1'43'n'8802'm_3362 ∷ Integer → Integer → T__'8801'__12 → T_Irrelevant_20 Source #

d_m'43'1'43'n'8802'n_3370 ∷ Integer → Integer → T__'8801'__12 → T_Irrelevant_20 Source #

d_m'43'1'43'n'8802'0_3384 ∷ Integer → Integer → T__'8801'__12 → T_Irrelevant_20 Source #

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

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

d_'43''45'cancel'737''45''8804'_3414 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'43''45'cancel'737''45''8804'_3414 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'43''45'cancel'691''45''8804'_3422 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'43''45'cancel'691''45''8804'_3422 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

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

d_'43''45'cancel'737''45''60'_3434 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'43''45'cancel'737''45''60'_3434 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'43''45'cancel'691''45''60'_3444 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'43''45'cancel'691''45''60'_3444 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

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

d_m'8804'n'8658'm'8804'o'43'n_3458 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'8804'n'8658'm'8804'o'43'n_3458 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_m'8804'n'8658'm'8804'n'43'o_3468 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'8804'n'8658'm'8804'n'43'o_3468 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_m'8804'm'43'n_3482 ∷ Integer → Integer → T__'8804'__22 Source #

du_m'8804'm'43'n_3482 ∷ Integer → T__'8804'__22 Source #

d_m'8804'n'43'm_3494 ∷ Integer → Integer → T__'8804'__22 Source #

du_m'8804'n'43'm_3494 ∷ Integer → T__'8804'__22 Source #

d_m'43'n'8804'o'8658'm'8804'o_3508 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'43'n'8804'o'8658'm'8804'o_3508 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'43'n'8804'o'8658'n'8804'o_3522 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'43'n'8804'o'8658'n'8804'o_3522 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'43''45'mono'45''8804'_3530 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

du_'43''45'mono'45''8804'_3530 ∷ Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'43''45'mono'737''45''8804'_3544 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'43''45'mono'737''45''8804'_3544 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'43''45'mono'691''45''8804'_3554 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'43''45'mono'691''45''8804'_3554 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'43''45'mono'45''60''45''8804'_3560 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

du_'43''45'mono'45''60''45''8804'_3560 ∷ T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'43''45'mono'45''8804''45''60'_3570 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

du_'43''45'mono'45''8804''45''60'_3570 ∷ Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'43''45'mono'45''60'_3580 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

du_'43''45'mono'45''60'_3580 ∷ Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'43''45'mono'737''45''60'_3588 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'43''45'mono'737''45''60'_3588 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'43''45'mono'691''45''60'_3596 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'43''45'mono'691''45''60'_3596 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'43'1'43'n'8816'm_3608 ∷ Integer → Integer → T__'8804'__22 → T_Irrelevant_20 Source #

d_m'60'm'43'n_3618 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'60'm'43'n_3618 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'60'n'43'm_3630 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'60'n'43'm_3630 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'43'n'8814'n_3646 ∷ Integer → Integer → T__'8804'__22 → T_Irrelevant_20 Source #

d_m'43'n'8814'm_3660 ∷ Integer → Integer → T__'8804'__22 → T_Irrelevant_20 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_m'42'n'8802'0_3840 ∷ Integer → Integer → T_NonZero_112 → T_NonZero_112 → T_NonZero_112 Source #

du_m'42'n'8802'0_3840 ∷ T_NonZero_112 Source #

d_m'42'n'8802'0'8658'm'8802'0_3850 ∷ Integer → Integer → T_NonZero_112 → T_NonZero_112 Source #

du_m'42'n'8802'0'8658'm'8802'0_3850 ∷ T_NonZero_112 Source #

d_m'42'n'8802'0'8658'n'8802'0_3856 ∷ Integer → Integer → T_NonZero_112 → T_NonZero_112 Source #

du_m'42'n'8802'0'8658'n'8802'0_3856 ∷ T_NonZero_112 Source #

d_m'42'n'8801'0'8658'm'8801'0_3872 ∷ Integer → Integer → T_NonZero_112 → T__'8801'__12 → T__'8801'__12 Source #

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

d_m'42'n'8801'1'8658'n'8801'1_3894 ∷ 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'_3910 ∷ Integer → Integer → Integer → Integer → T__'8801'__12 Source #

d_m'8802'0'8743'n'62'1'8658'm'42'n'62'1_3998 ∷ Integer → Integer → T_NonZero_112 → T_NonTrivial_152 → T_NonTrivial_152 Source #

du_m'8802'0'8743'n'62'1'8658'm'42'n'62'1_3998 ∷ T_NonTrivial_152 Source #

d_n'8802'0'8743'm'62'1'8658'm'42'n'62'1_4012 ∷ Integer → Integer → T_NonZero_112 → T_NonTrivial_152 → T_NonTrivial_152 Source #

du_n'8802'0'8743'm'62'1'8658'm'42'n'62'1_4012 ∷ T_NonTrivial_152 Source #

d_'42''45'cancel'691''45''8804'_4030 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8804'__22 → T__'8804'__22 Source #

du_'42''45'cancel'691''45''8804'_4030 ∷ Integer → T__'8804'__22 Source #

d_'42''45'cancel'737''45''8804'_4044 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8804'__22 → T__'8804'__22 Source #

du_'42''45'cancel'737''45''8804'_4044 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'42''45'mono'45''8804'_4060 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

du_'42''45'mono'45''8804'_4060 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'42''45'mono'737''45''8804'_4070 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'42''45'mono'737''45''8804'_4070 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'42''45'mono'691''45''8804'_4080 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'42''45'mono'691''45''8804'_4080 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'42''45'mono'45''60'_4086 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

du_'42''45'mono'45''60'_4086 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'42''45'mono'737''45''60'_4100 ∷ Integer → T_NonZero_112 → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'42''45'mono'737''45''60'_4100 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'42''45'mono'691''45''60'_4114 ∷ Integer → T_NonZero_112 → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'42''45'mono'691''45''60'_4114 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'8804'm'42'n_4128 ∷ Integer → Integer → T_NonZero_112 → T__'8804'__22 Source #

du_m'8804'm'42'n_4128 ∷ Integer → Integer → T__'8804'__22 Source #

d_m'8804'n'42'm_4140 ∷ Integer → Integer → T_NonZero_112 → T__'8804'__22 Source #

du_m'8804'n'42'm_4140 ∷ Integer → Integer → T__'8804'__22 Source #

d_m'60'm'42'n_4152 ∷ Integer → Integer → T_NonZero_112 → T__'8804'__22 → T__'8804'__22 Source #

du_m'60'm'42'n_4152 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'60'n'8658'm'60'n'42'o_4166 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8804'__22 → T__'8804'__22 Source #

du_m'60'n'8658'm'60'n'42'o_4166 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'60'n'8658'm'60'o'42'n_4182 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8804'__22 → T__'8804'__22 Source #

du_m'60'n'8658'm'60'o'42'n_4182 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'42''45'cancel'691''45''60'_4192 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'42''45'cancel'691''45''60'_4192 ∷ Integer → Integer → Integer → T__'8804'__22 Source #

d_'42''45'cancel'737''45''60'_4208 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

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

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

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

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

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

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

d_'94''45'monoid'45'morphism_4266 ∷ Integer → T_IsMonoidMorphism_306 Source #

du_'94''45'monoid'45'morphism_4266 ∷ T_IsMonoidMorphism_306 Source #

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

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

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

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

d_m'94'n'8802'0_4324 ∷ Integer → Integer → T_NonZero_112 → T_NonZero_112 Source #

du_m'94'n'8802'0_4324 ∷ Integer → Integer → T_NonZero_112 Source #

d_m'94'n'62'0_4336 ∷ Integer → T_NonZero_112 → Integer → T__'8804'__22 Source #

du_m'94'n'62'0_4336 ∷ T__'8804'__22 Source #

d_'94''45'mono'737''45''8804'_4346 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'94''45'mono'737''45''8804'_4346 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'94''45'mono'691''45''8804'_4360 ∷ Integer → T_NonZero_112 → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'94''45'mono'691''45''8804'_4360 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'94''45'mono'737''45''60'_4376 ∷ Integer → T_NonZero_112 → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'94''45'mono'737''45''60'_4376 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'94''45'mono'691''45''60'_4388 ∷ Integer → T__'8804'__22 → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'8804'n'8658'm'8852'n'8801'n_4406 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #

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

d_m'8804'n'8658'm'8851'n'8801'm_4422 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #

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

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

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

d_'8852''8801''8852''8242'_4446 ∷ Integer → Integer → T__'8801'__12 Source #

d_'8851''8801''8851''8242'_4472 ∷ Integer → Integer → T__'8801'__12 Source #

d_x'8851'y'8804'x_4504 ∷ Integer → Integer → T__'8804'__22 Source #

d_x'8804'y'8658'x'8851'z'8804'y_4506 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_x'8804'y'8658'z'8851'x'8804'y_4508 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_x'8804'y'8658'x'8851'z'8804'y_4510 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_x'8804'y'8658'z'8851'x'8804'y_4512 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_x'8804'y'8851'z'8658'x'8804'y_4514 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_x'8804'y'8851'z'8658'x'8804'z_4516 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_x'8851'y'8804'y_4518 ∷ Integer → Integer → T__'8804'__22 Source #

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

d_x'8851'y'8776'y'8658'y'8804'x_4522 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #

d_x'8851'y'8804'x_4524 ∷ Integer → Integer → T__'8804'__22 Source #

d_x'8851'y'8804'x'8852'y_4526 ∷ Integer → Integer → T__'8804'__22 Source #

d_x'8851'y'8804'y_4528 ∷ Integer → Integer → T__'8804'__22 Source #

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

d_x'8851'y'8776'y'8658'y'8804'x_4532 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #

d_x'8804'y'8851'z'8658'x'8804'y_4534 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_x'8804'y'8851'z'8658'x'8804'z_4536 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

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

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

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

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

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

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

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

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

d_'8851''45'glb_4560 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

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

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

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

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

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

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

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

d_'8851''45'mono'45''8804'_4584 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8851''45'mono'691''45''8804'_4588 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'8851''45'mono'737''45''8804'_4590 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_'8851''45'glb_4652 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

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

d_'8851''45'mono'45''8804'_4656 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8851''45'mono'691''45''8804'_4660 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'8851''45'mono'737''45''8804'_4662 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_'8852''45'0'45'isMonoid_4714 ∷ T_IsMonoid_686 Source #

d_'8852''45'0'45'isCommutativeMonoid_4716 ∷ T_IsCommutativeMonoid_736 Source #

d_'8852''45'0'45'monoid_4718 ∷ T_Monoid_882 Source #

d_'8852''45'0'45'commutativeMonoid_4720 ∷ T_CommutativeMonoid_962 Source #

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

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

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

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

d_m'60'n'8658'm'60'n'8852'o_4764 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'60'n'8658'm'60'o'8852'n_4768 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'8852'n'60'o'8658'm'60'o_4776 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'8852'n'60'o'8658'm'60'o_4776 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'8852'n'60'o'8658'n'60'o_4790 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'8852'n'60'o'8658'n'60'o_4790 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'8852''45'mono'45''60'_4798 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8852''45'pres'45''60'm_4800 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

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

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

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

d_m'8852'n'8804'm'43'n_4830 ∷ Integer → Integer → T__'8804'__22 Source #

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

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

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

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

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

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

d_'8852''45''8851''45'isSemiringWithoutOne_4894 ∷ T_IsSemiringWithoutOne_1298 Source #

d_'8852''45''8851''45'isCommutativeSemiringWithoutOne_4896 ∷ T_IsCommutativeSemiringWithoutOne_1382 Source #

d_'8852''45''8851''45'commutativeSemiringWithoutOne_4898 ∷ T_CommutativeSemiringWithoutOne_2002 Source #

d_m'60'n'8658'm'8851'o'60'n_4902 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'60'n'8658'm'8851'o'60'n_4902 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'60'n'8658'o'8851'm'60'n_4910 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'60'n'8658'o'8851'm'60'n_4910 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'60'n'8851'o'8658'm'60'n_4920 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'60'n'8851'o'8658'm'60'o_4926 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'8851''45'mono'45''60'_4928 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8851''45'pres'45'm'60'_4930 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

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

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

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

d_m'8851'n'8804'm'43'n_4960 ∷ Integer → Integer → T__'8804'__22 Source #

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

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

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

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

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

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

d_m'8760'n'8804'm_5042 ∷ Integer → Integer → T__'8804'__22 Source #

d_m'8814'm'8760'n_5056 ∷ Integer → Integer → T__'8804'__22 → T_Irrelevant_20 Source #

d_1'43'm'8802'm'8760'n_5068 ∷ Integer → Integer → T__'8801'__12 → T_Irrelevant_20 Source #

d_'8760''45'mono_5076 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8760''45'mono'737''45''8804'_5090 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'8760''45'mono'691''45''8804'_5098 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'8760''45'mono'737''45''60'_5108 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

du_'8760''45'mono'737''45''60'_5108 ∷ Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8760''45'mono'691''45''60'_5134 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8760''45'cancel'691''45''8804'_5156 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

du_'8760''45'cancel'691''45''8804'_5156 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'8760''45'cancel'691''45''60'_5176 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'8760''45'cancel'691''45''60'_5176 ∷ Integer → Integer → T__'8804'__22 Source #

d_'8760''45'cancel'737''45''8801'_5196 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 → T__'8801'__12 Source #

d_'8760''45'cancel'691''45''8801'_5212 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 → T__'8801'__12 Source #

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

du_m'8760'n'8801'0'8658'm'8804'n_5222 ∷ Integer → T__'8804'__22 Source #

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

d_m'60'n'8658'0'60'n'8760'm_5236 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'60'n'8658'0'60'n'8760'm_5236 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'8760'n'8802'0'8658'n'60'm_5246 ∷ Integer → Integer → (T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 Source #

du_m'8760'n'8802'0'8658'n'60'm_5246 ∷ Integer → Integer → T__'8804'__22 Source #

d_m'62'n'8658'm'8760'n'8802'0_5274 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20 Source #

d_m'8804'n'8658'n'8760'm'8804'n_5280 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'8804'n'8658'n'8760'm'8804'n_5280 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'43''45''8760''45'comm_5290 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #

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

d_'43''45''8760''45'assoc_5332 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #

d_m'8804'n'43'o'8658'm'8760'n'8804'o_5354 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'8804'n'43'o'8658'm'8760'n'8804'o_5354 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'60'n'43'o'8658'm'8760'n'60'o_5374 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8804'__22 → T__'8804'__22 Source #

du_m'60'n'43'o'8658'm'8760'n'60'o_5374 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'43'n'8804'o'8658'm'8804'o'8760'n_5398 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_m'43'n'8804'o'8658'm'8804'o'8760'n_5398 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_m'8804'o'8760'n'8658'm'43'n'8804'o_5418 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

du_m'8804'o'8760'n'8658'm'43'n'8804'o_5418 ∷ T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_m'8804'n'43'm'8760'n_5444 ∷ Integer → Integer → T__'8804'__22 Source #

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

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

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

d_m'8760'n'43'n'8801'm_5492 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #

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

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

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

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

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

d_even'8802'odd_5560 ∷ Integer → Integer → T__'8801'__12 → T_Irrelevant_20 Source #

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

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

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

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

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

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

d_pred'91'n'93''8804'n_5644 ∷ Integer → T__'8804'__22 Source #

d_'8804'pred'8658''8804'_5648 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'8804'pred'8658''8804'_5648 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'8804''8658'pred'8804'_5656 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'8804''8658'pred'8804'_5656 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'60''8658''8804'pred_5664 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'60''8658''8804'pred_5664 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_suc'45'pred_5672 ∷ Integer → T_NonZero_112 → T__'8801'__12 Source #

d_pred'45'mono'45''8804'_5676 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_pred'45'mono'45''8804'_5676 ∷ Integer → T__'8804'__22 → T__'8804'__22 Source #

d_pred'45'mono'45''60'_5680 ∷ Integer → Integer → T_NonZero_112 → T__'8804'__22 → T__'8804'__22 Source #

du_pred'45'mono'45''60'_5680 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_pred'45'cancel'45''8804'_5682 ∷ Integer → Integer → T__'8804'__22 → T__'8846'__30 Source #

d_pred'45'cancel'45''60'_5686 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_pred'45'injective_5688 ∷ Integer → Integer → T_NonZero_112 → T_NonZero_112 → T__'8801'__12 → T__'8801'__12 Source #

d_pred'45'cancel'45''8801'_5694 ∷ Integer → Integer → T__'8801'__12 → T__'8846'__30 Source #

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

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

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

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

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

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

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

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

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

d_m'8760'n'8804''8739'm'45'n'8739'_5776 ∷ Integer → Integer → T__'8804'__22 Source #

d_'8739'm'45'n'8739''8804'm'8852'n_5806 ∷ Integer → Integer → T__'8804'__22 Source #

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

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

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

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

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

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

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

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

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

d_m'8804'n'43''8739'n'45'm'8739'_5918 ∷ Integer → Integer → T__'8804'__22 Source #

d_m'8804'n'43''8739'm'45'n'8739'_5932 ∷ Integer → Integer → T__'8804'__22 Source #

d_m'8804''8739'm'45'n'8739''43'n_5946 ∷ Integer → Integer → T__'8804'__22 Source #

d_'8739''45''8739''45'triangle_5954 ∷ Integer → Integer → Integer → T__'8804'__22 Source #

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

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

d_'8739''45''8739''45'isPreMetric_6010 ∷ T_IsPreMetric_102 Source #

d_'8739''45''8739''45'isQuasiSemiMetric_6012 ∷ T_IsQuasiSemiMetric_174 Source #

d_'8739''45''8739''45'isSemiMetric_6014 ∷ T_IsSemiMetric_250 Source #

d_'8739''45''8739''45'isMetric_6016 ∷ T_IsGeneralMetric_332 Source #

d_'8739''45''8739''45'quasiSemiMetric_6018 ∷ T_QuasiSemiMetric_186 Source #

d_'8739''45''8739''45'semiMetric_6020 ∷ T_SemiMetric_284 Source #

d_'8739''45''8739''45'preMetric_6022 ∷ T_PreMetric_96 Source #

d_'8739''45''8739''45'metric_6024 ∷ T_Metric_388 Source #

d_'8970'n'47'2'8971''45'mono_6026 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'8970'n'47'2'8971''45'mono_6026 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_'8968'n'47'2'8969''45'mono_6030 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'8968'n'47'2'8969''45'mono_6030 ∷ T__'8804'__22 → T__'8804'__22 Source #

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

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

d_'8970'n'47'2'8971''8804'n_6048 ∷ Integer → T__'8804'__22 Source #

d_'8970'n'47'2'8971''60'n_6054 ∷ Integer → T__'8804'__22 Source #

d_n'8801''8970'n'43'n'47'2'8971'_6060 ∷ Integer → T__'8801'__12 Source #

d_'8968'n'47'2'8969''8804'n_6068 ∷ Integer → T__'8804'__22 Source #

d_'8968'n'47'2'8969''60'n_6074 ∷ Integer → T__'8804'__22 Source #

d_n'8801''8968'n'43'n'47'2'8969'_6080 ∷ Integer → T__'8801'__12 Source #

d_1'8804'n'33'_6088 ∷ Integer → T__'8804'__22 Source #

d__'33''8802'0_6094 ∷ Integer → T_NonZero_112 Source #

d__'33''42'_'33''8802'0_6102 ∷ Integer → Integer → T_NonZero_112 Source #

du__'33''42'_'33''8802'0_6102 ∷ T_NonZero_112 Source #

d_'8804''8242''45'trans_6108 ∷ Integer → Integer → Integer → T__'8804''8242'__338 → T__'8804''8242'__338 → T__'8804''8242'__338 Source #

du_'8804''8242''45'trans_6108 ∷ T__'8804''8242'__338 → T__'8804''8242'__338 → T__'8804''8242'__338 Source #

d_z'8804''8242'n_6116 ∷ Integer → T__'8804''8242'__338 Source #

d_s'8804''8242's_6120 ∷ Integer → Integer → T__'8804''8242'__338 → T__'8804''8242'__338 Source #

du_s'8804''8242's_6120 ∷ T__'8804''8242'__338 → T__'8804''8242'__338 Source #

d_'8804''8242''8658''8804'_6124 ∷ Integer → Integer → T__'8804''8242'__338 → T__'8804'__22 Source #

du_'8804''8242''8658''8804'_6124 ∷ Integer → T__'8804''8242'__338 → T__'8804'__22 Source #

d_'8804''8658''8804''8242'_6128 ∷ Integer → Integer → T__'8804'__22 → T__'8804''8242'__338 Source #

du_'8804''8658''8804''8242'_6128 ∷ Integer → T__'8804'__22 → T__'8804''8242'__338 Source #

d_'8804''8242''45'step'45'injective_6136 ∷ Integer → Integer → T__'8804''8242'__338 → T__'8804''8242'__338 → T__'8801'__12 → T__'8801'__12 Source #

d_z'60''8242's_6138 ∷ Integer → T__'8804''8242'__338 Source #

d_s'60''8242's_6142 ∷ Integer → Integer → T__'8804''8242'__338 → T__'8804''8242'__338 Source #

du_s'60''8242's_6142 ∷ T__'8804''8242'__338 → T__'8804''8242'__338 Source #

d_'60''8658''60''8242'_6146 ∷ Integer → Integer → T__'8804'__22 → T__'8804''8242'__338 Source #

du_'60''8658''60''8242'_6146 ∷ Integer → T__'8804'__22 → T__'8804''8242'__338 Source #

d_'60''8242''8658''60'_6150 ∷ Integer → Integer → T__'8804''8242'__338 → T__'8804'__22 Source #

du_'60''8242''8658''60'_6150 ∷ Integer → T__'8804''8242'__338 → T__'8804'__22 Source #

d_m'60'1'43'n'8658'm'60'n'8744'm'8801'n'8242'_6154 ∷ Integer → Integer → T__'8804'__22 → T__'8846'__30 Source #

d__'8804''8242''63'__6168 ∷ Integer → Integer → T_Dec_20 Source #

d__'60''8242''63'__6174 ∷ Integer → Integer → T_Dec_20 Source #

d__'8805''8242''63'__6180 ∷ Integer → Integer → T_Dec_20 Source #

d__'62''8242''63'__6182 ∷ Integer → Integer → T_Dec_20 Source #

d_m'8804''8242'm'43'n_6188 ∷ Integer → Integer → T__'8804''8242'__338 Source #

d_n'8804''8242'm'43'n_6198 ∷ Integer → Integer → T__'8804''8242'__338 Source #

du_n'8804''8242'm'43'n_6198 ∷ Integer → T__'8804''8242'__338 Source #

d_'8968'n'47'2'8969''8804''8242'n_6208 ∷ Integer → T__'8804''8242'__338 Source #

d_'8970'n'47'2'8971''8804''8242'n_6214 ∷ Integer → T__'8804''8242'__338 Source #

d_'8804''8658''8804''8243'_6218 ∷ Integer → Integer → T__'8804'__22 → T__'8739''737'__26 Source #

du_'8804''8658''8804''8243'_6218 ∷ Integer → Integer → T__'8739''737'__26 Source #

d_'60''8658''60''8243'_6222 ∷ Integer → Integer → T__'8804'__22 → T__'8739''737'__26 Source #

d_'8804''8243''8658''8804'_6224 ∷ Integer → Integer → T__'8739''737'__26 → T__'8804'__22 Source #

du_'8804''8243''8658''8804'_6224 ∷ Integer → T__'8739''737'__26 → T__'8804'__22 Source #

d_'8804''8243''45'proof_6232 ∷ Integer → Integer → T__'8739''737'__26 → T__'8801'__12 Source #

d_m'8804'n'8658''8707''91'o'93'm'43'o'8801'n_6238 ∷ Integer → Integer → T__'8804'__22 → T_Σ_14 Source #

du_m'8804'n'8658''8707''91'o'93'm'43'o'8801'n_6238 ∷ Integer → Integer → T_Σ_14 Source #

d_guarded'45''8760''8791''8760'_6250 ∷ T__'8804'__22 → T__'8801'__12 Source #

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

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

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

d_'60''7495''8658''60''8243'_6274 ∷ Integer → Integer → AgdaAny → T__'8739''737'__26 Source #

du_'60''7495''8658''60''8243'_6274 ∷ Integer → Integer → T__'8739''737'__26 Source #

d_'60''8243''8658''60''7495'_6284 ∷ Integer → Integer → T__'8739''737'__26 → AgdaAny Source #

du_'60''8243''8658''60''7495'_6284 ∷ Integer → T__'8739''737'__26 → AgdaAny Source #

d__'60''8243''63'__6290 ∷ Integer → Integer → T_Dec_20 Source #

d__'8804''8243''63'__6296 ∷ Integer → Integer → T_Dec_20 Source #

d__'8805''8243''63'__6304 ∷ Integer → Integer → T_Dec_20 Source #

d__'62''8243''63'__6306 ∷ Integer → Integer → T_Dec_20 Source #

d_'8804''8243''45'irrelevant_6308 ∷ Integer → Integer → T__'8739''737'__26 → T__'8739''737'__26 → T__'8801'__12 Source #

d_'60''8243''45'irrelevant_6322 ∷ Integer → Integer → T__'8739''737'__26 → T__'8739''737'__26 → T__'8801'__12 Source #

d_'62''8243''45'irrelevant_6324 ∷ Integer → Integer → T__'8739''737'__26 → T__'8739''737'__26 → T__'8801'__12 Source #

d_'8805''8243''45'irrelevant_6326 ∷ Integer → Integer → T__'8739''737'__26 → T__'8739''737'__26 → T__'8801'__12 Source #

d_'8804''8244''8658''8804''8243'_6332 ∷ Integer → Integer → T__'8804''8244'__408 → T__'8739''737'__26 Source #

du_'8804''8244''8658''8804''8243'_6332 ∷ T__'8804''8244'__408 → T__'8739''737'__26 Source #

d_m'8804''8244'm'43'k_6346 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8804''8244'__408 Source #

du_m'8804''8244'm'43'k_6346 ∷ Integer → T__'8804''8244'__408 Source #

d_'8804''8243''8658''8804''8244'_6362 ∷ Integer → Integer → T__'8739''737'__26 → T__'8804''8244'__408 Source #

du_'8804''8243''8658''8804''8244'_6362 ∷ T__'8739''737'__26 → T__'8804''8244'__408 Source #

d_0'8804''8244'n_6366 ∷ Integer → T__'8804''8244'__408 Source #

d_'60''7495''8658''60''8244'_6368 ∷ Integer → Integer → AgdaAny → T__'8804''8244'__408 Source #

du_'60''7495''8658''60''8244'_6368 ∷ Integer → Integer → T__'8804''8244'__408 Source #

d_'60''8244''8658''60''7495'_6376 ∷ Integer → Integer → T__'8804''8244'__408 → AgdaAny Source #

du_'60''8244''8658''60''7495'_6376 ∷ Integer → T__'8804''8244'__408 → AgdaAny Source #

d__'60''8244''63'__6380 ∷ Integer → Integer → T_Dec_20 Source #

d__'8804''8244''63'__6386 ∷ Integer → Integer → T_Dec_20 Source #

d__'8805''8244''63'__6394 ∷ Integer → Integer → T_Dec_20 Source #

d__'62''8244''63'__6396 ∷ Integer → Integer → T_Dec_20 Source #

d_'8804''8658''8804''8244'_6398 ∷ Integer → Integer → T__'8804'__22 → T__'8804''8244'__408 Source #

du_'8804''8658''8804''8244'_6398 ∷ Integer → Integer → T__'8804''8244'__408 Source #

d_'8804''8244''8658''8804'_6400 ∷ Integer → Integer → T__'8804''8244'__408 → T__'8804'__22 Source #

du_'8804''8244''8658''8804'_6400 ∷ Integer → T__'8804''8244'__408 → T__'8804'__22 Source #

d_eq'63'_6406 ∷ T_Level_18 → () → T_Injection_776 → AgdaAny → AgdaAny → T_Dec_20 Source #

du_eq'63'_6406 ∷ T_Injection_776 → AgdaAny → AgdaAny → T_Dec_20 Source #

d_anyUpTo'63'_6424 ∷ T_Level_18 → (Integer → ()) → (Integer → T_Dec_20) → Integer → T_Dec_20 Source #

du_anyUpTo'63'_6424 ∷ (Integer → T_Dec_20) → Integer → T_Dec_20 Source #

d_'172'Pn'60'1'43'v_6458 ∷ T_Level_18 → (Integer → ()) → (Integer → T_Dec_20) → Integer → (AgdaAny → T_Irrelevant_20) → (T_Σ_14 → T_Irrelevant_20) → T_Σ_14 → T_Irrelevant_20 Source #

d_allUpTo'63'_6488 ∷ T_Level_18 → (Integer → ()) → (Integer → T_Dec_20) → Integer → T_Dec_20 Source #

du_allUpTo'63'_6488 ∷ (Integer → T_Dec_20) → Integer → T_Dec_20 Source #

d_Pn'60'1'43'v_6520 ∷ T_Level_18 → (Integer → ()) → (Integer → T_Dec_20) → Integer → AgdaAny → (Integer → T__'8804'__22 → AgdaAny) → Integer → T__'8804'__22 → AgdaAny Source #

du_Pn'60'1'43'v_6520 ∷ Integer → AgdaAny → (Integer → T__'8804'__22 → AgdaAny) → Integer → T__'8804'__22 → AgdaAny Source #

d_'8704''91'm'8804'n'8658'm'8802'o'93''8658'o'60'n_6546 ∷ Integer → Integer → (Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 Source #

d_'8704''91'm'60'n'8658'm'8802'o'93''8658'o'8804'n_6554 ∷ Integer → Integer → (Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 Source #

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

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

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

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

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

d_m'8804'n'8658'n'8852'm'8801'n_6566 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #

d_m'8804'n'8658'n'8851'm'8801'm_6568 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #

d_n'8852'm'8801'm'8658'n'8804'm_6570 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #

d_n'8852'm'8801'n'8658'm'8804'n_6572 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #

d_n'8804'm'8852'n_6574 ∷ Integer → Integer → T__'8804'__22 Source #

d_'8852''45'least_6576 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8851''45'greatest_6578 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8852''45'pres'45''8804'm_6580 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'8851''45'pres'45'm'8804'_6582 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

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

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

d_suc'91'pred'91'n'93''93''8801'n_6588 ∷ Integer → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 Source #

d_'8804''45'step_6594 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'8804''45'step_6594 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_'8804''45'steps'737'_6596 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'8804''45'steps'737'_6596 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_'8804''45'steps'691'_6598 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

du_'8804''45'steps'691'_6598 ∷ T__'8804'__22 → T__'8804'__22 Source #

d_'60''45'step_6600 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_pred'45'mono_6602 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #

d_'60''45'trans'691'_6604 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #

d_'60''45'trans'737'_6606 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #