sead - Linear Logic Proof Explorer

	Linear Logic Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > LLPE Home > Th. List > sead		Structured version

Theorem sead 231

Description: Distribution of sending over ⊕.

**Assertion**
Ref	Expression
sead	⊦ (([x ≪ y] 1 ⊗ (𝜑 ⊕ 𝜓)) ⧟ (([x ≪ y] 1 ⊗ 𝜑) ⊕ ([x ≪ y] 1 ⊗ 𝜓)))

**Proof of Theorem sead**
Step	Hyp	Ref	Expression

Colors of variables: wff var nilad

Syntax hints: ⧟ wlb 55 1wone 103 ⊗ wmc 105 ⊕ wad 131 nvar 203 [wse 204

WARNING: This theorem has an incomplete proof.

This theorem is referenced by: (None)