Index

_

__contains__() (kdrag.rewrite.Order class method) __getitem__() (kdrag.rewrite.Order class method)

__iter__() (kdrag.rewrite.Order class method) __len__() (kdrag.rewrite.Order class method)

A

a (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) abstract_arith() (in module kdrag.theories.real), [1] accessor_lemmas() (in module kdrag.datatype), [1] accessor_num() (in module kdrag.datatype), [1] add (in module kdrag.notation) add() (kdrag.solvers.BaseSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.SATSolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) add_note() (kdrag.kernel.LemmaError method) (kdrag.rewrite.RewriteRuleException method) admit (kdrag.kernel.Proof attribute) (kdrag.Proof attribute) admit() (kdrag.Lemma method) (kdrag.tactics.Lemma method) alpha_eq() (in module kdrag.utils), [1]

and_ (in module kdrag.notation) apply() (in module kdrag.rewrite), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) arb_bnd() (in module kdrag.theories.real.arb), [1] arb_ge() (in module kdrag.theories.real.arb), [1] arb_gt() (in module kdrag.theories.real.arb), [1] arb_le_ax() (in module kdrag.theories.real.arb), [1] arb_lt_ax() (in module kdrag.theories.real.arb), [1] arb_over_of_mid_rad() (in module kdrag.theories.real.arb), [1] args (kdrag.kernel.Defn attribute) (kdrag.kernel.LemmaError attribute) (kdrag.rewrite.RewriteRuleException attribute) assert_and_track() (kdrag.solvers.BaseSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) assert_eq() (kdrag.property.TypeClass method) assumption() (kdrag.Lemma method) (kdrag.tactics.Lemma method) ast_size_sexpr() (in module kdrag.utils), [1] auto() (kdrag.Lemma method) (kdrag.tactics.Lemma method) ax (kdrag.kernel.Defn attribute) axiom() (in module kdrag) (in module kdrag.kernel), [1]

B

b (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) backward_rule() (in module kdrag.rewrite), [1] BaseSolver (class in kdrag.solvers) beta() (in module kdrag.rewrite), [1]

beta_conv() (in module kdrag.kernel), [1] BigUnion() (in module kdrag.theories.set), [1] binop() (in module kdrag.hypothesis), [1] binops() (in module kdrag.hypothesis), [1] binpath() (in module kdrag.solvers), [1] BitVecN (in module kdrag.theories.bitvec) BitVecNConst() (in module kdrag.theories.bitvec), [1] BitVecNVal() (in module kdrag.theories.bitvec), [1] BitVecSort() (in module kdrag.theories.bitvec), [1] body (kdrag.kernel.Defn attribute) bound() (kdrag.solvers.gappa.GappaSolver method) bound_ax() (in module kdrag.theories.real.arb), [1] bounds() (in module kdrag.theories.real.arb), [1] BVNot() (in module kdrag.theories.bitvec), [1]

C

c (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) Calc (class in kdrag) (class in kdrag.tactics) cases() (kdrag.Lemma method) (kdrag.tactics.Lemma method) check() (kdrag.solvers.BaseSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.SATSolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) check_tptp_status() (kdrag.solvers.BaseSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method)

clear() (kdrag.Lemma method) (kdrag.tactics.Lemma method) collect_decls() (in module kdrag.solvers), [1] collect_sorts() (in module kdrag.solvers), [1] compares() (in module kdrag.hypothesis), [1] complement() (in module kdrag.theories.set), [1] conc (kdrag.rewrite.Rule attribute) Cond (class in kdrag.notation) cond() (in module kdrag) (in module kdrag.notation), [1] conde() (in module kdrag.notation), [1] Cons() (in module kdrag.theories.list), [1] consider() (in module kdrag.kernel), [1] constructor_num() (in module kdrag.datatype), [1] copy() (kdrag.Lemma method) (kdrag.tactics.Lemma method) cos_bnd() (in module kdrag.theories.real.arb), [1] count() (kdrag.rewrite.RewriteRule method) (kdrag.rewrite.Rule method) (kdrag.tactics.Goal method) ctx (kdrag.tactics.Goal attribute)

