Changeset 737 for src/RTLabs/test
 Timestamp:
 Apr 4, 2011, 5:13:09 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/test/search.ma
r731 r737 47 47 definition search1 := 1. 48 48 definition search0 := 0. 49 definition C_cost0 := ident_of_nat 8.50 definition C_cost1 := ident_of_nat 7.51 definition C_cost8 := ident_of_nat 6.52 definition C_cost6 := ident_of_nat 5.53 definition C_cost7 := ident_of_nat 4.54 definition C_cost4 := ident_of_nat 3.55 definition C_cost5 := ident_of_nat 2.56 definition C_cost2 := ident_of_nat 1.57 definition C_cost3 := ident_of_nat 0.49 definition C_cost0 := costlabel_of_nat 8. 50 definition C_cost1 := costlabel_of_nat 7. 51 definition C_cost8 := costlabel_of_nat 6. 52 definition C_cost6 := costlabel_of_nat 5. 53 definition C_cost7 := costlabel_of_nat 4. 54 definition C_cost4 := costlabel_of_nat 3. 55 definition C_cost5 := costlabel_of_nat 2. 56 definition C_cost2 := costlabel_of_nat 1. 57 definition C_cost3 := costlabel_of_nat 0. 58 58 59 59 … … 154 154 definition main1 := 1. 155 155 definition main0 := 0. 156 definition C_cost9 := ident_of_nat 0.156 definition C_cost9 := costlabel_of_nat 0. 157 157 158 158 … … 229 229 normalize (* you can examine the result here *) 230 230 % qed. 231
Note: See TracChangeset
for help on using the changeset viewer.