Changeset 3478 for LTS/Language.ma
 Timestamp:
 Sep 22, 2014, 4:50:21 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Language.ma
r3449 r3478 926 926 lemma fresh_keep_n_ok : ∀n,m,l. 927 927 is_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 929 930 normalize [2: * #H1] #H2 #H3 [ %] /2 by transitive_le/ 930 931 qed. … … 1355 1356 lemma fresh_for_subset : ∀l1,l2,n.l1 ⊆ l2 → is_fresh_for_return … l2 n → 1356 1357 is_fresh_for_return … l1 n. 1357 #l1 elim l1 // * * #x#xs #IH #l2 #n * #H1 #H2 #H3 whd1358 #l1 elim l1 // * [1,2,3: * #x] #xs #IH #l2 #n * #H1 #H2 #H3 whd 1358 1359 try(@IH) // % [2: @IH //] elim l2 in H1 H3; normalize [*] 1359 * * #y#ys #IH normalize1360 * [1,2,3: * #y] #ys #IH normalize 1360 1361 [2,3: * [2,4: #H3 [2: @IH //] * #H4 #H5 @IH // 1361 1362 *: #EQ destruct * // 1362 1363 ]] 1363 1364 * 1364 [ #EQ destruct ] #H3 #H4 @IH //1365 [1,3: #EQ destruct ] #H3 #H4 @IH // 1365 1366 qed. 1366 1367 1367 1368 lemma fresh_append : ∀n,l1,l2.is_fresh_for_return l1 n → is_fresh_for_return l2 n → 1368 1369 is_fresh_for_return (l1@l2) n. 1369 #n #l1 lapply n n elim l1 // * * #x#xs #IH #n #l2 [2: * #H1 ] #H2 #H31370 #n #l1 lapply n n elim l1 // * [1,2,3: * #x] #xs #IH #n #l2 [2: * #H1 ] #H2 #H3 1370 1371 [ % // @IH //] @IH // 1371 1372 qed.
Note: See TracChangeset
for help on using the changeset viewer.