/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/base/ |
H A D | fp_params.pyg | 127 …('spacer.use_lemma_as_cti', BOOL, False, 'SPACER: use a lemma instead of a CTI in flexible_trace'), 153 ('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'), 164 … ('spacer.validate_lemmas', BOOL, False, 'Validate each lemma after generalization'),
|
/dports/print/lyx/lyx-2.3.4.2/lib/layouts/ |
H A D | theorems-ams-chap-bytype.inc | 32 Counter lemma 149 LabelCounter lemma
|
/dports/math/eprover/eprover-E-2.0/EXAMPLE_PROBLEMS/TPTP/ |
H A D | SET844-1.p | 4 % Problem : Problem about Zorn's lemma
|
/dports/math/cvc4/CVC4-1.7/src/proof/ |
H A D | clausal_bitvector_proof.cpp | 102 void LfscClausalBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, in printTheoryLemmaProof() argument
|
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/tptp/ |
H A D | SYN000+2.p | 68 fof(role_lemma,lemma,(
|
H A D | SYN000-2.p | 58 cnf(role_lemma,lemma,
|
/dports/editors/texmacs/TeXmacs-1.99.4-src/TeXmacs/progs/convert/tools/ |
H A D | tmpre.scm | 34 theorem proposition lemma corollary axiom definition notation conjecture
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
H A D | theory_arith_new.cpp | 4045 Theorem lemma; in propagateTheory() local 4050 lemma = d_rules->implyWeakerInequality(assertExpr, findExpr); in propagateTheory() 4053 lemma = d_rules->implyNegatedInequality(assertExpr, findExpr); in propagateTheory() 4056 TRACE("propagate_arith", "lemma ==>", lemma.toString(), ""); in propagateTheory() 4057 TRACE("arith_atoms", "Propagate: ", lemma.getExpr().toString(), ""); in propagateTheory() 4060 enqueueFact(lemma); in propagateTheory() 4083 Theorem lemma; in propagateTheory() local 4088 lemma = d_rules->implyWeakerInequality(assertExpr, findExpr); in propagateTheory() 4091 lemma = d_rules->implyNegatedInequality(assertExpr, findExpr); in propagateTheory() 4093 TRACE("propagate_arith", "lemma ==>", lemma.toString(), ""); in propagateTheory() [all …]
|
/dports/math/yices/yices-2.6.2/doc/ |
H A D | YICES-LANGUAGE | 814 Yices includes heuristics to build theory lemmas. A theory lemma is 830 (<= n 3) then a valid theory lemma is that (<= n 3) implies (<= n 4). 838 (F x z) then we can add the following lemma 842 This is a known as Ackermann's lemma for the terms (F x y) and (F x z). 848 lemma is written as two clauses: 866 Parameters that control theory lemma generation 894 lemma generation more aggressive. 967 lemma for 'x' and 'y', to force agreement. Semantically, such a 973 Yices will generate the lemma
|
/dports/lang/p5-Marpa-XS/Marpa-XS-1.008000/inc/proof/ |
H A D | proof.lyx | 2232 By assumption in the statement of the lemma. 2273 By assumption in the statement of the lemma. 2442 By assumptions in for the lemma. 2466 From an assumption for this lemma. 2475 An assumption for this lemma. 2494 This proves the lemma. 3503 This proves the lemma. 3737 From an assumption for this lemma. 4248 lemma 4393 This proves the lemma [all …]
|
/dports/lang/p5-Marpa/Marpa-0.208000/inc/proof/ |
H A D | proof.lyx | 2224 By assumption in the statement of the lemma. 2265 By assumption in the statement of the lemma. 2434 By assumptions in for the lemma. 2458 From an assumption for this lemma. 2467 An assumption for this lemma. 2486 This proves the lemma. 3495 This proves the lemma. 3729 From an assumption for this lemma. 4240 lemma 4385 This proves the lemma [all …]
|
/dports/math/hpipm/hpipm-0.1.1/experimental/andrea/notes/ |
H A D | notes.tex | 40 %%\newtheorem{lemma}{Lemma} 41 %\newtheorem{lemma}[theorem]{Lemma}
|
/dports/math/abella/abella-2.0.7/examples/process-calculi/pic_lambda/ |
H A D | picalc_str_eq_is_bisimulation.thm | 7 /*lemma */ 129 /* lemma */
|
/dports/misc/xiphos/xiphos-4.2.1/help/C/ |
H A D | xiphos-31-advanced-search.page | 97 Strong's references. Enter your search preceded by "lemma:", so to search for 98 Strong's Greek #140, enter "lemma:G140". You must have selected <gui>Optimized
|
H A D | xiphos-33-original-language.page | 112 "lemma:" and "G" for Greek or "H" for Hebrew. So to look for the Hebrew word 113 tsad-deek (6662), enter "lemma:H6662". Once the search is done, the results
|
/dports/math/gap/gap-4.11.0/pkg/liepring-1.9.2/lib/dim6/notes/ |
H A D | note5.45.tex | 41 \newtheorem{lemma}[theorem]{Lemma}
|
/dports/math/dune-uggrid/dune-uggrid-bc2d1229420367563410ce9e519f5ff82b45266f/doc/ |
H A D | const.tex | 49 \newtheorem{lemma}{\noindent\bf Lemma}[section]
|
/dports/editors/texmacs/TeXmacs-1.99.4-src/TeXmacs/progs/text/ |
H A D | text-drd.scm | 115 theorem proposition lemma corollary conjecture)
|
/dports/textproc/bat/bat-0.18.3/tests/syntax-tests/source/Lean/ |
H A D | test.lean | 10 lemma split_eq {m n : Type*} (x : m × n) (p p' : m × n) :
|
/dports/lang/guile2/guile-2.2.7/gc-benchmarks/larceny/ |
H A D | sboyer.sch | 96 (add-lemma-lst 467 (define (add-lemma-lst lst) 470 (else (add-lemma (car lst)) 471 (add-lemma-lst (cdr lst))))) 473 (define (add-lemma term)
|
H A D | nboyer.sch | 95 (add-lemma-lst 466 (define (add-lemma-lst lst) 469 (else (add-lemma (car lst)) 470 (add-lemma-lst (cdr lst))))) 472 (define (add-lemma term)
|
/dports/lang/guile/guile-3.0.7/gc-benchmarks/larceny/ |
H A D | sboyer.sch | 96 (add-lemma-lst 467 (define (add-lemma-lst lst) 470 (else (add-lemma (car lst)) 471 (add-lemma-lst (cdr lst))))) 473 (define (add-lemma term)
|
H A D | nboyer.sch | 95 (add-lemma-lst 466 (define (add-lemma-lst lst) 469 (else (add-lemma (car lst)) 470 (add-lemma-lst (cdr lst))))) 472 (define (add-lemma term)
|
/dports/lang/chibi-scheme/chibi-scheme-0.10/benchmarks/gabriel/ |
H A D | nboyer.sch | 81 (add-lemma-lst 452 (define (add-lemma-lst lst) 455 (else (add-lemma (car lst)) 456 (add-lemma-lst (cdr lst))))) 458 (define (add-lemma term)
|
H A D | sboyer.sch | 84 (add-lemma-lst 455 (define (add-lemma-lst lst) 458 (else (add-lemma (car lst)) 459 (add-lemma-lst (cdr lst))))) 461 (define (add-lemma term)
|