Changeset 2481 for src/joint/linearise.ma
 Timestamp:
 Nov 20, 2012, 6:40:08 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/linearise.ma
r2474 r2481 731 731 λp,prog_in,sigma. 732 732 let prog_out ≝ linearise … prog_in in 733 ∀i. 734 let fn_in ≝ prog_if_of_function ?? prog_in i in 735 let fn_out ≝ prog_if_of_function ?? prog_out «i, hide_prf ??» in 733 ∀i : Σi.is_internal_function_of_program … prog_in i.∀prf. 734 let fn_in ≝ if_of_function … i in 735 let i' : Σi.is_internal_function_of_program … prog_out i ≝ «pi1 ?? i, prf» in 736 let fn_out ≝ if_of_function … i' in 736 737 let sigma_local ≝ sigma i in 737 738 good_local_sigma ?? (joint_if_code ?? fn_in) (joint_if_entry … fn_in) 738 739 (joint_if_code ?? fn_out) sigma_local. 739 @if_propagate @(pi2 … i)740 qed.741 740 742 741 lemma linearise_spec : ∀p,prog.∃sigma.good_sigma p prog sigma. 743 742 #p #prog 744 743 letin sigma ≝ 745 (λi .746 let fn_in ≝ prog_if_of_function ?? progi in744 (λi : Σi.is_internal_function_of_program … prog i. 745 let fn_in ≝ if_of_function … i in 747 746 \snd (linearise_int_fun … fn_in)) 748 747 %{sigma} 749 #i >(prog_if_of_function_transform … i) [2: % ]748 #i #prf >(prog_if_of_function_transform … i) [2: % ] 750 749 normalize nodelta 751 750 cases (linearise_int_fun ???) * #fn_out #sigma_loc
Note: See TracChangeset
for help on using the changeset viewer.