Ignore:
Timestamp:
Jul 2, 2012, 4:12:12 PM (8 years ago)
Author:
campbell
Message:

Cost labelling doesn't affect interaction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/SmallstepExec.ma

    r2118 r2145  
    112112] qed.
    113113
     114lemma extract_interact : ∀O,I,TS,ge,s,o,k.
     115  exec_inf_aux O I TS ge (step … ge s) = e_interact … o k →
     116  ∃k'. step … ge s = Interact … o k' ∧ k = (λv. exec_inf_aux ??? ge (k' v)).
     117#O #I #TS #ge #s #o #k >exec_inf_aux_unfold
     118cases (step … s)
     119[ #o' #k' normalize #E destruct %{k'} /2/
     120| * #x #y normalize cases (is_final ?????) normalize
     121  #X try #Y destruct
     122| normalize #m #E destruct
     123] qed.
     124
    114125lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
    115126  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
Note: See TracChangeset for help on using the changeset viewer.