-
Notifications
You must be signed in to change notification settings - Fork 3
Expand file tree
/
Copy pathRULES
More file actions
266 lines (266 loc) · 27.4 KB
/
RULES
File metadata and controls
266 lines (266 loc) · 27.4 KB
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
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
{1,Continuity} continuity/continuity_rule_gen.v : rule_continuity_true3
{2,StrongContinuity2} continuity/stronger_continuity_rule4_v3.v : rule_strong_continuity_true2_v3_2
{1,addAssociative} rules/rules_integer_ring.v : rule_add_associative_true
{1,addCommutative} rules/rules_integer_ring.v : rule_add_commutative_true
{2672,addEquality} rules/rules_arith.v : rule_arithop_equality_true3
{40,addExceptionCases} rules/rules_arith_exception.v : rule_arith_exception_cases_true
{2,addInverse} rules/rules_integer_ring.v : rule_add_inverse_true
{1,addMonotonic} rules/rules_integer_ordered_ring.v : rule_add_monotonic_true
{1,addZero} rules/rules_integer_ring.v : rule_add_zero_true
{9447,applyEquality} rules/rules_function.v : rule_apply_equality_true
{70,applyExceptionCases} rules/rules_apply_callbyvalue.v : rule_isexc_apply_cases_true
{2,applyInl} rules/rules_apply_callbyvalue.v : rule_apply_inl_true
{2,applyInr} rules/rules_apply_callbyvalue.v : rule_apply_inr_true
{1,applyInt} rules/rules_apply_callbyvalue.v : rule_apply_int_true
{3,applyPair} rules/rules_apply_callbyvalue.v : rule_apply_pair_true
{3,atom1_eqExceptionCases} . : .
{3,atom2_eqExceptionCases} . : .
{527,atomEquality} . : .
{3,atom_eqEquality} . : .
{4,atom_eqExceptionCases} . : .
{3,atom_eqReduceFalseSq} . : .
{3,atom_eqReduceTrueSq} . : .
{124,atomnEquality} . : .
{5,atomn_eqEquality} . : .
{4,atomn_eqReduceFalseSq} . : .
{6,atomn_eqReduceTrueSq} . : .
{6116,axiomEquality} rules/rules_equality4.v : rule_axiom_equality_true3
{1514,sqequalAxiom} rules/rules_squiggle6.v : rule_cequiv_member_eq_true3
{313,axiomSqleEquality} rules/rules_squiggle6.v : rule_approx_member_eq_true3
{4,axiomSqleNEquality} . : .
{2,barInduction} . : .
{1,bar_Induction} . : .
{1356,baseApply} rules/rules_squiggle6.v : rule_apply_in_base_true3
{1,baseAtom} rules/rules_squiggle5.v : rule_atom_subtype_base_true
{2,baseAtomn} rules/rules_squiggle5.v : rule_uatom_subtype_base_true
{4818,baseClosed} rules/rules_base.v : rule_base_closed_true
{1,baseEquality} rules/rules_base.v : rule_base_equality_true3
{1,baseInt} rules/rules_squiggle5.v : rule_int_subtype_base_true
{12113,because_Cache} . : .
{5,bottomDivergent} rules/rules_false.v : rule_bottom_diverges_true3
{73,callbyvalueAdd} rules/rules_arith_callbyvalue.v : rule_callbyvalue_arith_true
{78,callbyvalueApply} rules/rules_apply_callbyvalue.v : rule_callbyvalue_apply_true
{3,callbyvalueApplyCases} rules/rules_apply_callbyvalue.v : rule_callbyvalue_apply_cases_true
{3,callbyvalueAtom} . : .
{3,callbyvalueAtom1} . : .
{3,callbyvalueAtom2} . : .
{5,callbyvalueAtomEq} . : .
{6,callbyvalueAtomnEq} . : .
{149,callbyvalueCallbyvalue} rules/rules_cft_callbyvalue.v : rule_callbyvalue_cbv_true
{142,callbyvalueDecide} rules/rules_halts_decide.v : rule_halt_decide_true3
{6,callbyvalueDivide} rules/rules_arith_callbyvalue.v : rule_callbyvalue_arith_true
{116,callbyvalueExceptionCases} rules/rules_cbv_exception.v : rule_cbv_exception_cases_true
{6,callbyvalueInt} rules/rules_number.v : rule_callbyvalue_int_true3
{12,callbyvalueIntEq} . : .
{3,callbyvalueIsatom} rules/rules_cft_callbyvalue.v : rule_callbyvalue_can_test_true
{1,callbyvalueIsatom1} rules/rules_cft_callbyvalue.v : rule_callbyvalue_can_test_true
{2,callbyvalueIsatom2} rules/rules_cft_callbyvalue.v : rule_callbyvalue_can_test_true
{12,callbyvalueIsaxiom} rules/rules_cft_callbyvalue.v : rule_callbyvalue_can_test_true
{2,callbyvalueIsinl} rules/rules_cft_callbyvalue.v : rule_callbyvalue_can_test_true
{1,callbyvalueIsinr} rules/rules_cft_callbyvalue.v : rule_callbyvalue_can_test_true
{2,callbyvalueIsint} rules/rules_cft_callbyvalue.v : rule_callbyvalue_can_test_true
{5,callbyvalueIslambda} rules/rules_cft_callbyvalue.v : rule_callbyvalue_can_test_true
{28,callbyvalueIspair} rules/rules_cft_callbyvalue.v : rule_callbyvalue_can_test_true
{26,callbyvalueLess} . : .
{7,callbyvalueMinus} rules/rules_arith_callbyvalue.v : rule_callbyvalue_minus_true
{12,callbyvalueMultiply} rules/rules_arith_callbyvalue.v : rule_callbyvalue_arith_true
{757,callbyvalueReduce} rules/rules_callbyvalue.v : rule_callbyvalue_reduce_true3
{2,callbyvalueRemainder} rules/rules_arith_callbyvalue.v : rule_callbyvalue_arith_true
{26,callbyvalueSpread} rules/rules_halts_spread.v : rule_halt_spread_true
{1,callbyvalueType} rules/rules_uni.v : rule_callbyvalue_type_true3
{2,classicalIntroduction} rules/rules_classical.v : rule_classical_introduction_true3
{1356,closedConclusion} rules/rules_struct2.v : rule_closed_conclusion_true3
{124,comment} . : .
{22,compactness} . : .
{13507,computationStep} . : .
{3383,computeAll} . : .
{6826,cumulativity} rules/rules_uni.v : rule_cumulativity_true3
{14507,cut} rules/rules_struct.v : rule_cut_true3
{47,cutEval} . : .
{141,decideExceptionCases} rules/rules_decide_exception.v : rule_decide_exception_cases_true
{41,dependentIntersectionElimination} . : .
{31,dependentIntersectionEqElimination} . : .
{2,dependentIntersectionEquality} . : .
{12,dependentIntersection_memberEquality} . : .
{10335,dependent_functionElimination} . : .
{652,dependent_pairEquality} rules/rules_product.v : rule_pair_equality_true
{5134,dependent_pairFormation} rules/rules_product.v : rule_pair_formation_true
{5092,dependent_set_memberEquality} . : .
{146,dependent_set_memberFormation} rules/rules_set.v : rule_dependent_set_member_formation_true
{378,divergentSqle} rules/rules_squiggle3.v : rule_convergence_true3
{1,divergentSqlen} . : .
{164,divideEquality} rules/rules_arith.v : rule_arithop_equality_true3
{6,divideExceptionCases} rules/rules_arith_exception.v : rule_arith_exception_cases_true
{1,divideRemainderSum} rules/integer_division.v : rule_div_rem_sum_true
{3049,equalityElimination} . : .
{7,equalityEquality} rules/rules_equality3.v : rule_equality_equality_true3
{1,equalityEqualityBase} rules/rules_equality3.v : rule_equality_equality_base_true3
{1,equalityEqualityBase1} rules/rules_equality3.v : rule_equality_equality_base1_true3
{1,equalityEqualityBase2} rules/rules_equality3.v : rule_equality_equality_base2_true3
{10012,equalitySymmetry} rules/rules_equality5.v : rule_equality_symmetry_true3
{9855,equalityTransitivity} rules/rules_equality5.v : rule_equality_transitivity_true3
{450,equalityUniverse} rules/rules_equality6.v : rule_equality_universe_true3
{1,equalityUniverseElim} rules/rules_equality.v : rule_equality_universe_elim_true
{1,exceptionAdd} rules/rules_arith_exception.v : rule_exception_arith_true3
{1,exceptionApplyCases} rules/rules_apply_exception_cases_true.v : rule_apply_exception_cases_true
{2,exceptionAtomeq} . : .
{1,exceptionAtomeq1} . : .
{1,exceptionAtomeq2} . : .
{4,exceptionCompactness} . : .
{1,exceptionDivide} rules/rules_arith_exception.v : rule_exception_arith_true3
{1,exceptionInteq} . : .
{8,exceptionLess} . : .
{1,exceptionMultiply} rules/rules_arith_exception.v : rule_exception_arith_true3
{1,exceptionNotAxiom} rules/rules_exception.v : rule_exception_not_axiom_true
{1,exceptionNotBottom} rules/rules_exception.v : rule_exception_not_bottom_true
{1,exceptionRemainder} rules/rules_arith_exception.v : rule_exception_arith_true3
{337,exceptionSqequal} rules/rules_exception.v : rule_exception_sqequal_true
{455,extract_by_obid} . : .
{20,fixpointLeast} . : .
{2,freeFromAtom1Atom2} . : .
{5,freeFromAtomAbsurdity} . : .
{21,freeFromAtomApplication} . : .
{17,freeFromAtomAxiom} . : .
{7,freeFromAtomBase} . : .
{3,freeFromAtomEquality} rules/rules_free_from_atom.v : rule_free_from_atom_equality_true3
{11,freeFromAtomSet} . : .
{23,freeFromAtomTriviality} . : .
{5937,functionEquality} rules/rules_function.v : rule_function_equality_true
{840,functionExtensionality} rules/rules_function.v : rule_function_extensionality_true
{221,hyp_replacement} rules/rules_equality7.v : rule_hyp_replacement_true3
{14505,hypothesis} rules/rules_struct.v : rule_hypothesis_true3
{13819,hypothesisEquality} rules/rules_struct.v : rule_hypothesis_equality_true
{1172,hypothesis_subsumption} . : .
{4379,imageElimination} rules/rules_image.v : rule_image_elimination_true (UNFINISHED)
{2,imageEqInduction} . : .
{1,imageEquality} rules/rules_image.v : rule_image_equality_true
{3800,imageMemberEquality} rules/rules_image.v : rule_image_member_equality_true
{9660,independent_functionElimination} . : .
{9133,independent_isectElimination} . : .
{2112,independent_pairEquality} . : .
{7350,independent_pairFormation} . : .
{486,inlEquality} rules/rules_union.v : rule_inl_equality_true
{1371,inlFormation} rules/rules_union.v : rule_inr_formation_true3
{365,inrEquality} rules/rules_union.v : rule_inr_equality_true
{1428,inrFormation} rules/rules_union.v : rule_inr_formation_true3
{5777,instantiate} . : .
{5629,intEquality} rules/rules_number.v : rule_int_equality_true3
{904,intWeakElimination} . : .
{3371,int_eqEquality} . : .
{11,int_eqExceptionCases} . : .
{64,int_eqReduceFalseSq} . : .
{82,int_eqReduceTrueSq} . : .
{10272,introduction} rules/rules_struct.v : rule_introduction_true3
{2,isAtom1ReduceTrue} . : .
{7,isAtom2ReduceTrue} . : .
{1,isatom1Cases} . : .
{1,isatom1ExceptionCases} rules/rules_cft_exception.v : rule_can_test_exception_cases_true
{5,isatom2Cases} . : .
{2,isatom2ExceptionCases} rules/rules_cft_exception.v : rule_can_test_exception_cases_true
{11,isatomCases} . : .
{3,isatomExceptionCases} rules/rules_cft_exception.v : rule_can_test_exception_cases_true
{20,isatomReduceTrue} . : .
{26,isaxiomCases} rules/rules_axiom_cases.v : rule_isaxiom_cases_true
{10,isaxiomExceptionCases} rules/rules_cft_exception.v : rule_can_test_exception_cases_true
{12876,isectElimination} rules/rules_isect_elimination.v : rule_isect_elimination_true3
{331,isectEquality} rules/rules_isect.v : rule_isect_equality_true3
{10008,isect_memberEquality} rules/rules_isect2.v : rule_isect_member_equality_true
{10524,isect_memberFormation} rules/rules_isect.v : rule_isect_member_formation_true3
{17,isinlCases} rules/rules_inl_inr_cases.v : rule_isinl_cases_true
{2,isinlExceptionCases} rules/rules_cft_exception.v : rule_can_test_exception_cases_true
{17,isinrCases} rules/rules_inl_inr_cases.v : rule_isinr_cases_true
{1,isinrExceptionCases} rules/rules_cft_exception.v : rule_can_test_exception_cases_true
{12,isintCases} . : .
{2,isintExceptionCases} rules/rules_cft_exception.v : rule_can_test_exception_cases_true
{3,isintReduceAtom} . : .
{81,isintReduceTrue} rules/rules_isint.v : rule_isint_reduce_true_true3
{6,islambdaCases} . : .
{4,islambdaExceptionCases} rules/rules_cft_exception.v : rule_can_test_exception_cases_true
{20,ispairCases} rules/rules_cft.v : rule_ispair_cases_true
{21,ispairExceptionCases} rules/rules_cft_exception.v : rule_can_test_exception_cases_true
{10560,lambdaEquality} rules/rules_function.v : rule_lambda_equality_true
{10310,lambdaFormation} rules/rules_function.v : rule_lambda_formation_true
{14232,lemma_by_obid} . : .
{223,lessCases} . : .
{1,lessDiscrete} rules/rules_integer_ordered_ring.v : rule_less_discrete_true
{25,lessExceptionCases} rules/rules_less_exception.v : rule_less_exception_cases_true
{2,lessTransitive} rules/rules_integer_ordered_ring.v : rule_less_transitive_true
{6,lessTrichotomy} rules/rules_integer_ordered_ring.v : rule_less_trichotomy_true
{7,minusExceptionCases} rules/rules_arith_exception.v : rule_minus_exception_cases_true
{1,multiplyAssociative} rules/rules_integer_ring.v : rule_mul_associative_true
{1,multiplyCommutative} rules/rules_integer_ring.v : rule_mul_commutative_true
{1,multiplyDistributive} rules/rules_integer_ring.v : rule_mul_distributive_true
{957,multiplyEquality} rules/rules_arith.v : rule_arithop_equality_true3
{11,multiplyExceptionCases} rules/rules_arith_exception.v : rule_arith_exception_cases_true
{1,multiplyOne} rules/rules_integer_ring.v : rule_mul_one_true
{2,multiplyPositive} rules/rules_integer_ordered_ring.v : rule_multiply_positive_true
{7257,natural_numberEquality} rules/rules_number.v : rule_natural_number_equality_true3
{1,parameterizedRecEquality} . : .
{341,pertypeElimination} rules/rules_pertype.v : rule_pertype_elimination_t_true
{10,pertypeEquality} rules/rules_pertype.v : rule_pertype_equality_true
{10,pertypeMemberEquality} rules/rules_pertype.v : rule_pertype_member_equality_true
{679,pointwiseFunctionality} rules/rules_functionality.v : rule_functionaliy_true
{225,pointwiseFunctionalityForEquality} rules/rules_functionality.v : rule_functionaliy_for_equality_true
{9650,productElimination} rules/rules_product.v : rule_product_elimination_true
{3924,productEquality} rules/rules_product.v : rule_product_equality_true
{1,productUniverseElim} . : .
{3395,promote_hyp} . : .
{1,remainderBounds1} rules/integer_division.v : rule_rem_bounds1_true
{1,remainderBounds2} rules/integer_division.v : rule_rem_bounds2_true
{1,remainderBounds3} rules/integer_division.v : rule_rem_bounds3_true
{1,remainderBounds4} rules/integer_division.v : rule_rem_bounds4_true
{1,remZero} rules/integer_division.v : rule_rem_zero_true
{2,remPositive} rules/integer_division.v : rule_rem_positive_true
{2,remNegative} rules/integer_division.v : rule_rem_negative_true
{145,remainderEquality} rules/rules_arith.v : rule_arithop_equality_true3
{2,remainderExceptionCases} rules/rules_arith_exception.v : rule_arith_exception_cases_true
{7743,rename} . : .
{7939,setElimination} rules/rules_set.v : rule_set_elimination_true
{4128,setEquality} rules/rules_set.v : rule_set_equality_true
{191,spreadEquality} rules/rules_product.v : rule_spread_equality_true
{25,spreadExceptionCases} rules/rules_exception.v : rule_spread_exception_cases_true
{13295,sqequalRule} . : .
{2,sqequalBase} rules/rules_squiggle.v : rule_cequiv_base_true
{1,sqequalDefinition} . : .
{3,sqequalElimination} . : .
{11,sqequalExtensionalEquality} rules/rules_squiggle4.v : rule_cequiv_extensional_equality_true
{13257,sqequalHypSubstitution} rules/rules_squiggle2.v : rule_cequiv_subst_hyp_true
{222,sqequalIntensionalEquality} . : .
{13946,sqequalReflexivity} rules/rules_squiggle.v : rule_cequiv_refl_true
{181,sqequalSqle} rules/rules_squiggle.v : rule_cequiv_approx_true3
{13505,sqequalSubstitution} rules/rules_squiggle2.v : rule_cequiv_subst_concl_true3
{13507,sqequalTransitivity} rules/rules_squiggle8.v : rule_cequiv_trans_true3
{6,sqequalZero} . : .
{5,sqequal_n rule} . : .
{1,sqequalnIntensionalEquality} . : .
{4,sqequalnReflexivity} . : .
{1,sqequalnSqlen} . : .
{1,sqequalnSymm} . : .
{162,sqleRule} . : .
{1,sqleDefinition} . : .
{3,sqleExtensionalEquality} rules/rules_squiggle4.v : rule_approx_extensional_equality_true
{6,sqleIntensionalEquality} . : .
{1,sqleLambda} . : .
{531,sqleReflexivity} rules/rules_squiggle.v : rule_approx_refl_true3
{10,sqleTransitivity} rules/rules_squiggle8.v : rule_approx_trans_true3
{1,sqleZero} . : .
{1,sqle_n rule} . : .
{1,sqlenIntensionalEquality} . : .
{2,sqlenSqequaln} . : .
{1,sqlenSubtypeRel} . : .
{18,strong_bar_Induction} . : .
{2044,substitution} . : .
{14225,thin} rules/rules_struct.v : rule_thin_true
{2,token1Equality} . : .
{65,token2Equality} . : .
{442,tokenEquality} . : .
{2,tryReduceValue} rules/rules_exception2.v : rule_try_reduce_value_true
{45,unhideable_token_permute} . : .
{6262,unionElimination} rules/rules_union.v : rule_union_elimination_true (UNFINISHED)
{1398,unionEquality} rules/rules_union.v : rule_union_equality_true
{7415,universeEquality} rules/rules_uni.v : rule_universe_equality_true3
{7964,voidElimination} rules/rules_void.v : rule_void_elimination_true
{6596,voidEquality} rules/rules_void.v : rule_void_equality_true3
--------------------------------------------------------------------------------------------------------------------------------
TOTAL RULES PROVED: 161 out of 263
(not counting 2 UNFINISHED)