Theory "decomp"

Parents MachineTransition mu

Signature

Constant	Type
AP_EXT	:('state1 -> bool) mu -> ('state1 # 'state2 -> bool) mu

Definitions

AP_EXT_def

|- (AP_EXT T = T) /\ (AP_EXT F = F) /\ (!f. AP_EXT ~f = ~AP_EXT f) /\
   (!f1 f2. AP_EXT (f1 /\ f2) = AP_EXT f1 /\ AP_EXT f2) /\
   (!f1 f2. AP_EXT (f1 \/ f2) = AP_EXT f1 \/ AP_EXT f2) /\
   (!Q. AP_EXT (RV Q) = RV Q) /\
   (!p. AP_EXT AP p = AP @p'. !s1 s2. p s1 = p' (s1,s2)) /\
   (!a f. AP_EXT <> f = <> (AP_EXT f)) /\
   (!a f. AP_EXT [[a]] f = [[a]] (AP_EXT f)) /\
   (!Q f. AP_EXT (mu Q.. f) = mu Q.. AP_EXT f) /\
   !Q f. AP_EXT (nu Q.. f) = nu Q.. AP_EXT f

Theorems

APEXT_NNF

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

APEXT_IMF

|- !f. IMF f = IMF (AP_EXT f)

AP_EXT_THM

|- !ks1 ks2 s1 s2 e1 e2 f.
     wfKS ks1 ==>
     wfKS ks2 ==>
     (!p s1. p IN ks1.L s1 = p s1) ==>
     (!p s1 s2. p IN ks2.L (s1,s2) = p (s1,s2)) ==>
     (!p.
        p IN ks1.ap ==> ?p'. !s1 s2. p IN ks1.L s1 = p' IN ks2.L (s1,s2)) ==>
     (!a s1 s1' s2 s2'. s1>--ks1/a-->s1' = (s1,s2)>--ks2/a-->(s1',s2')) ==>
     (!Q s1 s2. s1 IN e1 Q = (s1,s2) IN e2 Q) ==>
     IMF f ==>
     (!p. AP p SUBF f ==> p IN ks1.ap) ==>
     (s1 IN STATES f ks1 e1 = (s1,s2) IN STATES (AP_EXT f) ks2 e2)

PAR_SYNC_DECOMP

|- !s e ks1 ks2 f.
     wfKS ks1 ==>
     wfKS ks2 ==>
     (ks1.ap = ks2.ap) ==>
     (ks1.L = ks2.L) ==>
     (!a s s'. ks2.T a (s,s') ==> ks1.T a (s,s')) ==>
     IMF f ==>
     (!a g. ~(<> g SUBF NNF f)) ==>
     s IN STATES f ks1 e ==>
     s IN STATES f ks2 e