-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathpm_304.txt
115 lines (110 loc) · 1.77 KB
/
pm_304.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
# PM Chapter 304 proof relations
volume 3
part 6
section A
page 279
Df 304.01
Df 304.02
Df 304.03
Thm 304.1
<- 304.01
Thm 304.11
<- 304.1
Thm 304.12
<- 304.11 303.13
Thm 304.13
<- 117.5 113.602 304.1 303.7 []->
Thm 304.14
<- 304.02
Thm 304.15
<- 304.14 304.1 303.71
Thm 304.151
<- 304.15
Thm 304.152
<- 304.151 303.731
Thm 304.16
<- 304.15
Thm 304.161
<- 304.12 304.151
Thm 304.2
<- 303.37 304.15 2.03 []->
Thm 304.201
<- 303.37 304.15 2.03 []->
page 280
Thm 304.21
<- 304.15 117.571 120.51 126.51 []->
Thm 304.211
<- 304.15 117.571 120.51 126.51 []->
Thm 304.22
<- 126.33 304.15
Thm 304.221
<- 126.33 304.15
Thm 304.23
<- 304.2 304.21 304.22
Thm 304.24
<- 120.414 120.415 120.416 304.15
Thm 304.241
<- 300.14 120.14 304.15
Thm 304.25
<- 304.24 304.241 304.16
Thm 304.251
<- 300.14 117.571 304.15 []->
Thm 304.26
<- 302.39 304.25 304.251 304.15 304.16
page 281
Thm 304.261
<- 304.25 304.251 304.15
Thm 304.262
<- 304.261 304.16
Thm 304.27
<- 300.14 304.25 304.261 117.32 []->
Thm 304.28
<- 300.14 304.261 304.262 303.71
Thm 304.281
<- 304.28 304.261 304.262
Thm 304.282
<- 304.27 304.28 303.66
Thm 304.29
<- 304.1 126.5 []->
Thm 304.3
<- 304.29 304.23
Thm 304.31
<- 304.281 300.14
# new tactic []<=
# new tactic []>=
Thm 304.32
<- 304.15 303.211 302.22 123.52 300.21 304.28 303.26 300.21
page 282
Thm 304.33
<- 304.3 304.31 304.32 273.1
Thm 304.34
<- 303.78 304.28
Thm 304.4
<- 303.71 304.03
Thm 304.401
<- 304.4 303.78
Thm 304.41
<- 304.25 304.251 304.15
Thm 304.42
Thm 304.43
<- 304.42
Thm 304.44
<- 304.41 304.42
Thm 304.45
<- 304.41 304.42 303.6
Thm 304.46
<- 304.45 304.4 304.27 304.1
Thm 304.47
<- 304.46 304.33
Thm 304.48
<- 304.43 304.46 304.23
Thm 304.49
<- 304.34 304.46
Thm 304.5
<- 303.73 304.14
Thm 304.51
<- 303.63 304.43 303.73 304.4
Thm 304.52
<- 304.44 300.18
Thm 304.53
<- 304.28 300.18