-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathpm_373.txt
147 lines (138 loc) · 2.4 KB
/
pm_373.txt
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
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
# PM Chapter 373 proof relations
volume 3
part 6
section D
page 477
# new tactic Dft
Df 373.01
Df 373.02
# new tactic Dft
Df 373.03
Thm 373.1
<- 373.01
Thm 373.11
<- 372.29
Thm 373.12
<- 372.121
Thm 373.13
<- 373.12 371.12
# new tactic Induct
Thm 373.14
<- 372.29 351.1
Thm 373.141
<- 373.11 373.13 373.14
Thm 373.1412
<- 373.141
# new tactic Induct
Thm 373.15
<- 373.1 373.14 372.18 371.2 372.13 []->
Thm 373.16
<- 373.1 371.26 373.15 372.2 []->
page 478
Thm 373.17
<- 373.16 373.14 373.03
Thm 373.18
<- 50.5 50.51
Thm 373.19
<- 373.18
Thm 373.2
<- 301.5 373.1
Thm 373.21
<- 373.2 373.19
# NOTE: cannot determine exact proof
Thm 373.22
<- 373.2 373.21
Thm 373.23
<- 370.26
# new tactic Induct
Thm 373.231
Thm 373.24
<- 117.661 116.301 10.24 261.26 263.47 116.52 116.321 373.231 116.52 []->
page 479
Thm 373.25
<- 373.22 373.24 373.23 373.14
Thm 373.3
<- 300.23 301.2 302.25 301.23 301.504 373.03
Thm 373.31
<- 373.3
Thm 373.32
<- 373.31 2.03 373.03
Thm 373.33
<- 373.3
Thm 373.4
<- 373.01
Thm 373.401
<- 373.25
Thm 373.402
<- 373.4
Thm 373.403
<- 373.4
# new tactic Induct
Thm 373.404
<- 373.401 373.402 373.403
# new tactic Induct
Thm 373.405
<- 373.4
page 480
# new tactic Induct
Thm 373.406
<- 373.4
Thm 373.407
<- 373.406
Thm 373.41
<- 373.405 373.407 373.403
Thm 373.42
<- 373.405 300.23 373.33 373.405 373.407 []->
Thm 373.43
<- 373.404 373.405 373.42
Thm 373.44
<- 302.1 303.39 303.341 302.1 113.621 2.03 302.36 303.39 303.341 126.41 302.1 []->
page 481
Thm 373.441
<- 126.41 373.44 302.1 2.03 []->
Thm 373.45
<- 370.33 373.31 373.44 301.504 373.441 373.33 117.62 []->
# new tactic Induct
Thm 373.451
<- 261.26 263.47 373.44 []->
page 482
Thm 373.452
<- 373.451
Thm 373.46
<- 373.43 373.45 373.18 373.452
Thm 373.5
<- 302.25 301.504 120.57 301.23 330.32 2.03 120.57 []->
Thm 373.51
<- 301.504
Thm 373.52
<- 373.33 373.441 301.504 373.51 91.6 120.426 2.03 []->
Thm 373.521
<- 301.2 13.14 301.21
page 483
Thm 373.522
<- 373.521 91.6 91.343 []->
Thm 373.53
<- 371.23 373.522 91.36 2.03
Thm 373.531
<- 373.53
Thm 373.532
<- 373.531 2.03 371.12
Thm 373.533
<- 373.532
Thm 373.54
<- 373.533 2.03 373.3 373.5 261.26 91.6
Thm 373.55
<- 373.3 373.5 373.54 100.34 []->
Thm 373.56
<- 205.21 301.21 371.15 373.55 371.16 301.2 13.14 372.17 []->
page 484
Thm 373.6
<- 373.46 373.56 373.5 261.26 372.11
Thm 373.61
<- 372.28 373.6
Thm 373.62
<- 373.55 373.56 373.61 373.54 372.28 13.12 373.33 372.19 []->
Thm 373.63
<- 373.61 373.62
Thm 373.64
<- 373.63 373.5