-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathpm_311.txt
113 lines (106 loc) · 1.88 KB
/
pm_311.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
# PM Chapter 311 proof relations
volume 3
part 6
section A
page 321
Df 311.01
Df 311.02
Thm 311.1
<- 311.02
Thm 311.11
<- 311.02
Thm 311.12
<- 311.1 311.11 308.4
Thm 311.121
<- 311.1 311.11 308.63
Thm 311.13
<- 310.16 311.01
Thm 311.14
<- 311.13 310.17
Thm 311.15
<- 310.13 310.16
Thm 311.2
<- 308.72 304.34 304.401 37.6 306.52 []<->
Thm 311.21
<- 306.52 304.401 40.51 40.61 304.23 []->
page 322
Thm 311.22
<- 304.23 311.2 311.21
Thm 311.23
<- 311.22 310.12
Thm 311.24
<- 304.31 306.52 []->
Thm 311.25
<- 310.12 311.24 311.11 311.12 []->
# new tactic []=
Thm 311.26
<- 311.23 311.11 310.12 311.25 []->
Thm 311.27
<- 311.25 310.12 311.26 211.703 308.32 308.72 306.23 200.5 []->
page 323
# new tactic []=
Thm 311.31
<- 311.13 311.1 311.11 308.411
Thm 311.32
<- 311.31 310.17
Thm 311.33
<- 311.31 310.18
Thm 311.41
<- 311.25 310.16 311.33 310.17 []->
Thm 311.42
<- 311.27 310.16 311.33 []->
# new tactic []=
Thm 311.43
<- 311.11 308.51
Thm 311.44
<- 311.27 311.42 311.43
Thm 311.45
<- 311.25 311.41 311.43
# new tactic Induct
Thm 311.51
<- 38.13 306.52 306.51 305.7 []->
page 324
Thm 311.511
<- 311.51 2.03
Thm 311.52
<- 311.511 311.11 310.11 311.27 []->
Thm 311.53
<- 311.52 311.33
Thm 311.56
<- 311.1 311.43 311.52 311.53
Thm 311.57
<- 311.56 311.1
Thm 311.58
<- 304.3 270.31
Thm 311.6
<- 310.11 308.42 308.72 311.58 []->
Thm 311.61
<- 311.6
Thm 311.62
<- 311.58
Thm 311.621
<- 311.62 308.46 308.42 308.72 310.11 308.43 37.1 310.12 []->
page 325
Thm 311.63
<- 311.58 308.42 308.72
Thm 311.631
<- 311.58 308.72 311.63
Thm 311.632
<- 306.52 311.63 311.58 311.511 308.72 []->
Thm 311.633
<- 308.61 308.4 308.63 311.632 308.72 311.631
page 326
Thm 311.64
<- 311.633 311.621 311.61 311.11 []->
Thm 311.65
<- 311.52 311.64
Thm 311.66
<- 310.11 310.111 311.65 311.32 310.16 310.19 []<->
Thm 311.73
<- 311.65 311.121 311.27 []->
Thm 311.731
<- 311.73
Thm 311.74
<- 311.27 311.1 311.73 2.03 310.1
Thm 311.75
<- 311.74 311.43