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
|
(HANOI::PLAY-HANOI)
(HANOI::H)
(HANOI::HANOI)
(HANOI::TOWER)
(HANOI::INIT-STATE)
(HANOI::FINAL-STATE)
(HANOI::EXAMPLES)
(HANOI::BIG-TOPS)
(HANOI::INDUCTION-HINT)
(HANOI::PLAY-APP
(18 17 (:REWRITE DEFAULT-CAR))
(16 15 (:REWRITE DEFAULT-CDR))
(15 15 (:REWRITE S-DIFF-S))
(9 9 (:TYPE-PRESCRIPTION HANOI::APP))
(2 2 (:REWRITE G-DIFF-S))
)
(HANOI::APP2-LIST
(15 11 (:REWRITE DEFAULT-CAR))
(13 9 (:REWRITE DEFAULT-CDR))
)
(HANOI::POP-PUSH)
(HANOI::TOP-PUSH)
(HANOI::S-FROM-G-FROM-NO-CHANGE)
(HANOI::H-LEMMA
(1116 372 (:REWRITE FOLD-CONSTS-IN-+))
(1109 1109 (:REWRITE DEFAULT-+-2))
(1109 1109 (:REWRITE DEFAULT-+-1))
(1084 1084 (:TYPE-PRESCRIPTION HANOI::PUSH))
(981 246 (:REWRITE ZP-OPEN))
(696 696 (:TYPE-PRESCRIPTION HANOI::TOWER))
(686 658 (:REWRITE DEFAULT-CDR))
(686 658 (:REWRITE DEFAULT-CAR))
(584 348 (:TYPE-PRESCRIPTION HANOI::APP))
(381 319 (:REWRITE DEFAULT-<-2))
(319 319 (:REWRITE DEFAULT-<-1))
(62 62 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
)
(HANOI::APP-NIL
(5 5 (:REWRITE DEFAULT-CDR))
(3 3 (:REWRITE DEFAULT-CAR))
)
(HANOI::TRUE-LISTP-TOWER-N
(36 29 (:REWRITE DEFAULT-CDR))
(29 17 (:REWRITE ZP-OPEN))
(16 16 (:REWRITE DEFAULT-+-2))
(16 16 (:REWRITE DEFAULT-+-1))
(15 15 (:REWRITE DEFAULT-CAR))
(12 4 (:REWRITE FOLD-CONSTS-IN-+))
(6 6 (:REWRITE DEFAULT-<-2))
(6 6 (:REWRITE DEFAULT-<-1))
)
(HANOI::HANOI-CORRECT
(30 6 (:DEFINITION HANOI::APP))
(8 8 (:TYPE-PRESCRIPTION HANOI::PUSH))
(8 8 (:REWRITE DEFAULT-CDR))
(8 8 (:REWRITE DEFAULT-CAR))
(8 8 (:REWRITE DEFAULT-+-2))
(8 8 (:REWRITE DEFAULT-+-1))
(6 6 (:REWRITE ZP-OPEN))
(4 4 (:REWRITE S-DIFF-S))
(1 1 (:REWRITE DEFAULT-<-2))
(1 1 (:REWRITE DEFAULT-<-1))
)
|
