%% PVS Version 3.1 %% 6.2 [Linux (x86)] (Feb 14, 2003 18:42) $$$pvs-strategies ;; ;; Proof rules for CSP ;; ;; Each rule corresponds to a step in a proof of A # R |> RankUser(rho) ;; ;; initialisation: install all the automatic rules ;; is assumes that the events are of type ;; "event[id, msg]" (defstep init-csp (id msg) (let ((rank-user-stop (format nil "rank_user_stop[~A,~A]" id msg)) (rank-user-input (format nil "rank_user_input[~A,~A]" id msg)) (rank-user-output (format nil "rank_user_output[~A,~A]" id msg)) (restriction-stop (format nil "restriction_stop[event[~A,~A]]" id msg))) (auto-rewrite rank-user-stop rank-user-input rank-user-output restriction-stop)) "Installs the automatic CSP rules" "Installing CSP rules") ;; choice: applies the simple choice rule (defstep choice () (try (rewrite "restriction_choice") (then (rewrite "rank_user_choice") (ground)) (skip-msg "No change")) "CSP rule for (P1 \/ P2) # R |> RankUser(rho)." "Applying choice rule") ;; choice2: same thing for unbounded choice (defstep choice2 () (try (rewrite "restriction_choice2") (then (rewrite "rank_user_choice2") (skolem!)) (skip-msg "No change")) "CSP rule for Choice(SP) # R |> RankUser(rho)" "Applying choice rule") ;; choice3: parametric choice (defstep choice3 () (try (rewrite "restriction_choice3") (then (rewrite "rank_user_choice3") (skolem!)) (skip-msg "No change")) "CSP rule for Choice! i : P(i) # R |> RankUser(rho)" "Applying choice rule") ;; prefix (defstep prefix () (try (rewrite "restriction_pref") (then* (lift-if) (assert) (prop)) (skip-msg "No change")) "CSP rule for (a >> P) # R |> RankUser(rho)" "Applying prefix rule") ;; parallel composition with synchro (defstep parallel () (try (rewrite "restriction_par") (then (rewrite "rank_user_par")(prop)) (skip-msg "No change")) "CSP rule for Par(A)(P1, P2) # R |> RankUser(rho)" "Applying parallel rule") ;; free parallel composition (defstep interleaving () (try (rewrite "restriction_free_par") (then (rewrite "rank_user_free_par")(prop)) (skip-msg "No change")) "CSP rule for (P1 // P2) # R |> RankUser(rho)" "Applying interleaving rule") ;; multiple parallel composition (defstep parallel2 () (try (rewrite "restriction_par2") (then (rewrite "rank_rule_par2")(skolem!)) (skip-msg "No change")) "CSP rule for Par(A)(lambda i : P(i)) # R |> RankUser(rho)" "Applying parallel rule") ;; multiple interleaving (defstep interleaving2 () (try (rewrite "restriction_free_par2") (then (rewrite "rank_user_free_par2")(skolem!)) (skip-msg "No change")) "CSP rule for (P1 // P2) # R |> RankUser(rho)" "Applying interleaving rule") $$$csp_traces.pvs % % Includes all the basic theories for CSP % trace semantics % csp_traces : THEORY BEGIN IMPORTING processes, parametric_choice, multipar, satisfaction, satisfaction2, satisfaction3, fixed_points, fixed_points2, process_rules END csp_traces $$$fixed_points2.pvs % % Theory for non-parametic fixed points % i.e. of monotonic functions F : [process[T] -> process[T]] % fixed_points2 [ T : TYPE ] : THEORY BEGIN IMPORTING fixed_points F : VAR [process[T] -> process[T]] X, Y : VAR process[T] %----------------------- % Monotonic functions %----------------------- monotonic?(F) : bool = FORALL X, Y : subset?(X, Y) IMPLIES subset?(F(X), F(Y)) G : VAR (monotonic?) %----------------------------------------------------------- % short cut: everything translated to the parametric case %----------------------------------------------------------- dummy : NONEMPTY_TYPE rep : dummy x : VAR dummy H : VAR [dummy -> process[T]] ext(F)(H) : [dummy -> process[T]] = lambda x : F(H(x)) mu(G) : process[T] = mu(ext(G))(rep) closure_mu2 : LEMMA subset?(G(mu(G)), mu(G)) smallest_closed2 : LEMMA subset?(G(X), X) IMPLIES subset?(mu(G), X) fixed_point2 : LEMMA G(mu(G)) = mu(G) least_fixed_point2 : LEMMA G(X) = X IMPLIES subset?(mu(G), X) %--------------------- % Induction rules %--------------------- E : VAR set[trace[T]] induction : PROPOSITION Stop[T] |> E AND (FORALL X : X |> E IMPLIES G(X) |> E) IMPLIES mu(G) |> E induction2 : PROPOSITION E(null) AND (FORALL X : X |> E IMPLIES G(X) |> E) IMPLIES mu(G) |> E END fixed_points2 $$$fixed_points2.prf (|fixed_points2| (|mu_TCC1| "" (GRIND :IF-MATCH NIL) (("" (INST - "X!1(x!1)" "Y!1(x!1)") (("" (REDUCE) NIL))))) (|closure_mu2| "" (SKOLEM!) (("" (AUTO-REWRITE "mu_TCC1" "ext" "<=") (("" (EXPAND "mu") (("" (USE "closure_mu" ("G" "ext(G!1)")) (("" (ASSERT) (("" (INST?) NIL))))))))))) (|smallest_closed2| "" (SKOSIMP) (("" (AUTO-REWRITE "mu_TCC1" "ext" "<=") (("" (EXPAND "mu") (("" (USE "smallest_closed" ("G" "ext(G!1)" "X" "lambda x : X!1")) (("" (GROUND) (("1" (INST?) NIL) ("2" (SKOLEM!) NIL))))))))))) (|fixed_point2| "" (SKOLEM!) (("" (AUTO-REWRITE "mu_TCC1" "ext" "<=") (("" (USE "fixed_point" ("G" "ext(G!1)")) (("" (EXPAND "mu" 1 2) (("" (REPLACE -1 + RL) (("" (ASSERT) (("" (EXPAND "mu" 1 1) (("" (PROPAX) NIL))))))))))))))) (|least_fixed_point2| "" (SKOSIMP) (("" (AUTO-REWRITE "mu_TCC1" "ext" "<=") (("" (EXPAND "mu") (("" (USE "least_fixed_point" ("G" "ext(G!1)" "X" "lambda x : X!1")) (("" (GROUND) (("1" (INST?) NIL) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))))))) (|induction| "" (SKOSIMP) (("" (AUTO-REWRITE "mu_TCC1" "ext") (("" (EXPAND "mu") (("" (USE "param_induction" ("G" "ext(G!1)" "E" "lambda x : E!1")) (("" (GROUND) (("1" (INST?) NIL) ("2" (SKOLEM!) NIL) ("3" (SKOSIMP*) (("3" (INST?) (("3" (INST?) (("3" (ASSERT) NIL))))))))))))))))) (|induction2| "" (SKOSIMP) (("" (USE "induction") (("" (GROUND) (("" (DELETE -2 2) (("" (GRIND) NIL)))))))))) $$$fixed_points.pvs fixed_points [ U, T : TYPE ] : THEORY BEGIN IMPORTING processes, satisfaction x, x1, x2 : VAR U X, Y, Z : VAR [U -> process[T]]; t : VAR trace[T] Q : VAR process[T] %================================================= % Fixed points of a monotonic function F % F : [[U -> process[T]] -> [U -> process[T]]] %================================================= %-------------------------------------- % Order between parametric processes %-------------------------------------- <=(X, Y) : bool = FORALL x : subset?(X(x), Y(x)) reflexive : LEMMA X <= X antisymmetric : LEMMA X <= Y AND Y <= X IMPLIES X = Y transitive : LEMMA X <= Y AND Y <= Z IMPLIES X <= Z %------------------------ % greater lower bounds %------------------------ SX : VAR set[[U -> process[T]]] glb(SX)(x) : process[T] = { t | FORALL (X : (SX)) : X(x)(t) } glb_is_bound : LEMMA FORALL (X : (SX)) : glb(SX) <= X glb_is_inf : LEMMA (FORALL (X : (SX)) : Y <= X) IMPLIES Y <= glb(SX) %--------------- % Fixed point %--------------- F : VAR [[U -> process[T]] -> [U -> process[T]]] monotonic?(F) : bool = FORALL X, Y : X <= Y IMPLIES F(X) <= F(Y) G : VAR (monotonic?) mu(G) : [U -> process[T]] = glb({X | G(X) <= X}) closure_mu : LEMMA G(mu(G)) <= mu(G) smallest_closed : LEMMA G(X) <= X IMPLIES mu(G) <= X fixed_point : LEMMA G(mu(G)) = mu(G) least_fixed_point : LEMMA G(X) = X IMPLIES mu(G) <= X %------------------- % Induction rule %------------------- E : VAR [ U -> pred[trace[T]] ] <(X, E) : bool = FORALL x : X(x) |> E(x) pseudo_transitive : LEMMA X <= Y AND Y < E IMPLIES X < E SY : VAR { SX | not empty?(SX) } lub(SY)(x) : process[T] = { t | EXISTS (X : (SY)) : X(x)(t) } lub_is_bound : LEMMA FORALL (X : (SY)) : X <= lub(SY) lub_is_sup : LEMMA (FORALL (X : (SY)) : X < E) IMPLIES lub(SY) < E induction_aux : LEMMA (EXISTS X : X < E) AND (FORALL X : X < E implies G(X) < E) IMPLIES mu(G) < E param_induction0 : PROPOSITION (FORALL x : EXISTS Q : Q |> E(x)) AND (FORALL X : (FORALL x : X(x) |> E(x)) => (FORALL x : G(X)(x) |> E(x))) IMPLIES (FORALL x : mu(G)(x) |> E(x)) param_induction : PROPOSITION (FORALL x : Stop[T] |> E(x)) AND (FORALL X : (FORALL x : X(x) |> E(x)) => (FORALL x : G(X)(x) |> E(x))) IMPLIES (FORALL x : mu(G)(x) |> E(x)) param_induction2 : PROPOSITION (FORALL x : E(x)(null)) AND (FORALL X : (FORALL x : X(x) |> E(x)) => (FORALL x : G(X)(x) |> E(x))) IMPLIES (FORALL x : mu(G)(x) |> E(x)) END fixed_points $$$fixed_points.prf (|fixed_points| (|reflexive| "" (GRIND) NIL NIL) (|antisymmetric| "" (GRIND :IF-MATCH NIL) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) (("" (INST?) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) (("" (INST?) (("" (BDDSIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|transitive| "" (GRIND) NIL NIL) (|glb_TCC1| "" (GRIND :IF-MATCH NIL :EXCLUDE "prefix") (("" (INST?) (("" (TYPEPRED "X!1(x!1)") (("" (ASSERT) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|glb_is_bound| "" (GRIND) NIL NIL) (|glb_is_inf| "" (GRIND :IF-MATCH BEST) NIL NIL) (|closure_mu| "" (AUTO-REWRITE "glb_is_bound" "mu" "monotonic?") (("" (SKOLEM-TYPEPRED) (("" (ASSERT) (("" (REWRITE "glb_is_inf") (("" (SKOLEM-TYPEPRED) (("" (INST - "mu(G!1)" "X!1") (("" (ASSERT) (("" (USE "transitive" ("X" "G!1(mu(G!1))" "Y" "G!1(X!1)" "Z" "X!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|smallest_closed| "" (AUTO-REWRITE "mu" "glb_is_bound") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|fixed_point| "" (AUTO-REWRITE "monotonic?") (("" (SKOLEM-TYPEPRED) (("" (USE* "closure_mu" "antisymmetric") (("" (ASSERT) (("" (DELETE 2) (("" (EXPAND "mu" 1 1) (("" (REWRITE "glb_is_bound") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|least_fixed_point| "" (SKOSIMP) (("" (REWRITE "smallest_closed") (("" (REPLACE*) (("" (REWRITE "reflexive") NIL NIL)) NIL)) NIL)) NIL) (|pseudo_transitive| "" (GRIND) NIL NIL) (|lub_TCC1| "" (GRIND :EXCLUDE ("prefix")) (("" (TYPEPRED "X!1(x!1)") (("" (ASSERT) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|lub_is_bound| "" (GRIND) NIL NIL) (|lub_is_sup| "" (GRIND) NIL NIL) (|induction_aux| "" (SKOSIMP) (("" (CASE "empty?({ X | X < E!1})") (("1" (DELETE -3 1) (("1" (GRIND :EXCLUDE ("<" "prefix_closed") :IF-MATCH NIL) (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (DELETE -1 1) (("2" (NAME "Z!1" "lub({X | X < E!1})") (("2" (USE "lub_is_sup" ("E" "E!1")) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) (("2" (USE "lub_is_bound" ("SY" "{X | X < E!1}" "X" "G!1(Z!1)")) (("2" (REPLACE*) (("2" (FORWARD-CHAIN "smallest_closed") (("2" (FORWARD-CHAIN "pseudo_transitive") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|param_induction0| "" (SKOSIMP) (("" (USE "induction_aux") (("" (EXPAND "<") (("" (GROUND) (("" (DELETE -2 2) (("" (INST + "lambda x : epsilon! Q : Q |> E!1(x)") (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) (("" (USE "epsilon_ax" ("p" "lambda Q : Q |> E!1(x!1)")) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|param_induction| "" (SKOSIMP) (("" (REWRITE "param_induction0") (("" (DELETE -2 2) (("" (SKOLEM!) (("" (INST? -) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|param_induction2| "" (SKOSIMP) (("" (REWRITE "param_induction") (("" (DELETE -2 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) $$$satisfaction3.pvs % % Properties of sat and unbounded interleave % satisfaction3 [U : NONEMPTY_TYPE, T : TYPE ] : THEORY BEGIN IMPORTING satisfaction, multipar P : VAR [U -> process[T]] x : VAR U E : VAR set[trace[T]] sat_free_par3 : LEMMA Interleave(P) |> E IMPLIES P(x) |> E END satisfaction3 $$$satisfaction3.prf (|satisfaction3| (|sat_free_par3| "" (SKOSIMP) (("" (USE "interleave_subset3[U, T]") (("" (REWRITE "|>" :DIR RL) (("" (FORWARD-CHAIN "sat_transitive1") NIL)))))))) $$$satisfaction2.pvs satisfaction2 [ T : TYPE, U : TYPE ] : THEORY BEGIN IMPORTING satisfaction, parametric_choice P : VAR [U -> process[T]] x : VAR U E : VAR set[trace[T]] sat_choice3 : LEMMA Choice(P) |> E IFF Stop[T] |> E AND (FORALL x : P(x) |> E) END satisfaction2 $$$satisfaction2.prf (|satisfaction2| (|sat_choice3| "" (GRIND :EXCLUDE ("prefix_closed")) NIL)) $$$satisfaction.pvs % % Definition of the satisfaction relation % - if P is a process, E a trace predicate % P |> E means "P sat E" % - if E is also a process, % P |> E can mean "P is a refinement of E" % satisfaction [T : TYPE ] : THEORY BEGIN IMPORTING processes, process_rules P, Q : VAR process[T] E, F : VAR pred[trace[T]] SP : VAR set[process[T]] |> (P, E) : bool = subset?(P, E) sat_idempotent : LEMMA P |> P sat_transitive1 : LEMMA (P |> Q) AND (Q |> E) IMPLIES (P |> E) sat_transitive2 : LEMMA (P |> E) AND subset?(E, F) IMPLIES (P |> F) sat_choice1 : LEMMA (P \/ Q) |> E IFF P |> E AND Q |> E sat_choice2 : LEMMA Choice(SP) |> E IFF Stop[T] |> E AND (FORALL (P : (SP)) : P |> E ) sat_free_par1 : LEMMA (P // Q) |> E IMPLIES P |> E sat_free_par2 : LEMMA (P // Q) |> E IMPLIES Q |> E END satisfaction $$$satisfaction.prf (|satisfaction| (|sat_idempotent| "" (SKOLEM!) (("" (GRIND) NIL NIL)) NIL) (|sat_transitive1| "" (SKOSIMP) (("" (GRIND) NIL NIL)) NIL) (|sat_transitive2| "" (SKOSIMP) (("" (GRIND) NIL NIL)) NIL) (|sat_choice1| "" (SKOLEM!) (("" (GRIND) NIL NIL)) NIL) (|sat_choice2| "" (GRIND :EXCLUDE ("prefix_closed") :IF-MATCH NIL) (("1" (INST?) (("1" (GROUND) (("1" (INST + "P!1") NIL NIL)) NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST - "P!1" "x!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL) (|sat_free_par1| "" (SKOSIMP) (("" (USE "interleaves_subset1[T]") (("" (REWRITE "|>" :DIR RL) (("" (FORWARD-CHAIN "sat_transitive1") NIL NIL)) NIL)) NIL)) NIL) (|sat_free_par2| "" (SKOSIMP) (("" (USE "interleaves_subset2[T]") (("" (REWRITE "|>" :DIR RL) (("" (FORWARD-CHAIN "sat_transitive1") NIL NIL)) NIL)) NIL)) NIL)) $$$multiprod.pvs % % products of a non-empty family of traces % multiprod [ U : NONEMPTY_TYPE, T : TYPE ] : THEORY BEGIN IMPORTING traces, parametric_sets t, t1, t2 : VAR [U -> trace[T]] u, v : VAR trace[T] i, j, k : VAR U A, B, C : VAR set[T] S : VAR [U -> set[T]] %---------------------------------------------------------------- % prod(A)(t, u) : "u is a product of the traces {t(i) | i in U} % with synchronisations on A %---------------------------------------------------------------- prod(A)(t, u) : RECURSIVE bool = CASES u OF null: (FORALL i : t(i) = null), cons(x, y): IF A(x) THEN (FORALL i : cons?(t(i)) AND car(t(i)) = x) AND prod(A)(lambda j : cdr(t(j)), y) ELSE EXISTS i : cons?(t(i)) AND car(t(i)) = x AND prod(A)(t with [(i) := cdr(t(i))], y) ENDIF ENDCASES MEASURE length(u) proj_multiprod : LEMMA prod(A)(t, u) IMPLIES FORALL i : proj(t(i), A) = proj(u, A) prefix_multiprod : LEMMA prod(A)(t, u) AND prefix(v, u) IMPLIES EXISTS t1 : prod(A)(t1, v) AND FORALL i : prefix(t1(i), t(i)) multiprod_fullset : LEMMA prod(fullset)(t, u) IFF (FORALL i : t(i) = u) free_multiprod : LEMMA prod(emptyset)((lambda i : null::list[T]) WITH [(j) := u], u) sigma_multiprod : LEMMA prod(A)(t, u) IMPLIES sigma(u) = union! i : sigma(t(i)) sigma_multiprod_inter : LEMMA prod(A)(t, u) IMPLIES intersection(sigma(t(i)), A) = intersection(sigma(u), A) %---------------------------------------------------------------- % Interleaving when the traces have mutually disjoint alphabets %---------------------------------------------------------------- sub_alphabet(t, S) : bool = FORALL i : subset?(sigma(t(i)), S(i)) disj_alphabet(S) : bool = FORALL i, j : i /= j IMPLIES disjoint?(S(i), S(j)) inter_disjoint : LEMMA disj_alphabet(S) AND sub_alphabet(t, S) AND prod(emptyset)(t, u) IMPLIES FORALL i : t(i) = proj(u, S(i)) %--------------------------------------- % Projections/restrictions %----------------------------------------- inter_proj : LEMMA prod(emptyset)(t, u) IMPLIES prod(emptyset)(lambda i : proj(t(i), B), proj(u, B)) null_proj_multiprod : LEMMA prod(A)(t, u) IMPLIES (proj(u, B) = null IFF FORALL i : proj(t(i), B) = null) null_proj_multiprod2 : LEMMA prod(A)(t, u) AND subset?(B, A) AND proj(t(i), B) = null IMPLIES proj(u, B) = null null_inter_proj : LEMMA prod(emptyset)(t, u) IMPLIES (proj(u, B) = null IFF FORALL i : proj(t(i), B) = null) END multiprod $$$multiprod.prf (|multiprod| (|prod_TCC1| "" (SKOSIMP*) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|prod_TCC2| "" (TERMINATION-TCC) NIL NIL) (|prod_TCC3| "" (TERMINATION-TCC) NIL NIL) (|proj_multiprod| "" (AUTO-REWRITE-DEFS) (("" (SKOLEM + ("A!1" _ _)) (("" (INDUCT "u") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (CASE "A!1(cons1_var!1)") (("1" (REDUCE) NIL NIL) ("2" (ASSERT) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (INST?) (("2" (GROUND) (("2" (INST - "i!1") (("2" (CASE "i!1 = i!2") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_multiprod| "" (AUTO-REWRITE "prefix_null[T]" "null_prefix[T]") (("" (SKOLEM + ("A!1" _ _ _)) (("" (INDUCT "u") (("1" (AUTO-REWRITE "prod") (("1" (SKOSIMP) (("1" (INST + "lambda i : null") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (REWRITE "prefix_equiv") (("2" (GROUND) (("1" (AUTO-REWRITE "prod") (("1" (INST + "lambda i : null") (("1" (DELETE -2 -3) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "prod") (("2" (CASE "A!1(cons1_var!1)") (("1" (ASSERT) (("1" (GROUND) (("1" (INST - "LAMBDA (i: U): cdr(t!1(i))" "cdr(v!1)") (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST + "lambda i : cons(cons1_var!1, t1!1(i))") (("1" (GROUND) (("1" (LEMMA "eta[U, trace[T]]") (("1" (INST - "t1!1") (("1" (REPLACE -1) (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST?) (("2" (INST?) (("2" (REWRITE "prefix_equiv" +) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (INST - "t!1 WITH [(i!1) := cdr(t!1(i!1))]" "cdr(v!1)") (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "t1!1 with [(i!1) := cons(cons1_var!1, t1!1(i!1))]") (("2" (GROUND) (("1" (INST + "i!1") (("1" (ASSERT) (("1" (CASE-REPLACE "t1!1 WITH [(i!1):= cons(cons1_var!1, t1!1(i!1)), (i!1) := t1!1(i!1)] = t1!1") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (CASE "x!1 = i!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST - "i!2") (("2" (CASE "i!1 = i!2") (("1" (ASSERT) (("1" (REWRITE "prefix_equiv" +) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|multiprod_fullset| "" (AUTO-REWRITE "fullset" "prod") (("" (INDUCT "u") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (GROUND) (("1" (INST? -3) (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST?) (("1" (INST?) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -2 2) (("2" (REDUCE) NIL NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST?) (("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (INST? -2) (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST?) (("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|free_multiprod| "" (INDUCT-AND-SIMPLIFY "u") NIL NIL) (|sigma_multiprod| "" (INDUCT-AND-SIMPLIFY "u") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (REDUCE) NIL NIL)) NIL) ("2" (REPLACE*) (("2" (DELETE -1 -4) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (REDUCE) (("1" (INST + "epsilon! i : true") (("1" (REDUCE) NIL NIL)) NIL)) NIL) ("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (DELETE -1 -4) (("3" (APPLY-EXTENSIONALITY :HIDE? T) (("3" (IFF) (("3" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOLEM!) (("2" (INST + "i!2") (("2" (SMASH) NIL NIL)) NIL)) NIL) ("3" (SKOLEM!) (("3" (INST?) (("3" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_multiprod_inter| "" (SKOSIMP) (("" (FORWARD-CHAIN "proj_multiprod") (("" (INST?) (("" (REWRITE "sigma_proj" :DIR RL) (("" (REWRITE "sigma_proj" :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|inter_disjoint| "" (AUTO-REWRITE "prod" "emptyset" "proj" "filter") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (SKOLEM + ("A!1" _ _)) (("" (INDUCT "u") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL) ("2" (AUTO-REWRITE "sub_alphabet" "disj_alphabet" "sigma" "list2set") (("2" (SKOSIMP) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST - "t!1 WITH [(i!1) := cdr(t!1(i!1))]") (("2" (GROUND) (("1" (INST? -3) (("1" (INST -3 "cons1_var!1") (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST?) (("1" (CASE "i!1 = i!2") (("1" (ASSERT) (("1" (APPLY-EXTENSIONALITY) NIL NIL)) NIL) ("2" (INST - "i!1" "i!2") (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -5 2) (("2" (SKOLEM!) (("2" (INST - "i!2") (("2" (CASE "i!1 = i!2") (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|inter_proj| "" (AUTO-REWRITE "prod" "emptyset" "proj" "filter") (("" (SKOLEM + ("A!1" _ _)) (("" (INDUCT "u") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST? :WHERE -4) (("2" (ASSERT) (("2" (LIFT-IF) (("2" (GROUND) (("1" (INST?) (("1" (ASSERT) (("1" (CASE-REPLACE "(LAMBDA i : filter(t!1(i), A!1)) WITH [(i!1) := filter(cdr(t!1(i!1)), A!1)] = (LAMBDA i : filter(t!1 WITH [(i!1) := cdr(t!1(i!1))](i), A!1))") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (CASE "x!1 = i!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE-REPLACE "(LAMBDA i : filter(t!1(i), A!1)) = LAMBDA i : filter(t!1 WITH [(i!1) := cdr(t!1(i!1))](i), A!1)") (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (CASE "x!1 = i!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_multiprod| "" (SKOSIMP) (("" (AUTO-REWRITE "null_proj_equiv[T]") (("" (ASSERT) (("" (FORWARD-CHAIN "sigma_multiprod") (("" (REPLACE*) (("" (DELETE -) (("" (EXPAND "union") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_multiprod2| "" (SKOSIMP) (("" (AUTO-REWRITE "null_proj_equiv[T]") (("" (ASSERT) (("" (USE "sigma_multiprod_inter") (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) (("" (CASE "intersection(sigma(t!1(i!1)), A!1)(x!1)") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_inter_proj| "" (SKOSIMP) (("" (USE "null_proj_multiprod") (("" (ASSERT) NIL NIL)) NIL)) NIL)) $$$multipar.pvs % % Parallel composition of a non-empty family of processes % % T : event type % U : parameter type % multipar [ U : NONEMPTY_TYPE, T : TYPE ] : THEORY BEGIN IMPORTING processes, multiprod, process_rules P : VAR [U -> process[T]] A : VAR set[T] S : VAR [U -> set[T]] u : VAR trace[T] i, j : VAR U %-------------------------------------------------- % Parallel composition with synchronisation on A %-------------------------------------------------- Par(A)(P) : process[T] = { u | EXISTS (t : [i:U -> (P(i))]) : prod(A)(t, u) } %---------------- % Interleaving %---------------- Interleave(P) : process[T] = Par(emptyset)(P) %-------------- % Properties %-------------- sigma_par2 : LEMMA subset?(sigma(Par(A)(P)), union! i : sigma(P(i))) sigma_free_par2 : LEMMA sigma(Interleave(P)) = union! i : sigma(P(i)) par_full2 : LEMMA Par(fullset)(P) = intersection! i : P(i) interleave_subset3 : LEMMA subset?(P(i), Interleave(P)) %-------------------------------------------------------- % Interleaving when processes have disjoint interfaces %-------------------------------------------------------- interleave_disjoint : LEMMA (FORALL i : subset?(sigma(P(i)), S(i))) AND (FORALL i, j : i /= j IMPLIES disjoint?(S(i), S(j))) IMPLIES subset?(Interleave(P), { u | FORALL i : P(i)(proj(u, S(i))) }) END multipar $$$multipar.prf (multipar (U_TCC1 0 (U_TCC1-1 nil 3238606746 nil nil nil nil nil nil nil shostak)) (Par_TCC1 0 (Par_TCC1-1 nil 3238606746 nil ("" (skolem!) (("" (ground) (("1" (inst + "lambda i : null") (("1" (expand "prod") (("1" (propax) nil))) ("2" (reduce) nil))) ("2" (auto-rewrite "prefix_closed") (("2" (assert) (("2" (skosimp*) (("2" (forward-chain "prefix_multiprod") (("2" (skosimp) (("2" (inst + "t1!2") (("2" (skolem!) (("2" (inst?) (("2" (typepred "P!1(x1!1)") (("2" (assert) (("2" (inst?) (("2" (assert) nil)))))))))))))))))))))))))) nil) proved-complete ((NOT const-decl "[bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (prefix_multiprod formula-decl nil multiprod nil) (process type-eq-decl nil processes nil) (prefix_closed const-decl "bool" processes nil) (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (trace type-eq-decl nil traces nil) (list type-decl nil list_adt nil) (T formal-type-decl nil multipar nil) (U formal-nonempty-type-decl nil multipar nil) (prod def-decl "bool" multiprod nil)) nil nil nil nil)) (sigma_par2 0 (sigma_par2-1 nil 3238606746 nil ("" (expand "Par") (("" (expand "sigma") (("" (grind :defs nil :theories ("sets[T]" "sets[trace[T]]") :if-match nil) (("" (forward-chain "sigma_multiprod") (("" (replace -1) (("" (expand "union") (("" (skolem!) (("" (inst + "i!1") (("" (inst?) nil)))))))))))))))) nil) proved-complete ((Par const-decl "process[T]" multipar nil) (T formal-type-decl nil multipar nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (prod def-decl "bool" multiprod nil) (set type-eq-decl nil sets nil) (process type-eq-decl nil processes nil) (prefix_closed const-decl "bool" processes nil) (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (setof type-eq-decl nil defined_types nil) (trace type-eq-decl nil traces nil) (list type-decl nil list_adt nil) (U formal-nonempty-type-decl nil multipar nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (union const-decl "set[T]" parametric_sets nil) (sigma_multiprod formula-decl nil multiprod nil) (sigma const-decl "setof[T]" processes nil)) nil nil nil nil)) (sigma_free_par2 0 (sigma_free_par2-1 nil 3238606746 3238607542 ("" (expand "Interleave") (("" (skolem!) (("" (apply-extensionality :hide? t) (("" (iff) (("" (ground) (("1" (use "sigma_par2") (("1" (expand* "subset?" "member") (("1" (forward-chain -1) nil nil)) nil)) nil) ("2" (expand* "union" "Par" "sigma") (("2" (skosimp* :preds? t) (("2" (inst?) (("2" (inst + "lambda i : IF i = i!1 THEN t!1 ELSE null[T] ENDIF") (("1" (lemma "free_multiprod" ("j" "i!1" "u" "t!1")) (("1" (case-replace "(LAMBDA i: IF i = i!1 THEN t!1 ELSE null[T] ENDIF) = ((LAMBDA i: null[T]::list[T]) WITH [(i!1) := t!1])") (("1" (delete -1 -3 2) (("1" (apply-extensionality :hide? t) (("1" (smash) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((prod def-decl "bool" multiprod nil) (P!1 skolem-const-decl "[U -> process[T]]" multipar nil) (i!1 skolem-const-decl "U" multipar nil) (t!1 skolem-const-decl "(P!1(i!1))" multipar nil) (free_multiprod formula-decl nil multiprod nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (sigma_par2 formula-decl nil multipar nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (list type-decl nil list_adt nil) (trace type-eq-decl nil traces nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (prefix_closed const-decl "bool" processes nil) (process type-eq-decl nil processes nil) (sigma const-decl "setof[T]" processes nil) (set type-eq-decl nil sets nil) (U formal-nonempty-type-decl nil multipar nil) (Par const-decl "process[T]" multipar nil) (emptyset const-decl "set" sets nil) (union const-decl "set[T]" parametric_sets nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil multipar nil) (Interleave const-decl "process[T]" multipar nil)) 485161 29960 t nil)) (par_full2 0 (par_full2-1 nil 3238606746 nil ("" (auto-rewrite "Par" "intersection") (("" (skolem!) (("" (apply-extensionality :hide? t) (("" (iff) (("" (ground) (("1" (skolem!) (("1" (rewrite "multiprod_fullset") (("1" (skolem!) (("1" (inst?) (("1" (assert) nil))))))))) ("2" (inst + "lambda i : x!1") (("2" (rewrite "multiprod_fullset") nil)))))))))))) nil) proved-complete ((T formal-type-decl nil multipar nil) (list type-decl nil list_adt nil) (trace type-eq-decl nil traces nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (intersection const-decl "set[T]" parametric_sets nil) (fullset const-decl "set" sets nil) (Par const-decl "process[T]" multipar nil) (process type-eq-decl nil processes nil) (prefix_closed const-decl "bool" processes nil) (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (U formal-nonempty-type-decl nil multipar nil) (set type-eq-decl nil sets nil) (multiprod_fullset formula-decl nil multiprod nil)) nil nil nil nil)) (interleave_subset3 0 (interleave_subset3-1 nil 3238606746 3238607582 ("" (grind :exclude ("prod")) (("" (use "free_multiprod[U, T]") (("" (inst + "lambda i : IF i = i!1 THEN x!1 ELSE null[T] ENDIF") (("1" (case-replace "(LAMBDA i: IF i = i!1 THEN x!1 ELSE null[T] ENDIF) = (LAMBDA i: null::list[T]) WITH [(i!1) := x!1]") (("1" (delete -1 2) (("1" (apply-extensionality :hide? t) (("1" (reduce) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) proved ((T formal-type-decl nil multipar nil) (U formal-nonempty-type-decl nil multipar nil) (free_multiprod formula-decl nil multiprod nil) (list type-decl nil list_adt nil) (trace type-eq-decl nil traces nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (prefix_closed const-decl "bool" processes nil) (process type-eq-decl nil processes nil) (P!1 skolem-const-decl "[U -> process[T]]" multipar nil) (i!1 skolem-const-decl "U" multipar nil) (x!1 skolem-const-decl "trace[T]" multipar nil) (subset? const-decl "bool" sets nil) (Par const-decl "process[T]" multipar nil) (member const-decl "bool" sets nil) (Interleave const-decl "process[T]" multipar nil)) 29733 8080 t nil)) (interleave_disjoint 0 (interleave_disjoint-1 nil 3238606746 nil ("" (grind :exclude ("proj" "sigma" "disjoint?") :rewrites ("disj_alphabet[U, T]" "sub_alphabet[U, T]") :if-match nil) (("" (use "inter_disjoint[U, T]" ("t" "t!1")) (("" (ground) (("1" (inst?) (("1" (assert) nil))) ("2" (rewrite "sub_alphabet") (("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (delete -2 -3 1 3) (("2" (use "sigma_subset" ("P" "P!1(i!2)")) (("2" (reduce) nil)))))))))))))))))) nil) proved-complete ((member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (/= const-decl "boolean" notequal nil) (Interleave const-decl "process[T]" multipar nil) (Par const-decl "process[T]" multipar nil) (disj_alphabet const-decl "bool" multiprod nil) (sub_alphabet const-decl "bool" multiprod nil) (sigma_subset formula-decl nil process_rules nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil multipar nil) (U formal-nonempty-type-decl nil multipar nil) (process type-eq-decl nil processes nil) (prefix_closed const-decl "bool" processes nil) (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (trace type-eq-decl nil traces nil) (list type-decl nil list_adt nil) (inter_disjoint formula-decl nil multiprod nil)) nil nil nil nil))) $$$parametric_sets.pvs % % union and intersection of a family of sets % % T : element type % U : index type % parametric_sets [ U, T : TYPE ] : THEORY BEGIN A : VAR [U -> set[T]] i : VAR U x : VAR T S : VAR set[T] %--------------- % Definitions %--------------- union(A) : set[T] = { x | EXISTS i : A(i)(x) } intersection(A) : set[T] = { x | FORALL i : A(i)(x) } %-------------- % Properties %-------------- union_is_bound : LEMMA subset?(A(i), union(A)) union_is_lub : LEMMA (FORALL i : subset?(A(i), S)) IMPLIES subset?(union(A), S) inter_is_bound : LEMMA subset?(intersection(A), A(i)) inter_is_glb : LEMMA (FORALL i : subset?(S, A(i))) IMPLIES subset?(S, intersection(A)) END parametric_sets $$$parametric_sets.prf (|parametric_sets| (|union_is_bound| "" (GRIND) NIL) (|union_is_lub| "" (GRIND) NIL) (|inter_is_bound| "" (GRIND) NIL) (|inter_is_glb| "" (GRIND) NIL)) $$$process_rules.pvs process_rules [ T : TYPE ] : THEORY BEGIN IMPORTING processes, parametric_sets P, P1, P2, P3, P4 : VAR process[T] SP, SP1, SP2 : VAR set[process[T]] a, b, c : VAR T A, B, C : VAR set[T] t : VAR trace[T] %------------------ % Prefix closure %------------------ process_add : LEMMA P(add(t, a)) IMPLIES P(t) %------------------- % Rules for sigma %------------------- sigma_stop : LEMMA sigma(Stop[T]) = emptyset sigma_choice : LEMMA sigma(P1 \/ P2) = union(sigma(P1), sigma(P2)) sigma_choice2 : LEMMA sigma(Choice(SP)) = union! (P : (SP)) : sigma(P) sigma_pref : LEMMA sigma(a >> P) = add(a, sigma(P)) sigma_par : LEMMA subset?(sigma(Par(A)(P1, P2)), union(sigma(P1), sigma(P2))) sigma_free_par : LEMMA sigma(P1 // P2) = union(sigma(P1), sigma(P2)) sigma_empty : LEMMA sigma(P) = emptyset IFF P = Stop[T] sigma_union : LEMMA sigma(P) = union! (t : (P)) : sigma(t) sigma_subset : LEMMA FORALL (t : (P)) : subset?(sigma(t), sigma(P)) %-------------------------------- % Stop is the smallest process %-------------------------------- stop_subset : LEMMA subset?(Stop[T], P) stop_smallest : LEMMA subset?(P, Stop[T]) IFF P = Stop[T] %---------------------------- % Rules for bounded choice %---------------------------- choice_commutes : LEMMA (P1 \/ P2) = (P2 \/ P1) choice_assoc : LEMMA (P1 \/ (P2 \/ P3)) = ((P1 \/ P2) \/ P3) choice_idempotent : LEMMA (P \/ P) = P choice_subset1 : LEMMA subset?(P1, P1 \/ P2) choice_subset2 : LEMMA subset?(P2, P1 \/ P2) choice_stop1 : LEMMA (P \/ Stop[T]) = P choice_stop2 : LEMMA (Stop[T] \/ P) = P choice_stop3 : LEMMA (P1 \/ P2) = Stop[T] IFF P1 = Stop[T] AND P2 = Stop[T] %------------------------------ % Rules for unbounded choice %------------------------------ choice_empty : LEMMA Choice(emptyset[process[T]]) = Stop[T] choice_add : LEMMA Choice(add(P, SP)) = (P \/ Choice(SP)) choice_singleton : LEMMA Choice(singleton(P)) = P choice_union : LEMMA Choice(union(SP1, SP2)) = (Choice(SP1) \/ Choice(SP2)) choice_member : LEMMA FORALL (P : (SP)) : subset?(P, Choice(SP)) %---------------------------------- % Rules for parallel composition %---------------------------------- par_commutes : LEMMA Par(A)(P1, P2) = Par(A)(P2, P1) par_assoc : LEMMA Par(A)(P1, Par(A)(P2, P3)) = Par(A)(Par(A)(P1, P2), P3) par_stop : LEMMA Par(A)(P, Stop) = { t | P(t) AND proj(t, A) = null } par_full : LEMMA Par(fullset)(P1, P2) = intersection(P1, P2) %--------------------------- % Rules for interleaving %--------------------------- interleaves_commutes : LEMMA P1 // P2 = P2 // P1 interleaves_assoc : LEMMA (P1 // P2) // P3 = P1 // (P2 // P3) interleaves_subset1 : LEMMA subset?(P1, P1 // P2) interleaves_subset2 : LEMMA subset?(P2, P1 // P2) interleaves_stop1 : LEMMA P // Stop[T] = P interleaves_stop2 : LEMMA Stop[T] // P = P END process_rules $$$process_rules.prf (|process_rules| (|process_add| "" (AUTO-REWRITE "prefix_closed[T]" "prefix[T]" "add[T]") (("" (SKOSIMP :PREDS? T) (("" (ASSERT) (("" (INST - "t!1" "add(t!1, a!1)") (("" (ASSERT) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_stop| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL) (|sigma_choice| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :DEFS NIL :REWRITES ("sigma" "Choice" "\\/") :THEORIES ("sets[T]" "sets[trace[T]]")) NIL NIL)) NIL)) NIL) (|sigma_choice2| "" (AUTO-REWRITE "sigma" "Choice" "union" "emptyset" "list2set") (("" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (SKOLEM-TYPEPRED) (("1" (ASSERT) (("1" (GROUND) (("1" (SKOLEM!) (("1" (INST + "P!1") (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST?) (("2" (FLATTEN) (("2" (INST + "i!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_pref| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :IF-MATCH NIL) (("1" (INST?) NIL NIL) ("2" (INST + "(: a!1 :)") (("1" (ASSERT) NIL NIL) ("2" (INST?) NIL NIL)) NIL) ("3" (INST + "cons(a!1, t!1)") (("1" (ASSERT) NIL NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_par| "" (EXPAND "Par") (("" (EXPAND "sigma") (("" (GRIND :DEFS NIL :THEORIES ("sets[T]" "sets[trace[T]]") :IF-MATCH NIL) (("" (FORWARD-CHAIN "sigma_prod") (("" (REPLACE*) (("" (ASSERT) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_free_par| "" (SKOLEM!) (("" (EXPAND "//") (("" (USE "sigma_par") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (IFF) (("" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE -2) (("2" (GRIND :DEFS NIL :REWRITES ("Par" "sigma" "free_prod_left[T]" "free_prod_right[T]") :IF-MATCH NIL) (("1" (INST?) (("1" (INST + "t!1" "null") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INST?) (("2" (INST + "null" "t!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_empty| "" (SKOLEM!) (("" (GROUND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (EXPAND "Stop") (("1" (REWRITE "emptyset_is_empty?" :DIR RL) (("1" (GRIND) (("1" (INST - "car(x!1)") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (REWRITE "sigma_stop") NIL NIL)) NIL)) NIL)) NIL) (|sigma_union| "" (EXPAND "sigma" 1 1) (("" (EXPAND "union") (("" (PROPAX) NIL NIL)) NIL)) NIL) (|sigma_subset| "" (SKOLEM!) (("" (REWRITE "sigma_union") (("" (USE "union_is_bound" ("A" "lambda (t: (P!1)): sigma(t)")) NIL NIL)) NIL)) NIL) (|stop_subset| "" (GRIND :EXCLUDE "prefix_closed") NIL NIL) (|stop_smallest| "" (GRIND :EXCLUDE "prefix_closed" :IF-MATCH NIL) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) (("" (IFF) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|choice_commutes| "" (GRIND :EXCLUDE "prefix_closed") (("" (REWRITE "union_commutative") NIL NIL)) NIL) (|choice_assoc| "" (AUTO-REWRITE "\\/" "Choice") (("" (SKOLEM!) (("" (ASSERT) (("" (REWRITE "union_associative") NIL NIL)) NIL)) NIL)) NIL) (|choice_idempotent| "" (AUTO-REWRITE "\\/" "Choice") (("" (SKOLEM!) (("" (ASSERT) (("" (REWRITE "union_idempotent") NIL NIL)) NIL)) NIL)) NIL) (|choice_subset1| "" (AUTO-REWRITE "\\/" "Choice") (("" (SKOLEM!) (("" (ASSERT) (("" (REWRITE "union_subset1") NIL NIL)) NIL)) NIL)) NIL) (|choice_subset2| "" (SKOLEM!) (("" (REWRITE "choice_commutes") (("" (REWRITE "choice_subset1") NIL NIL)) NIL)) NIL) (|choice_stop1| "" (AUTO-REWRITE "\\/" "Choice") (("" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|choice_stop2| "" (SKOLEM!) (("" (REWRITE "choice_commutes") (("" (REWRITE "choice_stop1") NIL NIL)) NIL)) NIL) (|choice_stop3| "" (AUTO-REWRITE "choice_idempotent" "stop_smallest") (("" (SKOLEM!) (("" (GROUND) (("1" (USE "choice_subset1") (("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (USE "choice_subset2") (("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|choice_empty| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL) (|choice_add| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE "prefix_closed" :IF-MATCH NIL) (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL) ("3" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|choice_singleton| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE "prefix_closed") NIL NIL)) NIL)) NIL) (|choice_union| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE "prefix_closed") NIL NIL)) NIL)) NIL) (|choice_member| "" (GRIND :EXCLUDE "prefix_closed") NIL NIL) (|par_commutes| "" (SKOLEM!) (("" (EXPAND "Par") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (SKOSIMP) (("1" (REWRITE "prod_commutes") (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (REWRITE "prod_commutes") (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|par_assoc| "" (SKOLEM!) (("" (EXPAND "Par") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE :IF-MATCH NIL) (("1" (USE "prod_assoc2" ("u" "t2!1")) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST + "u1!1" "t2!2") (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "prod_assoc1" ("u" "t1!1")) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "t1!2" "u1!1") (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|par_stop| "" (AUTO-REWRITE "Par" "Stop") (("" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (PROP) (("1" (SKOLEM-TYPEPRED) (("1" (ASSERT) (("1" (REPLACE*) (("1" (FORWARD-CHAIN "prod_null1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM-TYPEPRED) (("2" (ASSERT) (("2" (REPLACE*) (("2" (FORWARD-CHAIN "proj_prod2") (("2" (AUTO-REWRITE "proj") (("2" (AUTO-REWRITE "proj" "filter") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (FORWARD-CHAIN "prod_null3") (("3" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|par_full| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE ("prod") :REWRITES ("prod_fullset[T]")) NIL NIL)) NIL)) NIL) (|interleaves_commutes| "" (EXPAND "//") (("" (SKOLEM!) (("" (REWRITE "par_commutes") NIL NIL)) NIL)) NIL) (|interleaves_assoc| "" (SKOLEM!) (("" (EXPAND "//") (("" (REWRITE "par_assoc") NIL NIL)) NIL)) NIL) (|interleaves_subset1| "" (GRIND :EXCLUDE ("prefix_closed" "prod") :IF-MATCH NIL) (("" (INST + "x!1" "null") (("" (REWRITE "free_prod_left") NIL NIL)) NIL)) NIL) (|interleaves_subset2| "" (GRIND :EXCLUDE ("prefix_closed" "prod") :IF-MATCH NIL) (("" (INST + "null" "x!1") (("" (REWRITE "free_prod_right") NIL NIL)) NIL)) NIL) (|interleaves_stop1| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE ("prod" "prefix_closed") :IF-MATCH NIL) (("1" (USE "prod_null1" ("t1" "t1!1" "t" "x!1")) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "x!1" "null") (("2" (REWRITE "free_prod_left") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|interleaves_stop2| "" (SKOLEM!) (("" (REWRITE "interleaves_commutes") (("" (REWRITE "interleaves_stop1") NIL NIL)) NIL)) NIL)) $$$parametric_choice.pvs % % Unbounded choice of a family {P(i) | i in U} % % T = event type % U = parameter type % parametric_choice [ U, T : TYPE] : THEORY BEGIN IMPORTING processes, process_rules P : VAR [U -> process[T]] Q : VAR process[T] t : VAR trace[T] i : VAR U %-------------- % Definition %-------------- Choice(P) : process[T] = { t | null?(t) OR EXISTS i : P(i)(t) } %----------------- % Various rules %----------------- choice_equiv : LEMMA Choice(P) = Choice({ Q | EXISTS i : Q = P(i)}) choice_nonempty_param : LEMMA (EXISTS i : true) IMPLIES Choice(P) = union! i : P(i) choice_empty_param : LEMMA (FORALL i : false) IMPLIES Choice(P) = Stop sigma_choice3 : LEMMA sigma(Choice(P)) = union! i : sigma(P(i)) choice_member2 : LEMMA subset?(P(i), Choice(P)) END parametric_choice $$$parametric_choice.prf (|parametric_choice| (|Choice_TCC1| "" (GRIND :IF-MATCH NIL :EXCLUDE ("prefix")) (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (INST?) (("2" (TYPEPRED "P!1(i!1)") (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|choice_equiv| "" (SKOLEM!) (("" (EXPAND "Choice") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (DELETE 1) (("1" (REDUCE) NIL NIL)) NIL) ("2" (DELETE 1) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|choice_nonempty_param| "" (SKOSIMP*) (("" (TYPEPRED "P!1(i!1)") (("" (DELETE -2) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|choice_empty_param| "" (SKOSIMP) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|sigma_choice3| "" (SKOLEM!) (("" (REWRITE "choice_equiv") (("" (REWRITE "sigma_choice2") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "union") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|choice_member2| "" (SKOLEM!) (("" (REWRITE "choice_nonempty_param") (("1" (USE "union_is_bound" ("A" "lambda i : P!1(i)")) NIL NIL) ("2" (INST + "i!1") NIL NIL)) NIL)) NIL)) $$$more_list_props.pvs % % Extension of the pre-defined operations on lists % and extra properties % more_list_props [ T : TYPE] : THEORY BEGIN l, l1, l2 : VAR list[T] cons_l, cons_l1, cons_l2 : VAR (cons?[T]) a, b, c : VAR T P : VAR [list[T] -> bool] %---------------------------------------- % add(l, a) : append a at the end of l %---------------------------------------- add(l, a) : (cons?[T]) = append(l, cons(a, null)) add_null : LEMMA add(null, a) = (: a :) add_cons : LEMMA add(cons(a, l), b) = cons(a, add(l, b)) %------------------------ % Properties of length %------------------------ length_append : LEMMA length(append(l1, l2)) = length(l1) + length(l2) length_add : LEMMA length(add(l, a)) = length(l) + 1 length_reverse : LEMMA length(reverse(l)) = length(l) length_cdr : LEMMA length(cdr(cons_l)) = length(cons_l) - 1 length_zero : LEMMA length(l) = 0 IFF l = null length_non_zero : LEMMA length(l) > 0 IFF cons?(l) %----------------------- % Induction using add %----------------------- cons_to_add : LEMMA FORALL cons_l : EXISTS a, l : cons_l = add(l, a) add_induction : PROPOSITION P(null) AND (FORALL l, a : P(l) IMPLIES P(add(l, a))) IMPLIES (FORALL l : P(l)) END more_list_props $$$more_list_props.prf (|more_list_props| (|add_TCC1| "" (SKOLEM!) (("" (EXPAND "append") (("" (LIFT-IF) (("" (ASSERT) NIL))))))) (|add_null| "" (GRIND) NIL) (|add_cons| "" (GRIND) NIL) (|length_append| "" (SKOLEM + (_ "l2!1")) (("" (INDUCT-AND-SIMPLIFY "l1") NIL))) (|length_add| "" (AUTO-REWRITE "length" "add" "length_append") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|length_reverse| "" (INDUCT-AND-SIMPLIFY "l" :REWRITES ("length_append")) NIL) (|length_cdr| "" (AUTO-REWRITE "length") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|length_zero| "" (GRIND) NIL) (|length_non_zero| "" (GRIND) NIL) (|cons_to_add| "" (AUTO-REWRITE "add_null" "add_cons") (("" (INDUCT "cons_l") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (SKOSIMP) (("3" (GROUND) (("1" (SKOLEM!) (("1" (INST + "a!1" "cons(cons1_var!1, l!1)") (("1" (ASSERT) NIL))))) ("2" (INST + "cons1_var!1" "null") (("2" (ASSERT) (("2" (ASSERT) NIL))))))))))))) (|add_induction| "" (SKOSIMP) (("" (CASE "FORALL (n : nat), l : length(l) = n IMPLIES P!1(l)") (("1" (SKOLEM!) (("1" (INST - "length(l!1)" "l!1") (("1" (ASSERT) NIL))))) ("2" (DELETE 2) (("2" (AUTO-REWRITE "length_zero" "length_add") (("2" (INDUCT "n") (("1" (SKOSIMP) (("1" (ASSERT) NIL))) ("2" (SKOSIMP*) (("2" (USE "length_non_zero" ("l" "l!1")) (("2" (ASSERT) (("2" (USE "cons_to_add" ("cons_l" "l!1")) (("2" (SKOLEM!) (("2" (REPLACE -1) (("2" (INST - "l!2") (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))))))))))) $$$traces.pvs % % Traces over events of type T % defines operators specific to PVS % % Functions defined in the prelude: % length(t) : nat % member(a, t) : bool % nth(t, i) : T (i : below[length(t)]) % append(t1, t2) : trace % reverse(t) : trace % cons(a, t) : trace % null : trace % car(t) : T % cdr(t) : trace % % filter(t, S) : trace % filter(S)(t) : trace % list2set(t) : set[T] % % Defined in more_list_props % add(t, a) : trace % % Defined in trace % prefix(t1, t2) : bool % proj(t, S) : trace % prod(S)(t1, t2, t) : bool % sigma(t) : set[T] % traces [ T : TYPE ] : THEORY BEGIN IMPORTING more_list_props trace : TYPE = list[T] a, b, c : VAR T A, B, C : VAR setof[T] t, t1, t2, t3 : VAR trace u, u1, u2 : VAR trace %----------- % Prefix %----------- prefix(t1, t2) : bool = EXISTS t : t2 = append(t1, t) prefix_equiv : LEMMA prefix(t1, t2) IFF null?(t1) OR (cons?(t1) AND cons?(t2) AND car(t1) = car(t2) AND prefix(cdr(t1), cdr(t2))) null_prefix : LEMMA prefix(null, t) prefix_null : LEMMA prefix(t, null) IFF t = null cons_prefix : LEMMA prefix(cons(a, t1), cons(b, t2)) IFF a = b AND prefix(t1, t2) prefix_append1 : LEMMA prefix(t1, t2) IMPLIES prefix(t1, append(t2, t3)) prefix_append2 : LEMMA prefix(t1, t2) IMPLIES prefix(append(t, t1), append(t, t2)) prefix_add1 : LEMMA prefix(t, add(t, a)) prefix_add2 : LEMMA prefix(t1, t2) IMPLIES prefix(t1, add(t2, a)) length_prefix : LEMMA prefix(t1, t2) IMPLIES length(t1) <= length(t2) prefix_reflexive : LEMMA prefix(t, t) prefix_transitive : LEMMA prefix(t1, t2) AND prefix(t2, t3) IMPLIES prefix(t1, t3) prefix_antisymmetric : LEMMA prefix(t1, t2) AND prefix(t2, t1) IMPLIES t1 = t2 %-------------- % Projection %-------------- proj : [trace, set[T] -> trace] = filter proj_null : LEMMA proj(null, A) = null proj_cons : LEMMA proj(cons(a, t), A) = IF A(a) THEN cons(a, proj(t, A)) ELSE proj(t, A) ENDIF proj_append : LEMMA proj(append(t1, t2), A) = append(proj(t1, A), proj(t2, A)) proj_add : LEMMA proj(add(t, a), A) = IF A(a) THEN add(proj(t, A), a) ELSE proj(t, A) ENDIF proj_prefix : LEMMA prefix(t1, t2) IMPLIES prefix(proj(t1, A), proj(t2, A)) proj_reverse : LEMMA proj(reverse(t), A) = reverse(proj(t, A)) prefix_of_proj : LEMMA prefix(t1, proj(t, A)) IMPLIES EXISTS t2 : prefix(t2, t) AND t1 = proj(t2, A) prefix_of_proj2 : LEMMA prefix(t1, proj(t, A)) IFF EXISTS t2 : prefix(t2, t) AND t1 = proj(t2, A) proj_twice : LEMMA proj(proj(t, A), B) = proj(t, intersection(A, B)) %------------------------------------------------ % product: for parallel composition % -> prod(A)(t1, t2, t) holds if % % t is a possible interleaving of t1 and t2 % with events in A synchronized %------------------------------------------------- prod(A)(t1, t2, t) : RECURSIVE bool = CASES t OF null : null?(t1) AND null?(t2), cons(x, y) : IF A(x) THEN cons?(t1) AND cons?(t2) AND car(t1) = x AND car(t2) = x AND prod(A)(cdr(t1), cdr(t2), y) ELSE (cons?(t1) AND car(t1) = x AND prod(A)(cdr(t1), t2, y)) OR (cons?(t2) AND car(t2) = x AND prod(A)(t1, cdr(t2), y)) ENDIF ENDCASES MEASURE length(t) prod_commutes : LEMMA prod(A)(t1, t2, t) IFF prod(A)(t2, t1, t) proj_prod1 : LEMMA prod(A)(t1, t2, t) IMPLIES proj(t1, A) = proj(t, A) proj_prod2 : LEMMA prod(A)(t1, t2, t) IMPLIES proj(t2, A) = proj(t, A) prod_null1 : LEMMA prod(A)(t1, null, t) IMPLIES t1 = t prod_null2 : LEMMA prod(A)(null, t2, t) IMPLIES t2 = t prod_null3 : LEMMA proj(t, A) = null IMPLIES prod(A)(t, null, t) prod_null4 : LEMMA proj(t, A) = null IMPLIES prod(A)(null, t, t) prefix_prod : LEMMA prod(A)(t1, t2, t) AND prefix(u, t) IMPLIES EXISTS u1, u2 : prefix(u1, t1) AND prefix(u2, t2) AND prod(A)(u1, u2, u) prod_assoc1 : LEMMA prod(A)(t1, t2, u) AND prod(A)(u, t3, t) IMPLIES EXISTS u1 : prod(A)(t1, u1, t) AND prod(A)(t2, t3, u1) prod_assoc2 : LEMMA prod(A)(t1, u, t) AND prod(A)(t2, t3, u) IMPLIES EXISTS u1 : prod(A)(t1, t2, u1) AND prod(A)(u1, t3, t) prod_assoc : LEMMA (EXISTS u : prod(A)(t1, t2, u) AND prod(A)(u, t3, t)) IFF (EXISTS u : prod(A)(t1, u, t) AND prod(A)(t2, t3, u)) prod_fullset : LEMMA prod(fullset)(t1, t2, u) IFF t1 = u AND t2 = u free_prod_left : LEMMA prod(emptyset)(t, null, t) free_prod_right : LEMMA prod(emptyset)(null, t, t) %--------------------------- % sigma(t) : events of t %-------------------------- sigma : [trace -> set[T]] = list2set sigma_equiv : LEMMA sigma(t) = { a | member(a, t) } sigma_null : LEMMA sigma(null) = emptyset sigma_cons : LEMMA sigma(cons(a, t)) = add(a, sigma(t)) sigma_empty : LEMMA empty?(sigma(t)) IFF t = null sigma_append : LEMMA sigma(append(t1, t2)) = union(sigma(t1), sigma(t2)) sigma_add : LEMMA sigma(add(t, a)) = add(a, sigma(t)) sigma_prefix : LEMMA prefix(t1, t2) IMPLIES subset?(sigma(t1), sigma(t2)) sigma_proj : LEMMA sigma(proj(t, A)) = intersection(sigma(t), A) sigma_prod : LEMMA prod(A)(t1, t2, t) IMPLIES sigma(t) = union(sigma(t1), sigma(t2)) sigma_prod_inter1 : LEMMA prod(A)(t1, t2, t) IMPLIES intersection(sigma(t), A) = intersection(sigma(t1), A) sigma_prod_inter2 : LEMMA prod(A)(t1, t2, t) IMPLIES intersection(sigma(t), A) = intersection(sigma(t2), A) %---------------------- % Empty projections %---------------------- null_proj_equiv : LEMMA proj(t, B) = null IFF disjoint?(sigma(t), B) null_proj_subset : LEMMA subset?(A, B) AND proj(t, B) = null IMPLIES proj(t, A) = null null_proj_union : LEMMA proj(t, union(A, B)) = null IFF proj(t, A) = null AND proj(t, B) = null null_proj_prod : LEMMA prod(A)(t1, t2, t) IMPLIES (proj(t, B) = null IFF proj(t1, B) = null AND proj(t2, B) = null) null_proj_prod1 : LEMMA prod(A)(t1, t2, t) AND proj(t, B) = null IMPLIES proj(t1, B) = null null_proj_prod2 : LEMMA prod(A)(t1, t2, t) AND proj(t, B) = null IMPLIES proj(t2, B) = null null_proj_prod3 : LEMMA prod(A)(t1, t2, t) AND subset?(B, A) AND proj(t1, B) = null IMPLIES proj(t, B) = null null_proj_prod4 : LEMMA prod(A)(t1, t2, t) AND subset?(B, A) AND proj(t2, B) = null IMPLIES proj(t, B) = null END traces $$$traces.prf (|traces| (|prefix_equiv| "" (AUTO-REWRITE "prefix" "append") (("" (SKOLEM!) (("" (GROUND) (("1" (SKOLEM!) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOLEM!) (("2" (ASSERT) (("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOLEM!) (("3" (INST + "t!1") (("3" (REPLACE*) (("3" (EXPAND "append" 1 1) (("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOLEM!) (("4" (INST + "t!1") (("4" (APPLY-EXTENSIONALITY) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_prefix| "" (SKOLEM!) (("" (REWRITE "prefix_equiv") NIL NIL)) NIL) (|prefix_null| "" (SKOLEM!) (("" (REWRITE "prefix_equiv") (("" (GROUND) NIL NIL)) NIL)) NIL) (|cons_prefix| "" (SKOLEM!) (("" (GROUND) (("1" (REWRITE "prefix_equiv") NIL NIL) ("2" (REWRITE "prefix_equiv" -) NIL NIL) ("3" (REWRITE "prefix_equiv" +) NIL NIL)) NIL)) NIL) (|prefix_append1| "" (EXPAND "prefix") (("" (SKOSIMP*) (("" (REPLACE*) (("" (INST + "append(t!1, t3!1)") (("" (REWRITE "append_assoc") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_append2| "" (EXPAND "prefix") (("" (SKOSIMP*) (("" (REPLACE*) (("" (INST + "t!2") (("" (REWRITE "append_assoc") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_add1| "" (AUTO-REWRITE "add" "prefix") (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|prefix_add2| "" (AUTO-REWRITE "add" "prefix_append1") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|length_prefix| "" (GRIND :DEFS NIL :REWRITES ("prefix" "length_append[T]")) NIL NIL) (|prefix_reflexive| "" (AUTO-REWRITE "append_null" "prefix") (("" (AUTO-REWRITE "append_null[T]" "prefix") (("" (SKOLEM!) (("" (ASSERT) (("" (INST + "null") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_transitive| "" (EXPAND "prefix") (("" (SKOSIMP*) (("" (REPLACE*) (("" (INST + "append(t!1, t!2)") (("" (REWRITE "append_assoc") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_antisymmetric| "" (EXPAND "prefix") (("" (SKOSIMP*) (("" (AUTO-REWRITE "length_zero[T]" "append_null[T]") (("" (CASE "length(t!1) = 0") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (USE "length_append[T]") (("2" (USE "length_append[T]" ("l1" "t2!1")) (("2" (STOP-REWRITE "length_zero[T]") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|proj_null| "" (GRIND) NIL NIL) (|proj_cons| "" (AUTO-REWRITE "proj" "filter[T]") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|proj_append| "" (SKOLEM 1 ("A!1" _ "t!2")) (("" (INDUCT-AND-SIMPLIFY "t1") NIL NIL)) NIL) (|proj_add| "" (AUTO-REWRITE "proj_append" "add") (("" (SKOLEM!) (("" (ASSERT) (("" (AUTO-REWRITE "proj" "filter" "append_null[T]") (("" (LIFT-IF) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|proj_prefix| "" (GRIND :EXCLUDE ("append" "proj") :REWRITES ("proj_append")) NIL NIL) (|proj_reverse| "" (INDUCT "t") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP*) (("2" (AUTO-REWRITE "reverse" "proj_append") (("2" (ASSERT) (("2" (AUTO-REWRITE "proj" "filter" "append_null[T]") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_of_proj| "" (SKOLEM + ("A!1" _ _)) (("" (AUTO-REWRITE "proj" "filter" "prefix_null" "null_prefix" "cons_prefix") (("" (INDUCT "t") (("1" (SKOSIMP) (("1" (ASSERT) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (LIFT-IF) (("2" (GROUND) (("1" (REWRITE "prefix_equiv") (("1" (GROUND) (("1" (INST + "null") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? -) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "cons(cons1_var!1, t2!1)") (("2" (ASSERT) (("2" (APPLY-EXTENSIONALITY) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST? -) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "cons(cons1_var!1, t2!1)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_of_proj2| "" (GRIND :DEFS NIL :IF-MATCH NIL :REWRITES ("prefix_of_proj" "proj_prefix")) NIL NIL) (|proj_twice| "" (SKOLEM 1 ("A!1" "B!1" _)) (("" (INDUCT-AND-SIMPLIFY "t") NIL NIL)) NIL) (|prod_TCC1| "" (GRIND) NIL NIL) (|prod_TCC2| "" (GRIND) NIL NIL) (|prod_TCC3| "" (GRIND) NIL NIL) (|prod_commutes| "" (SKOLEM!) (("" (CASE "FORALL t1, t2, t : prod(A!1)(t1, t2, t) IMPLIES prod(A!1)(t2, t1, t)") (("1" (GRIND :IF-MATCH ALL) NIL NIL) ("2" (DELETE 2) (("2" (AUTO-REWRITE "prod" "proj" "filter") (("2" (INDUCT "t") (("1" (SKOSIMP) (("1" (ASSERT) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (CASE "A!1(cons1_var!1)") (("1" (ASSERT) (("1" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (SPLIT -) (("1" (FLATTEN) (("1" (INST? - :WHERE 3) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (INST? - :WHERE 2) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|proj_prod1| "" (INDUCT-AND-SIMPLIFY "t") NIL NIL) (|proj_prod2| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (FORWARD-CHAIN "proj_prod1") NIL NIL)) NIL)) NIL) (|prod_null1| "" (INDUCT-AND-SIMPLIFY "t") (("" (APPLY-EXTENSIONALITY) NIL NIL)) NIL) (|prod_null2| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (FORWARD-CHAIN "prod_null1") NIL NIL)) NIL)) NIL) (|prod_null3| "" (INDUCT-AND-SIMPLIFY "t") NIL NIL) (|prod_null4| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (REWRITE "prod_null3") NIL NIL)) NIL)) NIL) (|prefix_prod| "" (SKOLEM + ("A!1" _ _ _ _)) (("" (AUTO-REWRITE "prod" "prefix_null" "null_prefix") (("" (INDUCT "t") (("1" (SKOSIMP) (("1" (ASSERT) (("1" (INST + "null" "null") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (CASE "null?(u!1)") (("1" (DELETE -2 -3) (("1" (INST + "null" "null") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REWRITE "prefix_equiv") (("2" (ASSERT) (("2" (GROUND) (("1" (INST? -) (("1" (INST? -) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST + "cons(cons1_var!1, u1!1)" "cons(cons1_var!1, u2!1)") (("1" (ASSERT) (("1" (AUTO-REWRITE "prefix_equiv") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST? -) (("2" (INST? -) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "cons(cons1_var!1, u1!1)" "u2!1") (("2" (ASSERT) (("2" (REWRITE "prefix_equiv" +) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST? -) (("3" (INST? -) (("3" (ASSERT) (("3" (SKOSIMP) (("3" (INST + "u1!1" "cons(cons1_var!1, u2!1)") (("3" (ASSERT) (("3" (REWRITE "prefix_equiv" +) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_assoc1| "" (SKOLEM 1 ("A!1" _ _ _ _ _)) (("" (AUTO-REWRITE "prod") (("" (INDUCT "t") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (REDUCE :IF-MATCH NIL) (("1" (INST?) (("1" (INST?) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST + "cons(cons1_var!1, u1!1)") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST? -) (("2" (INST? -) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST? -) (("3" (INST? -) (("3" (ASSERT) (("3" (SKOSIMP) (("3" (INST + "cons(cons1_var!1, u1!1)") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (INST? -) (("4" (INST? -) (("4" (ASSERT) (("4" (SKOSIMP) (("4" (INST + "cons(cons1_var!1, u1!1)") (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_assoc2| "" (SKOLEM 1 ("A!1" _ _ _ _ _)) (("" (AUTO-REWRITE "prod") (("" (INDUCT "t") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (REDUCE :IF-MATCH NIL) (("1" (INST - "cdr(t1!1)" "cdr(t2!1)" "cdr(t3!1)" "cdr(u!1)") (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST + "cons(cons1_var!1, u1!1)") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST - "cdr(t1!1)" "t2!1" "t3!1" "u!1") (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "cons(cons1_var!1, u1!1)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST - "t1!1" "cdr(t2!1)" "t3!1" "cdr(u!1)") (("3" (ASSERT) (("3" (SKOSIMP) (("3" (INST + "cons(cons1_var!1, u1!1)") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (INST - "t1!1" "t2!1" "cdr(t3!1)" "cdr(u!1)") (("4" (ASSERT) (("4" (SKOSIMP) (("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_assoc| "" (REDUCE :IF-MATCH NIL) (("1" (USE "prod_assoc1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (USE "prod_assoc2") (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|prod_fullset| "" (AUTO-REWRITE "fullset" "prod") (("" (INDUCT "u") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (SPLIT) (("1" (FLATTEN) (("1" (ASSERT) (("1" (INST?) (("1" (GROUND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (ASSERT) (("2" (INST?) (("2" (REPLACE*) (("2" (DELETE -) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|free_prod_left| "" (INDUCT-AND-SIMPLIFY "t") NIL NIL) (|free_prod_right| "" (INDUCT-AND-SIMPLIFY "t") NIL NIL) (|sigma_equiv| "" (INDUCT-AND-SIMPLIFY "t") (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (REPLACE*) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|sigma_null| "" (GRIND) NIL NIL) (|sigma_cons| "" (GRIND) NIL NIL) (|sigma_empty| "" (GRIND) NIL NIL) (|sigma_append| "" (INDUCT-AND-SIMPLIFY "t1") (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (REPLACE*) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|sigma_add| "" (EXPAND "add" 1 1) (("" (SKOLEM!) (("" (REWRITE "sigma_append") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_prefix| "" (AUTO-REWRITE "prefix" "sigma_append") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL NIL)) NIL)) NIL) (|sigma_proj| "" (INDUCT-AND-SIMPLIFY "t") (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (REPLACE*) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (APPLY-EXTENSIONALITY :HIDE? T) (("3" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|sigma_prod| "" (INDUCT-AND-SIMPLIFY "t") (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (REPLACE*) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (IFF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (APPLY-EXTENSIONALITY :HIDE? T) (("3" (IFF) (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("4" (REPLACE*) (("4" (APPLY-EXTENSIONALITY :HIDE? T) (("4" (IFF) (("4" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_prod_inter1| "" (SKOSIMP) (("" (FORWARD-CHAIN "proj_prod1") (("" (REWRITE "sigma_proj" :DIR RL) (("" (REWRITE "sigma_proj" :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_prod_inter2| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (FORWARD-CHAIN "sigma_prod_inter1") NIL NIL)) NIL)) NIL) (|null_proj_equiv| "" (SKOLEM + ("B!1" _)) (("" (INDUCT-AND-SIMPLIFY "t") NIL NIL)) NIL) (|null_proj_subset| "" (AUTO-REWRITE "null_proj_equiv") (("" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_union| "" (AUTO-REWRITE "null_proj_equiv") (("" (SKOLEM!) (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_prod| "" (AUTO-REWRITE "null_proj_equiv") (("" (SKOSIMP) (("" (ASSERT) (("" (FORWARD-CHAIN "sigma_prod") (("" (REPLACE*) (("" (DELETE -) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_prod1| "" (SKOSIMP) (("" (USE "null_proj_prod") (("" (GROUND) NIL NIL)) NIL)) NIL) (|null_proj_prod2| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (FORWARD-CHAIN "null_proj_prod1") NIL NIL)) NIL)) NIL) (|null_proj_prod3| "" (AUTO-REWRITE "null_proj_equiv") (("" (SKOSIMP) (("" (ASSERT) (("" (FORWARD-CHAIN "sigma_prod_inter1") (("" (DELETE -2) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) (("" (CASE "intersection(sigma(t!1), A!1)(x!1)") (("1" (REPLACE -2) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_prod4| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (FORWARD-CHAIN "null_proj_prod3") NIL NIL)) NIL)) NIL)) $$$processes.pvs % % Processes with alphabet T % (trace semantics) % processes [ T : TYPE ] : THEORY BEGIN IMPORTING traces S : VAR setof[trace[T]] A : VAR setof[T] t, t1, t2 : VAR trace[T] %=================================================== % process: non-empty, prefix closed set of traces %=================================================== prefix_closed(S) : bool = FORALL t1, t2 : prefix(t1, t2) AND S(t2) IMPLIES S(t1) process : TYPE = { S | S(null) AND prefix_closed(S) } P, P1, P2 : VAR process SP : VAR set[process] a : VAR T %=================== % Process algebra %=================== %----------- % Stop[T] %----------- Stop : process = { t | t = null }; %------------------ % Bounded choice %------------------ \/(P1, P2) : process = union(P1, P2) %--------------------- % Unbounded choice %--------------------- Choice(SP) : process = { t | null?(t) OR EXISTS (P : (SP)) : P(t) }; %----------- % a >> P %----------- >> (a, P) : process = { t | null?(t) OR EXISTS (t1 : (P)) : t = cons(a, t1) } %------------------------ % Parallel composition %------------------------ Par(A)(P1, P2) : process = { t | EXISTS (t1 : (P1)), (t2 : (P2)) : prod(A)(t1, t2, t) }; %---------------- % Interleaving %---------------- //(P1, P2) : process = Par(emptyset)(P1, P2) %========================== % sigma(P) = events of P %========================== sigma(P) : setof[T] = { a | EXISTS (t : (P)) : sigma(t)(a) } END processes $$$processes.prf (|processes| (|Stop_TCC1| "" (GRIND :EXCLUDE ("prefix") :REWRITES ("prefix_null[T]")) NIL NIL) (|vee_TCC1| "" (GRIND :EXCLUDE ("prefix")) NIL NIL) (|Choice_TCC1| "" (GRIND :EXCLUDE "prefix" :IF-MATCH NIL) (("1" (DELETE 2) (("1" (EXPAND "prefix") (("1" (REDUCE) NIL NIL)) NIL)) NIL) ("2" (REDUCE) NIL NIL)) NIL) (|doublegreaterp_TCC1| "" (GRIND :DEFS NIL :REWRITES ("prefix_closed") :IF-MATCH NIL) (("1" (REWRITE "prefix_equiv") NIL NIL) ("2" (REWRITE "prefix_equiv") (("2" (GROUND) (("2" (INST? -) (("2" (ASSERT) (("2" (INST + "cdr(t1!1)") (("2" (APPLY-EXTENSIONALITY) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Par_TCC1| "" (SKOLEM-TYPEPRED) (("" (PROP) (("1" (EXPAND "prod") (("1" (INST + "null" "null") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (EXPAND "prefix_closed") (("2" (SKOSIMP*) (("2" (FORWARD-CHAIN "prefix_prod") (("2" (SKOSIMP) (("2" (INST? - :WHERE -1) (("2" (INST? - :WHERE -2) (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL))