- Timestamp:
- Jun 14, 2012, 4:03:19 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2071 r2072 804 804 let 〈ppc,code〉 ≝ ppc_code in 805 805 ppc = bitvector_of_nat … (|pre|) ∧ 806 nat_of_bitvector … (sigma ppc) = |code| ∧ 806 807 ∀ppc'.∀ppc_ok'. 807 808 nat_of_bitvector … ppc' < nat_of_bitvector … ppc → … … 823 824 fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉. 824 825 [ cases (foldl_strong ? (λx.Σy.?) ???) in p2; #ignore_revcode #Hfold #EQignore_revcode 825 >EQignore_revcode in Hfold; * #Hfold1#Hfold2 whd >p1 whd #ppc #LTppc @Hfold2826 >EQignore_revcode in Hfold; * * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd #ppc #LTppc @Hfold2 826 827 >Hfold1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 827 828 (* CSC: FALSE, NEEDS ADDITIONAL ASSUMPTION *) cases daemon 828 | % // #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip] 829 | % 830 [ % // (*CSC: NEW INVARIANT FOR JAAP!*) cases daemon ] 831 #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip] 829 832 | cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code 830 * #IH1 #IH2 whd % [ normalize nodelta >IH1 >length_append cases daemon (*CSC: TRUE, LEMMA NEEDED *)] 833 * * #IH1 #IH3 #IH2 whd % [% 834 [ >length_append normalize nodelta >IH1 (*CSC: TRUE, LEMMA NEEDED *) cases daemon 835 |2: (*CSC: NEES JAAP INVARIANT*) cases daemon]] 831 836 #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 #LTppc_ppc 832 837 cases (le_to_or_lt_eq … LTppc_ppc) … … 873 878 >eq_assembly_1_pseudoinstruction #j #LTj >reverse_append >reverse_reverse #K 874 879 >IH 875 [2: (*CSC: FALSE, WE CAN PROVE PPC'<=PPC, SO WHAT? *) cases daemon880 [2: >length_reverse <IH3 (*CSC: FALSE, WE CAN PROVE PPC'<=PPC, SO WHAT? *) cases daemon 876 881 | @shift_nth_prefix 877 882 |3: @le_S_S_to_le @(transitive_le … LTppc'') >nat_of_bitvector_add
Note: See TracChangeset
for help on using the changeset viewer.