examples/CCS/ObsCongrLawsScript.sml

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')))