Definition df-ss 290

Description: Definition of the S combinator.

Assertion

Ref	Expression
df-ss	⊦ S = λaλbλc((b' a)' (c' a))

Distinct variable group:   a,b,c

Detailed syntax breakdown of Definition df-ss

Step	Hyp	Ref	Expression
1		nss 286	. 2 nilad S
2		va	. . 3 var a
3		vb	. . . 4 var b
4		vc	. . . . 5 var c
5	3	nvar 203	. . . . . . 7 nilad b
6	2	nvar 203	. . . . . . 7 nilad a
7	5, 6	nfv 281	. . . . . 6 nilad (b' a)
8	4	nvar 203	. . . . . . 7 nilad c
9	8, 6	nfv 281	. . . . . 6 nilad (c' a)
10	7, 9	nfv 281	. . . . 5 nilad ((b' a)' (c' a))
11	4, 10	nla 279	. . . 4 nilad λc((b' a)' (c' a))
12	3, 11	nla 279	. . 3 nilad λbλc((b' a)' (c' a))
13	2, 12	nla 279	. 2 nilad λaλbλc((b' a)' (c' a))
14	1, 13	weq 246	1 wff S = λaλbλc((b' a)' (c' a))

This definition is referenced by: (None)