es48 (by A. Nicolosi)


Per il Teorema di Church-Rosser, se i due termin fossero b-convertibili, esisterebbe un altro
 \-termine L al quale entrambi si b-riducono. 
Ma (\x.xx)(\x.xx) non si riduce ad altro che a se stesso: pertanto deve accadere che: 
(\x.xx)(\x.xxx) ->> (\x.xx)(\x.xx).     (*)
Dopo il primo passo di b-riduzione, (\x.xx)(\x.xxx) si riduce a (\x.xxx)(\x.xxx). 
Sopra è stato provato che tale termine si riduce solo a termini del tipo p...p, dove p == (\x.xxx). 
Pertanto non potrà mai accadere che da (\x.xx)(\x.xxx) si pervenga a (\x.xx)(\x.xx), per cui la (*) è assurda. 
L'assurdo deriva dall'aver supposto che i due termini fossero b-convertibili.