D

datatype_call() (in module kdrag.datatype), [1] datatype_iter() (in module kdrag.datatype), [1] datatype_len() (in module kdrag.datatype), [1] datatype_match_() (in module kdrag.datatype), [1] datatype_replace() (in module kdrag.datatype), [1] decl_index() (in module kdrag.rewrite), [1] decls() (in module kdrag.utils), [1] def_eq() (in module kdrag.rewrite), [1] default (kdrag.reflect.KnuckleClosure attribute)

define() (in module kdrag) (in module kdrag.kernel), [1] (kdrag.notation.SortDispatch method) define_fix() (in module kdrag.kernel), [1] Defn (class in kdrag.kernel) defns (in module kdrag.kernel) diff() (in module kdrag.theories.real.sympy), [1] (in module kdrag.theories.set), [1] distinct_lemmas() (in module kdrag.datatype), [1] div (in module kdrag.notation)

E

einstan() (in module kdrag.kernel), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) empty() (kdrag.tactics.Goal class method) Enum() (in module kdrag.datatype), [1] EProverTHFSolver (class in kdrag.solvers) eq (in module kdrag.notation) EQ (kdrag.rewrite.Order attribute) Eq() (in module kdrag.smt), [1] eq() (kdrag.Calc method) (kdrag.Lemma method) (kdrag.tactics.Calc method) (kdrag.tactics.Lemma method)

eval_() (in module kdrag.reflect), [1] exists() (kdrag.Lemma method) (kdrag.tactics.Lemma method) ExistsUnique() (in module kdrag.notation), [1] exp_bnd() (in module kdrag.theories.real.arb), [1] expand() (in module kdrag.theories.real.sympy), [1] expr() (kdrag.notation.Cond method) expr_to_smtlib() (in module kdrag.solvers), [1] expr_to_tptp() (in module kdrag.solvers), [1] ext() (kdrag.Lemma method) (kdrag.tactics.Lemma method)

F

factor() (in module kdrag.theories.real.sympy), [1] Finite() (in module kdrag.theories.set), [1] FinSort() (in module kdrag.theories.real.vec), [1] fix() (kdrag.Lemma method) (kdrag.tactics.Lemma method) FixedSort() (in module kdrag.theories.fixed), [1] fixes() (kdrag.Lemma method) (kdrag.tactics.Lemma method) flint_bnd() (in module kdrag.theories.real.arb), [1]

flint_eq_ax_unsafe() (in module kdrag.theories.real.arb), [1] forget() (in module kdrag.kernel), [1] forget2() (in module kdrag.kernel), [1] forward_rule() (in module kdrag.rewrite), [1] free_vars() (in module kdrag.utils), [1] fresh_const() (in module kdrag.kernel), [1] fromBV() (in module kdrag.theories.bitvec), [1] full_simp() (in module kdrag.rewrite), [1] funcdecl_smtlib() (in module kdrag.solvers), [1]

G

gappa_of_bool() (in module kdrag.solvers.gappa), [1] gappa_of_real() (in module kdrag.solvers.gappa), [1] GappaSolver (class in kdrag.solvers.gappa) ge (in module kdrag.notation) ge() (kdrag.Calc method) (kdrag.tactics.Calc method) generalize() (kdrag.Lemma method) (kdrag.tactics.Lemma method) generate() (in module kdrag.utils), [1] GenericProof (class in kdrag.property)

get() (in module kdrag.theories.option), [1] (kdrag.property.GenericProof method) get_registry() (kdrag.property.TypeClass class method) getitem (in module kdrag.notation) globals (kdrag.reflect.KnuckleClosure attribute) Goal (class in kdrag.tactics) goal (kdrag.tactics.Goal attribute) GR (kdrag.rewrite.Order attribute) gt (in module kdrag.notation) gt() (kdrag.Calc method) (kdrag.tactics.Calc method)

