 |
|
|
|
.. (parent) |
 |
- |
rw-r--r-- |
1,458 |
acl2-customization.lsp
|
|
- |
rw-r--r-- |
4,155 |
appeal-identity.lisp
|
|
- |
rw-r--r-- |
12,101 |
arities-okp.lisp
|
|
- |
rw-r--r-- |
4,183 |
base-evaluator.lisp
|
|
- |
rw-r--r-- |
14 |
cert.image
|
|
- |
rw-r--r-- |
5,437 |
disjoin-formulas.lisp
|
|
- |
rw-r--r-- |
2,389 |
find-proof.lisp
|
|
- |
rw-r--r-- |
3,736 |
formula-size.lisp
|
|
- |
rw-r--r-- |
3,147 |
formulas-1.lisp
|
|
- |
rw-r--r-- |
4,479 |
formulas-2-atblp.lisp
|
|
- |
rw-r--r-- |
5,955 |
formulas-2-basic.lisp
|
|
- |
rw-r--r-- |
3,469 |
formulas-2-basic2.lisp
|
|
- |
rw-r--r-- |
2,247 |
formulas-2-equal.lisp
|
|
- |
rw-r--r-- |
1,884 |
formulas-2-list.lisp
|
|
- |
rw-r--r-- |
3,959 |
formulas-2.lisp
|
|
- |
rw-r--r-- |
1,873 |
formulas-3-list-atblp.lisp
|
|
- |
rw-r--r-- |
1,631 |
formulas.lisp
|
|
- |
rw-r--r-- |
3,574 |
fterm-lists.lisp
|
|
- |
rw-r--r-- |
4,686 |
functional-axiom.lisp
|
|
- |
rw-r--r-- |
4,632 |
groundp.lisp
|
|
- |
rw-r--r-- |
196 |
make-image.lsp
|
|
- |
rw-r--r-- |
5,367 |
negate-formulas.lisp
|
|
- |
rw-r--r-- |
2,215 |
negate-term.lisp
|
|
- |
rw-r--r-- |
13,148 |
patmatch-term.lisp
|
|
- |
rw-r--r-- |
4,074 |
pequal-list-1.lisp
|
|
- |
rw-r--r-- |
2,389 |
pequal-list-2-basic.lisp
|
|
- |
rw-r--r-- |
1,897 |
pequal-list-2-lhses.lisp
|
|
- |
rw-r--r-- |
1,962 |
pequal-list-2-rhses.lisp
|
|
- |
rw-r--r-- |
2,567 |
pequal-list.lisp
|
|
- |
rw-r--r-- |
5,666 |
por-list.lisp
|
|
- |
rw-r--r-- |
6,263 |
proofp-1.lisp
|
|
- |
rw-r--r-- |
5,118 |
proofp-2-induction.lisp
|
|
- |
rw-r--r-- |
2,577 |
proofp-2-strip-conclusions.lisp
|
|
- |
rw-r--r-- |
12,768 |
proofp-2.lisp
|
|
- |
rw-r--r-- |
5,478 |
proofp-3-provablep.lisp
|
|
- |
rw-r--r-- |
19,611 |
proofp-3-subproofs.lisp
|
|
- |
rw-r--r-- |
3,308 |
proofp.lisp
|
|
- |
rw-r--r-- |
2,602 |
quote-range.lisp
|
|
- |
rw-r--r-- |
5,410 |
replace-subterm.lisp
|
|
- |
rw-r--r-- |
3,083 |
substitute-formula-1.lisp
|
|
- |
rw-r--r-- |
1,854 |
substitute-formula-2-each.lisp
|
|
- |
rw-r--r-- |
1,833 |
substitute-formula-2-list.lisp
|
|
- |
rw-r--r-- |
4,018 |
substitute-formula.lisp
|
|
- |
rw-r--r-- |
6,910 |
substitute-term-1-sigma-atblp.lisp
|
|
- |
rw-r--r-- |
2,165 |
substitute-term-1-sigmap.lisp
|
|
- |
rw-r--r-- |
4,317 |
substitute-term-1-substitute.lisp
|
|
- |
rw-r--r-- |
1,811 |
substitute-term-1.lisp
|
|
- |
rw-r--r-- |
2,036 |
substitute-term-2-all-bound.lisp
|
|
- |
rw-r--r-- |
1,931 |
substitute-term-2-empty-sigma.lisp
|
|
- |
rw-r--r-- |
1,692 |
substitute-term-2-list-list.lisp
|
|
- |
rw-r--r-- |
2,150 |
substitute-term-2-pair-lists.lisp
|
|
- |
rw-r--r-- |
1,874 |
substitute-term-2-submapp.lisp
|
|
- |
rw-r--r-- |
2,269 |
substitute-term-2-term-atblp.lisp
|
|
- |
rw-r--r-- |
2,070 |
substitute-term-2-termp.lisp
|
|
- |
rw-r--r-- |
1,803 |
substitute-term.lisp
|
|
- |
rw-r--r-- |
6,929 |
subtermp.lisp
|
|
- |
rwxr-xr-x |
52 |
symmetry
|
|
- |
rw-r--r-- |
3,867 |
term-formula.lisp
|
|
- |
rw-r--r-- |
8,946 |
term-order-consts.lisp
|
|
- |
rw-r--r-- |
6,356 |
term-order-fns.lisp
|
|
- |
rw-r--r-- |
6,172 |
term-order-vars.lisp
|
|
- |
rw-r--r-- |
7,279 |
term-order.lisp
|
|
- |
rw-r--r-- |
3,138 |
terms-1.lisp
|
|
- |
rw-r--r-- |
1,633 |
terms-2-constant-listp.lisp
|
|
- |
rw-r--r-- |
1,514 |
terms-2-function-symbol-listp.lisp
|
|
- |
rw-r--r-- |
1,516 |
terms-2-none-constantp.lisp
|
|
- |
rw-r--r-- |
3,874 |
terms-2-term-vars.lisp
|
|
- |
rw-r--r-- |
4,294 |
terms-2-termp.lisp
|
|
- |
rw-r--r-- |
1,568 |
terms-2-unquote-list.lisp
|
|
- |
rw-r--r-- |
1,672 |
terms-2-variable-listp.lisp
|
|
- |
rw-r--r-- |
1,948 |
terms-2.lisp
|
|
- |
rw-r--r-- |
3,530 |
terms-3-arity-tablep.lisp
|
|
- |
rw-r--r-- |
6,760 |
terms-3-functionp.lisp
|
|
- |
rw-r--r-- |
7,409 |
terms-3-lambdap.lisp
|
|
- |
rw-r--r-- |
2,086 |
terms-3-term-list-listp.lisp
|
|
- |
rw-r--r-- |
2,929 |
terms-3-term-vars.lisp
|
|
- |
rw-r--r-- |
5,364 |
terms-3.lisp
|
|
- |
rw-r--r-- |
6,524 |
terms.lisp
|
|
- |
rw-r--r-- |
5,552 |
top.lisp
|
