Lines Matching refs:prefix
522 STRONG_EQUIV (par (prefix u E) (prefix tau E'))
523 (sum (prefix u (par E (prefix tau E')))
524 (prefix tau (par (prefix u E) E')))``,
529 (?(u' :'b Action) E1 E2. (x = par (prefix u' E1) (prefix tau E2)) /\
530 (y = sum (prefix u' (par E1 (prefix tau E2)))
531 (prefix tau (par (prefix u' E1) E2))))``
553 ASSUME_TAC (REWRITE_RULE [ASSUME ``E = par (prefix u' E1) (prefix tau E2)``]
571 [ASSUME ``E' = sum (prefix u' (par E1 (prefix tau E2)))
572 (prefix tau (par (prefix u' E1) E2))``]
589 (par (prefix tau E) (prefix u E'))
590 (sum (prefix tau (par E (prefix u E')))
591 (prefix u (par (prefix tau E) E')))
601 (SPECL [``prefix (tau :'b Action) E``, ``prefix (u :'b Action) E'``] STRONG_PAR_COMM)
603 (SPECL [``prefix (u :'b Action) (par E' (prefix tau E))``,
604 ``prefix (tau :'b Action) (par (prefix u E') E)``] STRONG_SUM_COMM))
608 (SPECL [``prefix (u :'b Action) E'``, ``E :('a, 'b) CCS``] STRONG_PAR_COMM)))
611 (SPECL [``E' :('a, 'b) CCS``, ``prefix (tau :'b Action) E``] STRONG_PAR_COMM)))))));
632 (par (prefix (label l) E) (prefix (label l') E'))
633 (sum (prefix (label l) (par E (prefix (label l') E')))
634 (prefix (label l') (par (prefix (label l) E) E'))))``,
640 (x = par (prefix (label l1) E1) (prefix (label l2) E2)) /\
641 (y = sum (prefix (label l1) (par E1 (prefix (label l2) E2)))
642 (prefix (label l2) (par (prefix (label l1) E1) E2)))``
662 [ASSUME ``E = par (prefix (label l1) E1) (prefix (label l2) E2)``]
672 (ASSUME ``TRANS (par (prefix (label l1) E1)
673 (prefix (label l2) E2)) u E1'``)) \\
680 (prefix (label l1) (par E1 (prefix (label l2) E2)))
681 (prefix (label l2) (par (prefix (label l1) E1) E2))``]
702 (par (prefix (label l) E) (prefix (label l') E'))
704 (sum (prefix (label l) (par E (prefix (label l') E')))
705 (prefix (label l') (par (prefix (label l) E) E')))
706 (prefix tau (par E E')))``,
713 (x = par (prefix (label l1) E1) (prefix (label l2) E2)) /\
715 (sum (prefix (label l1) (par E1 (prefix (label l2) E2)))
716 (prefix (label l2) (par (prefix (label l1) E1) E2)))
717 (prefix tau (par E1 E2)))``
740 [ASSUME ``E = par (prefix (label l1) E1) (prefix (label l2) E2)``]
755 [ASSUME ``E' = sum (sum (prefix (label l1) (par E1 (prefix (label l2) E2)))
756 (prefix (label l2) (par (prefix (label l1) E1) E2)))
757 (prefix tau (par E1 E2))``]
889 STRONG_EQUIV (restr L (prefix tau E)) (prefix tau (restr L E))``,
893 ``\x y. (x = y) \/ (?E' L'. (x = restr L' (prefix tau E')) /\
894 (y = prefix tau (restr L' E')))``
910 ASSUME_TAC (REWRITE_RULE [ASSUME ``E = restr L' (prefix tau E'')``]
922 ASSUME_TAC (REWRITE_RULE [ASSUME ``E' = prefix tau (restr L' E'')``]
935 (!E. STRONG_EQUIV (restr L (prefix (label l) E)) nil)``,
942 (x = restr L' (prefix (label l') E')) /\
954 ASSUME_TAC (REWRITE_RULE [ASSUME ``E = restr L' (prefix (label l') E'')``]
962 ASSUME_TAC (REWRITE_RULE [ASSUME ``E = restr L' (prefix (label l') E'')``]
978 (!E. STRONG_EQUIV (restr L (prefix (label l) E))
979 (prefix (label l) (restr L E)))``,
985 (x = restr L' (prefix (label l') E')) /\
986 (y = prefix (label l') (restr L' E'))``
1007 ASSUME_TAC (REWRITE_RULE [ASSUME ``E = restr L' (prefix (label l') E'')``]
1020 ASSUME_TAC (REWRITE_RULE [ASSUME ``E' = prefix (label l') (restr L' E'')``]
1092 STRONG_EQUIV (relab (prefix u E) (RELAB labl))
1093 (prefix (relabel (RELAB labl) u) (relab E (RELAB labl)))``,
1097 ``\x y. (x = y) \/ (?u' E'. (x = relab (prefix u' E') (RELAB labl)) /\
1098 (y = prefix (relabel (RELAB labl) u')
1116 ASSUME_TAC (REWRITE_RULE [ASSUME ``E = relab (prefix u' E'') (RELAB labl)``]
1124 [ASSUME ``E' = prefix (relabel (RELAB labl) u')
1178 STRONG_EQUIV (prefix u (rec s (prefix v (prefix u (var s)))))
1179 (rec s (prefix u (prefix v (var s))))``,
1185 (x = prefix u' (rec s' (prefix v' (prefix u' (var s'))))) /\
1186 (y = rec s' (prefix u' (prefix v' (var s')))) \/
1187 (x = rec s' (prefix v' (prefix u' (var s')))) /\
1188 (y = prefix v' (rec s' (prefix u' (prefix v' (var s')))))``
1200 [ASSUME ``E = prefix u' (rec s' (prefix v' (prefix u' (var s'))))``]
1203 EXISTS_TAC ``prefix (v' :'b Action) (rec s' (prefix u' (prefix v' (var s'))))`` \\
1213 [ASSUME ``E' = rec s' (prefix u' (prefix v' (var s')))``,
1217 EXISTS_TAC ``rec s' (prefix v' (prefix u (var s')))`` \\
1225 (ASSUME ``E2 = prefix v' (rec s' (prefix u' (prefix v' (var s'))))``)] ],
1228 [ASSUME ``E = rec s' (prefix v' (prefix u' (var s')))``,
1232 EXISTS_TAC ``rec s' (prefix u' (prefix v' (var s')))`` \\
1240 [ASSUME ``E' = prefix v' (rec s' (prefix u' (prefix v' (var s'))))``]
1243 EXISTS_TAC ``prefix (u' :'b Action)
1244 (rec s' (prefix v' (prefix u' (var s'))))`` \\
1259 (rec s (prefix u (prefix u (var s))))
1260 (rec s (prefix u (var s)))``,
1266 (x = rec s' (prefix u' (prefix u' (var s')))) /\
1267 (y = rec s' (prefix u' (var s'))) \/
1268 (x = prefix u' (rec s' (prefix u' (prefix u' (var s'))))) /\
1269 (y = rec s' (prefix u' (var s'))))``
1281 (REWRITE_RULE [ASSUME ``E = rec s' (prefix u' (prefix u' (var s')))``,
1293 ASSUME_TAC (REWRITE_RULE [ASSUME ``E' = rec s'(prefix u'(var s'))``,
1297 EXISTS_TAC ``prefix (u' :'b Action) E`` \\
1309 [ASSUME ``E = prefix u' (rec s' (prefix u' (prefix u' (var s'))))``]
1322 ASSUME_TAC (REWRITE_RULE [ASSUME ``E' = rec s' (prefix u' (var s'))``,
1326 EXISTS_TAC ``rec s' (prefix u' (prefix u' (var s')))`` \\
1342 PREF_ACT (prefix (u :'b Action) E) = u `;
1345 PREF_PROC (prefix (u :'b Action) E) = E `;
1348 Is_Prefix E = (?(u :'b Action) E'. (E = prefix u E')) `;
1351 "PREF_IS_PREFIX", ``!(u :'b Action) E. Is_Prefix (prefix u E)``,
1416 then (prefix tau (par P (PREF_PROC (f 0))))
1422 then (sum (prefix tau (par P (PREF_PROC (f (SUC n))))) (SYNC u P f n))
1814 (SIGMA (\i. prefix (PREF_ACT (f i))
1816 (SIGMA (\j. prefix (PREF_ACT (f' j))
1830 (SIGMA (\i. prefix (PREF_ACT (f1 i))
1832 (SIGMA (\j. prefix (PREF_ACT(f2 j))
1872 (REWRITE_RULE [ASSUME ``(f1: num -> ('a, 'b) CCS) k = prefix u' E''``]
1888 (REWRITE_RULE [ASSUME ``(f2: num -> ('a, 'b) CCS) k = prefix u' E''``]
1905 (REWRITE_RULE [ASSUME ``(f2: num -> ('a, 'b) CCS) k = prefix u' E''``]
1908 (REWRITE_RULE [ASSUME ``(f1: num -> ('a, 'b) CCS) k' = prefix u'' E'''``]
1919 (\i:num. prefix (PREF_ACT (f1 i))
1922 (\j:num. prefix (PREF_ACT (f2 j))
1929 (SPECL [``SIGMA (\i:num. prefix (PREF_ACT (f1 i))
1931 ``SIGMA (\j:num. prefix (PREF_ACT (f2 j))
1939 (ASSUME ``TRANS ((\i: num. prefix (PREF_ACT (f1 i))
1956 (ASSUME ``TRANS ((\j: num. prefix (PREF_ACT (f2 j))
1983 (REWRITE_RULE [ASSUME ``(f1: num -> ('a, 'b) CCS) k = prefix u' E''``,
1994 (REWRITE_RULE [ASSUME ``(f2: num -> ('a, 'b) CCS) k' = prefix u' E''``,