H

have() (kdrag.Lemma method) (kdrag.tactics.Lemma method)

herb() (in module kdrag.kernel), [1] hyp (kdrag.rewrite.Rule attribute)

I

idem_simp() (in module kdrag.property), [1] in_range() (in module kdrag.theories.float), [1] index() (kdrag.rewrite.RewriteRule method) (kdrag.rewrite.Rule method) (kdrag.tactics.Goal method) induct (in module kdrag.notation) induct() (in module kdrag.theories.int), [1] (in module kdrag.theories.seq), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) induct_inductive() (in module kdrag.kernel), [1] induct_list() (in module kdrag.theories.seq), [1] induct_nat() (in module kdrag.theories.int), [1] induct_nat_strong() (in module kdrag.theories.int), [1] Inductive() (in module kdrag) (in module kdrag.kernel), [1] InductiveRel() (in module kdrag.datatype), [1] infer_sort() (in module kdrag.reflect), [1] inj_lemmas() (in module kdrag.datatype), [1] Injective() (in module kdrag.theories.set), [1] install_solvers() (in module kdrag.solvers), [1] instan() (in module kdrag.kernel), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method)

instan2() (in module kdrag.kernel), [1] integrate() (in module kdrag.theories.real.sympy), [1] inter() (in module kdrag.theories.set), [1] interp_flint() (in module kdrag.theories.real.arb), [1] intros() (kdrag.Lemma method) (kdrag.tactics.Lemma method) invert (in module kdrag.notation) is_accessor() (in module kdrag.smt), [1] is_constructor() (in module kdrag.smt), [1] is_defined() (in module kdrag.kernel), [1] is_empty() (kdrag.tactics.Goal method) is_finite() (in module kdrag.theories.float), [1] is_if() (in module kdrag.smt), [1] is_option() (in module kdrag.theories.option), [1] is_power() (in module kdrag.smt), [1] is_proof() (in module kdrag.kernel), [1] is_recognizer() (in module kdrag.smt), [1] is_set() (in module kdrag.theories.set), [1] is_subterm() (in module kdrag.utils), [1] is_uninterp() (in module kdrag.smt), [1] is_value() (in module kdrag.utils), [1] IsFinite() (in module kdrag.theories.float), [1]

K

k (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) kbo() (in module kdrag.rewrite), [1] kdify() (in module kdrag.theories.real.sympy), [1] kdrag module kdrag.all module kdrag.config module kdrag.datatype module kdrag.hypothesis module kdrag.kernel module kdrag.notation module kdrag.property module kdrag.reflect module kdrag.rewrite module kdrag.smt module kdrag.solvers module kdrag.solvers.aprove module kdrag.solvers.gappa module kdrag.tactics module kdrag.theories module

kdrag.theories.bitvec module kdrag.theories.bool module kdrag.theories.fixed module kdrag.theories.float module kdrag.theories.fun module kdrag.theories.int module kdrag.theories.list module kdrag.theories.nat module kdrag.theories.option module kdrag.theories.real module kdrag.theories.real.arb module kdrag.theories.real.complex module kdrag.theories.real.extended module kdrag.theories.real.geometry module kdrag.theories.real.interval module kdrag.theories.real.ndarray module kdrag.theories.real.sympy module kdrag.theories.real.vec module kdrag.theories.regex module kdrag.theories.seq module kdrag.theories.set module kdrag.utils module KnuckleClosure (class in kdrag.reflect)

L

lam (kdrag.reflect.KnuckleClosure attribute) le (in module kdrag.notation) le() (kdrag.Calc method) (kdrag.tactics.Calc method) left() (kdrag.Lemma method) (kdrag.tactics.Lemma method) Lemma (class in kdrag) (class in kdrag.tactics) lemma() (kdrag.property.GenericProof method) lemma_db() (in module kdrag.utils), [1] LemmaError

