Lines Matching defs:su
380 permette la quantificazione ristretta su tutte le variabili di una sequenza di variabili
714 mnemonici per variabili (ad esempio \ml{S} varia su insiemi e \ml{o}
715 varia su output)\footnote{Le costanti dichiarate nelle nuove teorie possono
887 \paragraph {Mappare funzioni su una coppia}
890 applicate in modo componente ({\small\verb+##+}, infisso) su una coppia di tipo
921 \paragraph {Relazioni benfondate su coppie}
1267 valori $\alpha$ indefiniti su \holtxt{NONE}.
1270 definizione di funzioni ricorsive primitive su valori option.
1300 Un altre funzione utile mappa una funzione su un'option:
1310 \holtxt{SOME} per quell'argomento del costruttore, ed � indefinita su
1540 definizioni ricorsive primitive su un range di tipi, non solo sui
1945 informazioni su come installare nuovi suffissi di un carattere, si consulti la
1953 � costruito come un quoziente su coppie di numeri naturali. E' definita
2143 2005\footnote{La teoria attuale sussume teorie di parola precedenti -- si � evoluta da uno sviluppo basato su una costruzione di classi di equivalenza. La teoria di parola di Wai Wong, che era basata sulla teoria \ml{rich\_list} di Paul Curzon, non � pi� distribuita con HOL. I principali vantaggi della teoria attuale sono che c'� un'unica teoria per tutte le dimensioni di parole e che non sono richiesti effetti secondari della lunghezza delle parole.}
2210 un meccanismo per la valutazione efficiente di alcune operazioni su parole attraverso la teoria
2295 si opera su numeri naturali, alcune delle versioni complemento
2418 \paragraph{Elenco di operazioni su vettori di bit}
2597 di dimostrazione principale usato per ragionare su operazioni che manipolano liste. Il
2723 Ci sono delle funzioni per mappare una funzione $f : \alpha \to \beta$ su
2739 \paragraph {Predicati su liste}
2768 Il predicato \holtxt{ALL\_DISTINCT} vale su una lista solo nel caso in cui
2864 sono non specificate su liste vuote.
3221 definito (\ml{F}, o \emph{false}) su percorsi infiniti, mentre il
3222 valore di \ml{last} su tali percorsi non � specificato:
3288 definizioni per operare su stringhe.
3330 Per esempio, \holtxt{NIL} e \holtxt{CONS} su liste hanno
3387 \index{espressioni case!su stringhe}
3472 L'insieme universale, \holtxt{UNIV}, su un tipo � la funzione caratteristica che � sempre vera per elementi di quel tipo.
3553 \paragraph{Funzioni su insiemi}
3554 L'immagine di una funzione $f :\alpha \to \beta$ su
3612 Come menzionato, le operazioni su insiemi si applicano sia a insiemi finiti che
3628 \theoryimp{pred\_set}, le propriet� delle operazioni su insiemi finiti devono
3661 \paragraph{Funzioni ricorsive su insiemi}
3663 Le funzioni ricorsive su insiemi possono essere definite dalla ricorsione
3691 definizione della sommatoria dei risultati di una funzione su un insieme finito di
3717 definita come un predicato su una relazione.
3990 su bag si riducono entrambe a un calcolo aritmetico sui loro
4045 Prendere l'immagina di una funzione su un multinsieme per ottenere un nuovo multinsieme
4113 \paragraph{Funzioni ricorsive su multinsiemi}
4115 Le funzioni ricorsive su multinsiemi possono essere definite per ricorsione
4760 Alcuni teoremi per ragionare su \holtxt{LEAST} si possono trovare nella
4780 Una teoria di polinomi su $\mathbb{R}$, che fornisce
4781 una collezione di operazioni su polinomi, e teoremi che li riguardano.