Tutorial dei Numeri Naturali

[hubabuba]

Salve avrei bisongo di capire il funzionamento di un programma.
Scrivo in Hol Light il tutorial dei numeri naturali e applico il seguente:

1 ) #let nat_RECURSION = new_axiom
`!e:A f.
?fn. fn 0 = e /\
(!n. fn (S n) = f (fn n) n)`;;
2) # let DOUBLE_EXISTS = ISPECL [`0`; `\p (n:nat). S (S p)`] nat_RECURSION;;
val ( DOUBLE_EXISTS ) : thm =
|- ?fn. fn 0 = 0 /\ (!n. fn (S n) = (\p n. S (S p)) (fn n) n)
3) # let DOUBLE_EXISTS = REWRITE_RULE [] DOUBLE_EXISTS;;
val ( DOUBLE_EXISTS ) : thm =
|- ?fn. fn 0 = 0 /\ (!n. fn (S n) = S (S (fn n))
Dove S è il succesore.
Per capire il funzionamento devo capire i passagi che ho messo in rosso.
1) Nel punto uno li dove c'è scritto con rosso significa che f viene ripettuto n volte: f(f(f...(f(fn n))))
2) Nel secondo passaggio devo sostituire il valore di f con `\p.S( S p)`. E questo si fa n volte.
3) Nel terzo passo non capisco come viene dato quel risultato. Praticamente, come si fa la sostituzione per arrivare qua. !n. fn (S n) = S (S (fn n).
Chi mi può dare una mano. Grazie

[hamming_burst]

Ciao,
potresti utilizzare i tag [code] e ricopiarlo di nuovo il post, inve che risciverlo.
Non capisco se tipo con /\ ti riferisci all'and \(\wedge\).
Poi vediamo cosa si può fare

[hubabuba]

∧ con questo simbolo è denotato and.

[hamming_burst]

Mi diresti che significato hanno l'applicazione di ! e ?