Helper

palice_n_erase

File dumas2017dual/dsdp/dsdp_pismc.v

Section dsdp_n_rsteps

Type Lemma

Proof Lines 16

Signature

Lemma palice_n_erase relays dk' v0' u' r' rand_a' : erase (@palice_n AHE ek n_relay relays dk' v0' u' r' rand_a') = pInit (priv_key dk') (pInit (d v0') (foldr (fun (fi : 'I_n_relay.+1 * nat) (cont : proc data) => alice_erase_body u' r' rand_a' fi.1 fi.2 cont) (alice_erase_tail dk' v0' u' r') (zip relays (iota 0 (size relays))))).

Description

Alice's erased program decomposes via erase_sproc_iter

Uses (0)

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

Used By (0)

No lemmas in the stats use this lemma.

Coq Source Code

View on GitHub

Loading source code...

← Back to Stats