Theory "mu"

Parents env muSyntax

Signature

Constant	Type
STATES_UNION_aux	:('prop mu # ('prop, 'state) KS # (string -> 'state -> bool) + 'prop mu # string # ('prop, 'state) KS # (string -> 'state -> bool) # num -> 'prop mu # ('prop, 'state) KS # (string -> 'state -> bool) + 'prop mu # string # ('prop, 'state) KS # (string -> 'state -> bool) # num -> bool) -> 'prop mu # ('prop, 'state) KS # (string -> 'state -> bool) + 'prop mu # string # ('prop, 'state) KS # (string -> 'state -> bool) # num -> 'state -> bool
STATES_UNION	:'prop mu # ('prop, 'state) KS # (string -> 'state -> bool) + 'prop mu # string # ('prop, 'state) KS # (string -> 'state -> bool) # num -> 'state -> bool
STATES	:'prop mu -> ('prop, 'state) KS -> (string -> 'state -> bool) -> 'state -> bool
MU_SAT	:'a mu -> ('a, 'b) KS -> (string -> 'b -> bool) -> 'b -> bool
MU_MODEL_SAT	:'a mu -> ('a, 'b) KS -> (string -> 'b -> bool) -> bool
FP	:'prop mu -> string -> ('prop, 'state) KS -> (string -> 'state -> bool) -> num -> 'state -> bool

Definitions

STATES_UNION_AUX_def

|- !R.
     STATES_UNION_aux R =
     WFREC R
       (\STATES_UNION a''.
          case a'' of
             INL (T,ks,e) -> I ks.S
          || INL (F,ks',e') -> I {}
          || INL (~f,ks'''',e'''') ->
               I (ks''''.S DIFF STATES_UNION (INL (f,ks'''',e'''')))
          || INL (f'' /\ g',ks'''''',e'''''') ->
               I
                 (STATES_UNION (INL (f'',ks'''''',e'''''')) INTER
                  STATES_UNION (INL (g',ks'''''',e'''''')))
          || INL (f' \/ g,ks''''',e''''') ->
               I
                 (STATES_UNION (INL (f',ks''''',e''''')) UNION
                  STATES_UNION (INL (g,ks''''',e''''')))
          || INL (RV Q,ks''',e''') -> I {s | s IN ks'''.S /\ e''' Q s}
          || INL (AP p,ks'',e'') -> I {s | s IN ks''.S /\ p IN ks''.L s}
          || INL (<> f''',ks''''''',e''''''') ->
               I
                 {s |
                  ?q.
                    q IN ks'''''''.S /\ s>--ks'''''''/a-->q /\
                    q IN STATES_UNION (INL (f''',ks''''''',e'''''''))}
          || INL ([[a']] f'''',ks'''''''',e'''''''') ->
               I
                 {s |
                  !q.
                    q IN ks''''''''.S /\
                    (s>--ks''''''''/a'-->q ==>
                     q IN STATES_UNION (INL (f'''',ks'''''''',e'''''''')))}
          || INL ((mu Q''.. f''''''),ks'''''''''',e'''''''''') ->
               I
                 {s |
                  ?n.
                    s IN
                    STATES_UNION
                      (INR
                         (f'''''',Q'',ks'''''''''',e''''''''''[[[Q''<--{}]]],
                          n))}
          || INL ((nu Q'.. f'''''),ks''''''''',e''''''''') ->
               I
                 {s |
                  !n.
                    s IN
                    STATES_UNION
                      (INR
                         (f''''',Q',ks''''''''',
                          e'''''''''[[[Q'<--ks'''''''''.S]]],n))}
          || INR (f''''''',Q''',ks''''''''''',e''''''''''',0) ->
               I (e''''''''''' Q''')
          || INR (f''''''',Q''',ks''''''''''',e''''''''''',SUC n) ->
               I
                 (STATES_UNION
                    (INL
                       (f''''''',ks''''''''''',
                        e'''''''''''[[[Q'''<--STATES_UNION
                                                (INR
                                                   (f''''''',Q''',
                                                    ks''''''''''',
                                                    e''''''''''',n))]]]))))

STATES_UNION_primitive_def

|- STATES_UNION =
   STATES_UNION_aux
     @R.
       WF R /\ (!e ks f. R (INL (f,ks,e)) (INL (~f,ks,e))) /\
       (!f e ks g. R (INL (g,ks,e)) (INL (f \/ g,ks,e))) /\
       (!g e ks f. R (INL (f,ks,e)) (INL (f \/ g,ks,e))) /\
       (!f e ks g. R (INL (g,ks,e)) (INL (f /\ g,ks,e))) /\
       (!g e ks f. R (INL (f,ks,e)) (INL (f /\ g,ks,e))) /\
       (!a e ks f. R (INL (f,ks,e)) (INL (<> f,ks,e))) /\
       (!e f a ks s q.
          s>--ks/a-->q ==> R (INL (f,ks,e)) (INL ([[a]] f,ks,e))) /\
       (!e ks Q f n.
          R (INR (f,Q,ks,e[[[Q<--ks.S]]],n)) (INL ((nu Q.. f),ks,e))) /\
       (!e ks Q f n.
          R (INR (f,Q,ks,e[[[Q<--{}]]],n)) (INL ((mu Q.. f),ks,e))) /\
       (!n Q e ks f.
          R (INL (f,ks,e[[[Q<--STATES_UNION_aux R (INR (f,Q,ks,e,n))]]]))
            (INR (f,Q,ks,e,SUC n))) /\
       !n e ks Q f. R (INR (f,Q,ks,e,n)) (INR (f,Q,ks,e,SUC n))

STATES_UNION_extract1_def

|- !x x1 x2 x3 x4. FP x x1 x2 x3 x4 = STATES_UNION (INR (x,x1,x2,x3,x4))

STATES_UNION_extract0_def

|- !x x1 x2. STATES x x1 x2 = STATES_UNION (INL (x,x1,x2))

MU_MODEL_SAT_def

|- !f ks e. MU_MODEL_SAT f ks e = !s. s IN ks.S0 ==> MU_SAT f ks e s

Theorems

STATES_def