es73 (By A. Nicolosi)

La dimostrazione si basa sul teorema di Standardizzazione: 
Se un \-termine ha forma normale, si perverrą a tale 
forma seguendo la strategia di riduzione leftmost-outermost.
In tutti i \-termini ottenibili per b-riduzione dal \-termine di partenza, 
c'č solo il b-redex (\x.xxx)(\x.xxx); dunque tutte le strategie sono 
equivalenti, e dovrebbero portare ad una forma normale. Ma poichč tale 
strategia riduce (\x.xxx)(\x.xxx) -> (\x.xxx)(\x.xxx)(\x.xxx), essa introduce 
sempre un b-redex e non terminerą mai di b-ridurre: pertanto (\x.xxx)(\x.xxx) 
non č normalizzabile. 
Resta da provare che nei \-termini ottenibili per b-riduziuone dal \-termine 
di partenza c'č sempre uno ed un solo b-redex. Proviamo per induzione che, 
posto p == (\x.xxx), dopo n b-riduzioni otteniamo p...p (n+2 volte). 

Caso Base: n = 0 
Dopo 0 b-riduzioni siamo all'inizio dove il \-termine e' 
(\x.xxx)(\x.xxx) == pp.

Passo Induttivo: 
Hp: Dopo n b-riduzioni otteniamo pp...p (n+2 volte). 
Ts: Dopo n+1 b-riduzioni otteniamo (pp)p...p (n+3 volte). 
Dim. 
L'unico b-redex in pp...p e' l'applicazione pp all'inizio:b-riducendola otteniamo (pp)p...p.
Cio' prova che i \-termini che otteniamo sono tutti della forma pp...p: 
e' chiaro che in tali \-termini c'e' sempre uno ed un solo b-redex, cioe' pp.