Helper

size_dsdp_n_procs

File dumas2017dual/dsdp/dsdp_pismc.v

Section dsdp_n_rsteps

Type Lemma

Proof Lines 1

Signature

Lemma size_dsdp_n_procs relays dk0 v0 u0 r0 rand_a dk_relay v_relay r1_relay r2_relay : size (@dsdp_n_procs AHE ek n_relay relays dk0 v0 u0 r0 rand_a dk_relay v_relay r1_relay r2_relay) = (size relays).+1.

Description

* ** Size of dsdp_n_procs

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