Ignore:
Timestamp:
Nov 20, 2012, 6:40:08 PM (8 years ago)
Author:
piccolo
Message:

corrected some inconsistencies
fixed some of lineariseProof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2474 r2481  
    731731  λp,prog_in,sigma.
    732732  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
    736737  let sigma_local ≝ sigma i in
    737738  good_local_sigma ?? (joint_if_code ?? fn_in) (joint_if_entry … fn_in)
    738739          (joint_if_code ?? fn_out) sigma_local.
    739 @if_propagate @(pi2 … i)
    740 qed.
    741740
    742741lemma linearise_spec : ∀p,prog.∃sigma.good_sigma p prog sigma.
    743742#p #prog
    744743letin sigma ≝
    745   (λi.
    746     let fn_in ≝ prog_if_of_function ?? prog i in
     744  (λi : Σi.is_internal_function_of_program … prog i.
     745    let fn_in ≝ if_of_function … i in
    747746    \snd (linearise_int_fun … fn_in))
    748747%{sigma}
    749 #i >(prog_if_of_function_transform … i) [2: % ]
     748#i #prf >(prog_if_of_function_transform … i) [2: % ]
    750749normalize nodelta
    751750cases (linearise_int_fun ???) * #fn_out #sigma_loc
Note: See TracChangeset for help on using the changeset viewer.