-- | generates the axioms of the module K
create_axs :: Set.Set SORT -> CASLSign -> CASLSign -> [Named CASLFORMULA]
              -> [Named CASLFORMULA]
create_axs sg_ss sg_m sg_k sens = forms
      where ss_m = sortSet sg_m
            ss = Set.map mkFreeName $ Set.difference ss_m sg_ss
            sr = sortRel sg_k
            comps = ops2comp $ opMap sg_k
            ss' = filterNoCtorSorts (opMap sg_k) ss
            ctor_sen = freeCons (ss', sr, comps)
            make_axs = make_forms sg_ss ++ make_hom_forms sg_ss
            h_axs_ops = homomorphism_axs_ops $ opMap sg_m
            h_axs_preds = homomorphism_axs_preds $ predMap sg_m
            h_axs_surj = hom_surjectivity $ sortSet sg_m
            q_axs = quotient_axs sens
            symm_ax = symmetry_axs ss_m
            tran_ax = transitivity_axs ss_m
            cong_ax = congruence_axs (opMap sg_m)
            satThM = sat_thm_ax sens
            prems = conjunct [symm_ax, tran_ax, cong_ax, satThM]
            ltkh = larger_than_ker_h ss_m (predMap sg_m)
            krnl_axs = [mkKernelAx ss_m (predMap sg_m) prems ltkh]
            forms = concat [ctor_sen, make_axs, h_axs_ops, h_axs_preds,
                            h_axs_surj, q_axs, krnl_axs]
create_axs :: Set.Set SORT -> CASLSign -> CASLSign -> [Named CASLFORMULA]
              -> [Named CASLFORMULA]
create_axs sg_ss sg_m sg_k sens = forms
      where ss_m = sortSet sg_m
            ss = Set.map mkFreeName $ Set.difference ss_m sg_ss
            sr = sortRel sg_k
            comps = ops2comp $ opMap sg_k
            ss' = filterNoCtorSorts (opMap sg_k) ss
            ctor_sen = freeCons (ss', sr, comps)
            make_axs = make_forms sg_ss ++ make_hom_forms sg_ss
            h_axs_ops = homomorphism_axs_ops $ opMap sg_m
            h_axs_preds = homomorphism_axs_preds $ predMap sg_m
            h_axs_surj = hom_surjectivity $ sortSet sg_m
            q_axs = quotient_axs sens
            symm_ax = symmetry_axs ss_m
            tran_ax = transitivity_axs ss_m
            cong_ax = congruence_axs (opMap sg_m)
            satThM = sat_thm_ax sens
            prems = conjunct [symm_ax, tran_ax, cong_ax, satThM]
            ltkh = larger_than_ker_h ss_m (predMap sg_m)
            krnl_axs = [mkKernelAx ss_m (predMap sg_m) prems ltkh]
            forms = concat [ctor_sen, make_axs, h_axs_ops, h_axs_preds,
                            h_axs_surj, q_axs, krnl_axs]
create_axs sg_ss sg_m sg_k sens = forms
      where ss_m = sortSet sg_m
            ss = Set.map mkFreeName $ Set.difference ss_m sg_ss
            sr = sortRel sg_k
            comps = ops2comp $ opMap sg_k
            ss' = filterNoCtorSorts (opMap sg_k) ss
            ctor_sen = freeCons (ss', sr, comps)
            make_axs = make_forms sg_ss ++ make_hom_forms sg_ss
            h_axs_ops = homomorphism_axs_ops $ opMap sg_m
            h_axs_preds = homomorphism_axs_preds $ predMap sg_m
            h_axs_surj = hom_surjectivity $ sortSet sg_m
            q_axs = quotient_axs sens
            symm_ax = symmetry_axs ss_m
            tran_ax = transitivity_axs ss_m
            cong_ax = congruence_axs (opMap sg_m)
            satThM = sat_thm_ax sens
            prems = conjunct [symm_ax, tran_ax, cong_ax, satThM]
            ltkh = larger_than_ker_h ss_m (predMap sg_m)
            krnl_axs = [mkKernelAx ss_m (predMap sg_m) prems ltkh]
            forms = concat [ctor_sen, make_axs, h_axs_ops, h_axs_preds,
                            h_axs_surj, q_axs, krnl_axs]