-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathpm_314.txt
54 lines (51 loc) · 976 Bytes
/
pm_314.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
# PM Chapter 314 proof relations
volume 3
part 6
section A
page 337
Df 314.01
Df 314.02
Df 314.03
Df 314.04
Df 314.05
Thm 314.1
<- 312.31 314.01
Thm 314.11
<- 314.1 312.34
Thm 314.12
Thm 314.13
<- 314.1 314.01 310.32
Thm 314.14
Thm 314.2
<- 310.31
Thm 314.21
<- 314.13 314.14 312.34 313.44 314.11 314.12
Thm 314.22
<- 314.13 314.14 312.51 313.43 []->
# new tactic []=
Thm 314.23
<- 314.13 43.421 312.52 []->
page 338
Thm 314.24
<- 312.41 314.01
Thm 314.25
<- 313.45 314.02
# new tactic []=
Thm 314.26
<- 314.13 312.48 314.13 314.11 314.21
Thm 314.27
<- 314.14 313.46 314.12 314.21
# new tactic []=
Thm 314.28
<- 314.13 314.14 314.21 313.55 314.11 314.12
Thm 314.4
<- 217.43 304.31 304.282 304.23 307.41 307.44 307.46 307.25 310.01 310.011 310.02 310.03
# NOTE: cannot determine exact proof
Thm 314.41
<- 310.31 303.62 310.12 307.25 310.121 303.52 41.11 310.1 []->
Thm 314.42
<- 314.4 314.41
Thm 314.5
<- 312.34 313.44 314.42 314.04 314.05
Thm 314.51
<- 314.42 314.04 314.05