Helper

S_E

Section dotp2

Type Lemma

Proof Lines 5

Lemma S_E : S = Dotp2_rv VS US \+ VU1.

S expressed as dot product: S = (V2,V3)·(U2,U3) + V1*U1. This is the DSDP constraint s = u2*v2 + u3*v3 + u1*v1 in RV form.

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

No lemmas in the stats use this lemma.

Loading source code...