1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
|
; % (time acl2 < script.lisp) > script.log
; or
; ACL2 !>(ld "script.lisp" :ld-pre-eval-print t)
(defpkg "M1"
(set-difference-eq (union-eq *acl2-exports*
*common-lisp-symbols-from-main-lisp-package*)
'(push pop pc program step
nth update-nth nth-update-nth)))
(certify-book "m1" 1)
(u)
(u)
; This is just an illustration of the capability of m1.lisp.
(include-book "m1")
(certify-book "template" 1)
(u)
(certify-book "sum" 1)
(u)
(certify-book "sumsq" 1)
(u)
(certify-book "fact" 1)
(u)
(certify-book "power" 1)
(u)
(certify-book "expt" 1)
(u)
(certify-book "alternating-sum" 1)
(u)
(certify-book "alternating-sum-variant" 1)
(u)
(certify-book "fib" 1)
(u)
(certify-book "lessp" 1)
(u)
(certify-book "even-solution-1" 1)
(u)
(certify-book "even-solution-2" 1)
(u)
(certify-book "sign" 1)
(u)
(certify-book "div" 1)
(u)
(certify-book "bexpt" 1)
(u)
(certify-book "magic" 1)
(u)
(certify-book "funny-fact" 1)
(u)
(certify-book "wormhole-abstraction" 1)
(u)
(u)
; Beginning of Turing Equivalence proofs
; Reduce tmi to tmi3
(include-book "m1")
(certify-book "tmi-reductions" 1)
(u)
(u)
(include-book "m1")
(certify-book "defsys-utilities" 1)
(u)
(u)
(include-book "defsys-utilities")
(certify-book "defsys" 1)
(u)
(u)
; Test defsys
(include-book "defsys")
(certify-book "low-seven" 1)
(u)
(u)
(include-book "tmi-reductions")
(certify-book "implementation" 1)
(u)
(u)
(include-book "m1")
(certify-book "theorems-a-and-b" 1)
(u)
(u)
(include-book "theorems-a-and-b")
(certify-book "find-k!" 1)
(u)
(u)
|
