Documentation

d__DistributesOver__10 :: (Integer -> Integer -> Integer) -> (Integer -> Integer -> Integer) -> () #

d__DistributesOver'691'__12 :: (Integer -> Integer -> Integer) -> (Integer -> Integer -> Integer) -> () #

d__DistributesOver'737'__14 :: (Integer -> Integer -> Integer) -> (Integer -> Integer -> Integer) -> () #

d_Associative_30 :: (Integer -> Integer -> Integer) -> () #

d_Commutative_32 :: (Integer -> Integer -> Integer) -> () #

d_Identity_48 :: Integer -> (Integer -> Integer -> Integer) -> () #

d_LeftIdentity_72 :: Integer -> (Integer -> Integer -> Integer) -> () #

d_LeftZero_80 :: Integer -> (Integer -> Integer -> Integer) -> () #

d_RightIdentity_100 :: Integer -> (Integer -> Integer -> Integer) -> () #

d_RightZero_108 :: Integer -> (Integer -> Integer -> Integer) -> () #

d_Zero_128 :: Integer -> (Integer -> Integer -> Integer) -> () #

d_IsCommutativeMonoid_144 :: p -> p -> () #

d_IsCommutativeSemigroup_148 :: p -> () #

d_IsCommutativeSemiring_150 :: p -> p -> p -> p -> () #

d_IsCommutativeSemiringWithoutOne_152 :: p -> p -> p -> () #

d_IsMagma_176 :: p -> () #

d_IsMonoid_182 :: p -> p -> () #

d_IsSemigroup_204 :: p -> () #

d_IsSemiring_208 :: p -> p -> p -> p -> () #

d_IsSemiringWithoutOne_212 :: p -> p -> p -> () #

d_comm_514 :: T_IsCommutativeMonoid_736 -> Integer -> Integer -> T__'8801'__12 #

d_isMonoid_530 :: T_IsCommutativeMonoid_736 -> T_IsMonoid_686 #

d_comm_682 :: T_IsCommutativeSemigroup_548 -> Integer -> Integer -> T__'8801'__12 #

d_isSemigroup_692 :: T_IsCommutativeSemigroup_548 -> T_IsSemigroup_472 #

d_'42''45'comm_714 :: T_IsCommutativeSemiring_1678 -> Integer -> Integer -> T__'8801'__12 #

d_isSemiring_784 :: T_IsCommutativeSemiring_1678 -> T_IsSemiring_1570 #

d_'42''45'comm_814 :: T_IsCommutativeSemiringWithoutOne_1382 -> Integer -> Integer -> T__'8801'__12 #

d_isSemiringWithoutOne_850 :: T_IsCommutativeSemiringWithoutOne_1382 -> T_IsSemiringWithoutOne_1298 #

d_isEquivalence_1476 :: T_IsMagma_176 -> T_IsEquivalence_26 #

d_'8729''45'cong_1490 :: T_IsMagma_176 -> Integer -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #

d_identity_1586 :: T_IsMonoid_686 -> T_Σ_14 #

d_isSemigroup_1598 :: T_IsMonoid_686 -> T_IsSemigroup_472 #

d_assoc_2330 :: T_IsSemigroup_472 -> Integer -> Integer -> Integer -> T__'8801'__12 #

d_isMagma_2334 :: T_IsSemigroup_472 -> T_IsMagma_176 #

d_isSemiringWithoutAnnihilatingZero_2448 :: T_IsSemiring_1570 -> T_IsSemiringWithoutAnnihilatingZero_1468 #

d_zero_2462 :: T_IsSemiring_1570 -> T_Σ_14 #

d_'42''45'assoc_2546 :: T_IsSemiringWithoutOne_1298 -> Integer -> Integer -> Integer -> T__'8801'__12 #

d_'42''45'cong_2548 :: T_IsSemiringWithoutOne_1298 -> Integer -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #

d_'43''45'isCommutativeMonoid_2562 :: T_IsSemiringWithoutOne_1298 -> T_IsCommutativeMonoid_736 #

d_distrib_2570 :: T_IsSemiringWithoutOne_1298 -> T_Σ_14 #

d_zero_2590 :: T_IsSemiringWithoutOne_1298 -> T_Σ_14 #

d_nonZero'63'_2652 :: Integer -> T_Dec_20 #

d_nonTrivial'63'_2656 :: Integer -> T_Dec_20 #

d_suc'45'injective_2660 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_'8801''7495''8658''8801'_2666 :: Integer -> Integer -> AgdaAny -> T__'8801'__12 #

d_'8801''8658''8801''7495'_2678 :: Integer -> Integer -> T__'8801'__12 -> AgdaAny #

du_'8801''8658''8801''7495'_2678 :: Integer -> AgdaAny #

d__'8799'__2688 :: Integer -> Integer -> T_Dec_20 #

d_'8801''45'irrelevant_2694 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #

d_'8799''45'diag_2698 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_'8801''45'isDecEquivalence_2700 :: T_IsDecEquivalence_44 #

d_'8801''45'decSetoid_2702 :: T_DecSetoid_84 #

d_0'8802'1'43'n_2704 :: Integer -> T__'8801'__12 -> T_Irrelevant_20 #

d_1'43'n'8802'0_2706 :: Integer -> T__'8801'__12 -> T_Irrelevant_20 #

d_1'43'n'8802'n_2708 :: Integer -> T__'8801'__12 -> T_Irrelevant_20 #

d_'60''7495''8658''60'_2716 :: Integer -> Integer -> AgdaAny -> T__'8804'__22 #

du_'60''7495''8658''60'_2716 :: Integer -> T__'8804'__22 #

d_'60''8658''60''7495'_2728 :: Integer -> Integer -> T__'8804'__22 -> AgdaAny #

du_'60''8658''60''7495'_2728 :: T__'8804'__22 -> AgdaAny #

d_'60''7495''45'reflects'45''60'_2736 :: Integer -> Integer -> T_Reflects_16 #

d_'8804''7495''8658''8804'_2746 :: Integer -> Integer -> AgdaAny -> T__'8804'__22 #

du_'8804''7495''8658''8804'_2746 :: Integer -> T__'8804'__22 #

d_'8804''8658''8804''7495'_2758 :: Integer -> Integer -> T__'8804'__22 -> AgdaAny #

du_'8804''8658''8804''7495'_2758 :: T__'8804'__22 -> AgdaAny #

d_'8804''7495''45'reflects'45''8804'_2766 :: Integer -> Integer -> T_Reflects_16 #

d_'8804''45'reflexive_2772 :: Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 #

du_'8804''45'reflexive_2772 :: Integer -> T__'8804'__22 #

d_'8804''45'refl_2776 :: Integer -> T__'8804'__22 #

d_'8804''45'antisym_2778 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 #

d_'8804''45'trans_2784 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

du_'8804''45'trans_2784 :: T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8804''45'total_2790 :: Integer -> Integer -> T__'8846'__30 #

d_'8804''45'irrelevant_2796 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 #

d__'8804''63'__2802 :: Integer -> Integer -> T_Dec_20 #

d__'8805''63'__2808 :: Integer -> Integer -> T_Dec_20 #

d_'8804''45'isPreorder_2810 :: T_IsPreorder_70 #

d_'8804''45'isTotalPreorder_2812 :: T_IsTotalPreorder_124 #

d_'8804''45'isPartialOrder_2814 :: T_IsPartialOrder_174 #

d_'8804''45'isTotalOrder_2816 :: T_IsTotalOrder_404 #

d_'8804''45'isDecTotalOrder_2818 :: T_IsDecTotalOrder_460 #

d_'8804''45'preorder_2820 :: T_Preorder_132 #

d_'8804''45'totalPreorder_2822 :: T_TotalPreorder_222 #

d_'8804''45'poset_2824 :: T_Poset_314 #

d_'8804''45'totalOrder_2826 :: T_TotalOrder_764 #

d_'8804''45'decTotalOrder_2828 :: T_DecTotalOrder_866 #

d_s'8804's'45'injective_2834 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 -> T__'8801'__12 #

d_'8804''45'pred_2836 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'8804''45'pred_2836 :: T__'8804'__22 -> T__'8804'__22 #

