Helper

dsdp_n4_terminates

Section dsdp_n4_idealized_duality

Type Lemma

Proof Lines 1

Lemma dsdp_n4_terminates traces : all_terminated (interp [> dsdp_n4_saprocs] dsdp_n4_procs traces).1.

4-party termination: after interpretation, all processes are terminal

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

No lemmas in the stats use this lemma.

Loading source code...