Helper

step_progress_trace_indep

Section interp_sound_section

Type Lemma

Proof Lines 5

Lemma step_progress_trace_indep (ps : seq (proc data)) tr1 tr2 i : (smc_interpreter.step ps tr1 i).2 = (smc_interpreter.step ps tr2 i).2.

The progress flag 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...