d_m'8804'n'8658'm'8804'1'43'n_2838 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'8804'n'8658'm'8804'1'43'n_2838 :: T__'8804'__22 -> T__'8804'__22 #

d_n'8804'1'43'n_2844 :: Integer -> T__'8804'__22 #

d_1'43'n'8816'n_2846 :: Integer -> T__'8804'__22 -> T_Irrelevant_20 #

d_n'8804'0'8658'n'8801'0_2850 :: Integer -> T__'8804'__22 -> T__'8801'__12 #

d_n'8804'1'8658'n'8801'0'8744'n'8801'1_2852 :: Integer -> T__'8804'__22 -> T__'8846'__30 #

du_n'8804'1'8658'n'8801'0'8744'n'8801'1_2852 :: T__'8804'__22 -> T__'8846'__30 #

d_'60''8658''8804'_2854 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'60''8658''8804'_2854 :: T__'8804'__22 -> T__'8804'__22 #

d_'60''8658''8802'_2858 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 -> T_Irrelevant_20 #

d_'62''8658''8802'_2862 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 -> T_Irrelevant_20 #

d_'8804''8658''8815'_2864 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T_Irrelevant_20 #

d_'60''8658''8817'_2870 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T_Irrelevant_20 #

d_'60''8658''8815'_2876 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T_Irrelevant_20 #

d_'8816''8658''8814'_2882 :: Integer -> Integer -> (T__'8804'__22 -> T_Irrelevant_20) -> T__'8804'__22 -> T_Irrelevant_20 #

d_'8816''8658''62'_2888 :: Integer -> Integer -> (T__'8804'__22 -> T_Irrelevant_20) -> T__'8804'__22 #

du_'8816''8658''62'_2888 :: Integer -> Integer -> T__'8804'__22 #

d_'8816''8658''8805'_2900 :: Integer -> Integer -> (T__'8804'__22 -> T_Irrelevant_20) -> T__'8804'__22 #

du_'8816''8658''8805'_2900 :: Integer -> Integer -> T__'8804'__22 #

d_'8814''8658''8805'_2902 :: Integer -> Integer -> (T__'8804'__22 -> T_Irrelevant_20) -> T__'8804'__22 #

du_'8814''8658''8805'_2902 :: Integer -> Integer -> T__'8804'__22 #

d_'8804''8743''8802''8658''60'_2918 :: Integer -> Integer -> T__'8804'__22 -> (T__'8801'__12 -> T_Irrelevant_20) -> T__'8804'__22 #

du_'8804''8743''8802''8658''60'_2918 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'8804''8743''8814''8658''8801'_2936 :: Integer -> Integer -> T__'8804'__22 -> (T__'8804'__22 -> T_Irrelevant_20) -> T__'8801'__12 #

d_'8804''45''60''45'connex_2942 :: Integer -> Integer -> T__'8846'__30 #

d_'8805''45''62''45'connex_2964 :: Integer -> Integer -> T__'8846'__30 #

d_'60''45''8804''45'connex_2966 :: Integer -> Integer -> T__'8846'__30 #

d_'62''45''8805''45'connex_2968 :: Integer -> Integer -> T__'8846'__30 #

d_'60''45'irrefl_2970 :: Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 -> T_Irrelevant_20 #

d_'60''45'asym_2974 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T_Irrelevant_20 #

d_'60''45'trans_2980 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

du_'60''45'trans_2980 :: Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8804''45''60''45'trans_2986 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

du_'8804''45''60''45'trans_2986 :: T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'60''45''8804''45'trans_2992 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

du_'60''45''8804''45'trans_2992 :: T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'60''45'cmp_2998 :: Integer -> Integer -> T_Tri_158 #

d__'60''63'__3030 :: Integer -> Integer -> T_Dec_20 #

d__'62''63'__3036 :: Integer -> Integer -> T_Dec_20 #

d_'60''45'irrelevant_3038 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 #

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

d_'60''45'isStrictPartialOrder_3046 :: T_IsStrictPartialOrder_290 #

d_'60''45'isStrictTotalOrder_3048 :: T_IsStrictTotalOrder_534 #

d_'60''45'strictPartialOrder_3050 :: T_StrictPartialOrder_556 #

d_'60''45'strictTotalOrder_3052 :: T_StrictTotalOrder_1036 #

d_s'60's'45'injective_3058 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 -> T__'8801'__12 #

d_'60''45'pred_3060 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'60''45'pred_3060 :: T__'8804'__22 -> T__'8804'__22 #

d_m'60'n'8658'm'60'1'43'n_3062 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'60'n'8658'm'60'1'43'n_3062 :: T__'8804'__22 -> T__'8804'__22 #

d_n'8814'0_3066 :: Integer -> T__'8804'__22 -> T_Irrelevant_20 #

d_n'8814'n_3070 :: Integer -> T__'8804'__22 -> T_Irrelevant_20 #

d_0'60'1'43'n_3074 :: Integer -> T__'8804'__22 #

du_0'60'1'43'n_3074 :: T__'8804'__22 #

d_n'60'1'43'n_3078 :: Integer -> T__'8804'__22 #

d_n'60'1'8658'n'8801'0_3082 :: Integer -> T__'8804'__22 -> T__'8801'__12 #

d_n'62'0'8658'n'8802'0_3086 :: Integer -> T__'8804'__22 -> T__'8801'__12 -> T_Irrelevant_20 #

d_n'8802'0'8658'n'62'0_3090 :: Integer -> (T__'8801'__12 -> T_Irrelevant_20) -> T__'8804'__22 #

du_n'8802'0'8658'n'62'0_3090 :: Integer -> T__'8804'__22 #

d_m'60'n'8658'0'60'n_3096 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'60'n'8658'0'60'n_3096 :: T__'8804'__22 -> T__'8804'__22 #

d_m'60'n'8658'n'8802'0_3098 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 -> T_Irrelevant_20 #

d_m'60'n'8658'm'8804'1'43'n_3102 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'60'n'8658'm'8804'1'43'n_3102 :: T__'8804'__22 -> T__'8804'__22 #

d_m'60'1'43'n'8658'm'60'n'8744'm'8801'n_3108 :: Integer -> Integer -> T__'8804'__22 -> T__'8846'__30 #

d_m'8804'n'8658'm'60'n'8744'm'8801'n_3118 :: Integer -> Integer -> T__'8804'__22 -> T__'8846'__30 #

d_m'60'1'43'n'8658'm'8804'n_3122 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'60'1'43'n'8658'm'8804'n_3122 :: T__'8804'__22 -> T__'8804'__22 #

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 #

du_'8704''91'm'8804'n'8658'm'8802'o'93''8658'n'60'o_3132 :: Integer -> Integer -> T__'8804'__22 #

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 #

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 #

du_'8704''91'm'60'n'8658'm'8802'o'93''8658'n'8804'o_3160 :: Integer -> Integer -> T__'8804'__22 #

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 #

d__IsRelatedTo__3188 :: p -> p -> () #

d__'8718'_3190 :: Integer -> T__IsRelatedTo__78 #

d_'60''45'go_3192 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__IsRelatedTo__78 -> T__IsRelatedTo__78 #

d_IsEquality_3194 :: p -> p -> p -> () #

d_IsEquality'63'_3196 :: Integer -> Integer -> T__IsRelatedTo__78 -> T_Dec_20 #

d_IsStrict_3198 :: p -> p -> p -> () #

d_IsStrict'63'_3200 :: Integer -> Integer -> T__IsRelatedTo__78 -> T_Dec_20 #

d_begin__3202 :: Integer -> Integer -> T__IsRelatedTo__78 -> T__'8804'__22 #

d_begin'45'contradiction__3204 :: Integer -> T__IsRelatedTo__78 -> AgdaAny -> T_Level_18 -> () -> AgdaAny #

d_begin__3206 :: Integer -> Integer -> T__IsRelatedTo__78 -> AgdaAny -> T__'8801'__12 #

d_begin__3208 :: Integer -> Integer -> T__IsRelatedTo__78 -> AgdaAny -> T__'8804'__22 #

d_eqRelation_3210 :: T_SubRelation_60 #

