Theorem rech 232

Description: Writing to a channel being read in multiple places causes a nondeterministic choice.

Assertion

Ref	Expression
rech	⊦ (([x ≪ x] 𝜑 ⊗ ([x ≫ x] 𝜓 ⊗ [x ≫ x] 𝜒)) ⧟ (𝜑 ⊗ (𝜓 ⊕ 𝜒)))

Proof of Theorem rech

Step	Hyp	Ref	Expression

Syntax hints:   ⧟ wlb 55   ⊗ wmc 105   ⊕ wad 131  nvar 203  [wse 204  [wre 205

 WARNING: This theorem has an incomplete proof.

This theorem is referenced by: (None)