Theory "muSyntax"

Parents reach ks

Signature

Type	Arity
mu	1
Constant	Type
nu	:string -> 'prop mu -> 'prop mu
mu_size2	:'prop mu -> num
mu_size	:('prop -> num) -> 'prop mu -> num
mu_pstv_size	:'prop mu -> num
mu_case	:'a -> 'a -> ('prop mu -> 'a) -> ('prop mu -> 'prop mu -> 'a) -> ('prop mu -> 'prop mu -> 'a) -> (string -> 'a) -> ('prop -> 'a) -> (string -> 'prop mu -> 'a) -> (string -> 'prop mu -> 'a) -> (string -> 'prop mu -> 'a) -> (string -> 'prop mu -> 'a) -> 'prop mu -> 'a
muSyntax9	:string -> 'prop mu -> 'prop mu
muSyntax8	:string -> 'prop mu -> 'prop mu
muSyntax7	:string -> 'prop mu -> 'prop mu
muSyntax6	:'prop -> 'prop mu
muSyntax5	:string -> 'prop mu
muSyntax4	:'prop mu -> 'prop mu -> 'prop mu
muSyntax3	:'prop mu -> 'prop mu -> 'prop mu
muSyntax2	:'prop mu -> 'prop mu
muSyntax10	:string -> 'prop mu -> 'prop mu
muSyntax1	:'prop mu
muSyntax0	:'prop mu
mu	:string -> 'prop mu -> 'prop mu
mk_mu	:(string # 'prop) recspace -> 'prop mu
dest_mu	:'prop mu -> (string # 'prop) recspace
TR	:'prop mu
SUBFORMULA	:'prop mu -> 'prop mu -> bool
RVNEG	:string -> 'prop mu -> 'prop mu
RV	:string -> 'prop mu
Or	:'prop mu -> 'prop mu -> 'prop mu
Not	:'prop mu -> 'prop mu
NNF	:'prop mu -> 'prop mu
IS_PROP	:'prop mu -> bool
IMF	:'prop mu -> bool
FV	:'prop mu -> string -> bool
FL	:'prop mu
DIAMOND	:string -> 'prop mu -> 'prop mu
CLOSED	:'prop mu -> bool
BOX	:string -> 'prop mu -> 'prop mu
And	:'prop mu -> 'prop mu -> 'prop mu
AP_SUBST	:'prop mu -> 'prop -> 'prop mu -> 'prop mu
AP	:'prop -> 'prop mu
ALLV	:'prop mu -> string -> bool

Definitions

mu_TY_DEF

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

mu_repfns

|- (!a. mk_mu (dest_mu a) = a) /\
   !r.
     (\a0'.
        !'mu'.
          (!a0'.
             (a0' =
              ind_type$CONSTR 0 ((@v. T), @v. T) (\n. ind_type$BOTTOM)) \/
             (a0' =
              ind_type$CONSTR (SUC 0) ((@v. T), @v. T)
                (\n. ind_type$BOTTOM)) \/
             (?a.
                (a0' =
                 (\a.
                    ind_type$CONSTR (SUC (SUC 0)) ((@v. T), @v. T)
                      (FCONS a (\n. ind_type$BOTTOM))) a) /\ 'mu' a) \/
             (?a0 a1.
                (a0' =
                 (\a0 a1.
                    ind_type$CONSTR (SUC (SUC (SUC 0))) ((@v. T), @v. T)
                      (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0 a1) /\
                'mu' a0 /\ 'mu' a1) \/
             (?a0 a1.
                (a0' =
                 (\a0 a1.
                    ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T), @v. T)
                      (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0 a1) /\
                'mu' a0 /\ 'mu' a1) \/
             (?a.
                a0' =
                (\a.
                   ind_type$CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) (a, @v. T)
                     (\n. ind_type$BOTTOM)) a) \/
             (?a.
                a0' =
                (\a.
                   ind_type$CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0))))))
                     ((@v. T),a) (\n. ind_type$BOTTOM)) a) \/
             (?a0 a1.
                (a0' =
                 (\a0 a1.
                    ind_type$CONSTR
                      (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))) (a0, @v. T)
                      (FCONS a1 (\n. ind_type$BOTTOM))) a0 a1) /\ 'mu' a1) \/
             (?a0 a1.
                (a0' =
                 (\a0 a1.
                    ind_type$CONSTR
                      (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))
                      (a0, @v. T) (FCONS a1 (\n. ind_type$BOTTOM))) a0 a1) /\
                'mu' a1) \/
             (?a0 a1.
                (a0' =
                 (\a0 a1.
                    ind_type$CONSTR
                      (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))
                      (a0, @v. T) (FCONS a1 (\n. ind_type$BOTTOM))) a0 a1) /\
                'mu' a1) \/
             (?a0 a1.
                (a0' =
                 (\a0 a1.
                    ind_type$CONSTR
                      (SUC
                         (SUC
                            (SUC
                               (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))
                      (a0, @v. T) (FCONS a1 (\n. ind_type$BOTTOM))) a0 a1) /\
                'mu' a1) ==>
             'mu' a0') ==>
          'mu' a0') r =
     (dest_mu (mk_mu r) = r)

muSyntax0_def

|- muSyntax0 =
   mk_mu (ind_type$CONSTR 0 ((@v. T), @v. T) (\n. ind_type$BOTTOM))

muSyntax1_def

|- muSyntax1 =
   mk_mu (ind_type$CONSTR (SUC 0) ((@v. T), @v. T) (\n. ind_type$BOTTOM))

muSyntax2_def

|- muSyntax2 =
   (\a.
      mk_mu
        ((\a.
            ind_type$CONSTR (SUC (SUC 0)) ((@v. T), @v. T)
              (FCONS a (\n. ind_type$BOTTOM))) (dest_mu a)))

muSyntax3_def

|- muSyntax3 =
   (\a0 a1.
      mk_mu
        ((\a0 a1.
            ind_type$CONSTR (SUC (SUC (SUC 0))) ((@v. T), @v. T)
              (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) (dest_mu a0)
           (dest_mu a1)))

muSyntax4_def

|- muSyntax4 =
   (\a0 a1.
      mk_mu
        ((\a0 a1.
            ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T), @v. T)
              (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) (dest_mu a0)
           (dest_mu a1)))

muSyntax5_def

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

muSyntax6_def

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

muSyntax7_def

|- muSyntax7 =
   (\a0 a1.
      mk_mu
        ((\a0 a1.
            ind_type$CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))
              (a0, @v. T) (FCONS a1 (\n. ind_type$BOTTOM))) a0 (dest_mu a1)))

