Helper

dsdp_n4_builder_correct

File dumas2017dual/dsdp/dsdp_pismc.v

Section dsdp_n4_idealized_duality

Type Lemma

Proof Lines 1

Signature

Lemma dsdp_n4_builder_correct : @dsdp_n_procs AHE ek4 2 [:: @Ordinal 3 0 isT; @Ordinal 3 1 isT; @Ordinal 3 2 isT] dk0 v0 u4 r4_3 rand4_3 dk_relay_4 v_relay_4 r1_relay_4 r2_relay_4 = erase_aprocs [aprocs palice_4; pfirst_4; pinter_4; plast_4].

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