-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathpm_333.txt
92 lines (85 loc) · 1.66 KB
/
pm_333.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
# PM Chapter 333 proof relations
volume 3
part 6
section B
page 377
Df 333.01
Df 333.011
Df 333.02
Df 333.03
page 378
Thm 333.1
<- 333.01 333.011
Thm 333.101
<- 333.02
Thm 333.11
<- 333.1 333.101
Thm 333.12
<- 332.11 332.22 333.1 333.101 []->
Thm 333.13
<- 332.11 332.22 333.1 333.101 []->
Thm 333.14
<- 330.626 332.31 330.6 332.46 2.03 333.13
Thm 333.15
<- 121.501 333.11 333.101
Thm 333.16
<- 121.501 33.14
Thm 333.17
<- 121.501 333.13
Thm 333.18
<- 333.101 300.3
Thm 333.19
<- 333.18 330.624 300.491
Thm 333.2
<- 333.19 331.12
page 379
Thm 333.21
<- 332.61 333.101 330.624 332.11 333.1 []->
Thm 333.22
<- 332.71 332.46 332.11 332.232 332.31 333.21
Thm 333.23
<- 332.62 332.11 332.22 333.1 333.21
# new tactic Induct
# new tactic []=
Thm 333.24
<- 301.2 332.243 332.63 330.6 301.16 301.22 301.21 332.33 330.624 301.21 332.33 []->
Thm 333.25
<- 330.626 331.12 332.31 330.6 333.24
page 380
# new tactic Induct
Thm 333.32
<- 330.61 301.2 330.623 330.622 330.621 []->
# new tactic Induct
# new tactic []=
Thm 333.33
<- 333.32 332.243 332.37 301.21 333.32
Thm 333.34
<- 330.626 330.6 332.31 333.24 333.33
Thm 333.41
<- 333.34 333.22 333.2 333.21 333.32 332.33 332.44 2.03 332.15 332.46 []->
Thm 333.42
<- 333.41
page 381
Thm 333.43
<- 333.21 332.26 333.41 330.624 []->
Thm 333.44
<- 301.5 333.24 333.41 333.21 []<->
Thm 333.45
<- 333.44
Thm 333.46
<- 332.36 333.21 333.44
Thm 333.47
<- 333.46 332.53 72.92 35.14 330.72 []->
Thm 333.48
<- 333.46 330.624 332.61 333.24 333.47 333.46 []->
page 382
Thm 333.49
<- 333.21 330.6 332.11 72.92 []->
Thm 333.5
<- 333.42 333.43 331.24
Thm 333.51
<- 333.47 301.23 120.412 120.416 333.101 []->
Thm 333.52
<- 333.51
Thm 333.53
<- 333.48 301.16 333.47 333.51 []->