Helper

dsdp_n4_no_fail

Section dsdp_n4_idealized_duality

Type Lemma

Proof Lines 1

Lemma dsdp_n4_no_fail traces : all_nonfail (interp [> dsdp_n4_saprocs] dsdp_n4_procs traces).1.

4-party no-fail: after interpretation, no process is Fail

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

No lemmas in the stats use this lemma.

Loading source code...