Theory "cache"

Parents mu

Theorems

MU_SAT_RV_ENV_EQ

|- !ks.
     wfKS ks ==>
     !s Q e e' X.
       (MU_SAT (RV Q) ks e s = X) /\ (e Q = e' Q) ==>
       (MU_SAT (RV Q) ks e' s = X)

SAT_T_ENV_INV

|- !ks e e'. MU_SAT T ks e = MU_SAT T ks e'

SAT_F_ENV_INV

|- !ks e e'. MU_SAT F ks e = MU_SAT F ks e'

SAT_AP_ENV_INV

|- !ks p e e'. MU_SAT (AP p) ks e = MU_SAT (AP p) ks e'

SAT_RV_ENV_INV

|- !ks Q e e'. (e Q = e' Q) ==> (MU_SAT (RV Q) ks e = MU_SAT (RV Q) ks e')

SAT_NEG_ENV_INV

|- !ks.
     wfKS ks ==>
     !f e e'.
       (!e e'. MU_SAT f ks e = MU_SAT f ks e') ==>
       (MU_SAT (~f) ks e = MU_SAT (~f) ks e')

SAT_NEG_ENV_INV2

|- !ks.
     wfKS ks ==>
     !f e e'.
       (MU_SAT f ks e = MU_SAT f ks e') ==>
       (MU_SAT (~f) ks e = MU_SAT (~f) ks e')

SAT_CONJ_ENV_INV

|- !ks f g e e'.
     (!e e'. MU_SAT f ks e = MU_SAT f ks e') /\
     (!e e'. MU_SAT g ks e = MU_SAT g ks e') ==>
     (MU_SAT (f /\ g) ks e = MU_SAT (f /\ g) ks e')

SAT_CONJ_ENV_INV2

|- !ks f g e e'.
     (MU_SAT f ks e = MU_SAT f ks e') /\ (MU_SAT g ks e = MU_SAT g ks e') ==>
     (MU_SAT (f /\ g) ks e = MU_SAT (f /\ g) ks e')

SAT_DISJ_ENV_INV

|- !ks f g e e'.
     (!e e'. MU_SAT f ks e = MU_SAT f ks e') /\
     (!e e'. MU_SAT g ks e = MU_SAT g ks e') ==>
     (MU_SAT (f \/ g) ks e = MU_SAT (f \/ g) ks e')

SAT_DISJ_ENV_INV2

|- !ks f g e e'.
     (MU_SAT f ks e = MU_SAT f ks e') /\ (MU_SAT g ks e = MU_SAT g ks e') ==>
     (MU_SAT (f \/ g) ks e = MU_SAT (f \/ g) ks e')

SAT_DMD_ENV_INV

|- !ks a f e e'.
     (!e e'. MU_SAT f ks e = MU_SAT f ks e') ==>
     (MU_SAT <> f ks e = MU_SAT <> f ks e')

SAT_DMD_ENV_INV2

|- !ks a f e e'.
     (MU_SAT f ks e = MU_SAT f ks e') ==>
     (MU_SAT <> f ks e = MU_SAT <> f ks e')

SAT_BOX_ENV_INV

|- !ks a f e e'.
     (!e e'. MU_SAT f ks e = MU_SAT f ks e') ==>
     (MU_SAT [[a]] f ks e = MU_SAT [[a]] f ks e')

SAT_BOX_ENV_INV2

|- !ks a f e e'.
     (MU_SAT f ks e = MU_SAT f ks e') ==>
     (MU_SAT [[a]] f ks e = MU_SAT [[a]] f ks e')

SAT_LFP_ENV_INV

|- !ks s Q f e e'.
     (!s X e e'. MU_SAT f ks e[[[Q<--X]]] s = MU_SAT f ks e'[[[Q<--X]]] s) ==>
     (MU_SAT (mu Q.. f) ks e s = MU_SAT (mu Q.. f) ks e' s)

SAT_LFP_ENV_INV2

|- !ks Q f e e'.
     (!X. MU_SAT f ks e[[[Q<--X]]] = MU_SAT f ks e'[[[Q<--X]]]) ==>
     (MU_SAT (mu Q.. f) ks e = MU_SAT (mu Q.. f) ks e')

SAT_GFP_ENV_INV

|- !ks s Q f e e'.
     (!s X e e'. MU_SAT f ks e[[[Q<--X]]] s = MU_SAT f ks e'[[[Q<--X]]] s) ==>
     (MU_SAT (nu Q.. f) ks e s = MU_SAT (nu Q.. f) ks e' s)

SAT_GFP_ENV_INV2

|- !ks Q f e e'.
     (!X. MU_SAT f ks e[[[Q<--X]]] = MU_SAT f ks e'[[[Q<--X]]]) ==>
     (MU_SAT (nu Q.. f) ks e = MU_SAT (nu Q.. f) ks e')

STATES_FP_BIGUNION_2

|- !f ks e Q1 X Y Q.
     IMF (mu Q.. f) /\ IMF (mu Q1.. f) /\ wfKS ks /\ X SUBSET Y ==>
     BIGUNION {P | ?n. P = FP f Q ks e[[[Q1<--X]]][[[Q<--{}]]] n} SUBSET
     BIGUNION {P | ?n. P = FP f Q ks e[[[Q1<--Y]]][[[Q<--{}]]] n}

GEN_STATES_FP_BIGUNION

|- !f ks e e' Q.
     wfKS ks /\ IMF (mu Q.. f) /\
     (!Q'.
        (if ~RV Q' SUBF NNF f then e Q' = e' Q' else e Q' SUBSET e' Q')) ==>
     BIGUNION {P | ?n. P = FP f Q ks e[[[Q<--{}]]] n} SUBSET
     BIGUNION {P | ?n. P = FP f Q ks e'[[[Q<--{}]]] n}

STATES_DEF_SYM_MU

|- !f ks e Q n.
     STATES f ks e[[[Q<--FP f Q ks e[[[Q<--{}]]] n]]] =
     FP f Q ks e[[[Q<--{}]]] (SUC n)

STATES_FP_BIGINTER_2

|- !f ks e Q1 X Y Q.
     IMF (nu Q.. f) /\ IMF (nu Q1.. f) /\ wfKS ks /\ X SUBSET Y ==>
     BIGINTER {P | ?n. P = FP f Q ks e[[[Q1<--X]]][[[Q<--ks.S]]] n} SUBSET
     BIGINTER {P | ?n. P = FP f Q ks e[[[Q1<--Y]]][[[Q<--ks.S]]] n}

GEN_STATES_FP_BIGINTER

|- !f ks e e' Q.
     wfKS ks /\ IMF (nu Q.. f) /\
     (!Q'.
        (if ~RV Q' SUBF NNF f then e Q' = e' Q' else e Q' SUBSET e' Q')) ==>
     BIGINTER {P | ?n. P = FP f Q ks e[[[Q<--ks.S]]] n} SUBSET
     BIGINTER {P | ?n. P = FP f Q ks e'[[[Q<--ks.S]]] n}

STATES_DEF_SYM_NU

|- !f ks e Q n.
     STATES f ks e[[[Q<--FP f Q ks e[[[Q<--ks.S]]] n]]] =
     FP f Q ks e[[[Q<--ks.S]]] (SUC n)