Theory: ascii

Parents

• pair
• ind_type
• sum

Types

• ascii(Arity = 0)

Constants

• ii_internal_mk_ascii  :(bool # bool # bool # bool # bool # bool # bool # bool) recspace -> ascii
• ascii_case  :(bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> 'a) -> ascii -> 'a
• ii_internal_dest_ascii  :ascii -> (bool # bool # bool # bool # bool # bool # bool # bool) recspace
• ASCII  :bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> ascii
• ii_internalascii0  :bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> ascii
• ascii_size  :ascii -> num

Definitions

ASCII

|- ASCII = ii_internalascii0

ascii_case_def

|- !f a0 a1 a2 a3 a4 a5 a6 a7.
     ascii_case f (ASCII a0 a1 a2 a3 a4 a5 a6 a7) = f a0 a1 a2 a3 a4 a5 a6 a7

ascii_repfns

|- (!a. ii_internal_mk_ascii (ii_internal_dest_ascii a) = a) /\
   !r.
     (\a0'.
        !'ascii'.
          (!a0'.
             (?a0 a1 a2 a3 a4 a5 a6 a7.
                a0' =
                (\a0 a1 a2 a3 a4 a5 a6 a7.
                   CONSTR 0 (a0,a1,a2,a3,a4,a5,a6,a7) (\n. BOTTOM)) a0 a1 a2
                  a3 a4 a5 a6 a7) ==>
             'ascii' a0') ==>
          'ascii' a0') r =
     (ii_internal_dest_ascii (ii_internal_mk_ascii r) = r)

ascii_size_def

|- !a0 a1 a2 a3 a4 a5 a6 a7. ascii_size (ASCII a0 a1 a2 a3 a4 a5 a6 a7) = 1

ascii_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0'.
          !'ascii'.
            (!a0'.
               (?a0 a1 a2 a3 a4 a5 a6 a7.
                  a0' =
                  (\a0 a1 a2 a3 a4 a5 a6 a7.
                     CONSTR 0 (a0,a1,a2,a3,a4,a5,a6,a7) (\n. BOTTOM)) a0 a1 a2
                    a3 a4 a5 a6 a7) ==>
               'ascii' a0') ==>
            'ascii' a0') rep

ii_internalascii0_def

|- ii_internalascii0 =
   (\a0 a1 a2 a3 a4 a5 a6 a7.
      ii_internal_mk_ascii
        ((\a0 a1 a2 a3 a4 a5 a6 a7.
            CONSTR 0 (a0,a1,a2,a3,a4,a5,a6,a7) (\n. BOTTOM)) a0 a1 a2 a3 a4 a5
           a6 a7))

Theorems

ascii_11

|- !a0 a1 a2 a3 a4 a5 a6 a7 a0' a1' a2' a3' a4' a5' a6' a7'.
     (ASCII a0 a1 a2 a3 a4 a5 a6 a7 = ASCII a0' a1' a2' a3' a4' a5' a6' a7') =
     (a0 = a0') /\ (a1 = a1') /\ (a2 = a2') /\ (a3 = a3') /\ (a4 = a4') /\
     (a5 = a5') /\ (a6 = a6') /\ (a7 = a7')

ascii_Axiom

|- !f.
     ?fn.
       !a0 a1 a2 a3 a4 a5 a6 a7.
         fn (ASCII a0 a1 a2 a3 a4 a5 a6 a7) = f a0 a1 a2 a3 a4 a5 a6 a7

ascii_case_cong

|- !f' f M' M.
     (M = M') /\
     (!a0 a1 a2 a3 a4 a5 a6 a7.
        (M' = ASCII a0 a1 a2 a3 a4 a5 a6 a7) ==>
        (f a0 a1 a2 a3 a4 a5 a6 a7 = f' a0 a1 a2 a3 a4 a5 a6 a7)) ==>
     (ascii_case f M = ascii_case f' M')

ascii_induction

|- !P. (!b b0 b1 b2 b3 b4 b5 b6. P (ASCII b b0 b1 b2 b3 b4 b5 b6)) ==> !a. P a

ascii_nchotomy

|- !a. ?b b0 b1 b2 b3 b4 b5 b6. a = ASCII b b0 b1 b2 b3 b4 b5 b6