-
Notifications
You must be signed in to change notification settings - Fork 0
/
.Induction.aux
146 lines (146 loc) · 4.53 KB
/
.Induction.aux
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
138
139
140
141
142
143
144
145
146
COQAUX1 9d74f2f9ea87736238e239ac3c9a818f /Users/antonio/Desktop/tmp/coc/Induction.v
0 0 VernacProof "tac:no using:no"
893 899 proof_build_time "0.001"
893 899 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
1348 1354 proof_build_time "0.002"
1348 1354 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2648 2652 proof_build_time "0.003"
0 0 plus_n_O "0.003"
2635 2647 context_used ""
2648 2652 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
3215 3219 proof_build_time "0.003"
0 0 minus_n_n "0.003"
3202 3214 context_used ""
3215 3219 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
3649 3653 proof_build_time "0.002"
0 0 mult_n_O "0.002"
3636 3648 context_used ""
3649 3653 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3889 3893 proof_build_time "0.003"
0 0 plus_n_Sm "0.003"
3876 3888 context_used ""
3889 3893 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
4160 4164 proof_build_time "0.003"
0 0 plus_comm "0.003"
4147 4159 context_used ""
4160 4164 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
4397 4401 proof_build_time "0.003"
0 0 plus_assoc "0.003"
4384 4396 context_used ""
4397 4401 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
4917 4921 proof_build_time "0.003"
0 0 double_plus "0.003"
4904 4916 context_used ""
4917 4921 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
5177 5181 proof_build_time "0.003"
0 0 evenb_S "0.003"
5164 5176 context_used ""
5177 5181 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
5835 5839 proof_build_time "0.002"
0 0 mult_0_plus' "0.002"
5822 5834 context_used ""
5835 5839 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
7546 7552 proof_build_time "0.001"
7546 7552 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
8046 8050 proof_build_time "0.002"
0 0 plus_rearrange "0.002"
8033 8045 context_used ""
8046 8050 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
8311 8315 proof_build_time "0.006"
0 0 plus_swap "0.006"
8298 8310 context_used ""
8311 8315 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
8555 8559 proof_build_time "0.005"
0 0 plus_swap' "0.005"
8542 8554 context_used ""
8555 8559 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
8994 8998 proof_build_time "0.004"
0 0 mult_n_Sm "0.004"
8981 8993 context_used ""
8994 8998 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
9265 9269 proof_build_time "0.005"
0 0 mult_comm "0.005"
9252 9264 context_used ""
9265 9269 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
9716 9720 proof_build_time "0.005"
0 0 leb_refl "0.005"
9703 9715 context_used ""
9716 9720 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
9823 9827 proof_build_time "0.001"
0 0 zero_nbeq_S "0.001"
9810 9822 context_used ""
9823 9827 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
10024 10028 proof_build_time "0.003"
0 0 andb_false_r "0.003"
10011 10023 context_used ""
10024 10028 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
10310 10314 proof_build_time "0.004"
0 0 plus_ble_compat_l "0.004"
10297 10309 context_used ""
10310 10314 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
10414 10418 proof_build_time "0.001"
0 0 S_nbeq_0 "0.001"
10401 10413 context_used ""
10414 10418 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
10533 10537 proof_build_time "0.002"
0 0 mult_1_l "0.002"
10520 10532 context_used ""
10533 10537 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
10896 10900 proof_build_time "0.004"
0 0 all3_spec "0.004"
10883 10895 context_used ""
10896 10900 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
11170 11174 proof_build_time "0.006"
0 0 mult_plus_distr_r "0.006"
11157 11169 context_used ""
11170 11174 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
11441 11445 proof_build_time "0.004"
0 0 mult_assoc "0.004"
11428 11440 context_used ""
11441 11445 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
11658 11662 proof_build_time "0.003"
0 0 eqb_refl "0.003"
11645 11657 context_used ""
11658 11662 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
14539 14543 proof_build_time "0.004"
0 0 test_bin_to_nat1 "0.004"
14526 14538 context_used ""
14539 14543 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
14623 14627 proof_build_time "0.001"
0 0 test_bin_to_nat2 "0.001"
14610 14622 context_used ""
14623 14627 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
14712 14716 proof_build_time "0.002"
0 0 test_bin_to_nat3 "0.002"
14699 14711 context_used ""
14712 14716 proof_check_time "0.000"
0 0 vo_compile_time "0.398"