muSyntax8_def

|- muSyntax8 =
   (\a0 a1.
      mk_mu
        ((\a0 a1.
            ind_type$CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))
              (a0, @v. T) (FCONS a1 (\n. ind_type$BOTTOM))) a0 (dest_mu a1)))

muSyntax9_def

|- muSyntax9 =
   (\a0 a1.
      mk_mu
        ((\a0 a1.
            ind_type$CONSTR
              (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))
              (a0, @v. T) (FCONS a1 (\n. ind_type$BOTTOM))) a0 (dest_mu a1)))

muSyntax10_def

|- muSyntax10 =
   (\a0 a1.
      mk_mu
        ((\a0 a1.
            ind_type$CONSTR
              (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))
              (a0, @v. T) (FCONS a1 (\n. ind_type$BOTTOM))) a0 (dest_mu a1)))

TR

|- T = muSyntax0

FL

|- F = muSyntax1

Not

|- $~ = muSyntax2

And

|- $/\ = muSyntax3

Or

|- $\/ = muSyntax4

RV

|- RV = muSyntax5

AP

|- $AP = muSyntax6

DIAMOND

|- DIAMOND = muSyntax7

BOX

|- BOX = muSyntax8

mu

|- $mu = muSyntax9

nu

|- $nu = muSyntax10

mu_case_def

|- (!v v1 f f1 f2 f3 f4 f5 f6 f7 f8.
      mu_case v v1 f f1 f2 f3 f4 f5 f6 f7 f8 T = v) /\
   (!v v1 f f1 f2 f3 f4 f5 f6 f7 f8.
      mu_case v v1 f f1 f2 f3 f4 f5 f6 f7 f8 F = v1) /\
   (!v v1 f f1 f2 f3 f4 f5 f6 f7 f8 a.
      mu_case v v1 f f1 f2 f3 f4 f5 f6 f7 f8 ~a = f a) /\
   (!v v1 f f1 f2 f3 f4 f5 f6 f7 f8 a0 a1.
      mu_case v v1 f f1 f2 f3 f4 f5 f6 f7 f8 (a0 /\ a1) = f1 a0 a1) /\
   (!v v1 f f1 f2 f3 f4 f5 f6 f7 f8 a0 a1.
      mu_case v v1 f f1 f2 f3 f4 f5 f6 f7 f8 (a0 \/ a1) = f2 a0 a1) /\
   (!v v1 f f1 f2 f3 f4 f5 f6 f7 f8 a.
      mu_case v v1 f f1 f2 f3 f4 f5 f6 f7 f8 (RV a) = f3 a) /\
   (!v v1 f f1 f2 f3 f4 f5 f6 f7 f8 a.
      mu_case v v1 f f1 f2 f3 f4 f5 f6 f7 f8 AP a = f4 a) /\
   (!v v1 f f1 f2 f3 f4 f5 f6 f7 f8 a0 a1.
      mu_case v v1 f f1 f2 f3 f4 f5 f6 f7 f8 <> a1 = f5 a0 a1) /\
   (!v v1 f f1 f2 f3 f4 f5 f6 f7 f8 a0 a1.
      mu_case v v1 f f1 f2 f3 f4 f5 f6 f7 f8 [[a0]] a1 = f6 a0 a1) /\
   (!v v1 f f1 f2 f3 f4 f5 f6 f7 f8 a0 a1.
      mu_case v v1 f f1 f2 f3 f4 f5 f6 f7 f8 (mu a0.. a1) = f7 a0 a1) /\
   !v v1 f f1 f2 f3 f4 f5 f6 f7 f8 a0 a1.
     mu_case v v1 f f1 f2 f3 f4 f5 f6 f7 f8 (nu a0.. a1) = f8 a0 a1

mu_size_def

|- (!f. mu_size f T = 0) /\ (!f. mu_size f F = 0) /\
   (!f a. mu_size f ~a = 1 + mu_size f a) /\
   (!f a0 a1. mu_size f (a0 /\ a1) = 1 + (mu_size f a0 + mu_size f a1)) /\
   (!f a0 a1. mu_size f (a0 \/ a1) = 1 + (mu_size f a0 + mu_size f a1)) /\
   (!f a. mu_size f (RV a) = 1 + STRLEN a) /\
   (!f a. mu_size f AP a = 1 + f a) /\
   (!f a0 a1. mu_size f <> a1 = 1 + (STRLEN a0 + mu_size f a1)) /\
   (!f a0 a1. mu_size f [[a0]] a1 = 1 + (STRLEN a0 + mu_size f a1)) /\
   (!f a0 a1. mu_size f (mu a0.. a1) = 1 + (STRLEN a0 + mu_size f a1)) /\
   !f a0 a1. mu_size f (nu a0.. a1) = 1 + (STRLEN a0 + mu_size f a1)