d_extractEquality_3214 :: Integer -> Integer -> T__IsRelatedTo__78 -> T_IsEquality_208 -> T__'8801'__12 #

d_extractStrict_3216 :: Integer -> Integer -> T__IsRelatedTo__78 -> T_IsStrict_172 -> T__'8804'__22 #

d_start_3224 :: Integer -> Integer -> T__IsRelatedTo__78 -> T__'8804'__22 #

d_step'45''60'_3226 :: Integer -> Integer -> Integer -> T__IsRelatedTo__78 -> T__'8804'__22 -> T__IsRelatedTo__78 #

d_step'45''8801'_3228 :: Integer -> Integer -> Integer -> T__IsRelatedTo__78 -> T__'8801'__12 -> T__IsRelatedTo__78 #

d_step'45''8801''45''8739'_3230 :: Integer -> Integer -> T__IsRelatedTo__78 -> T__IsRelatedTo__78 #

du_step'45''8801''45''8739'_3230 :: T__IsRelatedTo__78 -> T__IsRelatedTo__78 #

d_step'45''8801''45''10216'_3232 :: Integer -> Integer -> Integer -> T__IsRelatedTo__78 -> T__'8801'__12 -> T__IsRelatedTo__78 #

d_step'45''8801''45''10217'_3234 :: Integer -> Integer -> Integer -> T__IsRelatedTo__78 -> T__'8801'__12 -> T__IsRelatedTo__78 #

d_step'45''8801''728'_3236 :: Integer -> Integer -> Integer -> T__IsRelatedTo__78 -> T__'8801'__12 -> T__IsRelatedTo__78 #

d_step'45''8804'_3238 :: Integer -> Integer -> Integer -> T__IsRelatedTo__78 -> T__'8804'__22 -> T__IsRelatedTo__78 #

d_stop_3240 :: Integer -> T__IsRelatedTo__78 #

d_strictRelation_3244 :: T_SubRelation_60 #

d_'8776''45'go_3246 :: Integer -> Integer -> Integer -> T__'8801'__12 -> T__IsRelatedTo__78 -> T__IsRelatedTo__78 #

d_'8801''45'go_3248 :: Integer -> Integer -> Integer -> T__'8801'__12 -> T__IsRelatedTo__78 -> T__IsRelatedTo__78 #

du_'8801''45'go_3248 :: T__IsRelatedTo__78 -> T__IsRelatedTo__78 #

d_'8804''45'go_3250 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__IsRelatedTo__78 -> T__IsRelatedTo__78 #

d_'43''45'suc_3272 :: Integer -> Integer -> T__'8801'__12 #

d_'43''45'assoc_3280 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'43''45'identity'737'_3288 :: Integer -> T__'8801'__12 #

d_'43''45'identity'691'_3290 :: Integer -> T__'8801'__12 #

d_'43''45'identity_3294 :: T_Σ_14 #

d_'43''45'comm_3296 :: Integer -> Integer -> T__'8801'__12 #

d_'43''45'cancel'737''45''8801'_3304 :: Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_'43''45'cancel'691''45''8801'_3312 :: Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_'43''45'cancel'45''8801'_3314 :: T_Σ_14 #

d_'43''45'isMagma_3316 :: T_IsMagma_176 #

d_'43''45'isSemigroup_3318 :: T_IsSemigroup_472 #

d_'43''45'isCommutativeSemigroup_3320 :: T_IsCommutativeSemigroup_548 #

d_'43''45'0'45'isMonoid_3322 :: T_IsMonoid_686 #

d_'43''45'0'45'isCommutativeMonoid_3324 :: T_IsCommutativeMonoid_736 #

d_'43''45'magma_3326 :: T_Magma_68 #

d_'43''45'semigroup_3328 :: T_Semigroup_536 #

d_'43''45'commutativeSemigroup_3330 :: T_CommutativeSemigroup_662 #

d_'43''45'0'45'monoid_3332 :: T_Monoid_882 #

d_'43''45'0'45'commutativeMonoid_3334 :: T_CommutativeMonoid_962 #

d_'8760''45'magma_3336 :: T_Magma_68 #

d_m'8802'1'43'm'43'n_3342 :: Integer -> Integer -> T__'8801'__12 -> T_Irrelevant_20 #

d_m'8802'1'43'n'43'm_3352 :: Integer -> Integer -> T__'8801'__12 -> T_Irrelevant_20 #

d_m'43'1'43'n'8802'm_3362 :: Integer -> Integer -> T__'8801'__12 -> T_Irrelevant_20 #

d_m'43'1'43'n'8802'n_3370 :: Integer -> Integer -> T__'8801'__12 -> T_Irrelevant_20 #

d_m'43'1'43'n'8802'0_3384 :: Integer -> Integer -> T__'8801'__12 -> T_Irrelevant_20 #

d_m'43'n'8801'0'8658'm'8801'0_3398 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_m'43'n'8801'0'8658'n'8801'0_3406 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_'43''45'cancel'737''45''8804'_3414 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'43''45'cancel'737''45''8804'_3414 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'43''45'cancel'691''45''8804'_3422 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'43''45'cancel'691''45''8804'_3422 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'43''45'cancel'45''8804'_3432 :: T_Σ_14 #

d_'43''45'cancel'737''45''60'_3434 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'43''45'cancel'737''45''60'_3434 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'43''45'cancel'691''45''60'_3444 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'43''45'cancel'691''45''60'_3444 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'43''45'cancel'45''60'_3454 :: T_Σ_14 #

d_m'8804'n'8658'm'8804'o'43'n_3458 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'8804'n'8658'm'8804'o'43'n_3458 :: T__'8804'__22 -> T__'8804'__22 #

d_m'8804'n'8658'm'8804'n'43'o_3468 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'8804'n'8658'm'8804'n'43'o_3468 :: T__'8804'__22 -> T__'8804'__22 #

d_m'8804'm'43'n_3482 :: Integer -> Integer -> T__'8804'__22 #

du_m'8804'm'43'n_3482 :: Integer -> T__'8804'__22 #

d_m'8804'n'43'm_3494 :: Integer -> Integer -> T__'8804'__22 #

du_m'8804'n'43'm_3494 :: Integer -> T__'8804'__22 #

d_m'43'n'8804'o'8658'm'8804'o_3508 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'43'n'8804'o'8658'm'8804'o_3508 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'43'n'8804'o'8658'n'8804'o_3522 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'43'n'8804'o'8658'n'8804'o_3522 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'43''45'mono'45''8804'_3530 :: Integer -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

du_'43''45'mono'45''8804'_3530 :: Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'43''45'mono'737''45''8804'_3544 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'43''45'mono'737''45''8804'_3544 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'43''45'mono'691''45''8804'_3554 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'43''45'mono'691''45''8804'_3554 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'43''45'mono'45''60''45''8804'_3560 :: Integer -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

du_'43''45'mono'45''60''45''8804'_3560 :: T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'43''45'mono'45''8804''45''60'_3570 :: Integer -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

du_'43''45'mono'45''8804''45''60'_3570 :: Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'43''45'mono'45''60'_3580 :: Integer -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

du_'43''45'mono'45''60'_3580 :: Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'43''45'mono'737''45''60'_3588 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'43''45'mono'737''45''60'_3588 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'43''45'mono'691''45''60'_3596 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'43''45'mono'691''45''60'_3596 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'43'1'43'n'8816'm_3608 :: Integer -> Integer -> T__'8804'__22 -> T_Irrelevant_20 #

d_m'60'm'43'n_3618 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'60'm'43'n_3618 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'60'n'43'm_3630 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'60'n'43'm_3630 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'43'n'8814'n_3646 :: Integer -> Integer -> T__'8804'__22 -> T_Irrelevant_20 #

d_m'43'n'8814'm_3660 :: Integer -> Integer -> T__'8804'__22 -> T_Irrelevant_20 #

d_'42''45'suc_3672 :: Integer -> Integer -> T__'8801'__12 #

d_'42''45'identity'737'_3684 :: Integer -> T__'8801'__12 #

d_'42''45'identity'691'_3688 :: Integer -> T__'8801'__12 #

d_'42''45'identity_3692 :: T_Σ_14 #

