Changeset 3445 for LTS/Language.ma
 Timestamp:
 Feb 17, 2014, 5:45:26 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Language.ma
r3416 r3445 687 687 include "Simulation.ma". 688 688 689 let rec len ( S : abstract_status) (st1 : S) (st2 : S) (t : raw_trace Sst1 st2)689 let rec len (s : abstract_status) (st1 : s) (st2 : s) (t : raw_trace s st1 st2) 690 690 on t : ℕ ≝ 691 691 match t with 692 692 [ t_base s ⇒ O 693  t_ind s1 s2 s3 l prf lt ⇒ (len … lt) + 1693  t_ind s1 s2 s3 l prf lt ⇒ S (len … lt) 694 694 ]. 695 695 (* … … 1162 1162 qed. 1163 1163 1164 definition fresh_for_prog_aux : ∀p,p'.Program p p' → ℕ → ℕ ≝ 1165 λp,p',prog,n.foldl … (λn,i.max n (compute_max_n … (f_body … i))) n (env … prog). 1166 1167 include alias "arithmetics/nat.ma". 1168 1169 lemma max_1 : ∀n,m,k.k ≤ m → k ≤ max m n. 1170 #m #n #k #H normalize @leb_elim // normalize nodelta #H1 1171 /2 by transitive_le/ 1172 qed. 1173 1174 lemma max_2 : ∀n,m,k.k≤ n → k ≤ max m n. 1175 #m #n #k #H normalize @leb_elim // #H1 normalize nodelta 1176 @(transitive_le … H) @(transitive_le … (not_le_to_lt … H1)) // 1177 qed. 1178 1179 lemma fresh_aux_ok : ∀p,p'.∀prog : Program p p'.∀n,m.n ≤ m → 1180 fresh_for_prog_aux … prog n ≤ fresh_for_prog_aux … prog m. 1181 #p #p' * #env #main elim env // #hd #tl #IH #n #m #H whd in ⊢ (?%%); 1182 @IH whd in ⊢ (?%?); @leb_elim normalize nodelta 1183 [ #H1 @max_2 //  #_ @max_1 // ] 1184 qed. 1185 1164 1186 definition fresh_for_prog : ∀p,p'.Program p p' → ℕ ≝ 1165 λp,p',prog.f oldl … (λn,i.max n (compute_max_n … (f_body … i)))1166 (compute_max_n … (main … prog)) (env … prog).1187 λp,p',prog.fresh_for_prog_aux … prog 1188 (compute_max_n … (main … prog)). 1167 1189 1168 1190 definition translate_env ≝ … … 1344 1366 1345 1367 definition labels_of_prog : ∀p,p'.Program p p' → ? ≝ 1346 λp,p',prog.foldr … (λx,l.l @ (get_labels_of_code … (f_body … x))) [ ] (env … prog). 1368 λp,p',prog.foldr … (λx,l.l @ (get_labels_of_code … (f_body … x))) 1369 (get_labels_of_code … (main … prog)) (env … prog). 1347 1370 1348 1371 lemma cast_return_append : ∀l1,l2.cast_return_to_cost_labels … (l1 @ l2) = 1349 1372 (cast_return_to_cost_labels … l1) @ (cast_return_to_cost_labels … l2). 1350 #l1 #l2 @(sym_eq … (map_append …)) qed. 1373 #l1 #l2 @(sym_eq … (map_append …)) qed. 1374 1375 include alias "arithmetics/nat.ma". 1376 1377 1378 lemma is_fresh_code : ∀p.∀i : Instructions p. 1379 is_fresh_for_return (get_labels_of_code … i) (compute_max_n … i). 1380 #p #main elim main // 1381 [ #seq * [ * #lbl] #i #IH normalize // @(fresh_keep_n_ok … IH) 1382 inversion(leb ? lbl) // @leb_elim #Hlbl #EQ destruct normalize nodelta 1383 /2 by le_S/ 1384  #cond * #ltrue #i1 * #lfalse #i2 #i3 #IH1 #IH2 #IH3 whd in ⊢ (?%%); 1385 @fresh_append 1386 [ @(fresh_keep_n_ok … IH1) @le_S @max_1 @max_1 @max_1 @max_1 // 1387  @fresh_append 1388 [ @(fresh_keep_n_ok … IH2) @le_S @max_1 @max_1 @max_1 @max_2 // 1389  @(fresh_keep_n_ok … IH3) @le_S @max_1 @max_1 @max_2 // 1390 ] 1391 ] 1392  #cond * #ltrue #i1 * #lfalse #i2 #IH1 #IH2 whd in ⊢ (?%%); @fresh_append 1393 [ @(fresh_keep_n_ok … IH1) @le_S @max_1 @max_1 @max_1 // 1394  @(fresh_keep_n_ok … IH2) @le_S @max_1 @max_1 @max_2 // 1395 ] 1396  #f #act_p * [ * #lbl] #i #IH whd in ⊢ (?%%); // 1397 change with ([?]@?) in ⊢ (?%?); @fresh_append 1398 [ whd % // @le_S @max_1 // 1399  @(fresh_keep_n_ok … IH) @le_S @max_2 // 1400 ] 1401  * #lin #io * #lout #i #IH whd in ⊢ (?%%); @(fresh_keep_n_ok … IH) 1402 @le_S @max_1 @max_1 // 1403 ] 1404 qed. 1405 1406 lemma is_fresh_fresh_for_prog : ∀p,p'.∀prog : Program p p'. 1407 is_fresh_for_return (labels_of_prog … prog) (fresh_for_prog … prog). 1408 #p #p' * #env #main whd in match fresh_for_prog; normalize nodelta whd in ⊢ (?%?); 1409 elim env // * #sig #cost #i #tail #IH whd in ⊢ (?%?); @fresh_append 1410 [ @(fresh_keep_n_ok … IH) @fresh_aux_ok @max_1 // 1411  @(fresh_keep_n_ok … (is_fresh_code … i)) whd in match fresh_for_prog_aux; normalize nodelta 1412 whd in ⊢ (??%); elim tail [ @max_2 // ] #hd1 #tl1 #IH1 @(transitive_le … IH1) 1413 whd in ⊢ (??%); change with (fresh_for_prog_aux ?? (mk_Program ?? tl1 main) ?) in ⊢ (?%%); 1414 @fresh_aux_ok @max_1 // 1415 ] 1416 qed. 1417 1418 lemma subset_def : ∀A : DeqSet.∀l1,l2 : list A.(∀x.x ∈l1 → x ∈ l2) → l1 ⊆ l2. 1419 #A #l1 elim l1 // #x #xs #IH #l2 #H % 1420 [ @memb_to_mem >H // >memb_hd // 1421  @IH #y #H1 @H >memb_cons // >H1 // 1422 ] 1423 qed. 1424 1425 lemma memb_cast_return : ∀keep,x.x ∈ cast_return_to_cost_labels keep → 1426 ∃ y.x = a_return_post y ∧ bool_to_Prop (y ∈ keep). 1427 #keep elim keep 1428 [ #x *] #x #xs #IH #y whd in match cast_return_to_cost_labels; 1429 whd in match (map ????); whd in match (memb ???); inversion(y==x) 1430 [ #Hx #_ %{x} >(\P Hx) %{(refl …)} >memb_hd // 1431  #Hx normalize nodelta #H cases(IH … H) #z * #H1 #H2 %{z} %{H1} >memb_cons // >H2 // 1432 ] 1433 qed. 1434 1435 lemma subset_append : ∀A.∀l1,l2,l3 : list A.l1 ⊆ l3 → l2 ⊆ l3 → (l1 @ l2) ⊆ l3. 1436 #A #l1 elim l1 // #x #xs #IH #l2 #l3 * #H1 #H2 #H3 % /2/ 1437 qed. 1438 1439 lemma subset_def_inv : ∀A.∀l1,l2 : list A. l1 ⊆ l2 → ∀x.mem … x l1 → mem … x l2. 1440 #A #l1 elim l1 [ #l2 * #x * ] #x #xs #IH #l2 * #H1 #H2 #y * 1441 [ #EQ destruct //  #H3 @IH // ] 1442 qed. 1443 1444 lemma transitive_subset : ∀A.transitive … (subset A). 1445 #A #l1 elim l1 // #x #xs #IH #l2 #l3 * #H1 #H2 #H3 % 1446 [ @(subset_def_inv … H3) //  @IH // ] 1447 qed. 1448 1449 lemma subset_append_h1 : ∀A.∀l1,l2,l3 : list A.l1 ⊆ l3 → l1 ⊆ (l3 @ l2). 1450 #A #l1 elim l1 // #x #x2 #IH #l2 #l3 * #H1 #H2 % [ @mem_append_l1 //  @IH // ] 1451 qed. 1452 1453 lemma subset_append_h2 : ∀A.∀l1,l2,l3 : list A.l2 ⊆ l3 → l2 ⊆ (l1 @ l3). 1454 #A #l1 elim l1 // #x #xs #IH #l2 elim l2 // #y #ys #IH #l3 * #H1 #H2 % 1455 [ @mem_append_l2 //  @IH // ] 1456 qed. 1457 1458 lemma lab_to_keep_in_prog : ∀p,p'.∀prog : Program p p'. 1459 ∀t_prog,m,keep.trans_prog … prog = 〈t_prog,m,keep〉 → 1460 (cast_return_to_cost_labels keep) ⊆ (labels_of_prog p p' prog). 1461 #p #p' * #env #main #t_prog #m #keep whd in match trans_prog; normalize nodelta 1462 @pair_elim * #env1 #fresh * #m1 #keep1 #EQenv1 normalize nodelta #EQ destruct 1463 lapply EQenv1 EQenv1 lapply keep1 keep1 lapply m1 m1 lapply fresh fresh 1464 lapply env1 env1 generalize in match (fresh_for_prog ???); elim env 1465 [ #n #t_env #n1 #m #keep whd in ⊢ (??%? → ?); #EQ destruct whd in match (append ???); 1466 @subset_def #x #H whd in match (labels_of_prog); normalize nodelta 1467 whd in match (foldr ?????); cases(memb_cast_return … H) H #x1 * #EQ1 #H destruct 1468 @(lab_to_keep_in_domain … H) 1469  #x #xs #IH #n #t_env #n1 #m #keep whd in ⊢ (??%? → ?); @pair_elim 1470 * #t_env_tail #fresh_tail * #t_m_tail #t_keep_tail 1471 change with (translate_env ????) in match (foldr ?????); #EQt_env_tail 1472 normalize nodelta #EQ1 destruct >cast_return_append @subset_append 1473 [ >cast_return_append @subset_append 1474 [ whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????); 1475 @subset_def #y #H cases(memb_cast_return … H) H #y1 * #EQ destruct #H 1476 >memb_append_l2 // @(lab_to_keep_in_domain … H) 1477  whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????); 1478 change with (labels_of_prog ?? (mk_Program ?? xs ?)) in match (foldr ?????); 1479 @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail)) 1480 >cast_return_append @subset_append_h1 // 1481 ] 1482  whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????); 1483 change with (labels_of_prog ?? (mk_Program ?? xs ?)) in match (foldr ?????); 1484 @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail)) 1485 >cast_return_append @subset_append_h2 // 1486 ] 1487 ] 1488 qed. 1489 1490 lemma fresh_call_post_trans_ok : ∀p.∀i : Instructions p.∀n,l. 1491 n ≤ fresh … (call_post_trans … i n l). 1492 #p #i elim i // 1493 qed. 1494 1495 lemma fresh_translate_env_ok : ∀p,p'.∀env,t_env : list (env_item p p').∀n,n1,m,keep. 1496 translate_env … env n = 〈t_env,n1,m,keep〉 → n ≤ n1. 1497 #p #p' #env elim env 1498 [ #t_env #n #n1 #m #keep whd in ⊢ (??%? → ?); #EQ destruct // ] 1499 #x #xs #IH #t_env #n #n1 #m #keep whd in ⊢ (??%? → ?); 1500 change with (translate_env ????) in match (foldr ?????); @pair_elim 1501 * #t_env_tail #fresh_tail * #t_m_tail #t_keep_tail #EQt_env_tail normalize nodelta 1502 #EQ destruct @(transitive_le … (IH … EQt_env_tail)) @fresh_call_post_trans_ok 1503 qed. 1504 1351 1505 1352 1506 lemma trans_env_ok : ∀p : state_params.∀ prog. … … 1388 1542 [ @(fresh_keep_n_ok … Hfresh1) 1389 1543 @(fresh_for_subset … (labels_of_prog … prog)) 1390 cases daemon (*TODO*)1391  cases daemon (*TODO*)1544 [ @(lab_to_keep_in_prog … EQkeep1)  @is_fresh_fresh_for_prog ] 1545  @(transitive_le … (fresh_translate_env_ok … EQtail)) // 1392 1546 ] 1393 1547  whd in ⊢ (??%?); @eq_function_name_elim [2: * #H @⊥ @H %] #_ normalize nodelta … … 1522 1676 qed. 1523 1677 1524 1678 lemma len_append : ∀S : abstract_status.∀st1,st2,st3 : S. 1679 ∀t1 : raw_trace … st1 st2.∀t2 : raw_trace … st2 st3. 1680 len … (t1 @ t2) = len … t1 + len … t2. 1681 #S #st1 #st2 #st3 #t1 elim t1 normalize // 1682 qed. 1683 1684 axiom permute_ok : ∀A.∀l1,l2,l3,l4,l5,l6,l7,l8,l9,x,y. 1685 (is_permutation A ((l5 @l1) @l6@l7) ((l4 @[]) @l6@l7) 1686 →is_permutation A ((l6 @l2) @l7) ((l3 @l8) @l9) 1687 →is_permutation A 1688 (y ::((l6 @((x ::l5) @(l1 @l2))) @l7)) 1689 (((x ::l4 @y ::l3) @l8) @l9)). 1525 1690 1526 1691 lemma correctness : ∀p,p',prog. … … 1693 1858 [1,2,3,4,5,6,7,8: cases daemon (*assurdi*) ] 1694 1859 #st41 #st42 #r_t #mem1 #new_cont #opt_l1 #cd #EQcode41 #EQcont41 #EQ destruct(EQ) 1695 #EQio41 #EQio42 #EQmem1 #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct # _ #_1696 # _ whd in ⊢ (?(?%) → ?); >EQcode11 in ⊢ (% → ?); normalize nodelta1697 inversion(opt_l) in ⊢(% → ?); normalize nodelta [2: #lbl #_ * ] #EQopt_l *1698 # Hpre_t1 #Hpre_t2 whd in ⊢ (% → ?); #EQcont11_42 whd in ⊢ (% → ?); #EQ destruct1699 # IH1 #IH2 #st1' #abs_top #abs_tail1860 #EQio41 #EQio42 #EQmem1 #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct #st11_noio 1861 #st41_noio #_ whd in ⊢ (?(?%) → ?); >EQcode11 in ⊢ (% → ?); normalize nodelta 1862 inversion(opt_l) in ⊢(% → ?); normalize nodelta [2: #lbl #_ * ] #EQopt_l destruct(EQopt_l) 1863 #_ #Hpre_t1 #Hpre_t2 whd in ⊢ (% → ?); #EQcont11_42 whd in ⊢ (% → ?); 1864 #EQ destruct #IH1 #IH2 #st1' #abs_top #abs_tail 1700 1865 whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1 1701 1866 #abs_top_cont #abs_tail_cont #EQcheck … … 1704 1869 #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ) 1705 1870 lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H 1706 cases(H … EQenv_it) H #env_it' * #fresh' * #EQenv_it' ***** #EQtrans1871 cases(H … EQenv_it) H #env_it' * #fresh' ** #is_fresh_fresh' #EQenv_it' ***** #EQtrans 1707 1872 #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep 1708 1873 change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean; 1709 1874 [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind 1710 1875 inversion opt_l' in EQcode_st1'; [ #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta 1711 [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] cases(memb ???) normalize nodelta 1876 [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] destruct(EQopt_l') 1877 inversion(memb ???) normalize nodelta #Hlbl_keep' 1712 1878 [ cases(?==?) normalize nodelta ] 1713 1879 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct 1714 xxxxxxx 1715 1716 1717 1718 cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) (abs_top''@abs_tail_cont) (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?)))) 1719 [2: whd >EQcont12 1720 change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????); 1721 >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta >EQopt_l' 1722 whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta 1723 % // % // % // % [/5 by conj/] >EQcode12 <EQtrans 1724 @(inverse_call_post_trans … fresh') 1725 [2: % *: [2,3: /2 by / ] 1726 cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2 1727 whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append 1728 #no_dup lapply(no_duplicates_append_r … no_dup) #H1 1729 lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); H1 1730 change with ([?]@?) in match (?::?); #H1 1731 lapply(no_duplicates_append_r … H1) >append_nil // 1732 ] 1880 cases(IH1 1881 (mk_state ? 1882 (f_body … env_it') 1883 (〈ret_act (Some ? lbl'),i'〉 :: (cont … st1')) 1884 (store ? st12) false) 1885 (abs_top''@abs_tail_cont) 1886 (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?)))) 1887 [2: whd >EQcont12 1888 change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????); 1889 >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta 1890 whd in match ret_costed_abs; normalize nodelta >Hlbl_keep' normalize nodelta 1891 % // % // % // % [/5 by conj/] >EQcode12 <EQtrans 1892 @(inverse_call_post_trans … fresh') 1893 [2: % *: [2,3: /2 by / ] 1894 cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2 1895 whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append 1896 #no_dup lapply(no_duplicates_append_r … no_dup) #H1 1897 lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); H1 1898 change with ([?]@?) in match (?::?); #H1 1899 lapply(no_duplicates_append_r … H1) >append_nil // 1733 1900 ] 1734 #abs_top''' * #abs_tail''' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen 1735 %{abs_top'''} 1736 %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) … t')} 1737 [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [2: whd in ⊢ (??%%); >EQlen %] 1738 %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%); 1739 >EQlab_env_it >associative_append >associative_append 1740 >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%); 1741 >EQopt_l' in t'; #t' 1742 whd in match (map_labels_on_trace ??); >EQgen_labels 1743 whd in match (foldr ?????); >append_nil 1744 whd in match (get_costlabels_of_trace ????); 1745 @is_permutation_cons 1746 >append_nil whd in match (append ???) in ⊢ (???%); // 1747 1748 1749 ] 1750  whd in ⊢ (???% → ?); #EQ destruct 1751 ] 1752  1901 ] 1902 #abs_top''' * #abs_tail''' * #st41' * #t1' ** #Hst41st41' #EQcosts #EQlen 1903 whd in Hst41st41'; inversion(check_continuations …) in Hst41st41'; [ #_ * ] 1904 ** #H2 #abs_top_cont' #abs_tail_cont' >EQcont41 in ⊢ (% → ?); 1905 whd in ⊢ (??%? → ?); inversion(cont … st41') normalize nodelta 1906 [ #_ #EQ destruct(EQ) ] * #act_lbl #i'' #cont_st42' #_ #EQcont_st41' 1907 change with (check_continuations ?????) in match (foldr2 ???????); 1908 inversion(check_continuations ?????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] 1909 ** #H3 #abs_top_cont'' #abs_tail_cont'' #EQ_contst42 >m_return_bind 1910 normalize nodelta inversion(call_post_clean ?????) normalize nodelta 1911 [ #_ whd in ⊢ (??%% → ?); #EQ destruct ***** ] * #abs_top'''' #i''' 1912 #EQ_clean_i'' inversion(act_lbl) normalize nodelta [1,3,4: cases daemon (*assurdi*)] 1913 cut(act_lbl = ret_act (Some ? lbl') ∧ cont_st42' = cont … st1' ∧ i'' = i') 1914 [ cases daemon (*BIG LEMMA!!!*)] 1915 ** #EQ1 #EQ2 #EQ3 destruct #x #EQ destruct whd in match ret_costed_abs; normalize nodelta 1916 >Hlbl_keep' normalize nodelta 1917 whd in ⊢ (??%% → ?); #EQ destruct ****** #_ #HH3 #EQ destruct(EQ) 1918 >EQcode41 in ⊢ (% → ?); inversion(code … st41') 1919 [1,3,4,5,6,7: cases daemon (*ASSURDI*) ] #r_t' #EQcode_st41' whd in ⊢ (??%% → ?); 1920 #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct(EQ) #EQstore_st41' #EQinfo_st41' 1921 #EQ destruct(EQ) >EQcont11_42 in EQcheck; >EQ_contst42 in ⊢ (% → ?); 1922 #EQ destruct(EQ) >EQi' in EQ_clean_i''; #EQ destruct(EQ) 1923 cases(IH2 1924 (mk_state ? i' (cont … st1') (store … st42) (io_info … st42)) 1925 abs_tail_cont abs_top'''') 1926 [2: whd >EQ_contst42 normalize nodelta % // % // % // % // @EQi' ] 1927 #abs_top_1 * #abs_tail_1 * #st5' * #t2' ** #Hst5_st5' #EQcosts' 1928 #EQlen' %{abs_top_1} %{abs_tail_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))} 1929 [3: @hide_prf @(call … EQcode_st1' … EQenv_it') // 1930 1: @hide_prf @(ret_instr … EQcode_st41' … EQcont_st41') // 1931 2,4: skip 1932 ] 1933 % [2: whd in ⊢ (??%%); @eq_f >len_append >len_append @eq_f2 // 1934 whd in ⊢ (??%%); @eq_f // ] 1935 %{Hst5_st5'} whd in match (map_labels_on_trace ??); 1936 change with (map_labels_on_trace ??) in match (foldr ?????); 1937 >map_labels_on_trace_append >get_cost_label_append 1938 whd in match (get_costlabels_of_trace ??? (t_ind …)); 1939 whd in match (get_costlabels_of_trace ??? (t_ind …)); 1940 >get_cost_label_append 1941 whd in match (get_costlabels_of_trace ??? (t_ind …)); 1942 >map_labels_on_trace_append >EQlab_env_it >EQgen_labels 1943 whd in match (map_labels_on_trace ? [ ]); 1944 whd in match (append ? (nil ?) ?); 1945 cut (∀A.∀l: list A. [ ] @ l = l) [//] #nil_append 1946 >nil_append >nil_append >nil_append @(permute_ok … EQcosts EQcosts') 1947 ] 1948 qed. 1753 1949 1754 1950
Note: See TracChangeset
for help on using the changeset viewer.