LeoIIISolver (class in kdrag.solvers) lhs (kdrag.rewrite.RewriteRule attribute) limit() (in module kdrag.theories.real.sympy), [1] List() (in module kdrag.theories.list), [1] list() (in module kdrag.theories.list), [1] locals (kdrag.reflect.KnuckleClosure attribute) lookup() (kdrag.property.TypeClass class method) lpo() (in module kdrag.rewrite), [1] lt (in module kdrag.notation) lt() (kdrag.Calc method) (kdrag.tactics.Calc method)

M

m (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) mangle_decl() (in module kdrag.solvers), [1] mangle_decl_smtlib() (in module kdrag.solvers), [1] matmul (in module kdrag.notation) member() (in module kdrag.theories.set), [1] min_float64 (in module kdrag.theories.float) module kdrag kdrag.all kdrag.config kdrag.datatype kdrag.hypothesis kdrag.kernel kdrag.notation kdrag.property kdrag.reflect kdrag.rewrite kdrag.smt kdrag.solvers kdrag.solvers.aprove kdrag.solvers.gappa kdrag.tactics kdrag.theories kdrag.theories.bitvec kdrag.theories.bool kdrag.theories.fixed kdrag.theories.float kdrag.theories.fun kdrag.theories.int kdrag.theories.list kdrag.theories.nat kdrag.theories.option kdrag.theories.real kdrag.theories.real.arb kdrag.theories.real.complex kdrag.theories.real.extended kdrag.theories.real.geometry kdrag.theories.real.interval kdrag.theories.real.ndarray kdrag.theories.real.sympy kdrag.theories.real.vec kdrag.theories.regex kdrag.theories.seq kdrag.theories.set kdrag.utils

mul (in module kdrag.notation) multipattern_match() (in module kdrag.datatype), [1] MultiSolver (class in kdrag.solvers)

N

n (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) name (kdrag.kernel.Defn attribute) namedtuple_of_constructor() (in module kdrag.reflect), [1] NanoCopISolver (class in kdrag.solvers)

nbe() (in module kdrag.reflect), [1] ne (in module kdrag.notation) neg (in module kdrag.notation) newgoal() (kdrag.Lemma method) (kdrag.tactics.Lemma method) NewType() (in module kdrag) (in module kdrag.datatype), [1] NGE (kdrag.rewrite.Order attribute) Nil() (in module kdrag.theories.list), [1] nitpick() (in module kdrag.hypothesis), [1] no_overflow() (in module kdrag.theories.float), [1] None_() (in module kdrag.theories.option), [1] NoOverflow() (in module kdrag.theories.float), [1]

O

occurs() (in module kdrag.utils), [1] open_binder() (in module kdrag.utils), [1] open_binder_unhygienic() (in module kdrag.utils), [1]

Option() (in module kdrag.theories.option), [1] or_ (in module kdrag.notation) Order (class in kdrag.rewrite) otherwise() (kdrag.notation.Cond method)

P

pattern_match() (in module kdrag.datatype), [1] perf_event() (in module kdrag.config), [1] pf (kdrag.rewrite.Rule attribute) pmatch() (in module kdrag.utils), [1] pmatch_rec() (in module kdrag.utils), [1] pop() (kdrag.Lemma method) (kdrag.tactics.Lemma method) PopCount() (in module kdrag.theories.bitvec), [1] predefined (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute) predefined_sorts (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute)

prompt() (in module kdrag.utils), [1] Proof (class in kdrag) (class in kdrag.kernel) proof() (kdrag.solvers.BaseSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) prove() (in module kdrag) (in module kdrag.kernel), [1] (in module kdrag.tactics), [1] prune() (in module kdrag.utils), [1] push() (kdrag.Lemma method) (kdrag.tactics.Lemma method)

