Axiom ax-lock2 230

Description: Writing to a channel with nothing reading from it causes a deadlock.

Assertion

Ref	Expression
ax-lock2	⊦ (νx? [x ≪ a] 1 ⊸ 0)

Detailed syntax breakdown of Axiom ax-lock2

Step	Hyp	Ref	Expression
1		wone 103	. . . . 5 wff 1
2		vx	. . . . . 6 var x
3	2	nvar 203	. . . . 5 nilad x
4		va	. . . . . 6 var a
5	4	nvar 203	. . . . 5 nilad a
6	1, 3, 5	wse 204	. . . 4 wff [x ≪ a] 1
7	6	wne 48	. . 3 wff ? [x ≪ a] 1
8	7, 2	wnu 206	. 2 wff νx? [x ≪ a] 1
9		wzero 129	. 2 wff 0
10	8, 9	wli 61	1 wff (νx? [x ≪ a] 1 ⊸ 0)

This axiom is referenced by: (None)