blob: 78e448865f5151fd896647beb630abf3145d8fba (
plain)
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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
|
#FIG 3.2
Landscape
Center
Inches
Letter
100.00
Single
-2
1200 2
5 1 0 1 0 7 50 -1 -1 0.000 0 1 1 0 14032.500 7222.500 4725 3825 4425 4800 4200 6000
1 1 1.00 60.00 120.00
5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 8925.000 3600 9075 3450 8925 3600 8775
1 1 1.00 60.00 120.00
5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 8625.000 3600 8775 3450 8625 3600 8475
1 1 1.00 60.00 120.00
5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 8325.000 3600 8475 3450 8325 3600 8175
1 1 1.00 60.00 120.00
1 1 1.00 60.00 120.00
5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 8625.000 3600 8775 3450 8625 3600 8475
1 1 1.00 60.00 120.00
1 1 1.00 60.00 120.00
5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 8925.000 3600 9075 3450 8925 3600 8775
1 1 1.00 60.00 120.00
1 1 1.00 60.00 120.00
5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 9225.000 3600 9375 3450 9225 3600 9075
1 1 1.00 60.00 120.00
1 1 1.00 60.00 120.00
5 1 0 1 0 7 50 -1 -1 0.000 0 1 1 0 6309.515 5767.724 4200 3825 3450 5550 3825 7200
1 1 1.00 60.00 120.00
6 2025 300 7725 525
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
7725 525 2025 525
4 0 0 50 -1 0 12 0.0000 4 180 5700 2025 450 The dependency graph of axioms in the Calculus of Inductive Constructions\001
-6
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
4200 6225 4200 7200
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
7725 3900 7200 6000
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
7200 6225 7200 7050
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
1 1 1.00 60.00 120.00
1 1 1.00 60.00 120.00
5550 5625 5550 6000
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
4575 6000 6450 6000
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
1 1 1.00 60.00 120.00
1 1 1.00 60.00 120.00
3375 3225 3375 3600
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
3373 1950 3376 2250
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
1 1 1.00 60.00 120.00
1 1 1.00 60.00 120.00
3375 2625 3375 3000
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
2175 3600 3750 3600
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
3075 2475 2475 2475
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
3374 1125 3377 1425
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
1049 1950 1052 2250
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
1048 1125 1051 1425
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
3075 975 1575 975
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
3075 1725 2025 1725
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 4
8025 5925 8250 5925 9000 4950 9150 4950
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
8625 5400 8250 3900
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
7050 7350 4575 7950
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
4200 7500 4200 7950
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
4714 6255 7039 7080
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
1 1 1.00 60.00 120.00
1500 3900 2175 6000
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
1 1 1.00 60.00 120.00
1 1 1.00 60.00 120.00
1139 2771 1364 3521
2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
4425 4875 7350 3825
3 0 0 1 0 7 50 -1 -1 0.000 0 0 0 4
6450 7050 4050 6675 3750 6825 3750 7050
0.000 1.000 1.000 0.000
4 0 0 50 -1 0 12 0.0000 4 180 1830 6900 3750 Predicate extensionality\001
4 0 0 50 -1 0 12 0.0000 4 135 1800 3825 3750 Relational choice axiom\001
4 0 0 50 -1 0 12 0.0000 4 180 2100 6150 6150 Propositional extensionality\001
4 0 0 50 -1 0 12 0.0000 4 180 1005 450 1050 Operator iota\001
4 0 0 50 -1 2 12 0.0000 4 135 1020 450 1650 Constructive\001
4 0 0 50 -1 2 12 0.0000 4 180 1530 450 1875 definite description\001
4 0 0 50 -1 2 12 0.0000 4 180 2010 9000 5175 Functional extensionality\001
4 0 0 50 -1 0 12 0.0000 4 180 4740 150 10050 Statements in boldface are the most "interesting" ones for Coq\001
4 0 0 50 -1 0 12 0.0000 4 180 4800 3600 9375 Invariance by substitution of reflexivity proofs for equality on A\001
4 0 0 50 -1 0 12 0.0000 4 180 3735 3600 8475 Uniqueness of reflexivity proofs for equality on A\001
4 0 0 50 -1 0 12 0.0000 4 180 2670 3600 8775 Uniqueness of equality proofs on A\001
4 0 0 50 -1 0 12 0.0000 4 135 1080 3600 8175 Axiom K on A\001
4 0 0 50 -1 2 12 0.0000 4 135 1455 6450 7275 Proof-irrelevance\001
4 0 0 50 -1 2 12 0.0000 4 180 3360 3600 9075 Injectivity of equality on Sigma-types on A\001
4 0 0 50 -1 0 12 0.0000 4 180 2175 4950 6525 (needs Prop-impredicativity)\001
4 0 0 50 -1 0 12 0.0000 4 180 705 6000 6750 (Berardi)\001
4 0 0 50 -1 2 12 0.0000 4 135 1290 3675 6225 Excluded-middle\001
4 0 0 50 -1 0 12 0.0000 4 180 1905 4950 5550 Propositional degeneracy\001
4 0 0 50 -1 0 12 0.0000 4 180 1050 3750 5250 (Diaconescu)\001
4 0 0 50 -1 0 12 0.0000 4 180 2475 3375 7425 Decidability of equality on any A\001
4 0 0 50 -1 0 12 0.0000 4 180 1620 1275 5025 (if Set impredicative)\001
4 0 0 50 -1 0 12 0.0000 4 135 1560 1575 6225 Not excluded-middle\001
4 0 0 50 -1 0 12 0.0000 4 180 1770 450 2625 in propositional context\001
4 0 0 50 -1 2 12 0.0000 4 135 1020 3150 1650 Constructive\001
4 0 0 50 -1 2 12 0.0000 4 180 1665 3150 1875 indefinite description\001
4 0 0 50 -1 0 12 0.0000 4 180 2610 3150 2400 Constructive indefinite description\001
4 0 0 50 -1 0 12 0.0000 4 180 1770 3150 2625 in propositional context\001
4 0 0 50 -1 2 12 0.0000 4 135 1935 3150 3150 Functional choice axiom\001
4 0 0 50 -1 0 12 0.0000 4 135 2100 450 2400 Constructive definite descr.\001
4 0 0 50 -1 2 12 0.0000 4 180 1845 450 3750 Axiom of unique choice\001
4 0 0 50 -1 2 12 0.0000 4 180 1365 3150 1050 Operator epsilon\001
|