Q

qed() (kdrag.Calc method) (kdrag.Lemma method) (kdrag.tactics.Calc method) (kdrag.tactics.Lemma method) QExists() (in module kdrag) (in module kdrag.notation), [1]

QForAll() (in module kdrag) (in module kdrag.notation), [1] quant_kind_eq() (in module kdrag.utils), [1] quantifier_call() (in module kdrag.notation), [1] query() (kdrag.solvers.VampireSolver method)

R

radd (in module kdrag.notation) Range() (in module kdrag.theories.set), [1] reason (kdrag.kernel.Proof attribute) (kdrag.Proof attribute) recognizer_lemmas() (in module kdrag.datatype), [1] reflect() (in module kdrag.reflect), [1] reflect_expr_string() (in module kdrag.reflect), [1] register() (kdrag.notation.SortDispatch method) (kdrag.property.GenericProof method) (kdrag.property.TypeClass class method) reify() (in module kdrag.reflect), [1] rel (in module kdrag.datatype) replace_rational_with_ratval() (in module kdrag.theories.real.sympy), [1] res (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute)

ReSort() (in module kdrag.theories.regex), [1] rewrite() (in module kdrag.rewrite), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) rewrite1() (in module kdrag.rewrite), [1] rewrite1_rule() (in module kdrag.rewrite), [1] rewrite_star() (in module kdrag.rewrite), [1] RewriteRule (class in kdrag.rewrite) RewriteRuleException rhs (kdrag.rewrite.RewriteRule attribute) right() (kdrag.Lemma method) (kdrag.tactics.Lemma method) rlemma() (in module kdrag.theories.real), [1] rmul (in module kdrag.notation) round_up_neg (in module kdrag.theories.float) Rule (class in kdrag.rewrite) rule_of_expr() (in module kdrag.rewrite), [1] rule_of_theorem() (in module kdrag.rewrite), [1] run() (in module kdrag.solvers), [1] run_aprove() (in module kdrag.solvers.aprove), [1] rw() (kdrag.Lemma method) (kdrag.tactics.Lemma method)

S

sanity_check_consistency() (in module kdrag.utils), [1] SATSolver (class in kdrag.solvers) search() (in module kdrag) (in module kdrag.utils), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) search_decl() (in module kdrag.utils), [1] search_expr() (in module kdrag.utils), [1] select64() (in module kdrag.theories.bitvec), [1] SelectConcat() (in module kdrag.theories.bitvec), [1] Seq() (in module kdrag.theories.seq), [1] seq() (in module kdrag.theories.seq), [1] series() (in module kdrag.theories.real.sympy), [1] Set() (in module kdrag.theories.set), [1] set() (kdrag.solvers.BaseSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method) show() (kdrag.Lemma method) (kdrag.tactics.Lemma method) sig (kdrag.tactics.Goal attribute) simp() (in module kdrag) (in module kdrag.rewrite), [1] (in module kdrag.tactics), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method)

simp1() (in module kdrag.rewrite), [1] simp2() (in module kdrag.rewrite), [1] simp_tac() (in module kdrag.tactics), [1] simplify() (in module kdrag.theories.real.sympy), [1] sin_bnd() (in module kdrag.theories.real.arb), [1] sin_lower() (in module kdrag.theories.real), [1] skolem() (in module kdrag.kernel), [1] smt_datatype_val() (in module kdrag.hypothesis), [1] smt_generic_val() (in module kdrag.hypothesis), [1] smt_seq_val() (in module kdrag.hypothesis), [1] smtlib_datatypes() (in module kdrag.solvers), [1] solver_classes (kdrag.solvers.MultiSolver attribute) Some() (in module kdrag.theories.option), [1] sort_occurs() (in module kdrag.hypothesis), [1] sort_of_type() (in module kdrag.reflect), [1] sort_to_tptp() (in module kdrag.solvers), [1] SortDispatch (class in kdrag.notation) sorts() (in module kdrag.utils), [1] split() (kdrag.Lemma method) (kdrag.tactics.Lemma method) sqrt_bnd() (in module kdrag.theories.real), [1] sqrt_lower() (in module kdrag.theories.real), [1] sqrt_upper() (in module kdrag.theories.real), [1] Struct() (in module kdrag) (in module kdrag.datatype), [1] sub (in module kdrag.notation) subset() (in module kdrag.theories.set), [1] subterms() (in module kdrag.utils), [1] summation() (in module kdrag.theories.real.sympy), [1] Surjective() (in module kdrag.theories.set), [1] symm() (kdrag.Lemma method) (kdrag.tactics.Lemma method) sympify() (in module kdrag.theories.real.sympy), [1]

