Definition df-nab 267

Description: Using a nilad abstraction is the same as running the associated process 𝜑 and using its "return value" instead. Since the input to all other operators can be modeled using ≪, this is enough to fully describe nilad abstractions.

Unlike most defined operators, the nilad abstraction cannot directly be expanded to primitive symbols. Despite this, it is always possible to mechanically eliminate nilads from any expression that contains them by simply moving the process 𝜑 to before the variable y is used.

Assertion

Ref	Expression
df-nab	⊦ ([x ≪ {y | 𝜑}] 𝜓 ⧟ (𝜑 ⊗ [y ≫ a] [x ≪ a] 𝜓))

Distinct variable groups:   𝜑,a   𝜓,a   a,x   a,y

Detailed syntax breakdown of Definition df-nab

Step	Hyp	Ref	Expression
1		wps	. . 3 wff 𝜓
2		vx	. . . 4 var x
3	2	nvar 203	. . 3 nilad x
4		wph	. . . 4 wff 𝜑
5		vy	. . . 4 var y
6	4, 5	nnab 266	. . 3 nilad {y | 𝜑}
7	1, 3, 6	wse 204	. 2 wff [x ≪ {y | 𝜑}] 𝜓
8		va	. . . . . 6 var a
9	8	nvar 203	. . . . 5 nilad a
10	1, 3, 9	wse 204	. . . 4 wff [x ≪ a] 𝜓
11	5	nvar 203	. . . 4 nilad y
12	10, 8, 11	wre 205	. . 3 wff [y ≫ a] [x ≪ a] 𝜓
13	4, 12	wmc 105	. 2 wff (𝜑 ⊗ [y ≫ a] [x ≪ a] 𝜓)
14	7, 13	wlb 55	1 wff ([x ≪ {y | 𝜑}] 𝜓 ⧟ (𝜑 ⊗ [y ≫ a] [x ≪ a] 𝜓))

This definition is referenced by: (None)