Helper

step_proc_trace_indep

Section interp_sound_section

Type Lemma

Proof Lines 5

Lemma step_proc_trace_indep (ps : seq (proc data)) tr1 tr2 i : (smc_interpreter.step ps tr1 i).1.1 = (smc_interpreter.step ps tr2 i).1.1.

The process component of step is independent of the trace argument.

This lemma does not use any other lemmas from the stats.

No lemmas in the stats use this lemma.

Loading source code...