d_'42''45'zero'737'_3694 :: Integer -> T__'8801'__12 #

d_'42''45'zero'691'_3696 :: Integer -> T__'8801'__12 #

d_'42''45'zero_3700 :: T_Σ_14 #

d_'42''45'comm_3702 :: Integer -> Integer -> T__'8801'__12 #

d_'42''45'distrib'691''45''43'_3712 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'42''45'distrib'737''45''43'_3726 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'42''45'distrib'45''43'_3728 :: T_Σ_14 #

d_'42''45'assoc_3730 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'42''45'isMagma_3744 :: T_IsMagma_176 #

d_'42''45'isSemigroup_3746 :: T_IsSemigroup_472 #

d_'42''45'isCommutativeSemigroup_3748 :: T_IsCommutativeSemigroup_548 #

d_'42''45'1'45'isMonoid_3750 :: T_IsMonoid_686 #

d_'42''45'1'45'isCommutativeMonoid_3752 :: T_IsCommutativeMonoid_736 #

d_'43''45''42''45'isSemiring_3754 :: T_IsSemiring_1570 #

d_'43''45''42''45'isCommutativeSemiring_3756 :: T_IsCommutativeSemiring_1678 #

d_'42''45'magma_3758 :: T_Magma_68 #

d_'42''45'semigroup_3760 :: T_Semigroup_536 #

d_'42''45'commutativeSemigroup_3762 :: T_CommutativeSemigroup_662 #

d_'42''45'1'45'monoid_3764 :: T_Monoid_882 #

d_'42''45'1'45'commutativeMonoid_3766 :: T_CommutativeMonoid_962 #

d_'43''45''42''45'semiring_3768 :: T_Semiring_2280 #

d_'43''45''42''45'commutativeSemiring_3770 :: T_CommutativeSemiring_2446 #

d_'42''45'cancel'691''45''8801'_3780 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12 -> T__'8801'__12 #

d_'42''45'cancel'737''45''8801'_3802 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8801'__12 -> T__'8801'__12 #

d_m'42'n'8801'0'8658'm'8801'0'8744'n'8801'0_3822 :: Integer -> Integer -> T__'8801'__12 -> T__'8846'__30 #

du_m'42'n'8801'0'8658'm'8801'0'8744'n'8801'0_3822 :: Integer -> T__'8846'__30 #

d_m'42'n'8802'0_3840 :: Integer -> Integer -> T_NonZero_112 -> T_NonZero_112 -> T_NonZero_112 #

du_m'42'n'8802'0_3840 :: T_NonZero_112 #

d_m'42'n'8802'0'8658'm'8802'0_3850 :: Integer -> Integer -> T_NonZero_112 -> T_NonZero_112 #

du_m'42'n'8802'0'8658'm'8802'0_3850 :: T_NonZero_112 #

d_m'42'n'8802'0'8658'n'8802'0_3856 :: Integer -> Integer -> T_NonZero_112 -> T_NonZero_112 #

du_m'42'n'8802'0'8658'n'8802'0_3856 :: T_NonZero_112 #

d_m'42'n'8801'0'8658'm'8801'0_3872 :: Integer -> Integer -> T_NonZero_112 -> T__'8801'__12 -> T__'8801'__12 #

d_m'42'n'8801'1'8658'm'8801'1_3880 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_m'42'n'8801'1'8658'n'8801'1_3894 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

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 #

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 #

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

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 #

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

d_'42''45'cancel'691''45''8804'_4030 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8804'__22 #

du_'42''45'cancel'691''45''8804'_4030 :: Integer -> T__'8804'__22 #

d_'42''45'cancel'737''45''8804'_4044 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8804'__22 #

du_'42''45'cancel'737''45''8804'_4044 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'42''45'mono'45''8804'_4060 :: Integer -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

du_'42''45'mono'45''8804'_4060 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'42''45'mono'737''45''8804'_4070 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'42''45'mono'737''45''8804'_4070 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'42''45'mono'691''45''8804'_4080 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'42''45'mono'691''45''8804'_4080 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'42''45'mono'45''60'_4086 :: Integer -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

du_'42''45'mono'45''60'_4086 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'42''45'mono'737''45''60'_4100 :: Integer -> T_NonZero_112 -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'42''45'mono'737''45''60'_4100 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'42''45'mono'691''45''60'_4114 :: Integer -> T_NonZero_112 -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'42''45'mono'691''45''60'_4114 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'8804'm'42'n_4128 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22 #

du_m'8804'm'42'n_4128 :: Integer -> Integer -> T__'8804'__22 #

d_m'8804'n'42'm_4140 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22 #

du_m'8804'n'42'm_4140 :: Integer -> Integer -> T__'8804'__22 #

d_m'60'm'42'n_4152 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8804'__22 #

du_m'60'm'42'n_4152 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'60'n'8658'm'60'n'42'o_4166 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8804'__22 #

du_m'60'n'8658'm'60'n'42'o_4166 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'60'n'8658'm'60'o'42'n_4182 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8804'__22 #

du_m'60'n'8658'm'60'o'42'n_4182 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'42''45'cancel'691''45''60'_4192 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'42''45'cancel'691''45''60'_4192 :: Integer -> Integer -> Integer -> T__'8804'__22 #

d_'42''45'cancel'737''45''60'_4208 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'42''45'cancel'45''60'_4224 :: T_Σ_14 #

d_'94''45'identity'691'_4226 :: Integer -> T__'8801'__12 #

d_'94''45'zero'737'_4230 :: Integer -> T__'8801'__12 #

d_'94''45'distrib'737''45''43''45''42'_4240 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'94''45'semigroup'45'morphism_4258 :: Integer -> T_IsSemigroupMorphism_148 #

du_'94''45'semigroup'45'morphism_4258 :: T_IsSemigroupMorphism_148 #

d_'94''45'monoid'45'morphism_4266 :: Integer -> T_IsMonoidMorphism_306 #

du_'94''45'monoid'45'morphism_4266 :: T_IsMonoidMorphism_306 #

d_'94''45''42''45'assoc_4274 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_m'94'n'8801'0'8658'm'8801'0_4296 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_m'94'n'8801'1'8658'n'8801'0'8744'm'8801'1_4308 :: Integer -> Integer -> T__'8801'__12 -> T__'8846'__30 #

du_m'94'n'8801'1'8658'n'8801'0'8744'm'8801'1_4308 :: Integer -> T__'8846'__30 #

d_m'94'n'8802'0_4324 :: Integer -> Integer -> T_NonZero_112 -> T_NonZero_112 #

du_m'94'n'8802'0_4324 :: Integer -> Integer -> T_NonZero_112 #

d_m'94'n'62'0_4336 :: Integer -> T_NonZero_112 -> Integer -> T__'8804'__22 #

du_m'94'n'62'0_4336 :: T__'8804'__22 #

d_'94''45'mono'737''45''8804'_4346 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'94''45'mono'737''45''8804'_4346 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'94''45'mono'691''45''8804'_4360 :: Integer -> T_NonZero_112 -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'94''45'mono'691''45''8804'_4360 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'94''45'mono'737''45''60'_4376 :: Integer -> T_NonZero_112 -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'94''45'mono'737''45''60'_4376 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'94''45'mono'691''45''60'_4388 :: Integer -> T__'8804'__22 -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'8804'n'8658'm'8852'n'8801'n_4406 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_m'8805'n'8658'm'8852'n'8801'm_4412 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_m'8804'n'8658'm'8851'n'8801'm_4422 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_m'8805'n'8658'm'8851'n'8801'n_4428 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_'8851''45'operator_4438 :: T_MinOperator_98 #

d_'8852''45'operator_4440 :: T_MaxOperator_128 #

d_'8852''8801''8852''8242'_4446 :: Integer -> Integer -> T__'8801'__12 #

d_'8851''8801''8851''8242'_4472 :: Integer -> Integer -> T__'8801'__12 #

d_x'8851'y'8804'x_4504 :: Integer -> Integer -> T__'8804'__22 #

