Definition df-la 280

Description: Definition of lambda abstraction. The lambda exposes a "handle" f which reads a temporary communication channel a. The resulting function's input x and output Y are passed along a. The ! exponential creates infinite instances of this function "provider", which can all run in parallel. Compare with df-fv 282 to see how this function is called.

Assertion

Ref	Expression
df-la	⊦ λxY = {νf | ! [f ≫ a] [a ≫ x] [a ≪ Y] 1}

Distinct variable groups:   a,f,x   f,Y,a

Detailed syntax breakdown of Definition df-la

Step	Hyp	Ref	Expression
1		vx	. . 3 var x
2		ny	. . 3 nilad Y
3	1, 2	nla 279	. 2 nilad λxY
4		wone 103	. . . . . . 7 wff 1
5		va	. . . . . . . 8 var a
6	5	nvar 203	. . . . . . 7 nilad a
7	4, 6, 2	wse 204	. . . . . 6 wff [a ≪ Y] 1
8	7, 1, 6	wre 205	. . . . 5 wff [a ≫ x] [a ≪ Y] 1
9		vf	. . . . . 6 var f
10	9	nvar 203	. . . . 5 nilad f
11	8, 5, 10	wre 205	. . . 4 wff [f ≫ a] [a ≫ x] [a ≪ Y] 1
12	11	wpe 148	. . 3 wff ! [f ≫ a] [a ≫ x] [a ≪ Y] 1
13	12, 9	nvnab 271	. 2 nilad {νf | ! [f ≫ a] [a ≫ x] [a ≪ Y] 1}
14	3, 13	weq 246	1 wff λxY = {νf | ! [f ≫ a] [a ≫ x] [a ≪ Y] 1}

This definition is referenced by: (None)