aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2021-08-12 00:10:49 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2021-08-12 00:10:49 +0900
commitc1f965d3ce7fafd01f5dde64e921370d4e0fe16c (patch)
tree7c632e6e3d8e016691858792dce83ec05202c251
parentaf6e2bdb7f770d1d0822b217346d3896ed5afbc1 (diff)
permutations: Refactoring.
-rw-r--r--permutations.lisp2
1 files changed, 0 insertions, 2 deletions
diff --git a/permutations.lisp b/permutations.lisp
index d46c47e..7c01dc3 100644
--- a/permutations.lisp
+++ b/permutations.lisp
@@ -118,7 +118,6 @@
(mapcar-len x))
n))))
-
(defthm nat-listp-mapcar-len
(nat-listp (mapcar-len x)))
@@ -159,7 +158,6 @@
(equal (sum (mapcar-nat-expt (mapcar-len x) n))
(sum-of-nat-expt-lens x n)))
-
(defthm sum-of-nat-expt-1+lens-equal-sum-mapcar-nat-expt-1+-len/inverse
(equal (sum (mapcar-nat-expt (mapcar-sum (seq 1 (len x))
(mapcar-len x))