d_x'8804'y'8658'x'8851'z'8804'y_4506 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_x'8804'y'8658'z'8851'x'8804'y_4508 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_x'8804'y'8658'x'8851'z'8804'y_4510 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_x'8804'y'8658'z'8851'x'8804'y_4512 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_x'8804'y'8851'z'8658'x'8804'y_4514 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_x'8804'y'8851'z'8658'x'8804'z_4516 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_x'8851'y'8804'y_4518 :: Integer -> Integer -> T__'8804'__22 #

d_x'8851'y'8776'x'8658'x'8804'y_4520 :: Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 #

d_x'8851'y'8776'y'8658'y'8804'x_4522 :: Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 #

d_x'8851'y'8804'x_4524 :: Integer -> Integer -> T__'8804'__22 #

d_x'8851'y'8804'x'8852'y_4526 :: Integer -> Integer -> T__'8804'__22 #

d_x'8851'y'8804'y_4528 :: Integer -> Integer -> T__'8804'__22 #

d_x'8851'y'8776'x'8658'x'8804'y_4530 :: Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 #

d_x'8851'y'8776'y'8658'y'8804'x_4532 :: Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 #

d_x'8804'y'8851'z'8658'x'8804'y_4534 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_x'8804'y'8851'z'8658'x'8804'z_4536 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'8851''45'absorbs'45''8852'_4538 :: Integer -> Integer -> T__'8801'__12 #

d_'8851''45'assoc_4540 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'8851''45'band_4542 :: T_Band_596 #

d_'8851''45'comm_4544 :: Integer -> Integer -> T__'8801'__12 #

d_'8851''45'commutativeSemigroup_4546 :: T_CommutativeSemigroup_662 #

d_'8851''45'distrib'45''8852'_4554 :: T_Σ_14 #

d_'8851''45'distrib'691''45''8852'_4556 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'8851''45'distrib'737''45''8852'_4558 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'8851''45'glb_4560 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8851''45'idem_4562 :: Integer -> T__'8801'__12 #

d_'8851''45'isBand_4570 :: T_IsBand_508 #

d_'8851''45'isCommutativeSemigroup_4572 :: T_IsCommutativeSemigroup_548 #

d_'8851''45'isMagma_4574 :: T_IsMagma_176 #

d_'8851''45'isSelectiveMagma_4578 :: T_IsSelectiveMagma_436 #

d_'8851''45'isSemigroup_4580 :: T_IsSemigroup_472 #

d_'8851''45'magma_4582 :: T_Magma_68 #

d_'8851''45'mono'45''8804'_4584 :: Integer -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8851''45'mono'691''45''8804'_4588 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'8851''45'mono'737''45''8804'_4590 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'8851''45'sel_4594 :: Integer -> Integer -> T__'8846'__30 #

d_'8851''45'selectiveMagma_4596 :: T_SelectiveMagma_122 #

d_'8851''45'semigroup_4598 :: T_Semigroup_536 #

d_'8851''45'triangulate_4600 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'8851''45''8852''45'absorptive_4608 :: T_Σ_14 #

d_'8852''45'absorbs'45''8851'_4610 :: Integer -> Integer -> T__'8801'__12 #

d_'8851''45'assoc_4612 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'8851''45'band_4614 :: T_Band_596 #

d_'8851''45'comm_4616 :: Integer -> Integer -> T__'8801'__12 #

d_'8851''45'commutativeSemigroup_4618 :: T_CommutativeSemigroup_662 #

d_'8852''45'distrib'45''8851'_4626 :: T_Σ_14 #

d_'8852''45'distrib'691''45''8851'_4628 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'8852''45'distrib'737''45''8851'_4630 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'8851''45'idem_4632 :: Integer -> T__'8801'__12 #

d_'8851''45'isBand_4640 :: T_IsBand_508 #

d_'8851''45'isCommutativeSemigroup_4642 :: T_IsCommutativeSemigroup_548 #

d_'8851''45'isMagma_4644 :: T_IsMagma_176 #

d_'8851''45'isSelectiveMagma_4648 :: T_IsSelectiveMagma_436 #

d_'8851''45'isSemigroup_4650 :: T_IsSemigroup_472 #

d_'8851''45'glb_4652 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8851''45'magma_4654 :: T_Magma_68 #

d_'8851''45'mono'45''8804'_4656 :: Integer -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8851''45'mono'691''45''8804'_4660 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'8851''45'mono'737''45''8804'_4662 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'8851''45'sel_4664 :: Integer -> Integer -> T__'8846'__30 #

d_'8851''45'selectiveMagma_4666 :: T_SelectiveMagma_122 #

d_'8851''45'semigroup_4668 :: T_Semigroup_536 #

d_'8851''45'triangulate_4670 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'8852''45''8851''45'absorptive_4678 :: T_Σ_14 #

d_'8851''45'isSemilattice_4682 :: T_IsCommutativeBand_590 #

d_'8851''45'semilattice_4684 :: T_Semilattice_10 #

d_'8851''45''8852''45'distributiveLattice_4686 :: T_DistributiveLattice_584 #

d_'8851''45''8852''45'isDistributiveLattice_4688 :: T_IsDistributiveLattice_3036 #

d_'8851''45''8852''45'isLattice_4690 :: T_IsLattice_2962 #

d_'8851''45''8852''45'lattice_4692 :: T_Lattice_500 #

d_'8851''45'isSemilattice_4694 :: T_IsCommutativeBand_590 #

d_'8851''45'semilattice_4696 :: T_Semilattice_10 #

d_'8852''45''8851''45'distributiveLattice_4698 :: T_DistributiveLattice_584 #

d_'8852''45''8851''45'isDistributiveLattice_4700 :: T_IsDistributiveLattice_3036 #

d_'8852''45''8851''45'isLattice_4702 :: T_IsLattice_2962 #

d_'8852''45''8851''45'lattice_4704 :: T_Lattice_500 #

d_'8852''45'identity'737'_4706 :: Integer -> T__'8801'__12 #

d_'8852''45'identity'691'_4708 :: Integer -> T__'8801'__12 #

d_'8852''45'identity_4712 :: T_Σ_14 #

d_'8852''45'0'45'isMonoid_4714 :: T_IsMonoid_686 #

d_'8852''45'0'45'isCommutativeMonoid_4716 :: T_IsCommutativeMonoid_736 #

d_'8852''45'0'45'monoid_4718 :: T_Monoid_882 #

d_'8852''45'0'45'commutativeMonoid_4720 :: T_CommutativeMonoid_962 #

d_mono'45''8804''45'distrib'45''8852'_4728 :: (Integer -> Integer) -> (Integer -> Integer -> T__'8804'__22 -> T__'8804'__22) -> Integer -> Integer -> T__'8801'__12 #

d_mono'45''8804''45'distrib'45''8851'_4738 :: (Integer -> Integer) -> (Integer -> Integer -> T__'8804'__22 -> T__'8804'__22) -> Integer -> Integer -> T__'8801'__12 #

d_antimono'45''8804''45'distrib'45''8851'_4748 :: (Integer -> Integer) -> (Integer -> Integer -> T__'8804'__22 -> T__'8804'__22) -> Integer -> Integer -> T__'8801'__12 #

d_antimono'45''8804''45'distrib'45''8852'_4758 :: (Integer -> Integer) -> (Integer -> Integer -> T__'8804'__22 -> T__'8804'__22) -> Integer -> Integer -> T__'8801'__12 #

d_m'60'n'8658'm'60'n'8852'o_4764 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'60'n'8658'm'60'o'8852'n_4768 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'8852'n'60'o'8658'm'60'o_4776 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'8852'n'60'o'8658'm'60'o_4776 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'8852'n'60'o'8658'n'60'o_4790 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'8852'n'60'o'8658'n'60'o_4790 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'8852''45'mono'45''60'_4798 :: Integer -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8852''45'pres'45''60'm_4800 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'43''45'distrib'737''45''8852'_4810 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'43''45'distrib'691''45''8852'_4822 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'43''45'distrib'45''8852'_4824 :: T_Σ_14 #

d_m'8852'n'8804'm'43'n_4830 :: Integer -> Integer -> T__'8804'__22 #

d_'42''45'distrib'737''45''8852'_4860 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'42''45'distrib'691''45''8852'_4882 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'42''45'distrib'45''8852'_4884 :: T_Σ_14 #

