Changeset 2727


Ignore:
Timestamp:
Feb 25, 2013, 6:43:44 PM (6 years ago)
Author:
campbell
Message:

Remove a couple of redundant hypotheses.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2726 r2727  
    288288          destruct >Etrace
    289289          @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    290           [1,3: whd in match (cs_classify ??); >CL %
    291           |2,4: whd in match (cs_classify ??); <(rel_classify … REL) >CL %
     290          [ whd in match (cs_classify ??); >CL %
     291          | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
    292292          | @INV
    293293          | assumption
     
    533533          destruct >Etrace
    534534          @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g'))
    535           [1,3: whd in match (cs_classify ??); >CL %
    536           |2,4: whd in match (cs_classify ??); <(rel_classify … REL) >CL %
     535          [ whd in match (cs_classify ??); >CL %
     536          | whd in match (cs_classify ??); <(rel_classify … REL) >CL %
    537537          | @INV
    538538          | assumption
  • src/common/Measurable.ma

    r2725 r2727  
    221221
    222222lemma build_call_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem',H,H'.
    223   cs_classify C s = cl_call →
    224   cs_classify C' s' = cl_call →
    225223  all ? (λstr. normal_state C' (\fst str)) trace' →
    226224  intensional_trace_of_trace C (cs_callee C s H::callstack) rem = intensional_trace_of_trace C' (cs_callee C s H::callstack) rem' →
     
    228226  let trace ≝ 〈s',tr〉::trace' in
    229227  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
    230 #C #C' #callstack #s #s' #tr #trace #rem #rem' #H #H' #CL #CL' #NORMAL
     228#C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL
    231229whd in ⊢ (? → ? → %);
    232230whd in ⊢ (? → ? → ??%%); normalize nodelta
    233231@generalize_callee
    234232@generalize_callee
    235 >CL in H ⊢ %; * >CL' in H' ⊢ %; * normalize nodelta #calleef #calleef' #E #CALLEE <CALLEE
     233cases (cs_classify C s) in CL ⊢ %; * cases (cs_classify C' s') in CL' ⊢ %; *
     234normalize nodelta #calleef #calleef' #E #CALLEE <CALLEE
    236235cases (intensional_trace_of_trace ?? rem) in E ⊢ %; #cs_rem #ev_rem normalize nodelta
    237236>(int_trace_append_normal … NORMAL) normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.