# Generated by tools/translator: qualified upstream name -> MoonBit name.
ASM_METIS_TAC asm_metis_tac
METIS metis
METIS_TAC metis_tac
Metis.FOL_PREPARE_TAC fol_prepare_tac
Metis.GEN_METIS_TAC gen_metis_tac
Metis.PRINT_ID_TAC print_id_tac
Metis.PRINT_TAC print_tac
Metis.PURE_METIS_TAC pure_metis_tac
Metis.SIMPLE_METIS_REFUTE simple_metis_refute
Metis.split_limit split_limit
Metis.without_warnings without_warnings
Metis_debug.hide_types hide_types
Metis_debug.print_varandtype print_varandtype
Metis_debug.show_types show_types
Metis_generate.metis_name metis_name
Metis_generate.metis_of_atom metis_of_atom
Metis_generate.metis_of_clause metis_of_clause
Metis_generate.metis_of_clauses metis_of_clauses
Metis_generate.metis_of_literal metis_of_literal
Metis_generate.metis_of_term metis_of_term
Metis_mapping.fol_of_const fol_of_const
Metis_mapping.hol_of_atom hol_of_atom
Metis_mapping.hol_of_clause hol_of_clause
Metis_mapping.hol_of_const hol_of_const
Metis_mapping.hol_of_literal hol_of_literal
Metis_mapping.hol_of_substitution hol_of_substitution
Metis_mapping.hol_of_term hol_of_term
Metis_mapping.prefix prefix_v1
Metis_mapping.preterm_of_atom preterm_of_atom
Metis_mapping.preterm_of_const preterm_of_const
Metis_mapping.preterm_of_eq preterm_of_eq
Metis_mapping.preterm_of_fol_term preterm_of_fol_term
Metis_mapping.preterm_of_literal preterm_of_literal
Metis_mapping.preterm_of_predicate preterm_of_predicate
Metis_mapping.reset_consts reset_consts
Metis_mapping.typecheck typecheck
Metis_mapping.typecheckl typecheckl
Metis_path.hol_of_atom_path hol_of_atom_path
Metis_path.hol_of_literal_path hol_of_literal_path
Metis_path.hol_of_term_path hol_of_term_path
Metis_prover.Active.add add_v31
Metis_prover.Active.addAllSubterms addallsubterms
Metis_prover.Active.addClause addclause
Metis_prover.Active.addEquations addequations
Metis_prover.Active.addFactorClause addfactorclause
Metis_prover.Active.addLiterals addliterals
Metis_prover.Active.addRewrite addrewrite
Metis_prover.Active.addSubsume addsubsume
Metis_prover.Active.addSubterms addsubterms_v1
Metis_prover.Active.addUnit addunit
Metis_prover.Active.choose_clause_rewritables choose_clause_rewritables
Metis_prover.Active.clause_rewritables clause_rewritables
Metis_prover.Active.clauses clauses
Metis_prover.Active.deduce deduce
Metis_prover.Active.deduceParamodulationInto deduceparamodulationinto
Metis_prover.Active.deduceParamodulationWith deduceparamodulationwith
Metis_prover.Active.deduceResolution deduceresolution
Metis_prover.Active.default default_v3
Metis_prover.Active.delete delete_v17
Metis_prover.Active.empty empty_v27
Metis_prover.Active.extract_rewritables extract_rewritables
Metis_prover.Active.factor factor_v2
Metis_prover.Active.factor' factor_p_v1
Metis_prover.Active.factor1 factor1
Metis_prover.Active.getSubsume getsubsume
Metis_prover.Active.maxSimplify maxsimplify
Metis_prover.Active.mk_clause mk_clause
Metis_prover.Active.newActive newactive
Metis_prover.Active.orderedRedexResidues orderedredexresidues
Metis_prover.Active.post_factor post_factor
Metis_prover.Active.postfactor_simplify postfactor_simplify
Metis_prover.Active.pre_factor pre_factor
Metis_prover.Active.prefactor_simplify prefactor_simplify
Metis_prover.Active.rewritables rewritables
Metis_prover.Active.rewrite_rewritables rewrite_rewritables
Metis_prover.Active.saturation saturation
Metis_prover.Active.setRewrite setrewrite
Metis_prover.Active.simplify simplify_v2
Metis_prover.Active.simplifyActive simplifyactive
Metis_prover.Active.size size_v25
Metis_prover.Active.sort_utilitywise sort_utilitywise
Metis_prover.Active.toString tostring_v15
Metis_prover.Active.unorderedRedexResidues unorderedredexresidues
Metis_prover.Atom.Map.Ma.add add_v14
Metis_prover.Atom.Map.Ma.bindings bindings_v5
Metis_prover.Atom.Map.Ma.cardinal cardinal_v9
Metis_prover.Atom.Map.Ma.choose choose_v9
Metis_prover.Atom.Map.Ma.choose_opt choose_opt_v9
Metis_prover.Atom.Map.Ma.compare compare_v26
Metis_prover.Atom.Map.Ma.empty empty_v14
Metis_prover.Atom.Map.Ma.equal equal_v18
Metis_prover.Atom.Map.Ma.exists exists_v18
Metis_prover.Atom.Map.Ma.filter filter_v15
Metis_prover.Atom.Map.Ma.filter_map filter_map_v9
Metis_prover.Atom.Map.Ma.find find_v12
Metis_prover.Atom.Map.Ma.find_first find_first_v9
Metis_prover.Atom.Map.Ma.find_first_opt find_first_opt_v9
Metis_prover.Atom.Map.Ma.find_last find_last_v9
Metis_prover.Atom.Map.Ma.find_last_opt find_last_opt_v9
Metis_prover.Atom.Map.Ma.find_opt find_opt_v9
Metis_prover.Atom.Map.Ma.fold fold_v9
Metis_prover.Atom.Map.Ma.for_all for_all_v9
Metis_prover.Atom.Map.Ma.is_empty is_empty_v9
Metis_prover.Atom.Map.Ma.iter iter_v9
Metis_prover.Atom.Map.Ma.map map_v11
Metis_prover.Atom.Map.Ma.mapi mapi_v5
Metis_prover.Atom.Map.Ma.max_binding max_binding_v5
Metis_prover.Atom.Map.Ma.max_binding_opt max_binding_opt_v5
Metis_prover.Atom.Map.Ma.mem mem_v9
Metis_prover.Atom.Map.Ma.merge merge_v7
Metis_prover.Atom.Map.Ma.min_binding min_binding_v5
Metis_prover.Atom.Map.Ma.min_binding_opt min_binding_opt_v5
Metis_prover.Atom.Map.Ma.partition partition_v11
Metis_prover.Atom.Map.Ma.remove remove_v13
Metis_prover.Atom.Map.Ma.singleton singleton_v19
Metis_prover.Atom.Map.Ma.split split_v9
Metis_prover.Atom.Map.Ma.union union_v19
Metis_prover.Atom.Map.Ma.update update_v5
Metis_prover.Atom.Map.delete delete_v9
Metis_prover.Atom.Map.exists exists_v19
Metis_prover.Atom.Map.filter filter_v16
Metis_prover.Atom.Map.foldl foldl_v11
Metis_prover.Atom.Map.foldr foldr_v11
Metis_prover.Atom.Map.fromList fromlist_v10
Metis_prover.Atom.Map.get get_v5
Metis_prover.Atom.Map.inDomain indomain_v5
Metis_prover.Atom.Map.insert insert_v6
Metis_prover.Atom.Map.mapPartial mappartial_v6
Metis_prover.Atom.Map.newMap newmap_v5
Metis_prover.Atom.Map.null null_v12
Metis_prover.Atom.Map.peek peek_v7
Metis_prover.Atom.Map.singleton singleton_v20
Metis_prover.Atom.Map.size size_v11
Metis_prover.Atom.Map.toList tolist_v11
Metis_prover.Atom.Map.transform transform_v9
Metis_prover.Atom.Map.union union_v20
Metis_prover.Atom.Ordered.compare compare_v25
Metis_prover.Atom.Set.Se.add add_v15
Metis_prover.Atom.Set.Se.cardinal cardinal_v10
Metis_prover.Atom.Set.Se.choose choose_v10
Metis_prover.Atom.Set.Se.choose_opt choose_opt_v10
Metis_prover.Atom.Set.Se.compare compare_v27
Metis_prover.Atom.Set.Se.diff diff_v4
Metis_prover.Atom.Set.Se.disjoint disjoint_v5
Metis_prover.Atom.Set.Se.elements elements_v4
Metis_prover.Atom.Set.Se.empty empty_v15
Metis_prover.Atom.Set.Se.equal equal_v19
Metis_prover.Atom.Set.Se.exists exists_v20
Metis_prover.Atom.Set.Se.filter filter_v17
Metis_prover.Atom.Set.Se.filter_map filter_map_v10
Metis_prover.Atom.Set.Se.find find_v13
Metis_prover.Atom.Set.Se.find_first find_first_v10
Metis_prover.Atom.Set.Se.find_first_opt find_first_opt_v10
Metis_prover.Atom.Set.Se.find_last find_last_v10
Metis_prover.Atom.Set.Se.find_last_opt find_last_opt_v10
Metis_prover.Atom.Set.Se.find_opt find_opt_v10
Metis_prover.Atom.Set.Se.fold fold_v10
Metis_prover.Atom.Set.Se.for_all for_all_v10
Metis_prover.Atom.Set.Se.inter inter_v4
Metis_prover.Atom.Set.Se.is_empty is_empty_v10
Metis_prover.Atom.Set.Se.iter iter_v10
Metis_prover.Atom.Set.Se.map map_v12
Metis_prover.Atom.Set.Se.max_elt max_elt_v4
Metis_prover.Atom.Set.Se.max_elt_opt max_elt_opt_v4
Metis_prover.Atom.Set.Se.mem mem_v10
Metis_prover.Atom.Set.Se.min_elt min_elt_v4
Metis_prover.Atom.Set.Se.min_elt_opt min_elt_opt_v4
Metis_prover.Atom.Set.Se.partition partition_v12
Metis_prover.Atom.Set.Se.remove remove_v14
Metis_prover.Atom.Set.Se.singleton singleton_v21
Metis_prover.Atom.Set.Se.split split_v10
Metis_prover.Atom.Set.Se.subset subset_v8
Metis_prover.Atom.Set.Se.union union_v21
Metis_prover.Atom.Set.add add_v16
Metis_prover.Atom.Set.all all_v5
Metis_prover.Atom.Set.compare compare_v28
Metis_prover.Atom.Set.count count_v5
Metis_prover.Atom.Set.delete delete_v10
Metis_prover.Atom.Set.difference difference_v4
Metis_prover.Atom.Set.empty empty_v16
Metis_prover.Atom.Set.equal equal_v20
Metis_prover.Atom.Set.exists exists_v21
Metis_prover.Atom.Set.findl findl_v5
Metis_prover.Atom.Set.firstl firstl_v5
Metis_prover.Atom.Set.foldl foldl_v12
Metis_prover.Atom.Set.foldr foldr_v12
Metis_prover.Atom.Set.fromList fromlist_v11
Metis_prover.Atom.Set.intersect intersect_v5
Metis_prover.Atom.Set.intersectList intersectlist_v4
Metis_prover.Atom.Set.member member_v4
Metis_prover.Atom.Set.null null_v13
Metis_prover.Atom.Set.pick pick_v5
Metis_prover.Atom.Set.singleton singleton_v22
Metis_prover.Atom.Set.size size_v12
Metis_prover.Atom.Set.subset subset_v9
Metis_prover.Atom.Set.toList tolist_v12
Metis_prover.Atom.Set.transform transform_v10
Metis_prover.Atom.Set.union union_v22
Metis_prover.Atom.arguments arguments
Metis_prover.Atom.arity arity_v1
Metis_prover.Atom.compare compare_v24
Metis_prover.Atom.destBinop destbinop_v1
Metis_prover.Atom.destEq desteq
Metis_prover.Atom.destRefl destrefl
Metis_prover.Atom.eqRelation eqrelation
Metis_prover.Atom.eqRelationArity eqrelationarity
Metis_prover.Atom.eqRelationName eqrelationname
Metis_prover.Atom.equal equal_v17
Metis_prover.Atom.find find_v11
Metis_prover.Atom.freeIn freein_v1
Metis_prover.Atom.freeVars freevars_v2
Metis_prover.Atom.functionNames functionnames_v1
Metis_prover.Atom.functions functions_v2
Metis_prover.Atom.isBinop isbinop_v1
Metis_prover.Atom.isEq iseq
Metis_prover.Atom.isRefl isrefl
Metis_prover.Atom.lhs lhs
Metis_prover.Atom.matchAtoms matchatoms
Metis_prover.Atom.mkBinop mkbinop_v1
Metis_prover.Atom.mkEq mkeq
Metis_prover.Atom.mkRefl mkrefl
Metis_prover.Atom.name name_v1
Metis_prover.Atom.nonVarTypedSubterms nonvartypedsubterms_v1
Metis_prover.Atom.relation relation
Metis_prover.Atom.replace replace_v1
Metis_prover.Atom.rhs rhs
Metis_prover.Atom.subst subst_v1
Metis_prover.Atom.subterm subterm_v1
Metis_prover.Atom.subterms subterms_v1
Metis_prover.Atom.sym sym
Metis_prover.Atom.symbols symbols_v1
Metis_prover.Atom.typedSymbols typedsymbols_v1
Metis_prover.Atom.unify unify_v1
Metis_prover.Atom_net.atomToTerm atomtoterm
Metis_prover.Atom_net.filter filter_v28
Metis_prover.Atom_net.fromList fromlist_v19
Metis_prover.Atom_net.insert insert_v11
Metis_prover.Atom_net.matchNet matchnet_v1
Metis_prover.Atom_net.matched matched_v1
Metis_prover.Atom_net.newNet newnet_v1
Metis_prover.Atom_net.size size_v20
Metis_prover.Atom_net.termToAtom termtoatom
Metis_prover.Atom_net.toString tostring_v10
Metis_prover.Atom_net.unify unify_v4
Metis_prover.Clause.addLit addlit
Metis_prover.Clause.allSubterms allsubterms
Metis_prover.Clause.atomToTerms atomtoterms
Metis_prover.Clause.default default_v2
Metis_prover.Clause.dest dest_v1
Metis_prover.Clause.equalThms equalthms
Metis_prover.Clause.factor factor_v1
Metis_prover.Clause.freshVars freshvars_v2
Metis_prover.Clause.id id
Metis_prover.Clause.isContradiction iscontradiction_v1
Metis_prover.Clause.isLargerLiteral islargerliteral
Metis_prover.Clause.isLargerTerm islargerterm
Metis_prover.Clause.isTautology istautology_v1
Metis_prover.Clause.largestEquations largestequations
Metis_prover.Clause.largestLiterals largestliterals
Metis_prover.Clause.largestSubterms largestsubterms
Metis_prover.Clause.literals literals
Metis_prover.Clause.mk mk
Metis_prover.Clause.newClause newclause
Metis_prover.Clause.newId newid
Metis_prover.Clause.notStrictlyLess notstrictlyless
Metis_prover.Clause.paramodulate paramodulate
Metis_prover.Clause.reduce reduce_v2
Metis_prover.Clause.resolve resolve_v1
Metis_prover.Clause.rewrite rewrite_v1
Metis_prover.Clause.simplify simplify_v1
Metis_prover.Clause.strictlyLess strictlyless
Metis_prover.Clause.subsumes subsumes_v1
Metis_prover.Clause.thm thm
Metis_prover.Clause.toString tostring_v14
Metis_prover.Formula.Map.Ma.add add_v18
Metis_prover.Formula.Map.Ma.bindings bindings_v6
Metis_prover.Formula.Map.Ma.cardinal cardinal_v11
Metis_prover.Formula.Map.Ma.choose choose_v11
Metis_prover.Formula.Map.Ma.choose_opt choose_opt_v11
Metis_prover.Formula.Map.Ma.compare compare_v31
Metis_prover.Formula.Map.Ma.empty empty_v17
Metis_prover.Formula.Map.Ma.equal equal_v22
Metis_prover.Formula.Map.Ma.exists exists_v22
Metis_prover.Formula.Map.Ma.filter filter_v18
Metis_prover.Formula.Map.Ma.filter_map filter_map_v11
Metis_prover.Formula.Map.Ma.find find_v14
Metis_prover.Formula.Map.Ma.find_first find_first_v11
Metis_prover.Formula.Map.Ma.find_first_opt find_first_opt_v11
Metis_prover.Formula.Map.Ma.find_last find_last_v11
Metis_prover.Formula.Map.Ma.find_last_opt find_last_opt_v11
Metis_prover.Formula.Map.Ma.find_opt find_opt_v11
Metis_prover.Formula.Map.Ma.fold fold_v11
Metis_prover.Formula.Map.Ma.for_all for_all_v11
Metis_prover.Formula.Map.Ma.is_empty is_empty_v11
Metis_prover.Formula.Map.Ma.iter iter_v11
Metis_prover.Formula.Map.Ma.map map_v13
Metis_prover.Formula.Map.Ma.mapi mapi_v6
Metis_prover.Formula.Map.Ma.max_binding max_binding_v6
Metis_prover.Formula.Map.Ma.max_binding_opt max_binding_opt_v6
Metis_prover.Formula.Map.Ma.mem mem_v11
Metis_prover.Formula.Map.Ma.merge merge_v8
Metis_prover.Formula.Map.Ma.min_binding min_binding_v6
Metis_prover.Formula.Map.Ma.min_binding_opt min_binding_opt_v6
Metis_prover.Formula.Map.Ma.partition partition_v13
Metis_prover.Formula.Map.Ma.remove remove_v15
Metis_prover.Formula.Map.Ma.singleton singleton_v23
Metis_prover.Formula.Map.Ma.split split_v12
Metis_prover.Formula.Map.Ma.union union_v23
Metis_prover.Formula.Map.Ma.update update_v6
Metis_prover.Formula.Map.delete delete_v11
Metis_prover.Formula.Map.exists exists_v23
Metis_prover.Formula.Map.filter filter_v19
Metis_prover.Formula.Map.foldl foldl_v13
Metis_prover.Formula.Map.foldr foldr_v13
Metis_prover.Formula.Map.fromList fromlist_v12
Metis_prover.Formula.Map.get get_v6
Metis_prover.Formula.Map.inDomain indomain_v6
Metis_prover.Formula.Map.insert insert_v7
Metis_prover.Formula.Map.mapPartial mappartial_v7
Metis_prover.Formula.Map.newMap newmap_v6
Metis_prover.Formula.Map.null null_v14
Metis_prover.Formula.Map.peek peek_v8
Metis_prover.Formula.Map.singleton singleton_v24
Metis_prover.Formula.Map.size size_v13
Metis_prover.Formula.Map.toList tolist_v13
Metis_prover.Formula.Map.transform transform_v11
Metis_prover.Formula.Map.union union_v24
Metis_prover.Formula.Ordered.compare compare_v30
Metis_prover.Formula.Set.Se.add add_v19
Metis_prover.Formula.Set.Se.cardinal cardinal_v12
Metis_prover.Formula.Set.Se.choose choose_v12
Metis_prover.Formula.Set.Se.choose_opt choose_opt_v12
Metis_prover.Formula.Set.Se.compare compare_v32
Metis_prover.Formula.Set.Se.diff diff_v5
Metis_prover.Formula.Set.Se.disjoint disjoint_v6
Metis_prover.Formula.Set.Se.elements elements_v5
Metis_prover.Formula.Set.Se.empty empty_v18
Metis_prover.Formula.Set.Se.equal equal_v23
Metis_prover.Formula.Set.Se.exists exists_v24
Metis_prover.Formula.Set.Se.filter filter_v20
Metis_prover.Formula.Set.Se.filter_map filter_map_v12
Metis_prover.Formula.Set.Se.find find_v15
Metis_prover.Formula.Set.Se.find_first find_first_v12
Metis_prover.Formula.Set.Se.find_first_opt find_first_opt_v12
Metis_prover.Formula.Set.Se.find_last find_last_v12
Metis_prover.Formula.Set.Se.find_last_opt find_last_opt_v12
Metis_prover.Formula.Set.Se.find_opt find_opt_v12
Metis_prover.Formula.Set.Se.fold fold_v12
Metis_prover.Formula.Set.Se.for_all for_all_v12
Metis_prover.Formula.Set.Se.inter inter_v5
Metis_prover.Formula.Set.Se.is_empty is_empty_v12
Metis_prover.Formula.Set.Se.iter iter_v12
Metis_prover.Formula.Set.Se.map map_v14
Metis_prover.Formula.Set.Se.max_elt max_elt_v5
Metis_prover.Formula.Set.Se.max_elt_opt max_elt_opt_v5
Metis_prover.Formula.Set.Se.mem mem_v12
Metis_prover.Formula.Set.Se.min_elt min_elt_v5
Metis_prover.Formula.Set.Se.min_elt_opt min_elt_opt_v5
Metis_prover.Formula.Set.Se.partition partition_v14
Metis_prover.Formula.Set.Se.remove remove_v16
Metis_prover.Formula.Set.Se.singleton singleton_v25
Metis_prover.Formula.Set.Se.split split_v13
Metis_prover.Formula.Set.Se.subset subset_v10
Metis_prover.Formula.Set.Se.union union_v25
Metis_prover.Formula.Set.add add_v20
Metis_prover.Formula.Set.all all_v6
Metis_prover.Formula.Set.compare compare_v33
Metis_prover.Formula.Set.count count_v6
Metis_prover.Formula.Set.delete delete_v12
Metis_prover.Formula.Set.difference difference_v5
Metis_prover.Formula.Set.empty empty_v19
Metis_prover.Formula.Set.equal equal_v24
Metis_prover.Formula.Set.exists exists_v25
Metis_prover.Formula.Set.findl findl_v6
Metis_prover.Formula.Set.firstl firstl_v6
Metis_prover.Formula.Set.foldl foldl_v14
Metis_prover.Formula.Set.foldr foldr_v14
Metis_prover.Formula.Set.fromList fromlist_v13
Metis_prover.Formula.Set.intersect intersect_v6
Metis_prover.Formula.Set.intersectList intersectlist_v5
Metis_prover.Formula.Set.member member_v5
Metis_prover.Formula.Set.null null_v15
Metis_prover.Formula.Set.pick pick_v6
Metis_prover.Formula.Set.singleton singleton_v26
Metis_prover.Formula.Set.size size_v14
Metis_prover.Formula.Set.subset subset_v11
Metis_prover.Formula.Set.toList tolist_v14
Metis_prover.Formula.Set.transform transform_v12
Metis_prover.Formula.Set.union union_v26
Metis_prover.Formula.add add_v17
Metis_prover.Formula.add_asms add_asms
Metis_prover.Formula.add_var_asms add_var_asms
Metis_prover.Formula.compare compare_v29
Metis_prover.Formula.conjunctionName conjunctionname
Metis_prover.Formula.demote demote
Metis_prover.Formula.destAtom destatom
Metis_prover.Formula.destBoolean destboolean
Metis_prover.Formula.destEq desteq_v1
Metis_prover.Formula.destExists destexists
Metis_prover.Formula.destForall destforall
Metis_prover.Formula.destNeg destneg
Metis_prover.Formula.destNeq destneq
Metis_prover.Formula.destRefl destrefl_v1
Metis_prover.Formula.disjunctionName disjunctionname
Metis_prover.Formula.equal equal_v21
Metis_prover.Formula.equivalenceName equivalencename
Metis_prover.Formula.existentialName existentialname
Metis_prover.Formula.falsityName falsityname
Metis_prover.Formula.flattenConj flattenconj
Metis_prover.Formula.flattenDisj flattendisj
Metis_prover.Formula.flattenEquiv flattenequiv
Metis_prover.Formula.freeIn freein_v2
Metis_prover.Formula.freeVars freevars_v3
Metis_prover.Formula.freeVarsList freevarslist_v1
Metis_prover.Formula.functionNames functionnames_v2
Metis_prover.Formula.functions functions_v3
Metis_prover.Formula.generalize generalize
Metis_prover.Formula.implicationName implicationname
Metis_prover.Formula.isAtom isatom
Metis_prover.Formula.isBoolean isboolean
Metis_prover.Formula.isEq iseq_v1
Metis_prover.Formula.isExists isexists
Metis_prover.Formula.isFalse isfalse
Metis_prover.Formula.isForall isforall
Metis_prover.Formula.isNeg isneg
Metis_prover.Formula.isNeq isneq
Metis_prover.Formula.isRefl isrefl_v1
Metis_prover.Formula.isTrue istrue
Metis_prover.Formula.lhs lhs_v1
Metis_prover.Formula.listMkConj listmkconj
Metis_prover.Formula.listMkDisj listmkdisj
Metis_prover.Formula.listMkEquiv listmkequiv
Metis_prover.Formula.listMkExists listmkexists
Metis_prover.Formula.listMkForall listmkforall
Metis_prover.Formula.mkBoolean mkboolean
Metis_prover.Formula.mkEq mkeq_v1
Metis_prover.Formula.mkNeq mkneq
Metis_prover.Formula.mkRefl mkrefl_v1
Metis_prover.Formula.relationNames relationnames
Metis_prover.Formula.relations relations
Metis_prover.Formula.rhs rhs_v1
Metis_prover.Formula.setMkExists setmkexists
Metis_prover.Formula.setMkForall setmkforall
Metis_prover.Formula.specialize specialize
Metis_prover.Formula.split split_v11
Metis_prover.Formula.splitGoal splitgoal
Metis_prover.Formula.stripConj stripconj
Metis_prover.Formula.stripDisj stripdisj
Metis_prover.Formula.stripEquiv stripequiv
Metis_prover.Formula.stripExists stripexists
Metis_prover.Formula.stripForall stripforall
Metis_prover.Formula.stripNeg stripneg
Metis_prover.Formula.subst subst_v2
Metis_prover.Formula.substCheck substcheck
Metis_prover.Formula.substConn substconn
Metis_prover.Formula.substFm substfm
Metis_prover.Formula.substQuant substquant
Metis_prover.Formula.sym sym_v1
Metis_prover.Formula.symbols symbols_v2
Metis_prover.Formula.toString tostring_v5
Metis_prover.Formula.truthName truthname
Metis_prover.Formula.universalName universalname
Metis_prover.Heap.add add_v5
Metis_prover.Heap.app app_v2
Metis_prover.Heap.makeT maket
Metis_prover.Heap.merge merge_v3
Metis_prover.Heap.newHeap newheap
Metis_prover.Heap.null null_v6
Metis_prover.Heap.rank rank
Metis_prover.Heap.remove remove_v5
Metis_prover.Heap.size size_v5
Metis_prover.Heap.toList tolist_v5
Metis_prover.Heap.toString tostring_v2
Metis_prover.Heap.top top
Metis_prover.Intmap.Ma.add add_v1
Metis_prover.Intmap.Ma.bindings bindings
Metis_prover.Intmap.Ma.cardinal cardinal
Metis_prover.Intmap.Ma.choose choose
Metis_prover.Intmap.Ma.choose_opt choose_opt
Metis_prover.Intmap.Ma.compare compare_v4
Metis_prover.Intmap.Ma.empty empty_v1
Metis_prover.Intmap.Ma.equal equal_v2
Metis_prover.Intmap.Ma.exists exists_v2
Metis_prover.Intmap.Ma.filter filter_v2
Metis_prover.Intmap.Ma.filter_map filter_map
Metis_prover.Intmap.Ma.find find_v1
Metis_prover.Intmap.Ma.find_first find_first
Metis_prover.Intmap.Ma.find_first_opt find_first_opt
Metis_prover.Intmap.Ma.find_last find_last
Metis_prover.Intmap.Ma.find_last_opt find_last_opt
Metis_prover.Intmap.Ma.find_opt find_opt
Metis_prover.Intmap.Ma.fold fold
Metis_prover.Intmap.Ma.for_all for_all
Metis_prover.Intmap.Ma.is_empty is_empty
Metis_prover.Intmap.Ma.iter iter
Metis_prover.Intmap.Ma.map map_v2
Metis_prover.Intmap.Ma.mapi mapi
Metis_prover.Intmap.Ma.max_binding max_binding
Metis_prover.Intmap.Ma.max_binding_opt max_binding_opt
Metis_prover.Intmap.Ma.mem mem
Metis_prover.Intmap.Ma.merge merge_v1
Metis_prover.Intmap.Ma.min_binding min_binding
Metis_prover.Intmap.Ma.min_binding_opt min_binding_opt
Metis_prover.Intmap.Ma.partition partition_v2
Metis_prover.Intmap.Ma.remove remove_v2
Metis_prover.Intmap.Ma.singleton singleton_v2
Metis_prover.Intmap.Ma.split split
Metis_prover.Intmap.Ma.union union_v2
Metis_prover.Intmap.Ma.update update
Metis_prover.Intmap.Ordered.compare compare_v3
Metis_prover.Intmap.delete delete_v2
Metis_prover.Intmap.exists exists_v3
Metis_prover.Intmap.filter filter_v3
Metis_prover.Intmap.foldl foldl_v3
Metis_prover.Intmap.foldr foldr_v3
Metis_prover.Intmap.fromList fromlist_v2
Metis_prover.Intmap.get get_v1
Metis_prover.Intmap.inDomain indomain_v1
Metis_prover.Intmap.insert insert_v1
Metis_prover.Intmap.mapPartial mappartial_v2
Metis_prover.Intmap.newMap newmap_v1
Metis_prover.Intmap.null null_v3
Metis_prover.Intmap.peek peek_v2
Metis_prover.Intmap.singleton singleton_v3
Metis_prover.Intmap.size size_v2
Metis_prover.Intmap.toList tolist_v2
Metis_prover.Intmap.transform transform_v2
Metis_prover.Intmap.union union_v3
Metis_prover.Intset.Ordered.compare compare_v7
Metis_prover.Intset.Se.add add_v3
Metis_prover.Intset.Se.cardinal cardinal_v2
Metis_prover.Intset.Se.choose choose_v2
Metis_prover.Intset.Se.choose_opt choose_opt_v2
Metis_prover.Intset.Se.compare compare_v8
Metis_prover.Intset.Se.diff diff
Metis_prover.Intset.Se.disjoint disjoint_v1
Metis_prover.Intset.Se.elements elements
Metis_prover.Intset.Se.empty empty_v3
Metis_prover.Intset.Se.equal equal_v4
Metis_prover.Intset.Se.exists exists_v6
Metis_prover.Intset.Se.filter filter_v6
Metis_prover.Intset.Se.filter_map filter_map_v2
Metis_prover.Intset.Se.find find_v3
Metis_prover.Intset.Se.find_first find_first_v2
Metis_prover.Intset.Se.find_first_opt find_first_opt_v2
Metis_prover.Intset.Se.find_last find_last_v2
Metis_prover.Intset.Se.find_last_opt find_last_opt_v2
Metis_prover.Intset.Se.find_opt find_opt_v2
Metis_prover.Intset.Se.fold fold_v2
Metis_prover.Intset.Se.for_all for_all_v2
Metis_prover.Intset.Se.inter inter
Metis_prover.Intset.Se.is_empty is_empty_v2
Metis_prover.Intset.Se.iter iter_v2
Metis_prover.Intset.Se.map map_v4
Metis_prover.Intset.Se.max_elt max_elt
Metis_prover.Intset.Se.max_elt_opt max_elt_opt
Metis_prover.Intset.Se.mem mem_v2
Metis_prover.Intset.Se.min_elt min_elt
Metis_prover.Intset.Se.min_elt_opt min_elt_opt
Metis_prover.Intset.Se.partition partition_v4
Metis_prover.Intset.Se.remove remove_v4
Metis_prover.Intset.Se.singleton singleton_v6
Metis_prover.Intset.Se.split split_v2
Metis_prover.Intset.Se.subset subset_v1
Metis_prover.Intset.Se.union union_v6
Metis_prover.Intset.add add_v4
Metis_prover.Intset.all all_v2
Metis_prover.Intset.compare compare_v9
Metis_prover.Intset.count count_v2
Metis_prover.Intset.delete delete_v4
Metis_prover.Intset.difference difference_v1
Metis_prover.Intset.empty empty_v4
Metis_prover.Intset.equal equal_v5
Metis_prover.Intset.exists exists_v7
Metis_prover.Intset.findl findl_v2
Metis_prover.Intset.firstl firstl_v2
Metis_prover.Intset.foldl foldl_v5
Metis_prover.Intset.foldr foldr_v5
Metis_prover.Intset.fromList fromlist_v4
Metis_prover.Intset.intersect intersect_v2
Metis_prover.Intset.intersectList intersectlist_v1
Metis_prover.Intset.member member_v1
Metis_prover.Intset.null null_v5
Metis_prover.Intset.pick pick_v2
Metis_prover.Intset.singleton singleton_v7
Metis_prover.Intset.size size_v4
Metis_prover.Intset.subset subset_v2
Metis_prover.Intset.toList tolist_v4
Metis_prover.Intset.transform transform_v4
Metis_prover.Intset.union union_v7
Metis_prover.Knuth_bendix_order.add add_v28
Metis_prover.Knuth_bendix_order.arityPrecedence arityprecedence
Metis_prover.Knuth_bendix_order.compare compare_v44
Metis_prover.Knuth_bendix_order.default default_v1
Metis_prover.Knuth_bendix_order.firstNotEqualTerm firstnotequalterm
Metis_prover.Knuth_bendix_order.notEqualTerm notequalterm
Metis_prover.Knuth_bendix_order.uniformWeight uniformweight
Metis_prover.Knuth_bendix_order.weightAdd weightadd
Metis_prover.Knuth_bendix_order.weightEmpty weightempty
Metis_prover.Knuth_bendix_order.weightIsZero weightiszero
Metis_prover.Knuth_bendix_order.weightLowerBound weightlowerbound
Metis_prover.Knuth_bendix_order.weightNeg weightneg
Metis_prover.Knuth_bendix_order.weightSubtract weightsubtract
Metis_prover.Knuth_bendix_order.weightTerm weightterm
Metis_prover.Knuth_bendix_order.weightZero weightzero
Metis_prover.Literal.Map.Ma.add add_v21
Metis_prover.Literal.Map.Ma.bindings bindings_v7
Metis_prover.Literal.Map.Ma.cardinal cardinal_v13
Metis_prover.Literal.Map.Ma.choose choose_v13
Metis_prover.Literal.Map.Ma.choose_opt choose_opt_v13
Metis_prover.Literal.Map.Ma.compare compare_v36
Metis_prover.Literal.Map.Ma.empty empty_v20
Metis_prover.Literal.Map.Ma.equal equal_v26
Metis_prover.Literal.Map.Ma.exists exists_v26
Metis_prover.Literal.Map.Ma.filter filter_v21
Metis_prover.Literal.Map.Ma.filter_map filter_map_v13
Metis_prover.Literal.Map.Ma.find find_v16
Metis_prover.Literal.Map.Ma.find_first find_first_v13
Metis_prover.Literal.Map.Ma.find_first_opt find_first_opt_v13
Metis_prover.Literal.Map.Ma.find_last find_last_v13
Metis_prover.Literal.Map.Ma.find_last_opt find_last_opt_v13
Metis_prover.Literal.Map.Ma.find_opt find_opt_v13
Metis_prover.Literal.Map.Ma.fold fold_v13
Metis_prover.Literal.Map.Ma.for_all for_all_v13
Metis_prover.Literal.Map.Ma.is_empty is_empty_v13
Metis_prover.Literal.Map.Ma.iter iter_v13
Metis_prover.Literal.Map.Ma.map map_v15
Metis_prover.Literal.Map.Ma.mapi mapi_v7
Metis_prover.Literal.Map.Ma.max_binding max_binding_v7
Metis_prover.Literal.Map.Ma.max_binding_opt max_binding_opt_v7
Metis_prover.Literal.Map.Ma.mem mem_v13
Metis_prover.Literal.Map.Ma.merge merge_v9
Metis_prover.Literal.Map.Ma.min_binding min_binding_v7
Metis_prover.Literal.Map.Ma.min_binding_opt min_binding_opt_v7
Metis_prover.Literal.Map.Ma.partition partition_v15
Metis_prover.Literal.Map.Ma.remove remove_v17
Metis_prover.Literal.Map.Ma.singleton singleton_v27
Metis_prover.Literal.Map.Ma.split split_v14
Metis_prover.Literal.Map.Ma.union union_v27
Metis_prover.Literal.Map.Ma.update update_v7
Metis_prover.Literal.Map.delete delete_v13
Metis_prover.Literal.Map.exists exists_v27
Metis_prover.Literal.Map.filter filter_v22
Metis_prover.Literal.Map.foldl foldl_v15
Metis_prover.Literal.Map.foldr foldr_v15
Metis_prover.Literal.Map.fromList fromlist_v14
Metis_prover.Literal.Map.get get_v7
Metis_prover.Literal.Map.inDomain indomain_v7
Metis_prover.Literal.Map.insert insert_v8
Metis_prover.Literal.Map.mapPartial mappartial_v8
Metis_prover.Literal.Map.newMap newmap_v7
Metis_prover.Literal.Map.null null_v16
Metis_prover.Literal.Map.peek peek_v9
Metis_prover.Literal.Map.singleton singleton_v28
Metis_prover.Literal.Map.size size_v15
Metis_prover.Literal.Map.toList tolist_v15
Metis_prover.Literal.Map.transform transform_v13
Metis_prover.Literal.Map.union union_v28
Metis_prover.Literal.Ordered.compare compare_v35
Metis_prover.Literal.Set.Se.add add_v22
Metis_prover.Literal.Set.Se.cardinal cardinal_v14
Metis_prover.Literal.Set.Se.choose choose_v14
Metis_prover.Literal.Set.Se.choose_opt choose_opt_v14
Metis_prover.Literal.Set.Se.compare compare_v37
Metis_prover.Literal.Set.Se.diff diff_v6
Metis_prover.Literal.Set.Se.disjoint disjoint_v7
Metis_prover.Literal.Set.Se.elements elements_v6
Metis_prover.Literal.Set.Se.empty empty_v21
Metis_prover.Literal.Set.Se.equal equal_v27
Metis_prover.Literal.Set.Se.exists exists_v28
Metis_prover.Literal.Set.Se.filter filter_v23
Metis_prover.Literal.Set.Se.filter_map filter_map_v14
Metis_prover.Literal.Set.Se.find find_v17
Metis_prover.Literal.Set.Se.find_first find_first_v14
Metis_prover.Literal.Set.Se.find_first_opt find_first_opt_v14
Metis_prover.Literal.Set.Se.find_last find_last_v14
Metis_prover.Literal.Set.Se.find_last_opt find_last_opt_v14
Metis_prover.Literal.Set.Se.find_opt find_opt_v14
Metis_prover.Literal.Set.Se.fold fold_v14
Metis_prover.Literal.Set.Se.for_all for_all_v14
Metis_prover.Literal.Set.Se.inter inter_v6
Metis_prover.Literal.Set.Se.is_empty is_empty_v14
Metis_prover.Literal.Set.Se.iter iter_v14
Metis_prover.Literal.Set.Se.map map_v16
Metis_prover.Literal.Set.Se.max_elt max_elt_v6
Metis_prover.Literal.Set.Se.max_elt_opt max_elt_opt_v6
Metis_prover.Literal.Set.Se.mem mem_v14
Metis_prover.Literal.Set.Se.min_elt min_elt_v6
Metis_prover.Literal.Set.Se.min_elt_opt min_elt_opt_v6
Metis_prover.Literal.Set.Se.partition partition_v16
Metis_prover.Literal.Set.Se.remove remove_v18
Metis_prover.Literal.Set.Se.singleton singleton_v29
Metis_prover.Literal.Set.Se.split split_v15
Metis_prover.Literal.Set.Se.subset subset_v12
Metis_prover.Literal.Set.Se.union union_v29
Metis_prover.Literal.Set.add add_v23
Metis_prover.Literal.Set.all all_v7
Metis_prover.Literal.Set.compare compare_v38
Metis_prover.Literal.Set.conjoin conjoin
Metis_prover.Literal.Set.count count_v7
Metis_prover.Literal.Set.delete delete_v14
Metis_prover.Literal.Set.difference difference_v6
Metis_prover.Literal.Set.disjoin disjoin
Metis_prover.Literal.Set.empty empty_v22
Metis_prover.Literal.Set.equal equal_v28
Metis_prover.Literal.Set.exists exists_v29
Metis_prover.Literal.Set.findl findl_v7
Metis_prover.Literal.Set.firstl firstl_v7
Metis_prover.Literal.Set.foldl foldl_v16
Metis_prover.Literal.Set.foldr foldr_v16
Metis_prover.Literal.Set.freeIn freein_v4
Metis_prover.Literal.Set.freeVars freevars_v5
Metis_prover.Literal.Set.freeVarsList freevarslist_v2
Metis_prover.Literal.Set.fromList fromlist_v15
Metis_prover.Literal.Set.functions functions_v5
Metis_prover.Literal.Set.intersect intersect_v7
Metis_prover.Literal.Set.intersectList intersectlist_v6
Metis_prover.Literal.Set.member member_v6
Metis_prover.Literal.Set.negate negate_v1
Metis_prover.Literal.Set.negateMember negatemember
Metis_prover.Literal.Set.null null_v17
Metis_prover.Literal.Set.pick pick_v7
Metis_prover.Literal.Set.relations relations_v1
Metis_prover.Literal.Set.singleton singleton_v30
Metis_prover.Literal.Set.size size_v16
Metis_prover.Literal.Set.subset subset_v13
Metis_prover.Literal.Set.subst subst_v4
Metis_prover.Literal.Set.symbols symbols_v4
Metis_prover.Literal.Set.toList tolist_v16
Metis_prover.Literal.Set.toString tostring_v7
Metis_prover.Literal.Set.transform transform_v14
Metis_prover.Literal.Set.typedSymbols typedsymbols_v3
Metis_prover.Literal.Set.union union_v30
Metis_prover.Literal.Set_map.Ma.add add_v24
Metis_prover.Literal.Set_map.Ma.bindings bindings_v8
Metis_prover.Literal.Set_map.Ma.cardinal cardinal_v15
Metis_prover.Literal.Set_map.Ma.choose choose_v15
Metis_prover.Literal.Set_map.Ma.choose_opt choose_opt_v15
Metis_prover.Literal.Set_map.Ma.compare compare_v40
Metis_prover.Literal.Set_map.Ma.empty empty_v23
Metis_prover.Literal.Set_map.Ma.equal equal_v29
Metis_prover.Literal.Set_map.Ma.exists exists_v30
Metis_prover.Literal.Set_map.Ma.filter filter_v24
Metis_prover.Literal.Set_map.Ma.filter_map filter_map_v15
Metis_prover.Literal.Set_map.Ma.find find_v18
Metis_prover.Literal.Set_map.Ma.find_first find_first_v15
Metis_prover.Literal.Set_map.Ma.find_first_opt find_first_opt_v15
Metis_prover.Literal.Set_map.Ma.find_last find_last_v15
Metis_prover.Literal.Set_map.Ma.find_last_opt find_last_opt_v15
Metis_prover.Literal.Set_map.Ma.find_opt find_opt_v15
Metis_prover.Literal.Set_map.Ma.fold fold_v15
Metis_prover.Literal.Set_map.Ma.for_all for_all_v15
Metis_prover.Literal.Set_map.Ma.is_empty is_empty_v15
Metis_prover.Literal.Set_map.Ma.iter iter_v15
Metis_prover.Literal.Set_map.Ma.map map_v17
Metis_prover.Literal.Set_map.Ma.mapi mapi_v8
Metis_prover.Literal.Set_map.Ma.max_binding max_binding_v8
Metis_prover.Literal.Set_map.Ma.max_binding_opt max_binding_opt_v8
Metis_prover.Literal.Set_map.Ma.mem mem_v15
Metis_prover.Literal.Set_map.Ma.merge merge_v10
Metis_prover.Literal.Set_map.Ma.min_binding min_binding_v8
Metis_prover.Literal.Set_map.Ma.min_binding_opt min_binding_opt_v8
Metis_prover.Literal.Set_map.Ma.partition partition_v17
Metis_prover.Literal.Set_map.Ma.remove remove_v19
Metis_prover.Literal.Set_map.Ma.singleton singleton_v31
Metis_prover.Literal.Set_map.Ma.split split_v16
Metis_prover.Literal.Set_map.Ma.union union_v31
Metis_prover.Literal.Set_map.Ma.update update_v8
Metis_prover.Literal.Set_map.delete delete_v15
Metis_prover.Literal.Set_map.exists exists_v31
Metis_prover.Literal.Set_map.filter filter_v25
Metis_prover.Literal.Set_map.foldl foldl_v17
Metis_prover.Literal.Set_map.foldr foldr_v17
Metis_prover.Literal.Set_map.fromList fromlist_v16
Metis_prover.Literal.Set_map.get get_v8
Metis_prover.Literal.Set_map.inDomain indomain_v8
Metis_prover.Literal.Set_map.insert insert_v9
Metis_prover.Literal.Set_map.mapPartial mappartial_v9
Metis_prover.Literal.Set_map.newMap newmap_v8
Metis_prover.Literal.Set_map.null null_v18
Metis_prover.Literal.Set_map.peek peek_v10
Metis_prover.Literal.Set_map.singleton singleton_v32
Metis_prover.Literal.Set_map.size size_v17
Metis_prover.Literal.Set_map.toList tolist_v17
Metis_prover.Literal.Set_map.transform transform_v15
Metis_prover.Literal.Set_map.union union_v32
Metis_prover.Literal.Set_ordered.compare compare_v39
Metis_prover.Literal.Set_set.Se.add add_v25
Metis_prover.Literal.Set_set.Se.cardinal cardinal_v16
Metis_prover.Literal.Set_set.Se.choose choose_v16
Metis_prover.Literal.Set_set.Se.choose_opt choose_opt_v16
Metis_prover.Literal.Set_set.Se.compare compare_v41
Metis_prover.Literal.Set_set.Se.diff diff_v7
Metis_prover.Literal.Set_set.Se.disjoint disjoint_v8
Metis_prover.Literal.Set_set.Se.elements elements_v7
Metis_prover.Literal.Set_set.Se.empty empty_v24
Metis_prover.Literal.Set_set.Se.equal equal_v30
Metis_prover.Literal.Set_set.Se.exists exists_v32
Metis_prover.Literal.Set_set.Se.filter filter_v26
Metis_prover.Literal.Set_set.Se.filter_map filter_map_v16
Metis_prover.Literal.Set_set.Se.find find_v19
Metis_prover.Literal.Set_set.Se.find_first find_first_v16
Metis_prover.Literal.Set_set.Se.find_first_opt find_first_opt_v16
Metis_prover.Literal.Set_set.Se.find_last find_last_v16
Metis_prover.Literal.Set_set.Se.find_last_opt find_last_opt_v16
Metis_prover.Literal.Set_set.Se.find_opt find_opt_v16
Metis_prover.Literal.Set_set.Se.fold fold_v16
Metis_prover.Literal.Set_set.Se.for_all for_all_v16
Metis_prover.Literal.Set_set.Se.inter inter_v7
Metis_prover.Literal.Set_set.Se.is_empty is_empty_v16
Metis_prover.Literal.Set_set.Se.iter iter_v16
Metis_prover.Literal.Set_set.Se.map map_v18
Metis_prover.Literal.Set_set.Se.max_elt max_elt_v7
Metis_prover.Literal.Set_set.Se.max_elt_opt max_elt_opt_v7
Metis_prover.Literal.Set_set.Se.mem mem_v16
Metis_prover.Literal.Set_set.Se.min_elt min_elt_v7
Metis_prover.Literal.Set_set.Se.min_elt_opt min_elt_opt_v7
Metis_prover.Literal.Set_set.Se.partition partition_v18
Metis_prover.Literal.Set_set.Se.remove remove_v20
Metis_prover.Literal.Set_set.Se.singleton singleton_v33
Metis_prover.Literal.Set_set.Se.split split_v17
Metis_prover.Literal.Set_set.Se.subset subset_v14
Metis_prover.Literal.Set_set.Se.union union_v33
Metis_prover.Literal.Set_set.add add_v26
Metis_prover.Literal.Set_set.all all_v8
Metis_prover.Literal.Set_set.compare compare_v42
Metis_prover.Literal.Set_set.count count_v8
Metis_prover.Literal.Set_set.delete delete_v16
Metis_prover.Literal.Set_set.difference difference_v7
Metis_prover.Literal.Set_set.empty empty_v25
Metis_prover.Literal.Set_set.equal equal_v31
Metis_prover.Literal.Set_set.exists exists_v33
Metis_prover.Literal.Set_set.findl findl_v8
Metis_prover.Literal.Set_set.firstl firstl_v8
Metis_prover.Literal.Set_set.foldl foldl_v18
Metis_prover.Literal.Set_set.foldr foldr_v18
Metis_prover.Literal.Set_set.fromList fromlist_v17
Metis_prover.Literal.Set_set.intersect intersect_v8
Metis_prover.Literal.Set_set.intersectList intersectlist_v7
Metis_prover.Literal.Set_set.member member_v7
Metis_prover.Literal.Set_set.null null_v19
Metis_prover.Literal.Set_set.pick pick_v8
Metis_prover.Literal.Set_set.singleton singleton_v34
Metis_prover.Literal.Set_set.size size_v18
Metis_prover.Literal.Set_set.subset subset_v15
Metis_prover.Literal.Set_set.toList tolist_v18
Metis_prover.Literal.Set_set.transform transform_v16
Metis_prover.Literal.Set_set.union union_v34
Metis_prover.Literal.arguments arguments_v1
Metis_prover.Literal.arity arity_v2
Metis_prover.Literal.atom atom
Metis_prover.Literal.compare compare_v34
Metis_prover.Literal.destBinop destbinop_v2
Metis_prover.Literal.destEq desteq_v2
Metis_prover.Literal.destIrrefl destirrefl
Metis_prover.Literal.destNeq destneq_v1
Metis_prover.Literal.destRefl destrefl_v2
Metis_prover.Literal.equal equal_v25
Metis_prover.Literal.freeIn freein_v3
Metis_prover.Literal.freeVars freevars_v4
Metis_prover.Literal.fromFormula fromformula
Metis_prover.Literal.functionNames functionnames_v3
Metis_prover.Literal.functions functions_v4
Metis_prover.Literal.isBinop isbinop_v2
Metis_prover.Literal.isEq iseq_v2
Metis_prover.Literal.isIrrefl isirrefl
Metis_prover.Literal.isNeq isneq_v1
Metis_prover.Literal.isRefl isrefl_v2
Metis_prover.Literal.lhs lhs_v2
Metis_prover.Literal.matchLiterals matchliterals
Metis_prover.Literal.mkBinop mkbinop_v2
Metis_prover.Literal.mkEq mkeq_v2
Metis_prover.Literal.mkIrrefl mkirrefl
Metis_prover.Literal.mkNeq mkneq_v1
Metis_prover.Literal.mkRefl mkrefl_v2
Metis_prover.Literal.name name_v2
Metis_prover.Literal.negate negate
Metis_prover.Literal.negative negative
Metis_prover.Literal.nonVarTypedSubterms nonvartypedsubterms_v2
Metis_prover.Literal.polarity polarity
Metis_prover.Literal.positive positive
Metis_prover.Literal.relation relation_v1
Metis_prover.Literal.replace replace_v2
Metis_prover.Literal.rhs rhs_v2
Metis_prover.Literal.subst subst_v3
Metis_prover.Literal.subterm subterm_v2
Metis_prover.Literal.subterms subterms_v2
Metis_prover.Literal.sym sym_v2
Metis_prover.Literal.symbols symbols_v3
Metis_prover.Literal.toFormula toformula
Metis_prover.Literal.toString tostring_v6
Metis_prover.Literal.typedSymbols typedsymbols_v2
Metis_prover.Literal.unify unify_v2
Metis_prover.Literal_net.filter filter_v29
Metis_prover.Literal_net.fromList fromlist_v20
Metis_prover.Literal_net.insert insert_v12
Metis_prover.Literal_net.matchNet matchnet_v2
Metis_prover.Literal_net.matched matched_v2
Metis_prover.Literal_net.neg neg
Metis_prover.Literal_net.newNet newnet_v2
Metis_prover.Literal_net.pos pos
Metis_prover.Literal_net.size size_v21
Metis_prover.Literal_net.toString tostring_v11
Metis_prover.Literal_net.unify unify_v5
Metis_prover.Loop.loop loop__v1
Metis_prover.Loop.run run
Metis_prover.Mlist.enumerate enumerate
Metis_prover.Mlist.find find
Metis_prover.Mlist.first first
Metis_prover.Mlist.foldl foldl
Metis_prover.Mlist.foldr foldr
Metis_prover.Mlist.null null
Metis_prover.Mlist.revDivide revdivide
Metis_prover.Mlist.sortMap sortmap
Metis_prover.Mlist.tabulate tabulate
Metis_prover.Mlist.updateNth updatenth
Metis_prover.Model.addFn addfn_v1
Metis_prover.Model.addName addname
Metis_prover.Model.appendName appendname
Metis_prover.Model.arityProjectionFixed arityprojectionfixed
Metis_prover.Model.baseFix basefix
Metis_prover.Model.basicFixed basicfixed
Metis_prover.Model.boolToInt booltoint
Metis_prover.Model.cUNKNOWN cunknown
Metis_prover.Model.cardFn cardfn
Metis_prover.Model.cardName cardname
Metis_prover.Model.check check
Metis_prover.Model.checkAtom checkatom
Metis_prover.Model.checkClause checkclause
Metis_prover.Model.checkFormula checkformula
Metis_prover.Model.checkLiteral checkliteral
Metis_prover.Model.complementFn complementfn
Metis_prover.Model.complementName complementname
Metis_prover.Model.consName consname
Metis_prover.Model.constantValuation constantvaluation
Metis_prover.Model.cutN cutn
Metis_prover.Model.default default
Metis_prover.Model.defaultFixed defaultfixed
Metis_prover.Model.defaultSize defaultsize
Metis_prover.Model.destTerm destterm
Metis_prover.Model.differenceFn differencefn
Metis_prover.Model.differenceName differencename
Metis_prover.Model.divFn divfn_v1
Metis_prover.Model.divName divname
Metis_prover.Model.dividesName dividesname
Metis_prover.Model.dividesRel dividesrel_v1
Metis_prover.Model.elementListIndex elementlistindex
Metis_prover.Model.elementListSpace elementlistspace
Metis_prover.Model.eltN eltn
Metis_prover.Model.emptyFixed emptyfixed
Metis_prover.Model.emptyFn emptyfn
Metis_prover.Model.emptyFunctions emptyfunctions
Metis_prover.Model.emptyName emptyname
Metis_prover.Model.emptyRelations emptyrelations
Metis_prover.Model.emptyValuation emptyvaluation
Metis_prover.Model.eqRel eqrel
Metis_prover.Model.evenName evenname
Metis_prover.Model.evenRel evenrel_v1
Metis_prover.Model.expFn expfn_v1
Metis_prover.Model.expInt expint
Metis_prover.Model.expName expname
Metis_prover.Model.fixMap fixmap
Metis_prover.Model.fixed0 fixed0
Metis_prover.Model.fixed1 fixed1
Metis_prover.Model.fixed2 fixed2
Metis_prover.Model.foldValuation foldvaluation
Metis_prover.Model.geName gename
Metis_prover.Model.geRel gerel_v1
Metis_prover.Model.getFunctionFixed getfunctionfixed
Metis_prover.Model.getRelationFixed getrelationfixed
Metis_prover.Model.getTables gettables
Metis_prover.Model.getValuation getvaluation
Metis_prover.Model.gtName gtname
Metis_prover.Model.gtRel gtrel_v1
Metis_prover.Model.hasTypeFn hastypefn
Metis_prover.Model.iexp iexp
Metis_prover.Model.iexp' iexp_p
Metis_prover.Model.incrementElement incrementelement
Metis_prover.Model.incrementValuation incrementvaluation
Metis_prover.Model.insertFn insertfn
Metis_prover.Model.insertFunctionFixed insertfunctionfixed
Metis_prover.Model.insertName insertname
Metis_prover.Model.insertRelationFixed insertrelationfixed
Metis_prover.Model.insertValuation insertvaluation
Metis_prover.Model.intToBool inttobool
Metis_prover.Model.interpretAtom interpretatom
Metis_prover.Model.interpretClause interpretclause
Metis_prover.Model.interpretFormula interpretformula
Metis_prover.Model.interpretFunction interpretfunction
Metis_prover.Model.interpretLiteral interpretliteral
Metis_prover.Model.interpretRelation interpretrelation
Metis_prover.Model.interpretTerm interpretterm
Metis_prover.Model.intersectFn intersectfn
Metis_prover.Model.intersectName intersectname
Metis_prover.Model.isFixedFunction isfixedfunction
Metis_prover.Model.isFixedRelation isfixedrelation
Metis_prover.Model.isZeroName iszeroname
Metis_prover.Model.isZeroRel iszerorel_v1
Metis_prover.Model.leName lename
Metis_prover.Model.leRel lerel_v1
Metis_prover.Model.lengthName lengthname
Metis_prover.Model.listFixed listfixed
Metis_prover.Model.lookupTable lookuptable
Metis_prover.Model.lookupTables lookuptables
Metis_prover.Model.ltName ltname
Metis_prover.Model.ltRel ltrel_v1
Metis_prover.Model.mapFixed mapfixed
Metis_prover.Model.maxSpace maxspace
Metis_prover.Model.memberName membername
Metis_prover.Model.memberRel memberrel
Metis_prover.Model.minMaxInterval minmaxinterval
Metis_prover.Model.modFn modfn_v1
Metis_prover.Model.modN modn
Metis_prover.Model.modName modname
Metis_prover.Model.modelTerm modelterm
Metis_prover.Model.modularFixed modularfixed
Metis_prover.Model.msize msize
Metis_prover.Model.multFn multfn_v1
Metis_prover.Model.multInt multint
Metis_prover.Model.multN multn_v1
Metis_prover.Model.multName multname
Metis_prover.Model.negFn negfn_v1
Metis_prover.Model.negName negname
Metis_prover.Model.newModel newmodel
Metis_prover.Model.newTable newtable
Metis_prover.Model.newTables newtables
Metis_prover.Model.nilName nilname
Metis_prover.Model.nullName nullname
Metis_prover.Model.numeralFn numeralfn_v1
Metis_prover.Model.numeralList numerallist
Metis_prover.Model.numeralMax numeralmax
Metis_prover.Model.numeralMin numeralmin
Metis_prover.Model.numeralName numeralname
Metis_prover.Model.oddName oddname
Metis_prover.Model.oddRel oddrel_v1
Metis_prover.Model.oneN onen_v1
Metis_prover.Model.overflowFixed overflowfixed
Metis_prover.Model.peekFixedFunction peekfixedfunction
Metis_prover.Model.peekFixedRelation peekfixedrelation
Metis_prover.Model.peekFunctionFixed peekfunctionfixed
Metis_prover.Model.peekRelationFixed peekrelationfixed
Metis_prover.Model.peekValuation peekvaluation
Metis_prover.Model.pertAtom pertatom
Metis_prover.Model.pertClause pertclause
Metis_prover.Model.pertLiteral pertliteral
Metis_prover.Model.pertTerm pertterm
Metis_prover.Model.pertTerms pertterms
Metis_prover.Model.perturb perturb
Metis_prover.Model.perturbAtom perturbatom
Metis_prover.Model.perturbClause perturbclause
Metis_prover.Model.perturbLiteral perturbliteral
Metis_prover.Model.perturbTerm perturbterm
Metis_prover.Model.pickPerturb pickperturb
Metis_prover.Model.posN posn
Metis_prover.Model.preFn prefn_v1
Metis_prover.Model.preName prename
Metis_prover.Model.projectionFixed projectionfixed
Metis_prover.Model.projectionFn projectionfn
Metis_prover.Model.projectionList projectionlist
Metis_prover.Model.projectionMax projectionmax
Metis_prover.Model.projectionMin projectionmin
Metis_prover.Model.projectionName projectionname
Metis_prover.Model.psize psize
Metis_prover.Model.randomResult randomresult
Metis_prover.Model.randomValuation randomvaluation
Metis_prover.Model.setFixed setfixed
Metis_prover.Model.setN setn
Metis_prover.Model.singletonFn singletonfn
Metis_prover.Model.singletonName singletonname
Metis_prover.Model.subFn subfn_v1
Metis_prover.Model.subName subname
Metis_prover.Model.subsetName subsetname
Metis_prover.Model.subsetRel subsetrel
Metis_prover.Model.sucFn sucfn_v1
Metis_prover.Model.sucName sucname
Metis_prover.Model.symmetricDifferenceFn symmetricdifferencefn
Metis_prover.Model.symmetricDifferenceName symmetricdifferencename
Metis_prover.Model.tailName tailname
Metis_prover.Model.union union_v35
Metis_prover.Model.unionFixed unionfixed
Metis_prover.Model.unionFn unionfn
Metis_prover.Model.unionListFixed unionlistfixed
Metis_prover.Model.unionName unionname
Metis_prover.Model.univN univn
Metis_prover.Model.universeFn universefn
Metis_prover.Model.universeName universename
Metis_prover.Model.updateFunction updatefunction
Metis_prover.Model.updateRelation updaterelation
Metis_prover.Model.updateTable updatetable
Metis_prover.Model.updateTables updatetables
Metis_prover.Model.uselessFixedFunction uselessfixedfunction
Metis_prover.Model.uselessFixedRelation uselessfixedrelation
Metis_prover.Model.zeroElement zeroelement
Metis_prover.Model.zeroValuation zerovaluation
Metis_prover.Name.Map.Ma.add add_v6
Metis_prover.Name.Map.Ma.bindings bindings_v2
Metis_prover.Name.Map.Ma.cardinal cardinal_v3
Metis_prover.Name.Map.Ma.choose choose_v3
Metis_prover.Name.Map.Ma.choose_opt choose_opt_v3
Metis_prover.Name.Map.Ma.compare compare_v12
Metis_prover.Name.Map.Ma.empty empty_v5
Metis_prover.Name.Map.Ma.equal equal_v7
Metis_prover.Name.Map.Ma.exists exists_v8
Metis_prover.Name.Map.Ma.filter filter_v7
Metis_prover.Name.Map.Ma.filter_map filter_map_v3
Metis_prover.Name.Map.Ma.find find_v4
Metis_prover.Name.Map.Ma.find_first find_first_v3
Metis_prover.Name.Map.Ma.find_first_opt find_first_opt_v3
Metis_prover.Name.Map.Ma.find_last find_last_v3
Metis_prover.Name.Map.Ma.find_last_opt find_last_opt_v3
Metis_prover.Name.Map.Ma.find_opt find_opt_v3
Metis_prover.Name.Map.Ma.fold fold_v3
Metis_prover.Name.Map.Ma.for_all for_all_v3
Metis_prover.Name.Map.Ma.is_empty is_empty_v3
Metis_prover.Name.Map.Ma.iter iter_v3
Metis_prover.Name.Map.Ma.map map_v5
Metis_prover.Name.Map.Ma.mapi mapi_v2
Metis_prover.Name.Map.Ma.max_binding max_binding_v2
Metis_prover.Name.Map.Ma.max_binding_opt max_binding_opt_v2
Metis_prover.Name.Map.Ma.mem mem_v3
Metis_prover.Name.Map.Ma.merge merge_v4
Metis_prover.Name.Map.Ma.min_binding min_binding_v2
Metis_prover.Name.Map.Ma.min_binding_opt min_binding_opt_v2
Metis_prover.Name.Map.Ma.partition partition_v5
Metis_prover.Name.Map.Ma.remove remove_v6
Metis_prover.Name.Map.Ma.singleton singleton_v8
Metis_prover.Name.Map.Ma.split split_v3
Metis_prover.Name.Map.Ma.union union_v8
Metis_prover.Name.Map.Ma.update update_v2
Metis_prover.Name.Map.delete delete_v5
Metis_prover.Name.Map.exists exists_v9
Metis_prover.Name.Map.filter filter_v8
Metis_prover.Name.Map.foldl foldl_v6
Metis_prover.Name.Map.foldr foldr_v6
Metis_prover.Name.Map.fromList fromlist_v5
Metis_prover.Name.Map.get get_v3
Metis_prover.Name.Map.inDomain indomain_v3
Metis_prover.Name.Map.insert insert_v3
Metis_prover.Name.Map.mapPartial mappartial_v4
Metis_prover.Name.Map.newMap newmap_v3
Metis_prover.Name.Map.null null_v7
Metis_prover.Name.Map.peek peek_v4
Metis_prover.Name.Map.singleton singleton_v9
Metis_prover.Name.Map.size size_v6
Metis_prover.Name.Map.toList tolist_v6
Metis_prover.Name.Map.transform transform_v5
Metis_prover.Name.Map.union union_v9
Metis_prover.Name.Ordered.compare compare_v11
Metis_prover.Name.Set.Se.add add_v7
Metis_prover.Name.Set.Se.cardinal cardinal_v4
Metis_prover.Name.Set.Se.choose choose_v4
Metis_prover.Name.Set.Se.choose_opt choose_opt_v4
Metis_prover.Name.Set.Se.compare compare_v13
Metis_prover.Name.Set.Se.diff diff_v1
Metis_prover.Name.Set.Se.disjoint disjoint_v2
Metis_prover.Name.Set.Se.elements elements_v1
Metis_prover.Name.Set.Se.empty empty_v6
Metis_prover.Name.Set.Se.equal equal_v8
Metis_prover.Name.Set.Se.exists exists_v10
Metis_prover.Name.Set.Se.filter filter_v9
Metis_prover.Name.Set.Se.filter_map filter_map_v4
Metis_prover.Name.Set.Se.find find_v5
Metis_prover.Name.Set.Se.find_first find_first_v4
Metis_prover.Name.Set.Se.find_first_opt find_first_opt_v4
Metis_prover.Name.Set.Se.find_last find_last_v4
Metis_prover.Name.Set.Se.find_last_opt find_last_opt_v4
Metis_prover.Name.Set.Se.find_opt find_opt_v4
Metis_prover.Name.Set.Se.fold fold_v4
Metis_prover.Name.Set.Se.for_all for_all_v4
Metis_prover.Name.Set.Se.inter inter_v1
Metis_prover.Name.Set.Se.is_empty is_empty_v4
Metis_prover.Name.Set.Se.iter iter_v4
Metis_prover.Name.Set.Se.map map_v6
Metis_prover.Name.Set.Se.max_elt max_elt_v1
Metis_prover.Name.Set.Se.max_elt_opt max_elt_opt_v1
Metis_prover.Name.Set.Se.mem mem_v4
Metis_prover.Name.Set.Se.min_elt min_elt_v1
Metis_prover.Name.Set.Se.min_elt_opt min_elt_opt_v1
Metis_prover.Name.Set.Se.partition partition_v6
Metis_prover.Name.Set.Se.remove remove_v7
Metis_prover.Name.Set.Se.singleton singleton_v10
Metis_prover.Name.Set.Se.split split_v4
Metis_prover.Name.Set.Se.subset subset_v3
Metis_prover.Name.Set.Se.union union_v10
Metis_prover.Name.Set.add add_v8
Metis_prover.Name.Set.all all_v3
Metis_prover.Name.Set.compare compare_v14
Metis_prover.Name.Set.count count_v3
Metis_prover.Name.Set.delete delete_v6
Metis_prover.Name.Set.difference difference_v2
Metis_prover.Name.Set.empty empty_v7
Metis_prover.Name.Set.equal equal_v9
Metis_prover.Name.Set.exists exists_v11
Metis_prover.Name.Set.findl findl_v3
Metis_prover.Name.Set.firstl firstl_v3
Metis_prover.Name.Set.foldl foldl_v7
Metis_prover.Name.Set.foldr foldr_v7
Metis_prover.Name.Set.fromList fromlist_v6
Metis_prover.Name.Set.intersect intersect_v3
Metis_prover.Name.Set.intersectList intersectlist_v2
Metis_prover.Name.Set.member member_v2
Metis_prover.Name.Set.null null_v8
Metis_prover.Name.Set.pick pick_v3
Metis_prover.Name.Set.singleton singleton_v11
Metis_prover.Name.Set.size size_v7
Metis_prover.Name.Set.subset subset_v4
Metis_prover.Name.Set.toList tolist_v7
Metis_prover.Name.Set.transform transform_v6
Metis_prover.Name.Set.union union_v11
Metis_prover.Name.compare compare_v10
Metis_prover.Name.equal equal_v6
Metis_prover.Name.fromString fromstring
Metis_prover.Name.newName newname
Metis_prover.Name.newNames newnames
Metis_prover.Name.numName numname
Metis_prover.Name.prefix prefix
Metis_prover.Name.toString tostring_v3
Metis_prover.Name.variantNum variantnum
Metis_prover.Name.variantPrime variantprime
Metis_prover.Name_arity.Map.Ma.add add_v9
Metis_prover.Name_arity.Map.Ma.bindings bindings_v3
Metis_prover.Name_arity.Map.Ma.cardinal cardinal_v5
Metis_prover.Name_arity.Map.Ma.choose choose_v5
Metis_prover.Name_arity.Map.Ma.choose_opt choose_opt_v5
Metis_prover.Name_arity.Map.Ma.compare compare_v17
Metis_prover.Name_arity.Map.Ma.empty empty_v8
Metis_prover.Name_arity.Map.Ma.equal equal_v11
Metis_prover.Name_arity.Map.Ma.exists exists_v12
Metis_prover.Name_arity.Map.Ma.filter filter_v10
Metis_prover.Name_arity.Map.Ma.filter_map filter_map_v5
Metis_prover.Name_arity.Map.Ma.find find_v6
Metis_prover.Name_arity.Map.Ma.find_first find_first_v5
Metis_prover.Name_arity.Map.Ma.find_first_opt find_first_opt_v5
Metis_prover.Name_arity.Map.Ma.find_last find_last_v5
Metis_prover.Name_arity.Map.Ma.find_last_opt find_last_opt_v5
Metis_prover.Name_arity.Map.Ma.find_opt find_opt_v5
Metis_prover.Name_arity.Map.Ma.fold fold_v5
Metis_prover.Name_arity.Map.Ma.for_all for_all_v5
Metis_prover.Name_arity.Map.Ma.is_empty is_empty_v5
Metis_prover.Name_arity.Map.Ma.iter iter_v5
Metis_prover.Name_arity.Map.Ma.map map_v7
Metis_prover.Name_arity.Map.Ma.mapi mapi_v3
Metis_prover.Name_arity.Map.Ma.max_binding max_binding_v3
Metis_prover.Name_arity.Map.Ma.max_binding_opt max_binding_opt_v3
Metis_prover.Name_arity.Map.Ma.mem mem_v5
Metis_prover.Name_arity.Map.Ma.merge merge_v5
Metis_prover.Name_arity.Map.Ma.min_binding min_binding_v3
Metis_prover.Name_arity.Map.Ma.min_binding_opt min_binding_opt_v3
Metis_prover.Name_arity.Map.Ma.partition partition_v7
Metis_prover.Name_arity.Map.Ma.remove remove_v8
Metis_prover.Name_arity.Map.Ma.singleton singleton_v12
Metis_prover.Name_arity.Map.Ma.split split_v5
Metis_prover.Name_arity.Map.Ma.union union_v12
Metis_prover.Name_arity.Map.Ma.update update_v3
Metis_prover.Name_arity.Map.compose compose
Metis_prover.Name_arity.Map.delete delete_v7
Metis_prover.Name_arity.Map.exists exists_v13
Metis_prover.Name_arity.Map.filter filter_v11
Metis_prover.Name_arity.Map.foldl foldl_v8
Metis_prover.Name_arity.Map.foldr foldr_v8
Metis_prover.Name_arity.Map.fromList fromlist_v7
Metis_prover.Name_arity.Map.get get_v4
Metis_prover.Name_arity.Map.inDomain indomain_v4
Metis_prover.Name_arity.Map.insert insert_v4
Metis_prover.Name_arity.Map.mapPartial mappartial_v5
Metis_prover.Name_arity.Map.newMap newmap_v4
Metis_prover.Name_arity.Map.null null_v9
Metis_prover.Name_arity.Map.peek peek_v5
Metis_prover.Name_arity.Map.singleton singleton_v13
Metis_prover.Name_arity.Map.size size_v8
Metis_prover.Name_arity.Map.toList tolist_v8
Metis_prover.Name_arity.Map.transform transform_v7
Metis_prover.Name_arity.Map.union union_v13
Metis_prover.Name_arity.Ordered.compare compare_v16
Metis_prover.Name_arity.Set.Se.add add_v10
Metis_prover.Name_arity.Set.Se.cardinal cardinal_v6
Metis_prover.Name_arity.Set.Se.choose choose_v6
Metis_prover.Name_arity.Set.Se.choose_opt choose_opt_v6
Metis_prover.Name_arity.Set.Se.compare compare_v18
Metis_prover.Name_arity.Set.Se.diff diff_v2
Metis_prover.Name_arity.Set.Se.disjoint disjoint_v3
Metis_prover.Name_arity.Set.Se.elements elements_v2
Metis_prover.Name_arity.Set.Se.empty empty_v9
Metis_prover.Name_arity.Set.Se.equal equal_v12
Metis_prover.Name_arity.Set.Se.exists exists_v14
Metis_prover.Name_arity.Set.Se.filter filter_v12
Metis_prover.Name_arity.Set.Se.filter_map filter_map_v6
Metis_prover.Name_arity.Set.Se.find find_v7
Metis_prover.Name_arity.Set.Se.find_first find_first_v6
Metis_prover.Name_arity.Set.Se.find_first_opt find_first_opt_v6
Metis_prover.Name_arity.Set.Se.find_last find_last_v6
Metis_prover.Name_arity.Set.Se.find_last_opt find_last_opt_v6
Metis_prover.Name_arity.Set.Se.find_opt find_opt_v6
Metis_prover.Name_arity.Set.Se.fold fold_v6
Metis_prover.Name_arity.Set.Se.for_all for_all_v6
Metis_prover.Name_arity.Set.Se.inter inter_v2
Metis_prover.Name_arity.Set.Se.is_empty is_empty_v6
Metis_prover.Name_arity.Set.Se.iter iter_v6
Metis_prover.Name_arity.Set.Se.map map_v8
Metis_prover.Name_arity.Set.Se.max_elt max_elt_v2
Metis_prover.Name_arity.Set.Se.max_elt_opt max_elt_opt_v2
Metis_prover.Name_arity.Set.Se.mem mem_v6
Metis_prover.Name_arity.Set.Se.min_elt min_elt_v2
Metis_prover.Name_arity.Set.Se.min_elt_opt min_elt_opt_v2
Metis_prover.Name_arity.Set.Se.partition partition_v8
Metis_prover.Name_arity.Set.Se.remove remove_v9
Metis_prover.Name_arity.Set.Se.singleton singleton_v14
Metis_prover.Name_arity.Set.Se.split split_v6
Metis_prover.Name_arity.Set.Se.subset subset_v5
Metis_prover.Name_arity.Set.Se.union union_v14
Metis_prover.Name_arity.Set.add add_v11
Metis_prover.Name_arity.Set.all all_v4
Metis_prover.Name_arity.Set.allNullary allnullary
Metis_prover.Name_arity.Set.compare compare_v19
Metis_prover.Name_arity.Set.count count_v4
Metis_prover.Name_arity.Set.delete delete_v8
Metis_prover.Name_arity.Set.difference difference_v3
Metis_prover.Name_arity.Set.empty empty_v10
Metis_prover.Name_arity.Set.equal equal_v13
Metis_prover.Name_arity.Set.exists exists_v15
Metis_prover.Name_arity.Set.findl findl_v4
Metis_prover.Name_arity.Set.firstl firstl_v4
Metis_prover.Name_arity.Set.foldl foldl_v9
Metis_prover.Name_arity.Set.foldr foldr_v9
Metis_prover.Name_arity.Set.fromList fromlist_v8
Metis_prover.Name_arity.Set.intersect intersect_v4
Metis_prover.Name_arity.Set.intersectList intersectlist_v3
Metis_prover.Name_arity.Set.member member_v3
Metis_prover.Name_arity.Set.null null_v10
Metis_prover.Name_arity.Set.pick pick_v4
Metis_prover.Name_arity.Set.singleton singleton_v15
Metis_prover.Name_arity.Set.size size_v9
Metis_prover.Name_arity.Set.subset subset_v6
Metis_prover.Name_arity.Set.toList tolist_v9
Metis_prover.Name_arity.Set.transform transform_v8
Metis_prover.Name_arity.Set.union union_v15
Metis_prover.Name_arity.arity arity
Metis_prover.Name_arity.binary binary
Metis_prover.Name_arity.compare compare_v15
Metis_prover.Name_arity.equal equal_v10
Metis_prover.Name_arity.name name
Metis_prover.Name_arity.nary nary
Metis_prover.Name_arity.nullary nullary
Metis_prover.Name_arity.ternary ternary
Metis_prover.Name_arity.unary unary
Metis_prover.Option.bind bind
Metis_prover.Option.is_some is_some
Metis_prover.Option.value value
Metis_prover.Pmap.addLeftToRightIterator addlefttorightiterator
Metis_prover.Pmap.addRightToLeftIterator addrighttoleftiterator
Metis_prover.Pmap.addSidePath addsidepath
Metis_prover.Pmap.addSidesPath addsidespath
Metis_prover.Pmap.advanceIterator advanceiterator
Metis_prover.Pmap.all all
Metis_prover.Pmap.app app
Metis_prover.Pmap.compare compare_v1
Metis_prover.Pmap.compareIterator compareiterator
Metis_prover.Pmap.comparePriority comparepriority
Metis_prover.Pmap.count count
Metis_prover.Pmap.delete delete
Metis_prover.Pmap.deleteNth deletenth
Metis_prover.Pmap.deletePick deletepick
Metis_prover.Pmap.deleteRandom deleterandom
Metis_prover.Pmap.differenceDomain differencedomain
Metis_prover.Pmap.disjointDomain disjointdomain
Metis_prover.Pmap.equal equal
Metis_prover.Pmap.equalDomain equaldomain
Metis_prover.Pmap.equalIterator equaliterator
Metis_prover.Pmap.equalKey equalkey
Metis_prover.Pmap.exists exists
Metis_prover.Pmap.filter filter
Metis_prover.Pmap.findIterator finditerator
Metis_prover.Pmap.findl findl
Metis_prover.Pmap.findr findr
Metis_prover.Pmap.firstIterator firstiterator
Metis_prover.Pmap.firstl firstl
Metis_prover.Pmap.firstr firstr
Metis_prover.Pmap.foldIterator folditerator
Metis_prover.Pmap.foldl foldl_v1
Metis_prover.Pmap.foldr foldr_v1
Metis_prover.Pmap.fromList fromlist
Metis_prover.Pmap.fromSpineLeftToRightIterator fromspinelefttorightiterator
Metis_prover.Pmap.fromSpineRightToLeftIterator fromspinerighttoleftiterator
Metis_prover.Pmap.get get
Metis_prover.Pmap.inDomain indomain
Metis_prover.Pmap.insert insert
Metis_prover.Pmap.insertList insertlist
Metis_prover.Pmap.insertNodePath insertnodepath
Metis_prover.Pmap.intersect intersect
Metis_prover.Pmap.intersectDomain intersectdomain
Metis_prover.Pmap.intersectListDomain intersectlistdomain
Metis_prover.Pmap.keys keys
Metis_prover.Pmap.lowerPriorityNode lowerprioritynode
Metis_prover.Pmap.map map
Metis_prover.Pmap.mapPartial mappartial
Metis_prover.Pmap.merge merge
Metis_prover.Pmap.mkIterator mkiterator
Metis_prover.Pmap.mkNode mknode
Metis_prover.Pmap.mkNodeSingleton mknodesingleton
Metis_prover.Pmap.mkRevIterator mkreviterator
Metis_prover.Pmap.mkSidesPath mksidespath
Metis_prover.Pmap.mkTree mktree
Metis_prover.Pmap.newMap newmap
Metis_prover.Pmap.nodeDelete nodedelete
Metis_prover.Pmap.nodeDeleteNth nodedeletenth
Metis_prover.Pmap.nodeDeletePick nodedeletepick
Metis_prover.Pmap.nodeDifferenceDomain nodedifferencedomain
Metis_prover.Pmap.nodeIntersect nodeintersect
Metis_prover.Pmap.nodeIntersectDomain nodeintersectdomain
Metis_prover.Pmap.nodeLeftSpine nodeleftspine
Metis_prover.Pmap.nodeMap nodemap
Metis_prover.Pmap.nodeMapPartial nodemappartial
Metis_prover.Pmap.nodeMerge nodemerge
Metis_prover.Pmap.nodeNth nodenth
Metis_prover.Pmap.nodePartition nodepartition
Metis_prover.Pmap.nodePeek nodepeek
Metis_prover.Pmap.nodePeekKey nodepeekkey
Metis_prover.Pmap.nodePeekPath nodepeekpath
Metis_prover.Pmap.nodePick nodepick
Metis_prover.Pmap.nodeRightSpine noderightspine
Metis_prover.Pmap.nodeSingleton nodesingleton
Metis_prover.Pmap.nodeSize nodesize
Metis_prover.Pmap.nodeSubsetDomain nodesubsetdomain
Metis_prover.Pmap.nodeUnion nodeunion
Metis_prover.Pmap.nodeUnionDomain nodeuniondomain
Metis_prover.Pmap.nth nth
Metis_prover.Pmap.null null_v1
Metis_prover.Pmap.partition partition
Metis_prover.Pmap.peek peek
Metis_prover.Pmap.peekKey peekkey
Metis_prover.Pmap.pick pick
Metis_prover.Pmap.random random
Metis_prover.Pmap.randomPriority randompriority
Metis_prover.Pmap.readIterator readiterator
Metis_prover.Pmap.remove remove
Metis_prover.Pmap.singleton singleton
Metis_prover.Pmap.size size
Metis_prover.Pmap.subsetDomain subsetdomain
Metis_prover.Pmap.symmetricDifferenceDomain symmetricdifferencedomain
Metis_prover.Pmap.toList tolist
Metis_prover.Pmap.toString tostring
Metis_prover.Pmap.transform transform
Metis_prover.Pmap.treeAppend treeappend
Metis_prover.Pmap.treeCombine treecombine
Metis_prover.Pmap.treeDelete treedelete
Metis_prover.Pmap.treeDeleteNth treedeletenth
Metis_prover.Pmap.treeDeletePick treedeletepick
Metis_prover.Pmap.treeDifferenceDomain treedifferencedomain
Metis_prover.Pmap.treeInsert treeinsert
Metis_prover.Pmap.treeIntersect treeintersect
Metis_prover.Pmap.treeIntersectDomain treeintersectdomain
Metis_prover.Pmap.treeLeftSpine treeleftspine
Metis_prover.Pmap.treeMap treemap
Metis_prover.Pmap.treeMapPartial treemappartial
Metis_prover.Pmap.treeMerge treemerge
Metis_prover.Pmap.treeMkIterator treemkiterator
Metis_prover.Pmap.treeMkRevIterator treemkreviterator
Metis_prover.Pmap.treeNew treenew
Metis_prover.Pmap.treeNth treenth
Metis_prover.Pmap.treePeek treepeek
Metis_prover.Pmap.treePeekKey treepeekkey
Metis_prover.Pmap.treePeekPath treepeekpath
Metis_prover.Pmap.treePick treepick
Metis_prover.Pmap.treeRightSpine treerightspine
Metis_prover.Pmap.treeSingleton treesingleton
Metis_prover.Pmap.treeSize treesize
Metis_prover.Pmap.treeSubsetDomain treesubsetdomain
Metis_prover.Pmap.treeUnion treeunion
Metis_prover.Pmap.treeUnionDomain treeuniondomain
Metis_prover.Pmap.uncurriedIntersectDomain uncurriedintersectdomain
Metis_prover.Pmap.uncurriedUnionDomain uncurrieduniondomain
Metis_prover.Pmap.union union
Metis_prover.Pmap.unionDomain uniondomain
Metis_prover.Pmap.unionListDomain unionlistdomain
Metis_prover.Pmap.updateTree updatetree
Metis_prover.Pmap.updateTreePath updatetreepath
Metis_prover.Pmap.values values
Metis_prover.Proof.freeIn freein_v6
Metis_prover.Proof.freeVars freevars_v7
Metis_prover.Proof.inferenceToThm inferencetothm
Metis_prover.Proof.parents parents
Metis_prover.Proof.proof proof
Metis_prover.Proof.reconstruct reconstruct
Metis_prover.Proof.reconstructEquality reconstructequality
Metis_prover.Proof.reconstructResolvant reconstructresolvant
Metis_prover.Proof.reconstructSubst reconstructsubst
Metis_prover.Proof.thmToInference thmtoinference
Metis_prover.Pset.add add
Metis_prover.Pset.addList addlist
Metis_prover.Pset.advanceIterator advanceiterator_v1
Metis_prover.Pset.all all_v1
Metis_prover.Pset.app app_v1
Metis_prover.Pset.compare compare_v2
Metis_prover.Pset.compareValue comparevalue
Metis_prover.Pset.count count_v1
Metis_prover.Pset.delete delete_v1
Metis_prover.Pset.deleteNth deletenth_v1
Metis_prover.Pset.deletePick deletepick_v1
Metis_prover.Pset.deleteRandom deleterandom_v1
Metis_prover.Pset.dest dest
Metis_prover.Pset.difference difference
Metis_prover.Pset.disjoint disjoint
Metis_prover.Pset.domain domain
Metis_prover.Pset.empty empty
Metis_prover.Pset.equal equal_v1
Metis_prover.Pset.equalValue equalvalue
Metis_prover.Pset.exists exists_v1
Metis_prover.Pset.filter filter_v1
Metis_prover.Pset.findl findl_v1
Metis_prover.Pset.findr findr_v1
Metis_prover.Pset.firstl firstl_v1
Metis_prover.Pset.firstr firstr_v1
Metis_prover.Pset.foldl foldl_v2
Metis_prover.Pset.foldr foldr_v2
Metis_prover.Pset.fromList fromlist_v1
Metis_prover.Pset.intersect intersect_v1
Metis_prover.Pset.intersectList intersectlist
Metis_prover.Pset.map map_v1
Metis_prover.Pset.mapPartial mappartial_v1
Metis_prover.Pset.member member
Metis_prover.Pset.mkIterator mkiterator_v1
Metis_prover.Pset.mkRevIterator mkreviterator_v1
Metis_prover.Pset.nth nth_v1
Metis_prover.Pset.null null_v2
Metis_prover.Pset.partition partition_v1
Metis_prover.Pset.peek peek_v1
Metis_prover.Pset.pick pick_v1
Metis_prover.Pset.random random_v1
Metis_prover.Pset.readIterator readiterator_v1
Metis_prover.Pset.remove remove_v1
Metis_prover.Pset.singleton singleton_v1
Metis_prover.Pset.size size_v1
Metis_prover.Pset.subset subset
Metis_prover.Pset.symmetricDifference symmetricdifference
Metis_prover.Pset.toList tolist_v1
Metis_prover.Pset.toString tostring_v1
Metis_prover.Pset.transform transform_v1
Metis_prover.Pset.uncurriedAdd uncurriedadd
Metis_prover.Pset.union union_v1
Metis_prover.Pset.unionList unionlist
Metis_prover.Resolution.active active
Metis_prover.Resolution.default default_v5
Metis_prover.Resolution.iterate iterate
Metis_prover.Resolution.loop loop_
Metis_prover.Resolution.newResolution newresolution
Metis_prover.Resolution.waiting waiting
Metis_prover.Rewrite.add add_v29
Metis_prover.Rewrite.addEqn addeqn
Metis_prover.Rewrite.addList addlist_v1
Metis_prover.Rewrite.addRedexes addredexes
Metis_prover.Rewrite.addSubterms addsubterms
Metis_prover.Rewrite.cleanRedexes cleanredexes
Metis_prover.Rewrite.cleanSubterms cleansubterms
Metis_prover.Rewrite.deleteWaiting deletewaiting
Metis_prover.Rewrite.equations equations
Metis_prover.Rewrite.findReducibles findreducibles
Metis_prover.Rewrite.ins ins_v1
Metis_prover.Rewrite.isReduced isreduced
Metis_prover.Rewrite.literalReducible literalreducible
Metis_prover.Rewrite.literalsReducible literalsreducible
Metis_prover.Rewrite.matchingRedexes matchingredexes
Metis_prover.Rewrite.mkNeqConv mkneqconv
Metis_prover.Rewrite.mkNeqConvs mkneqconvs
Metis_prover.Rewrite.neqConvsAdd neqconvsadd
Metis_prover.Rewrite.neqConvsDelete neqconvsdelete
Metis_prover.Rewrite.neqConvsEmpty neqconvsempty
Metis_prover.Rewrite.neqConvsFoldl neqconvsfoldl
Metis_prover.Rewrite.neqConvsNull neqconvsnull
Metis_prover.Rewrite.neqConvsRewrIdLiterule neqconvsrewridliterule
Metis_prover.Rewrite.neqConvsToConv neqconvstoconv
Metis_prover.Rewrite.newRewrite newrewrite
Metis_prover.Rewrite.order order
Metis_prover.Rewrite.orderToOrient ordertoorient
Metis_prover.Rewrite.orderedRewrite orderedrewrite
Metis_prover.Rewrite.orientedEquation orientedequation
Metis_prover.Rewrite.peek peek_v11
Metis_prover.Rewrite.pick pick_v9
Metis_prover.Rewrite.rebuild rebuild
Metis_prover.Rewrite.redexResidue redexresidue
Metis_prover.Rewrite.redexResidues redexresidues
Metis_prover.Rewrite.reduce reduce
Metis_prover.Rewrite.reduce' reduce_p
Metis_prover.Rewrite.reduce1 reduce1
Metis_prover.Rewrite.reduceAcc reduceacc
Metis_prover.Rewrite.reorder reorder
Metis_prover.Rewrite.rewrConv rewrconv_v1
Metis_prover.Rewrite.rewrIdConv rewridconv
Metis_prover.Rewrite.rewrIdConv' rewridconv_p
Metis_prover.Rewrite.rewrite rewrite
Metis_prover.Rewrite.rewriteConv rewriteconv
Metis_prover.Rewrite.rewriteIdConv rewriteidconv
Metis_prover.Rewrite.rewriteIdConv' rewriteidconv_p
Metis_prover.Rewrite.rewriteIdEqn' rewriteideqn_p
Metis_prover.Rewrite.rewriteIdLiteralsRule rewriteidliteralsrule
Metis_prover.Rewrite.rewriteIdLiteralsRule' rewriteidliteralsrule_p
Metis_prover.Rewrite.rewriteIdRule rewriteidrule
Metis_prover.Rewrite.rewriteIdRule' rewriteidrule_p
Metis_prover.Rewrite.rewriteLiteralsRule rewriteliteralsrule
Metis_prover.Rewrite.rewriteRule rewriterule
Metis_prover.Rewrite.sameRedexes sameredexes
Metis_prover.Rewrite.size size_v23
Metis_prover.Rewrite.termReducible termreducible
Metis_prover.Rewrite.thmReducible thmreducible
Metis_prover.Rewrite.toStringOrient tostringorient
Metis_prover.Rewrite.toStringOrientOption tostringorientoption
Metis_prover.Rewrite.uncurriedAdd uncurriedadd_v1
Metis_prover.Rewrite.updateWaiting updatewaiting
Metis_prover.Rewrite.wellOriented welloriented
Metis_prover.Rule.addFactorEdge addfactoredge
Metis_prover.Rule.addIrreflEdge addirrefledge_v1
Metis_prover.Rule.addReflEdge addrefledge_v1
Metis_prover.Rule.allArgumentsLiterule allargumentsliterule
Metis_prover.Rule.allConv allconv
Metis_prover.Rule.allLiteralsRule allliteralsrule
Metis_prover.Rule.allLiterule allliterule
Metis_prover.Rule.allRule allrule
Metis_prover.Rule.argumentLiterule argumentliterule
Metis_prover.Rule.bottomUpConv bottomupconv
Metis_prover.Rule.changedConv changedconv
Metis_prover.Rule.changedLiterule changedliterule
Metis_prover.Rule.changedRule changedrule
Metis_prover.Rule.convRule convrule
Metis_prover.Rule.equationLiteral equationliteral
Metis_prover.Rule.everyConv everyconv_v1
Metis_prover.Rule.everyLiterule everyliterule_v1
Metis_prover.Rule.everyRule everyrule_v1
Metis_prover.Rule.expandAbbrevs expandabbrevs
Metis_prover.Rule.fact fact
Metis_prover.Rule.factor factor
Metis_prover.Rule.factor' factor_p
Metis_prover.Rule.firstConv firstconv_v1
Metis_prover.Rule.firstLiterule firstliterule_v1
Metis_prover.Rule.firstRule firstrule_v1
Metis_prover.Rule.flip flip
Metis_prover.Rule.freshVars freshvars_v1
Metis_prover.Rule.functionCongruence functioncongruence
Metis_prover.Rule.init_edges init_edges
Metis_prover.Rule.joinEdge joinedge
Metis_prover.Rule.literalRule literalrule
Metis_prover.Rule.literalsRule literalsrule
Metis_prover.Rule.mk_edges mk_edges
Metis_prover.Rule.noConv noconv
Metis_prover.Rule.noLiterule noliterule
Metis_prover.Rule.noRule norule
Metis_prover.Rule.orelseConv orelseconv
Metis_prover.Rule.orelseLiterule orelseliterule
Metis_prover.Rule.orelseRule orelserule
Metis_prover.Rule.pathConv pathconv
Metis_prover.Rule.pathLiterule pathliterule
Metis_prover.Rule.pathRule pathrule
Metis_prover.Rule.reflEqn refleqn
Metis_prover.Rule.reflexivity reflexivity
Metis_prover.Rule.reflexivityRule reflexivityrule
Metis_prover.Rule.relationCongruence relationcongruence
Metis_prover.Rule.removeIrrefl removeirrefl
Metis_prover.Rule.removeSym removesym
Metis_prover.Rule.repeatConv repeatconv
Metis_prover.Rule.repeatLiterule repeatliterule
Metis_prover.Rule.repeatRule repeatrule
Metis_prover.Rule.repeatTopDownConv repeattopdownconv
Metis_prover.Rule.rewrConv rewrconv
Metis_prover.Rule.rewrLiterule rewrliterule
Metis_prover.Rule.rewrRule rewrrule
Metis_prover.Rule.simplify simplify
Metis_prover.Rule.subtermConv subtermconv
Metis_prover.Rule.subtermsConv subtermsconv
Metis_prover.Rule.sym sym_v3
Metis_prover.Rule.symEq symeq
Metis_prover.Rule.symEqn symeqn
Metis_prover.Rule.symNeq symneq
Metis_prover.Rule.symmetry symmetry
Metis_prover.Rule.symmetryRule symmetryrule
Metis_prover.Rule.thenConv thenconv
Metis_prover.Rule.thenConvTrans thenconvtrans
Metis_prover.Rule.thenLiterule thenliterule
Metis_prover.Rule.thenRule thenrule
Metis_prover.Rule.topDownConv topdownconv
Metis_prover.Rule.transEqn transeqn
Metis_prover.Rule.transitivity transitivity
Metis_prover.Rule.tryConv tryconv
Metis_prover.Rule.tryLiterule tryliterule
Metis_prover.Rule.tryRule tryrule
Metis_prover.Rule.updateApart updateapart
Metis_prover.Rule.xIVar xivar
Metis_prover.Rule.xIVarName xivarname
Metis_prover.Rule.xVar xvar
Metis_prover.Rule.xVarName xvarname
Metis_prover.Rule.yIVar yivar
Metis_prover.Rule.yIVarName yivarname
Metis_prover.Rule.yVar yvar
Metis_prover.Rule.yVarName yvarname
Metis_prover.Rule.zVar zvar
Metis_prover.Rule.zVarName zvarname
Metis_prover.Stringmap.Ma.add add_v2
Metis_prover.Stringmap.Ma.bindings bindings_v1
Metis_prover.Stringmap.Ma.cardinal cardinal_v1
Metis_prover.Stringmap.Ma.choose choose_v1
Metis_prover.Stringmap.Ma.choose_opt choose_opt_v1
Metis_prover.Stringmap.Ma.compare compare_v6
Metis_prover.Stringmap.Ma.empty empty_v2
Metis_prover.Stringmap.Ma.equal equal_v3
Metis_prover.Stringmap.Ma.exists exists_v4
Metis_prover.Stringmap.Ma.filter filter_v4
Metis_prover.Stringmap.Ma.filter_map filter_map_v1
Metis_prover.Stringmap.Ma.find find_v2
Metis_prover.Stringmap.Ma.find_first find_first_v1
Metis_prover.Stringmap.Ma.find_first_opt find_first_opt_v1
Metis_prover.Stringmap.Ma.find_last find_last_v1
Metis_prover.Stringmap.Ma.find_last_opt find_last_opt_v1
Metis_prover.Stringmap.Ma.find_opt find_opt_v1
Metis_prover.Stringmap.Ma.fold fold_v1
Metis_prover.Stringmap.Ma.for_all for_all_v1
Metis_prover.Stringmap.Ma.is_empty is_empty_v1
Metis_prover.Stringmap.Ma.iter iter_v1
Metis_prover.Stringmap.Ma.map map_v3
Metis_prover.Stringmap.Ma.mapi mapi_v1
Metis_prover.Stringmap.Ma.max_binding max_binding_v1
Metis_prover.Stringmap.Ma.max_binding_opt max_binding_opt_v1
Metis_prover.Stringmap.Ma.mem mem_v1
Metis_prover.Stringmap.Ma.merge merge_v2
Metis_prover.Stringmap.Ma.min_binding min_binding_v1
Metis_prover.Stringmap.Ma.min_binding_opt min_binding_opt_v1
Metis_prover.Stringmap.Ma.partition partition_v3
Metis_prover.Stringmap.Ma.remove remove_v3
Metis_prover.Stringmap.Ma.singleton singleton_v4
Metis_prover.Stringmap.Ma.split split_v1
Metis_prover.Stringmap.Ma.union union_v4
Metis_prover.Stringmap.Ma.update update_v1
Metis_prover.Stringmap.Ordered.compare compare_v5
Metis_prover.Stringmap.delete delete_v3
Metis_prover.Stringmap.exists exists_v5
Metis_prover.Stringmap.filter filter_v5
Metis_prover.Stringmap.foldl foldl_v4
Metis_prover.Stringmap.foldr foldr_v4
Metis_prover.Stringmap.fromList fromlist_v3
Metis_prover.Stringmap.get get_v2
Metis_prover.Stringmap.inDomain indomain_v2
Metis_prover.Stringmap.insert insert_v2
Metis_prover.Stringmap.mapPartial mappartial_v3
Metis_prover.Stringmap.newMap newmap_v2
Metis_prover.Stringmap.null null_v4
Metis_prover.Stringmap.peek peek_v3
Metis_prover.Stringmap.singleton singleton_v5
Metis_prover.Stringmap.size size_v3
Metis_prover.Stringmap.toList tolist_v3
Metis_prover.Stringmap.transform transform_v3
Metis_prover.Stringmap.union union_v5
Metis_prover.Substitute.compose compose_v1
Metis_prover.Substitute.empty empty_v13
Metis_prover.Substitute.foldl foldl_v10
Metis_prover.Substitute.foldr foldr_v10
Metis_prover.Substitute.freeVars freevars_v1
Metis_prover.Substitute.freshVars freshvars
Metis_prover.Substitute.fromList fromlist_v9
Metis_prover.Substitute.functions functions_v1
Metis_prover.Substitute.insert insert_v5
Metis_prover.Substitute.invert invert
Metis_prover.Substitute.isRenaming isrenaming
Metis_prover.Substitute.matchTerms matchterms
Metis_prover.Substitute.normalize normalize
Metis_prover.Substitute.null null_v11
Metis_prover.Substitute.peek peek_v6
Metis_prover.Substitute.redexes redexes
Metis_prover.Substitute.remove remove_v12
Metis_prover.Substitute.residueFreeVars residuefreevars
Metis_prover.Substitute.restrict restrict
Metis_prover.Substitute.singleton singleton_v18
Metis_prover.Substitute.size size_v10
Metis_prover.Substitute.subst subst
Metis_prover.Substitute.toList tolist_v10
Metis_prover.Substitute.unify unify
Metis_prover.Substitute.union union_v18
Metis_prover.Subsume.addSym addsym
Metis_prover.Subsume.clauseStrictlySubsumes clausestrictlysubsumes
Metis_prover.Subsume.clauseSubsumes clausesubsumes
Metis_prover.Subsume.clauseSym clausesym
Metis_prover.Subsume.emptySubsumes emptysubsumes
Metis_prover.Subsume.filter filter_v30
Metis_prover.Subsume.findRest findrest
Metis_prover.Subsume.genClauseSubsumes genclausesubsumes
Metis_prover.Subsume.genSubsumes gensubsumes
Metis_prover.Subsume.idCompare idcompare
Metis_prover.Subsume.idSetAdd idsetadd
Metis_prover.Subsume.idSetAddMax idsetaddmax
Metis_prover.Subsume.idSetEmpty idsetempty
Metis_prover.Subsume.idSetIntersect idsetintersect
Metis_prover.Subsume.incompatible incompatible
Metis_prover.Subsume.insert insert_v13
Metis_prover.Subsume.isStrictlySubsumed isstrictlysubsumed
Metis_prover.Subsume.isSubsumed issubsumed
Metis_prover.Subsume.matchLit matchlit
Metis_prover.Subsume.newSubsume newsubsume
Metis_prover.Subsume.nonunitSubsumes nonunitsubsumes
Metis_prover.Subsume.size size_v22
Metis_prover.Subsume.sortClause sortclause
Metis_prover.Subsume.strictlySubsumes strictlysubsumes
Metis_prover.Subsume.subsumes subsumes
Metis_prover.Subsume.toString tostring_v12
Metis_prover.Subsume.unitSubsumes unitsubsumes
Metis_prover.Term.Map.add add_v12
Metis_prover.Term.Map.bindings bindings_v4
Metis_prover.Term.Map.cardinal cardinal_v7
Metis_prover.Term.Map.choose choose_v7
Metis_prover.Term.Map.choose_opt choose_opt_v7
Metis_prover.Term.Map.compare compare_v22
Metis_prover.Term.Map.empty empty_v11
Metis_prover.Term.Map.equal equal_v15
Metis_prover.Term.Map.exists exists_v16
Metis_prover.Term.Map.filter filter_v13
Metis_prover.Term.Map.filter_map filter_map_v7
Metis_prover.Term.Map.find find_v9
Metis_prover.Term.Map.find_first find_first_v7
Metis_prover.Term.Map.find_first_opt find_first_opt_v7
Metis_prover.Term.Map.find_last find_last_v7
Metis_prover.Term.Map.find_last_opt find_last_opt_v7
Metis_prover.Term.Map.find_opt find_opt_v7
Metis_prover.Term.Map.fold fold_v7
Metis_prover.Term.Map.for_all for_all_v7
Metis_prover.Term.Map.is_empty is_empty_v7
Metis_prover.Term.Map.iter iter_v7
Metis_prover.Term.Map.map map_v9
Metis_prover.Term.Map.mapi mapi_v4
Metis_prover.Term.Map.max_binding max_binding_v4
Metis_prover.Term.Map.max_binding_opt max_binding_opt_v4
Metis_prover.Term.Map.mem mem_v7
Metis_prover.Term.Map.merge merge_v6
Metis_prover.Term.Map.min_binding min_binding_v4
Metis_prover.Term.Map.min_binding_opt min_binding_opt_v4
Metis_prover.Term.Map.partition partition_v9
Metis_prover.Term.Map.remove remove_v10
Metis_prover.Term.Map.singleton singleton_v16
Metis_prover.Term.Map.split split_v7
Metis_prover.Term.Map.union union_v16
Metis_prover.Term.Map.update update_v4
Metis_prover.Term.Ordered.compare compare_v21
Metis_prover.Term.Set.add add_v13
Metis_prover.Term.Set.cardinal cardinal_v8
Metis_prover.Term.Set.choose choose_v8
Metis_prover.Term.Set.choose_opt choose_opt_v8
Metis_prover.Term.Set.compare compare_v23
Metis_prover.Term.Set.diff diff_v3
Metis_prover.Term.Set.disjoint disjoint_v4
Metis_prover.Term.Set.elements elements_v3
Metis_prover.Term.Set.empty empty_v12
Metis_prover.Term.Set.equal equal_v16
Metis_prover.Term.Set.exists exists_v17
Metis_prover.Term.Set.filter filter_v14
Metis_prover.Term.Set.filter_map filter_map_v8
Metis_prover.Term.Set.find find_v10
Metis_prover.Term.Set.find_first find_first_v8
Metis_prover.Term.Set.find_first_opt find_first_opt_v8
Metis_prover.Term.Set.find_last find_last_v8
Metis_prover.Term.Set.find_last_opt find_last_opt_v8
Metis_prover.Term.Set.find_opt find_opt_v8
Metis_prover.Term.Set.fold fold_v8
Metis_prover.Term.Set.for_all for_all_v8
Metis_prover.Term.Set.inter inter_v3
Metis_prover.Term.Set.is_empty is_empty_v8
Metis_prover.Term.Set.iter iter_v8
Metis_prover.Term.Set.map map_v10
Metis_prover.Term.Set.max_elt max_elt_v3
Metis_prover.Term.Set.max_elt_opt max_elt_opt_v3
Metis_prover.Term.Set.mem mem_v8
Metis_prover.Term.Set.min_elt min_elt_v3
Metis_prover.Term.Set.min_elt_opt min_elt_opt_v3
Metis_prover.Term.Set.partition partition_v10
Metis_prover.Term.Set.remove remove_v11
Metis_prover.Term.Set.singleton singleton_v17
Metis_prover.Term.Set.split split_v8
Metis_prover.Term.Set.subset subset_v7
Metis_prover.Term.Set.union union_v17
Metis_prover.Term.appName appname
Metis_prover.Term.avoid avoid
Metis_prover.Term.compare compare_v20
Metis_prover.Term.destApp destapp
Metis_prover.Term.destBinop destbinop
Metis_prover.Term.destConst destconst
Metis_prover.Term.destFn destfn
Metis_prover.Term.destFnApp destfnapp
Metis_prover.Term.destFnHasType destfnhastype
Metis_prover.Term.destVar destvar
Metis_prover.Term.equal equal_v14
Metis_prover.Term.equalVar equalvar
Metis_prover.Term.fN_SYMBOLS fn_symbols
Metis_prover.Term.find find_v8
Metis_prover.Term.fnArguments fnarguments
Metis_prover.Term.fnArity fnarity
Metis_prover.Term.fnFunction fnfunction
Metis_prover.Term.fnName fnname
Metis_prover.Term.freeIn freein
Metis_prover.Term.freeVars freevars
Metis_prover.Term.freeVarsList freevarslist
Metis_prover.Term.functionNames functionnames
Metis_prover.Term.functions functions
Metis_prover.Term.hasTypeFunction hastypefunction
Metis_prover.Term.hasTypeFunctionName hastypefunctionname
Metis_prover.Term.isApp isapp
Metis_prover.Term.isBinop isbinop
Metis_prover.Term.isConst isconst
Metis_prover.Term.isFn isfn
Metis_prover.Term.isFnApp isfnapp
Metis_prover.Term.isFnHasType isfnhastype
Metis_prover.Term.isTypedVar istypedvar
Metis_prover.Term.isVar isvar
Metis_prover.Term.listMkApp listmkapp
Metis_prover.Term.mkApp mkapp
Metis_prover.Term.mkBinop mkbinop
Metis_prover.Term.mkConst mkconst
Metis_prover.Term.mkFnApp mkfnapp
Metis_prover.Term.newVar newvar
Metis_prover.Term.newVars newvars
Metis_prover.Term.nonVarTypedSubterms nonvartypedsubterms
Metis_prover.Term.replace replace
Metis_prover.Term.stripApp stripapp
Metis_prover.Term.subterm subterm
Metis_prover.Term.subterm' subterm_p
Metis_prover.Term.subterms subterms
Metis_prover.Term.symbols symbols
Metis_prover.Term.toString tostring_v4
Metis_prover.Term.typedSymbols typedsymbols
Metis_prover.Term.vAR_SYMBOLS var_symbols
Metis_prover.Term.variantNum variantnum_v1
Metis_prover.Term.variantPrime variantprime_v1
Metis_prover.Term_net.add add_v27
Metis_prover.Term_net.addFn addfn_v2
Metis_prover.Term_net.addQterm addqterm
Metis_prover.Term_net.anonymousName anonymousname
Metis_prover.Term_net.anonymousVar anonymousvar
Metis_prover.Term_net.cmp cmp
Metis_prover.Term_net.compareFnQterm comparefnqterm
Metis_prover.Term_net.compareQterm compareqterm
Metis_prover.Term_net.computeSize computesize
Metis_prover.Term_net.equalFnQterm equalfnqterm
Metis_prover.Term_net.equalQterm equalqterm
Metis_prover.Term_net.fifoize fifoize
Metis_prover.Term_net.filter filter_v27
Metis_prover.Term_net.finally finally
Metis_prover.Term_net.fnCmp fncmp
Metis_prover.Term_net.fold fold_v18
Metis_prover.Term_net.foldEqualTerms foldequalterms
Metis_prover.Term_net.foldTerms foldterms
Metis_prover.Term_net.foldUnifiableTerms foldunifiableterms
Metis_prover.Term_net.fromList fromlist_v18
Metis_prover.Term_net.idwise idwise
Metis_prover.Term_net.inc inc
Metis_prover.Term_net.ins ins
Metis_prover.Term_net.insert insert_v10
Metis_prover.Term_net.mat mat_v2
Metis_prover.Term_net.matchNet matchnet
Metis_prover.Term_net.matchQtermQterm matchqtermqterm
Metis_prover.Term_net.matchQtermTerm matchqtermterm
Metis_prover.Term_net.matchTermQterm matchtermqterm
Metis_prover.Term_net.matched matched
Metis_prover.Term_net.netSize netsize
Metis_prover.Term_net.newNet newnet
Metis_prover.Term_net.norm norm
Metis_prover.Term_net.null null_v20
Metis_prover.Term_net.oadd oadd
Metis_prover.Term_net.pre pre
Metis_prover.Term_net.qm qm_v1
Metis_prover.Term_net.qn qn
Metis_prover.Term_net.qtermToTerm qtermtoterm
Metis_prover.Term_net.qu qu
Metis_prover.Term_net.qv qv
Metis_prover.Term_net.seenInc seeninc
Metis_prover.Term_net.singles singles
Metis_prover.Term_net.size size_v19
Metis_prover.Term_net.stackAddFn stackaddfn
Metis_prover.Term_net.stackAddQterm stackaddqterm
Metis_prover.Term_net.stackEmpty stackempty
Metis_prover.Term_net.stackValue stackvalue
Metis_prover.Term_net.termToQterm termtoqterm
Metis_prover.Term_net.toString tostring_v9
Metis_prover.Term_net.unify unify_v3
Metis_prover.Term_net.unifyQtermQterm unifyqtermqterm
Metis_prover.Term_net.unifyQtermTerm unifyqtermterm
Metis_prover.Term_net.unseenInc unseeninc
Metis_prover.Thm.assume assume
Metis_prover.Thm.axiom axiom
Metis_prover.Thm.clause clause
Metis_prover.Thm.compare compare_v43
Metis_prover.Thm.destUnit destunit
Metis_prover.Thm.destUnitEq destuniteq
Metis_prover.Thm.equal equal_v32
Metis_prover.Thm.equality equality
Metis_prover.Thm.freeIn freein_v5
Metis_prover.Thm.freeVars freevars_v6
Metis_prover.Thm.inference inference
Metis_prover.Thm.inferenceTypeToString inferencetypetostring
Metis_prover.Thm.isContradiction iscontradiction
Metis_prover.Thm.isTautology istautology
Metis_prover.Thm.isUnit isunit
Metis_prover.Thm.isUnitEq isuniteq
Metis_prover.Thm.member member_v8
Metis_prover.Thm.negateMember negatemember_v1
Metis_prover.Thm.print_proof print_proof
Metis_prover.Thm.refl refl
Metis_prover.Thm.resolve resolve
Metis_prover.Thm.subst subst_v5
Metis_prover.Thm.toString tostring_v8
Metis_prover.Units.add add_v30
Metis_prover.Units.addList addlist_v2
Metis_prover.Units.empty empty_v26
Metis_prover.Units.matchUnits matchunits
Metis_prover.Units.reduce reduce_v1
Metis_prover.Units.size size_v24
Metis_prover.Units.toString tostring_v13
Metis_prover.Useful.boolCompare boolcompare
Metis_prover.Useful.critical critical
Metis_prover.Useful.divides divides_v1
Metis_prover.Useful.exp exp
Metis_prover.Useful.generator generator
Metis_prover.Useful.intCompare intcompare
Metis_prover.Useful.interval interval
Metis_prover.Useful.isDigit isdigit
Metis_prover.Useful.lexCompare lexcompare
Metis_prover.Useful.mkPrefix mkprefix
Metis_prover.Useful.newInt newint
Metis_prover.Useful.newIntThunk newintthunk
Metis_prover.Useful.newInts newints
Metis_prover.Useful.newIntsThunk newintsthunk
Metis_prover.Useful.prodCompare prodcompare
Metis_prover.Useful.revCompare revcompare
Metis_prover.Useful.stripSuffix stripsuffix
Metis_prover.Useful.total total
Metis_prover.Waiting.add add_v32
Metis_prover.Waiting.add' add_p
Metis_prover.Waiting.checkModels checkmodels
Metis_prover.Waiting.clauseLiterals clauseliterals
Metis_prover.Waiting.clausePriority clausepriority
Metis_prover.Waiting.clauseSymbols clausesymbols
Metis_prover.Waiting.clauseVariables clausevariables
Metis_prover.Waiting.clauseWeight clauseweight
Metis_prover.Waiting.cmp cmp_v1
Metis_prover.Waiting.default default_v4
Metis_prover.Waiting.defaultModels defaultmodels
Metis_prover.Waiting.empty empty_v28
Metis_prover.Waiting.initialModel initialmodel
Metis_prover.Waiting.mkModelClause mkmodelclause
Metis_prover.Waiting.mkModelClauses mkmodelclauses
Metis_prover.Waiting.newWaiting newwaiting
Metis_prover.Waiting.perturbModel perturbmodel
Metis_prover.Waiting.perturbModels perturbmodels
Metis_prover.Waiting.remove remove_v21
Metis_prover.Waiting.size size_v26
Metis_prover.Waiting.toString tostring_v16
Metis_prover.Word.andb andb
Metis_prover.Word.compare compare
Metis_prover.Word.fromInt fromint
Metis_prover.Word.minus minus
Metis_prover.Word.notb notb
Metis_prover.Word.orb orb
Metis_prover.Word.shiftLeft shiftleft
Metis_prover.Word.shiftRight shiftright
Metis_prover.Word.toInt toint
Metis_prover.Word.xorb xorb
Metis_reconstruct2.hol_of_thm hol_of_thm
Metis_reconstruct2.match_elems match_elems
Metis_reconstruct2.match_fo_ho_clause match_fo_ho_clause
Metis_reconstruct2.reorient_tysubst reorient_tysubst
Metis_reconstruct2.string_of_instantiation string_of_instantiation
Metis_reconstruct2.string_of_tminst string_of_tminst
Metis_reconstruct2.string_of_tyinst string_of_tyinst
Metis_reconstruct2.term_eq_mod_type term_eq_mod_type
Metis_rules.DISCH_DISJ disch_disj
Metis_rules.DISCH_DISJS disch_disjs
Metis_rules.FRONT front
Metis_rules.RESOLVE resolve_v2
Metis_rules.RESOLVE_N resolve_n
Metis_unify.unify_fo_ho_atom unify_fo_ho_atom
Metis_unify.unify_fo_ho_literal unify_fo_ho_literal
Metis_unify.unify_fo_ho_term unify_fo_ho_term
Metis_unify.verb verb
Preterm.env_of_preterm env_of_preterm
Preterm.env_of_th env_of_th
Preterm.env_of_ths env_of_ths
Preterm.list_mk_combp list_mk_combp
Preterm.list_mk_disjp list_mk_disjp
Preterm.mk_conjp mk_conjp
Preterm.mk_disjp mk_disjp
Preterm.mk_eqp mk_eqp
Preterm.mk_negp mk_negp
Preterm.unconst_preterm unconst_preterm
exn:Metis_prover.Heap.Empty Empty
exn:Metis_prover.Useful.Bug Bug
exn:Metis_unify.Unify Unify
metisverb metisverb
type:Active.active Active
type:Active.active_t ActiveT
type:Active.parameters Parameters5
type:Active.simplify Simplify
type:Atom.Map.Ma.key Key5
type:Atom.Map.Ma.t T16
type:Atom.Map.map Map6
type:Atom.Ordered.t T15
type:Atom.Set.Se.elt Elt4
type:Atom.Set.Se.t T17
type:Atom.Set.set Set4
type:Atom.atom Atom
type:Atom.relation Relation
type:Atom.relationName RelationName
type:Atom_net.atomNet AtomNet
type:Atom_net.parameters Parameters2
type:Ax_cj.ax_cj_cl AxCjCl
type:Ax_cj.ax_cj_thm AxCjThm
type:Clause.clause Clause1
type:Clause.clauseId ClauseId1
type:Clause.clauseInfo ClauseInfo
type:Clause.literalOrder LiteralOrder
type:Clause.parameters Parameters4
type:Formula.Map.Ma.key Key6
type:Formula.Map.Ma.t T19
type:Formula.Map.map Map7
type:Formula.Ordered.t T18
type:Formula.Set.Se.elt Elt5
type:Formula.Set.Se.t T20
type:Formula.Set.set Set5
type:Formula.formula Formula
type:Heap.heap Heap
type:Heap.node Node1
type:Intmap.Ma.key Key
type:Intmap.Ma.t T1
type:Intmap.Ordered.t T
type:Intmap.map Map2
type:Intset.Ordered.t T4
type:Intset.Se.elt Elt
type:Intset.Se.t T5
type:Intset.set Set1
type:Knuth_bendix_order.kbo Kbo
type:Knuth_bendix_order.weight Weight
type:Literal.Map.Ma.key Key7
type:Literal.Map.Ma.t T22
type:Literal.Map.map Map8
type:Literal.Ordered.t T21
type:Literal.Set.Se.elt Elt6
type:Literal.Set.Se.t T23
type:Literal.Set.set Set6
type:Literal.Set_map.Ma.key Key8
type:Literal.Set_map.Ma.t T25
type:Literal.Set_map.map Map9
type:Literal.Set_ordered.t T24
type:Literal.Set_set.Se.elt Elt7
type:Literal.Set_set.Se.t T26
type:Literal.Set_set.set Set7
type:Literal.literal Literal
type:Literal.polarity Polarity
type:Literal_net.literalNet LiteralNet
type:Literal_net.parameters Parameters3
type:Ma.key Key8
type:Ma.t T25
type:Map.Ma.key Key7
type:Map.Ma.t T22
type:Map.key Key4
type:Map.map Map8
type:Map.t T13
type:Metis_prover.Active.active Active
type:Metis_prover.Active.active_t ActiveT
type:Metis_prover.Active.parameters Parameters5
type:Metis_prover.Active.simplify Simplify
type:Metis_prover.Atom.Map.Ma.key Key5
type:Metis_prover.Atom.Map.Ma.t T16
type:Metis_prover.Atom.Map.map Map6
type:Metis_prover.Atom.Ordered.t T15
type:Metis_prover.Atom.Set.Se.elt Elt4
type:Metis_prover.Atom.Set.Se.t T17
type:Metis_prover.Atom.Set.set Set4
type:Metis_prover.Atom.atom Atom
type:Metis_prover.Atom.relation Relation
type:Metis_prover.Atom.relationName RelationName
type:Metis_prover.Atom_net.atomNet AtomNet
type:Metis_prover.Atom_net.parameters Parameters2
type:Metis_prover.Ax_cj.ax_cj_cl AxCjCl
type:Metis_prover.Ax_cj.ax_cj_thm AxCjThm
type:Metis_prover.Clause.clause Clause1
type:Metis_prover.Clause.clauseId ClauseId1
type:Metis_prover.Clause.clauseInfo ClauseInfo
type:Metis_prover.Clause.literalOrder LiteralOrder
type:Metis_prover.Clause.parameters Parameters4
type:Metis_prover.Formula.Map.Ma.key Key6
type:Metis_prover.Formula.Map.Ma.t T19
type:Metis_prover.Formula.Map.map Map7
type:Metis_prover.Formula.Ordered.t T18
type:Metis_prover.Formula.Set.Se.elt Elt5
type:Metis_prover.Formula.Set.Se.t T20
type:Metis_prover.Formula.Set.set Set5
type:Metis_prover.Formula.formula Formula
type:Metis_prover.Heap.heap Heap
type:Metis_prover.Heap.node Node1
type:Metis_prover.Intmap.Ma.key Key
type:Metis_prover.Intmap.Ma.t T1
type:Metis_prover.Intmap.Ordered.t T
type:Metis_prover.Intmap.map Map2
type:Metis_prover.Intset.Ordered.t T4
type:Metis_prover.Intset.Se.elt Elt
type:Metis_prover.Intset.Se.t T5
type:Metis_prover.Intset.set Set1
type:Metis_prover.Knuth_bendix_order.kbo Kbo
type:Metis_prover.Knuth_bendix_order.weight Weight
type:Metis_prover.Literal.Map.Ma.key Key7
type:Metis_prover.Literal.Map.Ma.t T22
type:Metis_prover.Literal.Map.map Map8
type:Metis_prover.Literal.Ordered.t T21
type:Metis_prover.Literal.Set.Se.elt Elt6
type:Metis_prover.Literal.Set.Se.t T23
type:Metis_prover.Literal.Set.set Set6
type:Metis_prover.Literal.Set_map.Ma.key Key8
type:Metis_prover.Literal.Set_map.Ma.t T25
type:Metis_prover.Literal.Set_map.map Map9
type:Metis_prover.Literal.Set_ordered.t T24
type:Metis_prover.Literal.Set_set.Se.elt Elt7
type:Metis_prover.Literal.Set_set.Se.t T26
type:Metis_prover.Literal.Set_set.set Set7
type:Metis_prover.Literal.literal Literal
type:Metis_prover.Literal.polarity Polarity
type:Metis_prover.Literal_net.literalNet LiteralNet
type:Metis_prover.Literal_net.parameters Parameters3
type:Metis_prover.Model.element Element
type:Metis_prover.Model.fixed Fixed
type:Metis_prover.Model.fixedFunction FixedFunction
type:Metis_prover.Model.fixedMap FixedMap
type:Metis_prover.Model.fixedRelation FixedRelation
type:Metis_prover.Model.model Model
type:Metis_prover.Model.modelTerm ModelTerm
type:Metis_prover.Model.parameters Parameters
type:Metis_prover.Model.perturbation Perturbation
type:Metis_prover.Model.size Size
type:Metis_prover.Model.table Table
type:Metis_prover.Model.tables Tables
type:Metis_prover.Model.valuation Valuation
type:Metis_prover.Name.Map.Ma.key Key2
type:Metis_prover.Name.Map.Ma.t T7
type:Metis_prover.Name.Map.map Map4
type:Metis_prover.Name.Ordered.t T6
type:Metis_prover.Name.Set.Se.elt Elt1
type:Metis_prover.Name.Set.Se.t T8
type:Metis_prover.Name.Set.set Set2
type:Metis_prover.Name.name Name
type:Metis_prover.Name_arity.Map.Ma.key Key3
type:Metis_prover.Name_arity.Map.Ma.t T10
type:Metis_prover.Name_arity.Map.map Map5
type:Metis_prover.Name_arity.Ordered.t T9
type:Metis_prover.Name_arity.Set.Se.elt Elt2
type:Metis_prover.Name_arity.Set.Se.t T11
type:Metis_prover.Name_arity.Set.set Set3
type:Metis_prover.Name_arity.nameArity NameArity
type:Metis_prover.Pmap.iterator Iterator
type:Metis_prover.Pmap.map Map
type:Metis_prover.Pmap.node Node
type:Metis_prover.Pmap.priority Priority
type:Metis_prover.Pmap.tree Tree
type:Metis_prover.Proof.inference Inference1
type:Metis_prover.Proof.proof Proof
type:Metis_prover.Pset.iterator Iterator1
type:Metis_prover.Pset.map Map1
type:Metis_prover.Pset.set Set
type:Metis_prover.Resolution.decision Decision
type:Metis_prover.Resolution.parameters Parameters7
type:Metis_prover.Resolution.resolution Resolution
type:Metis_prover.Resolution.resolution_t ResolutionT
type:Metis_prover.Resolution.state State
type:Metis_prover.Rewrite.equation Equation1
type:Metis_prover.Rewrite.equationId EquationId
type:Metis_prover.Rewrite.neqConvs NeqConvs
type:Metis_prover.Rewrite.orient Orient
type:Metis_prover.Rewrite.reductionOrder ReductionOrder
type:Metis_prover.Rewrite.rewrite Rewrite
type:Metis_prover.Rewrite.rewrite_t RewriteT
type:Metis_prover.Rule.conv Conv
type:Metis_prover.Rule.edge Edge
type:Metis_prover.Rule.equation Equation
type:Metis_prover.Rule.joinStatus JoinStatus
type:Metis_prover.Rule.literule Literule
type:Metis_prover.Rule.rule Rule
type:Metis_prover.Stringmap.Ma.key Key1
type:Metis_prover.Stringmap.Ma.t T3
type:Metis_prover.Stringmap.Ordered.t T2
type:Metis_prover.Stringmap.map Map3
type:Metis_prover.Substitute.subst Subst
type:Metis_prover.Subsume.clauseId ClauseId
type:Metis_prover.Subsume.clauseLength ClauseLength
type:Metis_prover.Subsume.idSet IdSet
type:Metis_prover.Subsume.nonunit_t NonunitT
type:Metis_prover.Subsume.subsume Subsume
type:Metis_prover.Term.Map.key Key4
type:Metis_prover.Term.Map.t T13
type:Metis_prover.Term.Ordered.t T12
type:Metis_prover.Term.Set.elt Elt3
type:Metis_prover.Term.Set.t T14
type:Metis_prover.Term.const Const
type:Metis_prover.Term.functionName FunctionName
type:Metis_prover.Term.function_t FunctionT
type:Metis_prover.Term.path Path
type:Metis_prover.Term.term Term
type:Metis_prover.Term.var Var
type:Metis_prover.Term_net.net Net
type:Metis_prover.Term_net.parameters Parameters1
type:Metis_prover.Term_net.qterm Qterm
type:Metis_prover.Term_net.termNet TermNet
type:Metis_prover.Thm.clause Clause
type:Metis_prover.Thm.inference Inference
type:Metis_prover.Thm.inferenceType InferenceType
type:Metis_prover.Thm.thm Thm
type:Metis_prover.Units.unitThm UnitThm
type:Metis_prover.Units.units Units
type:Metis_prover.Waiting.distance Distance
type:Metis_prover.Waiting.modelClause ModelClause
type:Metis_prover.Waiting.modelParameters ModelParameters
type:Metis_prover.Waiting.parameters Parameters6
type:Metis_prover.Waiting.waiting Waiting
type:Metis_prover.Waiting.waiting_t WaitingT
type:Metis_prover.Waiting.weight Weight1
type:Metis_prover.Word.word Word
type:Model.element Element
type:Model.fixed Fixed
type:Model.fixedFunction FixedFunction
type:Model.fixedMap FixedMap
type:Model.fixedRelation FixedRelation
type:Model.model Model
type:Model.modelTerm ModelTerm
type:Model.parameters Parameters
type:Model.perturbation Perturbation
type:Model.size Size
type:Model.table Table
type:Model.tables Tables
type:Model.valuation Valuation
type:Name.Map.Ma.key Key2
type:Name.Map.Ma.t T7
type:Name.Map.map Map4
type:Name.Ordered.t T6
type:Name.Set.Se.elt Elt1
type:Name.Set.Se.t T8
type:Name.Set.set Set2
type:Name.name Name
type:Name_arity.Map.Ma.key Key3
type:Name_arity.Map.Ma.t T10
type:Name_arity.Map.map Map5
type:Name_arity.Ordered.t T9
type:Name_arity.Set.Se.elt Elt2
type:Name_arity.Set.Se.t T11
type:Name_arity.Set.set Set3
type:Name_arity.nameArity NameArity
type:Ordered.t T21
type:Pmap.iterator Iterator
type:Pmap.map Map
type:Pmap.node Node
type:Pmap.priority Priority
type:Pmap.tree Tree
type:Proof.inference Inference1
type:Proof.proof Proof
type:Pset.iterator Iterator1
type:Pset.map Map1
type:Pset.set Set
type:Resolution.decision Decision
type:Resolution.parameters Parameters7
type:Resolution.resolution Resolution
type:Resolution.resolution_t ResolutionT
type:Resolution.state State
type:Rewrite.equation Equation1
type:Rewrite.equationId EquationId
type:Rewrite.neqConvs NeqConvs
type:Rewrite.orient Orient
type:Rewrite.reductionOrder ReductionOrder
type:Rewrite.rewrite Rewrite
type:Rewrite.rewrite_t RewriteT
type:Rule.conv Conv
type:Rule.edge Edge
type:Rule.equation Equation
type:Rule.joinStatus JoinStatus
type:Rule.literule Literule
type:Rule.rule Rule
type:Se.elt Elt7
type:Se.t T26
type:Set.Se.elt Elt6
type:Set.Se.t T23
type:Set.elt Elt3
type:Set.set Set6
type:Set.t T14
type:Set_map.Ma.key Key8
type:Set_map.Ma.t T25
type:Set_map.map Map9
type:Set_ordered.t T24
type:Set_set.Se.elt Elt7
type:Set_set.Se.t T26
type:Set_set.set Set7
type:Stringmap.Ma.key Key1
type:Stringmap.Ma.t T3
type:Stringmap.Ordered.t T2
type:Stringmap.map Map3
type:Substitute.subst Subst
type:Subsume.clauseId ClauseId
type:Subsume.clauseLength ClauseLength
type:Subsume.idSet IdSet
type:Subsume.nonunit_t NonunitT
type:Subsume.subsume Subsume
type:Term.Map.key Key4
type:Term.Map.t T13
type:Term.Ordered.t T12
type:Term.Set.elt Elt3
type:Term.Set.t T14
type:Term.const Const
type:Term.functionName FunctionName
type:Term.function_t FunctionT
type:Term.path Path
type:Term.term Term
type:Term.var Var
type:Term_net.net Net
type:Term_net.parameters Parameters1
type:Term_net.qterm Qterm
type:Term_net.termNet TermNet
type:Thm.clause Clause
type:Thm.inference Inference
type:Thm.inferenceType InferenceType
type:Thm.thm Thm
type:Units.unitThm UnitThm
type:Units.units Units
type:Waiting.distance Distance
type:Waiting.modelClause ModelClause
type:Waiting.modelParameters ModelParameters
type:Waiting.parameters Parameters6
type:Waiting.waiting Waiting
type:Waiting.waiting_t WaitingT
type:Waiting.weight Weight1
type:Word.word Word
