[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Identical antecedent and consequent



Hi,

I am in the process of doing a proof, and I have arrived at a point where
the term in the antecedent is identical to the term in the consequent. I
expected the proof to be completed by this, but PVS does not agree. Can
you please tell me the conditions under which identical terms in the
antecedent and the consequent does not represent the completion of the
proof? 

The exact terms are shown below. The pvs dump file is also attached. The
theorem I am proving is process_rep_th6 in the OneComponent theory. 

process_rep_th6 :  

[-1]  process_rep(choice(c)(InitStates(c), choice_F))
  |-------
[1]   process_rep(choice(c)(InitStates(c), choice_F))

After further simplification, I come to:

process_rep_th6.1.1 :  

[-1]  (I(c)(car(s1!1)))
[-2]  O(c)(car(s1!1), post!1)
[-3]  choice_traces(c)(post!1)(append(cdr(s1!1), s2!1))
[-4]  (I(c)(car(s1!1)))
[-5]  O(c)(car(s1!1), post!2)
[-6]  choice_traces(c)(post!2)(cdr(s1!1))
[-7]  InitStates(c)(car(s1!1))
  |-------
[1]   O(c)(car(s1!1), post!2)
{2}   null?(s1!1)

Note that the antecedent -5 is identical to the consequent 1, but still
PVS does not consider the proof to be complete. 

Any help in this regard is highly appreciated. Thanks. Bye.

-- 
Best Wishes,
	-- Murali
***************************************************************************
Murali Rangarajan # rmurali@ececs.uc.edu # http://www.ececs.uc.edu/~rmurali
Knowledge Based Software Engineering Lab # Phone(Work): (785) 864 7759

"Try not. Do. Or do not. There is no try."  -- Yoda, Jedi Master 
***************************************************************************

$$$OneComponent.pvs
%%-----------------------------------------------------------------------------
%% Copyright (c) 1997 Ohio Board of Regents and the University of
%% Cincinnati.  All rights reserved.
%%
%% UC MAKES NO REPRESENTATIONS OR WARRANTIES ABOUT THE SUITABILITY OF 
%% THE SOFTWARE, EITHER EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED
%% TO THE IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A
%% PARTICULAR PURPOSE, OR NON-INFRINGEMENT.  UC SHALL NOT BE LIABLE
%% FOR ANY DAMAGES SUFFERED BY LICENSEE AS A RESULT OF USING,
%% RESULT OF USING, MODIFYING OR DISTRIBUTING THIS SOFTWARE OR ITS
%% DERIVATIVES.
%%
%% By using or copying this Software, Licensee agrees to abide by the
%% intellectual property laws, and all other applicable laws of the
%% U.S., and the terms of this license.
%%
%% author: Murali Rangarajan
%% rmurali@ececs.uc.edu
%%
%% Revision Information:
%% $Id: OneComponent.pvs,v 1.7 2000/06/01 21:22:52 rmurali Exp $
%%
%%-----------------------------------------------------------------------------
%% $Log: OneComponent.pvs,v $
%% Revision 1.7  2000/06/01 21:22:52  rmurali
%% Finished all proofs upto OneComponent. Comitting because I am going to
%% make large-scale modifications to incorporate Component type.
%%
%% Revision 1.6  2000/05/21 16:46:53  rmurali
%% I am partway through the proofs. I am commiting it just so I don't lose
%% anything.
%%
%% Revision 1.5  1999/08/21 21:13:27  rmurali
%% BasicVHDLTypes.pvs : Commented out the "event" operator over the
%% 		various types. This is now available in the theory
%% 		TypeSpecificInfo.
%% OneComponent.pvs : Commented otu the "equal" operator.
%% TypeSpecificInfo.pvs : This new theory contains all the operators that
%% 		need to be defined over all the types. This theory is
%% 		automatically included for each type in the system.
%%
%% Revision 1.4  1999/07/22 16:55:34  rmurali
%% Changed the Store model. Now, the store is only a simple theory
%% without any 'features'. The type Store and the constant empty:Store
%% are passed to OneComponent and all generated theories as parameters so
%% that there is always only one Store type in the system at all times.
%%
%% Revision 1.3  1999/06/02 19:12:58  rmurali
%% Part of the previous commit - fixed some bugs in the semantics of
%% VSPEC.
%% The modSet parts are still buggy. They are currently being commented
%% out in the generated theories.
%%
%%
%%-----------------------------------------------------------------------------
%% Description:
%% This theory is used to define the semantics of a single VSPEC component.
%% Initially, this trait and Chalin's LCLAux were identical copies of one
%% another (all they did was include ModAndTrash).  Now, this trait also
%% includes the CSP traits and defines some of the operators used in these
%% traits.  The reason this trait was created is so many of the proofs in
%% the implies section of the trait would be available for all VSPEC
%% components.
%%-----------------------------------------------------------------------------

OneComponent [Store: TYPE+, empty: Store, Component: TYPE+, c: Component
] : THEORY 
BEGIN
    ASSUMING
    IMPORTING OneComponentDeclarations[Store, empty, Component]
    initstates_psi_as: ASSUMPTION subset?(InitStates(c), Psi(c))
    ENDASSUMING

	% ---------Operator definitions from OneComponent---------

  %% Note:  I, O, modSet, Psi, InitStates and maintain_state are
  %% introduced in OneComponentDeclarations and must be fully defined by the
  %% including theory.  The definition of these must meet certain assumptions
  %% defined in the Assumptions part.  The need to state these
  %% assumptions is the reason these operator declarations were moved to
  %% OneComponentDeclarations.  F is also introduced in OneComponentDecls
  %% because traits such as TwoComponent need to make assumptions about it.

	%% Define that the unsorted value of some object is strongly equal in
	%% the two states passed in.  strongEq is defined in Chalin's traits.
	%%
	%% This operator makes it easier to state the maintain_state operator.
	%% equal(o: Obj, pre, post: Store): bool = 
	%%		strongEq(sortAttr(o), val(pre, o), val(post, o))

    % Predicate to define a subset of Psi
    subset_psi?(a:alphabet): bool = subset?(a, Psi(c))

	% ---------Variable declarations for use in theorems and axioms---------

	pre, post, x, y: VAR Store
	t: VAR trace
	a: VAR alphabet
    s: VAR (subset_psi?)
%	o: VAR Obj
	p: VAR process

	% ---------Axioms from OneComponent---------

	%% This provides part of the definition of the event attribute semantics.
	modset_ax1: AXIOM ( member(t, traces(entity_process(c))) AND
		member(pre, t) AND O(c)(pre, post)) => modSet_event(c)(post)

	%% All elements of a trace that satisfy the precondition have an
	%% associated post state that satisfies the functional requirements.
	f_ax1: AXIOM 
		(member(t, traces(entity_process(c))) AND member(pre, t) 
		 AND (t /= null) AND I(c)(pre)) => EXISTS post: F(c)(pre, post)

	%% If the inputs don't change, F still holds.
	f_ax3: AXIOM NOT input_event(c)(x) => F(c)(x, x)

    % Every state except the last state satisfies the pre-condition
    entity_process_ax1: AXIOM (member(t, traces(entity_process(c))) 
        AND member(x, t) AND (t /= null)) => (I(c)(x) <=> (x /= last(t)))

 	%% This is here just to make choice_F easier to read and
 	%% understand.
    %  The condition subset?(s, Psi) is embedded in the type of 's'.
 	choice_traces_ax1: AXIOM member(t, choice_traces(c)(post)) = 
        (member(x,s) <=> maintain_state(c)(post, x))
        AND member(t, traces(choice(c)(s, choice_F)))

	%% This defines the set LegalStates
	legalstates_ax1: AXIOM member(x, LegalStates(c)) <=> 
		(EXISTS (t: trace): member(t, traces(entity_process(c))) 
            AND member(x, t))
	
	%% F is defined almost like F in the Doug Smith's DRIO model.
    %  This has been transferred to OneComponentDeclarations so as to 
    %  obtain a constructive specification.
% 	f_ax4: AXIOM F(pre, post) = 
% 		(I(pre) => O(pre, post) )

	%% This is the function that defines choice in the CSP model.
% 	choice_f_ax1: AXIOM alpha(choice_F(pre)) = Psi
% 	choice_f_ax2: AXIOM member(t, traces(choice_F(pre))) = 
% 		IF (I(pre)) 
% 		THEN (EXISTS post : F(pre, post) AND member(t, choice_traces(post)))
% 		ELSE (t = null)
% 		ENDIF

	% ---------Theorems from OneComponent---------

	%% Psi and choice_F form a well defined alphabet.
	well_def_alpha_th1: THEOREM well_def_alpha(Psi(c), choice_F(c))

	%% Any subset of Psi and choice_F form a well defined alphabet.
	well_def_alpha_th2: THEOREM 
        subset?(a, Psi(c)) => well_def_alpha(a, choice_F(c))

	%% This means InitStates is a well defined alphabet.
	%% This can only be proved after InitStates is proved to be a
	%% subset of Psi in the generated theory.
	well_def_alpha_th3: THEOREM well_def_alpha(InitStates(c), choice_F(c))

	%% The entity_process is a process_rep.
	process_rep_th6: THEOREM process_rep(entity_process(c))

	%% The alphabet of the entity process is Psi.
	entity_process_th1: THEOREM alpha(entity_process(c)) = Psi(c)

	%% If s is a subset of Psi, all traces of choice(s) are also traces
	%% of Choice(Psi).
	choice_th1: THEOREM 
		(subset?(a, Psi(c)) AND member(t, traces(choice(c)(a, choice_F)))) =>
		member(t, traces(choice(c)(Psi(c), choice_F)))

    % Simplified version of the theorem f_th1
	f_th11: THEOREM (t /= null and member(t, traces(entity_process(c)))
			AND I(c)(car(t))) => EXISTS post: F(c)(car(t), post)

	%% All elements of a trace that don't satisfy the precondition must be
	%% the last element of the trace.
	entity_process_th2: THEOREM
		(member(t, traces(entity_process(c))) AND member(pre, t) 
			AND NOT I(c)(pre)) => (pre = nth(t, length(t) - 1))

END OneComponent

$$$OneComponent.prf
(|OneComponent| (|entity_process_ax1_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|well_def_alpha_th1| "" (EXPAND "well_def_alpha")
  (("" (EXPAND "choice_F")
    (("" (INST 1 "Psi(c)")
      (("" (SPLIT)
        (("1" (SKOSIMP*) NIL NIL)
         ("2" (ASSERT)
          (("2" (LEMMA "subset_reflexive[Store]")
            (("2" (INST -1 "Psi(c)") NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|well_def_alpha_th2| "" (SKOSIMP*)
  (("" (EXPAND "well_def_alpha")
    (("" (EXPAND "choice_F")
      (("" (INST 1 "Psi(c)")
        (("" (SPLIT) (("1" (SKOSIMP*) NIL NIL) ("2" (PROPAX) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|well_def_alpha_th3| "" (EXPAND "well_def_alpha")
  (("" (EXPAND "choice_F")
    (("" (INST 1 "Psi(c)")
      (("" (SPLIT)
        (("1" (SKOSIMP*) NIL NIL)
         ("2" (LEMMA "initstates_psi_as") (("2" (PROPAX) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|process_rep_th6| "" (EXPAND "entity_process")
  (("" (LEMMA "choice_ax1")
    (("" (INST -1 "InitStates(c)")
      (("" (ASSERT) (("" (POSTPONE) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|entity_process_th1| "" (EXPAND "entity_process")
  (("" (EXPAND "choice") (("" (PROPAX) NIL NIL)) NIL)) NIL)
 (|choice_th1| "" (SKOSIMP*)
  (("" (EXPAND "choice") (("" (GRIND) NIL NIL)) NIL)) NIL)
 (|f_th11_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|f_th11| "" (SKOSIMP*)
  (("" (EXPAND "entity_process")
    (("" (EXPAND "choice")
      (("" (EXPAND "choice_F")
        (("" (SIMPLIFY)
          (("" (EXPAND "list2set")
            (("" (EXPAND "emptyset")
              (("" (ASSERT)
                (("" (EXPAND "member" -1)
                  (("" (FLATTEN)
                    (("" (SKOSIMP*) (("" (INST 2 "post!1") NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|entity_process_th2_TCC1| "" (SKOSIMP *)
  (("" (EXPAND "length")
    (("" (EXPAND "member")
      (("" (ASSERT)
        (("" (LIFT-IF)
          (("" (CASE "null?(t!1)")
            (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|entity_process_th2| "" (SKOSIMP*)
  (("" (LEMMA "entity_process_ax1")
    (("" (INST -1 "t!1" "pre!1")
      (("" (CASE "t!1 /= null")
        (("1" (ASSERT)
          (("1" (EXPAND "last" 1) (("1" (GRIND) NIL NIL)) NIL)) NIL)
         ("2" (LEMMA "member_null[Store]")
          (("2" (INST -1 "t!1" "pre!1") (("2" (ASSERT) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))


$$$Choice.pvs
%%-----------------------------------------------------------------------------
%% Copyright (c) 1996 Ohio Board of Regents and the University of
%% Cincinnati.  All rights reserved.
%%
%% UC MAKES NO REPRESENTATIONS OR WARRANTIES ABOUT THE SUITABILITY OF 
%% THE SOFTWARE, EITHER EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED
%% TO THE IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A
%% PARTICULAR PURPOSE, OR NON-INFRINGEMENT.  UC SHALL NOT BE LIABLE
%% FOR ANY DAMAGES SUFFERED BY LICENSEE AS A RESULT OF USING,
%% RESULT OF USING, MODIFYING OR DISTRIBUTING THIS SOFTWARE OR ITS
%% DERIVATIVES.
%%
%% By using or copying this Software, Licensee agrees to abide by the
%% intellectual property laws, and all other applicable laws of the
%% U.S., and the terms of this license.
%%
%% author: Murali Rangarajan
%% rmurali@ececs.uc.edu	
%%
%% Revision Information:
%% $Id: Choice.pvs,v 1.5 2000/06/01 21:22:52 rmurali Exp $
%%
%% Description:
%% This theory defines the CSP choice operator.  Camilleri used a higher-order
%% function to do this. This theory tries to mimic it. This can be combined 
%% with the CSP theory, but it is seperated here to facilitate better 
%% understanding.
%%-----------------------------------------------------------------------------

Choice [event : TYPE+, Component: TYPE+,
    (IMPORTING CSPBasics[event], functions[event, process]) 
    f: [Component -> [event -> process]], 
    Psi: [Component -> alphabet]] : THEORY
BEGIN

    % This function returns the predicate to be used with "choice" operator. 
    % The definition is the same as that of well_def_alpha.

%     pred_fun(a:alphabet, f:[event -> process]) : pred[alphabet] = 
%         EXISTS (a1 : alphabet): (FORALL (x: event): 
%             member(x,a) => alpha(f(x)) = a1) AND subset?(a, a1)

%     pred_fun: pred[[alphabet, [event -> process]]] = 
%         (LAMBDA (a:alphabet, f: [event -> process]): 
%              EXISTS (a1 : alphabet): (FORALL (x: event): 
%                  member(x,a) => alpha(f(x)) = a1) AND subset?(a, a1))

%        LAMBDA EXISTS (a1 : alphabet): (FORALL (x: event): 
%            member(x,a) => alpha(f(x)) = a1) AND subset?(a, a1)

	% ---------Operator definitions from Choice---------

    well_def_alpha(a:alphabet, f: [event -> process]) : bool = 
         EXISTS (a1 : alphabet): (FORALL (x: event): 
             member(x,a) => alpha(f(x)) = a1) AND subset?(a, a1)

    % choice chooses an event from the alphabet randomly, and returns the 
    % process obtained by applying the function f to that chosen event.
    % The alphabet can be a subset of Psi only in the very first state.
    % After that (starting from the first partition), the alphabet of the
    % resulting process is always Psi.
	choice(c: Component)(a: alphabet, 
        f: [Component -> [event -> process]]): process = 
          (# alpha := Psi(c),
            traces := {t:trace | t = null or 
              (member(car(t), a) and member(cdr(t), traces(f(c)(car(t)))))} #)

	% ---------Variable declarations for use in theorems and axioms---------

	e, x: VAR event
	a, new_a: VAR alphabet
    a1: VAR alphabet
    c: Component
%    f: [event -> process]
    p: process
    t: VAR trace

    % ---------Definition of the choice operator---------

    % Defines the choice operator
%     choice_ax1 : AXIOM
%         well_def_alpha(a,f) => 
%             (alpha(choice(a,f)) = choose(pred_fun(a,f))) AND
%             (traces(choice(a,f)) = {t | t = null or 
%                 (member(car(t), a) and member(cdr(t), traces(f(car(t)))))})

    % When the predicate well_def_alpha holds for some function f and
    % alphabet a, the above representation of the choice operator is 
    % well defined
    choice_ax1 : AXIOM process_rep(choice(c)(a,f))
%        well_def_alpha(a,f) => process_rep(choice(a,f))

    % The following two axioms cannot be proved because we do not have 
    % any properties over the function f.	
	f_ax1 : AXIOM
		(member(e,a) and process_rep(f(c)(e))) => process_rep(choice(c)(a,f))

    f_ax2 : AXIOM member(e,a) => (alpha(choice(c)(a,f)) = alpha(f(c)(e)))

	% ---------Theorems from Choice---------

    % Since well_def_alpha is no longer critical to our semantics, the 
    % following theorems are no longer relavant.

    % This property does not hold in general, but holds in VSPEC semantics.
% 	well_def_alpha_th1 : THEOREM
% 		member(e,a) => member(e, alpha(choice(c)(a,f)))

% 	well_def_alpha_th1 : THEOREM
% 		(well_def_alpha(a,f) AND member(e,a)) =>
% 			member(e, alpha(choice(a,f)))

% 	well_def_alpha_th2 : THEOREM
% 		(well_def_alpha(a,f) AND member(e,a) => process_rep(f(e))) 
% 		=> process_rep(choice(a,f))

%     well_def_alpha_th3 : THEOREM
%         (well_def_alpha(a,f) and member(e,a)) =>
%             (alpha(choice(a,f)) = alpha(f(e)))

END Choice








$$$Choice.prf
(|Choice| (|choice_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|well_def_alpha_th1| "" (SKOSIMP*)
  (("" (EXPAND "choice") (("" (PROPAX) NIL NIL)) NIL)) NIL)
 (|well_def_alpha_th2| "" (SKOSIMP*)
  (("" (EXPAND "choice")
    (("" (EXPAND "process_rep")
      (("" (ASSERT)
        (("" (SKOSIMP*)
          (("" (GRIND)
            (("1" (POSTPONE) NIL NIL) ("2" (POSTPONE) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|well_def_alpha_th3| "" (SKOSIMP*)
  (("" (EXPAND "choice") (("" (GRIND) (("" (POSTPONE) NIL NIL)) NIL))
    NIL))
  NIL))


$$$CSPBasics.pvs

%%-------------------------------------------------------------------------
%% Conversion of Albert J. Camilleri's HOL axiomatization of CSP into LSL.
%% Albert John Camilleri,"Mechanizing CSP Trace Theory in HOL"
%% IEEE Transactions on Software Engineering,16(9):993-1004, September 1990
%%-------------------------------------------------------------------------

CSPBasics [event : TYPE+] : THEORY
BEGIN

	% ---------Type definitions from CSPAssumptions---------

	alphabet : TYPE = set[event]
	trace : TYPE = list[event]
	trace_set : TYPE = set[trace]
	nonempty_trace : TYPE = {t: trace | length(t) > 0}

	% ---------Type Definitions from CSPBasics---------

	process : TYPE = [# alpha: alphabet, traces: trace_set #]
	
    % Needed by the parallel operator. Added by rmurali.
    process_set : TYPE = set[process]

	% ---------General Operator Definitions---------
	
	precat(e: event, t: trace) : trace =
		cons(e, t)

    % Proofs involving postcat are getting really complex. So, I am
    % commenting them out until I findout I need them.
	%postcat(t:trace, e: event) : trace = append(t, cons(e, null))

	% ---------CSP Operator Definitions from CSPBasics---------

	%% Define restriction of a trace to a set of events.
	restrict(t:trace, a:alphabet): RECURSIVE trace = 
		IF t = null 
			THEN null 
			ELSE IF member(car(t),a) 
					THEN cons(car(t),restrict(cdr(t),a))
					ELSE restrict(cdr(t),a)
				ENDIF
		ENDIF
	MEASURE length(t)

	%% Define set of all possible traces of events in an alphabet.
	star(a:alphabet) : trace_set = { t:trace | restrict(t,a) = t }

% 	%% Define when a process tuple actually represents a process.
% 	process_rep(p: process) : bool = 
% 		subset?(traces(p),star(alpha(p))) AND
% 		member(null,traces(p)) AND
% 		(FORALL (s1,s2:trace): member(append(s1,s2),traces(p)) => 
% 				member(s1,traces(p)))

	%% Define when a process tuple actually represents a process.
	process_rep(p: process) : bool = 
		(FORALL (s1,s2:trace): member(append(s1,s2),traces(p)) => 
				member(s1,traces(p)))

	% ---------Variable declarations for use in theorems and axioms---------

	e, e1, e2: VAR event
	s, t: VAR trace
	a: VAR alphabet
	p, q: VAR process
	
    % ---------Axioms-------------------------------------------------------

    process_ax1: AXIOM member(null, traces(p))

    % All the events in all the traces of a process have to be from the 
    % alphabet of the process
    process_ax2: AXIOM 
        member(e,t) and member(t, traces(p)) => member(e, alpha(p))

    % Supplimentary axiom to define valid traces of a process
    process_ax3: AXIOM member(t, traces(p)) => (restrict(t, alpha(p)) = t)

    % This property (of lists in general, actually) should be easy to
    % prove, but it is not so in reality. So, I have added it as an axiom.
    trace_ax01 : AXIOM 
        (cons(e1, s) = cons(e2, t)) => ((e1 = e2) and (s = t))

    % alternative definition for star
    star_defn_ax : AXIOM
        star(a) = {t | member(e,t) => member(e,a)}

	% ---------Theorems from CSPAssumptions---------
	% In this trait, || represents concatenation operator on lists. 
	% None of the theorems in the implies section is reflected here as
	% they are all standard properties of sets and sequences. 
	

	% ---------Theorems from CSPBasics---------

	member_th0 : THEOREM
		member(t, star(a)) AND member(e,a) => member(cons(e,t), star(a))

	member_th02 : THEOREM
		member(e,a) AND member(cons(e,t),star(a)) => member(t, star(a))

	member_th1 : THEOREM 
		member(e,restrict(t,a)) => member(e,a)

    % This theorem, in conjunction with theorem member_restrict_th22, is
    % needed for proving member_th2.
    % The new proof for member_th2 no longer needs these. It uses the 
    % alternate definition for star to arrive at a simple solution.
    member_restrict_th21: THEOREM
        (restrict(s,a) = t) => (member(e,t) => member(e,a))

    % The following two theorems are needed for proving the theorem
    % member_restrict_th22.
    length_restrict_th221: THEOREM
        length(restrict(s,a)) <= length(s)

    length_trace_th222: THEOREM
        (s = t) => (length(s) = length(t))

    member_restrict_th22: THEOREM
        (restrict(cons(e,s), a) = cons(e,s)) => member(e,a)

    % The proof for this theorem uses the alternate definition for star
    % given as an axiom.
	member_th2 : THEOREM
		member(e,t) AND member(t,star(a)) => member(e,a)	

	% Prove that everything in the traces of a process is also in the
	% alphabet of the process.
	% This theorem uses the new axiom "process_ax2"
	member_th3 : THEOREM
		member(t,traces(p)) AND member(e,t)
		=> member(e,alpha(p))

	% Prove something in the restriction of a trace will also be in the
	% restriction of that trace precatted with something else.
	member_th4 : THEOREM
		member(e1,restrict(t,a))
		=> member(e1,restrict(cons(e2,t),a))

	% Prove something in a trace that is in some alphabet will also be in
	% the trace that results from restricting the trace to the alphabet.
	member_th5 : THEOREM
		member(e,t) AND member(e,a) => member(e,restrict(t,a))

    length_trace_th61: THEOREM
        length(restrict(s,a)) < length(cons(e,s))        

	% Prove if the restriction of a trace equals the trace, everything
	% in the trace must by in the alphabet.
	member_th6 : THEOREM
		(restrict(t,a)=t)	=> (member(e,t)	=> member(e,a))

	% Prove if the restriction of a trace does not equal the trace, there
	% must be something in the trace that is not in the alphabet.
	member_th7 : THEOREM
		NOT (restrict(t,a)=t) => (EXISTS (e3 : event) : 
				(member(e3,t) AND NOT member(e3,a)))

	%% Prove restriction applies to right half of concatenated trace.
	restrict_th1 : THEOREM
		( restrict(append(s,t),a) = append(s,t) )
			=> ( restrict(t,a) = t)
	
	%% Prove restriction applies to left half of concatenated trace.
	restrict_th2 : THEOREM
		restrict(append(s,t),a) = append(s,t)
			=> restrict(s,a) = s

    reverse_null_th3111: THEOREM reverse[trace](null) = null

    reverse_cons_th3112: THEOREM reverse(cons(e,null)) /= null

    reverse_th3113: THEOREM (t /= null) => (reverse(t) /= null)

    reverse_cons_th3114: THEOREM reverse(cons(e,t)) /= null

    % Proofs involving postcat and reverse are getting really complicated.
    % So, I am commenting them out now, and will do the proofs
    % if I find out that I need to use the operators. 

%     cons_reverse_th311: THEOREM
%         cons(e1, reverse(cons(e2, reverse(t)))) =
%             reverse(cons(e2, reverse(cons(e1, t))))

%     % The original definition of postcat. It was complicated to prove it
%     % using reverse. Therefore, changed the definition and added the
%     % old definition as theorem. 
%     postcat_th31: THEOREM postcat(t, e) = reverse(cons(e, reverse(t)))

% 	%% Prove law similar to law that defines restriction.  This fact just
% 	%% uses postcat as the generator.
% 	restrict_th3 : THEOREM
% 		restrict(postcat(t,e),a) = 
% 			IF member(e,a)
% 				THEN	postcat(restrict(t,a),e)
% 				ELSE  restrict(t,a)
% 			ENDIF
		
	%% Prove restriction distributes through concatenation.
	restrict_th4 : THEOREM
		restrict(append(s,t),a) = append(restrict(s,a),restrict(t,a))

	%% This and the definition of process_rep implies the following fact
	%% which is needed in one of the CSP proofs.
	mem_rest_th1 : THEOREM
		( member(restrict(append(s,t),alpha(p)),traces(p))
		  AND process_rep(p) ) =>
				member(restrict(s,alpha(p)),traces(p))

    restrict_th51: THEOREM
        (restrict(cons(e,t), a) = cons(e,t)) => 
            (member(e, a) and (restrict(t,a) = t))

    restrict_th52: THEOREM
        (member(e,a) and (restrict(t,a) = t)) => 
            (restrict(cons(e,t), a) = cons(e,t))

	%% Prove how restriction interacts with car and cdr.
	restrict_th5 : THEOREM
        ( (restrict(cons(e,t), a) = cons(e,t)) <=>
			  (member(car(cons(e,t)), a) AND 
                  (restrict(cdr(cons(e,t)),a) = cdr(cons(e,t)))))

    % A different of the axiom process_ax02 needed to prove the 
    % theorem restrict_th6
    process_th61: THEOREM member(t, traces(p)) => 
                              (member(e,t) => member(e, alpha(p)))

%     restrict_th62: THEOREM (member(e,t) => member(e, a)) => 
%                               (restrict(t, a) = t)

    member_cons_th631: THEOREM member(e, cons(e,t))

    % Restrict from processes
    restrict_th6: THEOREM
        (member(e, alpha(p)) and member(t, traces(p))) => 
            (restrict(cons(e, t), alpha(p)) = cons(e,t))

    % This will simplify the process_rep function definition.
    process_th01: THEOREM
        subset?(traces(p), star(alpha(p)))
		
END CSPBasics

$$$CSPBasics.prf
(|CSPBasics| (|restrict_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|restrict_TCC2| "" (TERMINATION-TCC) NIL NIL)
 (|restrict_TCC3| "" (TERMINATION-TCC) NIL NIL)
 (|member_th0| "" (SKOSIMP *)
  (("" (EXPAND "member")
    (("" (EXPAND "star")
      (("" (ASSERT)
        (("" (EXPAND "restrict" 1)
          (("" (LIFT-IF)
            (("" (ASSERT)
              (("" (EXPAND "member" 1) (("" (PROPAX) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|member_th02| "" (SKOSIMP *)
  (("" (EXPAND "member")
    (("" (EXPAND "star")
      (("" (EXPAND "restrict" -2)
        (("" (EXPAND "member" -2)
          (("" (ASSERT)
            (("" (LEMMA "trace_ax01")
              (("" (INST -1 "e!1" "e!1" "restrict(t!1, a!1)" "t!1")
                (("" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|member_th1| "" (INDUCT "t")
  (("1" (SKOSIMP*)
    (("1" (EXPAND "restrict")
      (("1" (EXPAND "member") (("1" (PROPAX) NIL NIL)) NIL)) NIL))
    NIL)
   ("2" (SKOSIMP *)
    (("2" (SKOSIMP *)
      (("2" (EXPAND "restrict" -2)
        (("2" (ASSERT)
          (("2" (INST -1 "a!1" "e!1")
            (("2" (CASE "member(cons1_var!1, a!1)")
              (("1" (ASSERT)
                (("1" (EXPAND "member" -2) (("1" (PROPAX) NIL NIL))
                  NIL))
                NIL)
               ("2" (ASSERT) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|member_restrict_th21| "" (INDUCT "s")
  (("1" (SKOSIMP*) (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)) NIL)
   ("2" (SKOSIMP*)
    (("2" (INST -1 "a!1" "e!1" "t!1")
      (("2" (EXPAND "restrict" -2)
        (("2" (LIFT-IF)
          (("2" (CASE "member(cons1_var!1, a!1)")
            (("1" (ASSERT)
              (("1" (REPLACE -2 -3 RL)
                (("1" (EXPAND "member" -3)
                  (("1" (LEMMA "member_th1")
                    (("1" (INST -1 "a!1" "e!1" "cons2_var!1")
                      (("1" (ASSERT) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (ASSERT) NIL NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|length_restrict_th221| "" (INDUCT "s")
  (("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
   ("2" (SKOSIMP*)
    (("2" (INST -1 "a!1")
      (("2" (EXPAND "restrict" 1)
        (("2" (ASSERT)
          (("2" (CASE "member(cons1_var!1, a!1)")
            (("1" (ASSERT)
              (("1" (EXPAND "length" 1) (("1" (ASSERT) NIL NIL)) NIL))
              NIL)
             ("2" (ASSERT)
              (("2" (EXPAND "length" 2)
                (("2" (ASSERT)
                  (("2" (EXPAND "length" -1)
                    (("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|length_trace_th222| "" (SKOSIMP*) (("" (GRIND) NIL NIL)) NIL)
 (|member_restrict_th22| "" (INDUCT "s")
  (("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
   ("2" (SKOSIMP*)
    (("2" (INST -1 "a!1" "e!1")
      (("2" (EXPAND "restrict" -2)
        (("2" (LIFT-IF)
          (("2" (ASSERT 1)
            (("2" (DO-REWRITE)
              (("2" (GRIND)
                (("1" (LEMMA "trace_ax01")
                  (("1"
                    (INST -1 "cons1_var!1" "e!1"
                     " restrict(cons2_var!1, a!1)"
                     "cons(cons1_var!1, cons2_var!1)")
                    (("1" (ASSERT) NIL NIL)) NIL))
                  NIL)
                 ("2" (LEMMA "length_trace_th222")
                  (("2"
                    (INST -1 "restrict(cons2_var!1, a!1)"
                     "cons(e!1, cons(cons1_var!1, cons2_var!1))")
                    (("2" (ASSERT)
                      (("2" (LEMMA "length_restrict_th221")
                        (("2" (INST -1 "a!1" "cons2_var!1")
                          (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|member_th2| "" (SKOSIMP*)
  (("" (LEMMA "star_defn_ax")
    (("" (INST -1 "a!1" "e!1")
      (("" (REPLACE -1) (("" (ASSERT) (("" (GRIND) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|member_th3| "" (SKOSIMP*)
  (("" (ASSERT)
    (("" (LEMMA "process_ax2")
      (("" (INST -1 "e!1" "p!1" "t!1") (("" (GRIND) NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|member_th4| "" (INDUCT "t")
  (("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
   ("2" (SKOSIMP*) (("2" (INST?) (("2" (GRIND) NIL NIL)) NIL)) NIL))
  NIL)
 (|member_th5| "" (INDUCT "t")
  (("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
   ("2" (SKOSIMP*) (("2" (INST?) (("2" (GRIND) NIL NIL)) NIL)) NIL))
  NIL)
 (|length_trace_th61| "" (SKOSIMP*)
  (("" (EXPAND "length")
    (("" (ASSERT)
      (("" (GRIND)
        (("" (LEMMA "length_restrict_th221")
          (("" (INST?) (("" (GRIND) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|member_th6| "" (INDUCT "t")
  (("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
   ("2" (SKOSIMP*)
    (("2" (INST?)
      (("2" (EXPAND "member" -3)
        (("2" (SPLIT)
          (("1" (PROPAX) NIL NIL)
           ("2" (ASSERT)
            (("2" (REPLACE -2 * RL)
              (("2" (EXPAND "restrict" -1)
                (("2" (LEMMA "length_trace_th222")
                  (("2"
                    (INST -1 "restrict(cons2_var!1, a!1)"
                     "cons(e!1, cons2_var!1)")
                    (("2" (LEMMA "length_trace_th61")
                      (("2" (INST?)
                        (("2" (INST -1 "e!1") (("2" (GRIND) NIL NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("3" (GRIND)
            (("1" (LEMMA "length_trace_th222")
              (("1"
                (INST -1 "restrict(cons2_var!1, a!1)"
                 "cons(cons1_var!1, cons2_var!1)")
                (("1" (ASSERT)
                  (("1" (LEMMA "length_restrict_th221")
                    (("1" (INST -1 "a!1" "cons2_var!1")
                      (("1" (GRIND) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (GRIND)
              (("2" (LEMMA "trace_ax01")
                (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
              NIL)
             ("3" (LEMMA "length_trace_th222")
              (("3"
                (INST -1 "restrict(cons2_var!1, a!1)"
                 "cons(cons1_var!1, cons2_var!1)")
                (("3" (ASSERT)
                  (("3" (LEMMA "length_restrict_th221")
                    (("3" (INST -1 "a!1" "cons2_var!1")
                      (("3" (ASSERT) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|member_th7| "" (INDUCT "t")
  (("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
   ("2" (SKOSIMP*)
    (("2" (INST -1 "a!1")
      (("2" (ASSERT)
        (("2" (EXPAND "restrict" 1)
          (("2" (SPLIT)
            (("1" (SKOSIMP*)
              (("1" (INST 3 "e3!1")
                (("1" (EXPAND "member" 3)
                  (("1" (ASSERT)
                    (("1" (EXPAND "member" 1) (("1" (PROPAX) NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (CASE "member(cons1_var!1, a!1)")
              (("1" (ASSERT) NIL NIL)
               ("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|restrict_th1| "" (INDUCT "s")
  (("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
   ("2" (SKOSIMP*)
    (("2" (INST -1 "a!1" "t!1")
      (("2" (SPLIT)
        (("1" (PROPAX) NIL NIL)
         ("2" (EXPAND "append" -1)
          (("2" (EXPAND "restrict" -1)
            (("2" (ASSERT)
              (("2" (CASE "member(cons1_var!1, a!1)")
                (("1" (ASSERT)
                  (("1" (LEMMA "trace_ax01")
                    (("1"
                      (INST -1 "cons1_var!1" "cons1_var!1"
                       "restrict(append(cons2_var!1, t!1), a!1)"
                       "append(cons2_var!1, t!1)")
                      (("1" (ASSERT) NIL NIL)) NIL))
                    NIL))
                  NIL)
                 ("2" (ASSERT)
                  (("2" (LEMMA "length_trace_th222")
                    (("2"
                      (INST -1
                       "restrict(append(cons2_var!1, t!1), a!1)"
                       "cons(cons1_var!1, append(cons2_var!1, t!1))")
                      (("2" (LEMMA "length_restrict_th221")
                        (("2"
                          (INST -1 "a!1" "append(cons2_var!1, t!1)")
                          (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|restrict_th2| "" (INDUCT "s")
  (("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
   ("2" (SKOSIMP*)
    (("2" (INST -1 "a!1" "t!1")
      (("2" (ASSERT)
        (("2" (EXPAND "append" -2)
          (("2" (EXPAND "restrict" -2)
            (("2" (CASE "member(cons1_var!1, a!1)")
              (("1" (ASSERT)
                (("1" (LEMMA "trace_ax01")
                  (("1"
                    (INST -1 "cons1_var!1" "cons1_var!1"
                     " restrict(append(cons2_var!1, t!1), a!1)"
                     " append(cons2_var!1, t!1)")
                    (("1" (ASSERT)
                      (("1" (EXPAND "restrict" 1)
                        (("1" (GRIND) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (ASSERT)
                (("2" (LEMMA "length_trace_th222")
                  (("2"
                    (INST -1 "restrict(append(cons2_var!1, t!1), a!1)"
                     "cons(cons1_var!1, append(cons2_var!1, t!1))")
                    (("2" (LEMMA "length_restrict_th221")
                      (("2" (INST -1 "a!1" "append(cons2_var!1, t!1)")
                        (("2" (GRIND) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|reverse_null_th3111| "" (EXPAND "reverse") (("" (PROPAX) NIL NIL))
  NIL)
 (|reverse_cons_th3112| "" (SKOSIMP*)
  (("" (LEMMA "length_trace_th222")
    (("" (INST -1 "reverse(cons(e!1, null))" "null")
      (("" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL)
 (|reverse_th3113| "" (SKOSIMP*)
  (("" (LEMMA "length_reverse" ("l" "t!1")) (("" (GRIND) NIL NIL))
    NIL))
  NIL)
 (|reverse_cons_th3114| "" (INDUCT "t")
  (("1" (SKOSIMP*)
    (("1" (LEMMA "reverse_cons_th3112")
      (("1" (INST -1 "e!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   ("2" (SKOSIMP*)
    (("2" (INST -1 "cons1_var!1")
      (("2" (EXPAND "reverse" -2)
        (("2" (EXPAND "append") (("2" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|restrict_th4| "" (INDUCT "s")
  (("1" (SKOSIMP*)
    (("1" (EXPAND "append")
      (("1" (EXPAND "restrict") (("1" (PROPAX) NIL NIL)) NIL)) NIL))
    NIL)
   ("2" (SKOSIMP*)
    (("2" (INST -1 "a!1" "t!1")
      (("2" (EXPAND "append" 1)
        (("2" (EXPAND "restrict" 1)
          (("2" (ASSERT)
            (("2" (LIFT-IF)
              (("2" (LIFT-IF) (("2" (GRIND) NIL NIL)) NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|mem_rest_th1| "" (SKOSIMP*)
  (("" (EXPAND "process_rep")
    (("" (ASSERT)
      (("" (LEMMA "restrict_th4")
        (("" (INST -1 "alpha(p!1)" "s!1" "t!1")
          (("" (REPLACE -1 -2)
            (("" (ASSERT)
              ((""
                (INST -3 "restrict(s!1, alpha(p!1))"
                 "restrict(t!1, alpha(p!1))")
                (("" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|restrict_th51| "" (INDUCT "t")
  (("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
   ("2" (SKOSIMP*)
    (("2" (INST -1 "a!1" "e!1")
      (("2" (EXPAND "restrict" -2)
        (("2" (CASE "member(e!1, a!1)")
          (("1" (ASSERT)
            (("1" (LEMMA "trace_ax01")
              (("1"
                (INST -1 "e!1" "e!1"
                 "restrict(cons(cons1_var!1, cons2_var!1), a!1)"
                 "cons(cons1_var!1, cons2_var!1)")
                (("1" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL)
           ("2" (ASSERT)
            (("2" (LEMMA "length_trace_th222")
              (("2"
                (INST -1
                 "restrict(cons(cons1_var!1, cons2_var!1), a!1)"
                 "cons(e!1, cons(cons1_var!1, cons2_var!1))")
                (("2" (LEMMA "length_restrict_th221")
                  (("2"
                    (INST -1 "a!1" "cons(cons1_var!1, cons2_var!1)")
                    (("2" (GRIND) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|restrict_th52| "" (INDUCT "t")
  (("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
   ("2" (SKOSIMP*)
    (("2" (INST -1 "a!1" "e!1")
      (("2" (ASSERT)
        (("2" (EXPAND "restrict" 1)
          (("2" (REPLACE -3 1) (("2" (PROPAX) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|restrict_th5| "" (SKOSIMP*)
  (("" (LEMMA "restrict_th51")
    (("" (INST -1 "a!1" "e!1" "t!1")
      (("" (LEMMA "restrict_th52")
        (("" (INST -1 "a!1" "e!1" "t!1")
          (("" (ASSERT) (("" (GRIND) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|process_th61| "" (SKOSIMP*)
  (("" (LEMMA "process_ax2")
    (("" (INST -1 "e!1" "p!1" "t!1") (("" (GRIND) NIL NIL)) NIL)) NIL))
  NIL)
 (|restrict_th62| "" (INDUCT "t")
  (("1" (POSTPONE) NIL NIL)
   ("2" (SKOSIMP*)
    (("2" (EXPAND "restrict" 1)
      (("2" (INST -1 "a!1" "e!1")
        (("2" (LIFT-IF)
          (("2" (SIMPLIFY)
            (("2" (SPLIT)
              (("1" (SPLIT)
                (("1" (PROP)
                  (("1" (REPLACE -3 1) (("1" (PROPAX) NIL NIL)) NIL)
                   ("2" (POSTPONE) NIL NIL))
                  NIL)
                 ("2" (POSTPONE) NIL NIL))
                NIL)
               ("2" (POSTPONE) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|member_cons_th631| "" (SKOSIMP*)
  (("" (ASSERT) (("" (EXPAND "member") (("" (PROPAX) NIL NIL)) NIL))
    NIL))
  NIL)
 (|restrict_th6| "" (SKOSIMP*)
  (("" (LEMMA "process_ax2")
    (("" (INST -1 "e!1" "p!1" "t!1")
      (("" (EXPAND "restrict")
        (("" (ASSERT)
          (("" (GRIND)
            (("" (LEMMA "process_ax3")
              (("" (INST -1 "p!1" "t!1") (("" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|process_th01| "" (SKOSIMP*)
  (("" (EXPAND "star")
    (("" (LEMMA "process_ax3")
      (("" (INST -1 "p!1" "_") (("" (GRIND) NIL NIL)) NIL)) NIL))
    NIL))
  NIL))


$$$CSP.pvs

%%-------------------------------------------------------------------------
%% Conversion of Albert J. Camilleri's HOL axiomatization of CSP into LSL.
%% Albert John Camilleri,"Mechanizing CSP Trace Theory in HOL"
%% IEEE Transactions on Software Engineering,16(9):993-1004, September 1990
%%-------------------------------------------------------------------------

CSP [event : TYPE+] : THEORY
BEGIN

	IMPORTING CSPBasics[event]

	% ---------Type Definitions from CSP---------

	% ---------CSP Operator Definitions from CSP---------

	stop(a:alphabet) : process = (# alpha := a, traces := singleton(null) #)

	run(a:alphabet) : process = (# alpha := a, traces := star(a) #)

	prefix(e: event, p: process): process

% 		IF member(e, alpha(p)) 
% 		THEN (# alpha := alpha(p), 
% 			traces := {t:trace | t = null OR 
% 					(car(t)=e AND member(cdr(t),traces(p))) } #)
% 		ELSE p
% 		ENDIF

% 	after(p: process, t: trace): process =
% 		(# alpha := alpha(p),
% 			traces := {s: trace | member(append(t,s), traces(p))} #)

	% The parallel operator, defined over a set of processes!
    parallel(ps:process_set) : process

    % Define a predicate that identifies non-null traces
    nonnull?(s:trace):bool = NOT null?(s)
    
    % The last operator returns the last event in a trace. It is just 
    % a short-cut to make some of the theorems more readable.
    last(s: (nonnull?)) : event = nth(s, length(s) - 1)

	% ---------Variable declarations for use in theorems and axioms---------

	e: VAR event
	s, t: VAR trace
    ts: VAR trace_set
	a,b : VAR alphabet
	p, q: VAR process
    ps : VAR process_set

    % Utility functions to define the parallel operator

    % This function returns the set of all the events in the alphabets 
    % of all the processes in the given process_set.
    union_alpha(ps: process_set): alphabet =
        {e: event | EXISTS (p:process): member(p, ps) and member(e, alpha(p))}

    % This function returns the set of all the traces closed over
    % all the set of all events in the alphabets of all the processes in 
    % the given process_set.
    star_union_alpha(ps: process_set): trace_set = 
        {t | member(t, star(union_alpha(ps)))}

%        {t | member(t, star(a)) and a = {b | b = alpha(p) and member(p,ps)}}

    % ---------Axioms defining the parallel composition operator-----------

    parallel_ax1 : AXIOM
        alpha(parallel(ps)) = union_alpha(ps)

    parallel_ax2 : AXIOM
        (member(t, traces(parallel(ps))) and member(p, ps)) => 
                member(restrict(t, alpha(p)), traces(p))

    parallel_ax3: AXIOM 
        subset?(traces(parallel(ps)), star(alpha(parallel(ps))))

    % This cannot be proved from the available facts.
    parallel_ax4: AXIOM (member(p, ps) and process_rep(p)) => 
                process_rep(parallel(ps))

%  = {t | (member(t, star_union_alpha(ps)) and
%                 (member(p, ps) => member(restrict(t, alpha(p)), traces(p)))}

    prefix_ax1: AXIOM member(e, alpha(p)) => 
                  ( (alpha(prefix(e,p)) = alpha(p)) and
                    (traces(prefix(e,p)) = {t | t = null or
                               (car(t) = e and member(cdr(t), traces(p)))}))

    last_ax1: AXIOM (t /= null) => (last(t) = last(append(s,t)))

	% ---------Theorems from CSP---------

	process_rep_th1 : THEOREM
		process_rep(stop(a))

	process_rep_th2 : THEOREM
		process_rep(run(a))

    list_th31: THEOREM
        (t /= null) => cons(car(t), cdr(t)) = t

%     trace_th32: THEOREM
%         member(cdr(t), traces(p)) => (t /= null)

    % Uses "after". This is not needed for now...	
% 	process_rep_th4 : THEOREM 
% 		member(t, traces(p)) AND process_rep(p) =>
% 			process_rep(after(p,t))

	prefix_th2: THEOREM member(e, alpha(p)) AND process_rep(p) =>
			            process_rep(prefix(e, p))
	
    % This is wrong. This is not neccessarily the case.
%     parallel_th31: THEOREM 
%         (member(p,ps) and member(restrict(t,alpha(p)), traces(p))) =>
%             member(t, traces(parallel(ps)))
    
    % Theorems from TwoComponentAssumptions - they should really be here

    %% These two facts are used to prove that if something in sc does not
    %% satisfy I, that thing must be the last element of sc || tc.
    parallel_th1 : THEOREM
        member(e,s) => member(e, append(s,t))
    
    %This original version is worng ... 
%     parallel_th2 : THEOREM
%         ((s /= null) and member(last(append(s,t)),s)) => 
%             (last(append(s,t)) = last(s))

    %% This fact will be useful in bisimulation proofs of two components.
    alphabet_th1 : THEOREM
        (member(e,a) or member(e,b)) = 
            ((member(e,a) and not member(e,b)) or
             (member(e,b) and not member(e,a)) or
             (member(e,a) and member(e,b)))

END CSP		

$$$CSP.prf
(CSP
 (|last_TCC1| "" (SUBTYPE-TCC)
  (("" (EXPAND "length")
    (("" (EXPAND "length")
      (("" (ASSERT)
        (("" (LIFT-IF)
          (("" (ASSERT)
            (("" (CASE "null?(cdr(s!1))")
              (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|prefix_ax1_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|prefix_ax1_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|last_ax1_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|last_ax1_TCC2| "" (SUBTYPE-TCC)
  (("" (GRIND) (("" (EXPAND "append") (("" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL)
 (|process_rep_th1| "" (SKOSIMP*)
  (("" (EXPAND "process_rep")
    (("" (EXPAND "stop") (("" (GRIND) NIL NIL)) NIL)) NIL))
  NIL)
 (|process_rep_th2| "" (SKOSIMP*)
  (("" (EXPAND "process_rep")
    (("" (EXPAND "run")
      (("" (GRIND)
        (("" (LEMMA "restrict_th2")
          (("" (INST -1 "a!1" "s1!1" "s2!1") (("" (ASSERT) NIL NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|list_th31_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|list_th31| "" (SKOSIMP*)
  (("" (GRIND) (("" (APPLY-EXTENSIONALITY) NIL NIL)) NIL)) NIL)
 (|prefix_th2| "" (SKOSIMP*)
  (("" (LEMMA "prefix_ax1")
    (("" (INST -1 "e!1" "p!1")
      (("" (ASSERT)
        (("" (FLATTEN)
          (("" (EXPAND "process_rep")
            (("" (SKOSIMP*)
              (("" (INST -4 "cdr(s1!1)" "s2!1")
                (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|process_rep_th3| "" (SKOSIMP*)
  (("" (LEMMA "parallel_ax1")
    (("" (INST -1 "ps!1")
      (("" (LEMMA "parallel_ax2")
        (("" (INST -1 "p!1" "ps!1" "_")
          (("" (EXPAND "union_alpha")
            (("" (EXPAND "process_rep")
              (("" (SKOSIMP*)
                (("" (INST -1 "append(s1!1, s2!1)")
                  (("" (ASSERT)
                    (("" (LEMMA "restrict_th4")
                      (("" (INST -1 "alpha(p!1)" "s1!1" "s2!1")
                        (("" (REPLACE -1 -2)
                          ((""
                            (INST -5 "restrict(s1!1, alpha(p!1))"
                             "restrict(s2!1, alpha(p!1))")
                            (("" (ASSERT)
                              ((""
                                (GRIND)
                                (("" (POSTPONE) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|parallel_th1| "" (INDUCT "s")
  (("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
   ("2" (SKOSIMP*)
    (("2" (EXPAND "append" 1) (("2" (GRIND) NIL NIL)) NIL)) NIL))
  NIL)
 (|alphabet_th1| "" (SKOSIMP*) (("" (GRIND) NIL NIL)) NIL))


$$$Store.pvs
Store [Store: TYPE+, empty: Store] : THEORY
BEGIN
    % This theory is currently empty. We might want to add some properties 
    % here in the future.

END Store

$$$Store.prf
(|Store| (IMPORTING1_TCC1 "" (GRIND) (("" (POSTPONE) NIL)))
 (|indep_TCC1| "" (GRIND) NIL) (|indep_TCC2| "" (GRIND) NIL))

$$$OneComponentDeclarations.pvs
%%-----------------------------------------------------------------------------
%% Copyright (c) 1997 Ohio Board of Regents and the University of
%% Cincinnati.  All rights reserved.
%%
%% UC MAKES NO REPRESENTATIONS OR WARRANTIES ABOUT THE SUITABILITY OF 
%% THE SOFTWARE, EITHER EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED
%% TO THE IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A
%% PARTICULAR PURPOSE, OR NON-INFRINGEMENT.  UC SHALL NOT BE LIABLE
%% FOR ANY DAMAGES SUFFERED BY LICENSEE AS A RESULT OF USING,
%% RESULT OF USING, MODIFYING OR DISTRIBUTING THIS SOFTWARE OR ITS
%% DERIVATIVES.
%%
%% By using or copying this Software, Licensee agrees to abide by the
%% intellectual property laws, and all other applicable laws of the
%% U.S., and the terms of this license.
%%
%% author: Murali Rangarajan
%% rmurali@ececs.uc.edu
%%
%% Revision Information:
%% $Id$
%%
%%-----------------------------------------------------------------------------
%% $Log$
%%
%%
%%-----------------------------------------------------------------------------
%% Description:
%% This theory contains all the declarations used by the OneComponent theory.
%% These are placed here as I needed a separate theory to declare InitStates
%% and Psi so that they can be used in the assuming clause, and I decided to 
%% put all the other declarations here as well.%%-----------------------------------------------------------------------------

OneComponentDeclarations [Store: TYPE+, empty: Store, Component: TYPE+] : THEORY
BEGIN

    IMPORTING Store[Store, empty], CSP[Store] 

	%% Including theory must define Psi as set of events that satisfy the
	%% component's sensitive to clause.
	Psi : [Component -> alphabet]

	%% Including trait must define I and O as the pre and postcondition.
	I : [Component -> [Store -> bool]]
	O : [Component -> [Store, Store -> bool]]

	%% F fully defined in OneComponent, but other theories need to make
	%% assumptions about it.
	%% F is defined almost like F in the Doug Smith's DRIO model.
	F(c: Component)(s1, s2: Store): bool = (I(c)(s1) => O(c)(s1, s2))

	%% Defined in the including trait.  Used to show that the post state of a
	%% trace Store shares some properties with the next Store in the trace.
	maintain_state(c: Component)(s1, s2: Store): bool

	%% This is used in the definition of choice_F, to make choice_F easier
    %% to read and understand.
	choice_traces(c: Component)(post: Store): trace_set 
%         = 
%         {t:trace | FORALL (a:alphabet, x:Store, post:Store): 
%             subset?(a, Psi) and 
%             (member(x, a) <=> maintain_state(post,x)) and 
%             member(t, traces(choice(a, choice_F)))}

	%% Function used by the choice operator.
    %% This is fully defined in the OneComponent theory.
	choice_F(c: Component)(pre: Store): process = (# alpha := Psi(c),
        traces := IF (I(c)(pre)) THEN 
                     {t:trace | EXISTS (post: Store): F(c)(pre, post) AND 
                                member(t, choice_traces(c)(post))}
                  ELSE null ENDIF #)

	IMPORTING Choice[Store, Component, choice_F, Psi]

 	% ---------Declarations from OneComponentDeclarations---------

	%% Including trait defines this as the set of states that the process
	%% can initially chose from.  *MUST* be a subset of Psi.
	InitStates : [Component -> alphabet]

	%% Process defined by this entity.
	entity_process(c: Component): process = choice(c)(InitStates(c), choice_F)

	%% Including trait defines modSet_event as there being an event on the
	%% value of at least one of the modified variables in the state passed in.
	modSet_event(c: Component)(s: Store): bool

	%% Including trait defines input_event as there being an event on the
	%% value of at least one of the input signals (including inout and buffer
	%% signals).
	input_event(c: Component)(s: Store): bool

	StoreSet : TYPE = set[Store]
	LegalStates(c: Component) : StoreSet

END OneComponentDeclarations