- Timestamp:
- Jul 6, 2012, 12:05:25 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2158 r2159 963 963 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip] % ] 964 964 #EQpc_delta2 965 cases (sigma_pol_ok2 … ppc_ok) -sigma_pol_ok2 966 <eq_fetch_pseudo_instruction <eq_create_label_cost_map <EQpc_delta2 967 #sigma_pol3 #sigma_pol4 965 968 % [ % [% [% ] ] ] 966 969 [ >length_append normalize nodelta >IH1 @sym_eq @add_bitvector_of_nat 967 | >length_append >length_reverse <IH3 cases daemon (*CSC: maybe, using monotonicity*) 968 | lapply (sigma_pol_ok2 … ppc_ok) * #sigma_pol_ok3 969 <eq_fetch_pseudo_instruction <eq_create_label_cost_map #sigma_pol4 970 >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta >EQpc_delta2 970 | >length_append >length_reverse <IH3 <EQpc_delta >commutative_plus 971 cases sigma_pol4 [ #LT @(transitive_le … LT) // | * #_ #EQ >EQ % ] 972 | >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta 971 973 #abs >abs in sigma_pol4; * 972 974 [ #abs' cases (absurd ? abs' (not_le_Sn_n …)) 973 975 | * #abs' #_ <abs' >length_append <plus_n_Sm <plus_n_O @eq_f >IH1 974 976 >nat_of_bitvector_bitvector_of_nat_inverse // ] 975 | cases (sigma_pol_ok2 … ppc_ok) 976 whd in match instruction_size; normalize nodelta >p2 <eq_fetch_pseudo_instruction 977 <eq_create_label_cost_map 978 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip] 979 #sigma_ok >sigma_ok #sigma_pol_ok3 -sigma_pol_ok2 980 >length_append >length_reverse <IH3 <EQpc_delta cases sigma_pol_ok3 981 [ #LT %1 >nat_of_bitvector_add 977 | >length_append >length_reverse <IH3 <EQpc_delta cases sigma_pol4 978 [ #LT %1 >sigma_pol3 >nat_of_bitvector_add 982 979 [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption] 983 980 >nat_of_bitvector_bitvector_of_nat_inverse try assumption // 984 981 | * #EQ1 #EQ2 %2 % 985 982 [ lapply (eq_f … (bitvector_of_nat 16) … EQ2) <add_bitvector_of_nat_plus 986 >bitvector_of_nat_inverse_nat_of_bitvector #X >X @bitvector_of_nat_exp_zero983 >bitvector_of_nat_inverse_nat_of_bitvector <sigma_pol3 #X >X @bitvector_of_nat_exp_zero 987 984 | >commutative_plus assumption ]] 988 985 | cases daemon
Note: See TracChangeset
for help on using the changeset viewer.