d_'8851''45'zero'737'_4886 :: Integer -> T__'8801'__12 #

d_'8851''45'zero'691'_4888 :: Integer -> T__'8801'__12 #

d_'8851''45'zero_4892 :: T_Σ_14 #

d_'8852''45''8851''45'isSemiringWithoutOne_4894 :: T_IsSemiringWithoutOne_1298 #

d_'8852''45''8851''45'isCommutativeSemiringWithoutOne_4896 :: T_IsCommutativeSemiringWithoutOne_1382 #

d_'8852''45''8851''45'commutativeSemiringWithoutOne_4898 :: T_CommutativeSemiringWithoutOne_2002 #

d_m'60'n'8658'm'8851'o'60'n_4902 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'60'n'8658'm'8851'o'60'n_4902 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'60'n'8658'o'8851'm'60'n_4910 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'60'n'8658'o'8851'm'60'n_4910 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'60'n'8851'o'8658'm'60'n_4920 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'60'n'8851'o'8658'm'60'o_4926 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'8851''45'mono'45''60'_4928 :: Integer -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8851''45'pres'45'm'60'_4930 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'43''45'distrib'737''45''8851'_4940 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'43''45'distrib'691''45''8851'_4952 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'43''45'distrib'45''8851'_4954 :: T_Σ_14 #

d_m'8851'n'8804'm'43'n_4960 :: Integer -> Integer -> T__'8804'__22 #

d_'42''45'distrib'737''45''8851'_4990 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'42''45'distrib'691''45''8851'_5012 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'42''45'distrib'45''8851'_5014 :: T_Σ_14 #

d_0'8760'n'8801'0_5016 :: Integer -> T__'8801'__12 #

d_n'8760'n'8801'0_5020 :: Integer -> T__'8801'__12 #

d_pred'91'm'8760'n'93''8801'm'8760''91'1'43'n'93'_5028 :: Integer -> Integer -> T__'8801'__12 #

d_m'8760'n'8804'm_5042 :: Integer -> Integer -> T__'8804'__22 #

d_m'8814'm'8760'n_5056 :: Integer -> Integer -> T__'8804'__22 -> T_Irrelevant_20 #

d_1'43'm'8802'm'8760'n_5068 :: Integer -> Integer -> T__'8801'__12 -> T_Irrelevant_20 #

d_'8760''45'mono_5076 :: Integer -> Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8760''45'mono'737''45''8804'_5090 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'8760''45'mono'691''45''8804'_5098 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'8760''45'mono'737''45''60'_5108 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

du_'8760''45'mono'737''45''60'_5108 :: Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8760''45'mono'691''45''60'_5134 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8760''45'cancel'691''45''8804'_5156 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

du_'8760''45'cancel'691''45''8804'_5156 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'8760''45'cancel'691''45''60'_5176 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'8760''45'cancel'691''45''60'_5176 :: Integer -> Integer -> T__'8804'__22 #

d_'8760''45'cancel'737''45''8801'_5196 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 -> T__'8801'__12 #

d_'8760''45'cancel'691''45''8801'_5212 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12 -> T__'8801'__12 #

d_m'8760'n'8801'0'8658'm'8804'n_5222 :: Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 #

du_m'8760'n'8801'0'8658'm'8804'n_5222 :: Integer -> T__'8804'__22 #

d_m'8804'n'8658'm'8760'n'8801'0_5230 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_m'60'n'8658'0'60'n'8760'm_5236 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'60'n'8658'0'60'n'8760'm_5236 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'8760'n'8802'0'8658'n'60'm_5246 :: Integer -> Integer -> (T__'8801'__12 -> T_Irrelevant_20) -> T__'8804'__22 #

du_m'8760'n'8802'0'8658'n'60'm_5246 :: Integer -> Integer -> T__'8804'__22 #

d_m'62'n'8658'm'8760'n'8802'0_5274 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 -> T_Irrelevant_20 #

d_m'8804'n'8658'n'8760'm'8804'n_5280 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'8804'n'8658'n'8760'm'8804'n_5280 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'43''45''8760''45'comm_5290 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_'8760''45''43''45'assoc_5308 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'43''45''8760''45'assoc_5332 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_m'8804'n'43'o'8658'm'8760'n'8804'o_5354 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'8804'n'43'o'8658'm'8760'n'8804'o_5354 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

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 #

du_m'60'n'43'o'8658'm'8760'n'60'o_5374 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_m'43'n'8804'o'8658'm'8804'o'8760'n_5398 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_m'43'n'8804'o'8658'm'8804'o'8760'n_5398 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

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 #

du_m'8804'o'8760'n'8658'm'43'n'8804'o_5418 :: T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_m'8804'n'43'm'8760'n_5444 :: Integer -> Integer -> T__'8804'__22 #

d_m'43'n'8760'n'8801'm_5458 :: Integer -> Integer -> T__'8801'__12 #

d_m'43'n'8760'm'8801'n_5470 :: Integer -> Integer -> T__'8801'__12 #

d_m'43''91'n'8760'm'93''8801'n_5478 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_m'8760'n'43'n'8801'm_5492 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_m'8760''91'm'8760'n'93''8801'n_5504 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_'91'm'43'n'93''8760''91'm'43'o'93''8801'n'8760'o_5520 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'42''45'distrib'691''45''8760'_5532 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'42''45'distrib'737''45''8760'_5552 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'42''45'distrib'45''8760'_5554 :: T_Σ_14 #

d_even'8802'odd_5560 :: Integer -> Integer -> T__'8801'__12 -> T_Irrelevant_20 #

d_m'8851'n'43'n'8760'm'8801'n_5576 :: Integer -> Integer -> T__'8801'__12 #

d_'91'm'8760'n'93''8851''91'n'8760'm'93''8801'0_5590 :: Integer -> Integer -> T__'8801'__12 #

d_'8760''45'distrib'737''45''8851''45''8852'_5606 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'8760''45'distrib'691''45''8851'_5614 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'8760''45'distrib'737''45''8852''45''8851'_5628 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'8760''45'distrib'691''45''8852'_5636 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_pred'91'n'93''8804'n_5644 :: Integer -> T__'8804'__22 #

d_'8804'pred'8658''8804'_5648 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'8804'pred'8658''8804'_5648 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'8804''8658'pred'8804'_5656 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'8804''8658'pred'8804'_5656 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'60''8658''8804'pred_5664 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'60''8658''8804'pred_5664 :: T__'8804'__22 -> T__'8804'__22 #

d_suc'45'pred_5672 :: Integer -> T_NonZero_112 -> T__'8801'__12 #

d_pred'45'mono'45''8804'_5676 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_pred'45'mono'45''8804'_5676 :: Integer -> T__'8804'__22 -> T__'8804'__22 #

d_pred'45'mono'45''60'_5680 :: Integer -> Integer -> T_NonZero_112 -> T__'8804'__22 -> T__'8804'__22 #

du_pred'45'mono'45''60'_5680 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_pred'45'cancel'45''8804'_5682 :: Integer -> Integer -> T__'8804'__22 -> T__'8846'__30 #

d_pred'45'cancel'45''60'_5686 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_pred'45'injective_5688 :: Integer -> Integer -> T_NonZero_112 -> T_NonZero_112 -> T__'8801'__12 -> T__'8801'__12 #

d_pred'45'cancel'45''8801'_5694 :: Integer -> Integer -> T__'8801'__12 -> T__'8846'__30 #

d_m'8801'n'8658''8739'm'45'n'8739''8801'0_5696 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_'8739'm'45'n'8739''8801'0'8658'm'8801'n_5700 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_m'8804'n'8658''8739'n'45'm'8739''8801'n'8760'm_5710 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_m'8804'n'8658''8739'm'45'n'8739''8801'n'8760'm_5716 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_'8739'm'45'n'8739''8801'm'8760'n'8658'n'8804'm_5722 :: Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 #

du_'8739'm'45'n'8739''8801'm'8760'n'8658'n'8804'm_5722 :: Integer -> Integer -> T__'8804'__22 #

d_'8739'n'45'n'8739''8801'0_5738 :: Integer -> T__'8801'__12 #

