Helper

pbob_is_first

Section smc_dsdp_program

Type Lemma

Proof Lines 1

Lemma pbob_is_first dk' v2' rb1' rb2' : pbob dk' v2' rb1' rb2' = DParty_first bob_idx charlie_idx dk' v2' rb1' rb2'.

Cross-equality: existing 3-party definitions are instances of templates

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

No lemmas in the stats use this lemma.

Loading source code...