Theorem

dsdp_3party_rsteps

Section dsdp_3party_rsteps

Type Theorem

Proof Lines 6

Theorem dsdp_3party_rsteps : exists final traces, rsteps procs3 final traces /\ all_terminated (tval final) /\ all_nonfail (tval final).

Main theorem: the 3-party protocol admits an rsteps reduction

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

No lemmas in the stats use this lemma.

Loading source code...