T

tan_bnd() (in module kdrag.theories.real.arb), [1] then() (kdrag.notation.Cond method) thm (kdrag.kernel.Proof attribute) (kdrag.Proof attribute) to_int (in module kdrag.notation) to_real (in module kdrag.notation)

toBV() (in module kdrag.theories.bitvec), [1] top_goal() (kdrag.Lemma method) (kdrag.tactics.Lemma method) translate_tuple_args() (in module kdrag.theories.real.sympy), [1] TweeSolver (class in kdrag.solvers) type_of_sort() (in module kdrag.reflect), [1] TypeClass (class in kdrag.property)

U

unfold() (in module kdrag.rewrite), [1] (kdrag.Lemma method) (kdrag.tactics.Lemma method) unify_db() (in module kdrag.utils), [1] union() (in module kdrag.theories.set), [1] Unit() (in module kdrag.theories.list), [1] (in module kdrag.theories.seq), [1] unsat_core() (kdrag.solvers.BaseSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method)

V

val_of_sort() (in module kdrag.hypothesis), [1] VampireSolver (class in kdrag.solvers) VampireTHFSolver (class in kdrag.solvers)

Vec() (in module kdrag.theories.real.vec), [1] Vec0() (in module kdrag.theories.real.vec), [1] vs (kdrag.rewrite.RewriteRule attribute) (kdrag.rewrite.Rule attribute)

W

wf (in module kdrag.notation) when() (kdrag.notation.Cond method) with_traceback() (kdrag.kernel.LemmaError method) (kdrag.rewrite.RewriteRuleException method) write_smt() (kdrag.solvers.BaseSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method)

write_tptp() (kdrag.solvers.BaseSolver method) (kdrag.solvers.EProverTHFSolver method) (kdrag.solvers.gappa.GappaSolver method) (kdrag.solvers.LeoIIISolver method) (kdrag.solvers.MultiSolver method) (kdrag.solvers.NanoCopISolver method) (kdrag.solvers.TweeSolver method) (kdrag.solvers.VampireSolver method) (kdrag.solvers.VampireTHFSolver method) (kdrag.solvers.ZipperpositionSolver method)

X

x (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute)

Y

y (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute)

Z

z (kdrag.solvers.BaseSolver attribute) (kdrag.solvers.EProverTHFSolver attribute) (kdrag.solvers.gappa.GappaSolver attribute) (kdrag.solvers.LeoIIISolver attribute) (kdrag.solvers.MultiSolver attribute) (kdrag.solvers.NanoCopISolver attribute) (kdrag.solvers.TweeSolver attribute) (kdrag.solvers.VampireSolver attribute) (kdrag.solvers.VampireTHFSolver attribute) (kdrag.solvers.ZipperpositionSolver attribute)

z3_array_val() (in module kdrag.hypothesis), [1] z3_mid_rad_of_arb() (in module kdrag.theories.real.arb), [1] z3_of_exact_arb() (in module kdrag.theories.real.arb), [1] ZipperpositionSolver (class in kdrag.solvers)