Theory pre_emit

Parents

words

Contents

Type operators

(none)

Constants

fromNum : num # α itself -> α word
sw2sw_itself : α itself -> β word -> α word
w2w_itself : α itself -> β word -> α word
word_concat_itself : α itself -> β word -> γ word -> α word
word_eq : α word -> α word -> bool
word_extract_itself : α itself -> num -> num -> β word -> α word
word_index : α word -> num -> bool

Definitions

fromNum_def_primitive sw2sw_itself_def w2w_itself_def word_concat_itself_def word_eq_def word_extract_itself_def word_index_def

Theorems

fromNum_def fromNum_ind

Definitions

fromNum_def_primitive

⊢ fromNum =
  WFREC (@R. WF R)
    (λfromNum a.
         case a of (v,v1) => I (n2w_itself (v MOD dimword (:α),(:α))))

sw2sw_itself_def

⊢ ∀w. sw2sw_itself (:α) w = sw2sw w

w2w_itself_def

⊢ ∀w. w2w_itself (:α) w = w2w w

word_concat_itself_def

⊢ ∀v w. word_concat_itself (:α) v w = v @@ w

⊢ ∀v w. word_eq v w ⇔ v = w

word_extract_itself_def

⊢ ∀h l w. word_extract_itself (:α) h l w = (h >< l) w

word_index_def

⊢ ∀w n. word_index w n ⇔ w ' n

Theorems

⊢ fromNum (n,(:α)) = n2w_itself (n MOD dimword (:α),(:α))

⊢ ∀P. (∀n. P (n,(:α))) ⇒ ∀v v1. P (v,v1)