Changeset 2055 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Jun 13, 2012, 12:11:21 PM (8 years ago)
Author:
sacerdot
Message:

Warning: this commit adds an hypothesis that breaks all of assembly stuff.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r2001 r2055  
    457457 (λ_.0).
    458458 @tech_cost_of_label0 @codom_dom
    459 qed.
    460 
    461 lemma shift_nth_safe:
    462  ∀T,i,l2,l1,K1,K2.
    463   nth_safe T i l1 K1 = nth_safe T (i+|l2|) (l2@l1) K2.
    464  #T #i #l2 elim l2 normalize
    465   [ #l1 #K1 <plus_n_O #K2 %
    466   | #hd #tl #IH #l1 #K1 <plus_n_Sm #K2 change with (? < ?) in K1; change with (? < ?) in K2;
    467     whd in ⊢ (???%); @IH ]
    468 qed.
    469 
    470 lemma shift_nth_prefix:
    471  ∀T,l1,i,l2,K1,K2.
    472   nth_safe T i l1 K1 = nth_safe T i (l1@l2) K2.
    473   #T #l1 elim l1 normalize
    474   [
    475     #i #l1 #K1 cases(lt_to_not_zero … K1)
    476   |
    477     #hd #tl #IH #i #l2
    478     cases i
    479     [
    480       //
    481     |
    482       #i' #K1 #K2 whd in ⊢ (??%%);
    483       @IH
    484     ]
    485   ]
    486459qed.
    487460
Note: See TracChangeset for help on using the changeset viewer.