Axiom ax-lock1 229

Description: Reading from a channel with nothing writing to it causes a deadlock.

Assertion

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

Detailed syntax breakdown of Axiom ax-lock1

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

This axiom is referenced by: (None)