Lines Matching defs:la
25 di supporto, come la documentazione. Alcune librerie forniscono semplicemente
31 \ML{} nominate seguendo la convenzione che la libreria \emph{x}
71 e dei termini attraverso la struttura \ml{Parse}.
76 del parser. Inoltre, la struttura del parser � esposta cos� che
99 di tipo) pu� essere ispezionata usando la funzione \ml{type\_grammar}.
124 di tipo, e manipolando la grammatica direttamente.}
129 Gli infissi possono essere introdotti con la funzione \ml{add\_infix\_type}.
139 Questo � fatto con la funzione \ML{} \ml{type\_abbrev}:
157 Per maggiori informazioni, si veda la voce \ml{type\_abbrev} in \REFERENCE.
163 la sintassi concreta per le formalizzazioni. Di solito, la grammatica \HOL{} viene
177 Di solito questa grammatica � la grammatica globale di default, ma gli utenti possono
182 serie di token. Per maggiori informazioni sul lexing, si veda la Sezione~\ref{HOL-lex}.
194 (un antiquote, si veda la Sezione~\ref{sec:quotation-antiquotation}); %
204 la Sezione~\ref{sec:parseprint-type-constraints}). A questo stadio della
221 La grammatica standard include una regola che associa la speciale
224 risolto come la costante \holtxt{bool\dol{}COND}.
226 Se si usa la sintassi di ``quotation'' con un dollaro nudo,%
240 \holtxt{\holquote{\$+~x}}, che genera la sintassi astratta
257 con la funzione
287 ed avere la stringa \holtxt{SUC} trattata come un numero nel
288 contesto dell'astrazione data, piuttosto che come la costante
308 Quando la risoluzione dei nomi determina che un identificatore dovrebbe essere trattato
323 anche la Sezione~\ref{sec:parser:syntactic-patterns} per maggiori informazioni sui
329 la funzione \ml{mk\_comb} %
335 identificatori che digita. (Si veda la Sezione~\ref{sec:parser:type-inference}
343 Quando � stato completato il controllo di tipo di un \ml{Preterm}, la conversione finale da
370 \ml{...Theory.sml} che falliranno di compilare, anche se la chiamata a
375 la sintassi unicode per la costante sottostante.
378 mostrare la loro sintassi, e confidano nel fatto che anche ognuno degli utenti delle loro
380 gli utenti vogliono mantenere la retro-compatibilit� con la pura sintassi
382 questo, possono creare una versione Unicode della sintassi con la
383 funzione \ml{Unicode.unicode\_version}. Quindi, quando la variabile
384 di traccia \ml{"Unicode"} � $0$, la sintassi ASCII sar� usata per
385 il parsing e la stampa. Se la traccia � impostata a $1$, allora funzioner�
386 anche la sintassi unicode nel parse, e il pretty-priunter
387 la preferir� quando i termini sono stampati.
391 \texttt{/\bs} con la chiamata
395 (In questo contesto, � stata aperta la struttura \ml{Unicode},
403 nome di una costante, allora, con la variabili di traccia abilitata, la stringa
406 creare una nuova regola che mappa allo stesso nome, ma con la stringa \ml{u}
418 i token si dividono quando la classe di caratteri cambia. Cos�, nella
439 mappe, una per il parsing, e una per la stampa. La mappa di parsing � da
447 il resto del termine dato. Se la lista risultante contiene pi� di
451 Il caso d'uso pi� comune per la mappa di overload � di avere nomi mappati a
453 mappare la stringa \ml{"+"} alla nozione rilevante di addizione, ognuna delle
456 possibile mappare a istanze di costanti con specifici tipi. Cos�, la
463 esempio, in \theoryimp{boolTheory} e nei suoi discendenti, la stringa
481 \holtxt{\td(x~=~y)}. Meglio, bench� questa sar� la struttura
493 non costruisca un valore \ml{Absyn}, questo processo inverte la fase del parsing
495 secondo la parte di sintassi concreta della grammatica data.)
498 la stampa deve essere in grado di ricondurre una complicata struttura di termine a
508 specifiche, ha la precedenza il pattern aggiunto
515 la \ml{x} e la \ml{y} in questo esempio erano legate da un'astrazione),
519 ``pi� grandi'', che coprono pi� di un termine hanno la precedenza. La difficolt�
529 macro � impostata la mappa di overload contiene gi� un mapping dalla
531 accade con ogni definizione di costante). Ma dopo la chiamata
532 che stabilisce il nuovo pattern per \holtxt{IS\_PREFIX}, la
534 ripetere la chiamata
538 Piuttosto (supponendo che \holtxt{isPREFIX} sia di fatto la forma
539 di stampa preferita), la chiamata deve essere
552 \holtxt{X:bool} vincola la variabile \holtxt{X} ad avere il tipo
604 significa che la costante \holtxt{=} ha tipo \holtxt{xty -> bool -> bool},
617 Di solito, questa assegnazione fa la cosa giusta. Tuttavia, a volte, il
619 di tipo ai sotto termini rilevanti. Per situazioni complicate, si pu� assegnare la
623 delle variabili di tipo per proprio conto, si pu� impostare la variabile globale
636 denota la negazione booleana nella teoria iniziale di \HOL, e denota anche
638 \ml{real}. Se carichiamo la teoria \ml{integer}
640 sistema ci informer� che � stata eseguita la risoluzione dell'overloading.
681 seconda quotation; la sua prima occorrenza � la negazione booleana, mentre
702 Cos� la sintassi concreta \verb+!v. M+ � rappresentata
724 \begin{Large}\holtxt{,}\end{Large} (la virgola\footnote{Quando
753 Questo potrebbe inizialmente apparire la stessa cosa di quanto accade con la normale applicazione di funzione dove il simbolo alla sinistra semplicemente non ha alcuna fixity: $f$ in $f(x)$ non si comporta forse come un prefisso?
754 Di fatto tuttavia, in un termine come $f(x)$, dove $f$ e $x$ non hanno fixity, la sintassi � trattata come se ci fosse una invisibile applicazione di funzione infissa tra i due token: $f\cdot{}x$.
757 Un esempio di questo � \verb+~+, la negazione logica.
766 poich� la precedenza di \verb+~+ � pi� bassa di quella dell'applicazione di funzione.
772 Dall'altro lato, la sintassi \holtxt{univ} per l'insieme universale (si veda la Sezione~\ref{sec:theory-of-sets}\index{universal set}) � un esempio di un operatore prefisso che lega pi� strettamente dell'applicazione.
821 usare la fase grammatica/sintassi per parsing per fare questo. Piuttosto, si
836 \ml{term\_grammar()}). Con la sola \ml{arithmeticTheory}
864 Dal momento che ci deve essere un termine ``a penzoloni'' sulla destra, la
867 la sintassi desiderata �:
880 \item[Sintassi mix-fix sintassi per la sostituzione di termini:]
886 denotando la sostituzione di $t_1$ per $t_2$ in $t_3$, magari
888 come ci dovesse essere un altro \ml{Prefix}, ma la scelta delle
890 in conflitto con la sintassi concreta per i letterali lista se si facesse questo.
892 \ml{CloseFix}, la nuova sintassi deve essere della stessa classe. Questo � abbastanza semplice
893 da fare: impostiamo la sintassi
899 corretto\footnote{Si noti che facendo la stessa cosa per
945 la stampa rimuovendo il nome dato dalla ``mappa di overload'' descritta
948 teorie discendenti da quella attuale. Si veda la voce \ml{hide} in
977 \subsubsection{Adattare la profondit� del pretty-print}
980 La seguente reference \ML{} pu� essere usata per impostare la profondit� massima
990 \index{profondit� di stampa di default, per la logica HOL@profondit� di stampa di default, per la logica \HOL{}|(}
1010 \index{profondit� di stampa di default, per la logica HOL@profondit� di stampa di default, per la logica \HOL{}|)}
1053 argomento \ml{`p /\bs{} q`}. Analogamente, la seconda espressione si espande
1060 rappresentazione di $\lambda$, ma anche nella sintassi per la congiunzione e
1061 la disgiunzione.
1070 modo in cui in \ML{} la sintassi delle stringhe tratta il backslash.) Cos�:
1084 includendo un esempio che accade quando non si segue la regola
1151 \noindent Le quotation sono polimorfiche, e la variabile di tipo di una
1197 cambiamento porta la sintassi delle logica pi� vicina a quella dell'SML e
1208 a sinistra. Questo porta il parser di \HOL{} in linea con la pratica
1215 rimossa. Cos� la stringa \holquote{\condexp} ora deve essere
1255 Un'abbreviazione per \ml{set\_goal} � la funzione \ml{g}: essa
1274 l'applicazione delle tattiche al goal attuale � fatto con la funzione
1296 nel goalstack, sono usate la funzione \ml{backup} e la sua abbreviazione
1302 la funzione \ml{restart}. Ovviamente, � anche importante liberarsi
1308 Ogni tentativo di dimostrazione ha la sua \emph{lista-di-annullamento} degli stati
1311 usare la funzione \ml{set\_backup}. Se la dimensione della lista di
1312 backup � impostata essere pi� piccola di quanto sia attualmente, la lista di annullamente sar�
1331 i subgoal in cima al goalstack corrente, mentre la seconda da una
1343 continua ad esistere (e anche la sua lista-di-annullamento): il suo compito principale ora � quello di
1358 Spesso vogliamo spostare la nostra attenzione a un differente goal nella dimostrazione
1400 teoremi di iniettivit� e distinzione, insieme con la definizione di costante
1427 che la tattica \ml{Cases\_on} � pi� generale di \ml{Cases}, ma
1453 si esegue l'induzione su $n$, � permesso assumere che la propriet� valga per
1460 \item [\ml{measureInduct\_on}] prende una quotation, e la suddivide
1495 La regola d'inferenza \texttt{PROVE} (e la tattica corrispondente
1498 \ml{METIS} eseguono la stessa funzionalit� ma usano un metodo di dimostrazione
1503 (e la tattica corrispondente \texttt{DECIDE\_TAC}) applica una procedura
1532 (accessibile attraverso la funzione \ml{srw\_ss}) che viene aggiornato ogni volta che viene caricato
1544 simpset per la logica pura, le somme, le coppie e il tipo \ml{option} �
1563 $(A,g)$, � creato un nuovo subgoal $(A,M)$ e ad esso � applicata la tattica $tac$.
1565 alle assunzioni del goal originale; cos� la dimostrazione procede con
1567 se la de-costruzione di $\ \vdash M$ espone delle disgiunzioni.) Cos�
1574 contraddizione assumendo la negazione del goal e spostando la
1592 \index{metodo model elimination per la logica del primo ordine}
1608 \texttt{meson} possono richiedere anche molto tempo per raggiungere la profondit� massima.
1637 \index{metodo di risoluzione per la logica del primo ordine}
1656 la ricerca della dimostrazione non ha successo.
1658 La famiglia \texttt{metisLib} di strumenti di dimostrazione implementano la risoluzione
1659 ordinata e il calcolo di paramodulazione ordinata per la logica del primo ordine,
1669 raccomandato come un cavallo di battaglia di scopo generale durante la dimostrazione di teoremi
1675 a termini, rimpiazzando le istanze di $l$ nel termine con $r$. Cos�, la
1711 valore possibile per la variabile quantificata \holtxt{x} era il valore
1721 Per esempio, la riscrittura \ml{arithmeticTheory.LEFT\_ADD\_DISTRIB}, che
1752 \ml{SIMP\_TAC} � la tattica di semplificazione pi� semplice: essa tenta di
1785 regola di riscrittura addizionale, e ha sostituito la \holtxt{x} di \holtxt{P x}
1789 un'assunzione \holtxt{\~{}P} sar� trattata come la riscrittura \holtxt{|- P = F}.
1795 La tattica \ml{FULL\_SIMP\_TAC} semplifica non solo la conclusione di
1799 assunzione � ri-aggiunta alla lista di assunzioni del goal con la
1808 del goal. Tipicamente quindi, la prima assunzione da semplificare
1833 In questo esempio, l'assunzione \holtxt{x = 4} ha fatto s� che la \holtxt{x}
1836 apparse nell'ordine opposto, solo la \holtxt{x} del goal sarebbe
1899 Piuttosto la sua operazione si fonda sempre sul \simpset{} incorporato
1902 stesso modo delle altre tattiche di semplificazione. Infine, la
1907 Per esempio, per includere la procedura di decisione Presburger, si potrebbe
1917 La tattica \ml{SRW\_TAC} esegue la stessa combinazione di semplificazione e
1919 due tattiche risiedono nel fatto che la seconda pu� essere inefficiente quando
1925 di riscritture non utilizzate non � mai un problema: la presenza di riscritture che
1926 fanno la cosa sbagliata pu� essere causa di maggiore irritazione.
1947 nella Sezione~\ref{sec:advanced-simplifier}; la generazione di regole
2029 \ml{std\_ss} aggiungendo la capacit� di decidere formule dell'aritmetica
2046 Si noti che la sottrazione su numeri naturali funziona in modi che possono
2047 sembrare non intuitivi. In particolare, la normalizzazione del coefficiente non pu�
2093 la Sezione~\ref{sec:computeLib} di sotto); \ml{computeLib} � pi�
2113 dinamicamente. In questo modo, la trasparenza referenziale � deliberatamente
2115 \ml{SIMP\_CONV~bool\_ss} � la stessa routine di semplificazione ovunque
2146 Gli utenti possono aumentare il \simpset{} stateful da soli con la funzione
2158 aggiunti nelle sessioni future quando la teoria � ricaricata.
2199 selezionare la funzione ``filtro'' di default per convertire teoremi in
2206 \simpset{} per la teoria dei numeri naturali si trovano in
2276 cercando per dei \emph{match}~(si veda la Sezione~\ref{sec:simp-homatch} di sotto)
2284 $t_0$ pu� creare la nuova equazione \[
2295 include due riscritture con esattamente gli stessi lati sinistri. la
2303 congruenza}~(una caratteristica avanzata, si veda la Sezione~\ref{sec:simp-congruences}
2309 la Sezione~\ref{sec:simp-embedding-code}). Se la fase di riscrittura o
2325 del termine, tenta di scaricare la condizione $P$. Se il
2334 condizioni collaterali su cui sta lavorando. Il semplificatore smette la dimostrazione
2337 che specifica la dimensione massima dello stack che il semplificatore pu�
2341 circa la divisione e il modulo sono spesso accompagnate da condizioni
2352 \holtxt{(k~MOD~(x~+~1))~MOD~(x~+~1)}: la procedura di decisione
2353 aritmetica pu� dimostrare che \holtxt{0 < x + 1}, giustificando la riscrittura.
2360 esistenziali. Questo significa che la riscrittura condizionale \[
2371 Ci sono due strade per cui un teorema per la riscrittura pu� essere passato al
2386 dipendente dal \simpset{} utilizzato: ciascun \simpset{} contiene la sua
2388 esso. La maggior parte dei \simpset{} usano la funzione filtro dal \simpset{}
2389 \ml{pure\_ss} (si veda la Sezione~\ref{sec:purebool-ss}). Tuttavia, quando un
2395 \index{semplificazione!garantire la terminazione}
2398 che pu� essere applicato. Si veda la Sezione~\ref{sec:simp-special-rewrite-forms}
2427 Analogamente, se � una negazione booleana $\neg P$, diventa la regola \[
2475 Assumiamo per i seguenti esempi che la variabile $x$ sia legata a uno
2476 scopo pi� alto. Allora, se $f(x)$ deve matchare $x + 4$, la variabile $f$
2519 perch� il predicato $P$ � applicato a un argomento che include la
2548 lette verso l'alto. Con \ml{ABS}, per esempio, la regola dice ``quando
2550 e poi il risultato � formato ri-astraendo con la variabile
2560 dove $E_1$ � la forma da riscrivere. Ciascun $\mathit{cond}_i$ pu�
2567 dove la variabile $V_2$ deve occorrere libera in $E_2$.
2569 Per esempio, la forma teorema di \ml{MK\_COMB} sarebbe
2573 e la forma teorema di \ml{ABS} sarebbe
2585 la regola di congruenza (che si trova in \ml{CONG\_ss}) per le implicazioni. Questa
2604 Questa regola permette di assumere la guardia quando si semplifica il
2605 ramo-vero del condizionale, e di assumere la sua negazione quando si
2615 la semplificazione dei rami delle espressioni condizionali:
2621 Se aggiunta al semplificatore, questa regola prender� la precedenza su qualsiasi
2632 i rami di un condizionali fino a quando la guarda di quel condizionale � semplificata
2675 L'ordine degli operandi nella forma normale-AC in cui lavora la normalizzazione-AC
2676 del semplificatore non � specificato. Tuttavia, la forma
2678 \ml{arith\_ss}, e il frammento \ml{ARITH\_ss} che ne � la base, ha
2680 numeri naturali. Combinare la normalizzazione-AC, come descritta qui, con
2683 I teoremi AC possono essere aggiunti ai \simpset{} anche attraverso la lista di teoremi parte
2684 dell'interfaccia della tattica e della conversione, usando la forma speciale di riscrittura
2693 Si veda la Sezione~\ref{sec:simp-special-rewrite-forms} per maggiori informazioni su speciali
2719 � acceso. Se la conversione � applicata, e se il livello di traccia del
2725 sotto-termini a cui la conversione dovrebbe essere applicata. Se il valore �
2726 \ml{NONE}, allora la conversione sar� provata ad ogni posizione.
2727 Altrimenti, la conversione � applicata a posizioni di termine che matchano il
2735 i tipi, e non controlla binding multipli. Questo significa che la
2739 Infine, la conversione stessa. Molti usi di questa infrastruttura sono per aggiungere
2748 L'argomento \ml{term} deve essere di tipo \holtxt{:bool}, e la chiamata
2751 futura versione di \HOL{} ma per come stanno le cose ora, la chiamata ricorsiva pu�
2752 essere usata \emph{solo} per scaricare la condizione collaterale. Si noti anche che
2785 pu� fare la seguente dichiarazione:
2804 procedura di decisione incorporata accesso ai teoremi che rappresentano la nuova informazione
2814 Quando un riduttore � applicato a un termine, � richiamata la funzione
2815 \ml{apply} fornita. Oltre che al termine da trasformare, la
2826 possibili. Questo significa che bench� la riscrittura del semplificatore avvenda in un maniera che va
2841 A due delle caratteristiche avanzate del semplificatore, la normalizzazione-AC e
2862 \index{semplificazione!garantire la terminazione}
2881 la tecnologia di congruenza del semplificatore pu� essere usata per forzare il
2900 Qualunque sia la loro origine, tali teoremi sono il classico esempio di
2924 costruiscono regole di congruenza per forzare la riscritture alla sinistra o alla destra di
2935 la semplificazione sulla sinistra o sulla destra di un'eguaglianza rispettivamente.
2945 \subsubsection{Limitare la semplificazione}
2948 \index{semplificazione!garantire la terminazione}
2961 di riscritture a quel termine. Quando sono usate riscritture condizionali, la
2963 limite, finch� la riscrittura � infine applicata. Anche l'applicazione
2971 altrimenti un buon metodo per assicurare che la semplificazione termina.
2986 $\lambda$-calcolo. Questo implicher� la definizione di un nuovo tipo
2988 funzioni appropriate (ad esempio, la sostituzione) e le relazioni su
2989 \texttt{lamterm}. E' probabile che si lavori con la chiusura riflessiva
3005 di sopra, ma anche quelle dei teoremi che descrivono la chiusura riflessiva e
3006 transitiva (si veda la Sezione~\ref{relation}).
3022 la riflessivit� di \bred{} dimostrer� il risultato desiderato. I teoremi
3051 \item[\texttt{trans}] Il teorema che afferma che la relazione �
3053 \item[\texttt{refl}] Il teorema che afferma che la relazione �
3057 $P_i$ menzioner� presumibilmente la nuova relazione $R$ applicata a una
3065 una relazione $\rightarrow_{wh}^*$ per la riduzione weak-head. Qualsiasi riduzione
3067 il semplificatore ``promuova'' automaticamente i fatti circa la riduzione weak-head
3068 a fatti circa la $\beta$-riduzione, e poi li usi come riscritture.
3069 \item[\texttt{rewrs}] Possibilmente riscritture condizionali, presumibilmente la maggior parte
3073 la riscrittura per $K$ di sopra, cos� come la definizione della
3080 \texttt{ss} esistente, cos� come la capacit� di riscrivere con la relazione
3089 La Sezione~\ref{sec:datatype} e la Sezione~\ref{TFL} mostrano la capacit� di
3108 Gli entry-point pi� accessibili per usare la libreria \ml{computeLib}
3109 sono la conversione \ml{EVAL} e la sua tattica corrispondente
3128 argomenti con variabili---la cosiddetta valutazione \emph{simbolica}---e
3131 sufficiente informazione nell'input, la valutazione simbolica pu� restituire
3147 \subsection{Trattare con la divergenza}
3149 La difficolt� maggiore con l'uso di \ml{EVAL} � la terminazione. Troppo
3150 spesso, la valutazione simbolica con \ml{EVAL} diverger�, o generer�
3152 test. Per esempio, la seguente definizione � probabilmente uguale a \holtxt{FACT},
3175 per nulla, mentre la ricorsione stile-decostruttore di \holtxt{fact} non smette mai
3220 la valutazione, se si incontra una delle costanti fornite, essa
3224 la valutazione. Si veda la voce per \ml{CBV\_CONV} in \REFERENCE{} per
3238 termini con numeri e booleani. Dato un \ml{compset}, la funzione
3246 asintoticamente inefficienti. Piuttosto, la stessa definizione dovrebbe essere
3249 lavorare su numeri di Peano. Per colmare questa lacuna, la funzione
3257 \ml{Define} aggiunge automaticamente la sua definizione al compset globale
3261 di terminazione. Inoltre, \ml{tprove} non aggiunge la definizione
3283 \ml{ARITH\_CONV}. Il valutatore e la procedura di decisione sono
3285 Allo stesso modo, la procedura di decisione dell'aritmetica lineare pu� essere invocata
3295 per la completa aritmetica Presburger. Queste sono disponibili come
3308 dei numeri reali e dell'analisi. Si veda la Sezione~\ref{reals}
3317 La libreria \theoryimp{wordsLib} fornisce uno strumento di supporto per i bit-vectors, questo include infrastrutture per: la valutazione, il parsing, il pretty-printing e la semplificazione.
3333 Si noti che qui � usata un'annotazione di tipo per designare la dimensione word. Quando la dimensione word � rappresentata da una variabile di tipo (cio� per word i lunghezza arbitraria), la valutazione
3348 E' possibile fare il parsing di numeri ottali, ma questo deve essere prima abilitato impostando la reference \ml{base\_tokens.allow\_octal\_input} a true. Per esempio:
3362 I word possono essere stampati usando le basi numeriche standard. Per esempio, la funzione
3377 La variabile di traccia \ml{"word printing"} fornisce un metodo alternativo per cambiare la base numerica di output --- � particolarmente adatta per selezionare temporaneamente una base numerica, per esempio:
3389 Si pu� aver notato che \ty{:word4} e \ty{:word8} sono stati usati come convenienti abbreviazioni di parsing per \ty{:\bool[4]} e \ty{:\bool[8]} --- questa agevolazione � disponibile per molte dimensioni standard di word. Gli utenti che desiderano usare questa notazione per dimensioni di non-standard di word possono usare la funzione \ml{wordsLib.mk\_word\_size}:
3406 I simboli per le operazioni aritmetiche standard (addizione, sottrazione e moltiplicazione) sono sottoposte a overload con operatori per altre teorie standard, cio� per i numeri naturali, interi, razionali e reali. In molti casi l'inferenza di tipo risolver� l'overloading, tuttavia, in alcuni casi questo non � possibile. La scelta dell'operatore dipender� dall'ordine in cui le teorie sono caricate. Per cambiare questo comportamento sono fornite le funzioni \ml{wordsLib.deprecate\_word} e \ml{wordsLib.prefer\_word}. Per esempio, nella seguente sessione, la selezione degli operatori word � deprecata:
3439 Naturalmente, potrebbero essere state aggiunte annotazioni di tipo per evitare questo problema completamente. Si noti che, diversamente da \ml{deprecate\_int}, la funzione \ml{deprecate\_word} non rimuove gli overloading, semplicemente abbassa la loro precedenza.
3443 Pu� essere una seccatura aggiungere annotazioni di tipo quando si specifica il tipo di ritorno per operazioni come: \holtxt{word\_extract}, \holtxt{word\_concat}, \holtxt{concat\_word\_list} e \holtxt{word\_replicate}. Questo perch� c'� spesso una lunghezza ``standard'' che potrebbe essere indovinata, ad esempio la concatenazione di solito somma le lunghezze dei word costituenti. Un'agevolazione per indovinare la lunghezza word � controllata dalla reference \ml{wordsLib.guessing\_word\_lengths}, che � falsa di default. Le congetture sono eseguite durante un passo di post-processing che avviene dopo l'applicazione di \ml{Parse.Term}. Questo � mostrato di sotto.
3458 Nell'esempio di sopra, le congetture sulla lunghezza dei word sono attivate. Sono fatte due congetture: ci si aspetta che l'estrazione dia un word di quattro bit, e che la concatenazione dia un word di dodici bit ($3 \times 4$). Se sono richieste lunghezze numeriche non standard allo si possono aggiungere delle annotazioni di tipo per evitare che siano fatte delle congetture. Quando la congettura � disattivata i tipi risultanti rimangono come variabili di tipo inventate, cio� come gli alfa e i beta di sopra.
3467 \item[\ml{WORD\_ARITH\_ss}] semplifica operazioni aritmetiche word. La sottrazione � sostituita con la moltiplicazione da -1.
3473 \item[\ml{WORD\_MUL\_LSL\_ss}] semplifica la moltiplicazione con un letterale word in una somma di prodotti parziali.
3475 Molti di questi frammenti \emph{simpset} hanno delle conversioni corrispondenti. Per esempio, la conversione \ml{WORD\_ARITH\_CONV} � basata si \ml{WORD\_ARITH\_EQ\_ss}, tuttavia, fa del lavoro extra per assicurare che \holtxt{``a = b``} e \holtxt{``b = a``} si convertano nella stessa espressioni. Di conseguenza, questa conversione � adatta per ragionare circa l'eguaglianza delle espressioni aritmetiche word.
3477 Il comportamento dei frammenti elencati di sopra � mostrato usando la seguente funzione:
3569 quando la negazione di un goal � insoddisfacibile.}. Questo approccio � ragionevolmente generale e
3575 ci sono molte addizioni annidate (magari attraverso la moltiplicazione).
3601 Ci sono anche tattiche bit-blasting: \ml{BBLAST\_TAC} e \ml{FULL\_BBLAST\_TAC}; dove solo la seconda fa uso delle assunzioni del goal.