Changeset 3479 for LTS/Language.ma
- Timestamp:
- Sep 22, 2014, 5:14:56 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Language.ma
r3478 r3479 608 608 | _ ⇒ false 609 609 ] 610 | init_act ⇒ match c2 with [init_act ⇒ true | _ ⇒ false]611 610 ]. 612 611 … … 1768 1767 * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta 1769 1768 cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta 1770 [ 1,4: [ #x #y ]#_ (*#_ #_ #_ #H*) *****1769 [ #x #y #_ (*#_ #_ #_ #H*) ***** 1771 1770 | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] ******[|*] #EQ @⊥ >EQ in Hl1; 1772 1771 normalize * /2/ ] * … … 1868 1867 [3: assumption |4: assumption |*:] /3 by nmk/ ] 1869 1868 % 1870 [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append 1869 [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} 1870 >(map_labels_on_trace_append … [lbl]) (*CSC: funzionava prima*) 1871 1871 whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el 1872 1872 @is_permutation_cons assumption … … 1913 1913 ] 1914 1914 ] 1915 #seq1 #opt_l #i' #_ #EQcode_s1' change with (m_bind ?????) in ⊢ (??%? → ?); 1915 #seq1 #opt_l #i' #_ #EQcode_s1' cases daemon (*CSC: ROTTO QUI 1916 change with (m_bind ?????) in ⊢ (??%? → ?); 1916 1917 inversion(call_post_clean ????) [1,3: #_ whd in ⊢ (??%% → ?); #EQ destruct] 1917 1918 * #gen_labs #i'' #EQclean >m_return_bind inversion(opt_l) normalize nodelta … … 1941 1942 cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % // 1942 1943 ]] 1943 %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct 1944 %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct *) 1944 1945 | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12 1945 1946 #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t … … 2277 2278 inversion(call_post_clean ?????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct *****] 2278 2279 * #gen_labs #i' #EQi' inversion act_lab normalize nodelta 2279 [ #f #lab | * [| #lbl1 ]| * [| #nf_l] |] #EQ destruct(EQ)2280 [ #f #lab | * [| #lbl1 ]| * [| #nf_l]] #EQ destruct(EQ) 2280 2281 [1,6: whd in ⊢ (??%% → ?); #EQ destruct ***** 2281 2282 |4,5: normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) ****** [2: *] #EQ destruct … … 2385 2386 cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh' 2386 2387 #EQenv_it' ***** #EQtrans 2387 #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep 2388 #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep cases daemon (*CSC: WAS WORKING 2388 2389 change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean; 2389 2390 [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind … … 2434 2435 ] 2435 2436 | whd in ⊢ (??%% → ?); #EQ destruct(EQ) 2436 ] 2437 ] *) 2437 2438 ] 2438 2439 | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #H inversion H in ⊢ ?; … … 2502 2503 lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H 2503 2504 cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh' #EQenv_it' ***** #EQtrans 2504 #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep 2505 #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep cases daemon (*CSC: was working 2505 2506 change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean; 2506 2507 [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind … … 2630 2631 ] 2631 2632 ] 2632 ]2633 qed. 2633 *)] 2634 qed.
Note: See TracChangeset
for help on using the changeset viewer.