mu_size2_def

|- !f. mu_size2 f = mu_size (\a. 0) f

NNF_primitive_def

|- NNF =
   WFREC
     (@R.
        WF R /\ (!f g. R g (f /\ g)) /\ (!g f. R f (f /\ g)) /\
        (!f g. R g (f \/ g)) /\ (!g f. R f (f \/ g)) /\ (!a f. R f <> f) /\
        (!a f. R f [[a]] f) /\ (!Q f. R f mu Q.. f) /\ (!Q f. R f nu Q.. f) /\
        (!f g. R (~g) ~(f /\ g)) /\ (!g f. R (~f) ~(f /\ g)) /\
        (!f g. R (~g) ~(f \/ g)) /\ (!g f. R (~f) ~(f \/ g)) /\
        (!a f. R (~f) ~ <> f) /\ (!a f. R (~f) ~[[a]] f) /\
        (!f. R f ~ ~f) /\ (!f Q. R (RVNEG Q ~f) ~mu Q.. f) /\
        !f Q. R (RVNEG Q ~f) ~nu Q.. f)
     (\NNF a''''.
        case a'''' of
           T -> I T
        || F -> I F
        || ~T -> I F
        || ~F -> I T
        || ~ ~f'''''''''' -> I (NNF f'''''''''')
        || ~(f'''''' /\ g'') -> I (NNF ~f'''''' \/ NNF ~g'')
        || ~(f''''''' \/ g''') -> I (NNF ~f''''''' /\ NNF ~g''')
        || ~RV Q''' -> I ~RV Q'''
        || ~AP p' -> I ~AP p'
        || ~ <> f'''''''' -> I [[a'']] (NNF ~f'''''''')
        || ~[[a''']] f''''''''' -> I <> (NNF ~f''''''''')
        || ~(mu Q''''.. f''''''''''') ->
             I (nu Q''''.. NNF (RVNEG Q'''' ~f'''''''''''))
        || ~(nu Q'''''.. f'''''''''''') ->
             I (mu Q'''''.. NNF (RVNEG Q''''' ~f''''''''''''))
        || f /\ g -> I (NNF f /\ NNF g)
        || f' \/ g' -> I (NNF f' \/ NNF g')
        || RV Q -> I (RV Q)
        || AP p -> I AP p
        || <> f'' -> I <> (NNF f'')
        || [[a']] f''' -> I [[a']] (NNF f''')
        || (mu Q'.. f'''') -> I (mu Q'.. NNF f'''')
        || (nu Q''.. f''''') -> I nu Q''.. NNF f''''')

mu_pstv_size_def

|- (mu_pstv_size T = mu_size2 T) /\ (mu_pstv_size F = mu_size2 F) /\
   (!f g. mu_pstv_size (f /\ g) = 1 + (mu_pstv_size f + mu_pstv_size g)) /\
   (!f g. mu_pstv_size (f \/ g) = 1 + (mu_pstv_size f + mu_pstv_size g)) /\
   (!p. mu_pstv_size AP p = mu_size2 AP p) /\
   (!Q. mu_pstv_size (RV Q) = mu_size2 (RV Q)) /\
   (!a f. mu_pstv_size <> f = 1 + mu_pstv_size f) /\
   (!a f. mu_pstv_size [[a]] f = 1 + mu_pstv_size f) /\
   (!Q f. mu_pstv_size (mu Q.. f) = 1 + (STRLEN Q + mu_pstv_size f)) /\
   (!Q f. mu_pstv_size (nu Q.. f) = 1 + (STRLEN Q + mu_pstv_size f)) /\
   !f. mu_pstv_size ~f = mu_pstv_size f

SUBFORMULA_def

|- (!g. g SUBF T = (g = T)) /\ (!g. g SUBF F = (g = F)) /\
   (!g f. g SUBF ~f = g SUBF f \/ (g = ~f)) /\
   (!g f1 f2. g SUBF (f1 /\ f2) = g SUBF f1 \/ g SUBF f2 \/ (g = f1 /\ f2)) /\
   (!g f1 f2. g SUBF (f1 \/ f2) = g SUBF f1 \/ g SUBF f2 \/ (g = f1 \/ f2)) /\
   (!g Q. g SUBF RV Q = (g = RV Q)) /\ (!g p. g SUBF AP p = (g = AP p)) /\
   (!g a f. g SUBF <> f = g SUBF f \/ (g = <> f)) /\
   (!g a f. g SUBF [[a]] f = g SUBF f \/ (g = [[a]] f)) /\
   (!g Q f. g SUBF (mu Q.. f) = g SUBF f \/ (g = mu Q.. f)) /\
   !g Q f. g SUBF (nu Q.. f) = g SUBF f \/ (g = nu Q.. f)

IS_PROP_def

|- (IS_PROP T = T) /\ (IS_PROP F = T) /\ (!f. IS_PROP ~f = IS_PROP f) /\
   (!f1 f2. IS_PROP (f1 /\ f2) = IS_PROP f1 /\ IS_PROP f2) /\
   (!f1 f2. IS_PROP (f1 \/ f2) = IS_PROP f1 /\ IS_PROP f2) /\
   (!Q. IS_PROP (RV Q) = F) /\ (!p. IS_PROP AP p = T) /\
   (!a f. IS_PROP <> f = F) /\ (!a f. IS_PROP [[a]] f = F) /\
   (!Q f. IS_PROP (mu Q.. f) = F) /\ !Q f. IS_PROP (nu Q.. f) = F

AP_SUBST_def

|- (!g ap. AP_SUBST g ap T = T) /\ (!g ap. AP_SUBST g ap F = F) /\
   (!g ap f. AP_SUBST g ap ~f = ~AP_SUBST g ap f) /\
   (!g ap f1 f2.
      AP_SUBST g ap (f1 /\ f2) = AP_SUBST g ap f1 /\ AP_SUBST g ap f2) /\
   (!g ap f1 f2.
      AP_SUBST g ap (f1 \/ f2) = AP_SUBST g ap f1 \/ AP_SUBST g ap f2) /\
   (!g ap Q. AP_SUBST g ap (RV Q) = RV Q) /\
   (!g ap p. AP_SUBST g ap AP p = (if p = ap then g else AP p)) /\
   (!g ap a f. AP_SUBST g ap <> f = <> (AP_SUBST g ap f)) /\
   (!g ap a f. AP_SUBST g ap [[a]] f = [[a]] (AP_SUBST g ap f)) /\
   (!g ap Q f. AP_SUBST g ap (mu Q.. f) = mu Q.. AP_SUBST g ap f) /\
   !g ap Q f. AP_SUBST g ap (nu Q.. f) = nu Q.. AP_SUBST g ap f

Theorems

datatype_mu

|- DATATYPE ((mu T.. F) $~ $/\ $\/ RV $AP DIAMOND BOX $mu $nu)

mu_11

|- (!a a'. (~a = ~a') = (a = a')) /\
   (!a0 a1 a0' a1'. (a0 /\ a1 = a0' /\ a1') = (a0 = a0') /\ (a1 = a1')) /\
   (!a0 a1 a0' a1'. (a0 \/ a1 = a0' \/ a1') = (a0 = a0') /\ (a1 = a1')) /\
   (!a a'. (RV a = RV a') = (a = a')) /\ (!a a'. (AP a = AP a') = (a = a')) /\
   (!a0 a1 a0' a1'. (<> a1 = <> a1') = (a0 = a0') /\ (a1 = a1')) /\
   (!a0 a1 a0' a1'. ([[a0]] a1 = [[a0']] a1') = (a0 = a0') /\ (a1 = a1')) /\
   (!a0 a1 a0' a1'.
      ((mu a0.. a1) = mu a0'.. a1') = (a0 = a0') /\ (a1 = a1')) /\
   !a0 a1 a0' a1'. ((nu a0.. a1) = nu a0'.. a1') = (a0 = a0') /\ (a1 = a1')

mu_distinct

|- ~(T = F) /\ (!a. ~(T = ~a)) /\ (!a1 a0. ~(T = a0 /\ a1)) /\
   (!a1 a0. ~(T = a0 \/ a1)) /\ (!a. ~(T = RV a)) /\ (!a. ~(T = AP a)) /\
   (!a1 a0. ~(T = <> a1)) /\ (!a1 a0. ~(T = [[a0]] a1)) /\
   (!a1 a0. ~(T = mu a0.. a1)) /\ (!a1 a0. ~(T = nu a0.. a1)) /\
   (!a. ~(F = ~a)) /\ (!a1 a0. ~(F = a0 /\ a1)) /\
   (!a1 a0. ~(F = a0 \/ a1)) /\ (!a. ~(F = RV a)) /\ (!a. ~(F = AP a)) /\
   (!a1 a0. ~(F = <> a1)) /\ (!a1 a0. ~(F = [[a0]] a1)) /\
   (!a1 a0. ~(F = mu a0.. a1)) /\ (!a1 a0. ~(F = nu a0.. a1)) /\
   (!a1 a0 a. ~(~a = a0 /\ a1)) /\ (!a1 a0 a. ~(~a = a0 \/ a1)) /\
   (!a' a. ~(~a = RV a')) /\ (!a' a. ~(~a = AP a')) /\
   (!a1 a0 a. ~(~a = <> a1)) /\ (!a1 a0 a. ~(~a = [[a0]] a1)) /\
   (!a1 a0 a. ~(~a = mu a0.. a1)) /\ (!a1 a0 a. ~(~a = nu a0.. a1)) /\
   (!a1' a1 a0' a0. ~(a0 /\ a1 = a0' \/ a1')) /\
   (!a1 a0 a. ~(a0 /\ a1 = RV a)) /\ (!a1 a0 a. ~(a0 /\ a1 = AP a)) /\
   (!a1' a1 a0' a0. ~(a0 /\ a1 = <> a1')) /\
   (!a1' a1 a0' a0. ~(a0 /\ a1 = [[a0']] a1')) /\
   (!a1' a1 a0' a0. ~(a0 /\ a1 = mu a0'.. a1')) /\
   (!a1' a1 a0' a0. ~(a0 /\ a1 = nu a0'.. a1')) /\
   (!a1 a0 a. ~(a0 \/ a1 = RV a)) /\ (!a1 a0 a. ~(a0 \/ a1 = AP a)) /\
   (!a1' a1 a0' a0. ~(a0 \/ a1 = <> a1')) /\
   (!a1' a1 a0' a0. ~(a0 \/ a1 = [[a0']] a1')) /\
   (!a1' a1 a0' a0. ~(a0 \/ a1 = mu a0'.. a1')) /\
   (!a1' a1 a0' a0. ~(a0 \/ a1 = nu a0'.. a1')) /\ (!a' a. ~(RV a = AP a')) /\
   (!a1 a0 a. ~(RV a = <> a1)) /\ (!a1 a0 a. ~(RV a = [[a0]] a1)) /\
   (!a1 a0 a. ~(RV a = mu a0.. a1)) /\ (!a1 a0 a. ~(RV a = nu a0.. a1)) /\
   (!a1 a0 a. ~(AP a = <> a1)) /\ (!a1 a0 a. ~(AP a = [[a0]] a1)) /\
   (!a1 a0 a. ~(AP a = mu a0.. a1)) /\ (!a1 a0 a. ~(AP a = nu a0.. a1)) /\
   (!a1' a1 a0' a0. ~(<> a1 = [[a0']] a1')) /\
   (!a1' a1 a0' a0. ~(<> a1 = mu a0'.. a1')) /\
   (!a1' a1 a0' a0. ~(<> a1 = nu a0'.. a1')) /\
   (!a1' a1 a0' a0. ~([[a0]] a1 = mu a0'.. a1')) /\
   (!a1' a1 a0' a0. ~([[a0]] a1 = nu a0'.. a1')) /\
   !a1' a1 a0' a0. ~((mu a0.. a1) = nu a0'.. a1')

mu_case_cong

|- !M M' v v1 f f1 f2 f3 f4 f5 f6 f7 f8.
     (M = M') /\ ((M' = T) ==> (v = v')) /\ ((M' = F) ==> (v1 = v1')) /\
     (!a. (M' = ~a) ==> (f a = f' a)) /\
     (!a0 a1. (M' = a0 /\ a1) ==> (f1 a0 a1 = f1' a0 a1)) /\
     (!a0 a1. (M' = a0 \/ a1) ==> (f2 a0 a1 = f2' a0 a1)) /\
     (!a. (M' = RV a) ==> (f3 a = f3' a)) /\
     (!a. (M' = AP a) ==> (f4 a = f4' a)) /\
     (!a0 a1. (M' = <> a1) ==> (f5 a0 a1 = f5' a0 a1)) /\
     (!a0 a1. (M' = [[a0]] a1) ==> (f6 a0 a1 = f6' a0 a1)) /\
     (!a0 a1. (M' = mu a0.. a1) ==> (f7 a0 a1 = f7' a0 a1)) /\
     (!a0 a1. (M' = nu a0.. a1) ==> (f8 a0 a1 = f8' a0 a1)) ==>
     (mu_case v v1 f f1 f2 f3 f4 f5 f6 f7 f8 M =
      mu_case v' v1' f' f1' f2' f3' f4' f5' f6' f7' f8' M')

mu_nchotomy

|- !m.
     (m = T) \/ (m = F) \/ (?m'. m = ~m') \/ (?m' m0. m = m' /\ m0) \/
     (?m' m0. m = m' \/ m0) \/ (?s. m = RV s) \/ (?p. m = AP p) \/
     (?s m'. m = <> m') \/ (?s m'. m = [[s]] m') \/
     (?s m'. m = mu s.. m') \/ ?s m'. m = nu s.. m'

~~mu_Axiom~~

|- !f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. ?fn. (fn T = f0) /\ (fn F = f1) /\ (!a. fn ~a = f2 a (fn a)) /\ (!a0 a1. fn (a0 /\ a1) = f3 a0 a1 (fn a0) (fn a1)) /\ (!a0 a1. fn (a0 \/ a1) = f4 a0 a1 (fn a0) (fn a1)) /\ (!a. fn (RV a) = f5 a) /\ (!a. fn AP a = f6 a) /\ (!a0 a1. fn <> a1 = f7 a0 a1 (fn a1)) /\ (!a0 a1. fn [[a0]] a1 = f8 a0 a1 (fn a1)) /\ (!a0 a1. fn (mu a0.. a1) = f9 a0 a1 (fn a1)) /\ !a0 a1. fn (nu a0.. a1) = f10 a0 a1 (fn a1)

~~mu_induction~~

|- !P. P T /\ P F /\ (!m. P m ==> P ~m) /\ (!m m0. P m /\ P m0 ==> P (m /\ m0)) /\ (!m m0. P m /\ P m0 ==> P (m \/ m0)) /\ (!s. P (RV s)) /\ (!p. P AP p) /\ (!m. P m ==> !s. P <~~> m) /\ (!m. P m ==> !s. P [[s]] m) /\ (!m. P m ==> !s. P mu s.. m) /\ (!m. P m ==> !s. P nu s.. m) ==> !m. P m~~

~~RVNEG_def~~

|- (!rv. RVNEG rv T = T) /\ (!rv. RVNEG rv F = F) /\ (!rv f g. RVNEG rv (f /\ g) = RVNEG rv f /\ RVNEG rv g) /\ (!rv f g. RVNEG rv (f \/ g) = RVNEG rv f \/ RVNEG rv g) /\ (!rv p. RVNEG rv AP p = AP p) /\ (!rv Q. RVNEG rv (RV Q) = (if rv = Q then ~RV Q else RV Q)) /\ (!rv a f. RVNEG rv <> f = <> (RVNEG rv f)) /\ (!rv a f. RVNEG rv [[a]] f = [[a]] (RVNEG rv f)) /\ (!rv Q f. RVNEG rv (mu Q.. f) = (if rv = Q then mu Q.. f else mu Q.. RVNEG rv f)) /\ (!rv Q f. RVNEG rv (nu Q.. f) = (if rv = Q then nu Q.. f else nu Q.. RVNEG rv f)) /\ !rv f. RVNEG rv ~f = ~RVNEG rv f

~~NNF_def~~

|- (NNF T = T) /\ (NNF F = F) /\ (NNF (f /\ g) = NNF f /\ NNF g) /\ (NNF (f \/ g) = NNF f \/ NNF g) /\ (NNF AP p = AP p) /\ (NNF (RV Q) = RV Q) /\ (NNF <> f = <> (NNF f)) /\ (NNF [[a]] f = [[a]] (NNF f)) /\ (NNF (mu Q.. f) = mu Q.. NNF f) /\ (NNF (nu Q.. f) = nu Q.. NNF f) /\ (NNF ~T = F) /\ (NNF ~F = T) /\ (NNF ~(f /\ g) = NNF ~f \/ NNF ~g) /\ (NNF ~(f \/ g) = NNF ~f /\ NNF ~g) /\ (NNF ~AP p = ~AP p) /\ (NNF ~RV Q = ~RV Q) /\ (NNF ~ <> f = [[a]] (NNF ~f)) /\ (NNF ~[[a]] f = <> (NNF ~f)) /\ (NNF ~ ~f = NNF f) /\ (NNF ~(mu Q.. f) = nu Q.. NNF (RVNEG Q ~f)) /\ (NNF ~(nu Q.. f) = mu Q.. NNF (RVNEG Q ~f))

~~NNF_IND_def~~

|- !P. P T /\ P F /\ (!f g. P f /\ P g ==> P (f /\ g)) /\ (!f g. P f /\ P g ==> P (f \/ g)) /\ (!p. P AP p) /\ (!Q. P (RV Q)) /\ (!a f. P f ==> P <> f) /\ (!a f. P f ==> P [[a]] f) /\ (!Q f. P f ==> P mu Q.. f) /\ (!Q f. P f ==> P nu Q.. f) /\ P ~T /\ P ~F /\ (!f g. P ~f /\ P ~g ==> P ~(f /\ g)) /\ (!f g. P ~f /\ P ~g ==> P ~(f \/ g)) /\ (!p. P ~AP p) /\ (!Q. P ~RV Q) /\ (!a f. P ~f ==> P ~ <> f) /\ (!a f. P ~f ==> P ~[[a]] f) /\ (!f. P f ==> P ~ ~f) /\ (!Q f. P (RVNEG Q ~f) ==> P ~mu Q.. f) /\ (!Q f. P (RVNEG Q ~f) ==> P ~nu Q.. f) ==> !v. P v

~~MU_SUB_def~~

|- (!g. g SUBF T = (g = T)) /\ (!g. g SUBF F = (g = F)) /\ (!g f. g SUBF ~f = g SUBF f \/ (g = ~f)) /\ (!g f1 f2. g SUBF (f1 /\ f2) = g SUBF f1 \/ g SUBF f2 \/ (g = f1 /\ f2)) /\ (!g f1 f2. g SUBF (f1 \/ f2) = g SUBF f1 \/ g SUBF f2 \/ (g = f1 \/ f2)) /\ (!g Q. g SUBF RV Q = (g = RV Q)) /\ (!g p. g SUBF AP p = (g = AP p)) /\ (!g a f. g SUBF <> f = g SUBF f \/ (g = <> f)) /\ (!g a f. g SUBF [[a]] f = g SUBF f \/ (g = [[a]] f)) /\ (!g Q f. g SUBF (mu Q.. f) = g SUBF f \/ (g = mu Q.. f)) /\ !g Q f. g SUBF (nu Q.. f) = g SUBF f \/ (g = nu Q.. f)

~~IMF_def~~

|- (IMF T = T) /\ (IMF F = T) /\ (!f. IMF ~f = IMF f) /\ (!f1 f2. IMF (f1 /\ f2) = IMF f1 /\ IMF f2) /\ (!f1 f2. IMF (f1 \/ f2) = IMF f1 /\ IMF f2) /\ (!Q. IMF (RV Q) = T) /\ (!p. IMF AP p = T) /\ (!a f. IMF <> f = IMF f) /\ (!a f. IMF [[a]] f = IMF f) /\ (!Q f. IMF (mu Q.. f) = ~(~RV Q SUBF NNF f) /\ IMF f) /\ !Q f. IMF (nu Q.. f) = ~(~RV Q SUBF NNF f) /\ IMF f

~~FV_def~~

|- (FV T = {}) /\ (FV F = {}) /\ (!f. FV ~f = FV f) /\ (!f1 f2. FV (f1 /\ f2) = FV f1 UNION FV f2) /\ (!f1 f2. FV (f1 \/ f2) = FV f1 UNION FV f2) /\ (!Q. FV (RV Q) = {Q}) /\ (!p. FV AP p = {}) /\ (!a f. FV <> f = FV f) /\ (!a f. FV [[a]] f = FV f) /\ (!Q f. FV (mu Q.. f) = FV f DELETE Q) /\ !Q f. FV (nu Q.. f) = FV f DELETE Q

~~ALLV_def~~

|- (ALLV T = {}) /\ (ALLV F = {}) /\ (!f. ALLV ~f = ALLV f) /\ (!f1 f2. ALLV (f1 /\ f2) = ALLV f1 UNION ALLV f2) /\ (!f1 f2. ALLV (f1 \/ f2) = ALLV f1 UNION ALLV f2) /\ (!Q. ALLV (RV Q) = {Q}) /\ (!p. ALLV AP p = {}) /\ (!a f. ALLV <> f = ALLV f) /\ (!a f. ALLV [[a]] f = ALLV f) /\ (!Q f. ALLV (mu Q.. f) = ALLV f) /\ !Q f. ALLV (nu Q.. f) = ALLV f

~~CLOSED_def~~

~~|- !f. CLOSED f = (FV f = {})~~

~~RVNEG_SYM~~

~~|- !Q Q' f. RVNEG Q (RVNEG Q' f) = RVNEG Q' (RVNEG Q f)~~

~~IMF_NEG_NEG_LEM1~~

~~|- !f Q Q'. ~(Q' = Q) ==> (~(~RV Q SUBF NNF (RVNEG Q' f)) = ~(~RV Q SUBF NNF f))~~

~~IMF_INV_RVNEG~~

~~|- !f Q. IMF (RVNEG Q f) = IMF f~~

~~IMF_INV_NEG_RVNEG~~

~~|- !f Q. IMF f = IMF (RVNEG Q ~f)~~

~~STATES_MONO_NEG_MU_LEM1~~

~~|- !Q' Q f. ~RV Q' SUBF NNF ~(mu Q.. f) = ~RV Q' SUBF NNF (RVNEG Q ~f)~~

~~STATES_MONO_LEM2~~

~~|- !f Q Q'. ~(Q' = Q) ==> (~RV Q' SUBF NNF f = ~RV Q' SUBF NNF (RVNEG Q f))~~

~~NNF_RVNEG_DUALITY~~

~~|- !f Q. NNF (RVNEG Q (RVNEG Q f)) = NNF f~~

~~IMF_MU_IFF_IMF_NU~~

~~|- !f Q. IMF (mu Q.. f) = IMF nu Q.. f~~

~~CLOSED_NEG~~

~~|- !f. CLOSED ~f = CLOSED f~~

~~CLOSED_AND~~

~~|- !f g. CLOSED (f /\ g) = CLOSED f /\ CLOSED g~~

~~CLOSED_OR~~

~~|- !f g. CLOSED (f \/ g) = CLOSED f /\ CLOSED g~~

~~CLOSED_AP~~

~~|- !p. CLOSED AP p~~

~~CLOSED_BOX~~

~~|- !f a. CLOSED [[a]] f = CLOSED f~~

~~CLOSED_DMD~~

~~|- !f a. CLOSED <> f = CLOSED f~~

~~SUBF_REFL~~

~~|- !f. f SUBF f~~

~~SUBF_CONJ~~

~~|- !f g h. (f /\ g) SUBF h ==> f SUBF h /\ g SUBF h~~

~~SUBF_DISJ~~

~~|- !f g h. (f \/ g) SUBF h ==> f SUBF h /\ g SUBF h~~

~~SUBF_DMD~~

~~|- !a f h. <> f SUBF h ==> f SUBF h~~

~~SUBF_BOX~~

~~|- !a f h. [[a]] f SUBF h ==> f SUBF h~~

~~SUBF_MU~~

~~|- !Q f h. (mu Q.. f) SUBF h ==> f SUBF h~~

~~SUBF_NU~~

~~|- !Q f h. (nu Q.. f) SUBF h ==> f SUBF h~~

~~SUB_RV_BOX~~

~~|- !f a Q. ~(~RV Q SUBF [[a]] f) = ~(~RV Q SUBF f)~~

~~SUB_RV_MU~~

~~|- !f Q Q'. ~(~RV Q' SUBF mu Q.. f) = ~(~RV Q' SUBF f)~~

~~SUB_RV_NU~~

~~|- !f Q Q'. ~(~RV Q' SUBF nu Q.. f) = ~(~RV Q' SUBF f)~~

~~SUB_AP_RVNEG~~

~~|- !f p Q. AP p SUBF f = AP p SUBF RVNEG Q ~f~~

~~SUB_AP_NEG_MU~~

~~|- !f p Q. AP p SUBF ~(mu Q.. f) = AP p SUBF RVNEG Q ~f~~

~~SUB_AP_NEG_NU~~

~~|- !f p Q. AP p SUBF ~(nu Q.. f) = AP p SUBF RVNEG Q ~f~~

~~SUB_AP_NEG~~

~~|- !f p. AP p SUBF ~f = AP p SUBF f~~

~~SUB_AP_CONJ~~

~~|- !f g p. AP p SUBF (f /\ g) = AP p SUBF f \/ AP p SUBF g~~

~~SUB_AP_DISJ~~

~~|- !f g p. AP p SUBF (f \/ g) = AP p SUBF f \/ AP p SUBF g~~

~~SUB_AP_BOX~~

~~|- !f p a. AP p SUBF [[a]] f = AP p SUBF f~~

~~SUB_AP_DMD~~

~~|- !f p a. AP p SUBF <> f = AP p SUBF f~~

~~SUB_AP_MU~~

~~|- !f p Q. AP p SUBF (mu Q.. f) = AP p SUBF f~~

~~SUB_AP_NU~~

~~|- !f p Q. AP p SUBF (nu Q.. f) = AP p SUBF f~~

~~NNF_NEG~~

~~|- !f. IMF f ==> !g. ~g SUBF NNF f ==> ?p. (g = AP p) \/ ?Q. g = RV Q~~

~~SUB_DMD_NEG~~

~~|- !f g a. ~(<> g SUBF ~f) = ~(<> g SUBF f)~~

~~SUB_DMD_CONJ~~

~~|- !f f1 g a. ~(<> g SUBF (f /\ f1)) = ~(<> g SUBF f) /\ ~(<> g SUBF f1)~~

~~SUB_DMD_DISJ~~

~~|- !f f1 g a. ~(<> g SUBF (f \/ f1)) = ~(<> g SUBF f) /\ ~(<> g SUBF f1)~~

~~SUB_DMD_DMD~~

~~|- !f a. ~ !a' g. ~(<> g SUBF <> f)~~

~~SUB_DMD_BOX~~

~~|- !f g a a'. ~(<> g SUBF [[a']] f) = ~(<> g SUBF f)~~

~~SUB_DMD_MU~~

~~|- !f g a Q. ~(<> g SUBF mu Q.. f) = ~(<> g SUBF f)~~

~~SUB_DMD_NU~~

~~|- !f g a Q. ~(<> g SUBF nu Q.. f) = ~(<> g SUBF f)~~

~~SUB_AP_NEG_CONJ~~

~~|- !f g p. AP p SUBF ~(f /\ g) = AP p SUBF ~f \/ AP p SUBF ~g~~

~~SUB_AP_NEG_DISJ~~

~~|- !f g p. AP p SUBF ~(f \/ g) = AP p SUBF ~f \/ AP p SUBF ~g~~

~~SUB_AP_NEG_DMD~~

~~|- !f p a. AP p SUBF ~ <> f = AP p SUBF ~f~~

~~SUB_AP_NEG_NEG~~

~~|- !f p. AP p SUBF ~ ~f = AP p SUBF f~~

~~SUB_DMD_NEG_CONJ~~

~~|- !f f1 g a. ~(<> g SUBF ~(f /\ f1)) = ~(<> g SUBF ~f) /\ ~(<> g SUBF ~f1)~~

~~SUB_DMD_NEG_DISJ~~

~~|- !f f1 g a. ~(<> g SUBF ~(f \/ f1)) = ~(<> g SUBF ~f) /\ ~(<> g SUBF ~f1)~~

~~SUB_DMD_NEG_DMD~~

~~|- !f a. (!a' g. ~(<> g SUBF ~ <> f)) ==> !a' g. ~(<> g SUBF ~f)~~

~~SUB_DMD_NEG_NEG~~

~~|- !f g a. ~(<> g SUBF ~ ~f) = ~(<> g SUBF f)~~

~~STATES_MONO_LEM3~~

~~|- !f Q. ~(~RV Q SUBF NNF f) = ~(~RV Q SUBF NNF (RVNEG Q ~f))~~

~~STATES_MONO_LEM6~~

~~|- !Q Q' f. ~RV Q' SUBF NNF (mu Q.. f) = ~RV Q' SUBF NNF f~~

~~STATES_MONO_LEM11~~

~~|- !Q Q' f. ~RV Q' SUBF NNF (nu Q.. f) = ~RV Q' SUBF NNF f~~

~~STATES_MONO_LEM8~~

~~|- !Q. ~(~RV Q SUBF NNF (RV Q))~~

~~STATES_MONO_LEM9~~

~~|- !Q. ~RV Q SUBF NNF ~RV Q~~

~~NNF_IDEM~~

~~|- !f. NNF (NNF f) = NNF f~~

~~IMF_NNF~~

~~|- !f. IMF f = IMF (NNF f)~~

~~IMF_MU_NNF~~

~~|- !f Q. IMF (mu Q.. f) = IMF mu Q.. NNF f~~

~~IMF_MU_CONJ~~

~~|- !f g Q. IMF (mu Q.. f /\ g) = IMF (mu Q.. f) /\ IMF mu Q.. g~~

~~IMF_MU_NEG_CONJ~~

~~|- !f g Q. IMF (mu Q.. ~(f /\ g)) = IMF (mu Q.. ~f) /\ IMF mu Q.. ~g~~

~~IMF_MU_DISJ~~

~~|- !f g Q. IMF (mu Q.. f \/ g) = IMF (mu Q.. f) /\ IMF mu Q.. g~~

~~IMF_MU_NEG_DISJ~~

~~|- !f g Q. IMF (mu Q.. ~(f \/ g)) = IMF (mu Q.. ~f) /\ IMF mu Q.. ~g~~

~~IMF_MU_DMD~~

~~|- !f a Q. IMF (mu Q.. <> f) = IMF mu Q.. f~~

~~IMF_MU_NEG_DMD~~

~~|- !f a Q. IMF (mu Q.. ~ <> f) = IMF mu Q.. ~f~~

~~IMF_MU_BOX~~

~~|- !f a Q. IMF (mu Q.. [[a]] f) = IMF mu Q.. f~~

~~IMF_MU_NEG_BOX~~

~~|- !f a Q. IMF (mu Q.. ~[[a]] f) = IMF mu Q.. ~f~~

~~IMF_MU_MU~~

~~|- !f Q Q'. IMF (mu Q.. mu Q'.. f) ==> IMF mu Q'.. f~~

~~IMF_MU_NEG_MU~~

~~|- !f Q Q'. IMF (mu Q.. ~mu Q'.. f) ==> IMF mu Q'.. f~~

~~IMF_MU_NU~~

~~|- !f Q Q'. IMF (mu Q.. nu Q'.. f) ==> IMF mu Q'.. f~~

~~IMF_MU_NEG_NU~~

~~|- !f Q Q'. IMF (mu Q.. ~nu Q'.. f) ==> IMF mu Q'.. f~~

~~IMF_MU_NEG_NEG~~

~~|- !f a Q. IMF (mu Q.. ~ ~f) = IMF mu Q.. f~~

~~IMF_MU_INV_RVNEG~~

~~|- !f Q. IMF (mu Q.. f) = IMF mu Q.. RVNEG Q ~f~~

~~IMF_MU_EXT~~

~~|- !f. IMF f ==> ?Q. IMF mu Q.. f~~