Theory: booleanSequence

Parents

• probExtra

Types

Constants

• STAKE  :num -> (num -> bool) -> bool list
• SCONST  :bool -> num -> bool
• SDEST  :(num -> bool) -> bool # (num -> bool)
• SCONS  :bool -> (num -> bool) -> num -> bool
• SDROP  :num -> (num -> bool) -> num -> bool
• SHD  :(num -> bool) -> bool
• STL  :(num -> bool) -> num -> bool

Definitions

SCONS_def

|- (!h t. SCONS h t 0 = h) /\ !h t n. SCONS h t (SUC n) = t n

SCONST_def

|- SCONST = K

SDEST_def

|- SDEST = (\s. (SHD s,STL s))

SDROP_def

|- (SDROP 0 = I) /\ !n. SDROP (SUC n) = SDROP n o STL

SHD_def

|- !f. SHD f = f 0

STAKE_def

|- (!s. STAKE 0 s = []) /\ !n s. STAKE (SUC n) s = SHD s::STAKE n (STL s)

STL_def

|- !f n. STL f n = f (SUC n)

Theorems

SCONS_SURJ

|- !x. ?h t. x = SCONS h t

SHD_SCONS

|- !h t. SHD (SCONS h t) = h

SHD_SCONST

|- !b. SHD (SCONST b) = b

SHD_STL_ISO

|- !h t. ?x. (SHD x = h) /\ (STL x = t)

STL_SCONS

|- !h t. STL (SCONS h t) = t

STL_SCONST

|- !b. STL (SCONST b) = SCONST b