d_'8739'm'45'm'43'n'8739''8801'n_5746 :: Integer -> Integer -> T__'8801'__12 #

d_'8739'm'43'n'45'm'43'o'8739''8801''8739'n'45'o'8739'_5760 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_m'8760'n'8804''8739'm'45'n'8739'_5776 :: Integer -> Integer -> T__'8804'__22 #

d_'8739'm'45'n'8739''8804'm'8852'n_5806 :: Integer -> Integer -> T__'8804'__22 #

d_'8739''45''8739''45'identity'737'_5816 :: Integer -> T__'8801'__12 #

d_'8739''45''8739''45'identity'691'_5820 :: Integer -> T__'8801'__12 #

d_'8739''45''8739''45'identity_5824 :: T_Σ_14 #

d_'8739''45''8739''45'comm_5826 :: Integer -> Integer -> T__'8801'__12 #

d_'8739'm'45'n'8739''8801''91'm'8760'n'93''8744''91'n'8760'm'93'_5840 :: Integer -> Integer -> T__'8846'__30 #

d_'42''45'distrib'737''45''8739''45''8739''45'aux_5868 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_'42''45'distrib'737''45''8739''45''8739'_5880 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'42''45'distrib'691''45''8739''45''8739'_5910 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_'42''45'distrib'45''8739''45''8739'_5912 :: T_Σ_14 #

d_m'8804'n'43''8739'n'45'm'8739'_5918 :: Integer -> Integer -> T__'8804'__22 #

d_m'8804'n'43''8739'm'45'n'8739'_5932 :: Integer -> Integer -> T__'8804'__22 #

d_m'8804''8739'm'45'n'8739''43'n_5946 :: Integer -> Integer -> T__'8804'__22 #

d_'8739''45''8739''45'triangle_5954 :: Integer -> Integer -> Integer -> T__'8804'__22 #

d_'8739''45''8739''8801''8739''45''8739''8242'_5986 :: Integer -> Integer -> T__'8801'__12 #

d_'8739''45''8739''45'isProtoMetric_6008 :: T_IsProtoMetric_30 #

d_'8739''45''8739''45'isPreMetric_6010 :: T_IsPreMetric_102 #

d_'8739''45''8739''45'isQuasiSemiMetric_6012 :: T_IsQuasiSemiMetric_174 #

d_'8739''45''8739''45'isSemiMetric_6014 :: T_IsSemiMetric_250 #

d_'8739''45''8739''45'isMetric_6016 :: T_IsGeneralMetric_332 #

d_'8739''45''8739''45'quasiSemiMetric_6018 :: T_QuasiSemiMetric_186 #

d_'8739''45''8739''45'semiMetric_6020 :: T_SemiMetric_284 #

d_'8739''45''8739''45'preMetric_6022 :: T_PreMetric_96 #

d_'8739''45''8739''45'metric_6024 :: T_Metric_388 #

d_'8970'n'47'2'8971''45'mono_6026 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'8970'n'47'2'8971''45'mono_6026 :: T__'8804'__22 -> T__'8804'__22 #

d_'8968'n'47'2'8969''45'mono_6030 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'8968'n'47'2'8969''45'mono_6030 :: T__'8804'__22 -> T__'8804'__22 #

d_'8970'n'47'2'8971''8804''8968'n'47'2'8969'_6036 :: Integer -> T__'8804'__22 #

d_'8970'n'47'2'8971''43''8968'n'47'2'8969''8801'n_6042 :: Integer -> T__'8801'__12 #

d_'8970'n'47'2'8971''8804'n_6048 :: Integer -> T__'8804'__22 #

d_'8970'n'47'2'8971''60'n_6054 :: Integer -> T__'8804'__22 #

d_n'8801''8970'n'43'n'47'2'8971'_6060 :: Integer -> T__'8801'__12 #

d_'8968'n'47'2'8969''8804'n_6068 :: Integer -> T__'8804'__22 #

d_'8968'n'47'2'8969''60'n_6074 :: Integer -> T__'8804'__22 #

d_n'8801''8968'n'43'n'47'2'8969'_6080 :: Integer -> T__'8801'__12 #

d_1'8804'n'33'_6088 :: Integer -> T__'8804'__22 #

d__'33''8802'0_6094 :: Integer -> T_NonZero_112 #

d__'33''42'_'33''8802'0_6102 :: Integer -> Integer -> T_NonZero_112 #

du__'33''42'_'33''8802'0_6102 :: T_NonZero_112 #

d_'8804''8242''45'trans_6108 :: Integer -> Integer -> Integer -> T__'8804''8242'__338 -> T__'8804''8242'__338 -> T__'8804''8242'__338 #

du_'8804''8242''45'trans_6108 :: T__'8804''8242'__338 -> T__'8804''8242'__338 -> T__'8804''8242'__338 #

d_z'8804''8242'n_6116 :: Integer -> T__'8804''8242'__338 #

d_s'8804''8242's_6120 :: Integer -> Integer -> T__'8804''8242'__338 -> T__'8804''8242'__338 #

du_s'8804''8242's_6120 :: T__'8804''8242'__338 -> T__'8804''8242'__338 #

d_'8804''8242''8658''8804'_6124 :: Integer -> Integer -> T__'8804''8242'__338 -> T__'8804'__22 #

du_'8804''8242''8658''8804'_6124 :: Integer -> T__'8804''8242'__338 -> T__'8804'__22 #

d_'8804''8658''8804''8242'_6128 :: Integer -> Integer -> T__'8804'__22 -> T__'8804''8242'__338 #

du_'8804''8658''8804''8242'_6128 :: Integer -> T__'8804'__22 -> T__'8804''8242'__338 #

d_'8804''8242''45'step'45'injective_6136 :: Integer -> Integer -> T__'8804''8242'__338 -> T__'8804''8242'__338 -> T__'8801'__12 -> T__'8801'__12 #

d_z'60''8242's_6138 :: Integer -> T__'8804''8242'__338 #

d_s'60''8242's_6142 :: Integer -> Integer -> T__'8804''8242'__338 -> T__'8804''8242'__338 #

du_s'60''8242's_6142 :: T__'8804''8242'__338 -> T__'8804''8242'__338 #

d_'60''8658''60''8242'_6146 :: Integer -> Integer -> T__'8804'__22 -> T__'8804''8242'__338 #

du_'60''8658''60''8242'_6146 :: Integer -> T__'8804'__22 -> T__'8804''8242'__338 #

d_'60''8242''8658''60'_6150 :: Integer -> Integer -> T__'8804''8242'__338 -> T__'8804'__22 #

du_'60''8242''8658''60'_6150 :: Integer -> T__'8804''8242'__338 -> T__'8804'__22 #

d_m'60'1'43'n'8658'm'60'n'8744'm'8801'n'8242'_6154 :: Integer -> Integer -> T__'8804'__22 -> T__'8846'__30 #

d__'8804''8242''63'__6168 :: Integer -> Integer -> T_Dec_20 #

d__'60''8242''63'__6174 :: Integer -> Integer -> T_Dec_20 #

d__'8805''8242''63'__6180 :: Integer -> Integer -> T_Dec_20 #

d__'62''8242''63'__6182 :: Integer -> Integer -> T_Dec_20 #

d_m'8804''8242'm'43'n_6188 :: Integer -> Integer -> T__'8804''8242'__338 #

d_n'8804''8242'm'43'n_6198 :: Integer -> Integer -> T__'8804''8242'__338 #

du_n'8804''8242'm'43'n_6198 :: Integer -> T__'8804''8242'__338 #

d_'8968'n'47'2'8969''8804''8242'n_6208 :: Integer -> T__'8804''8242'__338 #

d_'8970'n'47'2'8971''8804''8242'n_6214 :: Integer -> T__'8804''8242'__338 #

d_'8804''8658''8804''8243'_6218 :: Integer -> Integer -> T__'8804'__22 -> T__'8739''737'__26 #

du_'8804''8658''8804''8243'_6218 :: Integer -> Integer -> T__'8739''737'__26 #

d_'60''8658''60''8243'_6222 :: Integer -> Integer -> T__'8804'__22 -> T__'8739''737'__26 #

