-
Notifications
You must be signed in to change notification settings - Fork 0
/
.Semantics.aux
176 lines (176 loc) · 5.82 KB
/
.Semantics.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
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
COQAUX1 3023c0d7c6195672a6ec97774ad8d15e /home/rog0d/Escritorio/compiler_new/Semantics.v
0 0 VernacProof "tac:no using:no"
4114 4118 proof_build_time "0.059"
0 0 cstep_deterministic "0.059"
4108 4113 context_used ""
4114 4118 proof_check_time "0.056"
0 0 VernacProof "tac:no using:no"
5251 5260 proof_build_time "0.000"
0 0 not_goes_wrong "0.000"
5251 5260 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5607 5611 proof_build_time "0.006"
0 0 star_CS_SeqStep "0.006"
5599 5604 context_used ""
5607 5611 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
6694 6698 proof_build_time "0.007"
0 0 ceval_to_csteps "0.007"
6688 6693 context_used ""
6694 6698 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
7658 7662 proof_build_time "0.043"
0 0 cstep_append_ceval "0.043"
7634 7657 context_used ""
7658 7662 proof_check_time "0.013"
0 0 VernacProof "tac:no using:no"
7987 7991 proof_build_time "0.005"
0 0 csteps_to_ceval "0.005"
7943 7986 context_used ""
7987 7991 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
10896 10900 proof_build_time "0.001"
0 0 while_true_skip_diverges "0.001"
10880 10895 context_used ""
10896 10900 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
11244 11253 proof_build_time "0.000"
0 0 while_true_skip_diverges_wrong_proof "0.000"
11244 11253 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
11635 11644 proof_build_time "0.000"
0 0 counting_program_diverges "0.000"
11635 11644 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
13262 13266 proof_build_time "0.032"
0 0 cevalinf_can_progress "0.032"
13229 13261 context_used ""
13262 13266 proof_check_time "0.011"
0 0 VernacProof "tac:no using:no"
13673 13677 proof_build_time "0.001"
0 0 cevalinf_diverges "0.001"
13667 13672 context_used ""
13673 13677 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
14094 14098 proof_build_time "0.002"
0 0 diverges_skip_impossible "0.002"
14079 14092 context_used ""
14094 14098 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
14286 14290 proof_build_time "0.006"
0 0 diverges_assign_impossible "0.006"
14272 14285 context_used ""
14286 14290 proof_check_time "0.004"
0 0 VernacProof "tac:no using:no"
15279 15283 proof_build_time "0.021"
0 0 diverges_seq_inversion "0.021"
15254 15278 context_used ""
15279 15283 proof_check_time "0.006"
0 0 VernacProof "tac:no using:no"
15512 15516 proof_build_time "0.008"
0 0 diverges_ifthenelse_inversion "0.008"
15498 15511 context_used ""
15512 15516 proof_check_time "0.004"
0 0 VernacProof "tac:no using:no"
15900 15904 proof_build_time "0.016"
0 0 diverges_while_inversion "0.016"
15862 15899 context_used ""
15900 15904 proof_check_time "0.009"
0 0 VernacProof "tac:no using:no"
16789 16793 proof_build_time "0.007"
0 0 diverges_to_cevalinf "0.007"
16767 16788 context_used ""
16789 16793 proof_check_time "0.003"
0 0 VernacProof "tac:no using:no"
18287 18296 proof_build_time "0.000"
0 0 ceval_step__ceval "0.000"
18287 18296 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
18419 18428 proof_build_time "0.000"
0 0 ceval__ceval_step "0.000"
18419 18428 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
19032 19036 proof_build_time "0.007"
0 0 ceval__ceval_step_either "0.007"
19020 19031 context_used ""
19032 19036 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
19858 19862 proof_build_time "0.015"
0 0 cevalinf__ceval_step_bottom "0.015"
19841 19857 context_used ""
19858 19862 proof_check_time "0.005"
0 0 VernacProof "tac:no using:no"
20674 20678 proof_build_time "0.005"
0 0 ceval_step_limit "0.005"
20662 20673 context_used ""
20674 20678 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
23025 23029 proof_build_time "0.024"
0 0 ceval_step_bottom__cevalinf "0.024"
23013 23024 context_used ""
23025 23029 proof_check_time "0.022"
0 0 VernacProof "tac:no using:no"
24069 24073 proof_build_time "0.002"
0 0 interp_limit_dep "0.002"
24053 24068 context_used ""
24069 24073 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
24315 24319 proof_build_time "0.000"
0 0 denot_limit "0.000"
24298 24314 context_used ""
24315 24319 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
24659 24663 proof_build_time "0.001"
0 0 denot_charact "0.001"
24647 24658 context_used ""
24659 24663 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
24856 24860 proof_build_time "0.001"
0 0 denot_terminates "0.001"
24820 24855 context_used ""
24856 24860 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
25105 25109 proof_build_time "0.001"
0 0 denot_skip "0.001"
25099 25104 context_used ""
25105 25109 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
25263 25267 proof_build_time "0.001"
0 0 denot_assign "0.001"
25257 25262 context_used ""
25263 25267 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
25937 25941 proof_build_time "0.009"
0 0 denot_seq "0.009"
25932 25936 context_used ""
25937 25941 proof_check_time "0.006"
0 0 VernacProof "tac:no using:no"
26500 26504 proof_build_time "0.007"
0 0 denot_ifthenelse "0.007"
26495 26499 context_used ""
26500 26504 proof_check_time "0.004"
0 0 VernacProof "tac:no using:no"
27426 27430 proof_build_time "0.013"
0 0 denot_while "0.013"
27420 27425 context_used ""
27426 27430 proof_check_time "0.007"
0 0 VernacProof "tac:no using:no"
28326 28330 proof_build_time "0.006"
0 0 denot_while_least_fixpoint "0.006"
28321 28325 context_used ""
28326 28330 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
28636 28645 proof_build_time "0.000"
0 0 denot_while_compositional "0.000"
28636 28645 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
29139 29143 proof_build_time "0.041"
0 0 denot_ceval "0.041"
29134 29138 context_used ""
29139 29143 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
29486 29490 proof_build_time "0.002"
0 0 denot_cevalinf "0.002"
29467 29485 context_used ""
29486 29490 proof_check_time "0.000"
0 0 vo_compile_time "0.750"