examples/CCS/StrongLawsScript.sml

1824         (?f1 n1 f2 m2.
1826          (!j. j <= m2 ==> Is_Prefix(f2 j)) /\
1827          (x = par (SIGMA f1 n1) (SIGMA f2 m2)) /\
1831                                   (par (PREF_PROC (f1 i)) (SIGMA f2 m2))) n1)
1832                (SIGMA (\j. prefix (PREF_ACT(f2 j))
1833                                   (par (SIGMA f1 n1) (PREF_PROC (f2 j)))) m2))
1834               (ALL_SYNC f1 n1 f2 m2)))``
1857          (REWRITE_RULE [ASSUME ``E = par (SIGMA f1 n1) (SIGMA f2 m2)``]
1885                 (MATCH_MP (ASSUME ``!(j :num). j <= m2 ==> Is_Prefix (f2 j)``)
1888             (REWRITE_RULE [ASSUME ``(f2: num -> ('a, 'b) CCS) k = prefix u' E''``]
1889                 (ASSUME ``TRANS ((f2: num -> ('a, 'b) CCS) k) u E1'``)) \\
1898                 (MATCH_MP (ASSUME ``!(j :num). j <= m2 ==> Is_Prefix (f2 j)``)
1905             (REWRITE_RULE [ASSUME ``(f2: num -> ('a, 'b) CCS) k = prefix u' E''``]
1906                 (ASSUME ``TRANS ((f2: num -> ('a, 'b) CCS) k) (label (COMPL l)) E2``)) \\
1920                                               (par (PREF_PROC (f1 i)) (SIGMA f2 m2))) n1)
1922                                    (\j:num. prefix (PREF_ACT (f2 j))
1923                                               (par (SIGMA f1 n1) (PREF_PROC (f2 j)))) m2))
1924                              (ALL_SYNC f1 n1 f2 m2)``]
1930                                        (par (PREF_PROC (f1 i)) (SIGMA f2 m2))) n1``,
1931                     ``SIGMA (\j:num. prefix (PREF_ACT (f2 j))
1932                                        (par (SIGMA f1 n1) (PREF_PROC (f2 j)))) m2``,
1940                                             (par (PREF_PROC (f1 i)) (SIGMA f2 m2))) k)
1956                (ASSUME ``TRANS ((\j: num. prefix (PREF_ACT (f2 j))
1957                                             (par (SIGMA f1 n1) (PREF_PROC (f2 j)))) k)
1962                 (MATCH_MP (ASSUME ``!(j :num). j <= m2 ==> Is_Prefix (f2 j)``)
1991                 (MATCH_MP (ASSUME ``!(j :num). j <= m2 ==> Is_Prefix (f2 j)``)
1994              (REWRITE_RULE [ASSUME ``(f2: num -> ('a, 'b) CCS) k' = prefix u' E''``,
1996                 (ASSUME ``PREF_ACT ((f2: num -> ('a, 'b) CCS) k') = label (COMPL l)``)) \\