-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathpm_259.txt
67 lines (61 loc) · 1.18 KB
/
pm_259.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
# PM Chapter 259 proof relations
volume 3
part 5
section D
page 103
# new tactic Dft
Df 259.01
# new tactic Dft
Df 259.02
Df 259.03
# NOTE: "As in 258.14"
Thm 259.1
<- 258.14 201.18 259.02 259.01 258.202 []->
Thm 259.11
<- 258.242 259.1 41.13
page 104
Thm 259.111
<- 259.1 257.36
Thm 259.12
<- 259.02
Thm 259.121
<- 259.12
Thm 259.122
<- 259.11 257.3 259.12 257.121 []->
Thm 259.13
<- 259.122 257.123
Thm 259.14
<- 71.24 259.111 259.11
Thm 259.141
<- 71.24 259.111 259.11
page 105
Thm 259.15
<- 259.14 259.141
Thm 259.16
<- 259.111 150.1 258.242 259.11 []<->
Thm 259.17
<- 250.242 257.35 259.1 259.02 []->
Thm 259.171
<- 250.242 257.35 259.1 259.02 []->
Thm 259.2
<- 72.182 206.2 55.134 259.15
page 106
Thm 259.21
<- 206.133 206.21 37.461 206.18 41.43 258.242 206.132 40.16 40.67 259.111 11.62 10.23
<- 3.43 258.242 259.11 []->
Thm 259.211
<- 206.133 206.21 37.461 206.18 41.43 258.242 206.132 40.16 40.67 259.111 11.62 10.23
<- 3.43 258.242 259.11 []->
Thm 259.22
<- 211.22 211.63 258.242
Thm 259.221
Thm 259.222
<- 259.21 259.22 213.161
Thm 259.223
Thm 259.23
<- 259.2 259.21 259.222 259.223
page 107
Thm 259.24
<- 206.18 259.11 257.36 259.12 252.1 259.22 259.221 []->
Thm 259.25
<- 259.23 259.24