d_'8804''8243''8658''8804'_6224 :: Integer -> Integer -> T__'8739''737'__26 -> T__'8804'__22 #

du_'8804''8243''8658''8804'_6224 :: Integer -> T__'8739''737'__26 -> T__'8804'__22 #

d_'8804''8243''45'proof_6232 :: Integer -> Integer -> T__'8739''737'__26 -> T__'8801'__12 #

d_m'8804'n'8658''8707''91'o'93'm'43'o'8801'n_6238 :: Integer -> Integer -> T__'8804'__22 -> T_Σ_14 #

du_m'8804'n'8658''8707''91'o'93'm'43'o'8801'n_6238 :: Integer -> Integer -> T_Σ_14 #

d_guarded'45''8760''8791''8760'_6250 :: T__'8804'__22 -> T__'8801'__12 #

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 #

d_m'60''7495'1'43'm'43'n_6270 :: Integer -> Integer -> AgdaAny #

du_m'60''7495'1'43'm'43'n_6270 :: Integer -> AgdaAny #

d_'60''7495''8658''60''8243'_6274 :: Integer -> Integer -> AgdaAny -> T__'8739''737'__26 #

du_'60''7495''8658''60''8243'_6274 :: Integer -> Integer -> T__'8739''737'__26 #

d_'60''8243''8658''60''7495'_6284 :: Integer -> Integer -> T__'8739''737'__26 -> AgdaAny #

du_'60''8243''8658''60''7495'_6284 :: Integer -> T__'8739''737'__26 -> AgdaAny #

d__'60''8243''63'__6290 :: Integer -> Integer -> T_Dec_20 #

d__'8804''8243''63'__6296 :: Integer -> Integer -> T_Dec_20 #

d__'8805''8243''63'__6304 :: Integer -> Integer -> T_Dec_20 #

d__'62''8243''63'__6306 :: Integer -> Integer -> T_Dec_20 #

d_'8804''8243''45'irrelevant_6308 :: Integer -> Integer -> T__'8739''737'__26 -> T__'8739''737'__26 -> T__'8801'__12 #

d_'60''8243''45'irrelevant_6322 :: Integer -> Integer -> T__'8739''737'__26 -> T__'8739''737'__26 -> T__'8801'__12 #

d_'62''8243''45'irrelevant_6324 :: Integer -> Integer -> T__'8739''737'__26 -> T__'8739''737'__26 -> T__'8801'__12 #

d_'8805''8243''45'irrelevant_6326 :: Integer -> Integer -> T__'8739''737'__26 -> T__'8739''737'__26 -> T__'8801'__12 #

d_'8804''8244''8658''8804''8243'_6332 :: Integer -> Integer -> T__'8804''8244'__408 -> T__'8739''737'__26 #

du_'8804''8244''8658''8804''8243'_6332 :: T__'8804''8244'__408 -> T__'8739''737'__26 #

d_m'8804''8244'm'43'k_6346 :: Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8804''8244'__408 #

du_m'8804''8244'm'43'k_6346 :: Integer -> T__'8804''8244'__408 #

d_'8804''8243''8658''8804''8244'_6362 :: Integer -> Integer -> T__'8739''737'__26 -> T__'8804''8244'__408 #

du_'8804''8243''8658''8804''8244'_6362 :: T__'8739''737'__26 -> T__'8804''8244'__408 #

d_0'8804''8244'n_6366 :: Integer -> T__'8804''8244'__408 #

d_'60''7495''8658''60''8244'_6368 :: Integer -> Integer -> AgdaAny -> T__'8804''8244'__408 #

du_'60''7495''8658''60''8244'_6368 :: Integer -> Integer -> T__'8804''8244'__408 #

d_'60''8244''8658''60''7495'_6376 :: Integer -> Integer -> T__'8804''8244'__408 -> AgdaAny #

du_'60''8244''8658''60''7495'_6376 :: Integer -> T__'8804''8244'__408 -> AgdaAny #

d__'60''8244''63'__6380 :: Integer -> Integer -> T_Dec_20 #

d__'8804''8244''63'__6386 :: Integer -> Integer -> T_Dec_20 #

d__'8805''8244''63'__6394 :: Integer -> Integer -> T_Dec_20 #

d__'62''8244''63'__6396 :: Integer -> Integer -> T_Dec_20 #

d_'8804''8658''8804''8244'_6398 :: Integer -> Integer -> T__'8804'__22 -> T__'8804''8244'__408 #

du_'8804''8658''8804''8244'_6398 :: Integer -> Integer -> T__'8804''8244'__408 #

d_'8804''8244''8658''8804'_6400 :: Integer -> Integer -> T__'8804''8244'__408 -> T__'8804'__22 #

du_'8804''8244''8658''8804'_6400 :: Integer -> T__'8804''8244'__408 -> T__'8804'__22 #

d_eq'63'_6406 :: T_Level_18 -> () -> T_Injection_776 -> AgdaAny -> AgdaAny -> T_Dec_20 #

du_eq'63'_6406 :: T_Injection_776 -> AgdaAny -> AgdaAny -> T_Dec_20 #

d_anyUpTo'63'_6424 :: T_Level_18 -> (Integer -> ()) -> (Integer -> T_Dec_20) -> Integer -> T_Dec_20 #

du_anyUpTo'63'_6424 :: (Integer -> T_Dec_20) -> Integer -> T_Dec_20 #

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 #

d_allUpTo'63'_6488 :: T_Level_18 -> (Integer -> ()) -> (Integer -> T_Dec_20) -> Integer -> T_Dec_20 #

du_allUpTo'63'_6488 :: (Integer -> T_Dec_20) -> Integer -> T_Dec_20 #

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 #

du_Pn'60'1'43'v_6520 :: Integer -> AgdaAny -> (Integer -> T__'8804'__22 -> AgdaAny) -> Integer -> T__'8804'__22 -> AgdaAny #

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 #

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 #

d_'42''45''43''45'isSemiring_6556 :: T_IsSemiring_1570 #

d_'42''45''43''45'isCommutativeSemiring_6558 :: T_IsCommutativeSemiring_1678 #

d_'42''45''43''45'semiring_6560 :: T_Semiring_2280 #

d_'42''45''43''45'commutativeSemiring_6562 :: T_CommutativeSemiring_2446 #

d_'8739'm'43'n'45'm'43'o'8739''8801''8739'n'45'o'124'_6564 :: Integer -> Integer -> Integer -> T__'8801'__12 #

d_m'8804'n'8658'n'8852'm'8801'n_6566 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_m'8804'n'8658'n'8851'm'8801'm_6568 :: Integer -> Integer -> T__'8804'__22 -> T__'8801'__12 #

d_n'8852'm'8801'm'8658'n'8804'm_6570 :: Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 #

d_n'8852'm'8801'n'8658'm'8804'n_6572 :: Integer -> Integer -> T__'8801'__12 -> T__'8804'__22 #

d_n'8804'm'8852'n_6574 :: Integer -> Integer -> T__'8804'__22 #

d_'8852''45'least_6576 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8851''45'greatest_6578 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8852''45'pres'45''8804'm_6580 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8851''45'pres'45'm'8804'_6582 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'8852''45'abs'45''8851'_6584 :: Integer -> Integer -> T__'8801'__12 #

d_'8851''45'abs'45''8852'_6586 :: Integer -> Integer -> T__'8801'__12 #

d_suc'91'pred'91'n'93''93''8801'n_6588 :: Integer -> (T__'8801'__12 -> T_Irrelevant_20) -> T__'8801'__12 #

d_'8804''45'step_6594 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'8804''45'step_6594 :: T__'8804'__22 -> T__'8804'__22 #

d_'8804''45'steps'737'_6596 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'8804''45'steps'737'_6596 :: T__'8804'__22 -> T__'8804'__22 #

d_'8804''45'steps'691'_6598 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

du_'8804''45'steps'691'_6598 :: T__'8804'__22 -> T__'8804'__22 #

d_'60''45'step_6600 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_pred'45'mono_6602 :: Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 #

d_'60''45'trans'691'_6604 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #

d_'60''45'trans'737'_6606 :: Integer -> Integer -> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22 #