Lines Matching refs:prefix
87 OBS_CONGR (par (prefix u E) (prefix tau E'))
88 (sum (prefix u (par E (prefix tau E')))
89 (prefix tau (par (prefix u E) E')))
97 OBS_CONGR (par (prefix tau E) (prefix u E'))
98 (sum (prefix tau (par E (prefix u E')))
99 (prefix u (par (prefix tau E) E')))
107 OBS_CONGR (par (prefix tau E) (prefix tau E'))
108 (sum (prefix tau (par E (prefix tau E')))
109 (prefix tau (par (prefix tau E) E')))
118 OBS_CONGR (par (prefix (label l) E) (prefix (label l') E'))
119 (sum (prefix (label l) (par E (prefix (label l') E')))
120 (prefix (label l') (par (prefix (label l) E) E'))))
133 OBS_CONGR (par (prefix (label l) E) (prefix (label l') E'))
135 (sum (prefix (label l) (par E (prefix (label l') E')))
136 (prefix (label l') (par (prefix (label l) E) E')))
137 (prefix tau (par E E'))))
154 (SIGMA (\i. prefix (PREF_ACT (f i)) (par (PREF_PROC (f i)) (SIGMA f' m))) n)
155 (SIGMA (\j. prefix (PREF_ACT (f' j)) (par (SIGMA f n) (PREF_PROC (f' j)))) m))
183 |- !E L. OBS_CONGR (restr (prefix tau E) L) (prefix tau (restr E L))
192 (!E. OBS_CONGR (restr L (prefix (label l) E)) nil)
205 (SPECL [``restr (L :'b Label set) (prefix (label l) E)``, ``nil``]
211 (!E. OBS_CONGR (restr (prefix (label l) E) L) (prefix (label l) (restr E L)))
224 (SPECL [``restr (L :'b Label set) (prefix (label l) E)``,
225 ``prefix (label (l :'b Label)) (restr L E)``]
245 (prefix u (rec s (prefix v (prefix u (var s)))))
246 (rec s (prefix u (prefix v (var s))))
273 OBS_CONGR (relab (prefix u E) (RELAB labl))
274 (prefix (relabel (RELAB labl) u) (relab E (RELAB labl)))
288 |- !u E. OBS_CONGR (prefix u (prefix tau E)) (prefix u E)
291 ``!(u :'b Action) E. OBS_CONGR (prefix u (prefix tau E)) (prefix u E)``,
299 EXISTS_TAC ``prefix (u :'b Action) E`` \\
304 EXISTS_TAC ``prefix (tau :'b Action) E2`` \\
306 EXISTS_TAC ``prefix (u :'b Action) (prefix tau E2)`` \\
307 EXISTS_TAC ``prefix (tau :'b Action) E2`` \\
311 |- !u E. WEAK_EQUIV (prefix u (prefix tau E)) (prefix u E)
317 |- !E. OBS_CONGR (sum E (prefix tau E)) (prefix tau E)
320 ``!E. OBS_CONGR (sum E (prefix tau E)) (prefix tau E)``,
342 take [`sum E (prefix tau E)`, `E2`] \\
348 |- !E. WEAK_EQUIV (sum E (prefix tau E)) (prefix tau E)
355 OBS_CONGR (sum (prefix u (sum E (prefix tau E'))) (prefix u E'))
356 (prefix u (sum E (prefix tau E')))
360 OBS_CONGR (sum (prefix u (sum E (prefix tau E'))) (prefix u E'))
361 (prefix u (sum E (prefix tau E')))``,
376 take [`prefix (u :'b Action) (sum E (prefix tau E'))`,
377 `sum E (prefix tau E')`] \\
386 take [`sum (prefix u (sum E (prefix tau E'))) (prefix u E')`, `E2`] \\
393 WEAK_EQUIV (sum (prefix u (sum E (prefix tau E'))) (prefix u E'))
394 (prefix u (sum E (prefix tau E')))