Theory "ctl"

Parents env res_quan ks

Signature

Type	Arity
xnum	0
prodctl7	1
prodctl0	1
path	1
kripke_structure	2
ctl	1
bexp	1
Constant	Type
xnum_to	:num -> xnum -> num -> bool
xnum_size	:xnum -> num
xnum_case	:'a -> (num -> 'a) -> xnum -> 'a
path_size	:('s -> num) -> 's path -> num
path_case	:('s list -> 'a) -> ((num -> 's) -> 'a) -> 's path -> 'a
num_to	:num -> num -> num -> bool
mk_xnum	:num recspace -> xnum
mk_prodctl7	:'a bexp recspace -> 'a prodctl7
mk_prodctl0	:'a recspace -> 'a prodctl0
mk_path	:('s list # (num -> 's)) recspace -> 's path
mk_kripke_structure	:(('state -> bool) # ('state -> bool) # ('state # 'state -> bool) # ('prop -> bool) # ('state -> 'prop -> bool)) recspace -> ('prop, 'state) kripke_structure
mk_ctl	:'a bexp recspace -> 'a ctl
mk_bexp	:'a recspace -> 'a bexp
kripke_structure_size	:('prop -> num) -> ('state -> num) -> ('prop, 'state) kripke_structure -> num
kripke_structure_case	:(('state -> bool) -> ('state -> bool) -> ('state # 'state -> bool) -> ('prop -> bool) -> ('state -> 'prop -> bool) -> 'a) -> ('prop, 'state) kripke_structure -> 'a
kripke_structure_S_fupd	:(('state -> bool) -> 'state -> bool) -> ('prop, 'state) kripke_structure -> ('prop, 'state) kripke_structure
kripke_structure_S0_fupd	:(('state -> bool) -> 'state -> bool) -> ('prop, 'state) kripke_structure -> ('prop, 'state) kripke_structure
kripke_structure_S0	:('prop, 'state) kripke_structure -> 'state -> bool
kripke_structure_S	:('prop, 'state) kripke_structure -> 'state -> bool
kripke_structure_R_fupd	:(('state # 'state -> bool) -> 'state # 'state -> bool) -> ('prop, 'state) kripke_structure -> ('prop, 'state) kripke_structure
kripke_structure_R	:('prop, 'state) kripke_structure -> 'state # 'state -> bool
kripke_structure_P_fupd	:(('prop -> bool) -> 'prop -> bool) -> ('prop, 'state) kripke_structure -> ('prop, 'state) kripke_structure
kripke_structure_P	:('prop, 'state) kripke_structure -> 'prop -> bool
kripke_structure_L_fupd	:(('state -> 'prop -> bool) -> 'state -> 'prop -> bool) -> ('prop, 'state) kripke_structure -> ('prop, 'state) kripke_structure
kripke_structure_L	:('prop, 'state) kripke_structure -> 'state -> 'prop -> bool
kripke_structure	:('state -> bool) -> ('state -> bool) -> ('state # 'state -> bool) -> ('prop -> bool) -> ('state -> 'prop -> bool) -> ('prop, 'state) kripke_structure
dest_xnum	:xnum -> num recspace
dest_prodctl7	:'a prodctl7 -> 'a bexp recspace
dest_prodctl0	:'a prodctl0 -> 'a recspace
dest_path	:'s path -> ('s list # (num -> 's)) recspace
dest_kripke_structure	:('prop, 'state) kripke_structure -> (('state -> bool) # ('state -> bool) # ('state # 'state -> bool) # ('prop -> bool) # ('state -> 'prop -> bool)) recspace
dest_ctl	:'a ctl -> 'a bexp recspace
dest_bexp	:'a bexp -> 'a recspace
ctl_size2	:'prop ctl -> num
ctl_size	:('a -> num) -> 'a ctl -> num
ctl_pstv_size	:'a ctl -> num
ctl_case	:('a bexp -> 'c) -> ('a ctl -> 'c) -> ('a ctl # 'a ctl -> 'c) -> ('a ctl -> 'c) -> ('a ctl # 'a ctl -> 'c) -> ('a ctl -> 'c) -> 'a ctl -> 'c
ctl9	:'a ctl -> 'a ctl
ctl8	:'a bexp -> 'a ctl
ctl6	:'a bexp # 'a bexp -> 'a bexp
ctl5	:'a bexp -> 'a bexp -> 'a prodctl0
ctl4	:'a prodctl0 -> 'a bexp
ctl3	:'a bexp -> 'a bexp
ctl21	:num -> xnum
ctl20	:xnum
ctl2	:'a -> 'a bexp
ctl1_size	:('a -> num) -> 'a ctl # 'a ctl -> num
ctl19	:(num -> 's) -> 's path
ctl18	:'s list -> 's path
ctl17	:('state -> bool) -> ('state -> bool) -> ('state # 'state -> bool) -> ('prop -> bool) -> ('state -> 'prop -> bool) -> ('prop, 'state) kripke_structure
ctl16	:'a ctl # 'a ctl -> 'a ctl
ctl15	:'a ctl # 'a ctl -> 'a ctl
ctl14	:'a ctl -> 'a ctl -> 'a prodctl7
ctl13	:'a ctl -> 'a ctl
ctl12	:'a prodctl7 -> 'a ctl
ctl11	:'a ctl -> 'a ctl
ctl10	:'a prodctl7 -> 'a ctl
ctl1	:'a bexp
bexp_size2	:'prop bexp -> num
bexp_size	:('a -> num) -> 'a bexp -> num
bexp_pstv_size	:'a bexp -> num
bexp_case	:'c -> ('a -> 'c) -> ('a bexp -> 'c) -> ('a bexp # 'a bexp -> 'c) -> 'a bexp -> 'c
bexp1_size	:('a -> num) -> 'a bexp # 'a bexp -> num
XNUM	:num -> xnum
SUB_xnum_xnum_tupled	:xnum # xnum -> xnum
SUB_xnum_xnum	:xnum -> xnum -> xnum
SUB_xnum_num	:xnum -> num -> xnum
SUB_num_xnum	:num -> xnum -> xnum
RESTN	:'a path -> num -> 'a path
REST	:'a path -> 'a path
PLENGTH	:'a path -> xnum
PATH	:('a, 'b) kripke_structure -> 'b path -> 'b -> bool
LS_xnum_xnum_tupled	:xnum # xnum -> bool
LS_xnum_xnum	:xnum -> xnum -> bool
LS_xnum_num	:xnum -> num -> bool
LS_num_xnum	:num -> xnum -> bool
IS_INFINITE	:'a path -> bool
IS_FINITE	:'a path -> bool
IS_ACTL	:'a ctl -> bool
INFINITY	:xnum
INFINITE	:(num -> 's) -> 's path
HEAD	:'a path -> 'a
GT_xnum_xnum_tupled	:xnum # xnum -> bool
GT_xnum_xnum	:xnum -> xnum -> bool
GT_xnum_num	:xnum -> num -> bool
GT_num_xnum	:num -> xnum -> bool
FINITE	:'s list -> 's path
ELEM	:'a path -> num -> 'a
C_SEM_UNION_aux	:(('a, 'b) kripke_structure # 'a ctl # 'b + ('a, 'b) kripke_structure # ('b -> bool) # 'b + ('a, 'b) kripke_structure # (('b -> bool) # ('b -> bool)) # 'b + ('a, 'b) kripke_structure # ('b -> bool) # 'b -> ('a, 'b) kripke_structure # 'a ctl # 'b + ('a, 'b) kripke_structure # ('b -> bool) # 'b + ('a, 'b) kripke_structure # (('b -> bool) # ('b -> bool)) # 'b + ('a, 'b) kripke_structure # ('b -> bool) # 'b -> bool) -> ('a, 'b) kripke_structure # 'a ctl # 'b + ('a, 'b) kripke_structure # ('b -> bool) # 'b + ('a, 'b) kripke_structure # (('b -> bool) # ('b -> bool)) # 'b + ('a, 'b) kripke_structure # ('b -> bool) # 'b -> bool
C_SEM_UNION	:('a, 'b) kripke_structure # 'a ctl # 'b + ('a, 'b) kripke_structure # ('b -> bool) # 'b + ('a, 'b) kripke_structure # (('b -> bool) # ('b -> bool)) # 'b + ('a, 'b) kripke_structure # ('b -> bool) # 'b -> bool
C_SEM	:('a, 'b) kripke_structure -> 'a ctl -> 'b -> bool
C_OR2	:'prop ctl -> 'prop ctl -> 'prop ctl
C_OR	:'prop ctl # 'prop ctl -> 'prop ctl
C_NOT	:'a ctl -> 'a ctl
C_IMP2	:'prop ctl -> 'prop ctl -> 'prop ctl
C_IMP	:'prop ctl # 'prop ctl -> 'prop ctl
C_IFF	:'prop ctl -> 'prop ctl -> 'prop ctl
C_EX	:'a ctl -> 'a ctl
C_EU	:'a ctl # 'a ctl -> 'a ctl
C_EG	:'a ctl -> 'a ctl
C_EF	:'prop ctl -> 'prop ctl
C_BOOL	:'a bexp -> 'a ctl
C_AX	:'prop ctl -> 'prop ctl
C_AU	:'prop ctl # 'prop ctl -> 'prop ctl
C_AR	:'a ctl # 'a ctl -> 'a ctl
C_AND2	:'prop ctl -> 'prop ctl -> 'prop ctl
C_AND	:'a ctl # 'a ctl -> 'a ctl
C_AG	:'prop ctl -> 'prop ctl
C_AF	:'prop ctl -> 'prop ctl
CTL_SUB_tupled	:'a ctl # 'a ctl -> bool
CTL_SUB	:'a ctl -> 'a ctl -> bool
CTL_NNF	:'a ctl -> 'a ctl
CTL_MODEL_SAT	:('a, 'b) kripke_structure -> 'a ctl -> bool
CTL_BOOL_SUB_tupled	:'prop bexp # 'prop bexp -> bool
CTL_BOOL_SUB	:'prop bexp -> 'prop bexp -> bool
CEX	:('a, 'b) kripke_structure -> ('b -> bool) -> 'b -> bool
CEU	:('a, 'b) kripke_structure -> ('b -> bool) # ('b -> bool) -> 'b -> bool
CEG	:('a, 'b) kripke_structure -> ('b -> bool) -> 'b -> bool
B_TRUE	:'a bexp
B_SEM_tupled	:('prop -> bool) # 'prop bexp -> bool
B_SEM	:('prop -> bool) -> 'prop bexp -> bool
B_PROP	:'a -> 'a bexp
B_OR2	:'a bexp -> 'a bexp -> 'a bexp
B_OR	:'a bexp # 'a bexp -> 'a bexp
B_NOT	:'a bexp -> 'a bexp
B_IMP2	:'a bexp -> 'a bexp -> 'a bexp
B_IMP	:'a bexp # 'a bexp -> 'a bexp
B_IFF	:'a bexp -> 'a bexp -> 'a bexp
B_FALSE	:'a bexp
B_AND2	:'a bexp -> 'a bexp -> 'a bexp
B_AND	:'a bexp # 'a bexp -> 'a bexp
BEXP_NNF	:'a bexp -> 'a bexp

Definitions

bexp_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0'.
          !'bexp' 'prodctl0'.
            (!a0'.
               (a0' = ind_type$CONSTR 0 (@v. T) (\n. ind_type$BOTTOM)) \/
               (?a.
                  a0' =
                  (\a. ind_type$CONSTR (SUC 0) a (\n. ind_type$BOTTOM)) a) \/
               (?a.
                  (a0' =
                   (\a.
                      ind_type$CONSTR (SUC (SUC 0)) (@v. T)
                        (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'bexp' a) \/
               (?a.
                  (a0' =
                   (\a.
                      ind_type$CONSTR (SUC (SUC (SUC 0))) (@v. T)
                        (FCONS a (\n. ind_type$BOTTOM))) a) /\
                  'prodctl0' a) ==>
               'bexp' a0') /\
            (!a1'.
               (?a0 a1.
                  (a1' =
                   (\a0 a1.
                      ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) (@v. T)
                        (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0 a1) /\
                  'bexp' a0 /\ 'bexp' a1) ==>
               'prodctl0' a1') ==>
            'bexp' a0') rep

bexp_repfns

|- (!a. mk_bexp (dest_bexp a) = a) /\
   !r.
     (\a0'.
        !'bexp' 'prodctl0'.
          (!a0'.
             (a0' = ind_type$CONSTR 0 (@v. T) (\n. ind_type$BOTTOM)) \/
             (?a.
                a0' =
                (\a. ind_type$CONSTR (SUC 0) a (\n. ind_type$BOTTOM)) a) \/
             (?a.
                (a0' =
                 (\a.
                    ind_type$CONSTR (SUC (SUC 0)) (@v. T)
                      (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'bexp' a) \/
             (?a.
                (a0' =
                 (\a.
                    ind_type$CONSTR (SUC (SUC (SUC 0))) (@v. T)
                      (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'prodctl0' a) ==>
             'bexp' a0') /\
          (!a1'.
             (?a0 a1.
                (a1' =
                 (\a0 a1.
                    ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) (@v. T)
                      (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0 a1) /\
                'bexp' a0 /\ 'bexp' a1) ==>
             'prodctl0' a1') ==>
          'bexp' a0') r =
     (dest_bexp (mk_bexp r) = r)

prodctl0_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a1'.
          !'bexp' 'prodctl0'.
            (!a0'.
               (a0' = ind_type$CONSTR 0 (@v. T) (\n. ind_type$BOTTOM)) \/
               (?a.
                  a0' =
                  (\a. ind_type$CONSTR (SUC 0) a (\n. ind_type$BOTTOM)) a) \/
               (?a.
                  (a0' =
                   (\a.
                      ind_type$CONSTR (SUC (SUC 0)) (@v. T)
                        (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'bexp' a) \/
               (?a.
                  (a0' =
                   (\a.
                      ind_type$CONSTR (SUC (SUC (SUC 0))) (@v. T)
                        (FCONS a (\n. ind_type$BOTTOM))) a) /\
                  'prodctl0' a) ==>
               'bexp' a0') /\
            (!a1'.
               (?a0 a1.
                  (a1' =
                   (\a0 a1.
                      ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) (@v. T)
                        (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0 a1) /\
                  'bexp' a0 /\ 'bexp' a1) ==>
               'prodctl0' a1') ==>
            'prodctl0' a1') rep

prodctl0_repfns

|- (!a. mk_prodctl0 (dest_prodctl0 a) = a) /\
   !r.
     (\a1'.
        !'bexp' 'prodctl0'.
          (!a0'.
             (a0' = ind_type$CONSTR 0 (@v. T) (\n. ind_type$BOTTOM)) \/
             (?a.
                a0' =
                (\a. ind_type$CONSTR (SUC 0) a (\n. ind_type$BOTTOM)) a) \/
             (?a.
                (a0' =
                 (\a.
                    ind_type$CONSTR (SUC (SUC 0)) (@v. T)
                      (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'bexp' a) \/
             (?a.
                (a0' =
                 (\a.
                    ind_type$CONSTR (SUC (SUC (SUC 0))) (@v. T)
                      (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'prodctl0' a) ==>
             'bexp' a0') /\
          (!a1'.
             (?a0 a1.
                (a1' =
                 (\a0 a1.
                    ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) (@v. T)
                      (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0 a1) /\
                'bexp' a0 /\ 'bexp' a1) ==>
             'prodctl0' a1') ==>
          'prodctl0' a1') r =
     (dest_prodctl0 (mk_prodctl0 r) = r)

ctl1_def

|- ctl1 = mk_bexp (ind_type$CONSTR 0 (@v. T) (\n. ind_type$BOTTOM))

ctl2_def

|- ctl2 =
   (\a. mk_bexp ((\a. ind_type$CONSTR (SUC 0) a (\n. ind_type$BOTTOM)) a))

ctl3_def

|- ctl3 =
   (\a.
      mk_bexp
        ((\a.
            ind_type$CONSTR (SUC (SUC 0)) (@v. T)
              (FCONS a (\n. ind_type$BOTTOM))) (dest_bexp a)))

ctl4_def

|- ctl4 =
   (\a.
      mk_bexp
        ((\a.
            ind_type$CONSTR (SUC (SUC (SUC 0))) (@v. T)
              (FCONS a (\n. ind_type$BOTTOM))) (dest_prodctl0 a)))

ctl5_def

|- ctl5 =
   (\a0 a1.
      mk_prodctl0
        ((\a0 a1.
            ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) (@v. T)
              (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) (dest_bexp a0)
           (dest_bexp a1)))

ctl6

|- ctl6 = (\a. ctl4 ((@fn. !x y. fn (x,y) = ctl5 x y) a))

B_TRUE

|- T = ctl1

B_PROP

|- B_PROP = ctl2

B_NOT

|- $~ = ctl3

B_AND

|- B_AND = ctl6

bexp_case_def

|- (!v f f1 f2. bexp_case v f f1 f2 T = v) /\
   (!v f f1 f2 a. bexp_case v f f1 f2 (B_PROP a) = f a) /\
   (!v f f1 f2 a. bexp_case v f f1 f2 ~a = f1 a) /\
   !v f f1 f2 a. bexp_case v f f1 f2 (B_AND a) = f2 a

bexp_size_def

|- (!f. bexp_size f T = 0) /\ (!f a. bexp_size f (B_PROP a) = 1 + f a) /\
   (!f a. bexp_size f ~a = 1 + bexp_size f a) /\
   (!f a. bexp_size f (B_AND a) = 1 + bexp1_size f a) /\
   !f a0 a1. bexp1_size f (a0,a1) = 1 + (bexp_size f a0 + bexp_size f a1)

B_OR_def

|- !b1 b2. B_OR (b1,b2) = ~B_AND (~b1, ~b2)

B_FALSE_def

|- F = ~T

ctl_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0'.
          !'ctl' 'prodctl7'.
            (!a0'.
               (?a.
                  a0' = (\a. ind_type$CONSTR 0 a (\n. ind_type$BOTTOM)) a) \/
               (?a.
                  (a0' =
                   (\a.
                      ind_type$CONSTR (SUC 0) (@v. T)
                        (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'ctl' a) \/
               (?a.
                  (a0' =
                   (\a.
                      ind_type$CONSTR (SUC (SUC 0)) (@v. T)
                        (FCONS a (\n. ind_type$BOTTOM))) a) /\
                  'prodctl7' a) \/
               (?a.
                  (a0' =
                   (\a.
                      ind_type$CONSTR (SUC (SUC (SUC 0))) (@v. T)
                        (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'ctl' a) \/
               (?a.
                  (a0' =
                   (\a.
                      ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) (@v. T)
                        (FCONS a (\n. ind_type$BOTTOM))) a) /\
                  'prodctl7' a) \/
               (?a.
                  (a0' =
                   (\a.
                      ind_type$CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) (@v. T)
                        (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'ctl' a) ==>
               'ctl' a0') /\
            (!a1'.
               (?a0 a1.
                  (a1' =
                   (\a0 a1.
                      ind_type$CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0))))))
                        (@v. T) (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM))))
                     a0 a1) /\ 'ctl' a0 /\ 'ctl' a1) ==>
               'prodctl7' a1') ==>
            'ctl' a0') rep

ctl_repfns

|- (!a. mk_ctl (dest_ctl a) = a) /\
   !r.
     (\a0'.
        !'ctl' 'prodctl7'.
          (!a0'.
             (?a. a0' = (\a. ind_type$CONSTR 0 a (\n. ind_type$BOTTOM)) a) \/
             (?a.
                (a0' =
                 (\a.
                    ind_type$CONSTR (SUC 0) (@v. T)
                      (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'ctl' a) \/
             (?a.
                (a0' =
                 (\a.
                    ind_type$CONSTR (SUC (SUC 0)) (@v. T)
                      (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'prodctl7' a) \/
             (?a.
                (a0' =
                 (\a.
                    ind_type$CONSTR (SUC (SUC (SUC 0))) (@v. T)
                      (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'ctl' a) \/
             (?a.
                (a0' =
                 (\a.
                    ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) (@v. T)
                      (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'prodctl7' a) \/
             (?a.
                (a0' =
                 (\a.
                    ind_type$CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) (@v. T)
                      (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'ctl' a) ==>
             'ctl' a0') /\
          (!a1'.
             (?a0 a1.
                (a1' =
                 (\a0 a1.
                    ind_type$CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0))))))
                      (@v. T) (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0
                   a1) /\ 'ctl' a0 /\ 'ctl' a1) ==>
             'prodctl7' a1') ==>
          'ctl' a0') r =
     (dest_ctl (mk_ctl r) = r)

prodctl7_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a1'.
          !'ctl' 'prodctl7'.
            (!a0'.
               (?a.
                  a0' = (\a. ind_type$CONSTR 0 a (\n. ind_type$BOTTOM)) a) \/
               (?a.
                  (a0' =
                   (\a.
                      ind_type$CONSTR (SUC 0) (@v. T)
                        (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'ctl' a) \/
               (?a.
                  (a0' =
                   (\a.
                      ind_type$CONSTR (SUC (SUC 0)) (@v. T)
                        (FCONS a (\n. ind_type$BOTTOM))) a) /\
                  'prodctl7' a) \/
               (?a.
                  (a0' =
                   (\a.
                      ind_type$CONSTR (SUC (SUC (SUC 0))) (@v. T)
                        (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'ctl' a) \/
               (?a.
                  (a0' =
                   (\a.
                      ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) (@v. T)
                        (FCONS a (\n. ind_type$BOTTOM))) a) /\
                  'prodctl7' a) \/
               (?a.
                  (a0' =
                   (\a.
                      ind_type$CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) (@v. T)
                        (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'ctl' a) ==>
               'ctl' a0') /\
            (!a1'.
               (?a0 a1.
                  (a1' =
                   (\a0 a1.
                      ind_type$CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0))))))
                        (@v. T) (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM))))
                     a0 a1) /\ 'ctl' a0 /\ 'ctl' a1) ==>
               'prodctl7' a1') ==>
            'prodctl7' a1') rep

prodctl7_repfns

|- (!a. mk_prodctl7 (dest_prodctl7 a) = a) /\
   !r.
     (\a1'.
        !'ctl' 'prodctl7'.
          (!a0'.
             (?a. a0' = (\a. ind_type$CONSTR 0 a (\n. ind_type$BOTTOM)) a) \/
             (?a.
                (a0' =
                 (\a.
                    ind_type$CONSTR (SUC 0) (@v. T)
                      (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'ctl' a) \/
             (?a.
                (a0' =
                 (\a.
                    ind_type$CONSTR (SUC (SUC 0)) (@v. T)
                      (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'prodctl7' a) \/
             (?a.
                (a0' =
                 (\a.
                    ind_type$CONSTR (SUC (SUC (SUC 0))) (@v. T)
                      (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'ctl' a) \/
             (?a.
                (a0' =
                 (\a.
                    ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) (@v. T)
                      (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'prodctl7' a) \/
             (?a.
                (a0' =
                 (\a.
                    ind_type$CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) (@v. T)
                      (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'ctl' a) ==>
             'ctl' a0') /\
          (!a1'.
             (?a0 a1.
                (a1' =
                 (\a0 a1.
                    ind_type$CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0))))))
                      (@v. T) (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0
                   a1) /\ 'ctl' a0 /\ 'ctl' a1) ==>
             'prodctl7' a1') ==>
          'prodctl7' a1') r =
     (dest_prodctl7 (mk_prodctl7 r) = r)

ctl8_def

|- ctl8 = (\a. mk_ctl ((\a. ind_type$CONSTR 0 a (\n. ind_type$BOTTOM)) a))

ctl9_def

|- ctl9 =
   (\a.
      mk_ctl
        ((\a. ind_type$CONSTR (SUC 0) (@v. T) (FCONS a (\n. ind_type$BOTTOM)))
           (dest_ctl a)))

ctl10_def

|- ctl10 =
   (\a.
      mk_ctl
        ((\a.
            ind_type$CONSTR (SUC (SUC 0)) (@v. T)
              (FCONS a (\n. ind_type$BOTTOM))) (dest_prodctl7 a)))

ctl11_def

|- ctl11 =
   (\a.
      mk_ctl
        ((\a.
            ind_type$CONSTR (SUC (SUC (SUC 0))) (@v. T)
              (FCONS a (\n. ind_type$BOTTOM))) (dest_ctl a)))

ctl12_def

|- ctl12 =
   (\a.
      mk_ctl
        ((\a.
            ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) (@v. T)
              (FCONS a (\n. ind_type$BOTTOM))) (dest_prodctl7 a)))

ctl13_def

|- ctl13 =
   (\a.
      mk_ctl
        ((\a.
            ind_type$CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) (@v. T)
              (FCONS a (\n. ind_type$BOTTOM))) (dest_ctl a)))

ctl14_def

|- ctl14 =
   (\a0 a1.
      mk_prodctl7
        ((\a0 a1.
            ind_type$CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0)))))) (@v. T)
              (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) (dest_ctl a0)
           (dest_ctl a1)))

ctl15

|- ctl15 = (\a. ctl10 ((@fn. !x y. fn (x,y) = ctl14 x y) a))

ctl16

|- ctl16 = (\a. ctl12 ((@fn. !x y. fn (x,y) = ctl14 x y) a))

C_BOOL

|- C_BOOL = ctl8

C_NOT

|- $~ = ctl9

C_AND

|- C_AND = ctl15

C_EX

|- C_EX = ctl11

C_EU

|- C_EU = ctl16

C_EG

|- C_EG = ctl13

ctl_case_def

|- (!f f1 f2 f3 f4 f5 a. ctl_case f f1 f2 f3 f4 f5 (C_BOOL a) = f a) /\
   (!f f1 f2 f3 f4 f5 a. ctl_case f f1 f2 f3 f4 f5 ~a = f1 a) /\
   (!f f1 f2 f3 f4 f5 a. ctl_case f f1 f2 f3 f4 f5 (C_AND a) = f2 a) /\
   (!f f1 f2 f3 f4 f5 a. ctl_case f f1 f2 f3 f4 f5 (C_EX a) = f3 a) /\
   (!f f1 f2 f3 f4 f5 a. ctl_case f f1 f2 f3 f4 f5 (C_EU a) = f4 a) /\
   !f f1 f2 f3 f4 f5 a. ctl_case f f1 f2 f3 f4 f5 (C_EG a) = f5 a

ctl_size_def

|- (!f a. ctl_size f (C_BOOL a) = 1 + bexp_size f a) /\
   (!f a. ctl_size f ~a = 1 + ctl_size f a) /\
   (!f a. ctl_size f (C_AND a) = 1 + ctl1_size f a) /\
   (!f a. ctl_size f (C_EX a) = 1 + ctl_size f a) /\
   (!f a. ctl_size f (C_EU a) = 1 + ctl1_size f a) /\
   (!f a. ctl_size f (C_EG a) = 1 + ctl_size f a) /\
   !f a0 a1. ctl1_size f (a0,a1) = 1 + (ctl_size f a0 + ctl_size f a1)

kripke_structure_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0'.
          !'kripke_structure'.
            (!a0'.
               (?a0 a1 a2 a3 a4.
                  a0' =
                  (\a0 a1 a2 a3 a4.
                     ind_type$CONSTR 0 (a0,a1,a2,a3,a4) (\n. ind_type$BOTTOM))
                    a0 a1 a2 a3 a4) ==>
               'kripke_structure' a0') ==>
            'kripke_structure' a0') rep

kripke_structure_repfns

|- (!a. mk_kripke_structure (dest_kripke_structure a) = a) /\
   !r.
     (\a0'.
        !'kripke_structure'.
          (!a0'.
             (?a0 a1 a2 a3 a4.
                a0' =
                (\a0 a1 a2 a3 a4.
                   ind_type$CONSTR 0 (a0,a1,a2,a3,a4) (\n. ind_type$BOTTOM))
                  a0 a1 a2 a3 a4) ==>
             'kripke_structure' a0') ==>
          'kripke_structure' a0') r =
     (dest_kripke_structure (mk_kripke_structure r) = r)

ctl17_def

|- ctl17 =
   (\a0 a1 a2 a3 a4.
      mk_kripke_structure
        ((\a0 a1 a2 a3 a4.
            ind_type$CONSTR 0 (a0,a1,a2,a3,a4) (\n. ind_type$BOTTOM)) a0 a1 a2
           a3 a4))

kripke_structure

|- kripke_structure = ctl17

kripke_structure_case_def

|- !f a0 a1 a2 a3 a4.
     kripke_structure_case f (kripke_structure a0 a1 a2 a3 a4) =
     f a0 a1 a2 a3 a4

kripke_structure_size_def

|- !f f1 a0 a1 a2 a3 a4.
     kripke_structure_size f f1 (kripke_structure a0 a1 a2 a3 a4) = 1

kripke_structure_S

|- !f f0 f1 f2 f3. (kripke_structure f f0 f1 f2 f3).S = f

kripke_structure_S0

|- !f f0 f1 f2 f3. (kripke_structure f f0 f1 f2 f3).S0 = f0

kripke_structure_R

|- !f f0 f1 f2 f3. (kripke_structure f f0 f1 f2 f3).R = f1

kripke_structure_P

|- !f f0 f1 f2 f3. (kripke_structure f f0 f1 f2 f3).P = f2

kripke_structure_L

|- !f f0 f1 f2 f3. (kripke_structure f f0 f1 f2 f3).L = f3

kripke_structure_S_fupd

|- !f4 f f0 f1 f2 f3.
     kripke_structure f f0 f1 f2 f3 with S updated_by f4 =
     kripke_structure (f4 f) f0 f1 f2 f3

kripke_structure_S0_fupd

|- !f4 f f0 f1 f2 f3.
     kripke_structure f f0 f1 f2 f3 with S0 updated_by f4 =
     kripke_structure f (f4 f0) f1 f2 f3

kripke_structure_R_fupd

|- !f4 f f0 f1 f2 f3.
     kripke_structure f f0 f1 f2 f3 with R updated_by f4 =
     kripke_structure f f0 (f4 f1) f2 f3

kripke_structure_P_fupd

|- !f4 f f0 f1 f2 f3.
     kripke_structure f f0 f1 f2 f3 with P updated_by f4 =
     kripke_structure f f0 f1 (f4 f2) f3

kripke_structure_L_fupd

|- !f4 f f0 f1 f2 f3.
     kripke_structure f f0 f1 f2 f3 with L updated_by f4 =
     kripke_structure f f0 f1 f2 (f4 f3)

B_SEM_tupled_primitive_def

|- B_SEM_tupled =
   WFREC
     (@R.
        WF R /\ (!b l. R (l,b) (l, ~b)) /\
        (!b2 b1 l. R (l,b1) (l,B_AND (b1,b2))) /\
        !b1 b2 l. R (l,b2) (l,B_AND (b1,b2)))
     (\B_SEM_tupled a.
        case a of
           (l,T) -> I T
        || (l,B_PROP p) -> I (p IN l)
        || (l, ~b) -> I ~B_SEM_tupled (l,b)
        || (l,B_AND (b1,b2)) ->
             I (B_SEM_tupled (l,b1) /\ B_SEM_tupled (l,b2)))

B_SEM_curried_def

|- !x x1. B_SEM x x1 = B_SEM_tupled (x,x1)

path_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0.
          !'path'.
            (!a0.
               (?a.
                  a0 =
                  (\a. ind_type$CONSTR 0 (a, @v. T) (\n. ind_type$BOTTOM))
                    a) \/
               (?a.
                  a0 =
                  (\a.
                     ind_type$CONSTR (SUC 0) ((@v. T),a)
                       (\n. ind_type$BOTTOM)) a) ==>
               'path' a0) ==>
            'path' a0) rep

path_repfns

|- (!a. mk_path (dest_path a) = a) /\
   !r.
     (\a0.
        !'path'.
          (!a0.
             (?a.
                a0 =
                (\a. ind_type$CONSTR 0 (a, @v. T) (\n. ind_type$BOTTOM)) a) \/
             (?a.
                a0 =
                (\a.
                   ind_type$CONSTR (SUC 0) ((@v. T),a) (\n. ind_type$BOTTOM))
                  a) ==>
             'path' a0) ==>
          'path' a0) r =
     (dest_path (mk_path r) = r)

ctl18_def

|- ctl18 =
   (\a. mk_path ((\a. ind_type$CONSTR 0 (a, @v. T) (\n. ind_type$BOTTOM)) a))

ctl19_def

|- ctl19 =
   (\a.
      mk_path
        ((\a. ind_type$CONSTR (SUC 0) ((@v. T),a) (\n. ind_type$BOTTOM)) a))

FINITE

|- FINITE = ctl18

INFINITE

|- INFINITE = ctl19

path_case_def

|- (!f f1 a. path_case f f1 (FINITE a) = f a) /\
   !f f1 a. path_case f f1 (INFINITE a) = f1 a

path_size_def

|- (!f a. path_size f (FINITE a) = 1 + list_size f a) /\
   !f a. path_size f (INFINITE a) = 1

IS_FINITE_def

|- (!p. IS_FINITE (FINITE p) = T) /\ !f. IS_FINITE (INFINITE f) = F

IS_INFINITE_def

|- (!p. IS_INFINITE (FINITE p) = F) /\ !f. IS_INFINITE (INFINITE f) = T

HEAD_def

|- (!p. HEAD (FINITE p) = HD p) /\ !f. HEAD (INFINITE f) = f 0

REST_def

|- (!p. REST (FINITE p) = FINITE (TL p)) /\
   !f. REST (INFINITE f) = INFINITE (\n. f (n + 1))

RESTN_def

|- (!p. RESTN p 0 = p) /\ !p n. RESTN p (SUC n) = RESTN (REST p) n

ELEM_def

|- !p n. ELEM p n = HEAD (RESTN p n)

xnum_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0.
          !'xnum'.
            (!a0.
               (a0 = ind_type$CONSTR 0 (@v. T) (\n. ind_type$BOTTOM)) \/
               (?a.
                  a0 =
                  (\a. ind_type$CONSTR (SUC 0) a (\n. ind_type$BOTTOM)) a) ==>
               'xnum' a0) ==>
            'xnum' a0) rep

xnum_repfns

|- (!a. mk_xnum (dest_xnum a) = a) /\
   !r.
     (\a0.
        !'xnum'.
          (!a0.
             (a0 = ind_type$CONSTR 0 (@v. T) (\n. ind_type$BOTTOM)) \/
             (?a.
                a0 =
                (\a. ind_type$CONSTR (SUC 0) a (\n. ind_type$BOTTOM)) a) ==>
             'xnum' a0) ==>
          'xnum' a0) r =
     (dest_xnum (mk_xnum r) = r)

ctl20_def

|- ctl20 = mk_xnum (ind_type$CONSTR 0 (@v. T) (\n. ind_type$BOTTOM))

ctl21_def

|- ctl21 =
   (\a. mk_xnum ((\a. ind_type$CONSTR (SUC 0) a (\n. ind_type$BOTTOM)) a))

INFINITY

|- INFINITY = ctl20

XNUM

|- XNUM = ctl21

xnum_case_def

|- (!v f. xnum_case v f INFINITY = v) /\ !v f a. xnum_case v f (XNUM a) = f a

xnum_size_def

|- (xnum_size INFINITY = 0) /\ !a. xnum_size (XNUM a) = 1 + a

num_to_def

|- !m n i. (m to n) i = m <= i /\ i < n

xnum_to_def

|- (!m n i. (m to XNUM n) i = m <= i /\ i < n) /\
   !m i. (m to INFINITY) i = m <= i

SUB_num_xnum_def

|- !m n. m - XNUM n = XNUM (m - n)

SUB_xnum_num_def

|- !m n. XNUM m - n = XNUM (m - n)

SUB_xnum_xnum_tupled_primitive_def

|- SUB_xnum_xnum_tupled =
   WFREC (@R. WF R)
     (\SUB_xnum_xnum_tupled a.
        case a of
           (INFINITY,INFINITY) -> ARB
        || (INFINITY,XNUM n') -> I INFINITY
        || (XNUM m,INFINITY) -> ARB
        || (XNUM m,XNUM n) -> I (XNUM (m - n)))

SUB_xnum_xnum_curried_def

|- !x x1. x - x1 = SUB_xnum_xnum_tupled (x,x1)

LS_num_xnum_def

|- (!m n. m < XNUM n = m < n) /\ !m. m < INFINITY = T

LS_xnum_num_def

|- (!m n. XNUM m < n = m < n) /\ !n. INFINITY < n = F

LS_xnum_xnum_tupled_primitive_def

|- LS_xnum_xnum_tupled =
   WFREC (@R. WF R)
     (\LS_xnum_xnum_tupled a.
        case a of
           (INFINITY,v1) -> ARB
        || (XNUM m,INFINITY) -> ARB
        || (XNUM m,XNUM n) -> I (m < n))

LS_xnum_xnum_curried_def

|- !x x1. x < x1 = LS_xnum_xnum_tupled (x,x1)

GT_num_xnum_def

|- (!m n. m > XNUM n = m > n) /\ !m. m > INFINITY = F

GT_xnum_num_def

|- (!m n. XNUM m > n = m > n) /\ !n. INFINITY > n = T

GT_xnum_xnum_tupled_primitive_def

|- GT_xnum_xnum_tupled =
   WFREC (@R. WF R)
     (\GT_xnum_xnum_tupled a.
        case a of
           (INFINITY,v1) -> ARB
        || (XNUM m,INFINITY) -> ARB
        || (XNUM m,XNUM n) -> I (m > n))

GT_xnum_xnum_curried_def

|- !x x1. x > x1 = GT_xnum_xnum_tupled (x,x1)

PLENGTH_def

|- (!l. PLENGTH (FINITE l) = XNUM (LENGTH l)) /\
   !p. PLENGTH (INFINITE p) = INFINITY

PATH_def

|- !M p s.
     PATH M p s =
     IS_INFINITE p /\ (ELEM p 0 = s) /\ !n. M.R (ELEM p n,ELEM p (n + 1))

C_SEM_UNION_AUX_def

|- !R.
     C_SEM_UNION_aux R =
     WFREC R
       (\C_SEM_UNION a'.
          case a' of
             INL (M,C_BOOL b,s) -> I (B_SEM (M.L s) b)
          || INL (M, ~f,s) -> I ~C_SEM_UNION (INL (M,f,s))
          || INL (M,C_AND (f1,f2),s) ->
               I (C_SEM_UNION (INL (M,f1,s)) /\ C_SEM_UNION (INL (M,f2,s)))
          || INL (M,C_EX f',s) ->
               I
                 (C_SEM_UNION
                    (INR (INL (M,(\a. C_SEM_UNION (INL (M,f',a))),s))))
          || INL (M,C_EU (f1',f2'),s) ->
               I
                 (C_SEM_UNION
                    (INR
                       (INR
                          (INL
                             (M,
                              ((\a. C_SEM_UNION (INL (M,f1',a))),
                               (\a. C_SEM_UNION (INL (M,f2',a)))),s)))))
          || INL (M,C_EG f'',s) ->
               I
                 (C_SEM_UNION
                    (INR (INR (INR (M,(\a. C_SEM_UNION (INL (M,f'',a))),s)))))
          || INR (INL (M',X,s')) -> I (?p. PATH M' p s' /\ ELEM p 1 IN X)
          || INR (INR (INL (M'',(X1,X2),s''))) ->
               I
                 (?p.
                    PATH M'' p s'' /\
                    ?k::0 to PLENGTH p.
                      ELEM p k IN X2 /\ !j. j < k ==> ELEM p j IN X1)
          || INR (INR (INR (M''',X',s'''))) ->
               I ?p. PATH M''' p s''' /\ !j::0 to PLENGTH p. ELEM p j IN X')

C_SEM_UNION_primitive_def

|- C_SEM_UNION =
   C_SEM_UNION_aux
     @R.
       WF R /\ (!s f M. R (INL (M,f,s)) (INL (M, ~f,s))) /\
       (!f1 s f2 M. R (INL (M,f2,s)) (INL (M,C_AND (f1,f2),s))) /\
       (!f2 s f1 M. R (INL (M,f1,s)) (INL (M,C_AND (f1,f2),s))) /\
       (!s f M.
          R (INR (INL (M,(\a. C_SEM_UNION_aux R (INL (M,f,a))),s)))
            (INL (M,C_EX f,s))) /\
       (!s f M a. R (INL (M,f,a)) (INL (M,C_EX f,s))) /\
       (!s f2 f1 M.
          R
            (INR
               (INR
                  (INL
                     (M,
                      ((\a. C_SEM_UNION_aux R (INL (M,f1,a))),
                       (\a. C_SEM_UNION_aux R (INL (M,f2,a)))),s))))
            (INL (M,C_EU (f1,f2),s))) /\
       (!s f1 f2 M a. R (INL (M,f2,a)) (INL (M,C_EU (f1,f2),s))) /\
       (!s f2 f1 M a. R (INL (M,f1,a)) (INL (M,C_EU (f1,f2),s))) /\
       (!s f M a. R (INL (M,f,a)) (INL (M,C_EG f,s))) /\
       !s f M.
         R (INR (INR (INR (M,(\a. C_SEM_UNION_aux R (INL (M,f,a))),s))))
           (INL (M,C_EG f,s))

C_SEM_UNION_extract3_def

|- !x x1 x2. CEG x x1 x2 = C_SEM_UNION (INR (INR (INR (x,x1,x2))))

C_SEM_UNION_extract2_def

|- !x x1 x2. CEU x x1 x2 = C_SEM_UNION (INR (INR (INL (x,x1,x2))))

C_SEM_UNION_extract1_def

|- !x x1 x2. CEX x x1 x2 = C_SEM_UNION (INR (INL (x,x1,x2)))

C_SEM_UNION_extract0_def

|- !x x1 x2. C_SEM x x1 x2 = C_SEM_UNION (INL (x,x1,x2))

CTL_MODEL_SAT_def

|- !M f. CTL_MODEL_SAT M f = !s. s IN M.S0 ==> C_SEM M f s

C_AX_def

|- !f. C_AX f = ~C_EX ~f

C_EF_def

|- !f. C_EF f = C_EU (C_BOOL T,f)

C_AF_def

|- !f. C_AF f = ~C_EG ~f

C_AG_def

|- !f. C_AG f = ~C_EF ~f

C_AU_def

|- !f1 f2. C_AU (f1,f2) = C_AND (~C_EU (~f2,C_AND (~f1, ~f2)), ~C_EG ~f2)

C_AR_def

|- !f g. C_AR (f,g) = ~C_EU (~f, ~g)

C_OR_def

|- !f1 f2. C_OR (f1,f2) = ~C_AND (~f1, ~f2)

C_IMP_def

|- !f g. C_IMP (f,g) = C_OR (~f,g)

C_IFF_def

|- !f g. (f = g) = C_AND (C_IMP (f,g),C_IMP (g,f))

B_IMP_def

|- !f g. B_IMP (f,g) = B_OR (~f,g)

B_IFF_def

|- !f g. (f = g) = B_AND (B_IMP (f,g),B_IMP (g,f))

B_AND2_def

|- !f g. f /\ g = B_AND (f,g)

B_OR2_def

|- !f g. f \/ g = B_OR (f,g)

C_AND2_def

|- !f g. f /\ g = C_AND (f,g)

C_OR2_def

|- !f g. f \/ g = C_OR (f,g)

C_IMP2_def

|- !f g. f ==> g = C_IMP (f,g)

B_IMP2_def

|- !f g. f ==> g = B_IMP (f,g)

BEXP_NNF_primitive_def

|- BEXP_NNF =
   WFREC
     (@R.
        WF R /\ (!b1 b2. R b2 (B_AND (b1,b2))) /\
        (!b2 b1. R b1 (B_AND (b1,b2))) /\ (!b. R b ~ ~b) /\
        (!b2 b1. R (~b1) ~B_AND (b1,b2)) /\ !b1 b2. R (~b2) ~B_AND (b1,b2))
     (\BEXP_NNF a.
        case a of
           T -> I T
        || B_PROP p -> I (B_PROP p)
        || ~T -> I F
        || ~B_PROP p' -> I ~B_PROP p'
        || ~ ~b -> I (BEXP_NNF b)
        || ~B_AND (b1',b2') -> I (B_OR (BEXP_NNF ~b1',BEXP_NNF ~b2'))
        || B_AND (b1,b2) -> I (B_AND (BEXP_NNF b1,BEXP_NNF b2)))

CTL_NNF_primitive_def

|- CTL_NNF =
   WFREC
     (@R.
        WF R /\ (!f g. R g (C_AND (f,g))) /\ (!g f. R f (C_AND (f,g))) /\
        (!f. R f (C_EX f)) /\ (!f. R f (C_EG f)) /\
        (!f g. R g (C_EU (f,g))) /\ (!g f. R f (C_EU (f,g))) /\
        (!f g. R (~g) ~C_AND (f,g)) /\ (!g f. R (~f) ~C_AND (f,g)) /\
        (!f. R f ~ ~f) /\ (!f. R (~f) ~C_EX f) /\ (!f. R (~f) ~C_EG f) /\
        (!g f. R (~f) ~C_EU (f,g)) /\ !f g. R (~g) ~C_EU (f,g))
     (\CTL_NNF a.
        case a of
           C_BOOL b -> I (C_BOOL b)
        || ~C_BOOL b' -> I (C_BOOL (BEXP_NNF ~b'))
        || ~ ~f''''' -> I (CTL_NNF f''''')
        || ~C_AND (f'''',g'') -> I (C_OR (CTL_NNF ~f'''',CTL_NNF ~g''))
        || ~C_EX f'''''' -> I (C_AX (CTL_NNF ~f''''''))
        || ~C_EU (f'''''''',g''') ->
             I (C_AR (CTL_NNF ~f'''''''',CTL_NNF ~g'''))
        || ~C_EG f''''''' -> I (C_AF (CTL_NNF ~f'''''''))
        || C_AND (f,g) -> I (C_AND (CTL_NNF f,CTL_NNF g))
        || C_EX f' -> I (C_EX (CTL_NNF f'))
        || C_EU (f''',g') -> I (C_EU (CTL_NNF f''',CTL_NNF g'))
        || C_EG f'' -> I (C_EG (CTL_NNF f'')))

ctl_size2_def

|- !f. ctl_size2 f = ctl_size (\a. 0) f

bexp_size2_def

|- !b. bexp_size2 b = bexp_size (\a. 0) b

bexp_pstv_size_primitive_def

|- bexp_pstv_size =
   WFREC
     (@R.
        WF R /\ (!b1 b2. R b2 (B_AND (b1,b2))) /\
        (!b2 b1. R b1 (B_AND (b1,b2))) /\ !b. R b ~b)
     (\bexp_pstv_size a.
        case a of
           T -> I 0
        || B_PROP p -> I 1
        || ~b -> I (bexp_pstv_size b)
        || B_AND (b1,b2) -> I (1 + bexp_pstv_size b1 + bexp_pstv_size b2))

ctl_pstv_size_primitive_def

|- ctl_pstv_size =
   WFREC
     (@R.
        WF R /\ (!f1 f2. R f2 (C_AND (f1,f2))) /\
        (!f2 f1. R f1 (C_AND (f1,f2))) /\ (!f. R f ~f) /\
        (!f. R f (C_EX f)) /\ (!f. R f (C_EG f)) /\
        (!f2 f1. R f1 (C_EU (f1,f2))) /\ !f1 f2. R f2 (C_EU (f1,f2)))
     (\ctl_pstv_size a.
        case a of
           C_BOOL b -> I (1 + bexp_pstv_size b)
        || ~f -> I (ctl_pstv_size f)
        || C_AND (f1,f2) -> I (1 + ctl_pstv_size f1 + ctl_pstv_size f2)
        || C_EX f' -> I (1 + ctl_pstv_size f')
        || C_EU (f1',f2') -> I (1 + ctl_pstv_size f1' + ctl_pstv_size f2')
        || C_EG f'' -> I (1 + ctl_pstv_size f''))

CTL_BOOL_SUB_tupled_primitive_def

|- CTL_BOOL_SUB_tupled =
   WFREC
     (@R.
        WF R /\ (!be1 g. R (g,be1) (g, ~be1)) /\
        (!be2 be1 g. R (g,be1) (g,B_AND (be1,be2))) /\
        !be1 be2 g. R (g,be2) (g,B_AND (be1,be2)))
     (\CTL_BOOL_SUB_tupled a.
        case a of
           (g,T) -> ARB
        || (g,B_PROP b) -> I (g = B_PROP b)
        || (g, ~be1) -> I (CTL_BOOL_SUB_tupled (g,be1) \/ (g = ~be1))
        || (g,B_AND (be1',be2)) ->
             I
               (CTL_BOOL_SUB_tupled (g,be1') \/ CTL_BOOL_SUB_tupled (g,be2) \/
                (g = B_AND (be1',be2))))

CTL_BOOL_SUB_curried_def

|- !x x1. CTL_BOOL_SUB x x1 = CTL_BOOL_SUB_tupled (x,x1)

CTL_SUB_tupled_primitive_def

|- CTL_SUB_tupled =
   WFREC
     (@R.
        WF R /\ (!f1 f2 g. R (g,f2) (g,C_AND (f1,f2))) /\
        (!f2 f1 g. R (g,f1) (g,C_AND (f1,f2))) /\ (!f g. R (g,f) (g, ~f)) /\
        (!f g. R (g,f) (g,C_EX f)) /\ (!f g. R (g,f) (g,C_EG f)) /\
        (!f2 f1 g. R (g,f1) (g,C_EU (f1,f2))) /\
        !f1 f2 g. R (g,f2) (g,C_EU (f1,f2)))
     (\CTL_SUB_tupled a.
        case a of
           (g,C_BOOL b) -> I (?b'. (g = C_BOOL b') /\ CTL_BOOL_SUB b' b)
        || (g, ~f) -> I (CTL_SUB_tupled (g,f) \/ (g = ~f))
        || (g,C_AND (f1,f2)) ->
             I
               (CTL_SUB_tupled (g,f1) \/ CTL_SUB_tupled (g,f2) \/
                (g = C_AND (f1,f2)))
        || (g,C_EX f') -> I (CTL_SUB_tupled (g,f') \/ (g = C_EX f'))
        || (g,C_EU (f1',f2')) ->
             I
               (CTL_SUB_tupled (g,f1') \/ CTL_SUB_tupled (g,f2') \/
                (g = C_EU (f1',f2')))
        || (g,C_EG f'') -> I (CTL_SUB_tupled (g,f'') \/ (g = C_EG f'')))

CTL_SUB_curried_def

|- !x x1. CTL_SUB x x1 = CTL_SUB_tupled (x,x1)

IS_ACTL_def

|- !f.
     IS_ACTL f =
     (!g. ~CTL_SUB (C_EX g) (CTL_NNF f)) /\
     (!g. ~CTL_SUB (C_EG g) (CTL_NNF f)) /\
     !g1 g2. ~CTL_SUB (C_EU (g1,g2)) (CTL_NNF f)

Theorems

datatype_bexp

|- DATATYPE (bexp T B_PROP $~ B_AND)

bexp_11

|- (!a a'. (B_PROP a = B_PROP a') = (a = a')) /\
   (!a a'. (~a = ~a') = (a = a')) /\ !a a'. (B_AND a = B_AND a') = (a = a')

bexp_distinct

|- (!a. ~(T = B_PROP a)) /\ (!a. ~(T = ~a)) /\ (!a. ~(T = B_AND a)) /\
   (!a' a. ~(B_PROP a = ~a')) /\ (!a' a. ~(B_PROP a = B_AND a')) /\
   !a' a. ~(~a = B_AND a')

bexp_case_cong

|- !M M' v f f1 f2.
     (M = M') /\ ((M' = T) ==> (v = v')) /\
     (!a. (M' = B_PROP a) ==> (f a = f' a)) /\
     (!a. (M' = ~a) ==> (f1 a = f1' a)) /\
     (!a. (M' = B_AND a) ==> (f2 a = f2' a)) ==>
     (bexp_case v f f1 f2 M = bexp_case v' f' f1' f2' M')

bexp_nchotomy

|- !b. (b = T) \/ (?a. b = B_PROP a) \/ (?b'. b = ~b') \/ ?p. b = B_AND p

bexp_Axiom

|- !f0 f1 f2 f3 f4.
     ?fn0 fn1.
       (fn0 T = f0) /\ (!a. fn0 (B_PROP a) = f1 a) /\
       (!a. fn0 ~a = f2 a (fn0 a)) /\ (!a. fn0 (B_AND a) = f3 a (fn1 a)) /\
       !a0 a1. fn1 (a0,a1) = f4 a0 a1 (fn0 a0) (fn0 a1)

bexp_induction

|- !P0 P1.
     P0 T /\ (!a. P0 (B_PROP a)) /\ (!b. P0 b ==> P0 ~b) /\
     (!p. P1 p ==> P0 (B_AND p)) /\ (!b b0. P0 b /\ P0 b0 ==> P1 (b,b0)) ==>
     (!b. P0 b) /\ !p. P1 p

datatype_ctl

|- DATATYPE (ctl C_BOOL $~ C_AND C_EX C_EU C_EG)

ctl_11

|- (!a a'. (C_BOOL a = C_BOOL a') = (a = a')) /\
   (!a a'. (~a = ~a') = (a = a')) /\
   (!a a'. (C_AND a = C_AND a') = (a = a')) /\
   (!a a'. (C_EX a = C_EX a') = (a = a')) /\
   (!a a'. (C_EU a = C_EU a') = (a = a')) /\
   !a a'. (C_EG a = C_EG a') = (a = a')

ctl_distinct

|- (!a' a. ~(C_BOOL a = ~a')) /\ (!a' a. ~(C_BOOL a = C_AND a')) /\
   (!a' a. ~(C_BOOL a = C_EX a')) /\ (!a' a. ~(C_BOOL a = C_EU a')) /\
   (!a' a. ~(C_BOOL a = C_EG a')) /\ (!a' a. ~(~a = C_AND a')) /\
   (!a' a. ~(~a = C_EX a')) /\ (!a' a. ~(~a = C_EU a')) /\
   (!a' a. ~(~a = C_EG a')) /\ (!a' a. ~(C_AND a = C_EX a')) /\
   (!a' a. ~(C_AND a = C_EU a')) /\ (!a' a. ~(C_AND a = C_EG a')) /\
   (!a' a. ~(C_EX a = C_EU a')) /\ (!a' a. ~(C_EX a = C_EG a')) /\
   !a' a. ~(C_EU a = C_EG a')

ctl_case_cong

|- !M M' f f1 f2 f3 f4 f5.
     (M = M') /\ (!a. (M' = C_BOOL a) ==> (f a = f' a)) /\
     (!a. (M' = ~a) ==> (f1 a = f1' a)) /\
     (!a. (M' = C_AND a) ==> (f2 a = f2' a)) /\
     (!a. (M' = C_EX a) ==> (f3 a = f3' a)) /\
     (!a. (M' = C_EU a) ==> (f4 a = f4' a)) /\
     (!a. (M' = C_EG a) ==> (f5 a = f5' a)) ==>
     (ctl_case f f1 f2 f3 f4 f5 M = ctl_case f' f1' f2' f3' f4' f5' M')

ctl_nchotomy

|- !c.
     (?b. c = C_BOOL b) \/ (?c'. c = ~c') \/ (?p. c = C_AND p) \/
     (?c'. c = C_EX c') \/ (?p. c = C_EU p) \/ ?c'. c = C_EG c'

ctl_Axiom

|- !f0 f1 f2 f3 f4 f5 f6.
     ?fn0 fn1.
       (!a. fn0 (C_BOOL a) = f0 a) /\ (!a. fn0 ~a = f1 a (fn0 a)) /\
       (!a. fn0 (C_AND a) = f2 a (fn1 a)) /\
       (!a. fn0 (C_EX a) = f3 a (fn0 a)) /\
       (!a. fn0 (C_EU a) = f4 a (fn1 a)) /\
       (!a. fn0 (C_EG a) = f5 a (fn0 a)) /\
       !a0 a1. fn1 (a0,a1) = f6 a0 a1 (fn0 a0) (fn0 a1)

ctl_induction

|- !P0 P1.
     (!b. P0 (C_BOOL b)) /\ (!c. P0 c ==> P0 ~c) /\
     (!p. P1 p ==> P0 (C_AND p)) /\ (!c. P0 c ==> P0 (C_EX c)) /\
     (!p. P1 p ==> P0 (C_EU p)) /\ (!c. P0 c ==> P0 (C_EG c)) /\
     (!c c0. P0 c /\ P0 c0 ==> P1 (c,c0)) ==>
     (!c. P0 c) /\ !p. P1 p

kripke_structure_accessors

|- (!f f0 f1 f2 f3. (kripke_structure f f0 f1 f2 f3).S = f) /\
   (!f f0 f1 f2 f3. (kripke_structure f f0 f1 f2 f3).S0 = f0) /\
   (!f f0 f1 f2 f3. (kripke_structure f f0 f1 f2 f3).R = f1) /\
   (!f f0 f1 f2 f3. (kripke_structure f f0 f1 f2 f3).P = f2) /\
   !f f0 f1 f2 f3. (kripke_structure f f0 f1 f2 f3).L = f3

kripke_structure_fn_updates

|- (!f4 f f0 f1 f2 f3.
      kripke_structure f f0 f1 f2 f3 with S updated_by f4 =
      kripke_structure (f4 f) f0 f1 f2 f3) /\
   (!f4 f f0 f1 f2 f3.
      kripke_structure f f0 f1 f2 f3 with S0 updated_by f4 =
      kripke_structure f (f4 f0) f1 f2 f3) /\
   (!f4 f f0 f1 f2 f3.
      kripke_structure f f0 f1 f2 f3 with R updated_by f4 =
      kripke_structure f f0 (f4 f1) f2 f3) /\
   (!f4 f f0 f1 f2 f3.
      kripke_structure f f0 f1 f2 f3 with P updated_by f4 =
      kripke_structure f f0 f1 (f4 f2) f3) /\
   !f4 f f0 f1 f2 f3.
     kripke_structure f f0 f1 f2 f3 with L updated_by f4 =
     kripke_structure f f0 f1 f2 (f4 f3)

kripke_structure_accfupds

|- (!k f. (k with S0 updated_by f).S = k.S) /\
   (!k f. (k with R updated_by f).S = k.S) /\
   (!k f. (k with P updated_by f).S = k.S) /\
   (!k f. (k with L updated_by f).S = k.S) /\
   (!k f. (k with S updated_by f).S0 = k.S0) /\
   (!k f. (k with R updated_by f).S0 = k.S0) /\
   (!k f. (k with P updated_by f).S0 = k.S0) /\
   (!k f. (k with L updated_by f).S0 = k.S0) /\
   (!k f. (k with S updated_by f).R = k.R) /\
   (!k f. (k with S0 updated_by f).R = k.R) /\
   (!k f. (k with P updated_by f).R = k.R) /\
   (!k f. (k with L updated_by f).R = k.R) /\
   (!k f. (k with S updated_by f).P = k.P) /\
   (!k f. (k with S0 updated_by f).P = k.P) /\
   (!k f. (k with R updated_by f).P = k.P) /\
   (!k f. (k with L updated_by f).P = k.P) /\
   (!k f. (k with S updated_by f).L = k.L) /\
   (!k f. (k with S0 updated_by f).L = k.L) /\
   (!k f. (k with R updated_by f).L = k.L) /\
   (!k f. (k with P updated_by f).L = k.L) /\
   (!k f. (k with S updated_by f).S = f k.S) /\
   (!k f. (k with S0 updated_by f).S0 = f k.S0) /\
   (!k f. (k with R updated_by f).R = f k.R) /\
   (!k f. (k with P updated_by f).P = f k.P) /\
   !k f. (k with L updated_by f).L = f k.L

kripke_structure_fupdfupds

|- (!k g f.
      k with <|S updated_by f; S updated_by g|> =
      k with S updated_by f o g) /\
   (!k g f.
      k with <|S0 updated_by f; S0 updated_by g|> =
      k with S0 updated_by f o g) /\
   (!k g f.
      k with <|R updated_by f; R updated_by g|> =
      k with R updated_by f o g) /\
   (!k g f.
      k with <|P updated_by f; P updated_by g|> =
      k with P updated_by f o g) /\
   !k g f.
     k with <|L updated_by f; L updated_by g|> = k with L updated_by f o g

kripke_structure_fupdfupds_comp

|- ((!g f.
       kripke_structure_S_fupd f o kripke_structure_S_fupd g =
       kripke_structure_S_fupd (f o g)) /\
    !h g f.
      kripke_structure_S_fupd f o kripke_structure_S_fupd g o h =
      kripke_structure_S_fupd (f o g) o h) /\
   ((!g f.
       kripke_structure_S0_fupd f o kripke_structure_S0_fupd g =
       kripke_structure_S0_fupd (f o g)) /\
    !h g f.
      kripke_structure_S0_fupd f o kripke_structure_S0_fupd g o h =
      kripke_structure_S0_fupd (f o g) o h) /\
   ((!g f.
       kripke_structure_R_fupd f o kripke_structure_R_fupd g =
       kripke_structure_R_fupd (f o g)) /\
    !h g f.
      kripke_structure_R_fupd f o kripke_structure_R_fupd g o h =
      kripke_structure_R_fupd (f o g) o h) /\
   ((!g f.
       kripke_structure_P_fupd f o kripke_structure_P_fupd g =
       kripke_structure_P_fupd (f o g)) /\
    !h g f.
      kripke_structure_P_fupd f o kripke_structure_P_fupd g o h =
      kripke_structure_P_fupd (f o g) o h) /\
   (!g f.
      kripke_structure_L_fupd f o kripke_structure_L_fupd g =
      kripke_structure_L_fupd (f o g)) /\
   !h g f.
     kripke_structure_L_fupd f o kripke_structure_L_fupd g o h =
     kripke_structure_L_fupd (f o g) o h

kripke_structure_fupdcanon

|- (!k g f.
      k with <|S0 updated_by f; S updated_by g|> =
      k with <|S updated_by g; S0 updated_by f|>) /\
   (!k g f.
      k with <|R updated_by f; S updated_by g|> =
      k with <|S updated_by g; R updated_by f|>) /\
   (!k g f.
      k with <|R updated_by f; S0 updated_by g|> =
      k with <|S0 updated_by g; R updated_by f|>) /\
   (!k g f.
      k with <|P updated_by f; S updated_by g|> =
      k with <|S updated_by g; P updated_by f|>) /\
   (!k g f.
      k with <|P updated_by f; S0 updated_by g|> =
      k with <|S0 updated_by g; P updated_by f|>) /\
   (!k g f.
      k with <|P updated_by f; R updated_by g|> =
      k with <|R updated_by g; P updated_by f|>) /\
   (!k g f.
      k with <|L updated_by f; S updated_by g|> =
      k with <|S updated_by g; L updated_by f|>) /\
   (!k g f.
      k with <|L updated_by f; S0 updated_by g|> =
      k with <|S0 updated_by g; L updated_by f|>) /\
   (!k g f.
      k with <|L updated_by f; R updated_by g|> =
      k with <|R updated_by g; L updated_by f|>) /\
   !k g f.
     k with <|L updated_by f; P updated_by g|> =
     k with <|P updated_by g; L updated_by f|>

kripke_structure_fupdcanon_comp

|- ((!g f.
       kripke_structure_S0_fupd f o kripke_structure_S_fupd g =
       kripke_structure_S_fupd g o kripke_structure_S0_fupd f) /\
    !h g f.
      kripke_structure_S0_fupd f o kripke_structure_S_fupd g o h =
      kripke_structure_S_fupd g o kripke_structure_S0_fupd f o h) /\
   ((!g f.
       kripke_structure_R_fupd f o kripke_structure_S_fupd g =
       kripke_structure_S_fupd g o kripke_structure_R_fupd f) /\
    !h g f.
      kripke_structure_R_fupd f o kripke_structure_S_fupd g o h =
      kripke_structure_S_fupd g o kripke_structure_R_fupd f o h) /\
   ((!g f.
       kripke_structure_R_fupd f o kripke_structure_S0_fupd g =
       kripke_structure_S0_fupd g o kripke_structure_R_fupd f) /\
    !h g f.
      kripke_structure_R_fupd f o kripke_structure_S0_fupd g o h =
      kripke_structure_S0_fupd g o kripke_structure_R_fupd f o h) /\
   ((!g f.
       kripke_structure_P_fupd f o kripke_structure_S_fupd g =
       kripke_structure_S_fupd g o kripke_structure_P_fupd f) /\
    !h g f.
      kripke_structure_P_fupd f o kripke_structure_S_fupd g o h =
      kripke_structure_S_fupd g o kripke_structure_P_fupd f o h) /\
   ((!g f.
       kripke_structure_P_fupd f o kripke_structure_S0_fupd g =
       kripke_structure_S0_fupd g o kripke_structure_P_fupd f) /\
    !h g f.
      kripke_structure_P_fupd f o kripke_structure_S0_fupd g o h =
      kripke_structure_S0_fupd g o kripke_structure_P_fupd f o h) /\
   ((!g f.
       kripke_structure_P_fupd f o kripke_structure_R_fupd g =
       kripke_structure_R_fupd g o kripke_structure_P_fupd f) /\
    !h g f.
      kripke_structure_P_fupd f o kripke_structure_R_fupd g o h =
      kripke_structure_R_fupd g o kripke_structure_P_fupd f o h) /\
   ((!g f.
       kripke_structure_L_fupd f o kripke_structure_S_fupd g =
       kripke_structure_S_fupd g o kripke_structure_L_fupd f) /\
    !h g f.
      kripke_structure_L_fupd f o kripke_structure_S_fupd g o h =
      kripke_structure_S_fupd g o kripke_structure_L_fupd f o h) /\
   ((!g f.
       kripke_structure_L_fupd f o kripke_structure_S0_fupd g =
       kripke_structure_S0_fupd g o kripke_structure_L_fupd f) /\
    !h g f.
      kripke_structure_L_fupd f o kripke_structure_S0_fupd g o h =
      kripke_structure_S0_fupd g o kripke_structure_L_fupd f o h) /\
   ((!g f.
       kripke_structure_L_fupd f o kripke_structure_R_fupd g =
       kripke_structure_R_fupd g o kripke_structure_L_fupd f) /\
    !h g f.
      kripke_structure_L_fupd f o kripke_structure_R_fupd g o h =
      kripke_structure_R_fupd g o kripke_structure_L_fupd f o h) /\
   (!g f.
      kripke_structure_L_fupd f o kripke_structure_P_fupd g =
      kripke_structure_P_fupd g o kripke_structure_L_fupd f) /\
   !h g f.
     kripke_structure_L_fupd f o kripke_structure_P_fupd g o h =
     kripke_structure_P_fupd g o kripke_structure_L_fupd f o h

kripke_structure_component_equality

|- !k1 k2.
     (k1 = k2) =
     (k1.S = k2.S) /\ (k1.S0 = k2.S0) /\ (k1.R = k2.R) /\ (k1.P = k2.P) /\
     (k1.L = k2.L)

kripke_structure_updates_eq_literal

|- !k f3 f2 f1 f0 f.
     k with <|S := f3; S0 := f2; R := f1; P := f0; L := f|> =
     <|S := f3; S0 := f2; R := f1; P := f0; L := f|>

kripke_structure_literal_nchotomy

|- !k. ?f3 f2 f1 f0 f. k = <|S := f3; S0 := f2; R := f1; P := f0; L := f|>

FORALL_kripke_structure

|- !P.
     (!k. P k) =
     !f3 f2 f1 f0 f. P <|S := f3; S0 := f2; R := f1; P := f0; L := f|>

EXISTS_kripke_structure

|- !P.
     (?k. P k) =
     ?f3 f2 f1 f0 f. P <|S := f3; S0 := f2; R := f1; P := f0; L := f|>

kripke_structure_literal_11

|- !f31 f21 f11 f01 f1 f32 f22 f12 f02 f2.
     (<|S := f31; S0 := f21; R := f11; P := f01; L := f1|> =
      <|S := f32; S0 := f22; R := f12; P := f02; L := f2|>) =
     (f31 = f32) /\ (f21 = f22) /\ (f11 = f12) /\ (f01 = f02) /\ (f1 = f2)

datatype_kripke_structure

|- DATATYPE (record kripke_structure S S0 R P L)

kripke_structure_11

|- !a0 a1 a2 a3 a4 a0' a1' a2' a3' a4'.
     (kripke_structure a0 a1 a2 a3 a4 =
      kripke_structure a0' a1' a2' a3' a4') =
     (a0 = a0') /\ (a1 = a1') /\ (a2 = a2') /\ (a3 = a3') /\ (a4 = a4')

kripke_structure_case_cong

|- !M M' f.
     (M = M') /\
     (!a0 a1 a2 a3 a4.
        (M' = kripke_structure a0 a1 a2 a3 a4) ==>
        (f a0 a1 a2 a3 a4 = f' a0 a1 a2 a3 a4)) ==>
     (kripke_structure_case f M = kripke_structure_case f' M')

kripke_structure_nchotomy

|- !k. ?f f0 f1 f2 f3. k = kripke_structure f f0 f1 f2 f3

kripke_structure_Axiom

|- !f.
     ?fn.
       !a0 a1 a2 a3 a4.
         fn (kripke_structure a0 a1 a2 a3 a4) = f a0 a1 a2 a3 a4

kripke_structure_induction

|- !P. (!f f0 f1 f2 f3. P (kripke_structure f f0 f1 f2 f3)) ==> !k. P k

B_SEM_ind

|- !P.
     (!l. P l T) /\ (!l p. P l (B_PROP p)) /\ (!l b. P l b ==> P l ~b) /\
     (!l b1 b2. P l b1 /\ P l b2 ==> P l (B_AND (b1,b2))) ==>
     !v v1. P v v1

B_SEM_def

|- (B_SEM l T = T) /\ (B_SEM l (B_PROP p) = p IN l) /\
   (B_SEM l ~b = ~B_SEM l b) /\
   (B_SEM l (B_AND (b1,b2)) = B_SEM l b1 /\ B_SEM l b2)

datatype_path

|- DATATYPE (path FINITE INFINITE)

path_11

|- (!a a'. (FINITE a = FINITE a') = (a = a')) /\
   !a a'. (INFINITE a = INFINITE a') = (a = a')

path_distinct

|- !a' a. ~(FINITE a = INFINITE a')

path_case_cong

|- !M M' f f1.
     (M = M') /\ (!a. (M' = FINITE a) ==> (f a = f' a)) /\
     (!a. (M' = INFINITE a) ==> (f1 a = f1' a)) ==>
     (path_case f f1 M = path_case f' f1' M')

path_nchotomy

|- !p. (?l. p = FINITE l) \/ ?f. p = INFINITE f

path_Axiom

|- !f0 f1. ?fn. (!a. fn (FINITE a) = f0 a) /\ !a. fn (INFINITE a) = f1 a

path_induction

|- !P. (!l. P (FINITE l)) /\ (!f. P (INFINITE f)) ==> !p. P p

NOT_IS_INFINITE

|- IS_INFINITE p = ~IS_FINITE p

NOT_IS_FINITE

|- IS_FINITE p = ~IS_INFINITE p

IS_INFINITE_REST

|- !p. IS_INFINITE (REST p) = IS_INFINITE p

IS_INFINITE_RESTN

|- !n p. IS_INFINITE (RESTN p n) = IS_INFINITE p

IS_FINITE_REST

|- !p. IS_FINITE (REST p) = IS_FINITE p

IS_FINITE_RESTN

|- !n p. IS_FINITE (RESTN p n) = IS_FINITE p

FINITE_TL

|- !l. 0 < LENGTH l ==> (FINITE (TL l) = REST (FINITE l))

datatype_xnum

|- DATATYPE (xnum INFINITY XNUM)

xnum_11

|- !a a'. (XNUM a = XNUM a') = (a = a')

xnum_distinct

|- !a. ~(INFINITY = XNUM a)

xnum_case_cong

|- !M M' v f.
     (M = M') /\ ((M' = INFINITY) ==> (v = v')) /\
     (!a. (M' = XNUM a) ==> (f a = f' a)) ==>
     (xnum_case v f M = xnum_case v' f' M')

xnum_nchotomy

|- !x. (x = INFINITY) \/ ?n. x = XNUM n

xnum_Axiom

|- !f0 f1. ?fn. (fn INFINITY = f0) /\ !a. fn (XNUM a) = f1 a

xnum_induction

|- !P. P INFINITY /\ (!n. P (XNUM n)) ==> !x. P x

SUB_xnum_xnum_ind

|- !P.
     (!m. P (XNUM m) INFINITY) /\ P INFINITY INFINITY /\
     (!m n. P (XNUM m) (XNUM n)) /\ (!n. P INFINITY (XNUM n)) ==>
     !v v1. P v v1

SUB_xnum_xnum_def

|- (XNUM m - XNUM n = XNUM (m - n)) /\ (INFINITY - XNUM n = INFINITY)

SUB

|- ((!v f. xnum_case v f INFINITY = v) /\
    !v f a. xnum_case v f (XNUM a) = f a) /\ (!a. ~(INFINITY = XNUM a)) /\
   (!a. ~(XNUM a = INFINITY)) /\ (!a a'. (XNUM a = XNUM a') = (a = a')) /\
   (!m n. m - XNUM n = XNUM (m - n)) /\ (!m n. XNUM m - n = XNUM (m - n)) /\
   (XNUM m - XNUM n = XNUM (m - n)) /\ (INFINITY - XNUM n = INFINITY)

LS_xnum_xnum_ind

|- !P.
     (!m. P (XNUM m) INFINITY) /\ (!v3. P INFINITY v3) /\
     (!m n. P (XNUM m) (XNUM n)) ==>
     !v v1. P v v1

LS_xnum_xnum_def

|- XNUM m < XNUM n = m < n

LS

|- ((!m n. m < XNUM n = m < n) /\ !m. m < INFINITY = T) /\
   ((!m n. XNUM m < n = m < n) /\ !n. INFINITY < n = F) /\
   (XNUM m < XNUM n = m < n)

GT_xnum_xnum_ind

|- !P.
     (!m. P (XNUM m) INFINITY) /\ (!v3. P INFINITY v3) /\
     (!m n. P (XNUM m) (XNUM n)) ==>
     !v v1. P v v1

GT_xnum_xnum_def

|- XNUM m > XNUM n = m > n

GT

|- ((!m n. m > XNUM n = m > n) /\ !m. m > INFINITY = F) /\
   ((!m n. XNUM m > n = m > n) /\ !n. INFINITY > n = T) /\
   (XNUM m > XNUM n = m > n)

ALL_IN_INF

|- !j. j IN 0 to INFINITY

PATH_INF

|- !M p s. PATH M p s ==> (PLENGTH p = INFINITY)

ALL_IN_INF_PATH

|- !M p s j. PATH M p s ==> j IN 0 to PLENGTH p

C_SEM_ind

|- !P0 P1 P2 P3.
     (!M b s. P0 M (C_BOOL b) s) /\ (!M f s. P0 M f s ==> P0 M (~f) s) /\
     (!M f1 f2 s. P0 M f1 s /\ P0 M f2 s ==> P0 M (C_AND (f1,f2)) s) /\
     (!M f s.
        (!a. P0 M f a) /\ P1 M (\a. C_SEM M f a) s ==> P0 M (C_EX f) s) /\
     (!M f1 f2 s.
        (!a. P0 M f1 a) /\ (!a. P0 M f2 a) /\
        P2 M ((\a. C_SEM M f1 a),(\a. C_SEM M f2 a)) s ==>
        P0 M (C_EU (f1,f2)) s) /\
     (!M f s.
        (!a. P0 M f a) /\ P3 M (\a. C_SEM M f a) s ==> P0 M (C_EG f) s) /\
     (!M X s. P1 M X s) /\ (!M X1 X2 s. P2 M (X1,X2) s) /\
     (!M X s. P3 M X s) ==>
     (!v0 v1 v2. P0 v0 v1 v2) /\ (!v0 v1 v2. P1 v0 v1 v2) /\
     (!v0 v1 v2. P2 v0 v1 v2) /\ !v0 v1 v2. P3 v0 v1 v2

C_SEM_def

|- (C_SEM M (C_BOOL b) s = B_SEM (M.L s) b) /\
   (C_SEM M (~f) s = ~C_SEM M f s) /\
   (C_SEM M (C_AND (f1,f2)) s = C_SEM M f1 s /\ C_SEM M f2 s) /\
   (C_SEM M (C_EX f) s = CEX M (\a. C_SEM M f a) s) /\
   (C_SEM M (C_EU (f1,f2)) s =
    CEU M ((\a. C_SEM M f1 a),(\a. C_SEM M f2 a)) s) /\
   (C_SEM M (C_EG f) s = CEG M (\a. C_SEM M f a) s) /\
   (CEX M X s = ?p. PATH M p s /\ ELEM p 1 IN X) /\
   (CEU M (X1,X2) s =
    ?p.
      PATH M p s /\
      ?k::0 to PLENGTH p. ELEM p k IN X2 /\ !j. j < k ==> ELEM p j IN X1) /\
   (CEG M X s = ?p. PATH M p s /\ !j::0 to PLENGTH p. ELEM p j IN X)

BEXP_NNF_ind

|- !P.
     P T /\ (!p. P (B_PROP p)) /\
     (!b1 b2. P b1 /\ P b2 ==> P (B_AND (b1,b2))) /\ P ~T /\
     (!p. P ~B_PROP p) /\ (!b. P b ==> P ~ ~b) /\
     (!b1 b2. P ~b1 /\ P ~b2 ==> P ~B_AND (b1,b2)) ==>
     !v. P v

BEXP_NNF_def

|- (BEXP_NNF T = T) /\ (BEXP_NNF (B_PROP p) = B_PROP p) /\
   (BEXP_NNF (B_AND (b1,b2)) = B_AND (BEXP_NNF b1,BEXP_NNF b2)) /\
   (BEXP_NNF ~T = F) /\ (BEXP_NNF ~B_PROP p = ~B_PROP p) /\
   (BEXP_NNF ~ ~b = BEXP_NNF b) /\
   (BEXP_NNF ~B_AND (b1,b2) = B_OR (BEXP_NNF ~b1,BEXP_NNF ~b2))

CTL_NNF_ind

|- !P.
     (!b. P (C_BOOL b)) /\ (!f g. P f /\ P g ==> P (C_AND (f,g))) /\
     (!f. P f ==> P (C_EX f)) /\ (!f. P f ==> P (C_EG f)) /\
     (!f g. P f /\ P g ==> P (C_EU (f,g))) /\ (!b. P ~C_BOOL b) /\
     (!f g. P ~f /\ P ~g ==> P ~C_AND (f,g)) /\ (!f. P f ==> P ~ ~f) /\
     (!f. P ~f ==> P ~C_EX f) /\ (!f. P ~f ==> P ~C_EG f) /\
     (!f g. P ~f /\ P ~g ==> P ~C_EU (f,g)) ==>
     !v. P v

CTL_NNF_def

|- (CTL_NNF (C_BOOL b) = C_BOOL b) /\
   (CTL_NNF (C_AND (f,g)) = C_AND (CTL_NNF f,CTL_NNF g)) /\
   (CTL_NNF (C_EX f) = C_EX (CTL_NNF f)) /\
   (CTL_NNF (C_EG f) = C_EG (CTL_NNF f)) /\
   (CTL_NNF (C_EU (f,g)) = C_EU (CTL_NNF f,CTL_NNF g)) /\
   (CTL_NNF ~C_BOOL b = C_BOOL (BEXP_NNF ~b)) /\
   (CTL_NNF ~C_AND (f,g) = C_OR (CTL_NNF ~f,CTL_NNF ~g)) /\
   (CTL_NNF ~ ~f = CTL_NNF f) /\ (CTL_NNF ~C_EX f = C_AX (CTL_NNF ~f)) /\
   (CTL_NNF ~C_EG f = C_AF (CTL_NNF ~f)) /\
   (CTL_NNF ~C_EU (f,g) = C_AR (CTL_NNF ~f,CTL_NNF ~g))

bexp_pstv_size_ind

|- !P.
     P T /\ (!p. P (B_PROP p)) /\
     (!b1 b2. P b1 /\ P b2 ==> P (B_AND (b1,b2))) /\ (!b. P b ==> P ~b) ==>
     !v. P v

bexp_pstv_size_def

|- (bexp_pstv_size T = 0) /\ (bexp_pstv_size (B_PROP p) = 1) /\
   (bexp_pstv_size (B_AND (b1,b2)) =
    1 + bexp_pstv_size b1 + bexp_pstv_size b2) /\
   (bexp_pstv_size ~b = bexp_pstv_size b)

ctl_pstv_size_ind

|- !P.
     (!b. P (C_BOOL b)) /\ (!f1 f2. P f1 /\ P f2 ==> P (C_AND (f1,f2))) /\
     (!f. P f ==> P ~f) /\ (!f. P f ==> P (C_EX f)) /\
     (!f. P f ==> P (C_EG f)) /\
     (!f1 f2. P f1 /\ P f2 ==> P (C_EU (f1,f2))) ==>
     !v. P v

ctl_pstv_size_def

|- (ctl_pstv_size (C_BOOL b) = 1 + bexp_pstv_size b) /\
   (ctl_pstv_size (C_AND (f1,f2)) =
    1 + ctl_pstv_size f1 + ctl_pstv_size f2) /\
   (ctl_pstv_size ~f = ctl_pstv_size f) /\
   (ctl_pstv_size (C_EX f) = 1 + ctl_pstv_size f) /\
   (ctl_pstv_size (C_EG f) = 1 + ctl_pstv_size f) /\
   (ctl_pstv_size (C_EU (f1,f2)) = 1 + ctl_pstv_size f1 + ctl_pstv_size f2)

CTL_BOOL_SUB_ind

|- !P.
     (!g. P g T) /\ (!g b. P g (B_PROP b)) /\
     (!g be1. P g be1 ==> P g ~be1) /\
     (!g be1 be2. P g be1 /\ P g be2 ==> P g (B_AND (be1,be2))) ==>
     !v v1. P v v1

CTL_BOOL_SUB_def

|- (CTL_BOOL_SUB g (B_PROP b) = (g = B_PROP b)) /\
   (CTL_BOOL_SUB g ~be1 = CTL_BOOL_SUB g be1 \/ (g = ~be1)) /\
   (CTL_BOOL_SUB g (B_AND (be1,be2)) =
    CTL_BOOL_SUB g be1 \/ CTL_BOOL_SUB g be2 \/ (g = B_AND (be1,be2)))

CTL_SUB_ind

|- !P.
     (!g b. P g (C_BOOL b)) /\
     (!g f1 f2. P g f1 /\ P g f2 ==> P g (C_AND (f1,f2))) /\
     (!g f. P g f ==> P g ~f) /\ (!g f. P g f ==> P g (C_EX f)) /\
     (!g f. P g f ==> P g (C_EG f)) /\
     (!g f1 f2. P g f1 /\ P g f2 ==> P g (C_EU (f1,f2))) ==>
     !v v1. P v v1

CTL_SUB_def

|- (CTL_SUB g (C_BOOL b) = ?b'. (g = C_BOOL b') /\ CTL_BOOL_SUB b' b) /\
   (CTL_SUB g (C_AND (f1,f2)) =
    CTL_SUB g f1 \/ CTL_SUB g f2 \/ (g = C_AND (f1,f2))) /\
   (CTL_SUB g ~f = CTL_SUB g f \/ (g = ~f)) /\
   (CTL_SUB g (C_EX f) = CTL_SUB g f \/ (g = C_EX f)) /\
   (CTL_SUB g (C_EG f) = CTL_SUB g f \/ (g = C_EG f)) /\
   (CTL_SUB g (C_EU (f1,f2)) =
    CTL_SUB g f1 \/ CTL_SUB g f2 \/ (g = C_EU (f1,f2)))

CTL_NNF_ID

|- !f M. C_SEM M (CTL_NNF f) = C_SEM M f

REST_INFINITE

|- !f. REST (INFINITE f) = INFINITE (\n. f (n + 1))

RESTN_INFINITE

|- !f i. RESTN (INFINITE f) i = INFINITE (\n. f (n + i))

REST_FINITE

|- !l. REST (FINITE l) = FINITE (TL l)