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

proofs involving epsilon



Hi,

I am writing the CSP theory in PVS (from Camilleri's work using HOL). I
have used the epsilon operator to define CSP's choice operator. But I am
not able to do any proofs involving the epsilon operator. I have looked at
John Rushby's reply to Darryl Dieckman's question in the archive. Though
choose is defined in terms of epsilon, a similar involving "typepred" does
not seem to work. I have attached the dump-file for the theory to this
mail. Can somebody please give me some pointers regarding how to do the
proof? I appreciate your help. Thanks. Bye.

PS: An example of a theorem involving the epsilon operator is
"well_def_alpha_th1". I am stuck with "member(e!1, epsilon(pred_fun(a!1,
f)))" in the consequent.

-- 
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 
***************************************************************************

$$$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.4 2000/05/21 16:46:53 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+] : THEORY
BEGIN

    IMPORTING CSPBasics[event], functions[event, process]

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

%        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.
	choice(a: alphabet, f: [event -> process]): process

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

	e, x: VAR event
	a, new_a: VAR alphabet
    a1: VAR alphabet
    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)) = epsilon(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_ax2 : AXIOM
        well_def_alpha(a,f) => process_rep(choice(a,f))
	
	% ---------Theorems from Choice---------

	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_ax1_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|choice_ax1_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|well_def_alpha_th1| "" (SKOSIMP*)
  (("" (LEMMA "choice_ax1")
    (("" (INST -1 "a!1")
      (("" (ASSERT)
        (("" (EXPAND "well_def_alpha")
          (("" (SKOSIMP*)
            (("" (INST -3 "e!1")
              (("" (ASSERT)
                (("" (REPLACE -1 1) (("" (POSTPONE) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          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))