Helper

interp1E

Section interp_sound_section

Type Lemma

Proof Lines 14

Lemma interp1E h ps traces : size traces = size ps -> interp1 ps h = (interp h ps traces).1.

interp1 computes the same processes as interp

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

No lemmas in the stats use this lemma.

Loading source code...