Lines Matching defs:le
22 autosufficiente e cos� include le risposte agli esercizi fissati al
65 passo � di definire le riduzioni che i combinatori possono subire. Ci
98 funzione \ml{xHol\_reln}. In aggiunta a una quotation che specifica le
145 $\lambda$-calcolo, le macchine di Turing, e tutti gli altri modelli standard
396 & & & r}\] dove le linee tratteggiate indicano che questi passi (da $x$ a $p$,
498 noi gli diciamo quali sono le regole che governano \con{RTC}:
539 Ora possiamo applicare le nostre ipotesi d'induzione (assunzione 3) per completare
544 di cui abbiamo bisogno di fornire a \texttt{PROVE\_TAC} sono le regole per \con{RTC}:
801 Ora possiamo impostare un'elegante sintassi per le chiusure riflessiva e
804 anche come, definendo le due relazioni, dobbiamo usare il
849 \subsection{Dimostrare che le \con{RTC} sono le stesse}
952 dividere le congiunzioni ed inserire un ramo \texttt{THENL}.
998 Tutto ci� che dobbiamo fare � ``cucire insieme'' le due transizioni di sopra
1016 possiamo semplicemente fondere le liste di teoremi passate ad entrambe le invocazioni, distribuire
1149 le caratterizzazioni automaticamente:
1159 la disgiunzione [disjointness ndt] dei costruttori ed elimina le ovvie impossibilit�.
1337 le composizioni da destra a sinistra, prima semplificheremo con il
1339 nelle assunzioni, eliminando le disgiunzioni e gli esistenziali mentre andiamo
1351 questo, dovremmo fare alcune riscritture per essere sicuri che le uguaglianze nelle
1550 Se necessario, le risposte ai primi tre esercizi si possono trovare