Lines Matching refs:prefix
105 WEAK_EQUIV (par (prefix u E) (prefix tau E'))
106 (sum (prefix u (par E (prefix tau E')))
107 (prefix tau (par (prefix u E) E')))
115 WEAK_EQUIV (par (prefix tau E) (prefix u E'))
116 (sum (prefix tau (par E (prefix u E')))
117 (prefix u (par (prefix tau E) E')))
125 WEAK_EQUIV (par (prefix tau E) (prefix tau E'))
126 (sum (prefix tau (par E (prefix tau E')))
127 (prefix tau (par (prefix tau E) E')))
136 WEAK_EQUIV (par (prefix (label l) E) (prefix (label l') E'))
137 (sum (prefix (label l) (par E (prefix (label l') E')))
138 (prefix (label l') (par (prefix (label l) E) E'))))
151 WEAK_EQUIV (par (prefix (label l) E) (prefix (label l') E'))
153 (sum (prefix (label l) (par E (prefix (label l') E')))
154 (prefix (label l') (par (prefix (label l) E) E')))
155 (prefix tau (par E E'))))
172 (SIGMA (\i. prefix (PREF_ACT (f i)) (par (PREF_PROC (f i)) (SIGMA f' m))) n)
173 (SIGMA (\j. prefix (PREF_ACT (f' j)) (par (SIGMA f n) (PREF_PROC (f' j)))) m))
201 |- !E L. WEAK_EQUIV (restr (prefix tau E) L) (prefix tau (restr E L))
209 (!E. WEAK_EQUIV (restr (prefix (label l) E) L) nil)
222 (SPECL [``restr (L :'b Label set) (prefix (label l) E)``, ``nil``]
228 (!E. WEAK_EQUIV (restr (prefix (label l) E) L) (prefix (label l) (restr E L)))
241 (SPECL [``restr (L :'b Label set) (prefix (label l) E)``,
242 ``prefix (label (l :'b Label)) (restr L E)``]
266 WEAK_EQUIV (relab (prefix u E) (RELAB labl))
267 (prefix (relabel (Apply_Relab labl) u) (relab E (RELAB labl)))
290 (prefix u (rec s (prefix v (prefix u (var s)))))
291 (rec s (prefix u (prefix v (var s))))
303 (* Prove TAU_WEAK: |- !E. WEAK_EQUIV (prefix tau E) E *)
305 ``!E. WEAK_EQUIV (prefix tau E) E``,