Changeset 3478 for LTS/Language.ma


Ignore:
Timestamp:
Sep 22, 2014, 4:50:21 PM (5 years ago)
Author:
piccolo
Message:

fixed costlabels

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3449 r3478  
    926926lemma fresh_keep_n_ok : ∀n,m,l.
    927927is_fresh_for_return l n → n ≤ m → is_fresh_for_return l m.
    928 #n #m #l lapply n -n lapply m -m elim l // ** #x #xs #IH #n #m
     928#n #m #l lapply n -n lapply m -m elim l // *
     929[1,2,3: * #x] #xs #IH #n #m
    929930normalize [2: * #H1] #H2 #H3 [ %] /2 by transitive_le/
    930931qed.
     
    13551356lemma fresh_for_subset : ∀l1,l2,n.l1 ⊆ l2 → is_fresh_for_return … l2 n →
    13561357is_fresh_for_return … l1 n.
    1357 #l1 elim l1 // ** #x #xs #IH #l2 #n * #H1 #H2 #H3 whd
     1358#l1 elim l1 // * [1,2,3: * #x] #xs #IH #l2 #n * #H1 #H2 #H3 whd
    13581359try(@IH) // % [2: @IH //] elim l2 in H1 H3; normalize [*]
    1359 ** #y #ys #IH normalize
     1360* [1,2,3: * #y] #ys #IH normalize
    13601361[2,3: * [2,4: #H3 [2: @IH //] * #H4 #H5 @IH //
    13611362|*: #EQ destruct * //
    13621363]]
    13631364*
    1364 [ #EQ destruct ] #H3 #H4 @IH //
     1365[1,3: #EQ destruct ] #H3 #H4 @IH //
    13651366qed.
    13661367
    13671368lemma fresh_append : ∀n,l1,l2.is_fresh_for_return l1 n → is_fresh_for_return l2 n →
    13681369is_fresh_for_return (l1@l2) n.
    1369 #n #l1 lapply n -n elim l1 // ** #x #xs #IH #n #l2 [2: * #H1 ] #H2 #H3
     1370#n #l1 lapply n -n elim l1 // * [1,2,3: * #x] #xs #IH #n #l2 [2: * #H1 ] #H2 #H3
    13701371[ % // @IH //] @IH //
    13711372qed.
Note: See TracChangeset for help on using the changeset viewer.