Theory: probPseudo

Parents

• booleanSequence

Types

Constants

• pseudo_linear1  :num -> num -> bool
• pseudo  :num -> num -> bool
• pseudo_linear_hd  :num -> bool
• pseudo_linear_tl  :num -> num -> num -> num -> num

Definitions

pseudo_def

|- pseudo = pseudo_linear1

pseudo_linear1_def

|- (!x. SHD (pseudo_linear1 x) = pseudo_linear_hd x) /\
   !x. STL (pseudo_linear1 x) = pseudo_linear1 (pseudo_linear_tl 103 95 79 x)

pseudo_linear_hd_def

|- pseudo_linear_hd = EVEN

pseudo_linear_tl_def

|- !a b n x. pseudo_linear_tl a b n x = (a * x + b) MOD (2 * n + 1)

Theorems

PSEUDO_LINEAR1_EXECUTE

|- ?g.
     (!x. SHD (g x) = pseudo_linear_hd x) /\
     !x. STL (g x) = g (pseudo_linear_tl 103 95 79 x)